aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--libsolidity/formal/SMTChecker.cpp35
-rw-r--r--libsolidity/formal/SMTChecker.h9
-rw-r--r--libsolidity/formal/SolverInterface.h5
3 files changed, 41 insertions, 8 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a22e35d6..61cb110e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -71,6 +71,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_interface->reset();
m_currentSequenceCounter.clear();
m_nextFreeSequenceCounter.clear();
+ m_pathConditions.clear();
m_conditionalExecutionHappened = false;
initializeLocalVariables(_function);
return true;
@@ -344,14 +345,14 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
- m_interface->addAssertion(expr(*args[0]));
+ m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0])));
}
else if (funType.kind() == FunctionType::Kind::Require)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
- m_interface->addAssertion(expr(*args[0]));
+ m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0])));
}
}
@@ -514,11 +515,11 @@ void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const*
{
VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
- m_interface->push();
if (_condition)
- m_interface->addAssertion(*_condition);
+ pushPathCondition(*_condition);
_statement.accept(*this);
- m_interface->pop();
+ if (_condition)
+ popPathCondition();
m_conditionalExecutionHappened = true;
m_currentSequenceCounter = sequenceCountersStart;
@@ -533,7 +534,7 @@ void SMTChecker::checkCondition(
)
{
m_interface->push();
- m_interface->addAssertion(_condition);
+ m_interface->addAssertion(currentPathConditions() && _condition);
vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames;
@@ -605,12 +606,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
return;
m_interface->push();
- m_interface->addAssertion(expr(_condition));
+ m_interface->addAssertion(currentPathConditions() && expr(_condition));
auto positiveResult = checkSatisifable();
m_interface->pop();
m_interface->push();
- m_interface->addAssertion(!expr(_condition));
+ m_interface->addAssertion(currentPathConditions() && !expr(_condition));
auto negatedResult = checkSatisifable();
m_interface->pop();
@@ -828,3 +829,21 @@ smt::Expression SMTChecker::var(Declaration const& _decl)
solAssert(m_variables.count(&_decl), "");
return m_variables.at(&_decl);
}
+
+void SMTChecker::popPathCondition()
+{
+ solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
+ m_pathConditions.pop_back();
+}
+
+void SMTChecker::pushPathCondition(smt::Expression const& _e)
+{
+ m_pathConditions.push_back(currentPathConditions() && _e);
+}
+
+smt::Expression SMTChecker::currentPathConditions()
+{
+ if (m_pathConditions.size() == 0)
+ return smt::Expression(true);
+ return m_pathConditions.back();
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index e7481cca..7f990b97 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -26,6 +26,7 @@
#include <map>
#include <string>
+#include <vector>
namespace dev
{
@@ -145,6 +146,13 @@ private:
/// The function takes one argument which is the "sequence number".
smt::Expression var(Declaration const& _decl);
+ /// Adds a new path condition
+ void pushPathCondition(smt::Expression const& _e);
+ /// Remove the last path condition
+ void popPathCondition();
+ /// Returns the conjunction of all path conditions or True if empty
+ smt::Expression currentPathConditions();
+
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;
bool m_conditionalExecutionHappened = false;
@@ -152,6 +160,7 @@ private:
std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_expressions;
std::map<Declaration const*, smt::Expression> m_variables;
+ std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 74c993e8..88487310 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -72,6 +72,11 @@ public:
}, _trueValue.sort);
}
+ static Expression implies(Expression _a, Expression _b)
+ {
+ return !std::move(_a) || std::move(_b);
+ }
+
friend Expression operator!(Expression _a)
{
return Expression("not", std::move(_a), Sort::Bool);