From ff3d6efd870aca6cea94f13f806e5411c344c1d4 Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Fri, 8 Nov 2024 17:25:12 +0200 Subject: [PATCH] Implement logging (#183) * Implement logging * Add TODOs --- rust-semantics/expression/literals.md | 1 + rust-semantics/helpers.md | 23 +++ rust-semantics/representation.md | 8 +- tests/ulm-contracts/ulm.rs | 34 ++--- tests/ulm-with-contract/erc_20_token.1.run | 21 +-- tests/ulm-with-contract/events.1.run | 2 + ulm-semantics/main/encoding/encoder.md | 72 ++++++++++ ulm-semantics/main/encoding/syntax.md | 6 + ulm-semantics/main/hooks/ulm.md | 135 ++++++++++++++++++ ulm-semantics/main/preprocessing/endpoints.md | 49 ------- ulm-semantics/main/preprocessing/events.md | 83 ++++++++++- 11 files changed, 356 insertions(+), 78 deletions(-) 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 ```