From 00363a4d47c9b6962b4f3d36426ded7d35a10683 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 10:24:16 -0500 Subject: [PATCH 1/6] boolean and/or --- src/expression.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/expression.md b/src/expression.md index e4ba232..949bba9 100644 --- a/src/expression.md +++ b/src/expression.md @@ -150,6 +150,12 @@ module SOLIDITY-EXPRESSION rule v(true, bool) ? X : _ => X rule v(false, bool) ? _ : X => X + // boolean and/or + rule v(true, bool) && E => E + rule v(false, bool) && _ => v(false, bool) + rule v(true, bool) || _ => v(true, bool) + rule v(false, bool) || E => E + // helpers syntax Int ::= Number2Int(NumberLiteral) [function] rule Number2Int(X:HexNumber) => HexNumberString2Int(HexNumber2String(X)) From decce7de975be88637be26b0257a8c712c7fdd4c Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 10:24:30 -0500 Subject: [PATCH 2/6] if statements --- src/solidity-syntax.md | 4 ++-- src/statement.md | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md index 9bb5312..29c888f 100644 --- a/src/solidity-syntax.md +++ b/src/solidity-syntax.md @@ -183,8 +183,8 @@ Following is a list of supported statements. | VariableDeclaration "=" Expression ";" [strict(2)] | "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)] - syntax IfStatement ::= "if" "(" Expression ")" Statement - | "if" "(" Expression ")" Statement "else" Statement + syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)] + | "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)] syntax ForStatement ::= "for" "(" InitStatement ConditionStatement PostLoopStatement ")" Statement syntax InitStatement ::= VariableDeclarationStatement | ExpressionStatement | ";" diff --git a/src/statement.md b/src/statement.md index 3b8f4f5..d0063a0 100644 --- a/src/statement.md +++ b/src/statement.md @@ -31,4 +31,9 @@ module SOLIDITY-STATEMENT ... .List => ListItem(event(X, ARGS)) requires isKResult(ARGS) + // if statement + rule if ( v(true, bool ) ) S => S + rule if ( v(false, bool ) ) _ => .K + rule if ( v(true, bool ) ) S else _ => S + rule if ( v(false, bool ) ) _ else S => S endmodule From c7b643ea239021294af5cfa5355ddb5ea6fda7db Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 10:24:39 -0500 Subject: [PATCH 3/6] blocks --- src/statement.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/statement.md b/src/statement.md index d0063a0..9949f23 100644 --- a/src/statement.md +++ b/src/statement.md @@ -36,4 +36,13 @@ module SOLIDITY-STATEMENT rule if ( v(false, bool ) ) _ => .K rule if ( v(true, bool ) ) S else _ => S rule if ( v(false, bool ) ) _ else S => S + + // blocks + rule { S } => S ~> restoreEnv(E) ... + E + + syntax KItem ::= restoreEnv(Map) + rule restoreEnv(E) => .K ... + _ => E + endmodule From 4f9c6bef168045ef2a6eb8229e640e0472fdb0ef Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 11:11:15 -0500 Subject: [PATCH 4/6] add test --- test/regression/block.ref | 95 +++++++++++++++++++++++++++++ test/regression/block.sol | 15 +++++ test/regression/block.txn | 1 + test/regression/boolean.ref | 116 ++++++++++++++++++++++++++++++++++++ test/regression/boolean.sol | 28 +++++++++ test/regression/boolean.txn | 1 + test/regression/if.ref | 94 +++++++++++++++++++++++++++++ test/regression/if.sol | 20 +++++++ test/regression/if.txn | 1 + 9 files changed, 371 insertions(+) create mode 100644 test/regression/block.ref create mode 100644 test/regression/block.sol create mode 100644 test/regression/block.txn create mode 100644 test/regression/boolean.ref create mode 100644 test/regression/boolean.sol create mode 100644 test/regression/boolean.txn create mode 100644 test/regression/if.ref create mode 100644 test/regression/if.sol create mode 100644 test/regression/if.txn diff --git a/test/regression/block.ref b/test/regression/block.ref new file mode 100644 index 0000000..9f18fcc --- /dev/null +++ b/test/regression/block.ref @@ -0,0 +1,95 @@ + + + .K + + + BlockTest + + + .IfaceCellMap + + + + + BlockTest + + + .Map + + + .List + + + + + constructor + + + public + + + .List + + + .List + + + .List + + + .List + + + bool x = false ; { bool x = true ; require ( x , "" , .TypedVals ) ; .Statements } if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements + + + + + .ContractEventCellMap + + + + + + 1p160 + + + 0p256 + + + 1p160 + + + 2p160 + + + BlockTest + + + x |-> var ( 0 , bool ) + + + 0 |-> false + 1 |-> true + + + .List + + + + + 2p160 + + + BlockTest + + + .Map + + + + + 3p160 + + + diff --git a/test/regression/block.sol b/test/regression/block.sol new file mode 100644 index 0000000..c3a9706 --- /dev/null +++ b/test/regression/block.sol @@ -0,0 +1,15 @@ +pragma solidity ^0.8.24; + +contract BlockTest { + + constructor() { + bool x = false; + { + bool x = true; + require(x, ""); + } + if (x) { + require(false, ""); + } + } +} diff --git a/test/regression/block.txn b/test/regression/block.txn new file mode 100644 index 0000000..9571da7 --- /dev/null +++ b/test/regression/block.txn @@ -0,0 +1 @@ +create(1, 0, BlockTest, ) diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref new file mode 100644 index 0000000..135972b --- /dev/null +++ b/test/regression/boolean.ref @@ -0,0 +1,116 @@ + + + .K + + + BoolTest + + + .IfaceCellMap + + + + + BoolTest + + + .Map + + + .List + + + + + constructor + + + public + + + .List + + + .List + + + .List + + + .List + + + bool x = true ; if ( x || fail ( .TypedVals ) ) { .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } if ( x && true ) { .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } x = false ; if ( x && fail ( .TypedVals ) ) { require ( false , "" , .TypedVals ) ; .Statements } if ( x || true ) { .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } .Statements + + + + fail + + + private + + + .List + + + .List + + + .List + + + .List + + + require ( false , "" , .TypedVals ) ; .Statements + + + + + .ContractEventCellMap + + + + + + 1p160 + + + 0p256 + + + 1p160 + + + 2p160 + + + BoolTest + + + x |-> var ( 0 , bool ) + + + 0 |-> false + + + .List + + + + + 2p160 + + + BoolTest + + + .Map + + + + + 3p160 + + + diff --git a/test/regression/boolean.sol b/test/regression/boolean.sol new file mode 100644 index 0000000..bdf3984 --- /dev/null +++ b/test/regression/boolean.sol @@ -0,0 +1,28 @@ +pragma solidity ^0.8.24; + +contract BoolTest { + + function fail() private { + require(false, ""); + } + + constructor() { + bool x = true; + if (x || fail()) { + } else { + require(false, ""); + } + if (x && true) { + } else { + require(false, ""); + } + x = false; + if (x && fail()) { + require(false, ""); + } + if (x || true) { + } else { + require(false, ""); + } + } +} diff --git a/test/regression/boolean.txn b/test/regression/boolean.txn new file mode 100644 index 0000000..561f2f3 --- /dev/null +++ b/test/regression/boolean.txn @@ -0,0 +1 @@ +create(1, 0, BoolTest, ) diff --git a/test/regression/if.ref b/test/regression/if.ref new file mode 100644 index 0000000..ca54898 --- /dev/null +++ b/test/regression/if.ref @@ -0,0 +1,94 @@ + + + .K + + + IfTest + + + .IfaceCellMap + + + + + IfTest + + + .Map + + + .List + + + + + constructor + + + public + + + .List + + + .List + + + .List + + + .List + + + bool x = true ; if ( x ) { .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } x = false ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } else { .Statements } if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements + + + + + .ContractEventCellMap + + + + + + 1p160 + + + 0p256 + + + 1p160 + + + 2p160 + + + IfTest + + + x |-> var ( 0 , bool ) + + + 0 |-> false + + + .List + + + + + 2p160 + + + IfTest + + + .Map + + + + + 3p160 + + + diff --git a/test/regression/if.sol b/test/regression/if.sol new file mode 100644 index 0000000..fdf7c43 --- /dev/null +++ b/test/regression/if.sol @@ -0,0 +1,20 @@ +pragma solidity ^0.8.24; + +contract IfTest { + + constructor() { + bool x = true; + if (x) { + } else { + require(false, ""); + } + x = false; + if (x) { + require(false, ""); + } else { + } + if (x) { + require(false, ""); + } + } +} diff --git a/test/regression/if.txn b/test/regression/if.txn new file mode 100644 index 0000000..904ffed --- /dev/null +++ b/test/regression/if.txn @@ -0,0 +1 @@ +create(1, 0, IfTest, ) From 9441a50574b772b5acd0bed1db3cbc96809c70e3 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 11:22:27 -0500 Subject: [PATCH 5/6] update tests --- test/regression/block.ref | 3 +++ test/regression/boolean.ref | 3 +++ test/regression/if.ref | 3 +++ 3 files changed, 9 insertions(+) diff --git a/test/regression/block.ref b/test/regression/block.ref index 9f18fcc..263cf13 100644 --- a/test/regression/block.ref +++ b/test/regression/block.ref @@ -88,6 +88,9 @@ + + .List + 3p160 diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref index 135972b..1fdbda5 100644 --- a/test/regression/boolean.ref +++ b/test/regression/boolean.ref @@ -109,6 +109,9 @@ + + .List + 3p160 diff --git a/test/regression/if.ref b/test/regression/if.ref index ca54898..7878dd8 100644 --- a/test/regression/if.ref +++ b/test/regression/if.ref @@ -87,6 +87,9 @@ + + .List + 3p160 From c77bc8af07cf23c652a8798267c6ec6ecd796355 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 26 Aug 2024 11:45:02 -0500 Subject: [PATCH 6/6] update test to have better coverage --- test/regression/if.ref | 4 +++- test/regression/if.sol | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/test/regression/if.ref b/test/regression/if.ref index 7878dd8..f0e0f02 100644 --- a/test/regression/if.ref +++ b/test/regression/if.ref @@ -40,7 +40,7 @@ .List - bool x = true ; if ( x ) { .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } x = false ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } else { .Statements } if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements + bool x = true ; bool y = false ; if ( x ) { y = true ; .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } require ( y , "" , .TypedVals ) ; y = false ; x = false ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } else { y = true ; .Statements } require ( y , "" , .TypedVals ) ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements @@ -67,9 +67,11 @@ x |-> var ( 0 , bool ) + y |-> var ( 1 , bool ) 0 |-> false + 1 |-> true .List diff --git a/test/regression/if.sol b/test/regression/if.sol index fdf7c43..540a641 100644 --- a/test/regression/if.sol +++ b/test/regression/if.sol @@ -4,15 +4,21 @@ contract IfTest { constructor() { bool x = true; + bool y = false; if (x) { + y = true; } else { require(false, ""); } + require(y, ""); + y = false; x = false; if (x) { require(false, ""); } else { + y = true; } + require(y, ""); if (x) { require(false, ""); }