[SMTChecker] Implement uninterpreted functions and use it for blockhash()

1 files changed, 19 insertions, 3 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index cc580021..9a2b9bbf 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -78,6 +78,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);
 	}
@@ -412,9 +415,12 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 
 void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
 {
-	string blockHash = "blockhash()";
-	// TODO Define blockhash as an uninterpreted function
-	defineSpecialVariable(blockHash, _funCall);
+	string blockHash = "blockhash";
+	defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int);
+	auto const& arguments = _funCall.arguments();
+	solAssert(arguments.size() == 1, "");
+	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])}));
+	m_uninterpretedTerms.push_back(&_funCall);
 }
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -587,6 +593,11 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
 }
 
+void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::Sort> const& _domain, smt::Sort _codomain)
+{
+	if (!m_uninterpretedFunctions.count(_name))
+		m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain));
+}
 
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
@@ -770,6 +781,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;