diff --git a/Makefile b/Makefile
index e052e85..28e672a 100644
--- a/Makefile
+++ b/Makefile
@@ -108,7 +108,7 @@ build-legacy: \
$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
-test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test
+test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test ukm-with-contracts-test
test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
@@ -451,6 +451,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp
echo ">)>" >> $@.in.tmp
+ echo "<(<" >> $@.in.tmp
+ echo "::test_helpers" >> $@.in.tmp
+ echo "<|>" >> $@.in.tmp
+ cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/test_helpers.rs >> $@.in.tmp
+ echo ">)>" >> $@.in.tmp
+
echo "<(<" >> $@.in.tmp
echo "::state_hooks" >> $@.in.tmp
echo "<|>" >> $@.in.tmp
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index 5e71ed2..621248f 100644
--- a/rust-semantics/test/execution.md
+++ b/rust-semantics/test/execution.md
@@ -13,6 +13,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
| "return_value_to_arg"
| "check_eq" Expression [strict]
| "push" Expression [strict]
+ | "push_value" Expression [strict]
syntax KItem ::= mock(KItem, K)
endmodule
@@ -93,6 +94,12 @@ module RUST-EXECUTION-TEST
VALUES:Map => VALUES[NVI <- V]
NVI:Int => NVI +Int 1
+ rule
+ push_value ptrValue(_, V:Value) => .K ...
+ .List => ListItem(ptrValue(ptr(NVI), V)) ...
+ VALUES:Map => VALUES[NVI <- V]
+ NVI:Int => NVI +Int 1
+
syntax KItem ::= wrappedK(K)
syntax Mockable
@@ -106,4 +113,4 @@ module RUST-EXECUTION-TEST
[priority(10)]
endmodule
-```
\ No newline at end of file
+```
diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs
index 25d1ee1..ae8e34a 100644
--- a/tests/ukm-contracts/bytes_hooks.rs
+++ b/tests/ukm-contracts/bytes_hooks.rs
@@ -7,6 +7,7 @@ extern "C" {
fn append_u32(bytes_id: u64, value: u32) -> u64;
fn append_u16(bytes_id: u64, value: u16) -> u64;
fn append_u8(bytes_id: u64, value: u8) -> u64;
+ fn append_bool(bytes_id: u64, value: bool) -> u64;
fn append_str(bytes_id: u64, value: &str) -> u64;
fn decode_u128(bytes_id: u64) -> (u64, u128);
diff --git a/tests/ukm-contracts/test_helpers.rs b/tests/ukm-contracts/test_helpers.rs
new file mode 100644
index 0000000..e3be902
--- /dev/null
+++ b/tests/ukm-contracts/test_helpers.rs
@@ -0,0 +1,8 @@
+
+fn decode_single_u64(bytes_id: u64) -> u64 {
+ let (remaining_id, value) = :: bytes_hooks :: decode_u64(bytes_id);
+ if :: bytes_hooks :: length(remaining_id) > 0_u32 {
+ fail();
+ };
+ value
+}
diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run
index 7ed3553..4264f65 100644
--- a/tests/ukm-with-contract/endpoints.1.run
+++ b/tests/ukm-with-contract/endpoints.1.run
@@ -16,7 +16,7 @@ push_status;
check_eq 2;
output_to_arg;
-call :: endpoints :: decode_single_u64;
+call :: test_helpers :: decode_single_u64;
return_value;
check_eq 126_u64
diff --git a/tests/ukm-with-contract/endpoints.rs b/tests/ukm-with-contract/endpoints.rs
index 9fc6650..2fd7f61 100644
--- a/tests/ukm-with-contract/endpoints.rs
+++ b/tests/ukm-with-contract/endpoints.rs
@@ -13,11 +13,3 @@ pub trait Endpoints {
value + 3_u64
}
}
-
-fn decode_single_u64(bytes_id: u64) -> u64 {
- let (remaining_id, value) = :: bytes_hooks :: decode_u64(bytes_id);
- if :: bytes_hooks :: length(remaining_id) > 0_u32 {
- fail();
- };
- value
-}
diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md
index bf6acd3..9b25d37 100644
--- a/ukm-semantics/main/hooks/bytes.md
+++ b/ukm-semantics/main/hooks/bytes.md
@@ -38,6 +38,7 @@ module UKM-HOOKS-BYTES
| "append_u32" [token]
| "append_u16" [token]
| "append_u8" [token]
+ | "append_bool" [token]
| "append_str" [token]
| "decode_u128" [token]
| "decode_u64" [token]
@@ -105,6 +106,13 @@ module UKM-HOOKS-BYTES
)
=> ukmBytesAppendInt(BufferIdId, IntId)
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_bool :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendBool(BufferIdId, IntId)
+
rule
normalizedFunctionCall
( :: bytes_hooks :: append_str :: .PathExprSegments
@@ -170,6 +178,7 @@ module UKM-HOOKS-BYTES
| ukmBytesLength(UkmExpression) [strict(1)]
| ukmBytesAppendInt(Expression, Expression) [seqstrict]
| ukmBytesAppendInt(UkmExpression, Int) [strict(1)]
+ | ukmBytesAppendBool(Expression, Expression) [seqstrict]
| ukmBytesAppendStr(Expression, Expression) [seqstrict]
| ukmBytesAppendBytes(UkmExpression, Bytes) [strict(1)]
| ukmBytesAppendLenAndBytes(Bytes, Bytes)
@@ -212,6 +221,11 @@ module UKM-HOOKS-BYTES
rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int)
=> ukmBytesAppendLenAndBytes(B, Int2Bytes(Value, BE, Unsigned))
+ rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, false))
+ => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(0p8)))
+ rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true))
+ => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8)))
+
rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String))
=> ukmBytesAppendBytes(ukmBytesId(BytesId), String2Bytes(Value))
diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md
index b6d2a41..b6343f8 100644
--- a/ukm-semantics/main/hooks/ukm.md
+++ b/ukm-semantics/main/hooks/ukm.md
@@ -1,7 +1,8 @@
```k
module UKM-HOOKS-UKM-SYNTAX
- syntax UkmHook ::= CallDataHook()
+ syntax UkmHook ::= CallDataHook()
+ | CallerHook()
endmodule
@@ -12,9 +13,12 @@ module UKM-HOOKS-UKM
syntax Identifier ::= "ukm" [token]
| "CallData" [token]
+ | "Caller" [token]
- rule normalizedFunctionCall ( ukm :: CallData :: .PathExprSegments , .PtrList )
+ rule normalizedFunctionCall ( :: ukm :: CallData :: .PathExprSegments , .PtrList )
=> CallDataHook()
+ rule normalizedFunctionCall ( :: ukm :: Caller :: .PathExprSegments , .PtrList )
+ => CallerHook()
endmodule
```
diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md
index b97b986..33accc4 100644
--- a/ukm-semantics/main/preprocessing/endpoints.md
+++ b/ukm-semantics/main/preprocessing/endpoints.md
@@ -121,7 +121,7 @@ module UKM-PREPROCESSING-ENDPOINTS
block({
.InnerAttributes
concatNonEmptyStatements
- ( let buffer_id = ukm :: CallData();
+ ( let buffer_id = :: ukm :: CallData();
let ( buffer_id | .PatternNoTopAlts
, signature | .PatternNoTopAlts
, .Patterns
@@ -151,6 +151,7 @@ module UKM-PREPROCESSING-ENDPOINTS
| "append_u16" [token]
| "append_u32" [token]
| "append_u64" [token]
+ | "append_bool" [token]
| "decode_u8" [token]
| "decode_u16" [token]
| "decode_u32" [token]
@@ -232,6 +233,8 @@ module UKM-PREPROCESSING-ENDPOINTS
=> v(:: bytes_hooks :: append_u32 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u64)
=> v(:: bytes_hooks :: append_u64 ( BufferId , Value , .CallParamsList ))
+ rule appendValue(BufferId:Identifier, Value:Identifier, bool)
+ => v(:: bytes_hooks :: append_bool ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, _Value:Identifier, ()) => v(BufferId)
rule appendValue(BufferId:Identifier, Value:Identifier, T:Type)
=> e(error("appendValue: unrecognized type", ListItem(BufferId) ListItem(Value) ListItem(T)))
diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
index b407c07..de0d56c 100644
--- a/ukm-semantics/test/execution.md
+++ b/ukm-semantics/test/execution.md
@@ -5,6 +5,7 @@ module UKM-TEST-SYNTAX
imports RUST-EXECUTION-TEST-PARSING-SYNTAX
syntax ExecutionItem ::= "mock" "CallData"
+ | "mock" "Caller"
| "call_contract" Int
| "output_to_arg"
| "push_status"
@@ -30,6 +31,13 @@ module UKM-TEST-EXECUTION
...
+ rule
+ mock Caller => mock(CallerHook(), V) ...
+
+ (ListItem(ptrValue(_, u64(_BytesId)) #as V:PtrValue) => .List)
+ ...
+
+
rule call_contract Account => ukmExecute(Account, 100)
rule