kevm: add search command (#412)

* kevm: add search command * Jenkinsfile, Makefile, tests/interactive: add example search commands * Makefile, tests/interactive/search: more tests, simpler interface * kevm: correct documentation
runtimeverification · Jul 26, 2019 · ffd9552 · ffd9552
1 parent 160f2f8
commit ffd9552
Show file tree

Hide file tree

Showing 11 changed files with 702 additions and 2 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -130,6 +130,13 @@ pipeline {
                 '''
               }
             }
+            stage('Haskell Search') {
+              steps {
+                sh '''
+                  make test-interactive-search TEST_SYMBOLIC_BACKEND=haskell -j4
+                '''
+              }
+            }
             stage('KEVM help') {
               steps {
                 sh '''

diff --git a/Makefile b/Makefile
@@ -41,7 +41,7 @@ export LUA_PATH
         test test-all test-conformance test-slow-conformance test-all-conformance \
         test-vm test-slow-vm test-all-vm test-bchain test-slow-bchain test-all-bchain \
         test-proof test-klab-prove test-parse test-failure \
-        test-interactive test-interactive-help test-interactive-run test-interactive-prove \
+        test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search \
         media media-pdf sphinx metropolis-theme
 .SECONDARY:
 
@@ -383,6 +383,11 @@ tests/%.parse: tests/%
 tests/%.prove: tests/%
 	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
 
+tests/%.search: tests/%
+	$(TEST) search --backend $(TEST_SYMBOLIC_BACKEND) $< "<statusCode> EVMC_INVALID_INSTRUCTION </statusCode>" > $@-out
+	$(CHECK) $@-expected $@-out
+	rm -rf $@-out
+
 tests/%.klab-prove: tests/%
 	$(TEST) klab-prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
 
@@ -451,11 +456,14 @@ test-failure: $(failure_tests:=.run-expected)
 
 # Interactive Tests
 
-test-interactive: test-interactive-run test-interactive-prove test-interactive-help
+test-interactive: test-interactive-run test-interactive-prove test-interactive-search test-interactive-help
 
 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:
 	$(TEST) help
 

diff --git a/kevm b/kevm
@@ -60,6 +60,13 @@ run_prove() {
     kprove --directory "$backend_dir" "$run_file" "$@"
 }
 
+run_search() {
+    local search_pattern
+    search_pattern="$1" ; shift
+    export K_OPTS=-Xmx8G
+    run_krun --search --pattern "$search_pattern" "$@"
+}
+
 run_klab() {
     local run_mode klab_log
 
@@ -132,6 +139,7 @@ if [[ "$run_command" == 'help' ]]; then
                $0 interpret  [--backend (ocaml|llvm)]              <pgm>  <interpreter arg>*
                $0 kast       [--backend (ocaml|java)]              <pgm>  <output format> <K arg>*
                $0 prove      [--backend (java|haskell)]            <spec> <K arg>* -m <def_module>
+               $0 search     [--backend (java|haskell)]            <pgm>  <pattern> <K arg>*
                $0 klab-run                                         <pgm>  <K arg>*
                $0 klab-prove                                       <spec> <K arg>* -m <def_module>
                $0 klab-view                                        <spec>
@@ -140,6 +148,7 @@ if [[ "$run_command" == 'help' ]]; then
            $0 interpret : Run JSON EVM programs without K Frontend (external parser)
            $0 kast      : Parse an EVM program and output it in a supported format
            $0 prove     : Run an EVM K proof
+           $0 search    : Search for a K pattern in an EVM program execution
            $0 klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read
            $0 klab-view : View the statelog associated with a given program or spec
 
@@ -148,6 +157,7 @@ if [[ "$run_command" == 'help' ]]; then
                  <K arg> is an argument you want to pass to K.
                  <interpreter arg> is an argument you want to pass to the derived interpreter.
                  <output format> is the format for Kast to output the term in.
+                 <pattern> is the configuration pattern to search for.
                  <def_module> is the module to take as axioms when doing verification.
 
            klab-view: Make sure that the 'klab/bin' directory is on your PATH to use this option.
@@ -179,6 +189,7 @@ case "$run_command-$backend" in
     kast-@(ocaml|java|llvm|haskell) ) run_kast                        "$@" ;;
     interpret-@(ocaml|llvm)         ) run_interpret                   "$@" ;;
     prove-@(java|haskell)           ) run_prove                       "$@" ;;
+    search-@(java|haskell)          ) run_search                      "$@" ;;
     klab-@(run|prove)-java          ) run_klab "${run_command#klab-}" "$@" ;;
     klab-view-java                  ) view_klab                       "$@" ;;
     *) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;;

diff --git a/tests/interactive/search/branching-invalid.evm b/tests/interactive/search/branching-invalid.evm
@@ -0,0 +1,13 @@
+load "exec" : { "gas" : 10000
+              ,"code" : PUSH(1, 3) ; PUSH(1, 4) ; ADD
+                      ; PUSH(1, 8) ; EQ
+                      ; PUSH(1, 12) ; JUMPI     // jumpi("end")
+                      ; INVALID
+                      ; JUMPDEST                // jumpdest("end")
+                      ; STOP
+                      ; .OpCodes
+              }
+
+start
+
+.EthereumSimulation