Skip to content

Commit

Permalink
Use explicit values for logging mocks
Browse files Browse the repository at this point in the history
  • Loading branch information
virgil-serbanuta committed Nov 25, 2024
1 parent 6cc98d8 commit 212be93
Show file tree
Hide file tree
Showing 3 changed files with 46 additions and 6 deletions.
6 changes: 3 additions & 3 deletions tests/ulm-with-contract/erc_20_token.1.run
Original file line number Diff line number Diff line change
Expand Up @@ -8,19 +8,19 @@ list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ul
list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9900_u256 ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(0, u256);
list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 100_u256 ) 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 Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(100_u256:u256) ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256);
list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 200_u256 ) 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 Log3Hook ( eventSignature("Approval(address,address,uint256)") , 1010101 , 3030303 , encodeValues(200_u256:u256) ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) ) ulmIntResult(200, u256);
list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 0_u256 ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256);
list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256);
list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9700_u256 ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 300_u256 ) 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 Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(200_u256:u256) ) ulmNoResult();
list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9700, u256);
list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(300, u256);

Expand Down
2 changes: 0 additions & 2 deletions ulm-semantics/main/hooks/ulm.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ module ULM-SEMANTICS-HOOKS-ULM-SYNTAX
| CallerHook()
| 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)
Expand Down
44 changes: 43 additions & 1 deletion ulm-semantics/test/execution.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,11 @@ module ULM-TEST-SYNTAX
syntax UlmTestHook ::= SetAccountStorageHook(StorageKey, Expression) [seqstrict, result(TestResult)]
| GetAccountStorageHook(StorageKey) [seqstrict, result(TestResult)]
| Log3Hook(EventSignature, Int, Int, EncodeValues) [seqstrict(1, 4), result(TestResult)]
syntax StorageKey ::= storageKey(String, EncodeArgs)
syntax EventSignature ::= eventSignature(String)
syntax EncodeValues ::= encodeValues(EncodeArgs)
endmodule
module ULM-TEST-EXECUTION
Expand All @@ -68,7 +71,7 @@ module ULM-TEST-EXECUTION
syntax UlmTestHook ::= #SetAccountStorageHook(Int, IntOrError)
| #GetAccountStorageHook(Int)
| #Log3Hook(Int, Int, Int, Bytes)
syntax Mockable ::= UlmHook
syntax BytesOrError ::= extractCallSignature(EncodeCall) [function, total]
Expand Down Expand Up @@ -208,9 +211,12 @@ module ULM-TEST-EXECUTION
syntax Bool ::= isTestResult(K) [symbol(isTestResult), function]
rule isTestResult(_:K) => false [owise]
rule isTestResult(evaluatedStorageKey(_:Bytes)) => true
rule isTestResult(evaluatedEventSignature(_:Int)) => true
rule isTestResult(encodedValues(_:Bytes)) => true
rule isTestResult(_:PtrValue) => true
rule isTestResult(#SetAccountStorageHook(_:Int, _:Int)) => true
rule isTestResult(#GetAccountStorageHook(_:Int)) => true
rule isTestResult(#Log3Hook(_:Int, _:Int, _:Int, _:Bytes)) => true
syntax StorageKey ::= storageKey(NonEmptyStatementsOrError)
| storageKey(Expression) [strict(1)]
Expand All @@ -232,6 +238,30 @@ module ULM-TEST-EXECUTION
rule storageKey(ptrValue(_, u64(BytesId))) => storageKey(ulmBytesId(BytesId))
rule storageKey(ulmBytesValue(B:Bytes)) => evaluatedStorageKey(B)
syntax EventSignature ::= evaluatedEventSignature(Int)
rule eventSignature(Signature:String)
=> evaluatedEventSignature(Bytes2Int(Keccak256raw(String2Bytes(Signature)), BE, Unsigned))
syntax EncodeValues ::= encodeValues(NonEmptyStatementsOrError)
| encodeValues(Expression) [strict(1)]
| encodeValues(UlmExpression) [strict(1)]
| encodedValues(Bytes)
rule encodeValues(Args:EncodeArgs)
=> encodeValues
( concat
( let buffer_id = :: bytes_hooks :: empty( .CallParamsList );
.NonEmptyStatements
, encodeStatements
( buffer_id
, encodeArgsToEncodeValues(Args)
)
)
)
rule encodeValues(Statements:NonEmptyStatements)
=> encodeValues({.InnerAttributes Statements buffer_id })
rule encodeValues(ptrValue(_, u64(BytesId))) => encodeValues(ulmBytesId(BytesId))
rule encodeValues(ulmBytesValue(B:Bytes)) => encodedValues(B)
rule SetAccountStorageHook(evaluatedStorageKey(B:Bytes), ptrValue(_, Value:Value))
=> #SetAccountStorageHook
( Bytes2Int(Keccak256raw(B), BE, Unsigned)
Expand All @@ -257,6 +287,18 @@ module ULM-TEST-EXECUTION
GetAccountStorageHook(Key)
Result
rule Log3Hook(evaluatedEventSignature(I:Int), A:Int, C:Int, encodedValues(B2:Bytes))
=> #Log3Hook
( I
, A
, C
, B2
)
rule list_mock #Log3Hook(V1:Int, V2:Int, V3:Int, B:Bytes) Result:UlmHookResult
=> list_mock
Log3Hook(V1, V2, V3, B)
Result
// This may seem stupid, but it's a workaround for
// https://github.com/runtimeverification/k/issues/4683
rule isKResult(X) => true requires isTestResult(X)
Expand Down

0 comments on commit 212be93

Please sign in to comment.