Merge pull request #7353 from ethereum/develop

Update 0.6.0 from develop

libsolidity/formal/CVC4Interface.cpp

@@ -137,6 +137,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 				return m_context.mkConst(true);
 			else if (n == "false")
 				return m_context.mkConst(false);
+			else if (auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort))
+				return m_context.mkVar(n, cvc4Sort(*sortSort->inner));
 			else
 				try
 				{
@@ -187,6 +189,12 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
 		else if (n == "store")
 			return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
+		else if (n == "const_array")
+		{
+			shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
+			solAssert(sortSort, "");
+			return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
+		}
 
 		solAssert(false, "");
 	}

libsolidity/formal/SMTLib2Interface.cpp

@@ -17,8 +17,6 @@
 
 #include <libsolidity/formal/SMTLib2Interface.h>
 
-#include <libsolidity/interface/ReadFile.h>
-#include <liblangutil/Exceptions.h>
 #include <libdevcore/Keccak256.h>
 
 #include <boost/algorithm/string/join.hpp>
@@ -30,7 +28,6 @@
 #include <iostream>
 #include <memory>
 #include <stdexcept>
-#include <string>
 
 using namespace std;
 using namespace dev;
@@ -96,12 +93,12 @@ void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
 	}
 }
 
-void SMTLib2Interface::addAssertion(Expression const& _expr)
+void SMTLib2Interface::addAssertion(smt::Expression const& _expr)
 {
 	write("(assert " + toSExpr(_expr) + ")");
 }
 
-pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
+pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression> const& _expressionsToEvaluate)
 {
 	string response = querySolver(
 		boost::algorithm::join(m_accumulatedOutput, "\n") +
@@ -125,7 +122,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 	return make_pair(result, values);
 }
 
-string SMTLib2Interface::toSExpr(Expression const& _expr)
+string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 {
 	if (_expr.arguments.empty())
 		return _expr.name;
@@ -169,7 +166,7 @@ void SMTLib2Interface::write(string _data)
 	m_accumulatedOutput.back() += move(_data) + "\n";
 }
 
-string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> const& _expressionsToEvaluate)
 {
 	string command;
 	if (_expressionsToEvaluate.empty())

libsolidity/formal/SMTLib2Interface.h

@@ -50,21 +50,21 @@ public:
 
 	void declareVariable(std::string const&, Sort const&) override;
 
-	void addAssertion(Expression const& _expr) override;
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+	void addAssertion(smt::Expression const& _expr) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
 
 private:
 	void declareFunction(std::string const&, Sort const&);
 
-	std::string toSExpr(Expression const& _expr);
+	std::string toSExpr(smt::Expression const& _expr);
 	std::string toSmtLibSort(Sort const& _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
 	void write(std::string _data);
 
-	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
+	std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
 	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
 
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.

libsolidity/formal/SMTPortfolio.cpp

@@ -65,7 +65,7 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
 		s->declareVariable(_name, _sort);
 }
 
-void SMTPortfolio::addAssertion(Expression const& _expr)
+void SMTPortfolio::addAssertion(smt::Expression const& _expr)
 {
 	for (auto const& s: m_solvers)
 		s->addAssertion(_expr);
@@ -101,7 +101,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
  *
  *   If all solvers return ERROR, the result is ERROR.
 */
-pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate)
+pair<CheckResult, vector<string>> SMTPortfolio::check(vector<smt::Expression> const& _expressionsToEvaluate)
 {
 	CheckResult lastResult = CheckResult::ERROR;
 	vector<string> finalValues;

libsolidity/formal/SMTPortfolio.h

@@ -51,9 +51,9 @@ public:
 
 	void declareVariable(std::string const&, Sort const&) override;
 
-	void addAssertion(Expression const& _expr) override;
+	void addAssertion(smt::Expression const& _expr) override;
 
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override;
 	unsigned solvers() override { return m_solvers.size(); }
@@ -62,7 +62,7 @@ private:
 
 	std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
 
-	std::vector<Expression> m_assertions;
+	std::vector<smt::Expression> m_assertions;
 };
 
 }

libsolidity/formal/SolverInterface.h

@@ -17,6 +17,7 @@
 
 #pragma once
 
+#include <libsolidity/ast/Types.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/Exceptions.h>
 #include <libdevcore/Common.h>
@@ -45,7 +46,8 @@ enum class Kind
 	Int,
 	Bool,
 	Function,
-	Array
+	Array,
+	Sort
 };
 
 struct Sort
@@ -110,12 +112,33 @@ struct ArraySort: public Sort
 	SortPointer range;
 };
 
+struct SortSort: public Sort
+{
+	SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {}
+	bool operator==(Sort const& _other) const override
+	{
+		if (!Sort::operator==(_other))
+			return false;
+		auto _otherSort = dynamic_cast<SortSort const*>(&_other);
+		solAssert(_otherSort, "");
+		solAssert(_otherSort->inner, "");
+		solAssert(inner, "");
+		return *inner == *_otherSort->inner;
+	}
+
+	SortPointer inner;
+};
+
+// Forward declaration.
+SortPointer smtSort(solidity::Type const& _type);
+
 /// C++ representation of an SMTLIB2 expression.
 class Expression
 {
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
+	explicit Expression(solidity::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@@ -145,7 +168,8 @@ public:
 			{"/", 2},
 			{"mod", 2},
 			{"select", 2},
-			{"store", 3}
+			{"store", 3},
+			{"const_array", 2}
 		};
 		return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
 	}
@@ -202,6 +226,21 @@ public:
 		);
 	}
 
+	static Expression const_array(Expression _sort, Expression _value)
+	{
+		solAssert(_sort.sort->kind == Kind::Sort, "");
+		auto sortSort = std::dynamic_pointer_cast<SortSort>(_sort.sort);
+		auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
+		solAssert(sortSort && arraySort, "");
+		solAssert(_value.sort, "");
+		solAssert(*arraySort->range == *_value.sort, "");
+		return Expression(
+			"const_array",
+			std::vector<Expression>{std::move(_sort), std::move(_value)},
+			arraySort
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);

libsolidity/formal/SymbolicTypes.cpp

@@ -276,10 +276,31 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
-	if (isNumber(_type->category()))
-		_context.addAssertion(_expr == 0);
-	else if (isBool(_type->category()))
-		_context.addAssertion(_expr == Expression(false));
+	_context.addAssertion(_expr == zeroValue(_type));
+}
+
+Expression zeroValue(solidity::TypePointer const& _type)
+{
+	solAssert(_type, "");
+	if (isSupportedType(_type->category()))
+	{
+		if (isNumber(_type->category()))
+			return 0;
+		if (isBool(_type->category()))
+			return Expression(false);
+		if (isArray(_type->category()) || isMapping(_type->category()))
+		{
+			if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
+				return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType()));
+			auto mappingType = dynamic_cast<MappingType const*>(_type);
+			solAssert(mappingType, "");
+			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
+
+		}
+		solAssert(false, "");
+	}
+	// Unsupported types are abstracted as Int.
+	return 0;
 }
 
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context)

libsolidity/formal/SymbolicTypes.h

@@ -63,6 +63,7 @@ std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(solidity:
 
 Expression minValue(solidity::IntegerType const& _type);
 Expression maxValue(solidity::IntegerType const& _type);
+Expression zeroValue(solidity::TypePointer const& _type);
 
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
 void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context);

libsolidity/formal/Z3CHCInterface.cpp

@@ -33,6 +33,17 @@ Z3CHCInterface::Z3CHCInterface():
 	z3::set_param("rewriter.pull_cheap_ite", true);
 	// This needs to be set in the context.
 	m_context->set("timeout", queryTimeout);
+
+	// Spacer options.
+	// These needs to be set in the solver.
+	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
+	z3::params p(*m_context);
+	// These are useful for solving problems with arrays and loops.
+	// Use quantified lemma generalizer.
+	p.set("fp.spacer.q3.use_qgen", true);
+	// Ground pobs by using values from a model.
+	p.set("fp.spacer.ground_pobs", false);
+	m_solver.set(p);
 }
 
 void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort)
@@ -82,9 +93,11 @@ pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
 			break;
 		}
 		case z3::check_result::unknown:
+		{
 			result = CheckResult::UNKNOWN;
 			break;
 		}
+		}
 		// TODO retrieve model / invariants
 	}
 	catch (z3::exception const& _e)

libsolidity/formal/Z3Interface.cpp

@@ -132,6 +132,12 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 				return m_context.bool_val(true);
 			else if (n == "false")
 				return m_context.bool_val(false);
+			else if (_expr.sort->kind == Kind::Sort)
+			{
+				auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort);
+				solAssert(sortSort, "");
+				return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
+			}
 			else
 				try
 				{
@@ -178,6 +184,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return z3::select(arguments[0], arguments[1]);
 		else if (n == "store")
 			return z3::store(arguments[0], arguments[1], arguments[2]);
+		else if (n == "const_array")
+		{
+			shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
+			solAssert(sortSort, "");
+			auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
+			solAssert(arraySort && arraySort->domain, "");
+			return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
+		}
 
 		solAssert(false, "");
 	}

libsolidity/interface/ABI.cpp

@@ -40,7 +40,10 @@ bool anyDataStoredInStorage(TypePointers const& _pointers)
 
 Json::Value ABI::generate(ContractDefinition const& _contractDef)
 {
-	Json::Value abi(Json::arrayValue);
+	auto compare = [](Json::Value const& _a, Json::Value const& _b) -> bool {
+		return make_tuple(_a["type"], _a["name"]) < make_tuple(_b["type"], _b["name"]);
+	};
+	multiset<Json::Value, decltype(compare)> abi(compare);
 
 	for (auto it: _contractDef.interfaceFunctions())
 	{
@@ -71,7 +74,7 @@ Json::Value ABI::generate(ContractDefinition const& _contractDef)
 			it.second->returnParameterTypes(),
 			_contractDef.isLibrary()
 		);
-		abi.append(std::move(method));
+		abi.emplace(std::move(method));
 	}
 	if (_contractDef.constructor())
 	{
@@ -88,7 +91,7 @@ Json::Value ABI::generate(ContractDefinition const& _contractDef)
 			constrType.parameterTypes(),
 			_contractDef.isLibrary()
 		);
-		abi.append(std::move(method));
+		abi.emplace(std::move(method));
 	}
 	if (_contractDef.fallbackFunction())
 	{
@@ -98,7 +101,7 @@ Json::Value ABI::generate(ContractDefinition const& _contractDef)
 		method["type"] = "fallback";
 		method["payable"] = externalFunctionType->isPayable();
 		method["stateMutability"] = stateMutabilityToString(externalFunctionType->stateMutability());
-		abi.append(std::move(method));
+		abi.emplace(std::move(method));
 	}
 	for (auto const& it: _contractDef.interfaceEvents())
 	{
@@ -117,10 +120,13 @@ Json::Value ABI::generate(ContractDefinition const& _contractDef)
 			params.append(std::move(param));
 		}
 		event["inputs"] = std::move(params);
-		abi.append(std::move(event));
+		abi.emplace(std::move(event));
 	}
 
-	return abi;
+	Json::Value abiJson{Json::arrayValue};
+	for (auto& f: abi)
+		abiJson.append(std::move(f));
+	return abiJson;
 }
 
 Json::Value ABI::formatTypeList(