cerc-io/solidity
10
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] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions

Browse Source
This commit is contained in:
Leonardo Alt 2017-12-13 17:59:36 +01:00
parent 2af4d7c7dd
commit a1e296e392
2 changed files with 19 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsolidity/formal/SMTChecker.cpp
View File

@ -345,14 +345,14 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
solAssert(args.size() == 1, ""); solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0]))); addPathImpliedExpression(expr(*args[0]));
} }
else if (funType.kind() == FunctionType::Kind::Require) else if (funType.kind() == FunctionType::Kind::Require)
{ {
solAssert(args.size() == 1, ""); solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkBooleanNotConstant(*args[0], "Condition is always $VALUE."); checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0]))); addPathImpliedExpression(expr(*args[0]));
} }
} }
@ -534,7 +534,7 @@ void SMTChecker::checkCondition(
) )
{ {
m_interface->push(); m_interface->push();
m_interface->addAssertion(currentPathConditions() && _condition); addPathConjoinedExpression(_condition);
vector<smt::Expression> expressionsToEvaluate; vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames; vector<string> expressionNames;
@ -606,12 +606,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
return; return;
m_interface->push(); m_interface->push();
m_interface->addAssertion(currentPathConditions() && expr(_condition)); addPathConjoinedExpression(expr(_condition));
auto positiveResult = checkSatisifable(); auto positiveResult = checkSatisifable();
m_interface->pop(); m_interface->pop();
m_interface->push(); m_interface->push();
m_interface->addAssertion(currentPathConditions() && !expr(_condition)); addPathConjoinedExpression(!expr(_condition));
auto negatedResult = checkSatisifable(); auto negatedResult = checkSatisifable();
m_interface->pop(); m_interface->pop();
@ -847,3 +847,13 @@ smt::Expression SMTChecker::currentPathConditions()
return smt::Expression(true); return smt::Expression(true);
return m_pathConditions.back(); return m_pathConditions.back();
} }
void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
{
m_interface->addAssertion(currentPathConditions() && _e);
}
void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
{
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
}

4
libsolidity/formal/SMTChecker.h
View File

@ -152,6 +152,10 @@ private:
void popPathCondition(); void popPathCondition();
/// Returns the conjunction of all path conditions or True if empty /// Returns the conjunction of all path conditions or True if empty
smt::Expression currentPathConditions(); smt::Expression currentPathConditions();
/// 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);
std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage; std::shared_ptr<VariableUsage> m_variableUsage;