solidity/libsolidity/formal/BMC.h

190 lines
6.2 KiB
C++

/*
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/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <set>
#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,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
);
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
/// 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 true if _funCall should be inlined, otherwise false.
static bool shouldInlineFunctionCall(FunctionCall const& _funCall);
private:
/// AST visitors.
/// Only nodes that lead to verification targets being built
/// or checked are visited.
//@{
bool visit(ContractDefinition const& _node) override;
void endVisit(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();
//@}
std::unique_ptr<smt::SolverInterface> m_interface;
/// 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;
/// Assertions that are known to be safe.
std::set<Expression const*> m_safeAssertions;
};
}
}