[SMTChecker] Move expression handling to EncodingContext

libsolidity/formal/EncodingContext.cpp

@@ -37,6 +37,7 @@ EncodingContext::EncodingContext(SolverInterface& _solver):
 void EncodingContext::reset()
 {
 	resetAllVariables();
+	m_expressions.clear();
 	m_thisAddress->increaseIndex();
 	m_balances->increaseIndex();
 }
@@ -117,6 +118,43 @@ void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
 	setSymbolicUnknownValue(_variable, m_solver);
 }
 
+/// Expressions
+
+shared_ptr<SymbolicVariable> EncodingContext::expression(solidity::Expression const& _e)
+{
+	if (!knownExpression(_e))
+		createExpression(_e);
+	return m_expressions.at(&_e);
+}
+
+bool EncodingContext::createExpression(solidity::Expression const& _e, shared_ptr<SymbolicVariable> _symbVar)
+{
+	solAssert(_e.annotation().type, "");
+	if (knownExpression(_e))
+	{
+		expression(_e)->increaseIndex();
+		return false;
+	}
+	else if (_symbVar)
+	{
+		m_expressions.emplace(&_e, _symbVar);
+		return false;
+	}
+	else
+	{
+		auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), m_solver);
+		m_expressions.emplace(&_e, result.second);
+		return result.first;
+	}
+}
+
+bool EncodingContext::knownExpression(solidity::Expression const& _e) const
+{
+	return m_expressions.count(&_e);
+}
+
+// Blockchain
+
 Expression EncodingContext::thisAddress()
 {
 	return m_thisAddress->currentValue();

libsolidity/formal/EncodingContext.h

@@ -74,6 +74,20 @@ public:
 	void setUnknownValue(SymbolicVariable& _variable);
 	//@}
 
+	/// Methods related to expressions.
+	////@{
+	/// @returns the symbolic representation of an AST node expression.
+	std::shared_ptr<SymbolicVariable> expression(solidity::Expression const& _e);
+	/// @returns all symbolic expressions.
+	std::unordered_map<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
+
+	/// Creates the expression (value can be arbitrary).
+	/// @returns true if type is not supported.
+	bool createExpression(solidity::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbExpr = nullptr);
+	/// Checks if expression was created.
+	bool knownExpression(solidity::Expression const& _e) const;
+	//@}
+
 	/// Blockchain related methods.
 	//@{
 	/// Value of `this` address.
@@ -95,6 +109,9 @@ private:
 	/// Symbolic variables.
 	std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 
+	/// Symbolic expressions.
+	std::unordered_map<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
+
 	/// Symbolic `this` address.
 	std::unique_ptr<SymbolicAddressVariable> m_thisAddress;
 

libsolidity/formal/SMTChecker.cpp

@@ -111,7 +111,6 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		m_pathConditions.clear();
 		m_callStack.clear();
 		pushCallStack({&_function, nullptr});
-		m_expressions.clear();
 		m_globalContext.clear();
 		m_uninterpretedTerms.clear();
 		m_overflowTargets.clear();
@@ -332,21 +331,20 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 	{
 		if (auto init = _varDecl.initialValue())
 		{
-			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[init]);
+			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*init));
-			/// symbTuple == nullptr if it is the return of a non-inlined function call.
+			solAssert(symbTuple, "");
-			if (symbTuple)
-			{
 			auto const& components = symbTuple->components();
 			auto const& declarations = _varDecl.declarations();
+			if (components.size() == declarations.size())
 				for (unsigned i = 0; i < declarations.size(); ++i)
-				{
+					if (
-					solAssert(components.at(i), "");
+						components.at(i) &&
-					if (declarations.at(i) && m_context.knownVariable(*declarations.at(i)))
+						declarations.at(i) &&
+						m_context.knownVariable(*declarations.at(i))
+					)
 						assignment(*declarations.at(i), components.at(i)->currentValue(), declarations.at(i)->location());
 		}
 	}
-		}
-	}
 	else if (m_context.knownVariable(*_varDecl.declarations().front()))
 	{
 		if (_varDecl.initialValue())
@@ -390,7 +388,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		vector<smt::Expression> rightArguments;
 		if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
 		{
-			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]);
+			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.rightHandSide()));
 			solAssert(symbTuple, "");
 			for (auto const& component: symbTuple->components())
 			{
@@ -434,14 +432,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 					components.push_back(m_context.variable(*varDecl));
 				else
 				{
-					solAssert(knownExpr(*component), "");
+					solAssert(m_context.knownExpression(*component), "");
-					components.push_back(m_expressions[component.get()]);
+					components.push_back(m_context.expression(*component));
 				}
 			}
 			else
 				components.push_back(nullptr);
 		solAssert(components.size() == _tuple.components().size(), "");
-		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_tuple]);
+		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
 		symbTuple->setComponents(move(components));
 	}
@@ -575,8 +573,8 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 		}
 		else
 		{
-			solAssert(knownExpr(subExpr), "");
+			solAssert(m_context.knownExpression(subExpr), "");
-			auto const& symbVar = m_expressions[&subExpr];
+			auto const& symbVar = m_context.expression(subExpr);
 			symbVar->increaseIndex();
 			m_context.setZeroValue(*symbVar);
 			if (dynamic_cast<IndexAccess const*>(&_op.subExpression()))
@@ -791,7 +789,7 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 				solAssert(m_context.variable(*param), "");
 				components.push_back(m_context.variable(*param));
 			}
-			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_funCall]);
+			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
 			solAssert(symbTuple, "");
 			symbTuple->setComponents(move(components));
 		}
@@ -824,7 +822,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
 	vector<smt::Expression> smtArguments;
 	for (auto const& arg: _funCall.arguments())
 		smtArguments.push_back(expr(*arg));
-	defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
+	defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
 	m_uninterpretedTerms.insert(&_funCall);
 	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
 }
@@ -869,7 +867,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
 	else
 	{
 		createExpr(_funCall);
-		m_context.setUnknownValue(*m_expressions.at(&_funCall));
+		m_context.setUnknownValue(*m_context.expression(_funCall));
 		auto const& funCallCategory = _funCall.annotation().type->category();
 		// TODO: truncating and bytesX needs a different approach because of right padding.
 		if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address)
@@ -878,7 +876,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
 				defineExpr(_funCall, expr(*argument));
 			else
 			{
-				auto const& intType = dynamic_cast<IntegerType const&>(*m_expressions.at(&_funCall)->type());
+				auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
 				defineExpr(_funCall, smt::Expression::ite(
 					expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
 					expr(*argument),
@@ -900,7 +898,7 @@ void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
 	if (fType.returnParameterTypes().size() == 1)
 	{
 		defineGlobalFunction(fType.richIdentifier(), _identifier);
-		m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
+		m_context.createExpression(_identifier, m_globalContext.at(fType.richIdentifier()));
 	}
 }
 
@@ -920,7 +918,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 			auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
 			solAssert(stringLit, "");
 			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
-			m_expressions.emplace(&_literal, result.second);
+			m_context.createExpression(_literal, result.second);
 		}
 		m_errorReporter.warning(
 			_literal.location(),
@@ -933,7 +931,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 
 void SMTChecker::endVisit(Return const& _return)
 {
-	if (_return.expression() && knownExpr(*_return.expression()))
+	if (_return.expression() && m_context.knownExpression(*_return.expression()))
 	{
 		auto returnParams = m_callStack.back().first->returnParameters();
 		if (returnParams.size() > 1)
@@ -989,7 +987,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 		if (_memberAccess.memberName() == "balance")
 		{
 			defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
-			setSymbolicUnknownValue(*m_expressions[&_memberAccess], *m_interface);
+			setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface);
 			m_uninterpretedTerms.insert(&_memberAccess);
 			return false;
 		}
@@ -1015,8 +1013,8 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
 	}
 	else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
 	{
-		solAssert(knownExpr(*innerAccess), "");
+		solAssert(m_context.knownExpression(*innerAccess), "");
-		array = m_expressions[innerAccess];
+		array = m_context.expression(*innerAccess);
 	}
 	else
 	{
@@ -1757,17 +1755,12 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!knownExpr(_e))
+	if (!m_context.knownExpression(_e))
 	{
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
-	return m_expressions.at(&_e)->currentValue();
+	return m_context.expression(_e)->currentValue();
-}
-
-bool SMTChecker::knownExpr(Expression const& _e) const
-{
-	return m_expressions.count(&_e);
 }
 
 bool SMTChecker::knownGlobalSymbol(string const& _var) const
@@ -1777,19 +1770,12 @@ bool SMTChecker::knownGlobalSymbol(string const& _var) const
 
 void SMTChecker::createExpr(Expression const& _e)
 {
-	solAssert(_e.annotation().type, "");
+	bool abstract = m_context.createExpression(_e);
-	if (knownExpr(_e))
+	if (abstract)
-		m_expressions.at(&_e)->increaseIndex();
-	else
-	{
-		auto result = smt::newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
-		m_expressions.emplace(&_e, result.second);
-		if (result.first)
 		m_errorReporter.warning(
 			_e.location(),
 			"Assertion checker does not yet implement this type."
 		);
-	}
 }
 
 void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)

libsolidity/formal/SMTChecker.h

@@ -238,8 +238,6 @@ private:
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
-	/// Checks if expression was created
-	bool knownExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
@@ -281,9 +279,7 @@ private:
 	bool m_externalFunctionCallHappened = false;
 	// True if the "No SMT solver available" warning was already created.
 	bool m_noSolverWarning = false;
-	/// An Expression may have multiple smt::Expression due to
+
-	/// repeated calls to the same function.
-	std::unordered_map<Expression const*, std::shared_ptr<smt::SymbolicVariable>> m_expressions;
 	std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
 
 	/// Stores the instances of an Uninterpreted Function applied to arguments.