Implement ULM hooks

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "deps/ulm"]
+	path = deps/ulm
+	url = [email protected]:Pi-Squared-Inc/ulm

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

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

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