search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
449 stars 149 forks source link

Haskell backend integration: `kprove` should save a `compiled.bin` for the generated `vdefinition.kore` #1137

Closed traiansf closed 4 years ago

traiansf commented 4 years ago

This is required to ensure that there would be a definition which can be used to unparse the output of the haskell backend.

Currently kprove does not save the composed definition (including the main module to be used for proofs). However, the output (esp. if not #True), might include syntax defined in that module.

This is the case, for example with the KWASM Lemmas ( https://github.com/kframework/wasm-semantics/blob/master/kwasm-lemmas.md ) which define helping predicates such as

     syntax Bool ::= #isByteMap ( ByteMap ) [function, functional, smtlib(isByteMap)]

test.zip

steps to reproduce:

kompile  --backend haskell  verif.k -d .
kprove test-spec.k   -d .

Output:

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.                              
Please rerun your program with the --debug flag to generate a stack trace, and                           
file a bug report at https://github.com/kframework/k/issues (key not found:                              
isA(_)_VERIFICATION_Bool_S)
traiansf commented 4 years ago

This might be related to Issue #703 (duplicate?)

denis-bogdanas commented 4 years ago

The compiled definition was going to be stored differently in PRs below, but they stagnate for 4 months already for various reasons. So please don't work on this until we sort out the PRs below. https://github.com/kframework/k/pull/892 https://github.com/kframework/k/pull/910