search

runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

Duplications between llvm-backend and blockchain-k-plugin #383

Open gtrepta opened 3 years ago

gtrepta commented 3 years ago

runtime/json/json.cpp implements KoreHandler, KoreWriter, and write_json. In blockchain-k-plugin in plugin-c/json.cpp those are also being implemented, and slightly differently (I guess they're older versions?). Making a header file with declarations for these would allow the blockchain plugin to use them.

Inversely, runtime/json/json.cpp has a few structs declared which are provided by a header file in blockchain-k-plugin in plugin-c/k.h. These are zinj, stringinj, boolinj, jsonlist, json, and jsonmember, along with some extern "C" stuff. There are also declarations of global block * and blockheader constructs scattered around, even in firefly and iele-semantics. These are just typedefs and simple constructs but maybe it would be good to get them centralized somewhere with some basic utilities as a rudimentary "K API".

Baltoli commented 2 years ago

On first glance this duplication still exists - we should look further into the LLVM backend runtime exposing an API to semantics that need it.

gtrepta commented 2 years ago

runtime/header.h is basically the API, with typedefs and macros for handling the backend's data structures. It's probably sufficient enough to expose the json headers/functionality there.