Merge pull request #5307 from ethereum/smt_uf

[SMTChecker] Uninterpreted functions for blockhash()

Changelog.md

@@ -6,6 +6,8 @@ Language Features:
 Compiler Features:
  * Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
  * Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
+ * SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
+ * SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
 
 
 Bugfixes:

libsolidity/formal/CVC4Interface.cpp

@@ -50,7 +50,7 @@ void CVC4Interface::pop()
 	m_solver.pop();
 }
 
-void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
 {
 	if (!m_functions.count(_name))
 	{
@@ -201,3 +201,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
 	// Cannot be reached.
 	return m_context.integerType();
 }
+
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<Sort> const& _sorts)
+{
+	vector<CVC4::Type> cvc4Sorts;
+	for (auto const& _sort: _sorts)
+		cvc4Sorts.push_back(cvc4Sort(_sort));
+	return cvc4Sorts;
+}

libsolidity/formal/CVC4Interface.h

@@ -51,7 +51,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -61,6 +61,7 @@ public:
 private:
 	CVC4::Expr toCVC4Expr(Expression const& _expr);
 	CVC4::Type cvc4Sort(smt::Sort _sort);
+	std::vector<CVC4::Type> cvc4Sort(std::vector<smt::Sort> const& _sort);
 
 	CVC4::ExprManager m_context;
 	CVC4::SmtEngine m_solver;

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()";
+	string blockHash = "blockhash";
-	// TODO Define blockhash as an uninterpreted function
+	defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int);
-	defineSpecialVariable(blockHash, _funCall);
+	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;

libsolidity/formal/SMTChecker.h

@@ -83,6 +83,7 @@ private:
 	void inlineFunctionCall(FunctionCall const&);
 
 	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+	void defineUninterpretedFunction(std::string const& _name, std::vector<smt::Sort> const& _domain, smt::Sort _codomain);
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -193,6 +194,11 @@ private:
 	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;
+	/// Stores the declaration of an Uninterpreted Function.
+	std::unordered_map<std::string, smt::Expression> m_uninterpretedFunctions;
+	/// Stores the instances of an Uninterpreted Function applied to arguments.
+	/// Used to retrieve models.
+	std::vector<Expression const*> m_uninterpretedTerms;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 	std::shared_ptr<Scanner> m_scanner;

libsolidity/formal/SMTLib2Interface.cpp

@@ -64,9 +64,12 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
 {
 	// TODO Use domain and codomain as key as well
+	string domain("");
+	for (auto const& sort: _domain)
+		domain += toSmtLibSort(sort) + ' ';
 	if (!m_functions.count(_name))
 	{
 		m_functions.insert(_name);
@@ -74,7 +77,7 @@ void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomai
 			"(declare-fun |" +
 			_name +
 			"| (" +
-			(_domain == Sort::Int ? "Int" : "Bool") +
+			domain +
 			") " +
 			(_codomain == Sort::Int ? "Int" : "Bool") +
 			")"
@@ -140,6 +143,19 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
 	return sexpr;
 }
 
+string SMTLib2Interface::toSmtLibSort(Sort _sort)
+{
+	switch (_sort)
+	{
+	case Sort::Int:
+		return "Int";
+	case Sort::Bool:
+		return "Bool";
+	default:
+		solAssert(false, "Invalid SMT sort");
+	}
+}
+
 void SMTLib2Interface::write(string _data)
 {
 	solAssert(!m_accumulatedOutput.empty(), "");

libsolidity/formal/SMTLib2Interface.h

@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -58,6 +58,7 @@ public:
 
 private:
 	std::string toSExpr(Expression const& _expr);
+	std::string toSmtLibSort(Sort _sort);
 
 	void write(std::string _data);
 

libsolidity/formal/SMTPortfolio.cpp

@@ -64,7 +64,7 @@ void SMTPortfolio::pop()
 		s->pop();
 }
 
-void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTPortfolio::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
 {
 	for (auto s : m_solvers)
 		s->declareFunction(_name, _domain, _codomain);

libsolidity/formal/SMTPortfolio.h

@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 

libsolidity/formal/SolverInterface.h

@@ -45,9 +45,7 @@ enum class CheckResult
 enum class Sort
 {
 	Int,
-	Bool,
+	Bool
-	IntIntFun, // Function of one Int returning a single Int
-	IntBoolFun // Function of one Int returning a single Bool
 };
 
 /// C++ representation of an SMTLIB2 expression.
@@ -150,7 +148,7 @@ public:
 	{
 		return Expression("/", std::move(_a), std::move(_b), Sort::Int);
 	}
-	Expression operator()(Expression _a) const
+	Expression operator()(std::vector<Expression> _arguments) const
 	{
 		solAssert(
 			arguments.empty(),
@@ -158,10 +156,10 @@ public:
 		);
 		switch (sort)
 		{
-		case Sort::IntIntFun:
+		case Sort::Int:
-			return Expression(name, _a, Sort::Int);
+			return Expression(name, std::move(_arguments), Sort::Int);
-		case Sort::IntBoolFun:
+		case Sort::Bool:
-			return Expression(name, _a, Sort::Bool);
+			return Expression(name, std::move(_arguments), Sort::Bool);
 		default:
 			solAssert(
 				false,
@@ -199,18 +197,21 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0;
+	virtual void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) = 0;
-	Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain)
+	{
+		declareFunction(std::move(_name), std::vector<Sort>{std::move(_domain)}, std::move(_codomain));
+	}
+	Expression newFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain)
 	{
 		declareFunction(_name, _domain, _codomain);
-		solAssert(_domain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
 		switch (_codomain)
 		{
 		case Sort::Int:
-			return Expression(std::move(_name), {}, Sort::IntIntFun);
+			return Expression(std::move(_name), {}, Sort::Int);
 		case Sort::Bool:
-			return Expression(std::move(_name), {}, Sort::IntBoolFun);
+			return Expression(std::move(_name), {}, Sort::Bool);
 		default:
 			solAssert(false, "Function sort not supported.");
 			break;

libsolidity/formal/SymbolicTypes.cpp

@@ -24,6 +24,15 @@
 using namespace std;
 using namespace dev::solidity;
 
+smt::Sort dev::solidity::smtSort(Type::Category _category)
+{
+	if (isNumber(_category))
+		return smt::Sort::Int;
+	else if (isBool(_category))
+		return smt::Sort::Bool;
+	solAssert(false, "Invalid type");
+}
+
 bool dev::solidity::isSupportedType(Type::Category _category)
 {
 	return isNumber(_category) ||

libsolidity/formal/SymbolicTypes.h

@@ -28,6 +28,9 @@ namespace dev
 namespace solidity
 {
 
+/// Returns the SMT sort that models the Solidity type _type.
+smt::Sort smtSort(Type::Category _type);
+
 /// So far int, bool and address are supported.
 /// Returns true if type is supported.
 bool isSupportedType(Type::Category _category);

libsolidity/formal/SymbolicVariables.cpp

@@ -37,6 +37,11 @@ SymbolicVariable::SymbolicVariable(
 {
 }
 
+string SymbolicVariable::currentName() const
+{
+	return uniqueSymbol(m_ssa->index());
+}
+
 string SymbolicVariable::uniqueSymbol(unsigned _index) const
 {
 	return m_uniqueName + "_" + to_string(_index);

libsolidity/formal/SymbolicVariables.h

@@ -51,6 +51,8 @@ public:
 		return valueAtIndex(m_ssa->index());
 	}
 
+	std::string currentName() const;
+
 	virtual smt::Expression valueAtIndex(int _index) const = 0;
 
 	smt::Expression increaseIndex()

libsolidity/formal/Z3Interface.cpp

@@ -51,7 +51,7 @@ void Z3Interface::pop()
 	m_solver.pop();
 }
 
-void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void Z3Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
 {
 	if (!m_functions.count(_name))
 		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
@@ -183,3 +183,11 @@ z3::sort Z3Interface::z3Sort(Sort _sort)
 	// Cannot be reached.
 	return m_context.int_sort();
 }
+
+z3::sort_vector Z3Interface::z3Sort(vector<Sort> const& _sorts)
+{
+	z3::sort_vector z3Sorts(m_context);
+	for (auto const& _sort: _sorts)
+		z3Sorts.push_back(z3Sort(_sort));
+	return z3Sorts;
+}

libsolidity/formal/Z3Interface.h

@@ -40,7 +40,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -50,6 +50,7 @@ public:
 private:
 	z3::expr toZ3Expr(Expression const& _expr);
 	z3::sort z3Sort(smt::Sort _sort);
+	z3::sort_vector z3Sort(std::vector<smt::Sort> const& _sort);
 
 	z3::context m_context;
 	z3::solver m_solver;

test/libsolidity/smtCheckerTests/special/blockhash.sol

@@ -2,9 +2,13 @@ pragma experimental SMTChecker;
 
 contract C
 {
-	function f() public payable {
+	function f(uint x) public payable {
+		assert(blockhash(x) > 0);
 		assert(blockhash(2) > 0);
+		uint y = x;
+		assert(blockhash(x) == blockhash(y));
 	}
 }
 // ----
-// Warning: (79-103): Assertion violation happens here
+// Warning: (85-109): Assertion violation happens here
+// Warning: (113-137): Assertion violation happens here