diff --git a/src/contract.md b/src/contract.md index 6ca8298..c4fc5b8 100644 --- a/src/contract.md +++ b/src/contract.md @@ -79,14 +79,36 @@ module SOLIDITY-CONTRACT .Bag => X public + accessorTypes(T) + accessorNames(T, 0) ListItem(T) ListItem(noId) - return X ; + return accessor(X, T, 0) ; ... ... + syntax List ::= accessorTypes(TypeName) [function] + rule accessorTypes(_:ElementaryTypeName) => .List + rule accessorTypes(_:Id) => .List + rule accessorTypes(mapping(T1 _ => T2 _)) => ListItem(T1) accessorTypes(T2) + rule accessorTypes(T []) => ListItem(T) + + syntax List ::= accessorNames(TypeName, Int) [function] + rule accessorNames(_:ElementaryTypeName, _) => .List + rule accessorNames(_:Id, _) => .List + rule accessorNames(mapping(_ X:Id => T2 _), I) => ListItem(X) accessorNames(T2, I) + rule accessorNames(mapping(_ => T2 _), I) => ListItem(String2Id("$" +String Int2String(I))) accessorNames(T2, I +Int 1) + rule accessorNames(T [], I) => ListItem(String2Id("$" +String Int2String(I))) accessorNames(T, I +Int 1) + + syntax Expression ::= accessor(Expression, TypeName, Int) [function] + rule accessor(X, _:ElementaryTypeName, _) => X + rule accessor(X, _:Id, _) => X + rule accessor(X, mapping(_ Y:Id => T2 _), I) => accessor(X [ Y ], T2, I) + rule accessor(X, mapping(_ => T2 _), I) => accessor(X [ String2Id("$" +String Int2String(I)) ], T2, I +Int 1) + rule accessor(X, T [], I) => accessor(X [ String2Id("$" +String Int2String(I)) ], T, I +Int 1) + rule T:TypeName private X:Id ; => .K ... C C @@ -101,9 +123,11 @@ module SOLIDITY-CONTRACT .Bag => X public + accessorTypes(T) + accessorNames(T, 0) ListItem(T) ListItem(noId) - return X ; + return accessor(X, T, 0) ; ... ... diff --git a/src/expression.md b/src/expression.md index 327d941..fceeac9 100644 --- a/src/expression.md +++ b/src/expression.md @@ -7,7 +7,7 @@ module SOLIDITY-EXPRESSION imports INT // new contract - rule new X:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; + rule new X:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; FROM => THIS VALUE => 0p256 THIS => ADDR @@ -52,6 +52,12 @@ module SOLIDITY-EXPRESSION ADDR => ADDR +MInt 1p160 + // new array + rule new T[](Len:Int) => lv(!I:Int, .List, T[]) ... + S => S [ !I:Int <- makeList(Len, default(T)) ] + rule new T[](v(Len:MInt{256}, _)) => lv(!I:Int, .List, T[]) ... + S => S [ !I:Int <- makeList(MInt2Unsigned(Len), default(T)) ] + // literal assignment to state variable rule X:Id = N:Int => X = v(convert(N, LT), LT) ... TYPE @@ -76,6 +82,30 @@ module SOLIDITY-EXPRESSION ... X |-> var(I, LT) ... S => S [ I <- convert(V, RT, LT) ] + // reference assignment to local + rule X:Id = lv(I:Int, .List, T) => lv(I:Int, .List, T) ... + ... X |-> var(_ => I, T) ... + + // assignment to array element + context HOLE [ _ ] = _ + context _ [ HOLE ] = _ + rule lv(I:Int, L, LT []) [ Idx:Int ] = v(V, RT) => v(convert(V, RT, LT), LT) ... + S => S [ I <- write({S [ I ]}:>Value, L ListItem(Idx), convert(V, RT, LT), LT[]) ] + rule lv(I:Int, L, LT []) [ v(Idx:MInt{256}, _) ] = v(V, RT) => v(convert(V, RT, LT), LT) ... + S => S [ I <- write({S [ I ]}:>Value, L ListItem(MInt2Unsigned(Idx)), convert(V, RT, LT), LT[]) ] + rule lv(X:Id, L, mapping(LT1:ElementaryTypeName _ => T2)) [ v(Key, RT1) ] = v(V, RT) => v(convert(V, RT, T2), T2) ... + THIS + TYPE + TYPE + ... X |-> T ... + THIS + S => S [ X <- write({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT1, LT1)), convert(V, RT, T2), T) ] + + syntax Value ::= write(Value, List, Value, TypeName) [function] + rule write(_, .List, V, _) => V + rule write(L1:List, ListItem(I:Int) L2, V, T[]) => L1 [ I <- write({L1 [ I ]}:>Value, L2, V, T) ] + rule write(M:Map, ListItem(Key:Value) L2, V, mapping(_ _ => T2)) => M [ Key <- write({M [ Key ] orDefault default(T2)}:>Value, L2, V, T2) ] + // type conversion context _:ElementaryTypeName ( HOLE:CallArgumentList ) context _:Id ( HOLE:CallArgumentList ) @@ -98,16 +128,64 @@ module SOLIDITY-EXPRESSION ... X |-> T ... THIS S + requires notBool isAggregateType(T) + + rule X:Id => lv(X, .List, T) ... + TYPE + TYPE + ... X |-> T ... + requires isAggregateType(T) // local variable lookup rule X:Id => v(V, T) ... ... X |-> var(I, T) ... ... I |-> V ... + requires notBool isAggregateType(T) + + rule X:Id => lv(I, .List, T) ... + ... X |-> var(I, T) ... + requires isAggregateType(T) + + // array element lookup + context HOLE:Expression [ _:Expression ] + context _:Expression [ HOLE:Expression ] + rule lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ... + ... I |-> V ... + requires notBool isAggregateType(T) + rule lv(I:Int, L, T []) [ v(Idx:MInt{256}, _) ] => v(read(V, L ListItem(MInt2Unsigned(Idx)), T[]), T) ... + ... I |-> V ... + requires notBool isAggregateType(T) + rule lv(X:Id, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(Key, RT) ] => v(read({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT, T1)), T), T2) ... + THIS + TYPE + TYPE + ... X |-> T ... + THIS + S + requires notBool isAggregateType(T2) + + rule lv(R, L, T []) [ Idx:Int ] => lv(R, L ListItem(Idx), T) ... + requires isAggregateType(T) + rule lv(R, L, T []) [ v(Idx:MInt{256}, _) ] => lv(R, L ListItem(MInt2Unsigned(Idx)), T) ... + requires isAggregateType(T) + rule lv(R, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(V, RT) ] => lv(R, L ListItem(convert(V, RT, T1)), T2) ... + requires isAggregateType(T2) + + syntax Value ::= read(Value, List, TypeName) [function] + rule read(V, .List, _) => V + rule read(L1:List, ListItem(I:Int) L2, T[]) => read({L1 [ I ]}:>Value, L2, T) + rule read(M:Map, ListItem(V:Value) L, mapping(_ _ => T)) => read({M [ V ] orDefault default(T)}:>Value, L, T) + + // array length + syntax Id ::= "length" [token] + context HOLE . length + rule lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ... + ... I |-> V ... // external call context HOLE . _ ( _:CallArgumentList ) context (_ . _) ( HOLE:CallArgumentList ) - rule v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); + rule v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); FROM => THIS VALUE => 0p256 THIS => ADDR @@ -132,7 +210,7 @@ module SOLIDITY-EXPRESSION context _ . _ { value: HOLE } ( _ ) context _ . _ { _ } ( HOLE:CallArgumentList ) - rule v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); + rule v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); FROM => THIS VALUE => VALUE' THIS => ADDR @@ -153,14 +231,10 @@ module SOLIDITY-EXPRESSION requires isKResult(ARGS) andBool (PAYABLE orBool VALUE' ==MInt 0p256) // internal call - rule F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); - FROM - VALUE - TYPE + rule F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); E => .Map - S => .Map - ... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) - TYPE + S + ... .List => ListItem(frame(K, E)) F PARAMS TYPES @@ -307,14 +381,17 @@ module SOLIDITY-EXPRESSION syntax KItem ::= var(Int, TypeName) - 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) ... + syntax KItem ::= bind(Map, List, List, CallArgumentList, List, List) + rule bind(_, .List, .List, .CallArgumentList, .List, .List) => .K + rule bind(STORE, ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) + rule bind(STORE, .List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) + rule bind(STORE, ListItem(X:Id) PARAMS, ListItem(T:TypeName) TYPES, lv(I:Int, .List, T:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ... + E => E [ X <- var(!I:Int, T) ] + S => S [ !I <- STORE [ I ] ] + rule bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ... E => E [ X <- var(!I:Int, LT) ] S => S [ !I <- convert(V, RT, LT) ] - rule bind(.List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(.List, .List, .CallArgumentList, TYPES, NAMES) ... + rule bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ... E => E [ X <- var(!I:Int, LT) ] S => S [ !I <- default(LT) ] @@ -423,6 +500,8 @@ module SOLIDITY-EXPRESSION rule [[ default(X:Id) => 0p160 ]] X rule default(uint256) => 0p256 + rule default(_ []) => .List + rule default(mapping(_ _ => _ _)) => .Map syntax Expression ::= retval(List) [function] rule retval(.List) => void diff --git a/src/solidity.md b/src/solidity.md index 9aada5a..2df8c63 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -113,17 +113,13 @@ module SOLIDITY-DATA syntax KItem ::= "noId" syntax Id ::= "constructor" [token] - syntax TypedVal ::= v(Value, TypeName) | Int | String | "void" + syntax TypedVal ::= v(Value, TypeName) | lv(BaseRef, List, TypeName) | Int | String | "void" syntax TypedVals ::= List{TypedVal, ","} [overload(exps), hybrid, strict] syntax Expression ::= TypedVal syntax CallArgumentList ::= TypedVals syntax KResult ::= TypedVal - syntax Value ::= MInt{8} | MInt{32} | MInt{112} | MInt{160} | MInt{256} | Bool | String - syntax Reference ::= stateVarRef(Id) - | localVarRef(Int) - | mappingValueRef(Reference, Value) - | arrayElementRef(Reference, Value) - syntax Value ::= Reference + syntax Value ::= MInt{8} | MInt{32} | MInt{112} | MInt{160} | MInt{256} | Bool | String | List | Map + syntax BaseRef ::= Id | Int syntax List ::= getTypes(ParameterList) [function] rule getTypes(.ParameterList) => .List @@ -159,7 +155,15 @@ module SOLIDITY-DATA 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] + syntax Bool ::= isAggregateType(TypeName) [function] + rule isAggregateType(_[]) => true + rule isAggregateType(mapping(_ _ => _ _)) => true + rule isAggregateType(_) => false [owise] + + // external frame syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256}) + // internal frame + | frame(continuation: K, env: Map) syntax Event ::= event(name: Id, args: TypedVals) endmodule diff --git a/src/statement.md b/src/statement.md index c31fec5..18ae130 100644 --- a/src/statement.md +++ b/src/statement.md @@ -10,7 +10,7 @@ module SOLIDITY-STATEMENT rule _:TypedVal ; => .K // return statement - rule return V:TypedVal ; ~> _ => V ~> K + rule return v(V, T) ; ~> _ => v(V, T) ~> K THIS => FROM _ => VALUE _ => THIS @@ -19,6 +19,22 @@ module SOLIDITY-STATEMENT _ => S ... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List + rule return void ; ~> _ => void ~> K + THIS => FROM + _ => VALUE + _ => THIS + _ => TYPE + _ => E + _ => S + ... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List + + rule return lv(I:Int, .List, T) ; => return v(L, T) ; ... + ... I |-> L ... + + rule return V:TypedVal ; ~> _ => V ~> K + _ => E + ... ListItem(frame(K, E)) => .List + // variable declaration rule LT:TypeName X:Id = v(V, RT) ; => .K ... E => E [ X <- var(!I:Int, LT) ] @@ -26,6 +42,14 @@ module SOLIDITY-STATEMENT rule LT:TypeName X:Id = N:Int ; => .K ... E => E [ X <- var(!I:Int, LT) ] S => S [ !I <- convert(N, LT) ] + rule LT:TypeName memory X:Id = v(V, RT) ; => .K ... + E => E [ X <- var(!I:Int, LT) ] + S => S [ !I <- convert(V, RT, LT) ] + rule T:TypeName memory X:Id = lv(I:Int, .List, T) ; => .K ... + E => E [ X <- var(I, T) ] + rule T:TypeName X:Id ;::VariableDeclarationStatement => .K ... + E => E [ X <- var(!I:Int, T) ] + S => S [ !I <- default(T) ] // emit statement rule emit X:Id ( ARGS ) ; => .K ... diff --git a/src/transaction.md b/src/transaction.md index 1d0d8b0..1e8521d 100644 --- a/src/transaction.md +++ b/src/transaction.md @@ -7,7 +7,7 @@ module SOLIDITY-TRANSACTION imports INT imports private SOLIDITY-EXPRESSION - rule create(FROM, VALUE, NOW, CTOR, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ... + rule create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ... _ => Int2MInt(Number2Int(FROM)) _ => Int2MInt(Number2Int(VALUE)) _ => Int2MInt(Number2Int(FROM)) @@ -58,7 +58,7 @@ module SOLIDITY-TRANSACTION syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)] rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS) - rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> BODY ... + rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ... _ => Int2MInt(Number2Int(FROM)) _ => Int2MInt(Number2Int(VALUE)) _ => Int2MInt(Number2Int(FROM)) diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref index 7b671fa..ca67ee8 100644 --- a/test/regression/arraystestcontract.ref +++ b/test/regression/arraystestcontract.ref @@ -29,10 +29,10 @@ public - .List + ListItem ( uint256 ) - .List + ListItem ( $0 ) ListItem ( uint256 [ ] ) @@ -44,7 +44,7 @@ false - return arr ; .Statements + return arr [ $0 ] ; .Statements diff --git a/test/regression/function.ref b/test/regression/function.ref index ad34ab9..7b63acf 100644 --- a/test/regression/function.ref +++ b/test/regression/function.ref @@ -81,10 +81,12 @@ public - .List + ListItem ( address ) + ListItem ( address ) - .List + ListItem ( $0 ) + ListItem ( $1 ) ListItem ( mapping ( address => mapping ( address => uint256 ) ) ) @@ -96,7 +98,7 @@ false - return allowance ; .Statements + return allowance [ $0 ] [ $1 ] ; .Statements @@ -133,10 +135,10 @@ public - .List + ListItem ( address ) - .List + ListItem ( $0 ) ListItem ( mapping ( address => uint256 ) ) @@ -148,7 +150,7 @@ false - return balanceOf ; .Statements + return balanceOf [ $0 ] ; .Statements @@ -779,10 +781,10 @@ public - .List + ListItem ( address ) - .List + ListItem ( $0 ) ListItem ( mapping ( address => uint256 ) ) @@ -794,7 +796,7 @@ false - return balanceOf ; .Statements + return balanceOf [ $0 ] ; .Statements @@ -1132,10 +1134,12 @@ public - .List + ListItem ( address ) + ListItem ( address ) - .List + ListItem ( $0 ) + ListItem ( $1 ) ListItem ( mapping ( address => mapping ( address => address ) ) ) @@ -1147,7 +1151,7 @@ false - return local_pairs ; .Statements + return local_pairs [ $0 ] [ $1 ] ; .Statements @@ -1883,10 +1887,12 @@ public - .List + ListItem ( address ) + ListItem ( address ) - .List + ListItem ( $0 ) + ListItem ( $1 ) ListItem ( mapping ( address => mapping ( address => uint256 ) ) ) @@ -1898,7 +1904,7 @@ false - return allowance ; .Statements + return allowance [ $0 ] [ $1 ] ; .Statements @@ -1935,10 +1941,10 @@ public - .List + ListItem ( address ) - .List + ListItem ( $0 ) ListItem ( mapping ( address => uint256 ) ) @@ -1950,7 +1956,7 @@ false - return balanceOf ; .Statements + return balanceOf [ $0 ] ; .Statements diff --git a/test/regression/mapstestcontract.ref b/test/regression/mapstestcontract.ref index b4809ac..2b5c787 100644 --- a/test/regression/mapstestcontract.ref +++ b/test/regression/mapstestcontract.ref @@ -55,10 +55,10 @@ public - .List + ListItem ( address ) - .List + ListItem ( $0 ) ListItem ( mapping ( address => uint256 ) ) @@ -70,7 +70,7 @@ false - return testMap ; .Statements + return testMap [ $0 ] ; .Statements @@ -80,10 +80,10 @@ public - .List + ListItem ( address ) - .List + ListItem ( key ) ListItem ( mapping ( address key => uint256 val ) ) @@ -95,7 +95,7 @@ false - return testMapWithOptIds ; .Statements + return testMapWithOptIds [ key ] ; .Statements