Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove strict and context from the definition #38

Merged
merged 6 commits into from
Sep 24, 2024
Merged

Remove strict and context from the definition #38

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7a5dac3
Remove strict attribute.
mariaKt Sep 20, 2024
616cfb9
Updated reference that used freezers (names changed).
mariaKt Sep 20, 2024
fbb9e58
Remove contexts.
mariaKt Sep 20, 2024
1760ee2
Removed side conditions from heating rules.
mariaKt Sep 21, 2024
1055912
Merge branch 'main' into remove-strict
mariaKt Sep 23, 2024
fdeafab
Merge branch 'main' into remove-strict
mariaKt Sep 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
176 changes: 163 additions & 13 deletions src/expression.md
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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