2 files changed, 88 insertions, 54 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 2d2f05ec..0dc6e642 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -45,12 +45,7 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
 void SMTChecker::analyze(SourceUnit const& _source)
 {
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
-	{
-		m_interface->reset();
-		m_currentSequenceCounter.clear();
-		m_nextFreeSequenceCounter.clear();
 		_source.accept(*this);
-	}
 }
 
 void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
@@ -75,20 +70,21 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			_function.location(),
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
-	// TODO actually we probably also have to reset all local variables and similar things.
 	m_currentFunction = &_function;
-	m_interface->push();
+	// We only handle local variables, so we clear at the beginning of the function.
+	// If we add storage variables, those should be cleared differently.
+	m_interface->reset();
+	m_currentSequenceCounter.clear();
+	m_nextFreeSequenceCounter.clear();
+	m_conditionalExecutionHappened = false;
 	return true;
 }
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
 	// TOOD we could check for "reachability", i.e. satisfiability here.
-	// We only handle local variables, so we clear everything.
+	// We only handle local variables, so we clear at the beginning of the function.
 	// If we add storage variables, those should be cleared differently.
-	m_currentSequenceCounter.clear();
-	m_nextFreeSequenceCounter.clear();
-	m_interface->pop();
 	m_currentFunction = nullptr;
 }
 
@@ -98,55 +94,39 @@ bool SMTChecker::visit(IfStatement const& _node)
 
 	// TODO Check if condition is always true
 
-	auto countersAtStart = m_currentSequenceCounter;
-	m_interface->push();
-	m_interface->addAssertion(expr(_node.condition()));
-	_node.trueStatement().accept(*this);
-	auto countersAtEndOfTrue = m_currentSequenceCounter;
-	m_interface->pop();
-
-	decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+	auto touchedVariables = visitBranch(_node.trueStatement(), expr(_node.condition()));
 	if (_node.falseStatement())
-	{
-		m_currentSequenceCounter = countersAtStart;
-		m_interface->push();
-		m_interface->addAssertion(!expr(_node.condition()));
-		_node.falseStatement()->accept(*this);
-		countersAtEndOfFalse = m_currentSequenceCounter;
-		m_interface->pop();
-	}
-	else
-		countersAtEndOfFalse = countersAtStart;
-
-	// Reset all values that have been touched.
+		touchedVariables += visitBranch(*_node.falseStatement(), !expr(_node.condition()));
 
-	// TODO this should use a previously generated side-effect structure
+	resetVariables(touchedVariables);
 
-	solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
-	for (auto const& declCounter: countersAtEndOfTrue)
-	{
-		solAssert(countersAtEndOfFalse.count(declCounter.first), "");
-		auto decl = declCounter.first;
-		int trueCounter = countersAtEndOfTrue.at(decl);
-		int falseCounter = countersAtEndOfFalse.at(decl);
-		if (trueCounter == falseCounter)
-			continue; // Was not modified
-		newValue(*decl);
-		setValue(*decl, 0);
-	}
 	return false;
 }
 
 bool SMTChecker::visit(WhileStatement const& _node)
 {
-	_node.condition().accept(*this);
+	// TODO Check if condition is always true
 
-	//m_interface->push();
-	//m_interface->addAssertion(expr(_node.condition()));
-	// TDOO clear knowledge (increment sequence numbers and add bounds assertions	) apart from assertions
+	// TODO Weird side effects like
+	// uint x = 1;
+	// while (x ++ > 0) { assert(x == 2); }
+	// solution: clear variables first, then execute and assert condition, then executed body.
+	if (_node.isDoWhile())
+	{
+		auto touchedVariables = visitBranch(_node.body());
+		// TODO what about the side-effects of this?
+		// If we have a "break", this might never be executed.
+		_node.condition().accept(*this);
+		resetVariables(touchedVariables);
+	}
+	else
+	{
+		_node.condition().accept(*this);
+		auto touchedVariables = visitBranch(_node.body(), expr(_node.condition()));
+		resetVariables(touchedVariables);
+	}
 
-	// TODO combine similar to if
-	return true;
+	return false;
 }
 
 void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
@@ -386,6 +366,7 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	solAssert(_op.annotation().commonType, "");
 	if (_op.annotation().commonType->category() == Type::Category::Bool)
 	{
+		// @TODO check that both of them are not constant
 		if (_op.getOperator() == Token::And)
 			m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		else
@@ -395,7 +376,37 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 		m_errorReporter.warning(
 			_op.location(),
 			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
-		);
+					);
+}
+
+set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+{
+	return visitBranch(_statement, &_condition);
+}
+
+set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+{
+	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+
+	m_interface->push();
+	if (_condition)
+		m_interface->addAssertion(*_condition);
+	_statement.accept(*this);
+	m_interface->pop();
+
+	m_conditionalExecutionHappened = true;
+
+	set<Declaration const*> touched;
+	for (auto const& seq: m_currentSequenceCounter)
+	{
+		if (!sequenceCountersStart.count(seq.first))
+			touched.insert(seq.first);
+		else if (sequenceCountersStart[seq.first] != seq.second)
+			touched.insert(seq.first);
+	}
+	m_currentSequenceCounter = sequenceCountersStart;
+
+	return touched;
 }
 
 void SMTChecker::checkCondition(
@@ -446,6 +457,11 @@ void SMTChecker::checkCondition(
 		return;
 	}
 
+	string conditionalComment;
+	if (m_conditionalExecutionHappened)
+		conditionalComment =
+			"\nNote that some information is erased after conditional execution of parts of the code.\n"
+			"You can re-introduce information using require().";
 	switch (result)
 	{
 	case smt::CheckResult::SATISFIABLE:
@@ -471,13 +487,13 @@ void SMTChecker::checkCondition(
 		}
 		else
 			message << ".";
-		m_errorReporter.warning(_location, message.str());
+		m_errorReporter.warning(_location, message.str() + conditionalComment);
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
 		break;
 	case smt::CheckResult::UNKNOWN:
-		m_errorReporter.warning(_location, _description + " might happen here.");
+		m_errorReporter.warning(_location, _description + " might happen here." + conditionalComment);
 		break;
 	case smt::CheckResult::ERROR:
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
@@ -488,6 +504,15 @@ void SMTChecker::checkCondition(
 	m_interface->pop();
 }
 
+void SMTChecker::resetVariables(set<Declaration const*> _variables)
+{
+	for (auto const* decl: _variables)
+	{
+		newValue(*decl);
+		setValue(*decl, false);
+	}
+}
+
 void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
@@ -535,7 +560,6 @@ smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _seque
 
 smt::Expression SMTChecker::newValue(Declaration const& _decl)
 {
-	solAssert(m_currentSequenceCounter.count(&_decl), "");
 	solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
 	m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
 	return currentValue(_decl);
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index faaac639..6575dc1b 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -61,6 +61,12 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	// Visits the branch given by the statement, pushes and pops the SMT checker.
+	// @returns the set of touched declarations
+	// @param _condition if present, asserts that this condition is true within the branch.
+	std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression _condition);
+
 	void checkCondition(
 		smt::Expression _condition,
 		SourceLocation const& _location,
@@ -69,6 +75,7 @@ private:
 		smt::Expression* _additionalValue = nullptr
 	);
 
+	void resetVariables(std::set<Declaration const*> _variables);
 	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
 
 	static std::string uniqueSymbol(Declaration const& _decl);
@@ -93,6 +100,8 @@ private:
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);
 
+	using VariableSequenceCounters = std::map<Declaration const*, int>;
+
 	/// Returns the expression corresponding to the AST node. Creates a new expression
 	/// if it does not exist yet.
 	smt::Expression expr(Expression const& _e);
@@ -101,6 +110,7 @@ private:
 	smt::Expression var(Declaration const& _decl);
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
+	bool m_conditionalExecutionHappened = false;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_expressions;