cerc-io/solidity
11
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

[SMTChecker] Keeping better track of path condition through branches with return statement in the BMC engine.

Browse Source
This commit is contained in:
Martin Blicha
2020-11-30 11:47:49 +01:00
parent 45307a24d6
commit cd06d68cbe
24 changed files with 1027 additions and 491 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+42 -3
View File
@@ -162,6 +162,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
m_pathConditions.clear();
}
SMTEncoder::endVisit(_function);
@@ -184,7 +185,26 @@ bool BMC::visit(IfStatement const& _node)
);
m_context.popSolver();
SMTEncoder::visit(_node);
_node.condition().accept(*this);
auto conditionExpr = expr(_node.condition());
// visit true branch
auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr);
auto touchedVars = touchedVariables(_node.trueStatement());
// visit false branch
decltype(indicesEndTrue) indicesEndFalse;
auto falseEndPathCondition = currentPathConditions() && !conditionExpr;
if (_node.falseStatement())
{
std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr);
touchedVars += touchedVariables(*_node.falseStatement());
}
else
indicesEndFalse = copyVariableIndices();
// merge the information from branches
setPathCondition(trueEndPathCondition || falseEndPathCondition);
mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
return false;
}
@@ -224,7 +244,7 @@ bool BMC::visit(WhileStatement const& _node)
decltype(indicesBeforeLoop) indicesAfterLoop;
if (_node.isDoWhile())
{
indicesAfterLoop = visitBranch(&_node.body());
indicesAfterLoop = visitBranch(&_node.body()).first;
// TODO the assertions generated in the body should still be active in the condition
_node.condition().accept(*this);
if (isRootFunction())
@@ -244,7 +264,7 @@ bool BMC::visit(WhileStatement const& _node)
&_node.condition()
);
indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition())).first;
}
// We reset the execution to before the loop
@@ -406,6 +426,12 @@ void BMC::endVisit(FunctionCall const& _funCall)
}
}
void BMC::endVisit(Return const& _return)
{
SMTEncoder::endVisit(_return);
setPathCondition(smtutil::Expression(false));
}
/// Visitor helpers.
void BMC::visitAssert(FunctionCall const& _funCall)
@@ -467,7 +493,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`.
pushCallStack({funDef, &_funCall});
pushPathCondition(currentPathConditions());
funDef->accept(*this);
popPathCondition();
}
createReturnedExpressions(_funCall);
@@ -968,3 +996,14 @@ smtutil::CheckResult BMC::checkSatisfiable()
return checkSatisfiableAndGenerateModel({}).first;
}
void BMC::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
{
auto oldVar = _symVar.currentValue();
auto newVar = _symVar.increaseIndex();
m_context.addAssertion(smtutil::Expression::ite(
currentPathConditions(),
newVar == _value,
newVar == oldVar
));
}
libsolidity/formal/BMC.h
+2
View File
@@ -90,6 +90,7 @@ private:
bool visit(ForStatement const& _node) override;
void endVisit(UnaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(Return const& _node) override;
//@}
/// Visitor helpers.
@@ -97,6 +98,7 @@ private:
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
void visitAddMulMod(FunctionCall const& _funCall) override;
void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value) override;
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
libsolidity/formal/SMTEncoder.cpp
+26 -27
View File
@@ -155,8 +155,10 @@ void SMTEncoder::visitFunctionOrModifier()
if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
{
pushPathCondition(currentPathConditions());
if (function.isImplemented())
function.body().accept(*this);
popPathCondition();
}
else
{
@@ -193,6 +195,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
initializeFunctionCallParameters(*_definition, args);
pushCallStack({_definition, _invocation});
pushPathCondition(currentPathConditions());
if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
{
if (modifier->isImplemented())
@@ -205,6 +208,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
function->accept(*this);
// Functions are popped from the callstack in endVisit(FunctionDefinition)
}
popPathCondition();
}
void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
@@ -288,26 +292,6 @@ bool SMTEncoder::visit(TryCatchClause const& _clause)
return false;
}
bool SMTEncoder::visit(IfStatement const& _node)
{
_node.condition().accept(*this);
auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
auto touchedVars = touchedVariables(_node.trueStatement());
decltype(indicesEndTrue) indicesEndFalse;
if (_node.falseStatement())
{
indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
touchedVars += touchedVariables(*_node.falseStatement());
}
else
indicesEndFalse = copyVariableIndices();
mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
return false;
}
void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
{
if (_varDecl.declarations().size() != 1)
@@ -598,10 +582,10 @@ bool SMTEncoder::visit(Conditional const& _op)
{
_op.condition().accept(*this);
auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition()));
auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
auto touchedVars = touchedVariables(_op.trueExpression());
auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition()));
auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
touchedVars += touchedVariables(_op.falseExpression());
mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
@@ -1754,13 +1738,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
_op.leftExpression().accept(*this);
if (_op.getOperator() == Token::And)
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
}
else
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
@@ -1974,22 +1958,29 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression
m_context.addAssertion(_symVar.increaseIndex() == _value);
}
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
ASTNode const* _statement,
smtutil::Expression _condition
)
{
return visitBranch(_statement, &_condition);
}
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
ASTNode const* _statement,
smtutil::Expression const* _condition
)
{
auto indicesBeforeBranch = copyVariableIndices();
if (_condition)
pushPathCondition(*_condition);
_statement->accept(*this);
auto pathConditionOnExit = currentPathConditions();
if (_condition)
popPathCondition();
auto indicesAfterBranch = copyVariableIndices();
resetVariableIndices(indicesBeforeBranch);
return indicesAfterBranch;
return {indicesAfterBranch, pathConditionOnExit};
}
void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
@@ -2245,6 +2236,14 @@ void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
m_pathConditions.push_back(currentPathConditions() && _e);
}
void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
{
if (m_pathConditions.empty())
m_pathConditions.push_back(_e);
else
m_pathConditions.back() = _e;
}
smtutil::Expression SMTEncoder::currentPathConditions()
{
if (m_pathConditions.empty())
libsolidity/formal/SMTEncoder.h
+8 -5
View File
@@ -89,7 +89,7 @@ protected:
bool visit(FunctionDefinition const& _node) override;
void endVisit(FunctionDefinition const& _node) override;
bool visit(PlaceholderStatement const& _node) override;
bool visit(IfStatement const& _node) override;
bool visit(IfStatement const&) override { return false; }
bool visit(WhileStatement const&) override { return false; }
bool visit(ForStatement const&) override { return false; }
void endVisit(VariableDeclarationStatement const& _node) override;
@@ -197,7 +197,7 @@ protected:
/// Handles the actual assertion of the new value to the encoding context.
/// Other assignment methods should use this one in the end.
void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
virtual void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
void assignment(VariableDeclaration const& _variable, Expression const& _value);
/// Handles assignments to variables of different types.
@@ -219,9 +219,10 @@ protected:
/// Visits the branch given by the statement, pushes and pops the current path conditions.
/// @param _condition if present, asserts that this condition is true within the branch.
/// @returns the variable indices after visiting the branch.
VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
/// @returns the variable indices after visiting the branch and the expression representing
/// the path condition at the end of the branch.
std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
@@ -263,6 +264,8 @@ protected:
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smtutil::Expression _value);
/// Overwrites the current path condition
void setPathCondition(smtutil::Expression const& _e);
/// Adds a new path condition
void pushPathCondition(smtutil::Expression const& _e);
/// Remove the last path condition