diff --git a/src/expression.md b/src/expression.md index b8165da..e4ba232 100644 --- a/src/expression.md +++ b/src/expression.md @@ -81,13 +81,13 @@ module SOLIDITY-EXPRESSION TYPE // state variable lookup - rule X:Id => v(V, T) ... + rule X:Id => v({S[X] orDefault default(T)}:>Value, T) ... THIS TYPE TYPE - ... X |-> T + ... X |-> T ... THIS - ... X |-> V ... + S // local variable lookup rule X:Id => v(V, T) ... @@ -131,6 +131,9 @@ module SOLIDITY-EXPRESSION 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) @@ -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 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) ... E => E [ X <- var(!I:Int, LT) ] S => S [ !I <- convert(V, RT, LT) ] @@ -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 ]] + X + rule [[ default(X:Id) => 0p160 ]] + X + 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 diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md index a105bcc..c4eaf5d 100644 --- a/src/solidity-syntax.md +++ b/src/solidity-syntax.md @@ -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 diff --git a/src/solidity.md b/src/solidity.md index e4b316e..8e9bf02 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -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} @@ -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