Skip to content

Commit

Permalink
Merge branch 'main' into contract
Browse files Browse the repository at this point in the history
  • Loading branch information
@dwightguth
dwightguth authored Sep 4, 2024
2 parents 5752476 + 30b1339 commit d49aab8
Show file tree
Hide file tree
Showing 8 changed files with 192 additions and 55 deletions.
28 changes: 26 additions & 2 deletions src/contract.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,14 +79,36 @@ module SOLIDITY-CONTRACT
.Bag => <contract-fn>
<contract-fn-id> X </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<contract-fn-arg-types> accessorTypes(T) </contract-fn-arg-types>
<contract-fn-param-names> accessorNames(T, 0) </contract-fn-param-names>
<contract-fn-return-types> ListItem(T) </contract-fn-return-types>
<contract-fn-return-names> ListItem(noId) </contract-fn-return-names>
<contract-fn-body> return X ; </contract-fn-body>
<contract-fn-body> return accessor(X, T, 0) ; </contract-fn-body>
...
</contract-fn>
...
</contract-fns>
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 <k> T:TypeName private X:Id ; => .K ...</k>
<current-body> C </current-body>
<contract-id> C </contract-id>
Expand All @@ -101,9 +123,11 @@ module SOLIDITY-CONTRACT
.Bag => <contract-fn>
<contract-fn-id> X </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<contract-fn-arg-types> accessorTypes(T) </contract-fn-arg-types>
<contract-fn-param-names> accessorNames(T, 0) </contract-fn-param-names>
<contract-fn-return-types> ListItem(T) </contract-fn-return-types>
<contract-fn-return-names> ListItem(noId) </contract-fn-return-names>
<contract-fn-body> return X ; </contract-fn-body>
<contract-fn-body> return accessor(X, T, 0) ; </contract-fn-body>
...
</contract-fn>
...
Expand Down
111 changes: 95 additions & 16 deletions src/expression.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module SOLIDITY-EXPRESSION
imports INT
// new contract
rule <k> new X:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; </k>
rule <k> new X:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; </k>
<msg-sender> FROM => THIS </msg-sender>
<msg-value> VALUE => 0p256 </msg-value>
<this> THIS => ADDR </this>
Expand Down Expand Up @@ -52,6 +52,12 @@ module SOLIDITY-EXPRESSION
</live-contracts>
<next-address> ADDR => ADDR +MInt 1p160 </next-address>
// new array
rule <k> new T[](Len:Int) => lv(!I:Int, .List, T[]) ...</k>
<store> S => S [ !I:Int <- makeList(Len, default(T)) ] </store>
rule <k> new T[](v(Len:MInt{256}, _)) => lv(!I:Int, .List, T[]) ...</k>
<store> S => S [ !I:Int <- makeList(MInt2Unsigned(Len), default(T)) ] </store>
// literal assignment to state variable
rule <k> X:Id = N:Int => X = v(convert(N, LT), LT) ...</k>
<this-type> TYPE </this-type>
Expand All @@ -76,6 +82,30 @@ module SOLIDITY-EXPRESSION
<env>... X |-> var(I, LT) ...</env>
<store> S => S [ I <- convert(V, RT, LT) ] </store>
// reference assignment to local
rule <k> X:Id = lv(I:Int, .List, T) => lv(I:Int, .List, T) ...</k>
<env>... X |-> var(_ => I, T) ...</env>
// assignment to array element
context HOLE [ _ ] = _
context _ [ HOLE ] = _
rule <k> lv(I:Int, L, LT []) [ Idx:Int ] = v(V, RT) => v(convert(V, RT, LT), LT) ...</k>
<store> S => S [ I <- write({S [ I ]}:>Value, L ListItem(Idx), convert(V, RT, LT), LT[]) ] </store>
rule <k> lv(I:Int, L, LT []) [ v(Idx:MInt{256}, _) ] = v(V, RT) => v(convert(V, RT, LT), LT) ...</k>
<store> S => S [ I <- write({S [ I ]}:>Value, L ListItem(MInt2Unsigned(Idx)), convert(V, RT, LT), LT[]) ] </store>
rule <k> lv(X:Id, L, mapping(LT1:ElementaryTypeName _ => T2)) [ v(Key, RT1) ] = v(V, RT) => v(convert(V, RT, T2), T2) ...</k>
<this> THIS </this>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> T ...</contract-state>
<contract-address> THIS </contract-address>
<contract-storage> S => S [ X <- write({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT1, LT1)), convert(V, RT, T2), T) ] </contract-storage>
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 )
Expand All @@ -98,16 +128,64 @@ module SOLIDITY-EXPRESSION
<contract-state>... X |-> T ...</contract-state>
<contract-address> THIS </contract-address>
<contract-storage> S </contract-storage>
requires notBool isAggregateType(T)
rule <k> X:Id => lv(X, .List, T) ...</k>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> T ...</contract-state>
requires isAggregateType(T)
// local variable lookup
rule <k> X:Id => v(V, T) ...</k>
<env>... X |-> var(I, T) ...</env>
<store>... I |-> V ...</store>
requires notBool isAggregateType(T)
rule <k> X:Id => lv(I, .List, T) ...</k>
<env>... X |-> var(I, T) ...</env>
requires isAggregateType(T)
// array element lookup
context HOLE:Expression [ _:Expression ]
context _:Expression [ HOLE:Expression ]
rule <k> lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ...</k>
<store>... I |-> V ...</store>
requires notBool isAggregateType(T)
rule <k> lv(I:Int, L, T []) [ v(Idx:MInt{256}, _) ] => v(read(V, L ListItem(MInt2Unsigned(Idx)), T[]), T) ...</k>
<store>... I |-> V ...</store>
requires notBool isAggregateType(T)
rule <k> 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) ...</k>
<this> THIS </this>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> T ...</contract-state>
<contract-address> THIS </contract-address>
<contract-storage> S </contract-storage>
requires notBool isAggregateType(T2)
rule <k> lv(R, L, T []) [ Idx:Int ] => lv(R, L ListItem(Idx), T) ...</k>
requires isAggregateType(T)
rule <k> lv(R, L, T []) [ v(Idx:MInt{256}, _) ] => lv(R, L ListItem(MInt2Unsigned(Idx)), T) ...</k>
requires isAggregateType(T)
rule <k> lv(R, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(V, RT) ] => lv(R, L ListItem(convert(V, RT, T1)), T2) ...</k>
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 <k> lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ...</k>
<store>... I |-> V ...</store>
// external call
context HOLE . _ ( _:CallArgumentList )
context (_ . _) ( HOLE:CallArgumentList )
rule <k> v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
rule <k> v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<msg-sender> FROM => THIS </msg-sender>
<msg-value> VALUE => 0p256 </msg-value>
<this> THIS => ADDR </this>
Expand All @@ -132,7 +210,7 @@ module SOLIDITY-EXPRESSION
context _ . _ { value: HOLE } ( _ )
context _ . _ { _ } ( HOLE:CallArgumentList )
rule <k> v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
rule <k> v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<msg-sender> FROM => THIS </msg-sender>
<msg-value> VALUE => VALUE' </msg-value>
<this> THIS => ADDR </this>
Expand All @@ -153,14 +231,10 @@ module SOLIDITY-EXPRESSION
requires isKResult(ARGS) andBool (PAYABLE orBool VALUE' ==MInt 0p256)
// internal call
rule <k> F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<msg-sender> FROM </msg-sender>
<msg-value> VALUE </msg-value>
<this-type> TYPE </this-type>
rule <k> F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<env> E => .Map </env>
<store> S => .Map </store>
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
<contract-id> TYPE </contract-id>
<store> S </store>
<call-stack>... .List => ListItem(frame(K, E)) </call-stack>
<contract-fn-id> F </contract-fn-id>
<contract-fn-param-names> PARAMS </contract-fn-param-names>
<contract-fn-arg-types> TYPES </contract-fn-arg-types>
Expand Down Expand Up @@ -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 <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>
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 <k> 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) ...</k>
<env> E => E [ X <- var(!I:Int, T) ] </env>
<store> S => S [ !I <- STORE [ I ] ] </store>
rule <k> 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) ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
rule <k> bind(.List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(.List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
rule <k> bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- default(LT) ] </store>
Expand Down Expand Up @@ -423,6 +500,8 @@ module SOLIDITY-EXPRESSION
rule [[ default(X:Id) => 0p160 ]]
<iface-id> X </iface-id>
rule default(uint256) => 0p256
rule default(_ []) => .List
rule default(mapping(_ _ => _ _)) => .Map
syntax Expression ::= retval(List) [function]
rule retval(.List) => void
Expand Down
18 changes: 11 additions & 7 deletions src/solidity.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
26 changes: 25 additions & 1 deletion src/statement.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module SOLIDITY-STATEMENT
rule _:TypedVal ; => .K
// return statement
rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
rule <k> return v(V, T) ; ~> _ => v(V, T) ~> K </k>
<msg-sender> THIS => FROM </msg-sender>
<msg-value> _ => VALUE </msg-value>
<this> _ => THIS </this>
Expand All @@ -19,13 +19,37 @@ module SOLIDITY-STATEMENT
<store> _ => S </store>
<call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
rule <k> return void ; ~> _ => void ~> K </k>
<msg-sender> THIS => FROM </msg-sender>
<msg-value> _ => VALUE </msg-value>
<this> _ => THIS </this>
<this-type> _ => TYPE </this-type>
<env> _ => E </env>
<store> _ => S </store>
<call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
<store>... I |-> L ...</store>
rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
<env> _ => E </env>
<call-stack>... ListItem(frame(K, E)) => .List </call-stack>
// variable declaration
rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
rule <k> LT:TypeName X:Id = N:Int ; => .K ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- convert(N, LT) ] </store>
rule <k> LT:TypeName memory X:Id = v(V, RT) ; => .K ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
rule <k> T:TypeName memory X:Id = lv(I:Int, .List, T) ; => .K ...</k>
<env> E => E [ X <- var(I, T) ] </env>
rule <k> T:TypeName X:Id ;::VariableDeclarationStatement => .K ...</k>
<env> E => E [ X <- var(!I:Int, T) ] </env>
<store> S => S [ !I <- default(T) ] </store>
// emit statement
rule <k> emit X:Id ( ARGS ) ; => .K ...</k>
Expand Down
4 changes: 2 additions & 2 deletions src/transaction.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module SOLIDITY-TRANSACTION
imports INT
imports private SOLIDITY-EXPRESSION
rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
<msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
<msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
<tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
Expand Down Expand Up @@ -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 <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
<msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
<msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
<tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
Expand Down
6 changes: 3 additions & 3 deletions test/regression/arraystestcontract.ref
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,10 @@
public
</contract-fn-visibility>
<contract-fn-arg-types>
.List
ListItem ( uint256 )
</contract-fn-arg-types>
<contract-fn-param-names>
.List
ListItem ( $0 )
</contract-fn-param-names>
<contract-fn-return-types>
ListItem ( uint256 [ ] )
Expand All @@ -44,7 +44,7 @@
false
</contract-fn-payable>
<contract-fn-body>
return arr ; .Statements
return arr [ $0 ] ; .Statements
</contract-fn-body>
</contract-fn> <contract-fn>
<contract-fn-id>
Expand Down
Loading

0 comments on commit d49aab8

Please sign in to comment.