aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--libsolidity/formal/SMTChecker.cpp50
-rw-r--r--test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol17
-rw-r--r--test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol19
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_1_fail.sol17
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol18
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_5.sol2
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_6.sol5
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol10
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol13
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol18
-rw-r--r--test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol10
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_1.sol17
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_1_fail.sol14
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_2_fail.sol15
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol4
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol2
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol2
-rw-r--r--test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol2
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