diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md
index ded77dd1..25755a35 100644
--- a/rust-semantics/expression/literals.md
+++ b/rust-semantics/expression/literals.md
@@ -99,6 +99,7 @@ module RUST-EXPRESSION-INTEGER-LITERALS
andBool isHexadecimal(substrString(S, 1, lengthString(S)))
[owise]
+ rule integerToValue(E:SemanticsError, _) => E
rule integerToValue(I:Int, i8) => i8(Int2MInt(I))
requires sminMInt(8) <=Int I andBool I <=Int smaxMInt(8)
rule integerToValue(I:Int, u8) => u8(Int2MInt(I))
diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md
index ac594985..8a642303 100644
--- a/rust-semantics/helpers.md
+++ b/rust-semantics/helpers.md
@@ -50,5 +50,28 @@ module RUST-HELPERS
rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S
rule concatNonEmptyStatements(S:Statement Ss1:NonEmptyStatements, Ss2:NonEmptyStatements)
=> S concatNonEmptyStatements(Ss1, Ss2)
+
+ rule length(.NormalizedFunctionParameterList) => 0
+ rule length(_:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
+ => 1 +Int length(Ps)
+
+ rule last(P:NormalizedFunctionParameter, .NormalizedFunctionParameterList) => P
+ rule last
+ ( _:NormalizedFunctionParameter
+ , (P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
+ )
+ => last(P, Ps)
+
+ rule allButLast(_:NormalizedFunctionParameter, .NormalizedFunctionParameterList)
+ => .NormalizedFunctionParameterList
+ rule allButLast
+ ( Q:NormalizedFunctionParameter
+ , (P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
+ )
+ => Q , allButLast(P, Ps)
+
+ rule concatCallParamsList(.CallParamsList, S:CallParamsList) => S
+ rule concatCallParamsList(S:Expression , Ss1:CallParamsList, Ss2:CallParamsList)
+ => S , concatCallParamsList(Ss1, Ss2)
endmodule
```
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
index 127d84f2..504e2993 100644
--- a/rust-semantics/representation.md
+++ b/rust-semantics/representation.md
@@ -138,7 +138,7 @@ module RUST-REPRESENTATION
syntax IntOrError ::= Int | SemanticsError
syntax IntOrError ::= valueToInteger(Value) [function, total]
- syntax ValueOrError ::= integerToValue(Int, Type) [function, total]
+ syntax ValueOrError ::= integerToValue(IntOrError, Type) [function, total]
syntax StringOrError ::= String | SemanticsError
@@ -196,6 +196,12 @@ module RUST-REPRESENTATION
syntax NonEmptyStatementsOrError ::= NonEmptyStatements | SemanticsError
syntax NonEmptyStatements ::= concatNonEmptyStatements(NonEmptyStatements, NonEmptyStatements) [function, total]
+ syntax CallParamsList ::= concatCallParamsList(CallParamsList, CallParamsList) [function, total]
+
+ syntax Int ::= length(NormalizedFunctionParameterList) [function, total]
+ syntax NormalizedFunctionParameter ::= last(NormalizedFunctionParameter, NormalizedFunctionParameterList) [function, total]
+ syntax NormalizedFunctionParameterList ::= allButLast(NormalizedFunctionParameter, NormalizedFunctionParameterList) [function, total]
+
endmodule
```
diff --git a/tests/ulm-contracts/ulm.rs b/tests/ulm-contracts/ulm.rs
index d510b2c2..56f50c2c 100644
--- a/tests/ulm-contracts/ulm.rs
+++ b/tests/ulm-contracts/ulm.rs
@@ -1,7 +1,7 @@
#![no_std]
// TODO: Support structs and figure out the content of MessageResult
-struct MessageResult { gas: u64 }
+struct MessageResult { gas: u256 }
pub const EVMC_REJECTED: u64 = 0_u64;
pub const EVMC_INTERNAL_ERROR: u64 = 1_u64;
@@ -22,19 +22,19 @@ pub const EVMC_NONCE_EXCEEDED: u64 = 15_u64;
extern {
// block parameters
- fn sample_method(&self) -> u64;
+ fn sample_method(&self) -> u256;
fn GasLimit(&self) -> u256;
fn BaseFee(&self) -> u256;
- fn Coinbase(&self) -> u64;
- fn BlockTimestamp(&self) -> u64;
- fn BlockNumber(&self) -> u64;
- fn BlockDifficulty(&self) -> u64;
- fn PrevRandao(&self) -> u64;
- fn BlockHash(&self, index: u64) -> u64;
+ fn Coinbase(&self) -> u256;
+ fn BlockTimestamp(&self) -> u256;
+ fn BlockNumber(&self) -> u256;
+ fn BlockDifficulty(&self) -> u256;
+ fn PrevRandao(&self) -> u256;
+ fn BlockHash(&self, index: u256) -> u256;
// transaction parameters
- fn GasPrice(&self) -> u64;
- fn Origin(&self) -> u64;
+ fn GasPrice(&self) -> u256;
+ fn Origin(&self) -> u256;
// message parameters
fn Address(&self) -> u160;
@@ -43,7 +43,7 @@ extern {
fn CallData(&self) -> Bytes;
// chain parameters
- fn ChainId(&self) -> u64;
+ fn ChainId(&self) -> u256;
// account getters
fn GetAccountBalance(&self, acct: u160) -> u256;
@@ -58,17 +58,17 @@ extern {
fn AccessedAccount(&self, acct: u256) -> bool;
fn Transfer(&self, to: u160, value: u256) -> bool;
- fn SelfDestruct(&self, to: u64);
+ fn SelfDestruct(&self, to: u256);
fn SetAccountStorage(&self, key: u256, value: u256);
fn SetAccountTransientStorage(&self, key: u256, value: u256);
fn Log0(data: Bytes);
- fn Log1(topic0: u64, data: Bytes);
- fn Log2(topic0: u64, topic1: u64, data: Bytes);
- fn Log3(topic0: u64, topic1: u64, topic2: u64, data: Bytes);
- fn Log4(topic0: u64, topic1: u64, topic2: u64, topic3: u64, data: Bytes);
+ fn Log1(topic0: u256, data: Bytes);
+ fn Log2(topic0: u256, topic1: u256, data: Bytes);
+ fn Log3(topic0: u256, topic1: u256, topic2: u256, data: Bytes);
+ fn Log4(topic0: u256, topic1: u256, topic2: u256, topic3: u256, data: Bytes);
- fn MessageResult(gas: u256, data: Bytes, status: u64, target: u64) -> MessageResult;
+ fn MessageResult(gas: u256, data: Bytes, status: u256, target: u256) -> MessageResult;
fn Create(value: u256, data: Bytes, gas: u256) -> MessageResult;
fn Create2(value: u256, data: Bytes, salt: Bytes, gas: u256) -> MessageResult;
fn Call(gas: u256, to: u160, value: u256, data: Bytes) -> MessageResult;
diff --git a/tests/ulm-with-contract/erc_20_token.1.run b/tests/ulm-with-contract/erc_20_token.1.run
index b1c8ec05..854e5ad9 100644
--- a/tests/ulm-with-contract/erc_20_token.1.run
+++ b/tests/ulm-with-contract/erc_20_token.1.run
@@ -8,9 +8,11 @@ list_mock GetAccountStorageHook ( 1154948450467236006739439905978168116697077396
list_mock SetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 , 9900 ) ulmNoResult();
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(0, u256);
list_mock SetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 , 100 ) ulmNoResult();
+list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00d" ) ulmNoResult();
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9900, u256);
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 , 200 ) ulmNoResult();
+list_mock Log3Hook ( 63486140976153616755203102783360879283472101686154884697241723088393386309925 , 1010101 , 3030303 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult();
list_mock GetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 ) ulmIntResult(200, u256);
list_mock SetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 , 0 ) ulmNoResult();
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9900, u256);
@@ -18,6 +20,7 @@ list_mock GetAccountStorageHook ( 1154948450467236006739439905978168116697077396
list_mock SetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 , 9700 ) ulmNoResult();
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 , 300 ) ulmNoResult();
+list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult();
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9700, u256);
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(300, u256);
@@ -50,7 +53,7 @@ check_eq 0_u32;
push "balanceOf";
hold_string_from_test_stack;
-push "uint160";
+push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
@@ -74,7 +77,7 @@ check_eq 10000_u256;
push "transfer";
hold_string_from_test_stack;
-push "uint160";
+push "address";
push "uint256";
hold_list_values_from_test_stack;
push 2020202_u160;
@@ -103,7 +106,7 @@ check_eq 1_u64;
push "balanceOf";
hold_string_from_test_stack;
-push "uint160";
+push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
@@ -127,7 +130,7 @@ check_eq 9900_u256;
push "balanceOf";
hold_string_from_test_stack;
-push "uint160";
+push "address";
hold_list_values_from_test_stack;
push 2020202_u160;
hold_list_values_from_test_stack;
@@ -151,7 +154,7 @@ check_eq 100_u256;
push "approve";
hold_string_from_test_stack;
-push "uint160";
+push "address";
push "uint256";
hold_list_values_from_test_stack;
push 3030303_u160;
@@ -180,8 +183,8 @@ check_eq 1_u64;
push "transferFrom";
hold_string_from_test_stack;
-push "uint160";
-push "uint160";
+push "address";
+push "address";
push "uint256";
hold_list_values_from_test_stack;
push 1010101_u160;
@@ -212,7 +215,7 @@ check_eq 1_u64;
push "balanceOf";
hold_string_from_test_stack;
-push "uint160";
+push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
@@ -237,7 +240,7 @@ check_eq 9700_u256;
push "balanceOf";
hold_string_from_test_stack;
-push "uint160";
+push "address";
hold_list_values_from_test_stack;
push 2020202_u160;
hold_list_values_from_test_stack;
diff --git a/tests/ulm-with-contract/events.1.run b/tests/ulm-with-contract/events.1.run
index 34f870c4..a777cae0 100644
--- a/tests/ulm-with-contract/events.1.run
+++ b/tests/ulm-with-contract/events.1.run
@@ -1,3 +1,5 @@
+list_mock Log2Hook ( 74657075023537209477280918141328480329188930599530356189395812678724488965561 , 123 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02+" ) ulmNoResult();
+
push "logEvent";
hold_string_from_test_stack;
push "uint64";
diff --git a/ulm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md
index 84dd82df..f769b9ce 100644
--- a/ulm-semantics/main/encoding/encoder.md
+++ b/ulm-semantics/main/encoding/encoder.md
@@ -52,15 +52,31 @@ module ULM-CALLDATA-ENCODER
imports private BYTES
imports private INT-SYNTAX
imports private KRYPTO
+ imports private RUST-ERROR-SYNTAX
imports private STRING
imports private ULM-ENCODING-SYNTAX
imports private ULM-ENCODING-HELPER-SYNTAX
imports private ULM-ENCODING-HELPER
+ syntax Identifier ::= "bytes_hooks" [token]
+ | "append_u8" [token]
+ | "append_u16" [token]
+ | "append_u32" [token]
+ | "append_u64" [token]
+ | "append_u128" [token]
+ | "append_u160" [token]
+ | "append_u256" [token]
+ | "append_bool" [token]
+
+
rule encodeFunctionSignatureAsBytes(FS)
=> encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8))
rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E
+ rule encodeEventSignatureAsInt(FS)
+ => Bytes2Int(Keccak256raw(String2Bytes(FS)), BE, Unsigned)
+ rule encodeEventSignatureAsInt(E:SemanticsError) => E
+
// TODO: it may be worth extracting the substrString(Keccak256(String2Bytes(FS)), 0, 8)
// thing to a function that takes a String and produces a String or Bytes (as opposed to
// taking a StringOrError as below) (perhaps with an encodeAsBytes(...) on top of it) and
@@ -88,6 +104,62 @@ module ULM-CALLDATA-ENCODER
encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T))
rule encodeFunctionParams(.List, .List, B:Bytes) => B
+
+ rule appendValue(BufferId:Identifier, Value:Identifier, u8)
+ => v(:: bytes_hooks :: append_u8 ( BufferId , Value , .CallParamsList ))
+ rule appendValue(BufferId:Identifier, Value:Identifier, u16)
+ => v(:: bytes_hooks :: append_u16 ( BufferId , Value , .CallParamsList ))
+ rule appendValue(BufferId:Identifier, Value:Identifier, u32)
+ => 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, u128)
+ => v(:: bytes_hooks :: append_u128 ( BufferId , Value , .CallParamsList ))
+ rule appendValue(BufferId:Identifier, Value:Identifier, u160)
+ => v(:: bytes_hooks :: append_u160 ( BufferId , Value , .CallParamsList ))
+ rule appendValue(BufferId:Identifier, Value:Identifier, u256)
+ => v(:: bytes_hooks :: append_u256 ( 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)))
+ [owise]
+
+ rule methodSignature(S:String, Ps:NormalizedFunctionParameterList)
+ => encodeFunctionSignatureAsBytes(concat(concat(S +String "(", signatureTypes(Ps)), ")"))
+
+ rule eventSignature(S, Ps)
+ => integerToValue
+ ( encodeEventSignatureAsInt
+ (concat(concat(S +String "(", signatureTypes(Ps)), ")"))
+ , u256
+ )
+
+ syntax StringOrError ::= signatureTypes(NormalizedFunctionParameterList) [function, total]
+ | signatureType(Type) [function, total]
+
+ rule signatureTypes(.NormalizedFunctionParameterList) => ""
+ rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList)
+ => signatureType(T)
+ rule signatureTypes
+ ( _ : T:Type
+ , ((_:NormalizedFunctionParameter , _:NormalizedFunctionParameterList)
+ #as Ps:NormalizedFunctionParameterList)
+ )
+ => concat(signatureType(T), concat(",", signatureTypes(Ps)))
+
+ rule signatureType(u8) => "uint8"
+ rule signatureType(u16) => "uint16"
+ rule signatureType(u32) => "uint32"
+ rule signatureType(u64) => "uint64"
+ rule signatureType(u128) => "uint128"
+ // TODO: This is the wrong signature type. We should separate addresses from u160.
+ rule signatureType(u160) => "address"
+ rule signatureType(u256) => "uint256"
+ rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T))
+ [owise]
+
endmodule
```
\ No newline at end of file
diff --git a/ulm-semantics/main/encoding/syntax.md b/ulm-semantics/main/encoding/syntax.md
index 8f89ca49..9ec34ae4 100644
--- a/ulm-semantics/main/encoding/syntax.md
+++ b/ulm-semantics/main/encoding/syntax.md
@@ -16,6 +16,12 @@ module ULM-ENCODING-SYNTAX
| encodeFunctionParams (List, List, Bytes) [function]
syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total]
+ syntax IntOrError ::= encodeEventSignatureAsInt(StringOrError) [function, total]
+
+ syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total]
+ syntax ValueOrError ::= eventSignature(String, NormalizedFunctionParameterList) [function, total]
+
+ syntax ExpressionOrError ::= appendValue(bufferId: Identifier, value: Identifier, Type) [function, total]
endmodule
diff --git a/ulm-semantics/main/hooks/ulm.md b/ulm-semantics/main/hooks/ulm.md
index 87899455..eeced224 100644
--- a/ulm-semantics/main/hooks/ulm.md
+++ b/ulm-semantics/main/hooks/ulm.md
@@ -2,11 +2,19 @@
module ULM-SEMANTICS-HOOKS-ULM-SYNTAX
imports INT-SYNTAX
+ imports BYTES-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)
+ | Log0Hook(Bytes)
+ | Log1Hook(Int, Bytes)
+ | Log2Hook(Int, Int, Bytes)
+ | Log3Hook(Int, Int, Int, Bytes)
+ | Log4Hook(Int, Int, Int, Int, Bytes)
syntax K
syntax Type
@@ -18,6 +26,7 @@ endmodule
module ULM-SEMANTICS-HOOKS-ULM
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX
+ imports private ULM-HOOKS
imports private ULM-SEMANTICS-HOOKS-SIGNATURE
imports private ULM-SEMANTICS-HOOKS-ULM-SYNTAX
imports private ULM-REPRESENTATION
@@ -27,6 +36,11 @@ module ULM-SEMANTICS-HOOKS-ULM
| "Caller" [token]
| "SetAccountStorage" [token]
| "GetAccountStorage" [token]
+ | "Log0" [token]
+ | "Log1" [token]
+ | "Log2" [token]
+ | "Log3" [token]
+ | "Log4" [token]
rule normalizedFunctionCall ( :: ulm :: CallData :: .PathExprSegments , .PtrList )
=> CallDataHook()
@@ -58,6 +72,122 @@ module ULM-SEMANTICS-HOOKS-ULM
rule #GetAccountStorageHook(ptrValue(_, u256(Key)))
=> GetAccountStorageHook(MInt2Unsigned(Key))
+
+ rule normalizedFunctionCall
+ ( :: ulm :: Log0 :: .PathExprSegments
+ , (BytesPtr:Ptr , .PtrList)
+ )
+ => #Log0Hook(BytesPtr)
+
+ syntax UlmHook ::= #Log0Hook(Expression) [strict]
+ | #Log0Hook(UlmExpression) [strict]
+
+ rule #Log0Hook(ptrValue(_, u64(BytesId)))
+ => #Log0Hook(ulmBytesId(BytesId))
+ rule #Log0Hook(ulmBytesValue(B:Bytes)) => Log0Hook(B)
+
+
+ rule normalizedFunctionCall
+ ( :: ulm :: Log1 :: .PathExprSegments
+ , (V0:Ptr, BytesPtr:Ptr , .PtrList)
+ )
+ => #Log1Hook(ulmCast(V0, ptrValue(null, rustType(u256))), BytesPtr)
+
+ syntax UlmHook ::= #Log1Hook(Expression, Expression) [seqstrict]
+ | #Log1Hook(Int, UlmExpression) [strict(2)]
+
+ rule #Log1Hook(ptrValue(_, u256(V0)), ptrValue(_, u64(BytesId)))
+ => #Log1Hook(MInt2Unsigned(V0), ulmBytesId(BytesId))
+ rule #Log1Hook(V0:Int, ulmBytesValue(B:Bytes)) => Log1Hook(V0, B)
+
+
+ rule normalizedFunctionCall
+ ( :: ulm :: Log2 :: .PathExprSegments
+ , (V0:Ptr, V1:Ptr, BytesPtr:Ptr , .PtrList)
+ )
+ => #Log2Hook
+ ( ulmCast(V0, ptrValue(null, rustType(u256)))
+ , ulmCast(V1, ptrValue(null, rustType(u256)))
+ , BytesPtr
+ )
+
+ syntax UlmHook ::= #Log2Hook(Expression, Expression, Expression) [seqstrict]
+ | #Log2Hook(Int, Int, UlmExpression) [strict(3)]
+
+ rule #Log2Hook
+ ( ptrValue(_, u256(V0))
+ , ptrValue(_, u256(V1))
+ , ptrValue(_, u64(BytesId))
+ )
+ => #Log2Hook
+ ( MInt2Unsigned(V0)
+ , MInt2Unsigned(V1)
+ , ulmBytesId(BytesId)
+ )
+ rule #Log2Hook(V0:Int, V1:Int, ulmBytesValue(B:Bytes)) => Log2Hook(V0, V1, B)
+
+
+ rule normalizedFunctionCall
+ ( :: ulm :: Log3 :: .PathExprSegments
+ , (V0:Ptr, V1:Ptr, V2:Ptr, BytesPtr:Ptr , .PtrList)
+ )
+ => #Log3Hook
+ ( ulmCast(V0, ptrValue(null, rustType(u256)))
+ , ulmCast(V1, ptrValue(null, rustType(u256)))
+ , ulmCast(V2, ptrValue(null, rustType(u256)))
+ , BytesPtr
+ )
+
+ syntax UlmHook ::= #Log3Hook(Expression, Expression, Expression, Expression) [seqstrict]
+ | #Log3Hook(Int, Int, Int, UlmExpression) [strict(4)]
+
+ rule #Log3Hook
+ ( ptrValue(_, u256(V0))
+ , ptrValue(_, u256(V1))
+ , ptrValue(_, u256(V2))
+ , ptrValue(_, u64(BytesId))
+ )
+ => #Log3Hook
+ ( MInt2Unsigned(V0)
+ , MInt2Unsigned(V1)
+ , MInt2Unsigned(V2)
+ , ulmBytesId(BytesId)
+ )
+ rule #Log3Hook(V0:Int, V1:Int, V2:Int, ulmBytesValue(B:Bytes)) => Log3Hook(V0, V1, V2, B)
+
+
+ rule normalizedFunctionCall
+ ( :: ulm :: Log4 :: .PathExprSegments
+ , (V0:Ptr, V1:Ptr, V2:Ptr, V3:Ptr, BytesPtr:Ptr , .PtrList)
+ )
+ => #Log4Hook
+ ( ulmCast(V0, ptrValue(null, rustType(u256)))
+ , ulmCast(V1, ptrValue(null, rustType(u256)))
+ , ulmCast(V2, ptrValue(null, rustType(u256)))
+ , ulmCast(V3, ptrValue(null, rustType(u256)))
+ , BytesPtr
+ )
+
+ syntax UlmHook ::= #Log4Hook(Expression, Expression, Expression, Expression, Expression) [seqstrict]
+ | #Log4Hook(Int, Int, Int, Int, UlmExpression) [strict(4)]
+
+ rule #Log4Hook
+ ( ptrValue(_, u256(V0))
+ , ptrValue(_, u256(V1))
+ , ptrValue(_, u256(V2))
+ , ptrValue(_, u256(V4))
+ , ptrValue(_, u64(BytesId))
+ )
+ => #Log4Hook
+ ( MInt2Unsigned(V0)
+ , MInt2Unsigned(V1)
+ , MInt2Unsigned(V2)
+ , MInt2Unsigned(V4)
+ , ulmBytesId(BytesId)
+ )
+ rule #Log4Hook(V0:Int, V1:Int, V2:Int, V4:Int, ulmBytesValue(B:Bytes)) => Log4Hook(V0, V1, V2, V4, B)
+
+
rule ulmNoResult() => ptrValue(null, tuple(.ValueList))
rule ulmIntResult(Value:Int, T:Type) => ulmValueResult(integerToValue(Value, T))
@@ -78,6 +208,11 @@ module ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS
rule CallerHook() => ulmIntResult(Caller(), u160)
rule SetAccountStorageHook(Key:Int, Value:Int) => SetAccountStorage(Key, Value) ~> ulmNoResult()
rule GetAccountStorageHook(Key:Int) => ulmIntResult(GetAccountStorage(Key), u256)
+ rule Log0Hook(V:Bytes) => Log0(V) ~> ulmNoResult()
+ rule Log1Hook(V0:Int, V:Bytes) => Log1(V0, V) ~> ulmNoResult()
+ rule Log2Hook(V0:Int, V1:Int, V:Bytes) => Log2(V0, V1, V) ~> ulmNoResult()
+ rule Log3Hook(V0:Int, V1:Int, V2:Int, V:Bytes) => Log3(V0, V1, V2, V) ~> ulmNoResult()
+ rule Log4Hook(V0:Int, V1:Int, V2:Int, V3:Int, V:Bytes) => Log4(V0, V1, V2, V3, V) ~> ulmNoResult()
endmodule
module ULM-SEMANTICS-HOOKS-SIGNATURE
diff --git a/ulm-semantics/main/preprocessing/endpoints.md b/ulm-semantics/main/preprocessing/endpoints.md
index d4b46a07..ee261139 100644
--- a/ulm-semantics/main/preprocessing/endpoints.md
+++ b/ulm-semantics/main/preprocessing/endpoints.md
@@ -181,33 +181,6 @@ module ULM-PREPROCESSING-ENDPOINTS
| "EVMC_REVERT" [token]
| "EVMC_SUCCESS" [token]
- syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total]
- syntax StringOrError ::= signatureTypes(NormalizedFunctionParameterList) [function, total]
- | signatureType(Type) [function, total]
-
- rule methodSignature(S:String, Ps:NormalizedFunctionParameterList)
- => encodeFunctionSignatureAsBytes(concat(concat(S +String "(", signatureTypes(Ps)), ")"))
-
- rule signatureTypes(.NormalizedFunctionParameterList) => ""
- rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList)
- => signatureType(T)
- rule signatureTypes
- ( _ : T:Type
- , ((_:NormalizedFunctionParameter , _:NormalizedFunctionParameterList)
- #as Ps:NormalizedFunctionParameterList)
- )
- => concat(signatureType(T), concat(",", signatureTypes(Ps)))
-
- rule signatureType(u8) => "uint8"
- rule signatureType(u16) => "uint16"
- rule signatureType(u32) => "uint32"
- rule signatureType(u64) => "uint64"
- rule signatureType(u128) => "uint128"
- rule signatureType(u160) => "uint160"
- rule signatureType(u256) => "uint256"
- rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T))
- [owise]
-
syntax Statement ::= signatureToCall
( signature: Identifier
, signatures: List
@@ -245,28 +218,6 @@ module ULM-PREPROCESSING-ENDPOINTS
syntax Expression ::= decodeSignature(Identifier) [function, total]
rule decodeSignature(BufferId) => :: bytes_hooks :: decode_signature ( BufferId , .CallParamsList )
- syntax ExpressionOrError ::= appendValue(bufferId: Identifier, value: Identifier, Type) [function, total]
- rule appendValue(BufferId:Identifier, Value:Identifier, u8)
- => v(:: bytes_hooks :: append_u8 ( BufferId , Value , .CallParamsList ))
- rule appendValue(BufferId:Identifier, Value:Identifier, u16)
- => v(:: bytes_hooks :: append_u16 ( BufferId , Value , .CallParamsList ))
- rule appendValue(BufferId:Identifier, Value:Identifier, u32)
- => 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, u128)
- => v(:: bytes_hooks :: append_u128 ( BufferId , Value , .CallParamsList ))
- rule appendValue(BufferId:Identifier, Value:Identifier, u160)
- => v(:: bytes_hooks :: append_u160 ( BufferId , Value , .CallParamsList ))
- rule appendValue(BufferId:Identifier, Value:Identifier, u256)
- => v(:: bytes_hooks :: append_u256 ( 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)))
- [owise]
-
syntax NonEmptyStatementsOrError ::= decodeParams(Int, NormalizedFunctionParameterList) [function, total]
rule decodeParams(_:Int, .NormalizedFunctionParameterList) => .NonEmptyStatements
rule decodeParams(Index:Int, _ : T:Type , Ps:NormalizedFunctionParameterList)
diff --git a/ulm-semantics/main/preprocessing/events.md b/ulm-semantics/main/preprocessing/events.md
index 3f8c1b3e..d13c5af1 100644
--- a/ulm-semantics/main/preprocessing/events.md
+++ b/ulm-semantics/main/preprocessing/events.md
@@ -2,24 +2,103 @@
module ULM-PREPROCESSING-EVENTS
imports private COMMON-K-CELL
+ imports private RUST-ERROR-SYNTAX
imports private RUST-PREPROCESSING-CONFIGURATION
+ imports private ULM-ENCODING-SYNTAX
imports private ULM-PREPROCESSING-SYNTAX-PRIVATE
+ syntax Identifier ::= "bytes_hooks" [token]
+ | "data" [token]
+ | "empty" [token]
+ | "Log0" [token]
+ | "Log1" [token]
+ | "Log2" [token]
+ | "Log3" [token]
+ | "Log4" [token]
+ | "ulm" [token]
+
+ syntax UkmInstruction ::= #ulmPreprocessEvent
+ ( method: PathInExpression
+ , appendLastParam: ExpressionOrError
+ , logIdentifier: IdentifierOrError
+ , eventSignature: ValueOrError
+ )
+
rule
ulmPreprocessEvent
(... fullMethodPath: Method:PathInExpression
- , eventName: _EventName:String
+ , eventName: EventName:String
+ )
+ // TODO: This handles a very specific type of event: all fields
+ // but the last one are indexed. We should handle generic events.
+ => #ulmPreprocessEvent
+ ( Method
+ , appendParamToBytes(data, last(Param, Params))
+ , findLogIdentifier(1 +Int length(Params))
+ , eventSignature(EventName, (Param , Params))
+ )
+ ...
+
+ Method
+ (self : $selftype , Param:NormalizedFunctionParameter, Params:NormalizedFunctionParameterList)
+ empty
+ ()
+
+ rule
+
+ #ulmPreprocessEvent
+ (... method: Method:PathInExpression
+ , appendLastParam: v(AppendLast:Expression)
+ , logIdentifier: LogIdentifier:Identifier
+ , eventSignature: EventSignature:Value
)
=> .K
...
Method
+ (self : $selftype , Param:NormalizedFunctionParameter, Params:NormalizedFunctionParameterList)
- empty => block({.InnerAttributes .NonEmptyStatements})
+ empty => block({
+ .InnerAttributes
+ let data = :: bytes_hooks :: empty ( .CallParamsList );
+ let data = AppendLast;
+ :: ulm :: LogIdentifier
+ ( ptrValue(null, EventSignature)
+ , concatCallParamsList
+ ( paramsToArgs(allButLast(Param, Params))
+ , (data , .CallParamsList)
+ )
+ );
+ .NonEmptyStatements
+ })
()
+ syntax ExpressionOrError ::= appendParamToBytes
+ ( bufferId: Identifier
+ , NormalizedFunctionParameter
+ ) [function, total]
+ rule appendParamToBytes(B:Identifier, (I:Identifier : T:Type)) => appendValue(B, I, T)
+ rule appendParamToBytes(B, P)
+ => e(error("appendParamToBytes: unrecognized param", ListItem(B) ListItem(P)))
+ [owise]
+
+ syntax IdentifierOrError ::= findLogIdentifier(Int) [function, total]
+ rule findLogIdentifier(1) => Log1
+ rule findLogIdentifier(2) => Log2
+ rule findLogIdentifier(3) => Log3
+ rule findLogIdentifier(4) => Log4
+ rule findLogIdentifier(I:Int) => error("findLogIdentifier: unhandled arity", ListItem(I))
+ [owise]
+
+ syntax CallParamsList ::= paramsToArgs(NormalizedFunctionParameterList) [function, total]
+ rule paramsToArgs(.NormalizedFunctionParameterList) => .CallParamsList
+ rule paramsToArgs((P:Identifier : _:Type) , Ps:NormalizedFunctionParameterList)
+ => P , paramsToArgs(Ps)
+ rule paramsToArgs((S:SelfSort : _:Type) , Ps:NormalizedFunctionParameterList)
+ => S , paramsToArgs(Ps)
+
endmodule
```