A few miscellaneous changes (#14)

* bool literals

* fix state variable lookup

* fix return values with no name

* add missing integer types

src/expression.md

@@ -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>
@@ -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)
@@ -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>
@@ -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

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

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