Merge pull request #6758 from ethereum/smt_global_context

[SMTChecker] Move handling of global vars and functions

libsolidity/formal/EncodingContext.cpp

@@ -38,6 +38,7 @@ void EncodingContext::reset()
 {
 	resetAllVariables();
 	m_expressions.clear();
+	m_globalContext.clear();
 	m_thisAddress->increaseIndex();
 	m_balances->increaseIndex();
 }
@@ -153,6 +154,28 @@ bool EncodingContext::knownExpression(solidity::Expression const& _e) const
 	return m_expressions.count(&_e);
 }
 
+/// Global variables and functions.
+
+shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name)
+{
+	solAssert(knownGlobalSymbol(_name), "");
+	return m_globalContext.at(_name);
+}
+
+bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr)
+{
+	solAssert(!knownGlobalSymbol(_name), "");
+	auto result = newSymbolicVariable(*_expr.annotation().type, _name, m_solver);
+	m_globalContext.emplace(_name, result.second);
+	setUnknownValue(*result.second);
+	return result.first;
+}
+
+bool EncodingContext::knownGlobalSymbol(string const& _var) const
+{
+	return m_globalContext.count(_var);
+}
+
 // Blockchain
 
 Expression EncodingContext::thisAddress()

libsolidity/formal/EncodingContext.h

@@ -88,6 +88,19 @@ public:
 	bool knownExpression(solidity::Expression const& _e) const;
 	//@}
 
+	/// Methods related to global variables and functions.
+	//@{
+	/// Global variables and functions.
+	std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
+	/// @returns all symbolic variables.
+	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
+	/// Defines a new global variable or function
+	/// and @returns true if type was abstracted.
+	bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr);
+	/// Checks if special variable or function was seen.
+	bool knownGlobalSymbol(std::string const& _var) const;
+	//@}
+
 	/// Blockchain related methods.
 	//@{
 	/// Value of `this` address.
@@ -112,6 +125,10 @@ private:
 	/// Symbolic expressions.
 	std::unordered_map<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 
+	/// Symbolic representation of global symbols including
+	/// variables and functions.
+	std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
+
 	/// 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_globalContext.clear();
 		m_uninterpretedTerms.clear();
 		m_overflowTargets.clear();
 		resetStateVariables();
@@ -730,7 +729,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	// We increase the variable index since gasleft changes
 	// inside a tx.
 	defineGlobalVariable(gasLeft, _funCall, true);
-	auto const& symbolicVar = m_globalContext.at(gasLeft);
+	auto const& symbolicVar = m_context.globalSymbol(gasLeft);
 	unsigned index = symbolicVar->index();
 	// We set the current value to unknown anyway to add type constraints.
 	m_context.setUnknownValue(*symbolicVar);
@@ -897,8 +896,8 @@ void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
 	auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
 	if (fType.returnParameterTypes().size() == 1)
 	{
-		defineGlobalFunction(fType.richIdentifier(), _identifier);
+		defineGlobalVariable(fType.richIdentifier(), _identifier);
-		m_context.createExpression(_identifier, m_globalContext.at(fType.richIdentifier()));
+		m_context.createExpression(_identifier, m_context.globalSymbol(fType.richIdentifier()));
 	}
 }
 
@@ -1117,37 +1116,21 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 
 void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
 {
-	if (!knownGlobalSymbol(_name))
+	if (!m_context.knownGlobalSymbol(_name))
 	{
-		auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
+		bool abstract = m_context.createGlobalSymbol(_name, _expr);
-		m_globalContext.emplace(_name, result.second);
+		if (abstract)
-		m_context.setUnknownValue(*result.second);
-		if (result.first)
 			m_errorReporter.warning(
 				_expr.location(),
 				"Assertion checker does not yet support this global variable."
 			);
 	}
 	else if (_increaseIndex)
-		m_globalContext.at(_name)->increaseIndex();
+		m_context.globalSymbol(_name)->increaseIndex();
 	// The default behavior is not to increase the index since
 	// most of the global values stay the same throughout a tx.
 	if (smt::isSupportedType(_expr.annotation().type->category()))
-		defineExpr(_expr, m_globalContext.at(_name)->currentValue());
+		defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
-}
-
-void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _expr)
-{
-	if (!knownGlobalSymbol(_name))
-	{
-		auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
-		m_globalContext.emplace(_name, result.second);
-		if (result.first)
-			m_errorReporter.warning(
-				_expr.location(),
-				"Assertion checker does not yet support the type of this function."
-			);
-	}
 }
 
 bool SMTChecker::shortcutRationalNumber(Expression const& _expr)
@@ -1462,7 +1445,7 @@ void SMTChecker::checkCondition(
 				expressionNames.push_back(var.first->name());
 			}
 		}
-		for (auto const& var: m_globalContext)
+		for (auto const& var: m_context.globalSymbols())
 		{
 			auto const& type = var.second->type();
 			if (
@@ -1763,11 +1746,6 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 	return m_context.expression(_e)->currentValue();
 }
 
-bool SMTChecker::knownGlobalSymbol(string const& _var) const
-{
-	return m_globalContext.count(_var);
-}
-
 void SMTChecker::createExpr(Expression const& _e)
 {
 	bool abstract = m_context.createExpression(_e);

libsolidity/formal/SMTChecker.h

@@ -126,8 +126,9 @@ private:
 	/// visit depth.
 	void visitFunctionOrModifier();
 
+	/// Defines a new global variable or function.
 	void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
-	void defineGlobalFunction(std::string const& _name, Expression const& _expr);
+
 	/// Handles the side effects of assignment
 	/// to variable of some SMT array type
 	/// while aliasing is not supported.
@@ -241,9 +242,6 @@ private:
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
-	/// Checks if special variable or function was seen.
-	bool knownGlobalSymbol(std::string const& _var) const;
-
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
 	/// Remove the last path condition
@@ -280,8 +278,6 @@ private:
 	// True if the "No SMT solver available" warning was already created.
 	bool m_noSolverWarning = false;
 
-	std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
-
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
 	/// These may be direct application of UFs or Array index access.
 	/// Used to retrieve models.