[SMTChecker] Zero-initialize arrays

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;

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, "");
 	}

test/libsolidity/SMTChecker.cpp

@@ -212,7 +212,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 			uint[] array;
 			function f(uint x, uint p) public {
 				require(x == 2);
-				require(array[p] == 10);
+				array[p] = 10;
 				array[p] /= array[p] / x;
 				assert(array[p] == x);
 				assert(array[p] == 0);
@@ -225,7 +225,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 			mapping (uint => uint) map;
 			function f(uint x, uint p) public {
 				require(x == 2);
-				require(map[p] == 10);
+				map[p] = 10;
 				map[p] /= map[p] / x;
 				assert(map[p] == x);
 				assert(map[p] == 0);

test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(array[p] == 100);
+		array[p] = 100;
 		array[p] += array[p] + x;
 		assert(array[p] < 300);
 		assert(array[p] < 110);
 	}
 }
 // ----
-// Warning: (202-224): Assertion violation happens here
+// Warning: (192-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(map[p] == 100);
+		map[p] = 100;
 		map[p] += map[p] + x;
 		assert(map[p] < 300);
 		assert(map[p] < 110);
 	}
 }
 // ----
-// Warning: (208-228): Assertion violation happens here
+// Warning: (198-218): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 10);
-		require(array[p] == 10);
+		array[p] = 10;
 		array[p] *= array[p] + x;
 		assert(array[p] <= 190);
 		assert(array[p] < 50);
 	}
 }
 // ----
-// Warning: (201-222): Assertion violation happens here
+// Warning: (191-212): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 10);
-		require(map[p] == 10);
+		map[p] = 10;
 		map[p] *= map[p] + x;
 		assert(map[p] <= 190);
 		assert(map[p] < 50);
 	}
 }
 // ----
-// Warning: (207-226): Assertion violation happens here
+// Warning: (197-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(array[p] == 200);
+		array[p] = 200;
 		array[p] -= array[p] - x;
 		assert(array[p] >= 0);
 		assert(array[p] < 90);
 	}
 }
 // ----
-// Warning: (201-222): Assertion violation happens here
+// Warning: (191-212): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(map[p] == 200);
+		map[p] = 200;
 		map[p] -= map[p] - x;
 		assert(map[p] >= 0);
 		assert(map[p] < 90);
 	}
 }
 // ----
-// Warning: (207-226): Assertion violation happens here
+// Warning: (197-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array.sol

@@ -10,12 +10,9 @@ contract C
 			delete a;
 		else
 			delete a[2];
-		// Assertion fails as false positive because
-		// setZeroValue for arrays needs \forall i . a[i] = 0
-		// which is still unimplemented.
 		assert(a[2] == 0);
+		assert(a[1] == 0);
 	}
 }
 // ----
 // Warning: (118-119): Condition is always true.
-// Warning: (297-314): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol

@@ -6,10 +6,6 @@ contract C
 	function f() public {
 		require(a[2][3] == 4);
 		delete a;
-		// Fails as false positive.
-		// setZeroValue needs forall for arrays.
 		assert(a[2][3] == 0);
 	}
 }
-// ----
-// Warning: (194-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol

@@ -9,11 +9,7 @@ contract C
 			delete a;
 		else
 			delete a[2];
-		// Fails as false positive since
-		// setZeroValue for arrays needs forall
-		// which is unimplemented.
 		assert(a[2][3] == 0);
+		assert(a[1][1] == 0);
 	}
 }
-// ----
-// Warning: (266-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_function.sol

@@ -16,12 +16,9 @@ contract C
 			g();
 		else
 			h();
-		// Assertion fails as false positive because
-		// setZeroValue for arrays needs \forall i . a[i] = 0
-		// which is still unimplemented.
 		assert(a[2] == 0);
+		assert(a[1] == 0);
 	}
 }
 // ----
 // Warning: (201-202): Condition is always true.
-// Warning: (367-384): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[][] array;
 	function f(uint x, uint y, uint z, uint t) public view {
-		require(array[x][y] == 200);
+		// TODO change to = 200 when 2d assignments are supported.
+		require(array[x][y] < 200);
 		require(x == z && y == t);
 		assert(array[z][t] > 300);
 	}
 }
 // ----
-// Warning: (183-208): Assertion violation happens here
+// Warning: (243-268): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[][][] array;
 	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
-		require(array[x][y][z] == 200);
+		// TODO change to = 200 when 3d assignments are supported.
+		require(array[x][y][z] < 200);
 		require(x == t && y == w && z == v);
 		assert(array[t][w][v] > 300);
 	}
 }
 // ----
-// Warning: (214-242): Assertion violation happens here
+// Warning: (274-302): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol

@@ -4,10 +4,10 @@ contract C
 {
 	uint[10][20] array;
 	function f(uint x, uint y, uint z, uint t) public view {
-		require(array[x][y] == 200);
+		require(array[x][y] < 200);
 		require(x == z && y == t);
 		assert(array[z][t] > 300);
 	}
 }
 // ----
-// Warning: (187-212): Assertion violation happens here
+// Warning: (186-211): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[10][20][30] array;
 	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
-		require(array[x][y][z] == 200);
+		// TODO change to = 200 when 3d assignments are supported.
+		require(array[x][y][z] < 200);
 		require(x == t && y == w && z == v);
 		assert(array[t][w][v] > 300);
 	}
 }
 // ----
-// Warning: (220-248): Assertion violation happens here
+// Warning: (280-308): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/mapping_4.sol

@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning: (125-144): Assertion violation happens here