Merge pull request #3091 from ethereum/smt-cleanup

Various cleanups to Z3

4 files changed, 40 insertions, 31 deletions

diff --git a/libsolidity/ast/ASTForward.h b/libsolidity/ast/ASTForward.h
index 15735368..46675e51 100644
--- a/libsolidity/ast/ASTForward.h
+++ b/libsolidity/ast/ASTForward.h
@@ -57,6 +57,7 @@ class UserDefinedTypeName;
 class FunctionTypeName;
 class Mapping;
 class ArrayTypeName;
+class InlineAssembly;
 class Statement;
 class Block;
 class PlaceholderStatement;
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 7c8c089e..2d2f05ec 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 	{
 		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
-		solAssert(m_Variables.count(&_varDecl) == 0, "");
+		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
-		m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
 		setValue(_varDecl, _setToZero);
 	}
 	else
@@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_Expressions.count(&_e))
+	if (!m_expressions.count(&_e))
 	{
 		solAssert(_e.annotation().type, "");
 		switch (_e.annotation().type->category())
@@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		{
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
 				solAssert(!rational->isFractional(), "");
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		}
 		case Type::Category::Integer:
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		case Type::Category::Bool:
-			m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
 			break;
 		default:
 			solAssert(false, "Type not implemented.");
 		}
 	}
-	return m_Expressions.at(&_e);
+	return m_expressions.at(&_e);
 }
 
 smt::Expression SMTChecker::var(Declaration const& _decl)
 {
-	solAssert(m_Variables.count(&_decl), "");
-	return m_Variables.at(&_decl);
+	solAssert(m_variables.count(&_decl), "");
+	return m_variables.at(&_decl);
 }
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index d23fd201..faaac639 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -103,8 +103,8 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
-	std::map<Expression const*, smt::Expression> m_Expressions;
-	std::map<Declaration const*, smt::Expression> m_Variables;
+	std::map<Expression const*, smt::Expression> m_expressions;
+	std::map<Declaration const*, smt::Expression> m_variables;
 	ErrorReporter& m_errorReporter;
 
 	FunctionDefinition const* m_currentFunction = nullptr;
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 0ceed3a7..ab28baa3 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -73,28 +73,37 @@ void Z3Interface::addAssertion(Expression const& _expr)
 pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
 	CheckResult result;
-	switch (m_solver.check())
+	vector<string> values;
+	try
 	{
-	case z3::check_result::sat:
-		result = CheckResult::SATISFIABLE;
-		break;
-	case z3::check_result::unsat:
-		result = CheckResult::UNSATISFIABLE;
-		break;
-	case z3::check_result::unknown:
-		result = CheckResult::UNKNOWN;
-		break;
-	default:
-		solAssert(false, "");
+		switch (m_solver.check())
+		{
+		case z3::check_result::sat:
+			result = CheckResult::SATISFIABLE;
+			break;
+		case z3::check_result::unsat:
+			result = CheckResult::UNSATISFIABLE;
+			break;
+		case z3::check_result::unknown:
+			result = CheckResult::UNKNOWN;
+			break;
+		default:
+			solAssert(false, "");
+		}
+
+		if (result != CheckResult::UNSATISFIABLE)
+		{
+			z3::model m = m_solver.get_model();
+			for (Expression const& e: _expressionsToEvaluate)
+				values.push_back(toString(m.eval(toZ3Expr(e))));
+		}
 	}
-
-	vector<string> values;
-	if (result != CheckResult::UNSATISFIABLE)
+	catch (z3::exception const& _e)
 	{
-		z3::model m = m_solver.get_model();
-		for (Expression const& e: _expressionsToEvaluate)
-			values.push_back(toString(m.eval(toZ3Expr(e))));
+		result = CheckResult::ERROR;
+		values.clear();
 	}
+
 	return make_pair(result, values);
 }
 
@@ -118,8 +127,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		{">=", 2},
 		{"+", 2},
 		{"-", 2},
-		{"*", 2},
-		{">=", 2}
+		{"*", 2}
 	};
 	string const& n = _expr.name;
 	if (m_functions.count(n))