aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp283
1 files changed, 219 insertions, 64 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a7973852..1e27dc33 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -71,29 +71,41 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
_function.location(),
"Assertion checker does not yet support constructors and functions with modifiers."
);
- m_currentFunction = &_function;
- m_interface->reset();
- m_pathConditions.clear();
+ m_functionPath.push_back(&_function);
+ // Not visited by a function call
+ if (isRootFunction())
+ {
+ m_interface->reset();
+ m_pathConditions.clear();
+ m_expressions.clear();
+ resetStateVariables();
+ initializeLocalVariables(_function);
+ }
+
m_loopExecutionHappened = false;
- resetStateVariables();
- initializeLocalVariables(_function);
return true;
}
void SMTChecker::endVisit(FunctionDefinition const&)
{
- // TODO we could check for "reachability", i.e. satisfiability here.
- // We only handle local variables, so we clear at the beginning of the function.
- // If we add storage variables, those should be cleared differently.
- removeLocalVariables();
- m_currentFunction = nullptr;
+ // If _function was visited from a function call we don't remove
+ // the local variables just yet, since we might need them for
+ // future calls.
+ // Otherwise we remove any local variables from the context and
+ // keep the state variables.
+ if (isRootFunction())
+ removeLocalVariables();
+ m_functionPath.pop_back();
}
bool SMTChecker::visit(IfStatement const& _node)
{
_node.condition().accept(*this);
- checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
+ // We ignore called functions here because they have
+ // specific input values.
+ if (isRootFunction())
+ checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
@@ -122,12 +134,14 @@ bool SMTChecker::visit(WhileStatement const& _node)
visitBranch(_node.body());
// TODO the assertions generated in the body should still be active in the condition
_node.condition().accept(*this);
- checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
+ if (isRootFunction())
+ checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
}
else
{
_node.condition().accept(*this);
- checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+ if (isRootFunction())
+ checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
visitBranch(_node.body(), expr(_node.condition()));
}
@@ -158,7 +172,8 @@ bool SMTChecker::visit(ForStatement const& _node)
if (_node.condition())
{
_node.condition()->accept(*this);
- checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+ if (isRootFunction())
+ checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
}
VariableSequenceCounters sequenceCountersStart = m_variables;
@@ -198,10 +213,6 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
);
}
-void SMTChecker::endVisit(ExpressionStatement const&)
-{
-}
-
void SMTChecker::endVisit(Assignment const& _assignment)
{
if (_assignment.assignmentOperator() != Token::Value::Assign)
@@ -240,7 +251,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
if (_tuple.isInlineArray() || _tuple.components().size() != 1)
m_errorReporter.warning(
_tuple.location(),
- "Assertion checker does not yet implement tules and inline arrays."
+ "Assertion checker does not yet implement tuples and inline arrays."
);
else
defineExpr(_tuple, expr(*_tuple.components()[0]));
@@ -352,18 +363,95 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
if (funType.kind() == FunctionType::Kind::Assert)
- {
- solAssert(args.size() == 1, "");
- solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
- checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
- addPathImpliedExpression(expr(*args[0]));
- }
+ visitAssert(_funCall);
else if (funType.kind() == FunctionType::Kind::Require)
+ visitRequire(_funCall);
+ else if (funType.kind() == FunctionType::Kind::Internal)
+ inlineFunctionCall(_funCall);
+ else
{
- solAssert(args.size() == 1, "");
- solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+ m_errorReporter.warning(
+ _funCall.location(),
+ "Assertion checker does not yet implement this type of function call."
+ );
+ }
+}
+
+void SMTChecker::visitAssert(FunctionCall const& _funCall)
+{
+ auto const& args = _funCall.arguments();
+ solAssert(args.size() == 1, "");
+ solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+ checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
+ addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::visitRequire(FunctionCall const& _funCall)
+{
+ auto const& args = _funCall.arguments();
+ solAssert(args.size() == 1, "");
+ solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+ if (isRootFunction())
checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
- addPathImpliedExpression(expr(*args[0]));
+ addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
+{
+ FunctionDefinition const* _funDef = nullptr;
+ Expression const* _calledExpr = &_funCall.expression();
+
+ if (TupleExpression const* _fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
+ {
+ solAssert(_fun->components().size() == 1, "");
+ _calledExpr = _fun->components().at(0).get();
+ }
+
+ if (Identifier const* _fun = dynamic_cast<Identifier const*>(_calledExpr))
+ _funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+ else if (MemberAccess const* _fun = dynamic_cast<MemberAccess const*>(_calledExpr))
+ _funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+ else
+ {
+ m_errorReporter.warning(
+ _funCall.location(),
+ "Assertion checker does not yet implement this type of function call."
+ );
+ return;
+ }
+ solAssert(_funDef, "");
+
+ if (visitedFunction(_funDef))
+ m_errorReporter.warning(
+ _funCall.location(),
+ "Assertion checker does not support recursive function calls.",
+ SecondarySourceLocation().append("Starting from function:", _funDef->location())
+ );
+ else if (_funDef && _funDef->isImplemented())
+ {
+ vector<smt::Expression> funArgs;
+ for (auto arg: _funCall.arguments())
+ funArgs.push_back(expr(*arg));
+ initializeFunctionCallParameters(*_funDef, funArgs);
+ _funDef->accept(*this);
+ auto const& returnParams = _funDef->returnParameters();
+ if (_funDef->returnParameters().size())
+ {
+ if (returnParams.size() > 1)
+ m_errorReporter.warning(
+ _funCall.location(),
+ "Assertion checker does not yet support calls to functions that return more than one value."
+ );
+ else
+ defineExpr(_funCall, currentValue(*returnParams[0]));
+ }
+ }
+ else
+ {
+ m_errorReporter.warning(
+ _funCall.location(),
+ "Assertion checker does not support calls to functions without implementation."
+ );
}
}
@@ -388,6 +476,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
return;
+ createExpr(_identifier);
}
}
@@ -412,6 +501,21 @@ void SMTChecker::endVisit(Literal const& _literal)
);
}
+void SMTChecker::endVisit(Return const& _return)
+{
+ if (hasExpr(*_return.expression()))
+ {
+ auto returnParams = m_functionPath.back()->returnParameters();
+ if (returnParams.size() > 1)
+ m_errorReporter.warning(
+ _return.location(),
+ "Assertion checker does not yet support more than one return value."
+ );
+ else if (returnParams.size() == 1)
+ m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams[0]));
+ }
+}
+
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
{
switch (_op.getOperator())
@@ -578,7 +682,7 @@ void SMTChecker::checkCondition(
vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames;
- if (m_currentFunction)
+ if (m_functionPath.size())
{
if (_additionalValue)
{
@@ -607,7 +711,7 @@ void SMTChecker::checkCondition(
{
std::ostringstream message;
message << _description << " happens here";
- if (m_currentFunction)
+ if (m_functionPath.size())
{
std::ostringstream modelMessage;
modelMessage << " for:\n";
@@ -723,6 +827,30 @@ smt::CheckResult SMTChecker::checkSatisfiable()
return checkSatisfiableAndGenerateModel({}).first;
}
+void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector<smt::Expression> const& _callArgs)
+{
+ auto const& funParams = _function.parameters();
+ solAssert(funParams.size() == _callArgs.size(), "");
+ for (unsigned i = 0; i < funParams.size(); ++i)
+ if (createVariable(*funParams[i]))
+ m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i]));
+
+ for (auto const& variable: _function.localVariables())
+ if (createVariable(*variable))
+ {
+ newValue(*variable);
+ setZeroValue(*variable);
+ }
+
+ if (_function.returnParameterList())
+ for (auto const& retParam: _function.returnParameters())
+ if (createVariable(*retParam))
+ {
+ newValue(*retParam);
+ setZeroValue(*retParam);
+ }
+}
+
void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: _function.localVariables())
@@ -739,6 +867,17 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
setZeroValue(*retParam);
}
+void SMTChecker::removeLocalVariables()
+{
+ for (auto it = m_variables.begin(); it != m_variables.end(); )
+ {
+ if (it->first->isLocalVariable())
+ it = m_variables.erase(it);
+ else
+ ++it;
+ }
+}
+
void SMTChecker::resetStateVariables()
{
for (auto const& variable: m_variables)
@@ -779,7 +918,10 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
- if (SSAVariable::isSupportedType(_varDecl.type()->category()))
+ // This might be the case for multiple calls to the same function.
+ if (hasVariable(_varDecl))
+ return true;
+ else if (SSAVariable::isSupportedType(_varDecl.type()->category()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
@@ -838,40 +980,54 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
smt::Expression SMTChecker::expr(Expression const& _e)
{
- if (!m_expressions.count(&_e))
+ if (!hasExpr(_e))
{
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
}
- return m_expressions.at(&_e);
+ return prev(m_expressions.upper_bound(&_e))->second;
+}
+
+bool SMTChecker::hasExpr(Expression const& _e) const
+{
+ return m_expressions.count(&_e);
+}
+
+bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
+{
+ return m_variables.count(&_var);
}
void SMTChecker::createExpr(Expression const& _e)
{
- if (m_expressions.count(&_e))
- m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
- else
+ solAssert(_e.annotation().type, "");
+ string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e));
+ switch (_e.annotation().type->category())
{
- solAssert(_e.annotation().type, "");
- switch (_e.annotation().type->category())
- {
- case Type::Category::RationalNumber:
- {
- if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
- solAssert(!rational->isFractional(), "");
- m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
- break;
- }
- case Type::Category::Address:
- case Type::Category::Integer:
- m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
- break;
- case Type::Category::Bool:
- m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
- break;
- default:
- solUnimplementedAssert(false, "Type not implemented.");
- }
+ case Type::Category::RationalNumber:
+ {
+ if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
+ solAssert(!rational->isFractional(), "");
+ m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+ break;
+ }
+ case Type::Category::Address:
+ case Type::Category::Integer:
+ m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+ break;
+ case Type::Category::Bool:
+ m_expressions.emplace(&_e, m_interface->newBool(exprSymbol));
+ break;
+ case Type::Category::Function:
+ // This should be replaced by a `non-deterministic` type in the future.
+ m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+ break;
+ default:
+ m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+ m_errorReporter.warning(
+ _e.location(),
+ "Assertion checker does not yet implement this type."
+ );
}
}
@@ -909,13 +1065,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
}
-void SMTChecker::removeLocalVariables()
+bool SMTChecker::isRootFunction()
{
- for (auto it = m_variables.begin(); it != m_variables.end(); )
- {
- if (it->first->isLocalVariable())
- it = m_variables.erase(it);
- else
- ++it;
- }
+ return m_functionPath.size() == 1;
+}
+
+bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
+{
+ return contains(m_functionPath, _funDef);
}