Merge pull request #2993 from ethereum/trackVariables

SMT checker for various things

7 files changed, 771 insertions, 119 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 2d2f05ec..1050621e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -23,9 +23,12 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
 
+#include <libsolidity/formal/VariableUsage.h>
+
 #include <libsolidity/interface/ErrorReporter.h>
 
 #include <boost/range/adaptor/map.hpp>
+#include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
 using namespace dev;
@@ -44,28 +47,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
 
 void SMTChecker::analyze(SourceUnit const& _source)
 {
+	m_variableUsage = make_shared<VariableUsage>(_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)
 {
-	if (_varDecl.value())
-	{
-		m_errorReporter.warning(
-			_varDecl.location(),
-			"Assertion checker does not yet support this."
-		);
-	}
-	else if (_varDecl.isLocalOrReturn())
-		createVariable(_varDecl, true);
-	else if (_varDecl.isCallableParameter())
-		createVariable(_varDecl, false);
+	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
+		assignment(_varDecl, *_varDecl.value());
 }
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -75,20 +65,22 @@ 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;
+	initializeLocalVariables(_function);
 	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;
 }
 
@@ -96,57 +88,84 @@ bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
-	// 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();
+	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+	visitBranch(_node.trueStatement(), expr(_node.condition()));
+	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
 	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();
+		visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
-	else
-		countersAtEndOfFalse = countersAtStart;
 
-	// Reset all values that have been touched.
+	resetVariables(touchedVariables);
 
-	// TODO this should use a previously generated side-effect structure
+	return false;
+}
 
-	solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
-	for (auto const& declCounter: countersAtEndOfTrue)
+bool SMTChecker::visit(WhileStatement const& _node)
+{
+	auto touchedVariables = m_variableUsage->touchedVariables(_node);
+	resetVariables(touchedVariables);
+	if (_node.isDoWhile())
 	{
-		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);
+		visitBranch(_node.body());
+		// TODO the assertions generated in the body should still be active in the condition
+		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
+	else
+	{
+		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+
+		visitBranch(_node.body(), expr(_node.condition()));
+	}
+	resetVariables(touchedVariables);
+
 	return false;
 }
 
-bool SMTChecker::visit(WhileStatement const& _node)
+bool SMTChecker::visit(ForStatement const& _node)
 {
-	_node.condition().accept(*this);
+	if (_node.initializationExpression())
+		_node.initializationExpression()->accept(*this);
+
+	// Do not reset the init expression part.
+	auto touchedVariables =
+		m_variableUsage->touchedVariables(_node.body());
+	if (_node.condition())
+		touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
+	if (_node.loopExpression())
+		touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
+	// Remove duplicates
+	std::sort(touchedVariables.begin(), touchedVariables.end());
+	touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
+
+	resetVariables(touchedVariables);
+
+	if (_node.condition())
+	{
+		_node.condition()->accept(*this);
+		checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+	}
 
-	//m_interface->push();
-	//m_interface->addAssertion(expr(_node.condition()));
-	// TDOO clear knowledge (increment sequence numbers and add bounds assertions	) apart from assertions
+	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+	m_interface->push();
+	if (_node.condition())
+		m_interface->addAssertion(expr(*_node.condition()));
+	_node.body().accept(*this);
+	if (_node.loopExpression())
+		_node.loopExpression()->accept(*this);
 
-	// TODO combine similar to if
-	return true;
+	m_interface->pop();
+
+	m_conditionalExecutionHappened = true;
+	m_currentSequenceCounter = sequenceCountersStart;
+
+	resetVariables(touchedVariables);
+
+	return false;
 }
 
 void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
@@ -160,8 +179,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 	{
 		if (_varDecl.initialValue())
 			// TODO more checks?
-			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+			assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
 	}
 	else
 		m_errorReporter.warning(
@@ -190,9 +208,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 	{
 		Declaration const* decl = identifier->annotation().referencedDeclaration;
 		if (knownVariable(*decl))
-			// TODO more checks?
-			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
+			assignment(*decl, _assignment.rightHandSide());
 		else
 			m_errorReporter.warning(
 				_assignment.location(),
@@ -269,23 +285,17 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 {
 	Declaration const* decl = _identifier.annotation().referencedDeclaration;
 	solAssert(decl, "");
-	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	if (_identifier.annotation().lValueRequested)
 	{
-		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
-		return;
+		// Will be translated as part of the node that requested the lvalue.
 	}
+	else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
 		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
 			return;
-		// TODO for others, clear our knowledge about storage and memory
 	}
-	m_errorReporter.warning(
-		_identifier.location(),
-		"Assertion checker does not yet support the type of this expression (" +
-		_identifier.annotation().type->toString() +
-		")."
-	);
 }
 
 void SMTChecker::endVisit(Literal const& _literal)
@@ -298,10 +308,12 @@ void SMTChecker::endVisit(Literal const& _literal)
 
 		m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
 	}
+	else if (type.category() == Type::Category::Bool)
+		m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else
 		m_errorReporter.warning(
 			_literal.location(),
-			"Assertion checker does not yet support the type of this expression (" +
+			"Assertion checker does not yet support the type of this literal (" +
 			_literal.annotation().type->toString() +
 			")."
 		);
@@ -386,6 +398,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 +408,33 @@ 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"
-		);
+					);
+}
+
+void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
+{
+	// TODO more checks?
+	// TODO add restrictions about type (might be assignment from smaller type)
+	m_interface->addAssertion(newValue(_variable) == expr(_value));
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+{
+	visitBranch(_statement, &_condition);
+}
+
+void 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;
+	m_currentSequenceCounter = sequenceCountersStart;
 }
 
 void SMTChecker::checkCondition(
@@ -433,19 +472,13 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	try
-	{
-		tie(result, values) = m_interface->check(expressionsToEvaluate);
-	}
-	catch (smt::SolverError const& _e)
-	{
-		string description("Error querying SMT solver");
-		if (_e.comment())
-			description += ": " + *_e.comment();
-		m_errorReporter.warning(_location, description);
-		return;
-	}
+	tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
 
+	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:
@@ -457,27 +490,17 @@ void SMTChecker::checkCondition(
 			message << " for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			for (size_t i = 0; i < values.size(); ++i)
-			{
-				string formattedValue = values.at(i);
-				try
-				{
-					// Parse and re-format nicely
-					formattedValue = formatNumber(bigint(formattedValue));
-				}
-				catch (...) { }
-
-				message << "  " << expressionNames.at(i) << " = " << formattedValue << "\n";
-			}
+				message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
 		}
 		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,7 +511,110 @@ void SMTChecker::checkCondition(
 	m_interface->pop();
 }
 
-void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
+{
+	// Do not check for const-ness if this is a constant.
+	if (dynamic_cast<Literal const*>(&_condition))
+		return;
+
+	m_interface->push();
+	m_interface->addAssertion(expr(_condition));
+	auto positiveResult = checkSatisifable();
+	m_interface->pop();
+
+	m_interface->push();
+	m_interface->addAssertion(!expr(_condition));
+	auto negatedResult = checkSatisifable();
+	m_interface->pop();
+
+	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
+		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
+	{
+		// everything fine.
+	}
+	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
+		m_errorReporter.warning(_condition.location(), "Condition unreachable.");
+	else
+	{
+		string value;
+		if (positiveResult == smt::CheckResult::SATISFIABLE)
+		{
+			solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
+			value = "true";
+		}
+		else
+		{
+			solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
+			solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
+			value = "false";
+		}
+		m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value));
+	}
+}
+
+pair<smt::CheckResult, vector<string>>
+SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+{
+	smt::CheckResult result;
+	vector<string> values;
+	try
+	{
+		tie(result, values) = m_interface->check(_expressionsToEvaluate);
+	}
+	catch (smt::SolverError const& _e)
+	{
+		string description("Error querying SMT solver");
+		if (_e.comment())
+			description += ": " + *_e.comment();
+		m_errorReporter.warning(description);
+		result = smt::CheckResult::ERROR;
+	}
+
+	for (string& value: values)
+	{
+		try
+		{
+			// Parse and re-format nicely
+			value = formatNumber(bigint(value));
+		}
+		catch (...) { }
+	}
+
+	return make_pair(result, values);
+}
+
+smt::CheckResult SMTChecker::checkSatisifable()
+{
+	return checkSatisifableAndGenerateModel({}).first;
+}
+
+void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
+{
+	for (auto const& variable: _function.localVariables())
+		if (createVariable(*variable))
+			setZeroValue(*variable);
+
+	for (auto const& param: _function.parameters())
+		if (createVariable(*param))
+			setUnknownValue(*param);
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+			if (createVariable(*retParam))
+				setZeroValue(*retParam);
+}
+
+void SMTChecker::resetVariables(vector<Declaration const*> _variables)
+{
+	for (auto const* decl: _variables)
+	{
+		newValue(*decl);
+		setUnknownValue(*decl);
+	}
+}
+
+bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
 	{
@@ -498,13 +624,16 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
 		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
-		setValue(_varDecl, _setToZero);
+		return true;
 	}
 	else
+	{
 		m_errorReporter.warning(
 			_varDecl.location(),
 			"Assertion checker does not yet support the type of this variable."
 		);
+		return false;
+	}
 }
 
 string SMTChecker::uniqueSymbol(Declaration const& _decl)
@@ -535,23 +664,22 @@ 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);
 }
 
-void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
+void SMTChecker::setZeroValue(Declaration const& _decl)
 {
-	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+	solAssert(_decl.type()->category() == Type::Category::Integer, "");
+	m_interface->addAssertion(currentValue(_decl) == 0);
+}
 
-	if (_setToZero)
-		m_interface->addAssertion(currentValue(_decl) == 0);
-	else
-	{
-		m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
-		m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-	}
+void SMTChecker::setUnknownValue(Declaration const& _decl)
+{
+	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+	m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
+	m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
 }
 
 smt::Expression SMTChecker::minValue(IntegerType const& _t)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index faaac639..8e07d74d 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -17,8 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
@@ -29,6 +32,7 @@ namespace dev
 namespace solidity
 {
 
+class VariableUsage;
 class ErrorReporter;
 
 class SMTChecker: private ASTConstVisitor
@@ -48,6 +52,7 @@ private:
 	virtual void endVisit(FunctionDefinition const& _node) override;
 	virtual bool visit(IfStatement const& _node) override;
 	virtual bool visit(WhileStatement const& _node) override;
+	virtual bool visit(ForStatement const& _node) override;
 	virtual void endVisit(VariableDeclarationStatement const& _node) override;
 	virtual void endVisit(ExpressionStatement const& _node) override;
 	virtual void endVisit(Assignment const& _node) override;
@@ -61,6 +66,14 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void assignment(Declaration const& _variable, Expression const& _value);
+
+	// Visits the branch given by the statement, pushes and pops the SMT checker.
+	// @param _condition if present, asserts that this condition is true within the branch.
+	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	void visitBranch(Statement const& _statement, smt::Expression _condition);
+
+	/// Check that a condition can be satisfied.
 	void checkCondition(
 		smt::Expression _condition,
 		SourceLocation const& _location,
@@ -68,8 +81,24 @@ private:
 		std::string const& _additionalValueName = "",
 		smt::Expression* _additionalValue = nullptr
 	);
+	/// Checks that a boolean condition is not constant. Do not warn if the expression
+	/// is a literal constant.
+	/// @param _description the warning string, $VALUE will be replaced by the constant value.
+	void checkBooleanNotConstant(
+		Expression const& _condition,
+		std::string const& _description
+	);
+
+	std::pair<smt::CheckResult, std::vector<std::string>>
+	checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
 
-	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+	smt::CheckResult checkSatisifable();
+
+	void initializeLocalVariables(FunctionDefinition const& _function);
+	void resetVariables(std::vector<Declaration const*> _variables);
+	/// Tries to create an uninitialized variable and returns true on success.
+	/// This fails if the type is not supported.
+	bool createVariable(VariableDeclaration const& _varDecl);
 
 	static std::string uniqueSymbol(Declaration const& _decl);
 	static std::string uniqueSymbol(Expression const& _expr);
@@ -87,12 +116,16 @@ private:
 	/// sequence number to this value and returns the expression.
 	smt::Expression newValue(Declaration const& _decl);
 
-	/// Sets the value of the declaration either to zero or to its intrinsic range.
-	void setValue(Declaration const& _decl, bool _setToZero);
+	/// Sets the value of the declaration to zero.
+	void setZeroValue(Declaration const& _decl);
+	/// Resets the variable to an unknown value (in its range).
+	void setUnknownValue(Declaration const& decl);
 
 	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 +134,8 @@ private:
 	smt::Expression var(Declaration const& _decl);
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
+	std::shared_ptr<VariableUsage> m_variableUsage;
+	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;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 70dc1585..a69d19d5 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -52,6 +52,7 @@ class Expression
 {
 	friend class SolverInterface;
 public:
+	explicit Expression(bool _v): name(_v ? "true" : "false") {}
 	Expression(size_t _number): name(std::to_string(_number)) {}
 	Expression(u256 const& _number): name(_number.str()) {}
 	Expression(bigint const& _number): name(_number.str()) {}
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
new file mode 100644
index 00000000..4e96059d
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -0,0 +1,80 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/VariableUsage.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+VariableUsage::VariableUsage(ASTNode const& _node)
+{
+	auto nodeFun = [&](ASTNode const& n) -> bool
+	{
+		if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n))
+		{
+			Declaration const* declaration = identifier->annotation().referencedDeclaration;
+			solAssert(declaration, "");
+			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+				if (
+					varDecl->isLocalVariable() &&
+					identifier->annotation().lValueRequested &&
+					varDecl->annotation().type->isValueType()
+				)
+					m_touchedVariable[&n] = varDecl;
+		}
+		return true;
+	};
+	auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child)
+	{
+		if (m_touchedVariable.count(&_child) || m_children.count(&_child))
+			m_children[&_parent].push_back(&_child);
+	};
+
+	ASTReduce reducer(nodeFun, edgeFun);
+	_node.accept(reducer);
+}
+
+vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+{
+	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
+		return {};
+
+	set<Declaration const*> touched;
+	vector<ASTNode const*> toVisit;
+	toVisit.push_back(&_node);
+
+	while (!toVisit.empty())
+	{
+		ASTNode const* n = toVisit.back();
+		toVisit.pop_back();
+		if (m_children.count(n))
+		{
+			solAssert(!m_touchedVariable.count(n), "");
+			toVisit += m_children.at(n);
+		}
+		else
+		{
+			solAssert(m_touchedVariable.count(n), "");
+			touched.insert(m_touchedVariable.at(n));
+		}
+	}
+
+	return {touched.begin(), touched.end()};
+}
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
new file mode 100644
index 00000000..62561cce
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.h
@@ -0,0 +1,50 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ASTNode;
+class Declaration;
+
+/**
+ * This class collects information about which local variables of value type
+ * are modified in which parts of the AST.
+ */
+class VariableUsage
+{
+public:
+	explicit VariableUsage(ASTNode const& _node);
+
+	std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const;
+
+private:
+	// Variable touched by a specific AST node.
+	std::map<ASTNode const*, Declaration const*> m_touchedVariable;
+	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+};
+
+}
+}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 6111b2c8..e5c1aef4 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -91,7 +91,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 			solAssert(false, "");
 		}
 
-		if (result != CheckResult::UNSATISFIABLE)
+		if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
 		{
 			z3::model m = m_solver.get_model();
 			for (Expression const& e: _expressionsToEvaluate)
@@ -139,8 +139,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	}
 	else if (arguments.empty())
 	{
-		// We assume it is an integer...
-		return m_context.int_val(n.c_str());
+		if (n == "true")
+			return m_context.bool_val(true);
+		else if (n == "false")
+			return m_context.bool_val(false);
+		else
+			// We assume it is an integer...
+			return m_context.int_val(n.c_str());
 	}
 
 	solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 8d712a80..667d666b 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -105,6 +105,359 @@ BOOST_AUTO_TEST_CASE(warn_on_struct)
 	CHECK_WARNING_ALLOW_MULTI(text, "");
 }
 
+BOOST_AUTO_TEST_CASE(simple_assert)
+{
+	string text = R"(
+		contract C {
+			function f(uint a) public pure { assert(a == 2); }
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here for");
+}
+
+BOOST_AUTO_TEST_CASE(simple_assert_with_require)
+{
+	string text = R"(
+		contract C {
+			function f(uint a) public pure { require(a < 10); assert(a < 20); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(assignment_in_declaration)
+{
+	string text = R"(
+		contract C {
+			function f() public pure { uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(use_before_declaration)
+{
+	string text = R"(
+		contract C {
+			function f() public pure { a = 3; uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f() public pure { assert(a == 0); uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
+{
+	string text = R"(
+		contract C {
+			function f() public {
+				uint a = 3;
+				this.f();
+				assert(a == 3);
+				f();
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(branches_clear_variables)
+{
+	// Only clears accessed variables
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	// It is just a plain clear and will not combine branches.
+	text = R"(
+	contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a = 3;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Clear also works on the else branch
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+				} else {
+					a = 3;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Variable is not cleared, if it is only read.
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					assert(a == 3);
+				} else {
+					assert(a == 3);
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(branches_assert_condition)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				if (x > 10) {
+					assert(x > 9);
+				}
+				else
+				{
+					assert(x < 11);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				if (x > 10) {
+					assert(x > 9);
+				}
+				else if (x > 2)
+				{
+					assert(x <= 10 && x > 2);
+				}
+				else
+				{
+				   assert(0 <= x && x <= 2);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a++;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					++a;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a = 5;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+}
+
+BOOST_AUTO_TEST_CASE(while_loop_simple)
+{
+	// Check that variables are cleared
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				x = 2;
+				while (x > 1) {
+					x = 2;
+				}
+				assert(x == 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that condition is assumed.
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+					assert(x == 2);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	// Check that condition is not assumed after the body anymore
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+				}
+				assert(x == 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that negation of condition is not assumed after the body anymore
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+				}
+				assert(x != 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that side-effects of condition are taken into account
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				x = 7;
+				while ((x = 5) > 0) {
+				}
+				assert(x == 7);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+}
+
+BOOST_AUTO_TEST_CASE(constant_condition)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				if (x >= 0) { revert(); }
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Condition is always true");
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				if (x >= 10) { if (x < 10) { revert(); } }
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Condition is always false");
+	// a plain literal constant is fine
+	text = R"(
+		contract C {
+			function f(uint) public pure {
+				if (true) { revert(); }
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+
+BOOST_AUTO_TEST_CASE(for_loop)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				require(x == 2);
+				for (;;) {}
+				assert(x == 2);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				for (; x == 2; ) {
+					assert(x == 2);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				for (uint y = 2; x < 10; ) {
+					assert(y == 2);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				for (uint y = 2; x < 10; y = 3) {
+					assert(y == 2);
+				}
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				for (uint y = 2; x < 10; ) {
+					y = 3;
+				}
+				assert(y == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				for (uint y = 2; x < 10; ) {
+					y = 3;
+				}
+				assert(y == 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }