diff --git a/src/expression.md b/src/expression.md index 8c300e6..50184ea 100644 --- a/src/expression.md +++ b/src/expression.md @@ -13,7 +13,7 @@ module SOLIDITY-EXPRESSION THIS => ADDR TYPE => X E => .Map - S => .Map + S => .List ... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) X INIT @@ -38,7 +38,7 @@ module SOLIDITY-EXPRESSION THIS => ADDR TYPE => X E => .Map - S => .Map + S => .List ... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) X INIT @@ -53,10 +53,10 @@ 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)) ] + rule new T[](Len:Int) => lv(size(S), .List, T[]) ... + S => S ListItem(makeList(Len, default(T))) + rule new T[](v(Len:MInt{256}, _)) => lv(size(S), .List, T[]) ... + S => S ListItem(makeList(MInt2Unsigned(Len), default(T))) // literal assignment to state variable rule X:Id = N:Int => X = v(convert(N, LT), LT) ... @@ -139,7 +139,7 @@ module SOLIDITY-EXPRESSION // local variable lookup rule X:Id => v(V, T) ... ... X |-> var(I, T) ... - ... I |-> V ... + _ [ I <- V ] requires notBool isAggregateType(T) rule X:Id => lv(I, .List, T) ... @@ -150,10 +150,10 @@ module SOLIDITY-EXPRESSION 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 ... + _ [ 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 ... + _ [ 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 @@ -180,7 +180,7 @@ module SOLIDITY-EXPRESSION 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 ... + _ [ I <- V ] // external call context HOLE . _ ( _:CallArgumentList ) @@ -191,7 +191,7 @@ module SOLIDITY-EXPRESSION THIS => ADDR TYPE => TYPE' E => .Map - S => .Map + S => .List ... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) TYPE' F @@ -216,7 +216,7 @@ module SOLIDITY-EXPRESSION THIS => ADDR TYPE => TYPE' E => .Map - S => .Map + S => .List ... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) TYPE' F @@ -310,10 +310,10 @@ module SOLIDITY-EXPRESSION // local increment and decrement rule X:Id ++ => v(V, T) ... ... X |-> var(I, T) ... - ... I |-> (V => add(V, convert(1, T))) ... + _ [ I <- (V => add(V, convert(1, T))) ] rule X:Id -- => v(V, T) ... ... X |-> var(I, T) ... - ... I |-> (V => sub(V, convert(1, T))) ... + _ [ I <- (V => sub(V, convert(1, T))) ] // equality and inequality rule v(V1:Value, T) == v(V2:Value, T) => v(eq(V1, V2), bool) @@ -384,19 +384,19 @@ module SOLIDITY-EXPRESSION syntax KItem ::= var(Int, TypeName) - syntax KItem ::= bind(Map, List, List, CallArgumentList, List, List) + syntax KItem ::= bind(List, 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 ] ] + E => E [ X <- var(size(S), T) ] + S => S ListItem(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) ] + E => E [ X <- var(size(S), LT) ] + S => S ListItem(convert(V, RT, LT)) 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) ] + E => E [ X <- var(size(S), LT) ] + S => S ListItem(default(LT)) syntax Value ::= convert(Value, from: TypeName, to: TypeName) [function] rule convert(V, T, T) => V diff --git a/src/solidity.md b/src/solidity.md index b156896..3ff9b8e 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -67,7 +67,7 @@ module SOLIDITY-CONFIGURATION 0p160 Id .Map - .Map + .List .List @@ -163,7 +163,7 @@ module SOLIDITY-DATA rule isAggregateType(_) => false [owise] // external frame - syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256}) + syntax Frame ::= frame(continuation: K, env: Map, store: List, from: MInt{160}, type: Id, value: MInt{256}) // internal frame | frame(continuation: K, env: Map) syntax Event ::= event(name: Id, args: TypedVals) diff --git a/src/statement.md b/src/statement.md index 18ae130..51c11d5 100644 --- a/src/statement.md +++ b/src/statement.md @@ -29,7 +29,7 @@ module SOLIDITY-STATEMENT ... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List rule return lv(I:Int, .List, T) ; => return v(L, T) ; ... - ... I |-> L ... + _ [ I <- L ] rule return V:TypedVal ; ~> _ => V ~> K _ => E @@ -37,19 +37,19 @@ module SOLIDITY-STATEMENT // variable declaration rule LT:TypeName X:Id = v(V, RT) ; => .K ... - E => E [ X <- var(!I:Int, LT) ] - S => S [ !I <- convert(V, RT, LT) ] + E => E [ X <- var(size(S), LT) ] + S => S ListItem(convert(V, RT, LT)) rule LT:TypeName X:Id = N:Int ; => .K ... - E => E [ X <- var(!I:Int, LT) ] - S => S [ !I <- convert(N, LT) ] + E => E [ X <- var(size(S), LT) ] + S => S ListItem(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) ] + E => E [ X <- var(size(S), LT) ] + S => S ListItem(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) ] + E => E [ X <- var(size(S), T) ] + S => S ListItem(default(T)) // emit statement rule emit X:Id ( ARGS ) ; => .K ... diff --git a/src/transaction.md b/src/transaction.md index 1e8521d..44202f9 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(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ... + rule create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ... _ => Int2MInt(Number2Int(FROM)) _ => Int2MInt(Number2Int(VALUE)) _ => Int2MInt(Number2Int(FROM)) @@ -15,7 +15,7 @@ module SOLIDITY-TRANSACTION _ => ADDR _ => CTOR _ => .Map - _ => .Map + _ => .List CTOR INIT constructor @@ -41,7 +41,7 @@ module SOLIDITY-TRANSACTION _ => ADDR _ => CTOR _ => .Map - _ => .Map + _ => .List CTOR INIT @@ -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(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ... + rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ... _ => Int2MInt(Number2Int(FROM)) _ => Int2MInt(Number2Int(VALUE)) _ => Int2MInt(Number2Int(FROM)) @@ -66,7 +66,7 @@ module SOLIDITY-TRANSACTION _ => TO _ => TYPE _ => .Map - _ => .Map + _ => .List TO TYPE