aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp58
-rw-r--r--libsolidity/formal/SymbolicVariables.cpp26
-rw-r--r--libsolidity/formal/SymbolicVariables.h22
3 files changed, 64 insertions, 42 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index ebb09f0a..17dc11ac 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -24,6 +24,8 @@
#include <liblangutil/ErrorReporter.h>
+#include <libdevcore/StringUtils.h>
+
#include <boost/range/adaptor/map.hpp>
#include <boost/algorithm/string/replace.hpp>
@@ -136,13 +138,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 +167,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 +218,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;
}
@@ -271,14 +302,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _
checkCondition(
_value < minValue(_type),
_location,
- "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
+ "Underflow (resulting value less than " + formatNumberReadable(_type.minValue()) + ")",
"<result>",
&_value
);
checkCondition(
_value > maxValue(_type),
_location,
- "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
+ "Overflow (resulting value larger than " + formatNumberReadable(_type.maxValue()) + ")",
"<result>",
&_value
);
@@ -820,6 +851,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 +870,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.");
@@ -933,7 +965,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
try
{
// Parse and re-format nicely
- value = formatNumber(bigint(value));
+ value = formatNumberReadable(bigint(value));
}
catch (...) { }
}
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index efaeb97a..f7d2a119 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -37,16 +37,32 @@ SymbolicVariable::SymbolicVariable(
{
}
+smt::Expression SymbolicVariable::currentValue() const
+{
+ return valueAtIndex(m_ssa->index());
+}
+
string SymbolicVariable::currentName() const
{
return uniqueSymbol(m_ssa->index());
}
+smt::Expression SymbolicVariable::valueAtIndex(int _index) const
+{
+ return m_interface.newVariable(uniqueSymbol(_index), smtSort(*m_type));
+}
+
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
}
+smt::Expression SymbolicVariable::increaseIndex()
+{
+ ++(*m_ssa);
+ return currentValue();
+}
+
SymbolicBoolVariable::SymbolicBoolVariable(
TypePointer _type,
string const& _uniqueName,
@@ -57,11 +73,6 @@ SymbolicBoolVariable::SymbolicBoolVariable(
solAssert(m_type->category() == Type::Category::Bool, "");
}
-smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
-{
- return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
-}
-
SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type,
string const& _uniqueName,
@@ -72,11 +83,6 @@ SymbolicIntVariable::SymbolicIntVariable(
solAssert(isNumber(m_type->category()), "");
}
-smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
-{
- return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
-}
-
SymbolicAddressVariable::SymbolicAddressVariable(
string const& _uniqueName,
smt::SolverInterface& _interface
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index fcf32760..ef40944c 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -46,20 +46,10 @@ public:
virtual ~SymbolicVariable() = default;
- smt::Expression currentValue() const
- {
- return valueAtIndex(m_ssa->index());
- }
-
+ smt::Expression currentValue() const;
std::string currentName() const;
-
- virtual smt::Expression valueAtIndex(int _index) const = 0;
-
- smt::Expression increaseIndex()
- {
- ++(*m_ssa);
- return currentValue();
- }
+ virtual smt::Expression valueAtIndex(int _index) const;
+ smt::Expression increaseIndex();
unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); }
@@ -86,9 +76,6 @@ public:
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
-
-protected:
- smt::Expression valueAtIndex(int _index) const;
};
/**
@@ -102,9 +89,6 @@ public:
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
-
-protected:
- smt::Expression valueAtIndex(int _index) const;
};
/**
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-05 09:36:31 +0800