SMTChecker: Fix equality of array literals

There are two kinds of array literals in Solidity: string literals
(arrays of characters/bytes) and proper array literals (e.g., [1,2,3]).
While array literals cannot be directly tested for equality in Solidity,
it is possible to compute hash of these values and compare hashes.
The expectation is that hashes of the same array literals would be the
same, but previously SMTChecker returned false positive in this case,
saying that they don't have to be equal.

The reason for the false positive was the following.
We represent Solidity array literal as a tuple `(elements, length)` where
`length` is an integer representing the actualy length of the array
literal, and `elements` are an SMT-LIB array, where the first `length`
elements represent the actual content of the array literal.
However, SMT-LIB arrays are infinite objects (more like functions from
indices to elements). Previously, we left the part after `length`-th
element unspecified. For the solver this meant that two array literals
equal at the Solidity level were represented with two different SMT-LIB
arrays.

The proposed solution is to always start from a constant-zero array, and
use store operations to build an SMT-LIB array that matches the Solidity
array literal.

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence.
+ * SMTChecker: Fix false positive when comparing hashes of same array or string literals.
  * SMTChecker: Fix internal error on mapping access caused by too strong requirements on sort compatibility of the index and mapping domain.
  * SMTChecker: Fix internal error when using an empty tuple in a conditional operator.
  * SMTChecker: Fix internal error when using bitwise operators with an array element as argument.

libsolidity/formal/SMTEncoder.cpp

@@ -1296,8 +1296,27 @@ void SMTEncoder::addArrayLiteralAssertions(
 )
 {
 	m_context.addAssertion(_symArray.length() == _elementValues.size());
+
+	// Assert to the solver that _elementValues are exactly the elements at the beginning of the array.
+	// Since we create new symbolic representation for every array literal in the source file, we want to ensure that
+	// representations of two equal literals are also equal. For this reason we always start from constant-zero array.
+	// This ensures SMT-LIB arrays (which are infinite) are also equal beyond the length of the Solidity array literal.
+	auto type = _symArray.type();
+	smtAssert(type);
+	auto valueType = [&]() {
+		if (auto const* arrayType = dynamic_cast<ArrayType const*>(type))
+			return arrayType->baseType();
+		if (smt::isStringLiteral(*type))
+			return TypeProvider::stringMemory()->baseType();
+		smtAssert(false);
+	}();
+	auto tupleSort = std::dynamic_pointer_cast<smtutil::TupleSort>(smt::smtSort(*type));
+	auto sortSort = std::make_shared<smtutil::SortSort>(tupleSort->components.front());
+	smtutil::Expression arrayExpr = smtutil::Expression::const_array(smtutil::Expression(sortSort), smt::zeroValue(valueType));
+	smtAssert(arrayExpr.sort->kind == smtutil::Kind::Array);
 	for (size_t i = 0; i < _elementValues.size(); i++)
-		m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
+		arrayExpr = smtutil::Expression::store(arrayExpr, smtutil::Expression(i), _elementValues[i]);
+	m_context.addAssertion(_symArray.elements() == arrayExpr);
 }
 
 void SMTEncoder::bytesToFixedBytesAssertions(

test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_array.sol

@@ -0,0 +1,23 @@
+contract C {
+	function c1() public pure {
+		bytes32 k1 = keccak256(abi.encode([1]));
+		bytes32 k2 = keccak256(abi.encode([1]));
+		assert(k1 == k2);
+	}
+
+        function c2() public pure {
+		bytes32 s1 = sha256(abi.encode([1,2]));
+		bytes32 s2 = sha256(abi.encode([1,2]));
+		assert(s1 == s2);
+	}
+
+        function c3() public pure {
+		bytes32 r1 = ripemd160(abi.encode([1,2,3]));
+		bytes32 r2 = ripemd160(abi.encode([1,2,3]));
+		assert(r1 == r2);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol

@@ -0,0 +1,23 @@
+contract C {
+	function c1() public pure {
+		bytes32 k1 = keccak256("1");
+		bytes32 k2 = keccak256("1");
+		assert(k1 == k2);
+	}
+
+        function c2() public pure {
+		bytes32 s1 = sha256("10");
+		bytes32 s2 = sha256("10");
+		assert(s1 == s2);
+	}
+
+        function c3() public pure {
+		bytes32 r1 = ripemd160("100");
+		bytes32 r2 = ripemd160("100");
+		assert(r1 == r2);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol

@@ -24,4 +24,4 @@ contract C {
 // SMTIgnoreCex: no
 // ----
 // Warning 9302: (212-228): Return value of low-level calls not used.
-// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(0) -- reentrant call
+// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(1) -- reentrant call

test/libsolidity/smtCheckerTests/types/array_literal_3.sol

@@ -11,5 +11,5 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: no
 // ----
-// Warning 6328: (168-188): CHC: Assertion violation happens here.
+// Warning 6328: (168-188): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4]\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.