runtimeverification / mir-semantics

10 stars 3 forks source link

`KMIR` object and `llvm`/`haskell` dependencies #208

Closed dkcumming closed 9 months ago

dkcumming commented 1 year ago

Context

KMIR currently supports two backends (llvm and haskell) and three operations (parse, run, and prove). The relationship between these backends and the operations is:

Problem

Currently it is assumed that the haskell backend isn't needed, and that the llvm backend is needed. This is because previously the only operations offered were parse and run, however now that prove is supported this need to be changed.

Solution

I think there are three possible solutions:

  1. A simple but obtuse solution would be to require both backend's definitions are built and provided, this is not ideal as the user should only be required to provide what is necessary.
  2. Keep the structure mostly the same, and add conditional logic based on the operation. I think this is acceptable but also not ideal.
  3. Restructure and refactor KMIR to be more representative of KEVM. This would meant that KMIR directly inherits from both KProve and KPrint, instead of storing the KProve object and KMIR indirectly accessing _krun through a wrapper function. I believe doing this will also mean we do not have to call kmir init to create the syntax file for the glr parser in the nix build. I think this option is preferable, although it will take more time than 2.
yanliu18 commented 10 months ago

This issue might be closed as well. @dkcumming As the haskell_dir is now optional (I beliveve it is the same as you meant for conditional logic, no?). The left over issue is to generate the gen_glr_parser at build time, which is this issue #280 .

Are you OK with closing it? or We can wait till the refactor PR is merged (should need one more week).