Inject `ccopts` directly into `kevm_kompile` and fix some tests #2164

ehildenb · 2023-11-08T18:20:55Z

This PR is pulled out of: #2144

In particular:

A few proof tests that do not kompile properly with LLVM backend library because of shadowed module imports (due to symbolic attribute) are fixed.
The command kevm kompile ... is renamed to kevm kompile-spec ..., which is more representative of what it does. It defaults to --target haskell-booster, but only accepts haskell,haskell-booster,maude.
The kevm_kompile command no longer takes plugin_dir as an argument, but instead relies on user to pass in ccopts directly, which is all plugin_dir was used to calculate. This calculation is done at the call-site now instead, which makes kevm_kompile more generic (removes semantics specific component), and barely changes the call-sites.
The Makefile system is adjusted to make sure that evm-optimizations-spec.md is correctly updated on changes.
Adds a test to package/test-package.sh that was previously failing of using the booster on a proof. This was failing because we weren't correctly setting the plugin_dir (and thus ccopts) when using the booster at spec compile time. This was missed because the pytest testing harness did inject this option.

…ptimizations.md

…emmas

…backend

…le in symbolic module for LLVM

…mpile-spec} for more accurate usage

… ccopts directly

…e to plugin_dir being missing

kevm-pyk/src/kevm_pyk/kdist/plugin.py

kevm-pyk/src/kevm_pyk/__main__.py

kevm-pyk/src/kevm_pyk/kdist/plugin.py

…dency

kevm-pyk/src/kevm_pyk/kdist/plugin.py

* Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <devops@runtimeverification.com>

* lemmas on Boolean reasoning, set reasoning, map lookup, and keccak * Set Version: 1.0.277 * removing keccak lemmas that should not be upstreamed * addressing comments * Set Version: 1.0.278 * Set Version: 1.0.278 * corrections * removing ==Bool from expected files * Set Version: 1.0.279 * Set Version: 1.0.279 * Set Version: 1.0.309 * Set Version: 1.0.311 * updating expected outputs * Set Version: 1.0.312 * Set Version: 1.0.330 * Set Version: 1.0.334 * revisiting set simplifications * --amend * --amend * --amend * streamlining lookup simplifications * streamlining set simplifications * removing set reasoning entirely * Set Version: 1.0.336 * concretising set simplifications: * streamlining set simplifications * Set Version: 1.0.337 * even more concrete set simplifications * bringing old simplifications back * Set Version: 1.0.340 * resolving parsing ambiguities * --amend * --amend * Set Version: 1.0.341 * Set Version: 1.0.342 * Set Version: 1.0.343 * correction * syntax * --amend * Set Version: 1.0.349 * Set Version: 1.0.355 * Set Version: 1.0.356 * Set Version: 1.0.357 * Correctly ordered arguments in `typed_args` (#2174) * Correctly ordered arguments in `typed_args` * Set Version: 1.0.357 --------- Co-authored-by: devops <devops@runtimeverification.com> * Inject `ccopts` directly into `kevm_kompile` and fix some tests (#2164) * Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <devops@runtimeverification.com> * Fix circular import (#2179) * Fix circular import * Set Version: 1.0.359 --------- Co-authored-by: devops <devops@runtimeverification.com> * Move `--port` arguments to `rpc_args` (#2178) * Move `--port` arguments to `rpc_args` * Set Version: 1.0.359 * Set Version: 1.0.360 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Update dependency: deps/pyk_release (#2175) * deps/pyk_release: Set Version v0.1.501 * Set Version: 1.0.357 * kevm-pyk/: sync poetry files pyk version v0.1.501 * deps/k_release: sync release file version 6.1.14 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.359 * kevm-pyk/: sync poetry files pyk version v0.1.501 * Set Version: 1.0.361 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Update dependency: deps/pyk_release (#2181) * deps/pyk_release: Set Version v0.1.505 * kevm-pyk/: sync poetry files pyk version v0.1.505 * deps/k_release: sync release file version 6.1.20 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.362 --------- Co-authored-by: devops <devops@runtimeverification.com> * Set Version: 1.0.364 * Set Version: 1.0.364 * Set Version: 1.0.365 * Set Version: 1.0.372 * Set Version: 1.0.379 * adding tests * Set Version: 1.0.381 * normalising comparisons, adding keccak * reverting normalisation * removing equality simplification * Set Version: 1.0.382 * Set Version: 1.0.382 * bringing back comparison (but not equality) normalisation * bringing back equality normalisation * Set Version: 1.0.394 * Set Version: 1.0.396 * Set Version: 1.0.398 * removing unsound keccak simplifying assumptions * Set Version: 1.0.399 * Set Version: 1.0.400 * Set Version: 1.0.406 * Set Version: 1.0.407 * adding tests for comparison normalisation, removing keccak * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * ----- alignment * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

ehildenb added 11 commits November 8, 2023 17:59

Makefile: make sure evm-optimizations-spec is rebuilt on changes to o…

854e043

…ptimizations.md

kproj/optimizations: remove symbolic attribute on evm-optimizations-l…

b916af2

…emmas

tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM …

a8e2ef1

…backend

tests/specs/functional/infinite-gas-spec.k: allow import of main modu…

8a05603

…le in symbolic module for LLVM

kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => ko…

b1a68a0

…mpile-spec} for more accurate usage

README: update documentation

401a720

kevm-pyk/: all builds require plugin_dir, compute it directly

cbf038d

kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in…

7fbb01f

… ccopts directly

kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec

b942560

VERIFICATION: update documentation

3cc4cc0

Makefile: bring back --target argument

b9d6396

ehildenb self-assigned this Nov 8, 2023

Set Version: 1.0.343

e684c34

ehildenb mentioned this pull request Nov 8, 2023

Simplify and compact kompilation for Haskell vs Booster #2144

Merged

ehildenb and others added 7 commits November 8, 2023 18:25

test_prove: only add ccopts if were using the booster

33ba3d4

Merge remote-tracking branch 'upstream/master' into inject-ccopts

6664bcd

Set Version: 1.0.355

d8f372c

package/test-package: add previously failing test of using booster du…

831ff01

…e to plugin_dir being missing

kevm-pyk/__main__: use correct target for kompile-spec

d4d3e5f

Set Version: 1.0.356

0549bf3

Merge remote-tracking branch 'upstream/master' into inject-ccopts

c3805d6

ehildenb marked this pull request as ready for review November 13, 2023 16:36

ehildenb requested review from tothtamas28 and nwatson22 November 13, 2023 16:36

Set Version: 1.0.356

1e4ca0f

tothtamas28 reviewed Nov 13, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/kdist/plugin.py Outdated Show resolved Hide resolved

kevm-pyk/src/kevm_pyk/__main__.py Outdated Show resolved Hide resolved

kevm-pyk/plugin: correction from code review

97de1e7

tothtamas28 reviewed Nov 14, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/kdist/plugin.py Outdated Show resolved Hide resolved

ehildenb added 2 commits November 14, 2023 20:54

kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets

d5bceb6

kevm-pyk/: factor out generic run_kompile from kevm_kompile

75664dc

ehildenb and others added 5 commits November 14, 2023 21:03

kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts

8a671f2

Set Version: 1.0.357

23533c7

kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenn…

1767e88

…dency

Merge remote-tracking branch 'upstream/master' into inject-ccopts

afbce5b

Set Version: 1.0.357

b912b55

tothtamas28 approved these changes Nov 15, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/kdist/plugin.py Outdated Show resolved Hide resolved

kdist/plugin: drop self._deps

e813170

ehildenb added the automerge label Nov 15, 2023

devops and others added 3 commits November 15, 2023 16:11

Set Version: 1.0.358

5e2f742

Merge remote-tracking branch 'upstream/master' into inject-ccopts

a5e0579

Set Version: 1.0.358

875a416

rv-jenkins merged commit 0f62d62 into master Nov 15, 2023
11 checks passed

rv-jenkins deleted the inject-ccopts branch November 15, 2023 18:02

palinatolmach mentioned this pull request Nov 16, 2023

Update dependency: deps/kevm_release runtimeverification/kontrol#181

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Inject `ccopts` directly into `kevm_kompile` and fix some tests #2164

Inject `ccopts` directly into `kevm_kompile` and fix some tests #2164

ehildenb commented Nov 8, 2023 •

edited

Loading

Inject ccopts directly into kevm_kompile and fix some tests #2164

Inject ccopts directly into kevm_kompile and fix some tests #2164

Conversation

ehildenb commented Nov 8, 2023 • edited Loading

Inject `ccopts` directly into `kevm_kompile` and fix some tests #2164

Inject `ccopts` directly into `kevm_kompile` and fix some tests #2164

ehildenb commented Nov 8, 2023 •

edited

Loading