Remove legacy code and tests, use pyk runner more directly (#1977)

* package/test-package: update package testing script to run foundry proofs too * bin/kevm: drop solc-to-k and foundry-* commands directly through to pyk * bin/kevm, Makefile: remove kevm interpret command, no longer needed for tests * bin/kevm: simplify fallthrough to pyk * bin/kevm: use direct pyk prover always for run_proof * bin/kevm: simplify logic with removed options, pass them through to pyk * package/test-package: add search command test * bin/kevm: simplify more options * bin/kevm, scripts/kore-json: do not use dedicated kore -> json conversion * bin/kevm: more simplifications * bin/kevm: drop kompile straight through to pyk * Makefile: remove unexercised test-suites * Revert "package/test-package: add search command test" This reverts commit c6dfc55. * bin/kevm: remove search functionality * README: interpret => run * Set Version: 1.0.242 * Makefile: remove references to kore-json.py * Makefile, VERIFICATION, package/test-package, tests/specs/example/erc20-spec: remove mention of --pyk option * Makefile: run interactive tests with poetry enabled * Makefile: remove unused recipe * package/test-package: remove --pyk option * tests/failing: update expected output * bin/kevm: correctly handle kevm kompile * kevm-pyk/__main__: make sure we print out configuration on failed kruns too * bin/kevm: add foundry commands to ones passed through to kevm-pyk * flake.nix: include foundry in kevm-test target * package/test-package: disable foundry tests on nix ci * Set Version: 1.0.243 * Makefile: bring back proto-tester --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jul 28, 2023 · 33de9f0 · 33de9f0
1 parent f68af5b
commit 33de9f0
Show file tree

Hide file tree

Showing 13 changed files with 66 additions and 346 deletions.
diff --git a/Makefile b/Makefile
@@ -44,18 +44,13 @@ PLUGIN_FULL_PATH := $(abspath ${PLUGIN_SUBMODULE})
 export PLUGIN_FULL_PATH
 
 
-.PHONY: all clean distclean                                                                                        \
-        deps k-deps plugin-deps protobuf                                                                           \
-        poetry-env poetry shell kevm-pyk                                                                           \
-        build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm                \
-        test                                                                                                       \
-        test-integration test-conformance test-prove test-foundry-prove                                            \
-        test-vm test-rest-vm test-bchain test-rest-bchain                                                          \
-        test-node                                                                                                  \
-        test-prove-smoke test-klab-prove                                                                           \
-        test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search \
-        media media-pdf metropolis-theme                                                                           \
-        install uninstall
+.PHONY: all clean distclean install uninstall                                                            	\
+        deps k-deps plugin-deps protobuf proto-tester                                                      	\
+        poetry-env poetry shell kevm-pyk                                                                 	\
+        build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm      	\
+        test test-integration test-conformance test-prove test-foundry-prove test-prove-smoke            	\
+        test-vm test-rest-vm test-bchain test-rest-bchain test-node test-interactive test-interactive-run	\
+        media media-pdf metropolis-theme
 
 .SECONDARY:
 
@@ -70,8 +65,8 @@ distclean:
 # Non-K Dependencies
 # ------------------
 
-protobuf_out     := $(LOCAL_LIB)/proto/proto/msg.pb.cc
-protobuf:     $(protobuf_out)
+protobuf_out := $(LOCAL_LIB)/proto/proto/msg.pb.cc
+protobuf: $(protobuf_out)
 
 $(protobuf_out): $(NODE_DIR)/proto/msg.proto
 	@mkdir -p $(LOCAL_LIB)/proto
@@ -320,7 +315,6 @@ install_libs := $(haskell_kompiled)                                        \
                 $(foundry_kompiled)                                        \
                 $(haskell_standalone_kompiled)                             \
                 $(patsubst %, include/kframework/lemmas/%, $(kevm_lemmas)) \
-                kore-json.py                                               \
                 release.md                                                 \
                 version
 
@@ -348,12 +342,12 @@ $(KEVM_LIB)/release.md: INSTALL.md
 
 build: $(patsubst %, $(KEVM_BIN)/%, $(install_bins)) $(patsubst %, $(KEVM_LIB)/%, $(install_libs))
 
-build-llvm:               $(KEVM_LIB)/$(llvm_kompiled)    $(KEVM_LIB)/kore-json.py
-build-haskell:            $(KEVM_LIB)/$(haskell_kompiled) $(KEVM_LIB)/kore-json.py
-build-haskell-standalone: $(KEVM_LIB)/$(haskell_standalone_kompiled) $(KEVM_LIB)/kore-json.py
+build-llvm:               $(KEVM_LIB)/$(llvm_kompiled)
+build-haskell:            $(KEVM_LIB)/$(haskell_kompiled)
+build-haskell-standalone: $(KEVM_LIB)/$(haskell_standalone_kompiled)
 build-node:               $(KEVM_LIB)/$(node_kompiled)
 build-kevm:               $(KEVM_BIN)/kevm $(KEVM_LIB)/version $(kevm_includes) $(plugin_includes)
-build-foundry:            $(KEVM_BIN)/kevm $(KEVM_LIB)/$(foundry_kompiled) $(KEVM_LIB)/kore-json.py
+build-foundry:            $(KEVM_BIN)/kevm $(KEVM_LIB)/$(foundry_kompiled)
 
 all_bin_sources := $(shell find $(KEVM_BIN) -type f | sed 's|^$(KEVM_BIN)/||')
 all_lib_sources := $(shell find $(KEVM_LIB) -type f                                            \
@@ -408,32 +402,13 @@ test: test-integration test-conformance test-prove test-interactive
 tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_MODE     = VMTESTS
 tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = DEFAULT
 
-tests/%.run: tests/%
-	$(KEVM) interpret $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND)                                  \
-	    --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID)                                      \
-	    > tests/$*.$(TEST_CONCRETE_BACKEND)-out                                                                        \
-	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
-	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
-
 tests/%.run-interactive: tests/%
-	$(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND)                                        \
+	$(POETRY_RUN) $(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND)                          \
 	    --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID)                                      \
 	    > tests/$*.$(TEST_CONCRETE_BACKEND)-out                                                                        \
 	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
 	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 
-tests/%.run-expected: tests/% tests/%.expected
-	$(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND)    \
-	    --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID)  \
-	    > tests/$*.$(TEST_CONCRETE_BACKEND)-out                                    \
-	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/$*.expected
-	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
-
-tests/interactive/%.json.gst-to-kore.check: tests/ethereum-tests/GeneralStateTests/VMTests/%.json $(KEVM_BIN)/kevm
-	$(KEVM) kast $< $(KEVM_OPTS) $(KAST_OPTS) > tests/interactive/$*.gst-to-kore.out
-	$(CHECK) tests/interactive/$*.gst-to-kore.out tests/interactive/$*.gst-to-kore.expected
-	$(KEEP_OUTPUTS) || rm -rf tests/interactive/$*.gst-to-kore.out
-
 # solc-to-k
 # ---------
 
@@ -443,7 +418,7 @@ PYTEST_ARGS     :=
 test-foundry-prove: poetry build-kevm build-foundry
 	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_foundry_prove.py -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
 
-tests/specs/examples/%-bin-runtime.k: KEVM_OPTS += --pyk --verbose
+tests/specs/examples/%-bin-runtime.k: KEVM_OPTS += --verbose
 tests/specs/examples/%-bin-runtime.k: KEVM := $(POETRY_RUN) kevm
 
 tests/specs/examples/erc20-spec/haskell/timestamp: tests/specs/examples/erc20-bin-runtime.k
@@ -475,11 +450,6 @@ tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_F
 	    --syntax-module $(KPROVE_MODULE)                                                                        \
 	    $(KOMPILE_OPTS)
 
-tests/%.search: tests/%
-	$(KEVM) search $< "<statusCode> EVMC_INVALID_INSTRUCTION </statusCode>" $(KEVM_OPTS) $(KSEARCH_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) > $@-out
-	$(CHECK) $@-out $@-expected
-	$(KEEP_OUTPUTS) || rm -rf $@-out
-
 # Smoke Tests
 
 smoke_tests_run = tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json      \
@@ -514,9 +484,6 @@ test-prove: tests/specs/opcodes/evm-optimizations-spec.md poetry build-kevm buil
 
 test-prove-smoke: $(prove_smoke_tests:=.prove)
 
-test-klab-prove: KPROVE_OPTS += --debugger
-test-klab-prove: $(smoke_tests_prove:=.prove)
-
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
 tests/specs/opcodes/evm-optimizations-spec.md: include/kframework/optimizations.md
 	cat $< | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
@@ -528,26 +495,19 @@ test-integration: poetry build-kevm build-haskell build-llvm
 
 # Interactive Tests
 
-test-interactive: test-interactive-run test-interactive-prove test-interactive-search test-interactive-help
+test-interactive: test-interactive-run
 
 test-interactive-run: $(smoke_tests_run:=.run-interactive)
-test-interactive-prove: $(smoke_tests_prove:=.prove)
 
-search_tests:=$(wildcard tests/interactive/search/*.evm)
-test-interactive-search: $(search_tests:=.search)
-
-test-interactive-help:
-	$(KEVM) help
+node_tests:=$(wildcard tests/vm/*.bin)
+test-node: $(node_tests:=.run-node)
 
 proto_tester := $(LOCAL_BIN)/proto_tester
 proto-tester: $(proto_tester)
 $(proto_tester): tests/vm/proto_tester.cpp
 	@mkdir -p $(LOCAL_BIN)
 	$(CXX) -I $(LOCAL_LIB)/proto $(protobuf_out) $< -o $@ -lprotobuf -lpthread
 
-node_tests:=$(wildcard tests/vm/*.bin)
-test-node: $(node_tests:=.run-node)
-
 tests/vm/%.run-node: tests/vm/%.expected $(KEVM_BIN)/kevm-vm $(proto_tester)
 	bash -c " \
 	  kevm-vm 8888 127.0.0.1 & \

diff --git a/README.md b/README.md
@@ -262,7 +262,7 @@ make build-llvm KEVM_OPTS=--enable-llvm-debug
 To debug a conformance test, add the `--debugger` flag to the command:
 
 ```sh
-kevm interpret tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger
+kevm run tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger
 ```
 
 ### Keeping in mind while developing

diff --git a/VERIFICATION.md b/VERIFICATION.md
@@ -18,7 +18,7 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile sum-to-n-spec.k --pyk --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile sum-to-n-spec.k --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
 ```
 
 In this example, the arguments used are:
@@ -49,7 +49,7 @@ In this example, we rely on a helper module, `ERC20-VERIFICATION`, which must be
 The module is generated using the following `solc-to-k` command.
 
 ```sh
-kevm solc-to-k ERC20.sol ERC20 --pyk --main-module ERC20-VERIFICATION > erc20-bin-runtime.k
+kevm solc-to-k ERC20.sol ERC20 --main-module ERC20-VERIFICATION > erc20-bin-runtime.k
 ```
 
 - `solc-to-k` will parse a Solidity contract and generate a helper K module.
@@ -61,13 +61,13 @@ These rules are then used in the claims. As an example, the `#binRuntime(ERC20)`
 Following this, we can compile the Markdown file with:
 
 ```sh
-kevm kompile erc20-spec.md --pyk --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+kevm kompile erc20-spec.md --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
 ```
 
 Next, run the prover with:
 
 ```sh
-kevm prove erc20-spec.md --backend haskell  --definition erc20-spec/haskell --pyk --claim ERC20-SPEC.decimals
+kevm prove erc20-spec.md --backend haskell  --definition erc20-spec/haskell --claim ERC20-SPEC.decimals
 ```
 
 Here, `--claim` tells the prover to run only the `decimals` spec from the `ERC20-SPEC` module.
@@ -89,10 +89,10 @@ kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k --definition tests/s
 
 In addition to this, you can use `kevm show-kcfg ...` or `kevm view-kcfg ...` to get a visualization.
 
-`kevm view-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ...` command takes the same basic arguments as `kevm prove --pyk ...` does, including:
+`kevm view-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ...` command takes the same basic arguments as `kevm prove ...` does, including:
   - `spec_file` is the file to look in for specifications. This file is read like with `kevm prove —pyk …`; the `KProve.get_claims` invokes the frontend.
-  - `--save_directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --pyk --save-directory save_directory ...`
-  - `--claim claim_label` option is added, but unlike the `kevm prove --pyk ...`, you can only repeat it once. This option lets you select an individual claim out of the `spec_file`; if not supplied, it’s assumed that only one spec is present.
+  - `--save_directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --save-directory save_directory ...`
+  - `--claim claim_label` option is added, but unlike the `kevm prove ...`, you can only repeat it once. This option lets you select an individual claim out of the `spec_file`; if not supplied, it’s assumed that only one spec is present.
   - `--spec-module spec_module` is also an inherited option.
 
 The interactive KCFG (`view-kcfg`) puts your terminal in *application mode*. To select text in this mode, hold the modifier key provided by your terminal emulator (typically SHIFT or OPTION) while clicking and dragging. Refer to the [Textualize documentation](https://github.com/Textualize/textual/blob/main/FAQ.md#how-can-i-select-and-copy-text-in-a-textual-app) for more information.
@@ -101,8 +101,8 @@ A running example:
 
 ```sh
 mkdir kcfgs
-kevm kompile --pyk --backend haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
-kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --pyk --verbose --save-directory kcfgs
+kevm kompile --backend haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
 kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
 ```