Merge pull request #3304 from leonardoalt/smt_checker

[SMTChecker] Keep track of current path conditions

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]));
+		addPathImpliedExpression(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]));
+		addPathImpliedExpression(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);
+	addPathConjoinedExpression(_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));
+	addPathConjoinedExpression(expr(_condition));
 	auto positiveResult = checkSatisifable();
 	m_interface->pop();
 
 	m_interface->push();
-	m_interface->addAssertion(!expr(_condition));
+	addPathConjoinedExpression(!expr(_condition));
 	auto negatedResult = checkSatisifable();
 	m_interface->pop();
 
@@ -828,3 +829,31 @@ 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();
+}
+
+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));
+}

libsolidity/formal/SMTChecker.h

@@ -26,6 +26,7 @@
 
 #include <map>
 #include <string>
+#include <vector>
 
 namespace dev
 {
@@ -145,6 +146,17 @@ 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();
+	/// 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<VariableUsage> m_variableUsage;
 	bool m_conditionalExecutionHappened = false;
@@ -152,6 +164,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;

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);