diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..662c1e1 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "deps/ulm"] + path = deps/ulm + url = git@github.com:Pi-Squared-Inc/ulm diff --git a/Makefile b/Makefile index 26e8e57..bf5269a 100644 --- a/Makefile +++ b/Makefile @@ -87,6 +87,23 @@ UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-with-contract/output UKM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run) UKM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_WITH_CONTRACT_TESTING_INPUTS)) +UKM_FLAGS ::= -I deps/ulm/kllvm \ + -ccopt -Ldeps/ulm/kllvm \ + -ccopt -lulmkllvm + +# TODO: Use a plugin directory that is accessible from the current project +CRYPTO_FLAGS ::= -I ../evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin \ + -ccopt -lssl \ + -ccopt -lcrypto \ + -ccopt -lsecp256k1 \ + -ccopt $KRYPTO_DIR/evm-semantics/plugin/krypto.a \ + +# PLUGIN_FLAGS ::= --hook-namespaces 'ULM KRYPTO' +PLUGIN_FLAGS ::= --hook-namespaces 'ULM' \ + -ccopt -std=c++17 \ + ${UKM_FLAGS} \ + # ${CRYPTO_FLAGS} + .PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test ukm-no-contracts-test all: build test @@ -134,6 +151,10 @@ ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS) ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS) +ulm-plugin: + make -C deps/ulm/kllvm/ libulmkllvm.so +.PHONY: ulm-plugin + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -181,11 +202,12 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI -I . \ --debug -$(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) ulm-plugin # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(UKM_EXECUTION_KOMPILED) $$(which kompile) ukm-semantics/targets/execution/ukm-target.md \ --emit-json -o $(UKM_EXECUTION_KOMPILED) \ + ${PLUGIN_FLAGS} \ -I . \ --debug @@ -197,10 +219,11 @@ $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) -I . \ --debug -$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) ulm-plugin # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(UKM_TESTING_KOMPILED) $$(which kompile) ukm-semantics/targets/testing/ukm-target.md \ + ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ --debug diff --git a/deps/ulm b/deps/ulm new file mode 160000 index 0000000..f562a89 --- /dev/null +++ b/deps/ulm @@ -0,0 +1 @@ +Subproject commit f562a89482fdd060b23d57babbf0786ad3bca2dd diff --git a/ukm-semantics/main/hooks.md b/ukm-semantics/main/hooks.md index 934e5c0..1e930b3 100644 --- a/ukm-semantics/main/hooks.md +++ b/ukm-semantics/main/hooks.md @@ -4,6 +4,7 @@ requires "hooks/bytes.md" requires "hooks/helpers.md" requires "hooks/state.md" requires "hooks/ukm.md" +requires "ulm.k" module UKM-HOOKS imports private UKM-HOOKS-BYTES diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md index 94f5151..d239744 100644 --- a/ukm-semantics/main/hooks/ukm.md +++ b/ukm-semantics/main/hooks/ukm.md @@ -8,15 +8,19 @@ module UKM-HOOKS-UKM-SYNTAX | SetAccountStorageHook(Int, Int) | GetAccountStorageHook(Int) - syntax UkmHookResult ::= ukmNoResult() - | ukmInt64Result(Int) + syntax K + syntax Type + syntax UkmHookResult ::= ukmNoResult(K) + | ukmIntResult(Int, Type) endmodule module UKM-HOOKS-UKM imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX + imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-UKM-SYNTAX + imports private ULM-HOOKS syntax Identifier ::= "ukm" [token] | "CallData" [token] @@ -51,10 +55,18 @@ module UKM-HOOKS-UKM rule #GetAccountStorageHook(ptrValue(_, u64(Key))) => GetAccountStorageHook(MInt2Unsigned(Key)) - rule ukmNoResult() => ptrValue(null, tuple(.ValueList)) - syntax UkmHook ::= #ukmInt64Result(ValueOrError) - rule ukmInt64Result(Value:Int) => #ukmInt64Result(integerToValue(Value, u64)) - rule #ukmInt64Result(V:Value) => ptrValue(null, V) + rule ukmNoResult(.K) => ptrValue(null, tuple(.ValueList)) + rule ukmIntResult(Value:Int, T:Type) => ukmValueResult(integerToValue(Value, T)) + + syntax UkmHook ::= ukmValueResult(ValueOrError) + rule ukmValueResult(V:Value) => ptrValue(null, V) + + // Hook implementations + + rule CallDataHook() => ukmBytesNew(CallData()) + rule CallerHook() => ukmIntResult(Caller(), u160) + rule SetAccountStorageHook(Key:Int, Value:Int) => ukmNoResult(SetAccountStorage(Key, Value)) + rule GetAccountStorageHook(Key:Int) => ukmIntResult(Caller(), u256) endmodule