diff --git a/compilation/prepare-rust-bundle.sh b/compilation/prepare-rust-bundle.sh
index 3e696ec2..fb4dcc39 100755
--- a/compilation/prepare-rust-bundle.sh
+++ b/compilation/prepare-rust-bundle.sh
@@ -25,9 +25,9 @@ cat $ULM_CONTRACTS_TESTING_INPUT_DIR/bytes_hooks.rs >> $output_file
echo ">)>" >> $output_file
echo "<(<" >> $output_file
-echo "::test_helpers" >> $output_file
+echo "::debug" >> $output_file
echo "<|>" >> $output_file
-cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file
+cat $ULM_CONTRACTS_TESTING_INPUT_DIR/debug.rs >> $output_file
echo ">)>" >> $output_file
echo "<(<" >> $output_file
@@ -48,6 +48,12 @@ echo "<|>" >> $output_file
cat $ULM_CONTRACTS_TESTING_INPUT_DIR/single_value_mapper.rs >> $output_file
echo ">)>" >> $output_file
+echo "<(<" >> $output_file
+echo "::test_helpers" >> $output_file
+echo "<|>" >> $output_file
+cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file
+echo ">)>" >> $output_file
+
echo "<(<" >> $output_file
echo "::ulm" >> $output_file
echo "<|>" >> $output_file
diff --git a/tests/ulm-contracts/debug.rs b/tests/ulm-contracts/debug.rs
new file mode 100644
index 00000000..98d1c703
--- /dev/null
+++ b/tests/ulm-contracts/debug.rs
@@ -0,0 +1,12 @@
+extern "C" {
+ fn debug_u256(value: u256);
+ fn debug_u160(value: u160);
+ fn debug_u128(value: u128);
+ fn debug_u64(value: u64);
+ fn debug_u32(value: u32);
+ fn debug_u16(value: u16);
+ fn debug_u8(value: u8);
+ fn debug_bool(value: bool);
+ fn debug_str(value: &str);
+ fn debug_unit(value: ());
+}
diff --git a/tests/ulm-with-contract/storage.256.run b/tests/ulm-with-contract/storage.256.run
index 3109aa7c..52e8af47 100644
--- a/tests/ulm-with-contract/storage.256.run
+++ b/tests/ulm-with-contract/storage.256.run
@@ -1,5 +1,5 @@
-mock SetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 , 1000000000000000000000000000000000000000000000000000000000000 ) ulmNoResult();
-mock GetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256);
+mock SetAccountStorageHook ( storageKey("myData256", ) , 1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256 ) ulmNoResult();
+mock GetAccountStorageHook ( storageKey("myData256", ) ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256);
encode_call_data setMyData256(1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256:u256);
return_value;
diff --git a/tests/ulm-with-contract/storage.simple.run b/tests/ulm-with-contract/storage.simple.run
index 6d336cd6..cd6f5647 100644
--- a/tests/ulm-with-contract/storage.simple.run
+++ b/tests/ulm-with-contract/storage.simple.run
@@ -1,5 +1,5 @@
-mock SetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 , 123 ) ulmNoResult();
-mock GetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 ) ulmIntResult(123, u256);
+mock SetAccountStorageHook ( storageKey("myData", ) , 123_u64 ) ulmNoResult();
+mock GetAccountStorageHook ( storageKey("myData", ) ) ulmIntResult(123, u256);
encode_call_data setMyData(123_u64:u64);
return_value;
diff --git a/ulm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md
index 7d0d398c..bc3ed229 100644
--- a/ulm-semantics/main/encoding/encoder.md
+++ b/ulm-semantics/main/encoding/encoder.md
@@ -69,6 +69,17 @@ module ULM-CALLDATA-ENCODER
| "append_u256" [token]
| "append_bool" [token]
| "append_str" [token]
+ | "debug" [token]
+ | "debug_u8" [token]
+ | "debug_u16" [token]
+ | "debug_u32" [token]
+ | "debug_u64" [token]
+ | "debug_u128" [token]
+ | "debug_u160" [token]
+ | "debug_u256" [token]
+ | "debug_bool" [token]
+ | "debug_str" [token]
+ | "debug_unit" [token]
| "empty" [token]
| "length" [token]
@@ -134,6 +145,7 @@ module ULM-CALLDATA-ENCODER
, HeadSize
, Head, Tail
, appendType(T)
+ , debugType(T)
)
, appendValues(Evs, HeadSize, Head, Tail)
)
@@ -159,12 +171,30 @@ module ULM-CALLDATA-ENCODER
=> error("appendType: unrecognized type", ListItem(T))
[owise]
+ syntax PathInExpressionOrError ::= PathInExpression | SemanticsError
+ syntax PathInExpressionOrError ::= debugType(Type) [function, total]
+
+ rule debugType(u8 ) => :: debug :: debug_u8
+ rule debugType(u16 ) => :: debug :: debug_u16
+ rule debugType(u32 ) => :: debug :: debug_u32
+ rule debugType(u64 ) => :: debug :: debug_u64
+ rule debugType(u128) => :: debug :: debug_u128
+ rule debugType(u160) => :: debug :: debug_u160
+ rule debugType(u256) => :: debug :: debug_u256
+
+ rule debugType(bool) => :: debug :: debug_bool
+ rule debugType(()) => :: debug :: debug_unit
+ rule debugType(str) => :: debug :: debug_str
+ rule debugType(T:Type) => error("debugType: unrecognized type", ListItem(T))
+ [owise]
+
syntax NonEmptyStatementsOrError ::= appendValue
( value: Expression
, headSize: Expression
, head: Identifier
, tail: Identifier
, appendFn: AppendTypeOrError
+ , debugFn: PathInExpressionOrError
) [function, total]
rule appendValue
@@ -173,6 +203,16 @@ module ULM-CALLDATA-ENCODER
, head: _Head:Identifier
, tail: _Tail:Identifier
, appendFn: E:SemanticsError
+ , debugFn: _Debug:PathInExpressionOrError
+ )
+ => E
+ rule appendValue
+ (... value: _Value:Expression
+ , headSize: _HeadSize:Expression
+ , head: _Head:Identifier
+ , tail: _Tail:Identifier
+ , appendFn: _Append:AppendType
+ , debugFn: E:SemanticsError
)
=> E
rule appendValue
@@ -181,8 +221,10 @@ module ULM-CALLDATA-ENCODER
, head: Head:Identifier
, tail: _Tail:Identifier
, appendFn: fixedSize(P:PathInExpression)
+ , debugFn: Debug:PathInExpression
)
=> let Head = P ( Head , Value , .CallParamsList );
+ Debug ( Value, .CallParamsList );
.NonEmptyStatements
rule appendValue
(... value: Value:Expression
@@ -190,6 +232,7 @@ module ULM-CALLDATA-ENCODER
, head: Head:Identifier
, tail: Tail:Identifier
, appendFn: variableSize(P:PathInExpression)
+ , debugFn: Debug:PathInExpression
)
=> let Head = :: bytes_hooks :: append_u32
( Head
@@ -197,15 +240,18 @@ module ULM-CALLDATA-ENCODER
, .CallParamsList
);
let Tail = P ( Tail , Value , .CallParamsList );
+ Debug ( Value, .CallParamsList );
.NonEmptyStatements
rule appendValue
- (... value: _Value:Expression
+ (... value: Value:Expression
, headSize: _HeadSize:Expression
, head: _Head:Identifier
, tail: _Tail:Identifier
, appendFn: empty
+ , debugFn: Debug:PathInExpression
)
- => .NonEmptyStatements
+ => Debug ( Value, .CallParamsList );
+ .NonEmptyStatements
syntax ExpressionOrError ::= headSize(Type) [function, total]
rule headSize(u8 ) => v(ptrValue(null, u32(32p32)))
diff --git a/ulm-semantics/main/hooks.md b/ulm-semantics/main/hooks.md
index ad7f659c..0a077f3e 100644
--- a/ulm-semantics/main/hooks.md
+++ b/ulm-semantics/main/hooks.md
@@ -1,6 +1,7 @@
```k
requires "hooks/bytes.md"
+requires "hooks/debug.md"
requires "hooks/helpers.md"
requires "hooks/state.md"
requires "hooks/ulm.md"
@@ -8,6 +9,8 @@ requires "ulm.k"
module ULM-SEMANTICS-HOOKS
imports private ULM-SEMANTICS-HOOKS-BYTES
+ // Not including ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG
+ // here, they should be included directly in the target module.
imports private ULM-SEMANTICS-HOOKS-HELPERS
imports private ULM-SEMANTICS-HOOKS-STATE
imports private ULM-SEMANTICS-HOOKS-ULM
diff --git a/ulm-semantics/main/hooks/bytes.md b/ulm-semantics/main/hooks/bytes.md
index 5111ea00..d11bdbae 100644
--- a/ulm-semantics/main/hooks/bytes.md
+++ b/ulm-semantics/main/hooks/bytes.md
@@ -303,7 +303,6 @@ module ULM-SEMANTICS-HOOKS-BYTES
rule ulmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true))
=> ulmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8)))
- // TODO: This can create key ambiguity for storage
rule ulmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String))
=> ulmBytesAppendLenAndBytes(ulmBytesId(BytesId), String2Bytes(Value))
diff --git a/ulm-semantics/main/hooks/debug.md b/ulm-semantics/main/hooks/debug.md
new file mode 100644
index 00000000..7a6df087
--- /dev/null
+++ b/ulm-semantics/main/hooks/debug.md
@@ -0,0 +1,61 @@
+```k
+
+module ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
+ imports LIST
+
+ configuration
+
+ .List
+
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+ imports RUST-SHARED-SYNTAX
+
+ syntax Instruction ::= debugExpression(Expression)
+endmodule
+
+// Either ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG should be
+// included directly in the target module.
+module ULM-SEMANTICS-HOOKS-NO-DEBUG
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+ rule debugExpression(_:Expression) => .K
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG
+ imports private COMMON-K-CELL
+ imports private RUST-REPRESENTATION
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+ rule debugExpression(E:Expression) => debugExpressionImpl(E)
+
+ syntax Instruction ::= debugExpressionImpl(Expression) [strict(1)]
+
+ rule
+ debugExpressionImpl(V:PtrValue) => .K ...
+
+ ...
+ .List => ListItem(V)
+
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+ imports private RUST-REPRESENTATION
+ imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+ syntax Identifier ::= "debug" [token]
+
+ rule
+ normalizedFunctionCall
+ ( :: debug :: _:Identifier :: .PathExprSegments
+ , ValueId:Ptr, .PtrList
+ )
+ => debugExpression(ValueId)
+
+endmodule
+
+```
diff --git a/ulm-semantics/main/hooks/ulm.md b/ulm-semantics/main/hooks/ulm.md
index eeced224..af09a700 100644
--- a/ulm-semantics/main/hooks/ulm.md
+++ b/ulm-semantics/main/hooks/ulm.md
@@ -6,10 +6,10 @@ module ULM-SEMANTICS-HOOKS-ULM-SYNTAX
syntax UlmHook ::= CallDataHook()
| CallerHook()
- // TODO: Build mocks for all the hooks below in a meaningful
- // way in tests (right now we just use opaque values).
| SetAccountStorageHook(Int, Int)
| GetAccountStorageHook(Int)
+ // TODO: Build mocks for all the hooks below in a meaningful
+ // way in tests (right now we just use opaque values).
| Log0Hook(Bytes)
| Log1Hook(Int, Bytes)
| Log2Hook(Int, Int, Bytes)
diff --git a/ulm-semantics/targets/execution/ulm-target.md b/ulm-semantics/targets/execution/ulm-target.md
index 7b5e705f..40f63ce9 100644
--- a/ulm-semantics/targets/execution/ulm-target.md
+++ b/ulm-semantics/targets/execution/ulm-target.md
@@ -20,7 +20,7 @@ module ULM-TARGET
imports private ULM-DECODING
imports private ULM-ENCODING
imports private ULM-EXECUTION
- imports private ULM-PREPROCESSING
+ imports private ULM-SEMANTICS-HOOKS-NO-DEBUG
imports private ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS
imports private ULM-TARGET-CONFIGURATION
endmodule
diff --git a/ulm-semantics/targets/testing/configuration.md b/ulm-semantics/targets/testing/configuration.md
index e8627a9f..3474a479 100644
--- a/ulm-semantics/targets/testing/configuration.md
+++ b/ulm-semantics/targets/testing/configuration.md
@@ -25,6 +25,7 @@ module ULM-TARGET-CONFIGURATION
imports RUST-EXECUTION-TEST-CONFIGURATION
imports ULM-CONFIGURATION
imports ULM-FULL-PREPROCESSED-CONFIGURATION
+ imports ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION
imports ULM-TEST-CONFIGURATION
@@ -35,6 +36,7 @@ module ULM-TARGET-CONFIGURATION
+
endmodule
diff --git a/ulm-semantics/targets/testing/ulm-target.md b/ulm-semantics/targets/testing/ulm-target.md
index 36b874d0..b60f8438 100644
--- a/ulm-semantics/targets/testing/ulm-target.md
+++ b/ulm-semantics/targets/testing/ulm-target.md
@@ -23,6 +23,7 @@ module ULM-TARGET
imports private ULM-EXECUTION
imports private ULM-ENCODING
imports private ULM-PREPROCESSING
+ imports private ULM-SEMANTICS-HOOKS-DEBUG
imports private ULM-TARGET-CONFIGURATION
imports private ULM-TEST-EXECUTION
endmodule