Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Events definition handling #11

Merged
merged 5 commits into from
Aug 22, 2024
Merged

Events definition handling #11

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d9dac65
Events declaration handling.
mariaKt Aug 21, 2024
d228b9b
Modified contract.ref, to add (now expected) empty events cell.
mariaKt Aug 22, 2024
a04e8fd
Merge branch 'main' into events
dwightguth Aug 22, 2024
47bcb05
Updated reference files, adding empty events cell.
mariaKt Aug 22, 2024
365002a
Merge branch 'main' into events
mariaKt Aug 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions src/contract.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,5 +98,19 @@ module SOLIDITY-CONTRACT
<contract-state> Env => Env [ X <- T ] </contract-state>
<contract-init>... .List => ListItem(X = E;) </contract-init>

rule <k> event X ( EventParams ) ; => .K ...</k>
<current-body> C </current-body>
<contract-id> C </contract-id>
<contract-events>
.Bag => <contract-event>
<contract-event-id> X </contract-event-id>
<contract-event-arg-types> getTypes(EventParams) </contract-event-arg-types>
<contract-event-param-names> getNames(EventParams) </contract-event-param-names>
<contract-event-indexed-pos> getIndexed(EventParams) </contract-event-indexed-pos>
...
</contract-event>
...
</contract-events>

endmodule
```
30 changes: 30 additions & 0 deletions src/solidity.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,14 @@ module SOLIDITY-CONFIGURATION
<contract-fn-body> .Statements </contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
<contract-event multiplicity="*" type="Map">
<contract-event-id> Id </contract-event-id>
<contract-event-arg-types> .List </contract-event-arg-types>
<contract-event-param-names> .List </contract-event-param-names>
<contract-event-indexed-pos> .Set </contract-event-indexed-pos>
</contract-event>
</contract-events>
</contract>
</contracts>
<exec>
Expand Down Expand Up @@ -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"
Expand All @@ -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
```

Expand Down
3 changes: 3 additions & 0 deletions test/regression/arraystestcontract.ref
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,9 @@
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
.ContractEventCellMap
</contract-events>
</contract>
</contracts>
<exec>
Expand Down
3 changes: 3 additions & 0 deletions test/regression/contract.ref
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,9 @@
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
.ContractEventCellMap
</contract-events>
</contract>
</contracts>
<exec>
Expand Down
228 changes: 228 additions & 0 deletions test/regression/eventtestcontract.ref
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,228 @@
<solidity>
<k>
.K
</k>
<current-body>
TestEventsContract
</current-body>
<ifaces>
.IfaceCellMap
</ifaces>
<contracts>
<contract>
<contract-id>
TestEventsContract
</contract-id>
<contract-state>
.Map
</contract-state>
<contract-init>
.List
</contract-init>
<contract-fns>
<contract-fn>
<contract-fn-id>
constructor
</contract-fn-id>
<contract-fn-visibility>
public
</contract-fn-visibility>
<contract-fn-arg-types>
.List
</contract-fn-arg-types>
<contract-fn-param-names>
.List
</contract-fn-param-names>
<contract-fn-return-types>
.List
</contract-fn-return-types>
<contract-fn-body>
.Statements
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
<contract-event>
<contract-event-id>
Event0
</contract-event-id>
<contract-event-arg-types>
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( arg0 )
</contract-event-param-names>
<contract-event-indexed-pos>
.Set
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event1
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( arg0 )
ListItem ( arg1 )
ListItem ( arg2 )
</contract-event-param-names>
<contract-event-indexed-pos>
.Set
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event2
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( noId )
ListItem ( noId )
ListItem ( noId )
</contract-event-param-names>
<contract-event-indexed-pos>
.Set
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event3
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( idxarg0 )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event4
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( noId )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event5
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( idxarg0 )
ListItem ( idxarg1 )
ListItem ( arg2 )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
SetItem ( 1 )
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event6
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( idxarg0 )
ListItem ( noId )
ListItem ( arg2 )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
SetItem ( 1 )
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event7
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( noId )
ListItem ( idxarg1 )
ListItem ( arg2 )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
SetItem ( 1 )
</contract-event-indexed-pos>
</contract-event> <contract-event>
<contract-event-id>
Event8
</contract-event-id>
<contract-event-arg-types>
ListItem ( address )
ListItem ( address )
ListItem ( uint256 )
</contract-event-arg-types>
<contract-event-param-names>
ListItem ( noId )
ListItem ( noId )
ListItem ( noId )
</contract-event-param-names>
<contract-event-indexed-pos>
SetItem ( 0 )
SetItem ( 1 )
SetItem ( 2 )
</contract-event-indexed-pos>
</contract-event>
</contract-events>
</contract>
</contracts>
<exec>
<msg-sender>
1p160
</msg-sender>
<msg-value>
0p256
</msg-value>
<tx-origin>
1p160
</tx-origin>
<env>
.Map
</env>
<store>
.Map
</store>
<live-contracts>
<live-contract>
<contract-address>
2p160
</contract-address>
<contract-type>
TestEventsContract
</contract-type>
<contract-storage>
.Map
</contract-storage>
</live-contract>
</live-contracts>
<next-address>
3p160
</next-address>
</exec>
</solidity>
18 changes: 18 additions & 0 deletions test/regression/eventtestcontract.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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() {}
}

1 change: 1 addition & 0 deletions test/regression/eventtestcontract.txn
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
create(1, 0, TestEventsContract, )
3 changes: 3 additions & 0 deletions test/regression/mapstestcontract.ref
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,9 @@
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
.ContractEventCellMap
</contract-events>
</contract>
</contracts>
<exec>
Expand Down