mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #8307 from ethereum/smt_split_1
[SMTChecker] Some refactoring
This commit is contained in:
commit
2cadf7ec5a
@ -441,26 +441,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
|
||||
}
|
||||
else
|
||||
{
|
||||
vector<smt::Expression> funArgs;
|
||||
Expression const* calledExpr = &_funCall.expression();
|
||||
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
|
||||
solAssert(funType, "");
|
||||
|
||||
auto const& functionParams = funDef->parameters();
|
||||
auto const& arguments = _funCall.arguments();
|
||||
unsigned firstParam = 0;
|
||||
if (funType->bound())
|
||||
{
|
||||
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
|
||||
solAssert(boundFunction, "");
|
||||
funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
|
||||
firstParam = 1;
|
||||
}
|
||||
|
||||
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
|
||||
for (unsigned i = 0; i < arguments.size(); ++i)
|
||||
funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
|
||||
initializeFunctionCallParameters(*funDef, funArgs);
|
||||
initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall));
|
||||
|
||||
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
|
||||
// is that there we don't have `_funCall`.
|
||||
@ -575,7 +556,7 @@ void BMC::checkVerificationTargets(smt::Expression const& _constraints)
|
||||
checkVerificationTarget(target, _constraints);
|
||||
}
|
||||
|
||||
void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints)
|
||||
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints)
|
||||
{
|
||||
switch (_target.type)
|
||||
{
|
||||
@ -606,7 +587,7 @@ void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression c
|
||||
}
|
||||
}
|
||||
|
||||
void BMC::checkConstantCondition(VerificationTarget& _target)
|
||||
void BMC::checkConstantCondition(BMCVerificationTarget& _target)
|
||||
{
|
||||
checkBooleanNotConstant(
|
||||
*_target.expression,
|
||||
@ -617,7 +598,7 @@ void BMC::checkConstantCondition(VerificationTarget& _target)
|
||||
);
|
||||
}
|
||||
|
||||
void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints)
|
||||
void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
|
||||
{
|
||||
solAssert(
|
||||
_target.type == VerificationTarget::Type::Underflow ||
|
||||
@ -637,7 +618,7 @@ void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _co
|
||||
);
|
||||
}
|
||||
|
||||
void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints)
|
||||
void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
|
||||
{
|
||||
solAssert(
|
||||
_target.type == VerificationTarget::Type::Overflow ||
|
||||
@ -657,7 +638,7 @@ void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _con
|
||||
);
|
||||
}
|
||||
|
||||
void BMC::checkDivByZero(VerificationTarget& _target)
|
||||
void BMC::checkDivByZero(BMCVerificationTarget& _target)
|
||||
{
|
||||
solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
|
||||
checkCondition(
|
||||
@ -671,7 +652,7 @@ void BMC::checkDivByZero(VerificationTarget& _target)
|
||||
);
|
||||
}
|
||||
|
||||
void BMC::checkBalance(VerificationTarget& _target)
|
||||
void BMC::checkBalance(BMCVerificationTarget& _target)
|
||||
{
|
||||
solAssert(_target.type == VerificationTarget::Type::Balance, "");
|
||||
checkCondition(
|
||||
@ -684,7 +665,7 @@ void BMC::checkBalance(VerificationTarget& _target)
|
||||
);
|
||||
}
|
||||
|
||||
void BMC::checkAssert(VerificationTarget& _target)
|
||||
void BMC::checkAssert(BMCVerificationTarget& _target)
|
||||
{
|
||||
solAssert(_target.type == VerificationTarget::Type::Assert, "");
|
||||
if (!m_safeAssertions.count(_target.expression))
|
||||
@ -703,10 +684,12 @@ void BMC::addVerificationTarget(
|
||||
Expression const* _expression
|
||||
)
|
||||
{
|
||||
VerificationTarget target{
|
||||
_type,
|
||||
_value,
|
||||
currentPathConditions() && m_context.assertions(),
|
||||
BMCVerificationTarget target{
|
||||
{
|
||||
_type,
|
||||
_value,
|
||||
currentPathConditions() && m_context.assertions()
|
||||
},
|
||||
_expression,
|
||||
m_callStack,
|
||||
modelExpressions()
|
||||
|
@ -117,24 +117,21 @@ private:
|
||||
|
||||
/// Verification targets.
|
||||
//@{
|
||||
struct VerificationTarget
|
||||
struct BMCVerificationTarget: 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 checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
|
||||
void checkConstantCondition(BMCVerificationTarget& _target);
|
||||
void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
|
||||
void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
|
||||
void checkDivByZero(BMCVerificationTarget& _target);
|
||||
void checkBalance(BMCVerificationTarget& _target);
|
||||
void checkAssert(BMCVerificationTarget& _target);
|
||||
void addVerificationTarget(
|
||||
VerificationTarget::Type _type,
|
||||
smt::Expression const& _value,
|
||||
@ -179,7 +176,7 @@ private:
|
||||
/// ErrorReporter that comes from CompilerStack.
|
||||
langutil::ErrorReporter& m_outerErrorReporter;
|
||||
|
||||
std::vector<VerificationTarget> m_verificationTargets;
|
||||
std::vector<BMCVerificationTarget> m_verificationTargets;
|
||||
|
||||
/// Assertions that are known to be safe.
|
||||
std::set<Expression const*> m_safeAssertions;
|
||||
|
@ -505,6 +505,23 @@ void CHC::eraseKnowledge()
|
||||
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
|
||||
}
|
||||
|
||||
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
|
||||
{
|
||||
SMTEncoder::clearIndices(_contract, _function);
|
||||
for (auto const* var: m_stateVariables)
|
||||
/// SSA index 0 is reserved for state variables at the beginning
|
||||
/// of the current transaction.
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
if (_function)
|
||||
{
|
||||
for (auto const& var: _function->parameters() + _function->returnParameters())
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
for (auto const& var: _function->localVariables())
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool CHC::shouldVisit(ContractDefinition const& _contract) const
|
||||
{
|
||||
if (
|
||||
|
@ -83,6 +83,7 @@ private:
|
||||
//@{
|
||||
void reset();
|
||||
void eraseKnowledge();
|
||||
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
|
||||
bool shouldVisit(ContractDefinition const& _contract) const;
|
||||
bool shouldVisit(FunctionDefinition const& _function) const;
|
||||
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
|
||||
|
@ -46,7 +46,7 @@ public:
|
||||
/// should be used, even if all are available. The default choice is to use all.
|
||||
ModelChecker(
|
||||
langutil::ErrorReporter& _errorReporter,
|
||||
std::map<h256, std::string> const& _smtlib2Responses,
|
||||
std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
|
||||
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
|
||||
smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All()
|
||||
);
|
||||
|
@ -1682,3 +1682,31 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
|
||||
else if (returnParams.size() == 1)
|
||||
defineExpr(_funCall, currentValue(*returnParams.front()));
|
||||
}
|
||||
|
||||
vector<smt::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
|
||||
{
|
||||
auto const* function = functionCallToDefinition(_funCall);
|
||||
solAssert(function, "");
|
||||
|
||||
vector<smt::Expression> args;
|
||||
Expression const* calledExpr = &_funCall.expression();
|
||||
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
|
||||
solAssert(funType, "");
|
||||
|
||||
auto const& functionParams = function->parameters();
|
||||
auto const& arguments = _funCall.arguments();
|
||||
unsigned firstParam = 0;
|
||||
if (funType->bound())
|
||||
{
|
||||
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
|
||||
solAssert(boundFunction, "");
|
||||
args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
|
||||
firstParam = 1;
|
||||
}
|
||||
|
||||
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
|
||||
for (unsigned i = 0; i < arguments.size(); ++i)
|
||||
args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
|
||||
|
||||
return args;
|
||||
}
|
||||
|
@ -217,7 +217,7 @@ protected:
|
||||
/// Resets the variable indices.
|
||||
void resetVariableIndices(VariableIndices const& _indices);
|
||||
/// Used when starting a new block.
|
||||
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
|
||||
virtual void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
|
||||
|
||||
|
||||
/// @returns variables that are touched in _node's subtree.
|
||||
@ -230,9 +230,21 @@ protected:
|
||||
/// and set them as the components of the symbolic tuple.
|
||||
void createReturnedExpressions(FunctionCall const& _funCall);
|
||||
|
||||
/// @returns the symbolic arguments for a function call,
|
||||
/// taking into account bound functions and
|
||||
/// type conversion.
|
||||
std::vector<smt::Expression> symbolicArguments(FunctionCall const& _funCall);
|
||||
|
||||
/// @returns a note to be added to warnings.
|
||||
std::string extraComment();
|
||||
|
||||
struct VerificationTarget
|
||||
{
|
||||
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
|
||||
smt::Expression value;
|
||||
smt::Expression constraints;
|
||||
};
|
||||
|
||||
smt::VariableUsage m_variableUsage;
|
||||
bool m_arrayAssignmentHappened = false;
|
||||
// True if the "No SMT solver available" warning was already created.
|
||||
|
Loading…
Reference in New Issue
Block a user