Merge pull request #5571 from ethereum/develop

Version 0.5.1

1 files changed, 67 insertions, 13 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index cc580021..ebb09f0a 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -22,19 +22,29 @@
 #include <libsolidity/formal/VariableUsage.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
-#include <libsolidity/interface/ErrorReporter.h>
+#include <liblangutil/ErrorReporter.h>
 
 #include <boost/range/adaptor/map.hpp>
 #include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
 using namespace dev;
+using namespace langutil;
 using namespace dev::solidity;
 
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
-	m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
 	m_errorReporter(_errorReporter)
 {
+#if defined (HAVE_Z3) || defined (HAVE_CVC4)
+	if (!_smtlib2Responses.empty())
+		m_errorReporter.warning(
+			"SMT-LIB2 query responses were given in the auxiliary input, "
+			"but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
+			"These responses will be ignored."
+			"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
+		);
+#endif
 }
 
 void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
@@ -78,6 +88,9 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		m_interface->reset();
 		m_pathConditions.clear();
 		m_expressions.clear();
+		m_specialVariables.clear();
+		m_uninterpretedFunctions.clear();
+		m_uninterpretedTerms.clear();
 		resetStateVariables();
 		initializeLocalVariables(_function);
 	}
@@ -310,9 +323,6 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 			);
 		break;
 	}
-	case Token::Add: // +
-		defineExpr(_op, expr(_op.subExpression()));
-		break;
 	case Token::Sub: // -
 	{
 		defineExpr(_op, 0 - expr(_op.subExpression()));
@@ -405,16 +415,24 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	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();
+	setUnknownValue(*symbolicVar);
 	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);
+	string blockHash = "blockhash";
+	auto const& arguments = _funCall.arguments();
+	solAssert(arguments.size() == 1, "");
+	smt::SortPointer paramSort = smtSort(*arguments.at(0)->annotation().type);
+	smt::SortPointer returnSort = smtSort(*_funCall.annotation().type);
+	defineUninterpretedFunction(
+		blockHash,
+		make_shared<smt::FunctionSort>(vector<smt::SortPointer>{paramSort}, returnSort)
+	);
+	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments.at(0))}));
+	m_uninterpretedTerms.push_back(&_funCall);
 }
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -451,6 +469,14 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 	else if (_funDef && _funDef->isImplemented())
 	{
 		vector<smt::Expression> funArgs;
+		auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+		solAssert(funType, "");
+		if (funType->bound())
+		{
+			auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+			solAssert(boundFunction, "");
+			funArgs.push_back(expr(boundFunction->expression()));
+		}
 		for (auto arg: _funCall.arguments())
 			funArgs.push_back(expr(*arg));
 		initializeFunctionCallParameters(*_funDef, funArgs);
@@ -542,6 +568,10 @@ void SMTChecker::endVisit(Return const& _return)
 
 bool SMTChecker::visit(MemberAccess const& _memberAccess)
 {
+	auto const& accessType = _memberAccess.annotation().type;
+	if (accessType->category() == Type::Category::Function)
+		return true;
+
 	auto const& exprType = _memberAccess.expression().annotation().type;
 	solAssert(exprType, "");
 	if (exprType->category() == Type::Category::Magic)
@@ -573,7 +603,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	{
 		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
 		m_specialVariables.emplace(_name, result.second);
-		result.second->setUnknownValue();
+		setUnknownValue(*result.second);
 		if (result.first)
 			m_errorReporter.warning(
 				_expr.location(),
@@ -587,6 +617,11 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
 }
 
+void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
+{
+	if (!m_uninterpretedFunctions.count(_name))
+		m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
+}
 
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
@@ -770,6 +805,11 @@ void SMTChecker::checkCondition(
 			expressionsToEvaluate.emplace_back(var.second->currentValue());
 			expressionNames.push_back(var.first);
 		}
+		for (auto const& uf: m_uninterpretedTerms)
+		{
+			expressionsToEvaluate.emplace_back(expr(*uf));
+			expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+		}
 	}
 	smt::CheckResult result;
 	vector<string> values;
@@ -846,6 +886,10 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 	{
 		// everything fine.
 	}
+	else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
+	{
+		// can't do anything.
+	}
 	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
 		m_errorReporter.warning(_condition.location(), "Condition unreachable.");
 	else
@@ -1037,13 +1081,23 @@ smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setZeroValue();
+	setZeroValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setZeroValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicZeroValue(_variable, *m_interface);
 }
 
 void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setUnknownValue();
+	setUnknownValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setUnknownValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicUnknownValue(_variable, *m_interface);
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)