Skip to content

Commit

Permalink
Basic function bodies (#12)
Browse files Browse the repository at this point in the history 
* add create txn with no constructor

* move a few functions to a different module

* fix parameter and return value binding

* uint == uint256

* add this and this-type cells

* add message call transactions

* add (some) strictness

* add some expressions

* add statement.md

* update test output

* add second test

* add uint112 type

* support declaration and initialization to literal

* update tests with merge conflicts

* update output files

* update k version
  • Loading branch information
@dwightguth
dwightguth authored Aug 26, 2024
1 parent 0f82ab3 commit 832eea9
Show file tree
Hide file tree
Showing 14 changed files with 2,963 additions and 47 deletions.
2 changes: 1 addition & 1 deletion deps/k_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
7.1.114
7.1.119
3 changes: 3 additions & 0 deletions src/contract.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ module SOLIDITY-CONTRACT
<contract-fn-arg-types> getTypes(Params) </contract-fn-arg-types>
<contract-fn-param-names> getNames(Params) </contract-fn-param-names>
<contract-fn-return-types> getTypes(Rets) </contract-fn-return-types>
<contract-fn-return-names> getNames(Rets) </contract-fn-return-names>
<contract-fn-body> Body </contract-fn-body>
...
</contract-fn>
Expand Down Expand Up @@ -65,6 +66,7 @@ module SOLIDITY-CONTRACT
<contract-fn-id> X </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<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>
Expand All @@ -86,6 +88,7 @@ module SOLIDITY-CONTRACT
<contract-fn-id> X </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<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>
Expand Down
170 changes: 169 additions & 1 deletion src/expression.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,148 @@ module SOLIDITY-EXPRESSION
imports SOLIDITY-CONFIGURATION
imports INT
// cast literal to address
// new contract
rule <k> new X:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; </k>
<msg-sender> FROM => THIS </msg-sender>
<this> THIS => ADDR </this>
<this-type> TYPE => X </this-type>
<env> E => .Map </env>
<store> S => .Map </store>
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
<contract-id> X </contract-id>
<contract-init> INIT </contract-init>
<contract-fn-id> constructor </contract-fn-id>
<contract-fn-param-names> PARAMS </contract-fn-param-names>
<contract-fn-arg-types> TYPES </contract-fn-arg-types>
<contract-fn-body> BODY </contract-fn-body>
<live-contracts>
.Bag => <live-contract>
<contract-address> ADDR </contract-address>
<contract-type> X </contract-type>
...
</live-contract>
...
</live-contracts>
<next-address> ADDR => ADDR +MInt 1p160 </next-address>
requires isKResult(ARGS)
rule <k> new X:Id ( .TypedVals ) ~> K => List2Statements(INIT) ~> return v(ADDR, X) ; </k>
<msg-sender> FROM => THIS </msg-sender>
<this> THIS => ADDR </this>
<this-type> TYPE => X </this-type>
<env> E => .Map </env>
<store> S => .Map </store>
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
<contract-id> X </contract-id>
<contract-init> INIT </contract-init>
<live-contracts>
.Bag => <live-contract>
<contract-address> ADDR </contract-address>
<contract-type> X </contract-type>
...
</live-contract>
...
</live-contracts>
<next-address> ADDR => ADDR +MInt 1p160 </next-address>
// literal assignment to state variable
rule <k> X:Id = N:NumberLiteral => X = v(convert(Number2Int(N), LT), LT) ...</k>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> LT </contract-state>
// assignment to state variable
rule <k> X:Id = v(V, RT) => v(convert(V, RT, LT), LT) ...</k>
<this> THIS </this>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-state>... X |-> LT </contract-state>
<contract-address> THIS </contract-address>
<contract-storage> S => S [ X <- convert(V, RT, LT) ] </contract-storage>
// assignment to local variable
rule <k> X:Id = v(V, RT) => v(convert(V, RT, LT), LT) ...</k>
<env>... X |-> var(I, LT) ...</env>
<store> S => S [ I <- convert(V, RT, LT) ] </store>
// type conversion
context _:ElementaryTypeName ( HOLE:CallArgumentList )
context _:Id ( HOLE:CallArgumentList )
rule address(v(ADDR:MInt{160}, _)) => v(ADDR, address)
rule address ( I:NumberLiteral ) => v(Int2MInt(Number2Int(I))::MInt{160}, address)
rule <k> TYPE(v(ADDR:MInt{160}, _)) => v(ADDR, TYPE) ...</k>
<contract-id> TYPE </contract-id>
rule <k> TYPE(v(ADDR:MInt{160}, _)) => v(ADDR, TYPE) ...</k>
<iface-id> TYPE </iface-id>
// state variable lookup
rule <k> X:Id => v(V, T) ...</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>... X |-> V ...</contract-storage>
// local variable lookup
rule <k> X:Id => v(V, T) ...</k>
<env>... X |-> var(I, T) ...</env>
<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>
<msg-sender> FROM => THIS </msg-sender>
<this> THIS => ADDR </this>
<this-type> TYPE => TYPE' </this-type>
<env> E => .Map </env>
<store> S => .Map </store>
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
<contract-id> TYPE' </contract-id>
<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>
<contract-fn-return-types> RETTYPES </contract-fn-return-types>
<contract-fn-return-names> RETNAMES </contract-fn-return-names>
<contract-fn-body> BODY </contract-fn-body>
<contract-address> ADDR </contract-address>
<contract-type> TYPE' </contract-type>
requires isKResult(ARGS)
// internal call
rule <k> F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<msg-sender> FROM </msg-sender>
<this-type> TYPE </this-type>
<env> E => .Map </env>
<store> S => .Map </store>
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
<contract-id> TYPE </contract-id>
<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>
<contract-fn-return-types> RETTYPES </contract-fn-return-types>
<contract-fn-return-names> RETNAMES </contract-fn-return-names>
<contract-fn-body> BODY </contract-fn-body>
requires isKResult(ARGS)
// 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)
rule v(V1:MInt{160}, _) < v(V2, _) => v(V1 <uMInt V2, bool)
rule v(V1:MInt{160}, _) <= v(V2, _) => v(V1 <=uMInt V2, bool)
rule v(V1:MInt{160}, _) > v(V2, _) => v(V1 >uMInt V2, bool)
rule v(V1:MInt{160}, _) >= v(V2, _) => v(V1 >=uMInt V2, bool)
// require expression
syntax Id ::= "require" [token]
rule require(v(true, bool), _) => void
// ternary expression
rule v(true, bool) ? X : _ => X
rule v(false, bool) ? _ : X => X
// helpers
syntax Int ::= Number2Int(NumberLiteral) [function]
rule Number2Int(X:HexNumber) => HexNumberString2Int(HexNumber2String(X))
rule Number2Int(X:Decimal) => DecimalString2Int(Decimal2String(X))
Expand All @@ -24,4 +163,33 @@ module SOLIDITY-EXPRESSION
rule DecimalString2Int(S) => String2Int(replaceAll(S, "_", ""))
requires findChar(S, "eE.", 0) ==Int -1
syntax Statements ::= List2Statements(List) [function]
rule List2Statements(.List) => .Statements
rule List2Statements(ListItem(S) L) => S List2Statements(L)
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 <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>
rule <k> bind(.List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(.List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
<env> E => E [ X <- var(!I:Int, LT) ] </env>
<store> S => S [ !I <- default(LT) ] </store>
syntax Value ::= convert(Value, from: TypeName, to: TypeName) [function]
rule convert(V, T, T) => V
syntax Value ::= convert(Int, TypeName) [function]
rule convert(I:Int, uint112) => Int2MInt(I)::MInt{112}
rule convert(I:Int, uint256) => Int2MInt(I)::MInt{256}
syntax Value ::= default(TypeName) [function]
rule default(address) => 0p160
syntax Expression ::= retval(List) [function]
rule retval(.List) => void
rule retval(ListItem(X:Id)) => X
endmodule
53 changes: 27 additions & 26 deletions src/solidity-syntax.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,10 @@ 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" | "uint256" | "address" | "bool"
syntax ElementaryTypeName ::= "uint" [function] | "uint112" | "uint256" | "address" | "bool"
syntax DataLocation ::= "memory" | "storage" | "calldata"
syntax SubDenom ::= "wei" | "gwei" | "ether" | "seconds" | "minutes" | "hours" | "days" | "weeks" | "years"
rule uint => uint256
```

## Literals
Expand Down Expand Up @@ -176,11 +177,11 @@ In each code block, various statments and nested blocks can be present.
Following is a list of supported statements.

```k
syntax ExpressionStatement ::= Expression ";"
syntax ExpressionStatement ::= Expression ";" [strict]
syntax VariableDeclarationStatement ::= VariableDeclaration ";"
| VariableDeclaration "=" Expression ";"
| "(" VariableDeclaration "," ")" "=" Expression ";"
| VariableDeclaration "=" Expression ";" [strict(2)]
| "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)]
syntax IfStatement ::= "if" "(" Expression ")" Statement
| "if" "(" Expression ")" Statement "else" Statement
Expand All @@ -193,7 +194,7 @@ Following is a list of supported statements.
syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";"
syntax ReturnStatement ::= "return" ";"
| "return" Expression ";"
| "return" Expression ";" [strict]
syntax RevertStatement ::= "revert" "(" CallArgumentList ")" ";"
| "revert" Id "(" CallArgumentList ")" ";"
Expand Down Expand Up @@ -225,7 +226,7 @@ Following is a list of supported expressions. Operator precendences are taken fr
syntax Expression ::= Id | Literal | LiteralWithSubDenom | ElementaryTypeName
> "(" Expression ")" [bracket]
| "[" CallArgumentList "]"
| "new" TypeName "(" CallArgumentList ")"
| "new" TypeName "(" CallArgumentList ")" [strict(2)]
| Expression "++" | Expression "--"
| Expression "[" Expression "]" | Expression "[""]"
| Expression "." Id | Expression ".address"
Expand All @@ -235,29 +236,29 @@ Following is a list of supported expressions. Operator precendences are taken fr
| "!" Expression
> left: Expression "**" Expression
> left:
Expression "*" Expression
| Expression "/" Expression
| Expression "%" Expression
Expression "*" Expression [strict]
| Expression "/" Expression [strict]
| Expression "%" Expression [strict]
> left:
Expression "+" Expression
| Expression "-" Expression
Expression "+" Expression [strict]
| Expression "-" Expression [strict]
> left:
Expression "<" Expression
| Expression "<=" Expression
| Expression ">" Expression
| Expression ">=" Expression
Expression "<" Expression [strict]
| Expression "<=" Expression [strict]
| Expression ">" Expression [strict]
| Expression ">=" Expression [strict]
> left:
Expression "==" Expression
| Expression "!=" Expression
> left: Expression "&&" Expression
> left: Expression "||" Expression
> left:
Expression "?" Expression ":" Expression
| Expression "+=" Expression
| Expression "-=" Expression
| Expression "*=" Expression
| Expression "/=" Expression
| Expression "=" Expression
Expression "==" Expression [strict]
| Expression "!=" Expression [strict]
> left: Expression "&&" Expression [strict(1)]
> left: Expression "||" Expression [strict(1)]
> right:
Expression "?" Expression ":" Expression [strict(1)]
| Expression "+=" Expression [strict(2)]
| Expression "-=" Expression [strict(2)]
| Expression "*=" Expression [strict(2)]
| Expression "/=" Expression [strict(2)]
| Expression "=" Expression [strict(2)]
endmodule
Expand Down
17 changes: 14 additions & 3 deletions src/solidity.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ requires "interface.md"
requires "contract.md"
requires "transaction.md"
requires "expression.md"
requires "statement.md"
module SOLIDITY-CONFIGURATION
imports SOLIDITY-DATA
Expand Down Expand Up @@ -41,6 +42,7 @@ module SOLIDITY-CONFIGURATION
<contract-fn-arg-types> .List </contract-fn-arg-types>
<contract-fn-param-names> .List </contract-fn-param-names>
<contract-fn-return-types> .List </contract-fn-return-types>
<contract-fn-return-names> .List </contract-fn-return-names>
<contract-fn-body> .Statements </contract-fn-body>
</contract-fn>
</contract-fns>
Expand All @@ -58,8 +60,11 @@ module SOLIDITY-CONFIGURATION
<msg-sender> 0p160 </msg-sender>
<msg-value> 0p256 </msg-value>
<tx-origin> 0p160 </tx-origin>
<this> 0p160 </this>
<this-type> Id </this-type>
<env> .Map </env>
<store> .Map </store>
<call-stack> .List </call-stack>
<live-contracts>
<live-contract multiplicity="*" type="Map">
<contract-address> 0p160 </contract-address>
Expand All @@ -80,11 +85,12 @@ module SOLIDITY-DATA-SYNTAX
imports STRING-SYNTAX
imports SOLIDITY-SYNTAX
syntax MInt{112}
syntax MInt{160}
syntax MInt{256}
syntax Transactions ::= List{Transaction, ","}
syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, func: Id, args: CallArgumentList) [strict(5)]
syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, func: Id, args: CallArgumentList) [function]
syntax Transaction ::= create(from: Decimal, value: Decimal, ctor: Id, args: CallArgumentList) [strict(4)]
endmodule
Expand All @@ -96,17 +102,18 @@ module SOLIDITY-DATA
imports ID
imports LIST
imports SET
imports MAP
imports SOLIDITY-DATA-SYNTAX
syntax KItem ::= "noId"
syntax Id ::= "constructor" [token]
syntax TypedVal ::= v(Value, TypeName)
syntax TypedVal ::= v(Value, TypeName) | NumberLiteral | String | "void"
syntax TypedVals ::= List{TypedVal, ","} [overload(exps), hybrid, strict]
syntax Expression ::= TypedVal
syntax CallArgumentList ::= TypedVals
syntax KResult ::= TypedVal
syntax Value ::= MInt{160} | MInt{256} | Bool | String
syntax Value ::= MInt{112} | MInt{160} | MInt{256} | Bool | String
syntax List ::= getTypes(ParameterList) [function]
rule getTypes(.ParameterList) => .List
Expand Down Expand Up @@ -141,6 +148,9 @@ module SOLIDITY-DATA
rule getIndexed(_:TypeName indexed _:Id, Ep:EventParameters, N:Int) => SetItem(N) getIndexed(Ep, N +Int 1)
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 Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id)
endmodule
```

Expand All @@ -151,6 +161,7 @@ module SOLIDITY
imports SOLIDITY-CONTRACT
imports SOLIDITY-TRANSACTION
imports SOLIDITY-EXPRESSION
imports SOLIDITY-STATEMENT
rule _:PragmaDefinition Ss:SourceUnits => Ss
rule S:SourceUnit Ss:SourceUnits => S ~> Ss
Expand Down
Loading

0 comments on commit 832eea9

Please sign in to comment.