Merge pull request #5272 from ethereum/smt_special_vars

[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash

13 files changed, 144 insertions, 61 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 99ab2cb5..631a9eee 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -363,6 +363,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		visitAssert(_funCall);
 	else if (funType.kind() == FunctionType::Kind::Require)
 		visitRequire(_funCall);
+	else if (funType.kind() == FunctionType::Kind::GasLeft)
+		visitGasLeft(_funCall);
+	else if (funType.kind() == FunctionType::Kind::BlockHash)
+		visitBlockHash(_funCall);
 	else if (funType.kind() == FunctionType::Kind::Internal)
 		inlineFunctionCall(_funCall);
 	else
@@ -393,6 +397,27 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall)
 	addPathImpliedExpression(expr(*args[0]));
 }
 
+void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
+{
+	string gasLeft = "gasleft()";
+	// We increase the variable index since gasleft changes
+	// inside a tx.
+	defineSpecialVariable(gasLeft, _funCall, true);
+	auto const& symbolicVar = m_specialVariables.at(gasLeft);
+	unsigned index = symbolicVar->index();
+	// We set the current value to unknown anyway to add type constraints.
+	symbolicVar->setUnknownValue();
+	if (index > 0)
+		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
+}
+
+void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
+{
+	string blockHash = "blockhash()";
+	// TODO Define blockhash as an uninterpreted function
+	defineSpecialVariable(blockHash, _funCall);
+}
+
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* _funDef = nullptr;
@@ -460,7 +485,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	}
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
-		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
+		if (
+			fun->kind() == FunctionType::Kind::Assert ||
+			fun->kind() == FunctionType::Kind::Require ||
+			fun->kind() == FunctionType::Kind::GasLeft ||
+			fun->kind() == FunctionType::Kind::BlockHash
+		)
 			return;
 		createExpr(_identifier);
 	}
@@ -468,6 +498,8 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
 			defineExpr(_identifier, currentValue(*decl));
+		else if (_identifier.name() == "now")
+			defineSpecialVariable(_identifier.name(), _identifier);
 		else
 			// TODO: handle MagicVariableDeclaration here
 			m_errorReporter.warning(
@@ -496,7 +528,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 
 void SMTChecker::endVisit(Return const& _return)
 {
-	if (hasExpr(*_return.expression()))
+	if (knownExpr(*_return.expression()))
 	{
 		auto returnParams = m_functionPath.back()->returnParameters();
 		if (returnParams.size() > 1)
@@ -509,6 +541,54 @@ void SMTChecker::endVisit(Return const& _return)
 	}
 }
 
+bool SMTChecker::visit(MemberAccess const& _memberAccess)
+{
+	auto const& exprType = _memberAccess.expression().annotation().type;
+	solAssert(exprType, "");
+	if (exprType->category() == Type::Category::Magic)
+	{
+		auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
+		string accessedName;
+		if (identifier)
+			accessedName = identifier->name();
+		else
+			m_errorReporter.warning(
+				_memberAccess.location(),
+				"Assertion checker does not yet support this expression."
+			);
+		defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
+		return false;
+	}
+	else
+		m_errorReporter.warning(
+			_memberAccess.location(),
+			"Assertion checker does not yet support this expression."
+		);
+
+	return true;
+}
+
+void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
+{
+	if (!knownSpecialVariable(_name))
+	{
+		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
+		m_specialVariables.emplace(_name, result.second);
+		result.second->setUnknownValue();
+		if (result.first)
+			m_errorReporter.warning(
+				_expr.location(),
+				"Assertion checker does not yet support this special variable."
+			);
+	}
+	else if (_increaseIndex)
+		m_specialVariables.at(_name)->increaseIndex();
+	// The default behavior is not to increase the index since
+	// most of the special values stay the same throughout a tx.
+	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
+}
+
+
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
 	switch (_op.getOperator())
@@ -681,11 +761,15 @@ void SMTChecker::checkCondition(
 			expressionNames.push_back(_additionalValueName);
 		}
 		for (auto const& var: m_variables)
-			if (knownVariable(*var.first))
-			{
-				expressionsToEvaluate.emplace_back(currentValue(*var.first));
-				expressionNames.push_back(var.first->name());
-			}
+		{
+			expressionsToEvaluate.emplace_back(currentValue(*var.first));
+			expressionNames.push_back(var.first->name());
+		}
+		for (auto const& var: m_specialVariables)
+		{
+			expressionsToEvaluate.emplace_back(var.second->currentValue());
+			expressionNames.push_back(var.first);
+		}
 	}
 	smt::CheckResult result;
 	vector<string> values;
@@ -910,7 +994,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	// This might be the case for multiple calls to the same function.
-	if (hasVariable(_varDecl))
+	if (knownVariable(_varDecl))
 		return true;
 	auto const& type = _varDecl.type();
 	solAssert(m_variables.count(&_varDecl) == 0, "");
@@ -927,11 +1011,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	return true;
 }
 
-string SMTChecker::uniqueSymbol(Expression const& _expr)
-{
-	return "expr_" + to_string(_expr.id());
-}
-
 bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
 {
 	return m_variables.count(&_decl);
@@ -969,7 +1048,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!hasExpr(_e))
+	if (!knownExpr(_e))
 	{
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
@@ -977,20 +1056,20 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 	return m_expressions.at(&_e)->currentValue();
 }
 
-bool SMTChecker::hasExpr(Expression const& _e) const
+bool SMTChecker::knownExpr(Expression const& _e) const
 {
 	return m_expressions.count(&_e);
 }
 
-bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
+bool SMTChecker::knownSpecialVariable(string const& _var) const
 {
-	return m_variables.count(&_var);
+	return m_specialVariables.count(_var);
 }
 
 void SMTChecker::createExpr(Expression const& _e)
 {
 	solAssert(_e.annotation().type, "");
-	if (hasExpr(_e))
+	if (knownExpr(_e))
 		m_expressions.at(&_e)->increaseIndex();
 	else
 	{
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index f66693d2..95e01708 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -66,6 +66,7 @@ private:
 	virtual void endVisit(Identifier const& _node) override;
 	virtual void endVisit(Literal const& _node) override;
 	virtual void endVisit(Return const& _node) override;
+	virtual bool visit(MemberAccess const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
@@ -73,10 +74,14 @@ private:
 
 	void visitAssert(FunctionCall const&);
 	void visitRequire(FunctionCall const&);
+	void visitGasLeft(FunctionCall const&);
+	void visitBlockHash(FunctionCall const&);
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const&);
 
+	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@@ -129,8 +134,6 @@ private:
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
-	static std::string uniqueSymbol(Expression const& _expr);
-
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
 	/// has a valid index
 	bool knownVariable(VariableDeclaration const& _decl);
@@ -154,10 +157,13 @@ private:
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
 	/// Checks if expression was created
-	bool hasExpr(Expression const& _e) const;
+	bool knownExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
+	/// Checks if special variable was seen.
+	bool knownSpecialVariable(std::string const& _var) const;
+
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
 	/// Remove the last path condition
@@ -172,9 +178,6 @@ private:
 	/// Removes local variables from the context.
 	void removeLocalVariables();
 
-	/// Checks if VariableDeclaration was seen.
-	bool hasVariable(VariableDeclaration const& _e) const;
-
 	/// Copy the SSA indices of m_variables.
 	VariableIndices copyVariableIndices();
 	/// Resets the variable indices.
@@ -187,6 +190,7 @@ private:
 	/// repeated calls to the same function.
 	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
+	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index dbc58664..36e15508 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -28,6 +28,6 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex.reset (new int);
+	m_nextFreeIndex.reset (new unsigned);
 	*m_nextFreeIndex = 1;
 }
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index d357740d..46935472 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -34,19 +34,19 @@ public:
 	void resetIndex();
 
 	/// This function returns the current index of this SSA variable.
-	int index() const { return m_currentIndex; }
-	int& index() { return m_currentIndex; }
+	unsigned index() const { return m_currentIndex; }
+	unsigned& index() { return m_currentIndex; }
 
-	int operator++()
+	unsigned operator++()
 	{
 		return m_currentIndex = (*m_nextFreeIndex)++;
 	}
 
 private:
-	int m_currentIndex;
+	unsigned m_currentIndex;
 	/// The next free index is a shared pointer because we want
 	/// the copy and the copied to share it.
-	std::shared_ptr<int> m_nextFreeIndex;
+	std::shared_ptr<unsigned> m_nextFreeIndex;
 };
 
 }
diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp
index 68b95080..67a18540 100644
--- a/libsolidity/formal/SymbolicAddressVariable.cpp
+++ b/libsolidity/formal/SymbolicAddressVariable.cpp
@@ -24,18 +24,17 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicAddressVariable::SymbolicAddressVariable(
-	Type const& _type,
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicIntVariable(_type, _uniqueName, _interface)
+	SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
 {
-	solAssert(isAddress(_type.category()), "");
 }
 
 void SymbolicAddressVariable::setUnknownValue()
 {
-	IntegerType intType{160};
-	m_interface.addAssertion(currentValue() >= minValue(intType));
-	m_interface.addAssertion(currentValue() <= maxValue(intType));
+	auto intType = dynamic_cast<IntegerType const*>(m_type.get());
+	solAssert(intType, "");
+	m_interface.addAssertion(currentValue() >= minValue(*intType));
+	m_interface.addAssertion(currentValue() <= maxValue(*intType));
 }
diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h
index 4a0f2361..3c9c379a 100644
--- a/libsolidity/formal/SymbolicAddressVariable.h
+++ b/libsolidity/formal/SymbolicAddressVariable.h
@@ -31,7 +31,6 @@ class SymbolicAddressVariable: public SymbolicIntVariable
 {
 public:
 	SymbolicAddressVariable(
-		Type const& _type,
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index 9c41ca9d..4d753c5c 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -22,13 +22,13 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicBoolVariable::SymbolicBoolVariable(
-	Type const& _type,
+	TypePointer _type,
 	string const& _uniqueName,
 	smt::SolverInterface&_interface
 ):
-	SymbolicVariable(_type, _uniqueName, _interface)
+	SymbolicVariable(move(_type), _uniqueName, _interface)
 {
-	solAssert(_type.category() == Type::Category::Bool, "");
+	solAssert(m_type->category() == Type::Category::Bool, "");
 }
 
 smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index 85e41b3b..438af2c6 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -31,7 +31,7 @@ class SymbolicBoolVariable: public SymbolicVariable
 {
 public:
 	SymbolicBoolVariable(
-		Type const& _type,
+		TypePointer _type,
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index cf1a7486..a5939842 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -24,13 +24,13 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicIntVariable::SymbolicIntVariable(
-	Type const& _type,
+	TypePointer _type,
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(_type, _uniqueName, _interface)
+	SymbolicVariable(move(_type), _uniqueName, _interface)
 {
-	solAssert(isNumber(_type.category()), "");
+	solAssert(isNumber(m_type->category()), "");
 }
 
 smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
@@ -45,7 +45,7 @@ void SymbolicIntVariable::setZeroValue()
 
 void SymbolicIntVariable::setUnknownValue()
 {
-	auto intType = dynamic_cast<IntegerType const*>(&m_type);
+	auto intType = dynamic_cast<IntegerType const*>(m_type.get());
 	solAssert(intType, "");
 	m_interface.addAssertion(currentValue() >= minValue(*intType));
 	m_interface.addAssertion(currentValue() <= maxValue(*intType));
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index 110ebb09..a9e51b1b 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -31,7 +31,7 @@ class SymbolicIntVariable: public SymbolicVariable
 {
 public:
 	SymbolicIntVariable(
-		Type const& _type,
+		TypePointer _type,
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index d47869db..7e5db7bd 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -43,27 +43,28 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 {
 	bool abstract = false;
 	shared_ptr<SymbolicVariable> var;
+	TypePointer type = _type.shared_from_this();
 	if (!isSupportedType(_type))
 	{
 		abstract = true;
-		var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
 	}
 	else if (isBool(_type.category()))
-		var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
 	else if (isFunction(_type.category()))
-		var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
 	else if (isInteger(_type.category()))
-		var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+		var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
 	else if (isAddress(_type.category()))
-		var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+		var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
 	else if (isRational(_type.category()))
 	{
 		auto rational = dynamic_cast<RationalNumberType const*>(&_type);
 		solAssert(rational, "");
 		if (rational->isFractional())
-			var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+			var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
 		else
-			var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+			var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
 	}
 	else
 		solAssert(false, "");
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index c042ec48..530564d2 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -24,18 +24,18 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicVariable::SymbolicVariable(
-	Type const& _type,
+	TypePointer _type,
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	m_type(_type),
+	m_type(move(_type)),
 	m_uniqueName(_uniqueName),
 	m_interface(_interface),
 	m_ssa(make_shared<SSAVariable>())
 {
 }
 
-string SymbolicVariable::uniqueSymbol(int _index) const
+string SymbolicVariable::uniqueSymbol(unsigned _index) const
 {
 	return m_uniqueName + "_" + to_string(_index);
 }
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 417e1f92..e554139f 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -39,10 +39,11 @@ class SymbolicVariable
 {
 public:
 	SymbolicVariable(
-		Type const& _type,
+		TypePointer _type,
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
+
 	virtual ~SymbolicVariable() = default;
 
 	smt::Expression currentValue() const
@@ -58,8 +59,8 @@ public:
 		return currentValue();
 	}
 
-	int index() const { return m_ssa->index(); }
-	int& index() { return m_ssa->index(); }
+	unsigned index() const { return m_ssa->index(); }
+	unsigned& index() { return m_ssa->index(); }
 
 	/// Sets the var to the default value of its type.
 	/// Inherited types must implement.
@@ -69,9 +70,9 @@ public:
 	virtual void setUnknownValue() {}
 
 protected:
-	std::string uniqueSymbol(int _index) const;
+	std::string uniqueSymbol(unsigned _index) const;
 
-	Type const& m_type;
+	TypePointer m_type = nullptr;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
 	std::shared_ptr<SSAVariable> m_ssa = nullptr;