cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #7001 from ethereum/smt_refactor_files

Browse Source 
[SMTChecker] Split SMTChecker file into different components
This commit is contained in:
Leonardo 2019-07-01 15:50:22 +02:00 committed by GitHub
commit ccc7e30961
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 1319 additions and 920 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/CMakeLists.txt
View File

@ -75,10 +75,14 @@ set(sources
codegen/ir/IRGenerationContext.h
codegen/ir/IRLValue.cpp
codegen/ir/IRLValue.h
formal/BMC.cpp
formal/BMC.h
formal/EncodingContext.cpp
formal/EncodingContext.h
formal/SMTChecker.cpp
formal/SMTChecker.h
formal/ModelChecker.cpp
formal/ModelChecker.h
formal/SMTEncoder.cpp
formal/SMTEncoder.h
formal/SMTLib2Interface.cpp
formal/SMTLib2Interface.h
formal/SMTPortfolio.cpp

888
libsolidity/formal/BMC.cpp Normal file
View File

@ -0,0 +1,888 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <boost/algorithm/string/replace.hpp>
using namespace std;
using namespace dev;
using namespace langutil;
using namespace dev::solidity;
BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
SMTEncoder(_context, _smtlib2Responses),
m_outerErrorReporter(_errorReporter)
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
"SMT-LIB2 query responses were given in the auxiliary input, "
"but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
"These responses will be ignored."
"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
);
#endif
}
void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
m_scanner = _scanner;
_source.accept(*this);
solAssert(m_interface->solvers() > 0, "");
// If this check is true, Z3 and CVC4 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver.
if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
{
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
SourceLocation(),
"BMC analysis was not possible since no integrated SMT solver (Z3 or CVC4) was found."
);
}
}
else
m_outerErrorReporter.append(m_errorReporter.errors());
m_errorReporter.clear();
}
FunctionDefinition const* BMC::inlinedFunctionCallToDefinition(FunctionCall const& _funCall)
{
if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
return nullptr;
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (funType.kind() == FunctionType::Kind::External)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
auto identifier = memberAccess ?
dynamic_cast<Identifier const*>(&memberAccess->expression()) :
nullptr;
if (!(
identifier &&
identifier->name() == "this" &&
identifier->annotation().referencedDeclaration &&
dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
))
return nullptr;
}
else if (funType.kind() != FunctionType::Kind::Internal)
return nullptr;
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().front().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);
if (funDef && funDef->isImplemented())
return funDef;
return nullptr;
}
/// AST visitors.
bool BMC::visit(ContractDefinition const& _contract)
{
SMTEncoder::visit(_contract);
/// Check targets created by state variable initialization.
smt::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
return true;
}
bool BMC::visit(FunctionDefinition const& _function)
{
if (m_callStack.empty())
reset();
/// Already visits the children.
SMTEncoder::visit(_function);
return false;
}
void BMC::endVisit(FunctionDefinition const& _function)
{
if (isRootFunction())
{
smt::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
}
SMTEncoder::endVisit(_function);
}
bool BMC::visit(IfStatement const& _node)
{
// This check needs to be done in its own context otherwise
// constraints from the If body might influence it.
m_context.pushSolver();
_node.condition().accept(*this);
// We ignore called functions here because they have
// specific input values.
if (isRootFunction())
addVerificationTarget(
VerificationTarget::Type::ConstantCondition,
expr(_node.condition()),
&_node.condition()
);
m_context.popSolver();
SMTEncoder::visit(_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 BMC::visit(WhileStatement const& _node)
{
auto indicesBeforeLoop = copyVariableIndices();
auto touchedVars = touchedVariables(_node);
m_context.resetVariables(touchedVars);
decltype(indicesBeforeLoop) indicesAfterLoop;
if (_node.isDoWhile())
{
indicesAfterLoop = visitBranch(&_node.body());
// TODO the assertions generated in the body should still be active in the condition
_node.condition().accept(*this);
if (isRootFunction())
addVerificationTarget(
VerificationTarget::Type::ConstantCondition,
expr(_node.condition()),
&_node.condition()
);
}
else
{
_node.condition().accept(*this);
if (isRootFunction())
addVerificationTarget(
VerificationTarget::Type::ConstantCondition,
expr(_node.condition()),
&_node.condition()
);
indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
}
// 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(touchedVars, expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
m_loopExecutionHappened = true;
return false;
}
// Here we consider the execution of two branches similar to WhileStatement.
bool BMC::visit(ForStatement const& _node)
{
if (_node.initializationExpression())
_node.initializationExpression()->accept(*this);
auto indicesBeforeLoop = copyVariableIndices();
// Do not reset the init expression part.
auto touchedVars = touchedVariables(_node.body());
if (_node.condition())
touchedVars += touchedVariables(*_node.condition());
if (_node.loopExpression())
touchedVars += touchedVariables(*_node.loopExpression());
m_context.resetVariables(touchedVars);
if (_node.condition())
{
_node.condition()->accept(*this);
if (isRootFunction())
addVerificationTarget(
VerificationTarget::Type::ConstantCondition,
expr(*_node.condition()),
_node.condition()
);
}
m_context.pushSolver();
if (_node.condition())
m_context.addAssertion(expr(*_node.condition()));
_node.body().accept(*this);
if (_node.loopExpression())
_node.loopExpression()->accept(*this);
m_context.popSolver();
auto indicesAfterLoop = copyVariableIndices();
// We reset the execution to before the loop
// and visit the condition.
resetVariableIndices(indicesBeforeLoop);
if (_node.condition())
_node.condition()->accept(*this);
auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true);
mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices());
m_loopExecutionHappened = true;
return false;
}
void BMC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);
if (_op.annotation().type->category() == Type::Category::RationalNumber)
return;
switch (_op.getOperator())
{
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
case Token::Sub: // -
if (_op.annotation().type->category() == Type::Category::Integer)
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
default:
break;
}
}
void BMC::endVisit(FunctionCall const& _funCall)
{
solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
{
SMTEncoder::endVisit(_funCall);
return;
}
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
switch (funType.kind())
{
case FunctionType::Kind::Assert:
visitAssert(_funCall);
SMTEncoder::endVisit(_funCall);
break;
case FunctionType::Kind::Require:
visitRequire(_funCall);
SMTEncoder::endVisit(_funCall);
break;
case FunctionType::Kind::Internal:
case FunctionType::Kind::External:
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::Creation:
SMTEncoder::endVisit(_funCall);
internalOrExternalFunctionCall(_funCall);
break;
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160:
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod:
SMTEncoder::endVisit(_funCall);
abstractFunctionCall(_funCall);
break;
case FunctionType::Kind::Send:
case FunctionType::Kind::Transfer:
{
SMTEncoder::endVisit(_funCall);
auto value = _funCall.arguments().front();
solAssert(value, "");
smt::Expression thisBalance = m_context.balance();
addVerificationTarget(
VerificationTarget::Type::Balance,
thisBalance < expr(*value),
&_funCall
);
break;
}
default:
SMTEncoder::endVisit(_funCall);
break;
}
}
/// Visitor helpers.
void BMC::visitAssert(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
addVerificationTarget(
VerificationTarget::Type::Assert,
expr(*args.front()),
&_funCall
);
}
void BMC::visitRequire(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
if (isRootFunction())
addVerificationTarget(
VerificationTarget::Type::ConstantCondition,
expr(*args.front()),
args.front().get()
);
}
void BMC::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* funDef = inlinedFunctionCallToDefinition(_funCall);
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
{
vector<smt::Expression> funArgs;
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, "");
funArgs.push_back(expr(boundFunction->expression()));
}
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
initializeFunctionCallParameters(*funDef, funArgs);
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`.
pushCallStack({funDef, &_funCall});
// If an internal function is called to initialize
// a state variable.
if (m_callStack.empty())
initFunction(*funDef);
funDef->accept(*this);
auto const& returnParams = funDef->returnParameters();
if (returnParams.size() > 1)
{
vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto param: returnParams)
{
solAssert(m_context.variable(*param), "");
components.push_back(m_context.variable(*param));
}
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, "");
symbTuple->setComponents(move(components));
}
else if (returnParams.size() == 1)
defineExpr(_funCall, currentValue(*returnParams.front()));
}
}
void BMC::abstractFunctionCall(FunctionCall const& _funCall)
{
vector<smt::Expression> smtArguments;
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_context.solver());
}
void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
{
auto funDef = inlinedFunctionCallToDefinition(_funCall);
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (funDef)
inlineFunctionCall(_funCall);
else if (funType.kind() == FunctionType::Kind::Internal)
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this type of function call."
);
else
{
m_externalFunctionCallHappened = true;
resetStateVariables();
resetStorageReferences();
}
}
pair<smt::Expression, smt::Expression> BMC::arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
TypePointer const& _commonType,
Expression const& _expression
)
{
if (_op == Token::Div || _op == Token::Mod)
addVerificationTarget(
VerificationTarget::Type::DivByZero,
_right,
&_expression
);
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
values.second,
&_expression
);
return values;
}
void BMC::resetStorageReferences()
{
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
}
void BMC::reset()
{
m_externalFunctionCallHappened = false;
m_loopExecutionHappened = false;
}
pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
{
vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames;
for (auto const& var: m_context.variables())
if (var.first->type()->isValueType())
{
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
for (auto const& var: m_context.globalSymbols())
{
auto const& type = var.second->type();
if (
type->isValueType() &&
smt::smtKind(type->category()) != smt::Kind::Function
)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
}
}
for (auto const& uf: m_uninterpretedTerms)
if (uf->annotation().type->isValueType())
{
expressionsToEvaluate.emplace_back(expr(*uf));
expressionNames.push_back(m_scanner->sourceAt(uf->location()));
}
return {expressionsToEvaluate, expressionNames};
}
/// Verification targets.
void BMC::checkVerificationTargets(smt::Expression const& _constraints)
{
for (auto& target: m_verificationTargets)
checkVerificationTarget(target, _constraints);
}
void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints)
{
switch (_target.type)
{
case VerificationTarget::Type::ConstantCondition:
checkConstantCondition(_target);
break;
case VerificationTarget::Type::Underflow:
checkUnderflow(_target, _constraints);
break;
case VerificationTarget::Type::Overflow:
checkOverflow(_target, _constraints);
break;
case VerificationTarget::Type::UnderOverflow:
checkUnderflow(_target, _constraints);
checkOverflow(_target, _constraints);
break;
case VerificationTarget::Type::DivByZero:
checkDivByZero(_target);
break;
case VerificationTarget::Type::Balance:
checkBalance(_target);
break;
case VerificationTarget::Type::Assert:
checkAssert(_target);
break;
default:
solAssert(false, "");
}
}
void BMC::checkConstantCondition(VerificationTarget& _target)
{
checkBooleanNotConstant(
*_target.expression,
_target.constraints,
_target.value,
_target.callStack,
"Condition is always $VALUE."
);
}
void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Underflow ||
_target.type == VerificationTarget::Type::UnderOverflow,
""
);
auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
solAssert(intType, "");
checkCondition(
_target.constraints && _constraints && _target.value < smt::minValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
"<result>",
&_target.value
);
}
void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Overflow ||
_target.type == VerificationTarget::Type::UnderOverflow,
""
);
auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
solAssert(intType, "");
checkCondition(
_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
"<result>",
&_target.value
);
}
void BMC::checkDivByZero(VerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
checkCondition(
_target.constraints && (_target.value == 0),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
"Division by zero",
"<result>",
&_target.value
);
}
void BMC::checkBalance(VerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::Balance, "");
checkCondition(
_target.constraints && _target.value,
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
"Insufficient funds",
"address(this).balance"
);
}
void BMC::checkAssert(VerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::Assert, "");
checkCondition(
_target.constraints && !_target.value,
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
"Assertion violation"
);
}
void BMC::addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
Expression const* _expression
)
{
VerificationTarget target{
_type,
_value,
currentPathConditions() && m_context.assertions(),
_expression,
m_callStack,
modelExpressions()
};
if (_type == VerificationTarget::Type::ConstantCondition)
checkVerificationTarget(target);
else
m_verificationTargets.emplace_back(move(target));
}
/// Solving.
void BMC::checkCondition(
smt::Expression _condition,
vector<SMTEncoder::CallStackEntry> const& callStack,
pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
SourceLocation const& _location,
string const& _description,
string const& _additionalValueName,
smt::Expression const* _additionalValue
)
{
m_interface->push();
m_interface->addAssertion(_condition);
vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (callStack.size())
{
solAssert(m_scanner, "");
if (_additionalValue)
{
expressionsToEvaluate.emplace_back(*_additionalValue);
expressionNames.push_back(_additionalValueName);
}
}
smt::CheckResult result;
vector<string> values;
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
string extraComment = SMTEncoder::extraComment();
if (m_loopExecutionHappened)
extraComment +=
"\nNote that some information is erased after the execution of loops.\n"
"You can re-introduce information using require().";
if (m_externalFunctionCallHappened)
extraComment+=
"\nNote that external function calls are not inlined,"
" even if the source code of the function is available."
" This is due to the possibility that the actual called contract"
" has the same ABI but implements the function differently.";
SecondarySourceLocation secondaryLocation{};
secondaryLocation.append(extraComment, SourceLocation{});
switch (result)
{
case smt::CheckResult::SATISFIABLE:
{
std::ostringstream message;
message << _description << " happens here";
if (callStack.size())
{
std::ostringstream modelMessage;
modelMessage << " for:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(
_location,
message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(callStack))
.append(move(secondaryLocation))
);
}
else
{
message << ".";
m_errorReporter.warning(_location, message.str(), secondaryLocation);
}
break;
}
case smt::CheckResult::UNSATISFIABLE:
break;
case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(_location, _description + " might happen here.", secondaryLocation);
break;
case smt::CheckResult::CONFLICTING:
m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
break;
case smt::CheckResult::ERROR:
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
break;
}
m_interface->pop();
}
void BMC::checkBooleanNotConstant(
Expression const& _condition,
smt::Expression const& _constraints,
smt::Expression const& _value,
vector<SMTEncoder::CallStackEntry> const& _callStack,
string const& _description
)
{
// Do not check for const-ness if this is a constant.
if (dynamic_cast<Literal const*>(&_condition))
return;
m_interface->push();
m_interface->addAssertion(_constraints && _value);
auto positiveResult = checkSatisfiable();
m_interface->pop();
m_interface->push();
m_interface->addAssertion(_constraints && !_value);
auto negatedResult = checkSatisfiable();
m_interface->pop();
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
{
// everything fine.
}
else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
{
// can't do anything.
}
else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
m_errorReporter.warning(_condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
else
{
string value;
if (positiveResult == smt::CheckResult::SATISFIABLE)
{
solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
value = "true";
}
else
{
solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
value = "false";
}
m_errorReporter.warning(
_condition.location(),
boost::algorithm::replace_all_copy(_description, "$VALUE", value),
SMTEncoder::callStackMessage(_callStack)
);
}
}
pair<smt::CheckResult, vector<string>>
BMC::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
{
smt::CheckResult result;
vector<string> values;
try
{
tie(result, values) = m_interface->check(_expressionsToEvaluate);
}
catch (smt::SolverError const& _e)
{
string description("Error querying SMT solver");
if (_e.comment())
description += ": " + *_e.comment();
m_errorReporter.warning(description);
result = smt::CheckResult::ERROR;
}
for (string& value: values)
{
try
{
// Parse and re-format nicely
value = formatNumberReadable(bigint(value));
}
catch (...) { }
}
return make_pair(result, values);
}
smt::CheckResult BMC::checkSatisfiable()
{
return checkSatisfiableAndGenerateModel({}).first;
}

180
libsolidity/formal/BMC.h Normal file
View File

@ -0,0 +1,180 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
/**
* Class that implements an SMT-based Bounded Model Checker (BMC).
* Traverses the AST such that:
* - Loops are unrolled
* - Internal function calls are inlined
* Creates verification targets for:
* - Underflow/Overflow
* - Constant conditions
* - Assertions
*/
#pragma once
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Scanner.h>
#include <string>
#include <vector>
namespace langutil
{
class ErrorReporter;
struct SourceLocation;
}
namespace dev
{
namespace solidity
{
class BMC: public SMTEncoder
{
public:
BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
/// This is used if the SMT solver is not directly linked into this binary.
/// @returns a list of inputs to the SMT solver that were not part of the argument to
/// the constructor.
std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
/// @returns the FunctionDefinition of a called function if possible and should inline,
/// otherwise nullptr.
static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall);
std::shared_ptr<smt::SolverInterface> solver() { return m_interface; }
private:
/// AST visitors.
/// Only nodes that lead to verification targets being built
/// or checked are visited.
//@{
bool visit(ContractDefinition const& _node) override;
bool visit(FunctionDefinition const& _node) override;
void endVisit(FunctionDefinition const& _node) override;
bool visit(IfStatement const& _node) override;
bool visit(WhileStatement const& _node) override;
bool visit(ForStatement const& _node) override;
void endVisit(UnaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
//@}
/// Visitor helpers.
//@{
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
/// Creates an uninterpreted function call.
void abstractFunctionCall(FunctionCall const& _funCall);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
/// Creates underflow/overflow verification targets.
std::pair<smt::Expression, smt::Expression> arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
TypePointer const& _commonType,
Expression const& _expression
) override;
void resetStorageReferences();
void reset();
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions();
//@}
/// Verification targets.
//@{
struct VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
smt::Expression value;
smt::Expression constraints;
Expression const* expression;
std::vector<CallStackEntry> callStack;
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smt::Expression const& _constraints);
void checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
void checkConstantCondition(VerificationTarget& _target);
void checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkDivByZero(VerificationTarget& _target);
void checkBalance(VerificationTarget& _target);
void checkAssert(VerificationTarget& _target);
void addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
Expression const* _expression
);
//@}
/// Solver related.
//@{
/// Check that a condition can be satisfied.
void checkCondition(
smt::Expression _condition,
std::vector<CallStackEntry> const& callStack,
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
langutil::SourceLocation const& _location,
std::string const& _description,
std::string const& _additionalValueName = "",
smt::Expression const* _additionalValue = nullptr
);
/// Checks that a boolean condition is not constant. Do not warn if the expression
/// is a literal constant.
/// @param _description the warning string, $VALUE will be replaced by the constant value.
void checkBooleanNotConstant(
Expression const& _condition,
smt::Expression const& _constraints,
smt::Expression const& _value,
std::vector<CallStackEntry> const& _callStack,
std::string const& _description
);
std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
smt::CheckResult checkSatisfiable();
//@}
/// Flags used for better warning messages.
bool m_loopExecutionHappened = false;
bool m_externalFunctionCallHappened = false;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
std::vector<VerificationTarget> m_verificationTargets;
};
}
}

42
libsolidity/formal/ModelChecker.cpp Normal file
View File

@ -0,0 +1,42 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/ModelChecker.h>
using namespace std;
using namespace dev;
using namespace langutil;
using namespace dev::solidity;
ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_bmc(m_context, _errorReporter, _smtlib2Responses),
m_context(m_bmc.solver())
{
}
void ModelChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
{
if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return;
m_bmc.analyze(_source, _scanner);
}
vector<string> ModelChecker::unhandledQueries()
{
return m_bmc.unhandledQueries();
}

64
libsolidity/formal/ModelChecker.h Normal file
View File

@ -0,0 +1,64 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
/**
* Entry point to the model checking engines.
* The goal of this class is to make different
* engines share knowledge to boost their proving power.
*/
#pragma once
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Scanner.h>
namespace langutil
{
class ErrorReporter;
struct SourceLocation;
}
namespace dev
{
namespace solidity
{
class ModelChecker
{
public:
ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
/// This is used if the SMT solver is not directly linked into this binary.
/// @returns a list of inputs to the SMT solver that were not part of the argument to
/// the constructor.
std::vector<std::string> unhandledQueries();
private:
/// Bounded Model Checker engine.
BMC m_bmc;
/// Stores the context of the encoding.
smt::EncodingContext m_context;
};
}
}

921
libsolidity/formal/SMTChecker.cpp → libsolidity/formal/SMTEncoder.cpp
View File

File diff suppressed because it is too large Load Diff

115
libsolidity/formal/SMTChecker.h → libsolidity/formal/SMTEncoder.h
View File

@ -14,6 +14,11 @@
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
/**
* Encodes Solidity into SMT expressions without creating
* any verification targets.
* Also implements the SSA scheme for branches.
*/
#pragma once
@ -43,25 +48,15 @@ namespace dev
namespace solidity
{
class SMTChecker: private ASTConstVisitor
class SMTEncoder: public ASTConstVisitor
{
public:
SMTChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
SMTEncoder(smt::EncodingContext& _context, std::map<h256, std::string> const& _smtlib2Responses);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
/// This is used if the SMT solver is not directly linked into this binary.
/// @returns a list of inputs to the SMT solver that were not part of the argument to
/// the constructor.
std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
/// @returns the FunctionDefinition of a called function if possible and should inline,
/// otherwise nullptr.
static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall);
/// @returns the leftmost identifier in a multi-d IndexAccess.
static Expression const* leftmostBase(IndexAccess const& _indexAccess);
private:
protected:
// TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined
// TODO: or just force a certain order, but people might have a different idea about that.
@ -74,8 +69,8 @@ private:
void endVisit(FunctionDefinition const& _node) override;
bool visit(PlaceholderStatement const& _node) override;
bool visit(IfStatement const& _node) override;
bool visit(WhileStatement const& _node) override;
bool visit(ForStatement const& _node) override;
bool visit(WhileStatement const&) override { return false; }
bool visit(ForStatement const&) override { return false; }
void endVisit(VariableDeclarationStatement const& _node) override;
void endVisit(Assignment const& _node) override;
void endVisit(TupleExpression const& _node) override;
@ -95,10 +90,10 @@ private:
/// Symbolic _expr is the rational literal.
bool shortcutRationalNumber(Expression const& _expr);
void arithmeticOperation(BinaryOperation const& _op);
/// @returns _op(_left, _right).
/// @returns _op(_left, _right) with and without modular arithmetic.
/// Used by the function above, compound assignments and
/// unary increment/decrement.
smt::Expression arithmeticOperation(
virtual std::pair<smt::Expression, smt::Expression> arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
@ -108,18 +103,11 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void initFunction(FunctionDefinition const& _function);
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
void visitGasLeft(FunctionCall const& _funCall);
void visitTypeConversion(FunctionCall const& _funCall);
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
/// Creates an uninterpreted function call.
void abstractFunctionCall(FunctionCall const& _funCall);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);
/// Encodes a modifier or function body according to the modifier
@ -165,71 +153,9 @@ private:
using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
/// Verification targets.
//@{
struct VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
smt::Expression value;
smt::Expression constraints;
Expression const* expression;
std::vector<CallStackEntry> callStack;
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smt::Expression const& _constraints);
void checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
void checkConstantCondition(VerificationTarget& _target);
void checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkDivByZero(VerificationTarget& _target);
void checkBalance(VerificationTarget& _target);
void checkAssert(VerificationTarget& _target);
void addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
Expression const* _expression
);
//@}
/// Solver related.
//@{
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions();
/// Check that a condition can be satisfied.
void checkCondition(
smt::Expression const& _condition,
std::vector<CallStackEntry> const& callStack,
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
langutil::SourceLocation const& _location,
std::string const& _description,
std::string const& _additionalValueName = "",
smt::Expression const* _additionalValue = nullptr
);
/// Checks whether a Boolean condition is constant.
/// Do not warn if the expression is a literal constant.
/// @param _condition the Solidity expression, used to check whether it is a Literal and for location.
/// @param _constraints the program constraints, including control-flow.
/// @param _value the Boolean term to be checked.
/// @param _callStack the callStack to be shown with the model if applicable.
/// @param _description the warning string, $VALUE will be replaced by the constant value.
void checkBooleanNotConstant(
Expression const& _condition,
smt::Expression const& _constraints,
smt::Expression const& _value,
std::vector<CallStackEntry> const& _callStack,
std::string const& _description
);
std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
smt::CheckResult checkSatisfiable();
//@}
void initializeLocalVariables(FunctionDefinition const& _function);
void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
void resetStateVariables();
void resetStorageReferences();
/// @returns the type without storage pointer information if it has it.
TypePointer typeWithoutPointer(TypePointer const& _type);
@ -265,8 +191,6 @@ private:
CallStackEntry popCallStack();
/// Adds (_definition, _node) to the callstack.
void pushCallStack(CallStackEntry _entry);
/// Conjoin the current path conditions with the given parameter and add to the solver
void addPathConjoinedExpression(smt::Expression const& _e);
/// Add to the solver: the given expression implied by the current path conditions
void addPathImpliedExpression(smt::Expression const& _e);
@ -281,11 +205,12 @@ private:
/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
VariableDeclaration const* identifierToVariable(Expression const& _expr);
/// @returns a note to be added to warnings.
std::string extraComment();
std::shared_ptr<smt::SolverInterface> m_interface;
smt::VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false;
bool m_arrayAssignmentHappened = false;
bool m_externalFunctionCallHappened = false;
// True if the "No SMT solver available" warning was already created.
bool m_noSolverWarning = false;
@ -294,9 +219,7 @@ private:
/// Used to retrieve models.
std::set<Expression const*> m_uninterpretedTerms;
std::vector<smt::Expression> m_pathConditions;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_errorReporterReference;
/// Local SMTChecker ErrorReporter.
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.
langutil::ErrorReporter m_errorReporter;
@ -311,8 +234,6 @@ private:
/// Returns true if _funDef was already visited.
bool visitedFunction(FunctionDefinition const* _funDef);
std::vector<VerificationTarget> m_verificationTargets;
/// Depth of visit to modifiers.
/// When m_modifierDepth == #modifiers the function can be visited
/// when placeholder is visited.
@ -320,7 +241,7 @@ private:
std::vector<int> m_modifierDepthStack;
/// Stores the context of the encoding.
smt::EncodingContext m_context;
smt::EncodingContext& m_context;
};
}

8
libsolidity/formal/VariableUsage.cpp
View File

@ -17,7 +17,8 @@
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <algorithm>
@ -48,7 +49,7 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
{
/// identifier.annotation().lValueRequested == false, that's why we
/// need to check that before.
auto identifier = dynamic_cast<Identifier const*>(SMTChecker::leftmostBase(_indexAccess));
auto identifier = dynamic_cast<Identifier const*>(SMTEncoder::leftmostBase(_indexAccess));
if (identifier)
checkIdentifier(*identifier);
}
@ -56,7 +57,8 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
void VariableUsage::endVisit(FunctionCall const& _funCall)
{
if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall))
/// TODO this should run only in the BMC case, not for Horn.
if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall))
if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
funDef->accept(*this);
}

8
libsolidity/interface/CompilerStack.cpp
View File

@ -39,7 +39,7 @@
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/codegen/Compiler.h>
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/ABI.h>
#include <libsolidity/interface/Natspec.h>
#include <libsolidity/interface/GasEstimator.h>
@ -371,10 +371,10 @@ bool CompilerStack::analyze()
if (noErrors)
{
SMTChecker smtChecker(m_errorReporter, m_smtlib2Responses);
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast, source->scanner);
m_unhandledSMTLib2Queries += smtChecker.unhandledQueries();
modelChecker.analyze(*source->ast, source->scanner);
m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
}
}
catch(FatalError const&)

1
test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
View File

@ -58,3 +58,4 @@ contract MyConc{
// Warning: (834-839): Assertion checker does not yet support the type of this literal (literal_string "abc").
// Warning: (874-879): Underflow (resulting value less than 0) happens here.
// Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.

4
test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
View File

@ -8,8 +8,6 @@ contract C
require(x > 0);
_;
// Fails because of overflow behavior.
// Overflow is not reported because this assertion prevents
// it from reaching the end of the function.
assert(x > 1);
}
@ -19,4 +17,4 @@ contract C
}
}
// ----
// Warning: (245-258): Assertion violation happens here
// Warning: (136-149): Assertion violation happens here