Skip to content

Commit

Permalink
Remove strict and context from the definition (#38)
Browse files Browse the repository at this point in the history 
* Remove strict attribute.

* Updated reference that used freezers (names changed).

* Remove contexts.

* Removed side conditions from heating rules.

They were imposing a specific ordering rather than allowing non determinism.
  • Loading branch information
@mariaKt
mariaKt authored Sep 24, 2024
1 parent 5885979 commit b1c267e
Show file tree
Hide file tree
Showing 6 changed files with 230 additions and 45 deletions.
176 changes: 163 additions & 13 deletions src/expression.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,8 +89,6 @@ module SOLIDITY-EXPRESSION
<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>
Expand All @@ -109,8 +107,6 @@ module SOLIDITY-EXPRESSION
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 )
rule uint32(v(V:MInt{256}, _)) => v(roundMInt(V)::MInt{32}, uint32)
rule uint112(v(V:MInt{256}, _)) => v(roundMInt(V)::MInt{112}, uint112)
rule uint256(v(V:MInt{112}, _)) => v(roundMInt(V)::MInt{256}, uint256)
Expand Down Expand Up @@ -149,8 +145,6 @@ module SOLIDITY-EXPRESSION
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)
Expand Down Expand Up @@ -180,13 +174,10 @@ module SOLIDITY-EXPRESSION
// 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, _) . 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>
Expand All @@ -209,10 +200,6 @@ module SOLIDITY-EXPRESSION
syntax Id ::= "value" [token]
context HOLE . _ { value: _ } ( _ )
context _ . _ { value: HOLE } ( _ )
context _ . _ { _ } ( HOLE:CallArgumentList )
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>
Expand Down Expand Up @@ -515,4 +502,167 @@ module SOLIDITY-EXPRESSION
rule retval(.List) => void
rule retval(ListItem(noId)) => void
rule retval(ListItem(X:Id)) => X
// Heating and cooling rules
syntax KItem ::= freezerAssignment(Expression)
rule <k> E:Expression = HOLE:Expression => HOLE ~> freezerAssignment(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAssignment(E) => E = HOLE ...</k> [cool]
syntax KItem ::= freezerTernaryOperator(Expression, Expression)
rule <k> HOLE:Expression ? E1:Expression : E2:Expression => HOLE ~> freezerTernaryOperator(E1, E2) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerTernaryOperator(E1, E2) => HOLE ? E1 : E2 ...</k> [cool]
syntax KItem ::= freezerOr(Expression)
rule <k> HOLE:Expression || E:Expression => HOLE ~> freezerOr(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerOr(E) => HOLE || E ...</k> [cool]
syntax KItem ::= freezerAnd(Expression)
rule <k> HOLE:Expression && E:Expression => HOLE ~> freezerAnd(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAnd(E) => HOLE && E ...</k> [cool]
syntax KItem ::= freezerEq1(Expression)
| freezerEq2(Expression)
rule <k> HOLE:Expression == E:Expression => HOLE ~> freezerEq1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerEq1(E) => HOLE == E ...</k> [cool]
rule <k> E:Expression == HOLE:Expression => HOLE ~> freezerEq2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerEq2(E) => E == HOLE ...</k> [cool]
syntax KItem ::= freezerNeq1(Expression)
| freezerNeq2(Expression)
rule <k> HOLE:Expression != E:Expression => HOLE ~> freezerNeq1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerNeq1(E) => HOLE != E ...</k> [cool]
rule <k> E:Expression != HOLE:Expression => HOLE ~> freezerNeq2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerNeq2(E) => E != HOLE ...</k> [cool]
syntax KItem ::= freezerLt1(Expression)
| freezerLt2(Expression)
rule <k> HOLE:Expression < E:Expression => HOLE ~> freezerLt1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerLt1(E) => HOLE < E ...</k> [cool]
rule <k> E:Expression < HOLE:Expression => HOLE ~> freezerLt2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerLt2(E) => E < HOLE ...</k> [cool]
syntax KItem ::= freezerLeq1(Expression)
| freezerLeq2(Expression)
rule <k> HOLE:Expression <= E:Expression => HOLE ~> freezerLeq1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerLeq1(E) => HOLE <= E ...</k> [cool]
rule <k> E:Expression <= HOLE:Expression => HOLE ~> freezerLeq2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerLeq2(E) => E <= HOLE ...</k> [cool]
syntax KItem ::= freezerGt1(Expression)
| freezerGt2(Expression)
rule <k> HOLE:Expression > E:Expression => HOLE ~> freezerGt1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerGt1(E) => HOLE > E ...</k> [cool]
rule <k> E:Expression > HOLE:Expression => HOLE ~> freezerGt2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerGt2(E) => E > HOLE ...</k> [cool]
syntax KItem ::= freezerGeq1(Expression)
| freezerGeq2(Expression)
rule <k> HOLE:Expression >= E:Expression => HOLE ~> freezerGeq1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerGeq1(E) => HOLE >= E ...</k> [cool]
rule <k> E:Expression >= HOLE:Expression => HOLE ~> freezerGeq2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerGeq2(E) => E >= HOLE ...</k> [cool]
syntax KItem ::= freezerAdd1(Expression)
| freezerAdd2(Expression)
rule <k> HOLE:Expression + E:Expression => HOLE ~> freezerAdd1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAdd1(E) => HOLE + E ...</k> [cool]
rule <k> E:Expression + HOLE:Expression => HOLE ~> freezerAdd2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAdd2(E) => E + HOLE ...</k> [cool]
syntax KItem ::= freezerSub1(Expression)
| freezerSub2(Expression)
rule <k> HOLE:Expression - E:Expression => HOLE ~> freezerSub1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerSub1(E) => HOLE - E ...</k> [cool]
rule <k> E:Expression - HOLE:Expression => HOLE ~> freezerSub2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerSub2(E) => E - HOLE ...</k> [cool]
syntax KItem ::= freezerMul1(Expression)
| freezerMul2(Expression)
rule <k> HOLE:Expression * E:Expression => HOLE ~> freezerMul1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerMul1(E) => HOLE * E ...</k> [cool]
rule <k> E:Expression * HOLE:Expression => HOLE ~> freezerMul2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerMul2(E) => E * HOLE ...</k> [cool]
syntax KItem ::= freezerDiv1(Expression)
| freezerDiv2(Expression)
rule <k> HOLE:Expression / E:Expression => HOLE ~> freezerDiv1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerDiv1(E) => HOLE / E ...</k> [cool]
rule <k> E:Expression / HOLE:Expression => HOLE ~> freezerDiv2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerDiv2(E) => E / HOLE ...</k> [cool]
syntax KItem ::= freezerMod1(Expression)
| freezerMod2(Expression)
rule <k> HOLE:Expression % E:Expression => HOLE ~> freezerMod1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerMod1(E) => HOLE % E ...</k> [cool]
rule <k> E:Expression % HOLE:Expression => HOLE ~> freezerMod2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerMod2(E) => E % HOLE ...</k> [cool]
syntax KItem ::= freezerExp1(Expression)
| freezerExp2(Expression)
rule <k> HOLE:Expression ** E:Expression => HOLE ~> freezerExp1(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExp1(E) => HOLE ** E ...</k> [cool]
rule <k> E:Expression ** HOLE:Expression => HOLE ~> freezerExp2(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExp2(E) => E ** HOLE ...</k> [cool]
syntax KItem ::= freezerNew(TypeName)
rule <k> new T:TypeName ( HOLE:CallArgumentList ) => HOLE ~> freezerNew(T) ...</k> [heat]
rule <k> HOLE:CallArgumentList ~> freezerNew(T) => new T ( HOLE ) ...</k> [cool]
syntax KItem ::= freezerCallArgumentListHead(Expression)
| freezerCallArgumentListTail(CallArgumentList)
rule <k> HOLE:Expression, L:CallArgumentList => HOLE ~> freezerCallArgumentListTail(L) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerCallArgumentListTail(L) => HOLE, L ...</k> [cool]
rule <k> E:Expression, HOLE:CallArgumentList => HOLE ~> freezerCallArgumentListHead(E) ...</k> [heat]
rule <k> HOLE:CallArgumentList ~> freezerCallArgumentListHead(E) => E, HOLE ...</k> [cool]
syntax KItem ::= freezerTypedValsHead(TypedVal)
| freezerTypedValsTail(TypedVals)
rule <k> HOLE:TypedVal, L:TypedVals => HOLE ~> freezerTypedValsTail(L) ...</k> [heat]
rule <k> HOLE:TypedVal ~> freezerTypedValsTail(L) => HOLE, L ...</k> [cool]
rule <k> E:TypedVal, HOLE:TypedVals => HOLE ~> freezerTypedValsHead(E) ...</k> [heat]
rule <k> HOLE:TypedVals ~> freezerTypedValsHead(E) => E, HOLE ...</k> [cool]
syntax KItem ::= freezerAssignmentToArrayElementBase(Expression, Expression)
| freezerAssignmentToArrayElementIndex(Expression, Expression)
rule <k> HOLE:Expression [ E2:Expression ] = E3:Expression => HOLE ~> freezerAssignmentToArrayElementBase(E2, E3) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAssignmentToArrayElementBase(E2, E3) => HOLE [ E2 ] = E3 ...</k> [cool]
rule <k> E1:Expression [ HOLE:Expression ] = E3:Expression => HOLE ~> freezerAssignmentToArrayElementIndex(E1, E3) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerAssignmentToArrayElementIndex(E1, E3) => E1 [ HOLE ] = E3 ...</k> [cool]
syntax KItem ::= freezerCallElementaryTypeName(ElementaryTypeName)
rule <k> T:ElementaryTypeName ( HOLE:CallArgumentList ) => HOLE ~> freezerCallElementaryTypeName(T) ...</k> [heat]
rule <k> HOLE:CallArgumentList ~> freezerCallElementaryTypeName(T) => T ( HOLE ) ...</k> [cool]
syntax KItem ::= freezerCallId(Id)
rule <k> ID:Id ( HOLE:CallArgumentList ) => HOLE ~> freezerCallId(ID) ...</k> [heat]
rule <k> HOLE:CallArgumentList ~> freezerCallId(ID) => ID ( HOLE ) ...</k> [cool]
syntax KItem ::= freezerArrayElementLookupBase(Expression)
| freezerArrayElementLookupIndex(Expression)
rule <k> HOLE:Expression [ E:Expression ] => HOLE ~> freezerArrayElementLookupBase(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerArrayElementLookupBase(E) => HOLE [ E ] ...</k> [cool]
rule <k> E:Expression [ HOLE:Expression ] => HOLE ~> freezerArrayElementLookupIndex(E) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerArrayElementLookupIndex(E) => E [ HOLE ] ...</k> [cool]
syntax KItem ::= freezerLength()
rule <k> HOLE:Expression . length => HOLE ~> freezerLength() ...</k> [heat]
rule <k> HOLE:Expression ~> freezerLength() => HOLE . length ...</k> [cool]
syntax KItem ::= freezerExternalCallBase(Id, CallArgumentList)
| freezerExternalCallArgs(Expression, Id)
rule <k> HOLE:Expression . ID:Id ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallBase(ID, ARGS) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExternalCallBase(ID, ARGS) => (HOLE . ID) ( ARGS ) ...</k> [cool]
rule <k> (E:Expression . ID:Id) ( HOLE:CallArgumentList ) => HOLE ~> freezerExternalCallArgs(E, ID) ...</k> [heat]
rule <k> HOLE:CallArgumentList ~> freezerExternalCallArgs(E, ID) => (E . ID) ( HOLE ) ...</k> [cool]
syntax KItem ::= freezerExternalCallWithValueBase(Id, Expression, CallArgumentList)
| freezerExternalCallWithValueValue(Expression, Id, CallArgumentList)
| freezerExternalCallWithValueArgs(Expression, Id, KeyValues)
rule <k> HOLE:Expression . ID:Id { value: V:Expression } ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueBase(ID, V, ARGS) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExternalCallWithValueBase(ID, V, ARGS) => HOLE . ID { value : V } ( ARGS ) ...</k> [cool]
rule <k> E:Expression . ID:Id { value: HOLE:Expression } ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueValue(E, ID, ARGS) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExternalCallWithValueValue(E, ID, ARGS) => E . ID { value : HOLE } ( ARGS ) ...</k> [cool]
rule <k> E:Expression . ID:Id { L:KeyValues } ( HOLE:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueArgs(E, ID, L) ...</k> [heat]
rule <k> HOLE:Expression ~> freezerExternalCallWithValueArgs(E, ID, L) => E . ID { L } ( HOLE ) ...</k> [cool]
endmodule
51 changes: 25 additions & 26 deletions src/solidity-syntax.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,23 +179,23 @@ In each code block, various statments and nested blocks can be present.
Following is a list of supported statements.

```k
syntax ExpressionStatement ::= Expression ";" [strict]
syntax ExpressionStatement ::= Expression ";"
syntax VariableDeclarationStatement ::= VariableDeclaration ";"
| VariableDeclaration "=" Expression ";" [strict(2)]
| "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)]
| VariableDeclaration "=" Expression ";"
| "(" VariableDeclaration "," ")" "=" Expression ";"
syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)]
| "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)]
syntax IfStatement ::= "if" "(" Expression ")" Statement
| "if" "(" Expression ")" Statement "else" Statement [avoid]
syntax WhileStatement ::= "while" "(" Expression ")" Statement
syntax Block ::= "for" "(" VariableDeclarationStatement Expression ";" Expression ")" Statement [function]
rule for (Init Cond ; Post) Body => { Init while(Cond) { Body Post; } }
syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" [strict(2)]
syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";"
syntax ReturnStatement ::= "return" ";"
| "return" Expression ";" [strict]
| "return" Expression ";"
syntax RevertStatement ::= "revert" "(" CallArgumentList ")" ";"
| "revert" Id "(" CallArgumentList ")" ";"
Expand All @@ -207,7 +207,7 @@ Following is a list of supported statements.
`CallArgumentList` keeps a list of arguments for function calls and such (`revert()`, `emit()`, etc.)

```k
syntax CallArgumentList ::= List{Expression, ","} [overload(exps), strict]
syntax CallArgumentList ::= List{Expression, ","} [overload(exps)]
```

Expand All @@ -227,36 +227,35 @@ Following is a list of supported expressions. Operator precendences are taken fr
syntax Expression ::= Id | Literal | LiteralWithSubDenom | ElementaryTypeName
> "(" Expression ")" [bracket]
| "[" CallArgumentList "]"
| "new" TypeName "(" CallArgumentList ")" [strict(2)]
| "new" TypeName "(" CallArgumentList ")"
| Expression "++" | Expression "--"
| Expression "[" Expression "]" | Expression "[""]"
| Expression "." Id | Expression ".address"
| Expression "{" KeyValues "}"
| Expression "(" CallArgumentList ")"
> "++" Expression | "--" Expression
| "!" Expression
> left: Expression "**" Expression [strict]
> left: Expression "**" Expression
> left:
Expression "*" Expression [strict]
| Expression "/" Expression [strict]
| Expression "%" Expression [strict]
Expression "*" Expression
| Expression "/" Expression
| Expression "%" Expression
> left:
Expression "+" Expression [strict]
| Expression "-" Expression [strict]
Expression "+" Expression
| Expression "-" Expression
> left:
Expression "<" Expression [strict]
| Expression "<=" Expression [strict]
| Expression ">" Expression [strict]
| Expression ">=" Expression [strict]
Expression "<" Expression
| Expression "<=" Expression
| Expression ">" Expression
| Expression ">=" Expression
> left:
Expression "==" Expression [strict]
| Expression "!=" Expression [strict]
> left: Expression "&&" Expression [strict(1)]
> left: Expression "||" Expression [strict(1)]
Expression "==" Expression
| Expression "!=" Expression
> left: Expression "&&" Expression
> left: Expression "||" Expression
> right:
Expression "?" Expression ":" Expression [strict(1)]
| Expression "=" Expression [strict(2)]
Expression "?" Expression ":" Expression
| Expression "=" Expression
endmodule
```
4 changes: 2 additions & 2 deletions src/solidity.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ module SOLIDITY-DATA-SYNTAX
syntax Transactions ::= List{Transaction, ","}
syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [function]
syntax Transaction ::= create(from: Decimal, value: Decimal, timestamp: Decimal, ctor: Id, args: CallArgumentList) [strict(5)]
syntax Transaction ::= create(from: Decimal, value: Decimal, timestamp: Decimal, ctor: Id, args: CallArgumentList)
endmodule
module SOLIDITY-DATA
Expand All @@ -118,7 +118,7 @@ module SOLIDITY-DATA
syntax Id ::= "constructor" [token]
syntax TypedVal ::= v(Value, TypeName) | lv(BaseRef, List, TypeName) | Int | String | "void"
syntax TypedVals ::= List{TypedVal, ","} [overload(exps), strict]
syntax TypedVals ::= List{TypedVal, ","} [overload(exps)]
syntax Expression ::= TypedVal
syntax CallArgumentList ::= TypedVals
syntax KResult ::= TypedVal | TypedVals
Expand Down
Loading

0 comments on commit b1c267e

Please sign in to comment.