From 678461e828842bcadd9e6cbca76409faba84b20f Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 11 May 2023 16:43:12 +0200 Subject: [PATCH] Fix encoding of side-effects inside if and conditional statements in the BMC engine --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 4 +++ .../control_flow/side_effects_inside_if_1.sol | 15 +++++++++ .../control_flow/side_effects_inside_if_2.sol | 26 ++++++++++++++++ .../control_flow/side_effects_inside_if_3.sol | 30 ++++++++++++++++++ .../control_flow/side_effects_inside_if_4.sol | 15 +++++++++ .../side_effects_inside_ternary_1.sol | 16 ++++++++++ .../side_effects_inside_ternary_2.sol | 27 ++++++++++++++++ .../side_effects_inside_ternary_3.sol | 31 +++++++++++++++++++ .../side_effects_inside_ternary_4.sol | 16 ++++++++++ 10 files changed, 181 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_1.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_2.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_3.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_4.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_1.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_2.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_3.sol create mode 100644 test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_4.sol diff --git a/Changelog.md b/Changelog.md index 164d998c2..36bf4dcfa 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Compiler Features: Bugfixes: + * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine. ### 0.8.20 (2023-05-10) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index e0a5f312b..b72e8451a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -237,6 +237,7 @@ void BMC::endVisit(FunctionDefinition const& _function) bool BMC::visit(IfStatement const& _node) { + auto indicesBeforePush = copyVariableIndices(); // This check needs to be done in its own context otherwise // constraints from the If body might influence it. m_context.pushSolver(); @@ -251,6 +252,7 @@ bool BMC::visit(IfStatement const& _node) &_node.condition() ); m_context.popSolver(); + resetVariableIndices(std::move(indicesBeforePush)); _node.condition().accept(*this); auto conditionExpr = expr(_node.condition()); @@ -274,6 +276,7 @@ bool BMC::visit(IfStatement const& _node) bool BMC::visit(Conditional const& _op) { + auto indicesBeforePush = copyVariableIndices(); m_context.pushSolver(); _op.condition().accept(*this); @@ -284,6 +287,7 @@ bool BMC::visit(Conditional const& _op) &_op.condition() ); m_context.popSolver(); + resetVariableIndices(std::move(indicesBeforePush)); SMTEncoder::visit(_op); diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_1.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_1.sol new file mode 100644 index 000000000..9bea0383a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_1.sol @@ -0,0 +1,15 @@ +contract C { + function f() public pure { + uint x; + if (++x < 3) {} + + assert(x == 1); // should hold + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 6838: (72-79): BMC: Condition is always true. +// Warning 4661: (132-146): BMC: Assertion violation happens here. +// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_2.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_2.sol new file mode 100644 index 000000000..1780a7e20 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_2.sol @@ -0,0 +1,26 @@ +contract C { + uint x; + + function inc() internal returns (uint) { + // BMC inlines function calls and also looks at functions in isolation, + // therefore it says once that this is safe, when called by `f`, + // but also that it is unsafe just looking at this function (false positive). + ++x; + return x; + } + + function f() public { + require(x < 1000); + uint y = x; + if (inc() < 3) {} + + assert(x == y + 1); // should hold + assert(x != y + 1); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (499-517): BMC: Assertion violation happens here. +// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_3.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_3.sol new file mode 100644 index 000000000..2e415a7b0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_3.sol @@ -0,0 +1,30 @@ +contract C { + uint x; + + function inc() internal returns (uint) { + // BMC inlines function calls and also looks at functions in isolation, + // therefore it says once that this is safe, when called by `f`, + // but also that it is unsafe just looking at this function (false positive). + ++x; + return x; + } + + function inc2() internal returns (uint) { + return inc(); + } + + function f() public { + require(x < 1000); + uint y = x; + if (inc2() < 3) {} + + assert(x == y + 1); // should hold + assert(x != y + 1); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (575-593): BMC: Assertion violation happens here. +// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_4.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_4.sol new file mode 100644 index 000000000..6e624184e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_4.sol @@ -0,0 +1,15 @@ +contract C { + function f() public pure { + uint x = 2; + if (--x < 3) {} + + assert(x == 1); // should hold + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 6838: (76-83): BMC: Condition is always true. +// Warning 4661: (136-150): BMC: Assertion violation happens here. +// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_1.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_1.sol new file mode 100644 index 000000000..9801b99b5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_1.sol @@ -0,0 +1,16 @@ +contract C { + function f() public pure { + uint x; + uint y = (++x < 3) ? ++x : --x; + + assert(y == x); // should hold; + assert(x == 2); // should hold + assert(x != 2); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 6838: (77-86): BMC: Condition is always true. +// Warning 4661: (188-202): BMC: Assertion violation happens here. +// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_2.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_2.sol new file mode 100644 index 000000000..54d72960b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_2.sol @@ -0,0 +1,27 @@ +contract C { + uint x; + + function inc() internal returns (uint) { + // BMC inlines function calls and also looks at functions in isolation, + // therefore it says once that this is safe, when called by `f`, + // but also that it is unsafe just looking at this function (false positive). + ++x; + return x; + } + + function f() public { + require(x < 1000); + uint z = x; + uint y = (inc() < 3) ? inc() : inc(); + + assert(y == x); + assert(x == z + 2); // should hold + assert(x != z + 2); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (543-561): BMC: Assertion violation happens here. +// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_3.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_3.sol new file mode 100644 index 000000000..18e36c8fd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_3.sol @@ -0,0 +1,31 @@ +contract C { + uint x; + + function inc() internal returns (uint) { + // BMC inlines function calls and also looks at functions in isolation, + // therefore it says once that this is safe, when called by `f`, + // but also that it is unsafe just looking at this function (false positive). + ++x; + return x; + } + + function inc2() internal returns (uint) { + return inc(); + } + + function f() public { + require(x < 1000); + uint z = x; + uint y = (inc2() < 3) ? inc2() : inc2(); + + assert(y == x); // should hold + assert(x == z + 2); // should hold + assert(x != z + 2); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (636-654): BMC: Assertion violation happens here. +// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_4.sol b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_4.sol new file mode 100644 index 000000000..e24cdf297 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_4.sol @@ -0,0 +1,16 @@ +contract C { + function f() public pure { + uint x = 2; + uint y = (--x < 3) ? --x : 0; + + assert(y == x); // should hold + assert(x == 0); // should hold + assert(x != 0); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 6838: (81-90): BMC: Condition is always true. +// Warning 4661: (189-203): BMC: Assertion violation happens here. +// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.