From ffd9552f3703c0a60b6b3e2262b9430e2764e2f8 Mon Sep 17 00:00:00 2001 From: ehildenb Date: Fri, 26 Jul 2019 12:07:58 -0500 Subject: [PATCH] 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 --- Jenkinsfile | 7 + Makefile | 12 +- kevm | 11 + .../interactive/search/branching-invalid.evm | 13 + .../branching-invalid.evm.search-expected | 319 ++++++++++++++++++ .../search/branching-no-invalid.evm | 13 + .../branching-no-invalid.evm.search-expected | 1 + .../search/straight-line-no-invalid.evm | 7 + ...raight-line-no-invalid.evm.search-expected | 1 + tests/interactive/search/straight-line.evm | 7 + .../search/straight-line.evm.search-expected | 313 +++++++++++++++++ 11 files changed, 702 insertions(+), 2 deletions(-) create mode 100644 tests/interactive/search/branching-invalid.evm create mode 100644 tests/interactive/search/branching-invalid.evm.search-expected create mode 100644 tests/interactive/search/branching-no-invalid.evm create mode 100644 tests/interactive/search/branching-no-invalid.evm.search-expected create mode 100644 tests/interactive/search/straight-line-no-invalid.evm create mode 100644 tests/interactive/search/straight-line-no-invalid.evm.search-expected create mode 100644 tests/interactive/search/straight-line.evm create mode 100644 tests/interactive/search/straight-line.evm.search-expected diff --git a/Jenkinsfile b/Jenkinsfile index c5ca645892..764b7d7bc4 100644 --- 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 index 9d3fd6bb1a..d68a673bd9 100644 --- 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) $< " EVMC_INVALID_INSTRUCTION " > $@-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 index 80e807f01f..610153b04d 100755 --- 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)] * $0 kast [--backend (ocaml|java)] * $0 prove [--backend (java|haskell)] * -m + $0 search [--backend (java|haskell)] * $0 klab-run * $0 klab-prove * -m $0 klab-view @@ -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 is an argument you want to pass to K. is an argument you want to pass to the derived interpreter. is the format for Kast to output the term in. + is the configuration pattern to search for. 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 new file mode 100644 index 0000000000..0fb07f4af4 --- /dev/null +++ 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 diff --git a/tests/interactive/search/branching-invalid.evm.search-expected b/tests/interactive/search/branching-invalid.evm.search-expected new file mode 100644 index 0000000000..49cb885e8e --- /dev/null +++ b/tests/interactive/search/branching-invalid.evm.search-expected @@ -0,0 +1,319 @@ + { + DotVar0 + #Equals + + 0 + + } +#And + { + DotVar2 + #Equals + + + .Set + + + .AccountCellMap + + + .List + + + .List + + + .MessageCellMap + + + } +#And + { + _0 + #Equals + + .WordStack + + } +#And + { + _1 + #Equals + + .List + + } +#And + { + _2 + #Equals + + .List + + } +#And + { + _3 + #Equals + + .Set + + } +#And + { + _4 + #Equals + + + 0 |-> PUSH ( 1 , 3 ) + 2 |-> PUSH ( 1 , 4 ) + 4 |-> ADD + 5 |-> PUSH ( 1 , 8 ) + 7 |-> EQ + 8 |-> PUSH ( 1 , 12 ) + 10 |-> JUMPI + 11 |-> INVALID + 12 |-> JUMPDEST + 13 |-> STOP + + + .WordStack + + + 0 + + + 0 + + + .WordStack + + + 0 + + + .WordStack + + + .Map + + + 11 + + + 9972 + + + 0 + + + 0 + + + false + + + 0 + + + } +#And + { + _5 + #Equals + + + .Set + + + .List + + + 0 + + + } +#And + { + _6 + #Equals + + 0 + + } +#And + { + _7 + #Equals + + 0 + + } +#And + { + _8 + #Equals + + 0 + + } +#And + { + _9 + #Equals + + 0 + + } +#And + { + _10 + #Equals + + 0 + + } +#And + { + _11 + #Equals + + 0 + + } +#And + { + _12 + #Equals + + 0 + + } +#And + { + _13 + #Equals + + 0 + + } +#And + { + _14 + #Equals + + .WordStack + + } +#And + { + _15 + #Equals + + 0 + + } +#And + { + _16 + #Equals + + 0 + + } +#And + { + _17 + #Equals + + 0 + + } +#And + { + _18 + #Equals + + 0 + + } +#And + { + _19 + #Equals + + 0 + + } +#And + { + _20 + #Equals + + .WordStack + + } +#And + { + _21 + #Equals + + 0 + + } +#And + { + _22 + #Equals + + 0 + + } +#And + { + _23 + #Equals + + [ .JSONList ] + + } +#And + { + _24 + #Equals + + .List + + } +#And + { + _25 + #Equals + + #halt ~> .EthereumSimulation + + } +#And + { + _26 + #Equals + + 1 + + } +#And + { + _27 + #Equals + + NORMAL + + } +#And + { + _28 + #Equals + + BYZANTIUM + + } diff --git a/tests/interactive/search/branching-no-invalid.evm b/tests/interactive/search/branching-no-invalid.evm new file mode 100644 index 0000000000..933e777628 --- /dev/null +++ b/tests/interactive/search/branching-no-invalid.evm @@ -0,0 +1,13 @@ +load "exec" : { "gas" : 10000 + ,"code" : PUSH(1, 3) ; PUSH(1, 4) ; ADD + ; PUSH(1, 7) ; EQ + ; PUSH(1, 13) ; JUMPI // jumpi("end") + ; INVALID + ; JUMPDEST // jumpdest("end") + ; STOP + ; .OpCodes + } + +start + +.EthereumSimulation diff --git a/tests/interactive/search/branching-no-invalid.evm.search-expected b/tests/interactive/search/branching-no-invalid.evm.search-expected new file mode 100644 index 0000000000..5bca592b8b --- /dev/null +++ b/tests/interactive/search/branching-no-invalid.evm.search-expected @@ -0,0 +1 @@ +#False diff --git a/tests/interactive/search/straight-line-no-invalid.evm b/tests/interactive/search/straight-line-no-invalid.evm new file mode 100644 index 0000000000..aaacee0dd0 --- /dev/null +++ b/tests/interactive/search/straight-line-no-invalid.evm @@ -0,0 +1,7 @@ +load "exec" : { "gas" : 10000 + ,"code" : PUSH(32, 3) ; PUSH(32, 4) ; ADD ; .OpCodes + } + +start + +.EthereumSimulation diff --git a/tests/interactive/search/straight-line-no-invalid.evm.search-expected b/tests/interactive/search/straight-line-no-invalid.evm.search-expected new file mode 100644 index 0000000000..5bca592b8b --- /dev/null +++ b/tests/interactive/search/straight-line-no-invalid.evm.search-expected @@ -0,0 +1 @@ +#False diff --git a/tests/interactive/search/straight-line.evm b/tests/interactive/search/straight-line.evm new file mode 100644 index 0000000000..cf54bba2f3 --- /dev/null +++ b/tests/interactive/search/straight-line.evm @@ -0,0 +1,7 @@ +load "exec" : { "gas" : 10000 + ,"code" : PUSH(32, 3) ; PUSH(32, 4) ; ADD ; INVALID ; .OpCodes + } + +start + +.EthereumSimulation diff --git a/tests/interactive/search/straight-line.evm.search-expected b/tests/interactive/search/straight-line.evm.search-expected new file mode 100644 index 0000000000..6223ad8047 --- /dev/null +++ b/tests/interactive/search/straight-line.evm.search-expected @@ -0,0 +1,313 @@ + { + DotVar0 + #Equals + + 0 + + } +#And + { + DotVar2 + #Equals + + + .Set + + + .AccountCellMap + + + .List + + + .List + + + .MessageCellMap + + + } +#And + { + _0 + #Equals + + .WordStack + + } +#And + { + _1 + #Equals + + .List + + } +#And + { + _2 + #Equals + + .List + + } +#And + { + _3 + #Equals + + .Set + + } +#And + { + _4 + #Equals + + + 0 |-> PUSH ( 32 , 3 ) + 33 |-> PUSH ( 32 , 4 ) + 66 |-> ADD + 67 |-> INVALID + + + .WordStack + + + 0 + + + 0 + + + .WordStack + + + 0 + + + 7 : .WordStack + + + .Map + + + 67 + + + 9991 + + + 0 + + + 0 + + + false + + + 0 + + + } +#And + { + _5 + #Equals + + + .Set + + + .List + + + 0 + + + } +#And + { + _6 + #Equals + + 0 + + } +#And + { + _7 + #Equals + + 0 + + } +#And + { + _8 + #Equals + + 0 + + } +#And + { + _9 + #Equals + + 0 + + } +#And + { + _10 + #Equals + + 0 + + } +#And + { + _11 + #Equals + + 0 + + } +#And + { + _12 + #Equals + + 0 + + } +#And + { + _13 + #Equals + + 0 + + } +#And + { + _14 + #Equals + + .WordStack + + } +#And + { + _15 + #Equals + + 0 + + } +#And + { + _16 + #Equals + + 0 + + } +#And + { + _17 + #Equals + + 0 + + } +#And + { + _18 + #Equals + + 0 + + } +#And + { + _19 + #Equals + + 0 + + } +#And + { + _20 + #Equals + + .WordStack + + } +#And + { + _21 + #Equals + + 0 + + } +#And + { + _22 + #Equals + + 0 + + } +#And + { + _23 + #Equals + + [ .JSONList ] + + } +#And + { + _24 + #Equals + + .List + + } +#And + { + _25 + #Equals + + #halt ~> .EthereumSimulation + + } +#And + { + _26 + #Equals + + 1 + + } +#And + { + _27 + #Equals + + NORMAL + + } +#And + { + _28 + #Equals + + BYZANTIUM + + }