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

1 files changed, 82 insertions, 18 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index e5648eb3..db0cec7f 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,22 @@ 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);
+	m_specialVariables.at(gasLeft)->setUnknownValue();
+}
+
+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 +480,11 @@ 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 +492,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 +522,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 +535,45 @@ 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)
+	{
+		defineSpecialVariable(_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 +746,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 +979,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 +996,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 +1033,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 +1041,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
 	{