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] Support modifiers

Browse Source
This commit is contained in:
Leonardo Alt
2019-03-20 11:32:20 +01:00
parent 556d11dae0
commit 9659f40c8d
17 changed files with 374 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+80 -7
View File
@@ -93,14 +93,20 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
assignment(_varDecl, *_varDecl.value(), _varDecl.location());
}
bool SMTChecker::visit(ModifierDefinition const&)
{
return false;
}
bool SMTChecker::visit(FunctionDefinition const& _function)
{
if (!_function.modifiers().empty() || _function.isConstructor())
if (_function.isConstructor())
m_errorReporter.warning(
_function.location(),
"Assertion checker does not yet support constructors and functions with modifiers."
"Assertion checker does not yet support constructors."
);
m_functionPath.push_back(&_function);
m_modifierDepthStack.push_back(-1);
// Not visited by a function call
if (isRootFunction())
{
@@ -116,7 +122,54 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_loopExecutionHappened = false;
m_arrayAssignmentHappened = false;
}
_function.parameterList().accept(*this);
if (_function.returnParameterList())
_function.returnParameterList()->accept(*this);
visitFunctionOrModifier();
return false;
}
void SMTChecker::visitFunctionOrModifier()
{
solAssert(!m_functionPath.empty(), "");
solAssert(!m_modifierDepthStack.empty(), "");
++m_modifierDepthStack.back();
FunctionDefinition const& function = *m_functionPath.back();
if (m_modifierDepthStack.back() == int(function.modifiers().size()))
{
if (function.isImplemented())
function.body().accept(*this);
}
else
{
solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), "");
ASTPointer<ModifierInvocation> const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()];
solAssert(modifierInvocation, "");
modifierInvocation->accept(*this);
auto const& modifierDef = dynamic_cast<ModifierDefinition const&>(
*modifierInvocation->name()->annotation().referencedDeclaration
);
vector<smt::Expression> modifierArgsExpr;
if (modifierInvocation->arguments())
for (auto arg: *modifierInvocation->arguments())
modifierArgsExpr.push_back(expr(*arg));
initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
pushCallStack(modifierInvocation.get());
modifierDef.body().accept(*this);
popCallStack();
}
--m_modifierDepthStack.back();
}
bool SMTChecker::visit(PlaceholderStatement const&)
{
solAssert(!m_functionPath.empty(), "");
ASTNode const* lastCall = popCallStack();
visitFunctionOrModifier();
pushCallStack(lastCall);
return true;
}
@@ -131,8 +184,11 @@ void SMTChecker::endVisit(FunctionDefinition const&)
{
checkUnderOverflow();
removeLocalVariables();
solAssert(m_callStack.empty(), "");
}
m_functionPath.pop_back();
solAssert(m_modifierDepthStack.back() == -1, "");
m_modifierDepthStack.pop_back();
}
bool SMTChecker::visit(IfStatement const& _node)
@@ -497,9 +553,9 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
visitGasLeft(_funCall);
break;
case FunctionType::Kind::Internal:
m_callStack.push_back(&_funCall);
pushCallStack(&_funCall);
inlineFunctionCall(_funCall);
m_callStack.pop_back();
popCallStack();
break;
case FunctionType::Kind::External:
resetStateVariables();
@@ -1261,7 +1317,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
// can't do anything.
}
else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
m_errorReporter.warning(_condition.location(), "Condition unreachable.");
m_errorReporter.warning(_condition.location(), "Condition unreachable.", currentCallStack());
else
{
string value;
@@ -1276,7 +1332,11 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
value = "false";
}
m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value));
m_errorReporter.warning(
_condition.location(),
boost::algorithm::replace_all_copy(_description, "$VALUE", value),
currentCallStack()
);
}
}
@@ -1316,7 +1376,7 @@ smt::CheckResult SMTChecker::checkSatisfiable()
return checkSatisfiableAndGenerateModel({}).first;
}
void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector<smt::Expression> const& _callArgs)
void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smt::Expression> const& _callArgs)
{
auto const& funParams = _function.parameters();
solAssert(funParams.size() == _callArgs.size(), "");
@@ -1564,6 +1624,19 @@ SecondarySourceLocation SMTChecker::currentCallStack()
return callStackLocation;
}
ASTNode const* SMTChecker::popCallStack()
{
solAssert(!m_callStack.empty(), "");
ASTNode const* lastCalled = m_callStack.back();
m_callStack.pop_back();
return lastCalled;
}
void SMTChecker::pushCallStack(ASTNode const* _node)
{
m_callStack.push_back(_node);
}
void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
{
m_interface->addAssertion(currentPathConditions() && _e);
libsolidity/formal/SMTChecker.h
+17 -1
View File
@@ -63,8 +63,10 @@ private:
bool visit(ContractDefinition const& _node) override;
void endVisit(ContractDefinition const& _node) override;
void endVisit(VariableDeclaration const& _node) override;
bool visit(ModifierDefinition const& _node) override;
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(WhileStatement const& _node) override;
bool visit(ForStatement const& _node) override;
@@ -100,6 +102,10 @@ private:
void abstractFunctionCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);
/// Encodes a modifier or function body according to the modifier
/// visit depth.
void visitFunctionOrModifier();
void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
void defineGlobalFunction(std::string const& _name, Expression const& _expr);
/// Handles the side effects of assignment
@@ -174,7 +180,7 @@ private:
smt::CheckResult checkSatisfiable();
void initializeLocalVariables(FunctionDefinition const& _function);
void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs);
void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
void resetVariable(VariableDeclaration const& _variable);
void resetStateVariables();
void resetStorageReferences();
@@ -231,6 +237,10 @@ private:
smt::Expression currentPathConditions();
/// Returns the current callstack. Used for models.
langutil::SecondarySourceLocation currentCallStack();
/// Copies and pops the last called node.
ASTNode const* popCallStack();
/// Adds @param _node to the callstack.
void pushCallStack(ASTNode const* _node);
/// 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
@@ -280,6 +290,12 @@ private:
bool visitedFunction(FunctionDefinition const* _funDef);
std::vector<OverflowTarget> m_overflowTargets;
/// Depth of visit to modifiers.
/// When m_modifierDepth == #modifiers the function can be visited
/// when placeholder is visited.
/// Needs to be a stack because of function calls.
std::vector<int> m_modifierDepthStack;
};
}