diff --git a/src/contract.md b/src/contract.md index 54c4f91..d6c3181 100644 --- a/src/contract.md +++ b/src/contract.md @@ -98,5 +98,19 @@ module SOLIDITY-CONTRACT Env => Env [ X <- T ] ... .List => ListItem(X = E;) + rule event X ( EventParams ) ; => .K ... + C + C + + .Bag => + X + getTypes(EventParams) + getNames(EventParams) + getIndexed(EventParams) + ... + + ... + + endmodule ``` diff --git a/src/solidity.md b/src/solidity.md index 73723c8..6c3839c 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -44,6 +44,14 @@ module SOLIDITY-CONFIGURATION .Statements + + + Id + .List + .List + .Set + + @@ -81,11 +89,13 @@ module SOLIDITY-DATA-SYNTAX endmodule module SOLIDITY-DATA + imports INT imports MINT imports BOOL imports STRING imports ID imports LIST + imports SET imports SOLIDITY-DATA-SYNTAX syntax KItem ::= "noId" @@ -111,6 +121,26 @@ module SOLIDITY-DATA rule getNames(_:TypeName X:Id, Pp:ParameterList) => ListItem(X) getNames(Pp) rule getNames(_, Pp:ParameterList) => ListItem(noId) getNames(Pp) [owise] + syntax List ::= getTypes(EventParameters) [function] + rule getTypes(.EventParameters) => .List + rule getTypes(T:TypeName indexed _:Id, Ep:EventParameters) => ListItem(T) getTypes(Ep) + rule getTypes(T:TypeName _:Id, Ep:EventParameters) => ListItem(T) getTypes(Ep) + rule getTypes(T:TypeName indexed, Ep:EventParameters) => ListItem(T) getTypes(Ep) + rule getTypes(T:TypeName, Ep:EventParameters) => ListItem(T) getTypes(Ep) + + syntax List ::= getNames(EventParameters) [function] + rule getNames(.EventParameters) => .List + rule getNames(_:TypeName indexed X:Id, Ep:EventParameters) => ListItem(X) getNames(Ep) + rule getNames(_:TypeName X:Id, Ep:EventParameters) => ListItem(X) getNames(Ep) + rule getNames(_, Ep:EventParameters) => ListItem(noId) getNames(Ep) [owise] + + syntax Set ::= getIndexed(EventParameters) [function] + | getIndexed(EventParameters, Int) [function] + rule getIndexed(Ep:EventParameters) => getIndexed(Ep, 0) + rule getIndexed(.EventParameters, _:Int) => .Set + rule getIndexed(_:TypeName indexed _:Id, Ep:EventParameters, N:Int) => SetItem(N) getIndexed(Ep, N +Int 1) + rule getIndexed(_:TypeName indexed, Ep:EventParameters, N:Int) => SetItem(N) getIndexed(Ep, N +Int 1) + rule getIndexed(_, Ep:EventParameters, N:Int) => getIndexed(Ep, N +Int 1) [owise] endmodule ``` diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref index 61f4826..10526b0 100644 --- a/test/regression/arraystestcontract.ref +++ b/test/regression/arraystestcontract.ref @@ -61,6 +61,9 @@ + + .ContractEventCellMap + diff --git a/test/regression/contract.ref b/test/regression/contract.ref index ef72d4b..a79263c 100644 --- a/test/regression/contract.ref +++ b/test/regression/contract.ref @@ -259,6 +259,9 @@ + + .ContractEventCellMap + diff --git a/test/regression/eventtestcontract.ref b/test/regression/eventtestcontract.ref new file mode 100644 index 0000000..c29ea8d --- /dev/null +++ b/test/regression/eventtestcontract.ref @@ -0,0 +1,228 @@ + + + .K + + + TestEventsContract + + + .IfaceCellMap + + + + + TestEventsContract + + + .Map + + + .List + + + + + constructor + + + public + + + .List + + + .List + + + .List + + + .Statements + + + + + + + Event0 + + + ListItem ( uint256 ) + + + ListItem ( arg0 ) + + + .Set + + + + Event1 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( arg0 ) + ListItem ( arg1 ) + ListItem ( arg2 ) + + + .Set + + + + Event2 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( noId ) + ListItem ( noId ) + ListItem ( noId ) + + + .Set + + + + Event3 + + + ListItem ( address ) + + + ListItem ( idxarg0 ) + + + SetItem ( 0 ) + + + + Event4 + + + ListItem ( address ) + + + ListItem ( noId ) + + + SetItem ( 0 ) + + + + Event5 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( idxarg0 ) + ListItem ( idxarg1 ) + ListItem ( arg2 ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + Event6 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( idxarg0 ) + ListItem ( noId ) + ListItem ( arg2 ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + Event7 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( noId ) + ListItem ( idxarg1 ) + ListItem ( arg2 ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + Event8 + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( noId ) + ListItem ( noId ) + ListItem ( noId ) + + + SetItem ( 0 ) + SetItem ( 1 ) + SetItem ( 2 ) + + + + + + + + 1p160 + + + 0p256 + + + 1p160 + + + .Map + + + .Map + + + + + 2p160 + + + TestEventsContract + + + .Map + + + + + 3p160 + + + diff --git a/test/regression/eventtestcontract.sol b/test/regression/eventtestcontract.sol new file mode 100644 index 0000000..600342d --- /dev/null +++ b/test/regression/eventtestcontract.sol @@ -0,0 +1,18 @@ +pragma solidity ^0.8.24; + +contract TestEventsContract { + + event Event0(uint256 arg0); + event Event1(address arg0, address arg1, uint256 arg2); + event Event2(address, address, uint256); + + event Event3(address indexed idxarg0); + event Event4(address indexed); + event Event5(address indexed idxarg0, address indexed idxarg1, uint256 arg2); + event Event6(address indexed idxarg0, address indexed, uint256 arg2); + event Event7(address indexed, address indexed idxarg1, uint256 arg2); + event Event8(address indexed, address indexed, uint256 indexed); + + constructor() {} +} + diff --git a/test/regression/eventtestcontract.txn b/test/regression/eventtestcontract.txn new file mode 100644 index 0000000..3f14e18 --- /dev/null +++ b/test/regression/eventtestcontract.txn @@ -0,0 +1 @@ +create(1, 0, TestEventsContract, ) diff --git a/test/regression/mapstestcontract.ref b/test/regression/mapstestcontract.ref index e96272b..3e4ff44 100644 --- a/test/regression/mapstestcontract.ref +++ b/test/regression/mapstestcontract.ref @@ -81,6 +81,9 @@ + + .ContractEventCellMap +