Skip to content

Commit

Permalink
Switch --directory => --definition flag (#1241)
Browse files Browse the repository at this point in the history 
* Makefile, kevm, package/test-package: switch flag --directory => --definition

* Makefile: remove *-kompiled directories

* Makefile, cmake, kevm, kevm_pyk, optimizer: advoid using *-kompiled directories

* kevm: correct arguments

* Makefile, kevm, kevm_pyk/: adjustments

* .gitignore: ignore new kompiled dirs

* kevm: correct gen-spec
  • Loading branch information
@ehildenb
ehildenb committed May 5, 2022
1 parent 5496c29 commit cc1f577
Show file tree
Hide file tree
Showing 8 changed files with 78 additions and 77 deletions.
2 changes: 2 additions & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@
/tests/gen-spec/*.out
/tests/gen-spec/*.sol
/tests/specs/**/*-bin-runtime.k
/tests/specs/**/haskell
/tests/specs/**/java
/tests/specs/opcodes/evm-optimizations-spec.md
/tests/specs/**/*.prove.out
/tests/specs/**/*.sol.json
Expand Down
97 changes: 48 additions & 49 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ haskell_main_module := EDSL
haskell_syntax_module := $(haskell_main_module)
haskell_main_file := edsl.md
haskell_main_filename := $(basename $(notdir $(haskell_main_file)))
haskell_kompiled_dir := $(haskell_dir)/$(haskell_main_filename)-kompiled
haskell_kompiled_dir := $(haskell_dir)
haskell_kompiled := $(haskell_kompiled_dir)/definition.kore

ifeq ($(UNAME_S),Darwin)
Expand All @@ -240,7 +240,7 @@ llvm_main_module := ETHEREUM-SIMULATION
llvm_syntax_module := $(llvm_main_module)
llvm_main_file := driver.md
llvm_main_filename := $(basename $(notdir $(llvm_main_file)))
llvm_kompiled := $(llvm_dir)/$(llvm_main_filename)-kompiled/interpreter
llvm_kompiled := $(llvm_dir)/interpreter

ifeq ($(UNAME_S),Darwin)
$(KEVM_LIB)/$(llvm_kompiled): $(libcryptopp_out)
Expand All @@ -260,10 +260,9 @@ node_main_module := EVM-NODE
node_syntax_module := $(node_main_module)
node_main_file := evm-node.md
node_main_filename := $(basename $(notdir $(node_main_file)))
node_kore := $(node_dir)/$(node_main_filename)-kompiled/definition.kore
node_kore := $(node_dir)/definition.kore
node_kompiled := $(node_dir)/build/kevm-vm
export node_dir
export node_main_filename

$(KEVM_LIB)/$(node_kore): $(kevm_includes) $(plugin_includes) $(plugin_c_includes) $(libff_out) $(KEVM_BIN)/kevm
$(KOMPILE) --backend node \
Expand Down Expand Up @@ -435,36 +434,36 @@ tests/%.prove-legacy: tests/%
kevm-pyk-venv:
$(MAKE) -C ./kevm_pyk venv-prod

tests/specs/examples/erc20-spec/haskell/erc20-spec-kompiled/timestamp: tests/specs/examples/erc20-bin-runtime.k
tests/specs/examples/erc20-spec/haskell/timestamp: tests/specs/examples/erc20-bin-runtime.k
tests/specs/examples/erc20-bin-runtime.k: tests/specs/examples/ERC20.sol $(KEVM_LIB)/$(haskell_kompiled) kevm-pyk-venv
. ./kevm_pyk/venv-prod/bin/activate && $(KEVM) solc-to-k $< ERC20 > $@

tests/specs/examples/erc721-spec/haskell/erc721-spec-kompiled/timestamp: tests/specs/examples/erc721-bin-runtime.k
tests/specs/examples/erc721-spec/haskell/timestamp: tests/specs/examples/erc721-bin-runtime.k
tests/specs/examples/erc721-bin-runtime.k: tests/specs/examples/ERC721.sol $(KEVM_LIB)/$(haskell_kompiled) kevm-pyk-venv
. ./kevm_pyk/venv-prod/bin/activate && $(KEVM) solc-to-k $< ERC721 > $@

tests/specs/examples/empty-bin-runtime.k: tests/specs/examples/Empty.sol $(KEVM_LIB)/$(haskell_kompiled) kevm-pyk-venv
. ./kevm_pyk/venv-prod/bin/activate && $(KEVM) solc-to-k $< Empty > $@

tests/gen-spec/mcd-spec.k.check: tests/gen-spec/verification-kompiled/timestamp kevm-pyk-venv
. ./kevm_pyk/venv-prod/bin/activate && $(KEVM) gen-spec tests/gen-spec/verification-kompiled MCD-SPEC > $@.out
tests/gen-spec/mcd-spec.k.check: tests/gen-spec/kompiled/timestamp kevm-pyk-venv
. ./kevm_pyk/venv-prod/bin/activate && $(KEVM) gen-spec MCD-SPEC --definition tests/gen-spec/kompiled > $@.out
$(CHECK) $@.out $@.expected

tests/gen-spec/verification-kompiled/timestamp: tests/gen-spec/verification.k
$(KOMPILE) --backend haskell --directory tests/gen-spec $< --main-module MCD-VERIFICATION
tests/gen-spec/kompiled/timestamp: tests/gen-spec/verification.k
$(KOMPILE) --backend haskell --definition tests/gen-spec/kompiled $< --main-module MCD-VERIFICATION


.SECONDEXPANSION:
tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)/$$(KPROVE_FILE)-kompiled/timestamp
tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)/timestamp
$(KEVM) prove $< $(TEST_OPTIONS) --backend $(TEST_SYMBOLIC_BACKEND) --format-failures $(KPROVE_OPTS) \
--directory tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)

tests/specs/%-kompiled/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT) tests/specs/$$(firstword $$(subst /, ,$$*))/concrete-rules.txt $(kevm_includes) $(lemma_includes) $(plugin_includes) $(KEVM_BIN)/kevm
$(KOMPILE) --backend $(word 3, $(subst /, , $*)) $< \
--directory tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \
--main-module $(KPROVE_MODULE) \
--syntax-module $(KPROVE_MODULE) \
--concrete-rules-file tests/specs/$(firstword $(subst /, ,$*))/concrete-rules.txt \
--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)

tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT) tests/specs/$$(firstword $$(subst /, ,$$*))/concrete-rules.txt $(kevm_includes) $(lemma_includes) $(plugin_includes) $(KEVM_BIN)/kevm
$(KOMPILE) --backend $(word 3, $(subst /, , $*)) $< \
--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \
--main-module $(KPROVE_MODULE) \
--syntax-module $(KPROVE_MODULE) \
--concrete-rules-file tests/specs/$(firstword $(subst /, ,$*))/concrete-rules.txt \
$(KOMPILE_OPTS)

tests/%.search: tests/%
Expand Down Expand Up @@ -528,36 +527,36 @@ prove_mcd_tests := $(filter-out $(prove_skip_tests), $(wildcard $(prove
prove_optimization_tests := $(filter-out $(prove_skip_tests), tests/specs/opcodes/evm-optimizations-spec.md)

## best-effort list of provex kompiled definitions to produce ahead of time
provex_definitions := \
tests/specs/benchmarks/functional-spec/haskell/functional-spec-kompiled/timestamp \
tests/specs/benchmarks/functional-spec/java/functional-spec-kompiled/timestamp \
tests/specs/benchmarks/verification/haskell/verification-kompiled/timestamp \
tests/specs/benchmarks/verification/java/verification-kompiled/timestamp \
tests/specs/bihu/functional-spec/haskell/functional-spec-kompiled/timestamp \
tests/specs/bihu/functional-spec/java/functional-spec-kompiled/timestamp \
tests/specs/bihu/verification/haskell/verification-kompiled/timestamp \
tests/specs/bihu/verification/java/verification-kompiled/timestamp \
tests/specs/erc20/verification/haskell/verification-kompiled/timestamp \
tests/specs/erc20/verification/java/verification-kompiled/timestamp \
tests/specs/examples/erc20-spec/haskell/erc20-spec-kompiled/timestamp \
tests/specs/examples/erc721-spec/haskell/erc721-spec-kompiled/timestamp \
tests/specs/examples/solidity-code-spec/haskell/solidity-code-spec-kompiled/timestamp \
tests/specs/examples/solidity-code-spec/java/solidity-code-spec-kompiled/timestamp \
tests/specs/examples/sum-to-n-spec/haskell/sum-to-n-spec-kompiled/timestamp \
tests/specs/examples/sum-to-n-spec/java/sum-to-n-spec-kompiled/timestamp \
tests/specs/functional/infinite-gas-spec/haskell/infinite-gas-spec-kompiled/timestamp \
tests/specs/functional/lemmas-no-smt-spec/haskell/lemmas-no-smt-spec-kompiled/timestamp \
tests/specs/functional/lemmas-no-smt-spec/java/lemmas-no-smt-spec-kompiled/timestamp \
tests/specs/functional/lemmas-spec/haskell/lemmas-spec-kompiled/timestamp \
tests/specs/functional/lemmas-spec/java/lemmas-spec-kompiled/timestamp \
tests/specs/functional/merkle-spec/haskell/merkle-spec-kompiled/timestamp \
tests/specs/functional/storageRoot-spec/haskell/storageRoot-spec-kompiled/timestamp \
tests/specs/mcd/functional-spec/haskell/functional-spec-kompiled/timestamp \
tests/specs/mcd/functional-spec/java/functional-spec-kompiled/timestamp \
tests/specs/mcd/verification/haskell/verification-kompiled/timestamp \
tests/specs/mcd/verification/java/verification-kompiled/timestamp \
tests/specs/opcodes/evm-optimizations-spec/haskell/evm-optimizations-spec-kompiled/timestamp \
tests/specs/opcodes/verification/java/verification-kompiled/timestamp
provex_definitions := \
tests/specs/benchmarks/functional-spec/haskell/timestamp \
tests/specs/benchmarks/functional-spec/java/timestamp \
tests/specs/benchmarks/verification/haskell/timestamp \
tests/specs/benchmarks/verification/java/timestamp \
tests/specs/bihu/functional-spec/haskell/timestamp \
tests/specs/bihu/functional-spec/java/timestamp \
tests/specs/bihu/verification/haskell/timestamp \
tests/specs/bihu/verification/java/timestamp \
tests/specs/erc20/verification/haskell/timestamp \
tests/specs/erc20/verification/java/timestamp \
tests/specs/examples/erc20-spec/haskell/timestamp \
tests/specs/examples/erc721-spec/haskell/timestamp \
tests/specs/examples/solidity-code-spec/haskell/timestamp \
tests/specs/examples/solidity-code-spec/java/timestamp \
tests/specs/examples/sum-to-n-spec/haskell/timestamp \
tests/specs/examples/sum-to-n-spec/java/timestamp \
tests/specs/functional/infinite-gas-spec/haskell/timestamp \
tests/specs/functional/lemmas-no-smt-spec/haskell/timestamp \
tests/specs/functional/lemmas-no-smt-spec/java/timestamp \
tests/specs/functional/lemmas-spec/haskell/timestamp \
tests/specs/functional/lemmas-spec/java/timestamp \
tests/specs/functional/merkle-spec/haskell/timestamp \
tests/specs/functional/storageRoot-spec/haskell/timestamp \
tests/specs/mcd/functional-spec/haskell/timestamp \
tests/specs/mcd/functional-spec/java/timestamp \
tests/specs/mcd/verification/haskell/timestamp \
tests/specs/mcd/verification/java/timestamp \
tests/specs/opcodes/evm-optimizations-spec/haskell/timestamp \
tests/specs/opcodes/verification/java/timestamp
build-provex: $(provex_definitions)

test-prove: test-prove-benchmarks test-prove-functional test-prove-opcodes test-prove-erc20 test-prove-bihu test-prove-examples test-prove-mcd test-prove-optimizations
Expand Down
2 changes: 1 addition & 1 deletion cmake/node/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ list(APPEND CMAKE_MODULE_PATH "${K_LIB}/cmake/kframework")
include(LLVMKompilePrelude)
project (KevmVm CXX)

set(KOMPILED_DIR $ENV{KEVM_LIB_ABS}/$ENV{node_dir}/$ENV{node_main_filename}-kompiled)
set(KOMPILED_DIR $ENV{KEVM_LIB_ABS}/$ENV{node_dir})
set(KOMPILE_USE_MAIN "library")
set(TARGET_NAME "kevm-vm")

Expand Down
28 changes: 14 additions & 14 deletions kevm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ export KLAB_OUT="${KLAB_OUT:-~/.klab}"
run_kompile() {
local kompile_opts openssl_root

kompile_opts=( "${run_file}" --directory "${backend_dir}" )
kompile_opts=( "${run_file}" --output-definition "${backend_dir}" )
kompile_opts+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )
kompile_opts+=( --hook-namespaces "JSON KRYPTO BLOCKCHAIN" )
kompile_opts+=( --emit-json )
Expand Down Expand Up @@ -111,7 +111,7 @@ run_krun() {
parser='cat'
;;
esac
execute krun --directory "$backend_dir" \
execute krun --definition "$backend_dir" \
-cSCHEDULE="$cschedule" -pSCHEDULE="$parser" \
-cMODE="$cmode" -pMODE="$parser" \
-cCHAINID="$cchainid" -pCHAINID="$parser" \
Expand All @@ -124,9 +124,9 @@ run_kast() {
output_mode="${1:-kore}" ; shift

case "$run_file-$output_mode" in
*.json-kast) execute kast-json.py "$run_file" "$cSCHEDULE_kast" "$cMODE_kast" "$cCHAINID_kast" ;;
*.json-kore) execute kore-json.py "$run_file" "$cSCHEDULE_kore" "$cMODE_kore" "$cCHAINID_kore" ;;
*) check_k_install ; kast --directory "$backend_dir" "$run_file" --output "$output_mode" "$@" ;;
*.json-kast) execute kast-json.py "$run_file" "$cSCHEDULE_kast" "$cMODE_kast" "$cCHAINID_kast" ;;
*.json-kore) execute kore-json.py "$run_file" "$cSCHEDULE_kore" "$cMODE_kore" "$cCHAINID_kore" ;;
*) check_k_install ; kast --definition "$backend_dir" "$run_file" --output "$output_mode" "$@" ;;
esac
}

Expand All @@ -140,7 +140,7 @@ run_prove() {
eventlog_name="${run_file}.eventlog"

kprove=kprove
proof_args=(--directory "${backend_dir}" "${run_file}")
proof_args=(--definition "${backend_dir}" "${run_file}")
proof_args+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )

! ${provex} || kprove=kprovex
Expand Down Expand Up @@ -181,7 +181,7 @@ run_prove() {
execute kore-prof "${eventlog_name}" ${kore_prof_args} > "${eventlog_name}.json"
else
if ${pyk_minimize}; then
pyk_args=(${backend_dir}/*-kompiled print /dev/stdin --minimize)
pyk_args=(${backend_dir} print /dev/stdin --minimize)
[[ -z "${pyk_omit_labels}" ]] || pyk_args+=(--omit-labels "${pyk_omit_labels}")
execute ${kprove} "${proof_args[@]}" "$@" --output json | kpyk "${pyk_args[@]}"
else
Expand Down Expand Up @@ -210,7 +210,7 @@ view_klab() {
run_interpret() {
local interpreter kast output output_text output_format exit_status cmdprefix

interpreter="$backend_dir/driver-kompiled/interpreter"
interpreter="$backend_dir/interpreter"
kast="$(mktemp)"
output="$(mktemp)"
output_text="$(mktemp)"
Expand Down Expand Up @@ -239,7 +239,7 @@ run_interpret() {
;;

haskell) run_kast kore > "$kast"
execute kore-exec "$backend_dir/driver-kompiled/definition.kore" --pattern "$kast" --module ETHEREUM-SIMULATION --smt none --output "$output" || exit_status="$?"
execute kore-exec "$backend_dir/definition.kore" --pattern "$kast" --module ETHEREUM-SIMULATION --smt none --output "$output" || exit_status="$?"
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
cat "$output" | "${KEVM}" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
fi
Expand All @@ -257,11 +257,11 @@ run_solc() {
contract_name="$1" ; shift
json_run_file="${run_file}.json"

execute python3 -m kevm_pyk solc-to-k "$@" ${backend_dir}/*-kompiled "${run_file}" "${contract_name}"
execute python3 -m kevm_pyk solc-to-k "${backend_dir}" "${run_file}" "${contract_name}" "$@"
}

run_gen_spec() {
execute python3 -m kevm_pyk gen-spec-modules "$@"
execute python3 -m kevm_pyk gen-spec-modules "${backend_dir}" "$@"
}

# Main
Expand All @@ -279,8 +279,8 @@ if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
${KEVM} search [--backend (java|haskell)] [--profile|--debug] <pgm> <pattern> <K arg>*
${KEVM} kompile [--backend (java|llvm|haskell)] [--profile|--debug] <main> <K arg>*
${KEVM} klab-view [--profile|--debug] <spec>
${KEVM} solc-to-k [--profile|--debug] <sol> <sol contract> <solc arg>*
${KEVM} gen-spec [--profile|--debug] <kompiled-dir>
${KEVM} solc-to-k [--profile|--debug] <sol-file> <contract-name> <solc-arg>*
${KEVM} gen-spec [--profile|--debug] <module-name>
${KEVM} [help|--help|version|--version]
Expand Down Expand Up @@ -373,7 +373,7 @@ while [[ $# -gt 0 ]]; do
--kore-prof-args) kore_prof_args="$2" ; shift 2 ;;
--bug-report) bug_report=true ; shift ;;
--backend) backend="$2" ; shift 2 ;;
--directory) backend_dir="$2" ; shift 2 ;;
--definition) backend_dir="$2" ; shift 2 ;;
--concrete-rules-file) concrete_rules_file="$2" ; shift 2 ;;
--no-provex) provex=false ; shift ;;
--verif-module) verif_module="$2" ; shift 2 ;;
Expand Down
Loading

0 comments on commit cc1f577

Please sign in to comment.