Merge pull request #9521 from ethereum/smt_fix_array_name

[SMTChecker] Fix tuple name for arrays

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
 Bugfixes:
  * Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though.
  * SMTChecker: Fix internal error in BMC function inlining.
+ * SMTChecker: Fix internal error on array implicit conversion.
  * SMTChecker: Fix internal error on fixed bytes index access.
  * References Resolver: Fix internal bug when using constructor for library.
 

libsolidity/formal/SymbolicTypes.cpp

@@ -92,13 +92,35 @@ SortPointer smtSort(frontend::Type const& _type)
 		string tupleName;
 		if (
 			auto arrayType = dynamic_cast<ArrayType const*>(&_type);
-			(arrayType && arrayType->isString()) ||
+			(arrayType && (arrayType->isString() || arrayType->isByteArray())) ||
 			_type.category() == frontend::Type::Category::ArraySlice ||
 			_type.category() == frontend::Type::Category::StringLiteral
 		)
-			tupleName = "bytes_tuple";
+			tupleName = "bytes";
+		else if (auto arrayType = dynamic_cast<ArrayType const*>(&_type))
+		{
+			auto baseType = arrayType->baseType();
+			// Solidity allows implicit conversion also when assigning arrays.
+			// So if the base type potentially has a size, that size cannot go
+			// in the tuple's name.
+			if (auto tupleSort = dynamic_pointer_cast<TupleSort>(array->range))
+				tupleName = tupleSort->name;
+			else if (
+				baseType->category() == frontend::Type::Category::Integer ||
+				baseType->category() == frontend::Type::Category::FixedPoint
+			)
+				tupleName = "uint";
+			else if (baseType->category() == frontend::Type::Category::FixedBytes)
+				tupleName = "fixedbytes";
+			else
+				tupleName = arrayType->baseType()->toString(true);
+
+			tupleName += "[]";
+		}
 		else
-			tupleName = _type.toString(true) + "_tuple";
+			tupleName = _type.toString(true);
+
+		tupleName += "_tuple";
 
 		return make_shared<TupleSort>(
 			tupleName,

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -20,6 +20,9 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: cvc4
 // ----
-// Warning 6328: (320-339): Assertion violation happens here
+// Warning 4661: (296-316): Assertion violation happens here
-// Warning 6328: (343-362): Assertion violation happens here.
+// Warning 4661: (320-339): Assertion violation happens here
+// Warning 4661: (343-362): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol

@@ -26,4 +26,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (400-457): Assertion violation happens here
+// Warning 6328: (400-457): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/static_array_implicit_push_1.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	uint[][] a;
+	function f(uint[1] memory x) public {
+		a.push(x);
+	}
+}

test/libsolidity/smtCheckerTests/types/static_array_implicit_push_2.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	uint[][] a;
+	function f(uint[1][] memory x) public {
+		a.push(x[2]);
+	}
+}

test/libsolidity/smtCheckerTests/types/static_array_implicit_push_3.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract D {
+	bytes16[] inner;
+	bytes32[][] data;
+	function t() public {
+		data.push(inner);
+	}
+}
+

test/libsolidity/smtCheckerTests/types/static_array_implicit_push_4.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract D {
+	int16[] inner;
+	int[][] data;
+	function t() public {
+		data.push(inner);
+	}
+}
+