diff options
18 files changed, 217 insertions, 18 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index ebb09f0a..0c2af44b 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -136,13 +136,24 @@ bool SMTChecker::visit(IfStatement const& _node) return false; } +// Here we consider the execution of two branches: +// Branch 1 assumes the loop condition to be true and executes the loop once, +// after resetting touched variables. +// Branch 2 assumes the loop condition to be false and skips the loop after +// visiting the condition (it might contain side-effects, they need to be considered) +// and does not erase knowledge. +// If the loop is a do-while, condition side-effects are lost since the body, +// executed once before the condition, might reassign variables. +// Variables touched by the loop are merged with Branch 2. bool SMTChecker::visit(WhileStatement const& _node) { + auto indicesBeforeLoop = copyVariableIndices(); auto touchedVariables = m_variableUsage->touchedVariables(_node); resetVariables(touchedVariables); + decltype(indicesBeforeLoop) indicesAfterLoop; if (_node.isDoWhile()) { - visitBranch(_node.body()); + indicesAfterLoop = visitBranch(_node.body()); // TODO the assertions generated in the body should still be active in the condition _node.condition().accept(*this); if (isRootFunction()) @@ -154,19 +165,31 @@ bool SMTChecker::visit(WhileStatement const& _node) if (isRootFunction()) checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE."); - visitBranch(_node.body(), expr(_node.condition())); + indicesAfterLoop = visitBranch(_node.body(), expr(_node.condition())); } - m_loopExecutionHappened = true; - resetVariables(touchedVariables); + // We reset the execution to before the loop + // and visit the condition in case it's not a do-while. + // A do-while's body might have non-precise information + // in its first run about variables that are touched. + resetVariableIndices(indicesBeforeLoop); + if (!_node.isDoWhile()) + _node.condition().accept(*this); + + mergeVariables(touchedVariables, expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); + + m_loopExecutionHappened = true; return false; } +// Here we consider the execution of two branches similar to WhileStatement. bool SMTChecker::visit(ForStatement const& _node) { if (_node.initializationExpression()) _node.initializationExpression()->accept(*this); + auto indicesBeforeLoop = copyVariableIndices(); + // Do not reset the init expression part. auto touchedVariables = m_variableUsage->touchedVariables(_node.body()); @@ -193,13 +216,19 @@ bool SMTChecker::visit(ForStatement const& _node) _node.body().accept(*this); if (_node.loopExpression()) _node.loopExpression()->accept(*this); - m_interface->pop(); - m_loopExecutionHappened = true; + auto indicesAfterLoop = copyVariableIndices(); + // We reset the execution to before the loop + // and visit the condition. + resetVariableIndices(indicesBeforeLoop); + if (_node.condition()) + _node.condition()->accept(*this); - resetVariables(touchedVariables); + auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true); + mergeVariables(touchedVariables, forCondition, indicesAfterLoop, copyVariableIndices()); + m_loopExecutionHappened = true; return false; } @@ -820,6 +849,7 @@ void SMTChecker::checkCondition( loopComment = "\nNote that some information is erased after the execution of loops.\n" "You can re-introduce information using require()."; + switch (result) { case smt::CheckResult::SATISFIABLE: @@ -838,19 +868,19 @@ void SMTChecker::checkCondition( for (auto const& eval: sortedModel) modelMessage << " " << eval.first << " = " << eval.second << "\n"; - m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation())); + m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(modelMessage.str(), SourceLocation()).append(loopComment, SourceLocation())); } else { message << "."; - m_errorReporter.warning(_location, message.str() + loopComment); + m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(loopComment, SourceLocation())); } break; } case smt::CheckResult::UNSATISFIABLE: break; case smt::CheckResult::UNKNOWN: - m_errorReporter.warning(_location, _description + " might happen here." + loopComment); + m_errorReporter.warning(_location, _description + " might happen here.", SecondarySourceLocation().append(loopComment, SourceLocation())); break; case smt::CheckResult::CONFLICTING: m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol new file mode 100644 index 00000000..ea5bf044 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + do { + // Overflows due to resetting x. + x = x + 1; + } while (x < 10); + assert(x < 14); + } +} +// ---- +// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (179-193): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol new file mode 100644 index 00000000..33e598b6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + do { + // Overflows due to resetting x. + x = x + 1; + } while (x < 1000); + // The assertion is true but we can't infer so + // because x is touched in the loop. + assert(x > 0); + } +} +// ---- +// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (269-282): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol new file mode 100644 index 00000000..3858403a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + for(uint i = 0; i < 10; ++i) { + // Overflows due to resetting x. + x = x + 1; + } + assert(x < 14); + } +} +// ---- +// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (189-203): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol new file mode 100644 index 00000000..7d7b7015 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + for(uint i = 0; i < 10; ++i) { + // Overflows due to resetting x. + x = x + 1; + } + // The assertion is true but x is touched and reset. + assert(x > 0); + } +} +// ---- +// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (244-257): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol index 2c84960f..eb62d36e 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (167-181): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol index 90c4c328..b0c3cae4 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -5,8 +5,9 @@ contract C { for (y = 2; x < 10; ) { y = 3; } - assert(y == 2); + // False positive due to resetting y. + assert(y < 4); } } // ---- -// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (213-226): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol new file mode 100644 index 00000000..21e6c91e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (; x == 2;) {} + assert(x == 2); + } +} +// ---- +// Warning: (122-128): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol new file mode 100644 index 00000000..6184c441 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + uint y; + for (; x == 2;) { + y = 7; + } + assert(x == 2); + } +} +// ---- +// Warning: (138-144): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol new file mode 100644 index 00000000..eec59ded --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + uint y; + // The loop condition is always true, + // but since x is touched in the body + // we can't infer that. + for (; x == 2;) { + x = 2; + } + // False positive due to resetting x. + assert(x == 2); + } +} +// ---- +// Warning: (115-121): Unused local variable. +// Warning: (356-370): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol new file mode 100644 index 00000000..f367d8d9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (; x > 2;) {} + assert(x == 2); + } +} +// ---- +// Warning: (122-127): For loop condition is always false. diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol new file mode 100644 index 00000000..871ed929 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) + x = x + 1; + else + x = 0; + } + assert(x > 0); + } +} +// ---- +// Warning: (177-190): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol new file mode 100644 index 00000000..6964f7c8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + while (x < 10) { + x = x + 1; + } + assert(x < 14); + } +} +// ---- +// Warning: (139-153): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol new file mode 100644 index 00000000..4c52287d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + if (x > 10) + x = 2; + else + x = 10; + } + assert(x == 2); + } +} +// ---- +// Warning: (158-172): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol index 074be86f..9b5d04c3 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol @@ -4,10 +4,10 @@ contract C { function f(uint x) public pure { x = 2; while (x > 1) { - x = 2; + x = 1; } assert(x == 2); } } // ---- -// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (194-208): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol index a37df888..f3634edb 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol @@ -8,4 +8,4 @@ contract C { } } // ---- -// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (187-201): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol index f71da865..5a3aee9e 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol @@ -8,4 +8,4 @@ contract C { } } // ---- -// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (199-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol index 41559c99..6c81e36f 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (216-230): Assertion violation happens here |