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

A few miscellaneous changes #14

Merged
merged 4 commits into from
Aug 26, 2024
Merged

A few miscellaneous changes #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
34368e7
bool literals
dwightguth Aug 22, 2024
5aa48b4
fix state variable lookup
dwightguth Aug 22, 2024
f0ca224
fix return values with no name
dwightguth Aug 22, 2024
4c4b178
add missing integer types
dwightguth Aug 26, 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
19 changes: 16 additions & 3 deletions src/expression.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,13 +81,13 @@ module SOLIDITY-EXPRESSION
<iface-id> TYPE </iface-id>
// state variable lookup
rule <k> X:Id => v(V, T) ...</k>
rule <k> X:Id => v({S[X] orDefault default(T)}:>Value, T) ...</k>
<this> THIS </this>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> T </contract-state>
<contract-state>... X |-> T ...</contract-state>
<contract-address> THIS </contract-address>
<contract-storage>... X |-> V ...</contract-storage>
<contract-storage> S </contract-storage>
// local variable lookup
rule <k> X:Id => v(V, T) ...</k>
Expand Down Expand Up @@ -131,6 +131,9 @@ module SOLIDITY-EXPRESSION
<contract-fn-body> BODY </contract-fn-body>
requires isKResult(ARGS)
// boolean literal
rule B:Bool => v(B, bool)
// equality and inequality
rule v(V1:MInt{160}, _) == v(V2, _) => v(V1 ==MInt V2, bool)
rule v(V1:MInt{160}, _) != v(V2, _) => v(V1 =/=MInt V2, bool)
Expand Down Expand Up @@ -172,6 +175,7 @@ module SOLIDITY-EXPRESSION
syntax KItem ::= bind(List, List, CallArgumentList, List, List)
rule bind(.List, .List, .CallArgumentList, .List, .List) => .K
rule bind(ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(PARAMS, TYPES, ARGS, L1, L2)
rule bind(.List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(.List, .List, .CallArgumentList, TYPES, NAMES)
rule <k> bind(ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(PARAMS, TYPES, ARGS, L1, L2) ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
Expand All @@ -187,9 +191,18 @@ module SOLIDITY-EXPRESSION
rule convert(I:Int, uint256) => Int2MInt(I)::MInt{256}
syntax Value ::= default(TypeName) [function]
rule default(uint8) => 0p8
rule default(uint32) => 0p32
rule default(uint112) => 0p112
rule default(address) => 0p160
rule [[ default(X:Id) => 0p160 ]]
<contract-id> X </contract-id>
rule [[ default(X:Id) => 0p160 ]]
<iface-id> X </iface-id>
rule default(uint256) => 0p256
syntax Expression ::= retval(List) [function]
rule retval(.List) => void
rule retval(ListItem(noId)) => void
rule retval(ListItem(X:Id)) => X
endmodule
2 changes: 1 addition & 1 deletion src/solidity-syntax.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ We use tokens for the `pragma` definition in the header, hexadecimal numbers use
syntax HexNumber ::= r"0x[A-Fa-f0-9]+" [token]
syntax Decimal ::= r"(([0-9][_]?)+|([0-9][_]?)*[\\.]([0-9][_]?)+)([eE][\\-]?([0-9][_]?)+)?" [token]
syntax ElementaryTypeName ::= "uint" [function] | "uint112" | "uint256" | "address" | "bool"
syntax ElementaryTypeName ::= "uint" [function] | "uint8" | "uint32" | "uint112" | "uint256" | "address" | "bool"
syntax DataLocation ::= "memory" | "storage" | "calldata"
syntax SubDenom ::= "wei" | "gwei" | "ether" | "seconds" | "minutes" | "hours" | "days" | "weeks" | "years"
rule uint => uint256
Expand Down
4 changes: 3 additions & 1 deletion src/solidity.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,8 @@ module SOLIDITY-DATA-SYNTAX
imports STRING-SYNTAX
imports SOLIDITY-SYNTAX
syntax MInt{8}
syntax MInt{32}
syntax MInt{112}
syntax MInt{160}
syntax MInt{256}
Expand Down Expand Up @@ -113,7 +115,7 @@ module SOLIDITY-DATA
syntax Expression ::= TypedVal
syntax CallArgumentList ::= TypedVals
syntax KResult ::= TypedVal
syntax Value ::= MInt{112} | MInt{160} | MInt{256} | Bool | String
syntax Value ::= MInt{8} | MInt{32} | MInt{112} | MInt{160} | MInt{256} | Bool | String
syntax List ::= getTypes(ParameterList) [function]
rule getTypes(.ParameterList) => .List
Expand Down