Merge pull request #15701 from ethereum/smt-fix-array-of-strings

SMTChecker: Fix error when initializing fixed-sized-bytes array

Changelog.md

@@ -9,9 +9,10 @@ Compiler Features:
 
 
 Bugfixes:
-* General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
-* Standard JSON Interface: Fix ``generatedSources`` and ``sourceMap`` being generated internally even when not requested.
-* Yul: Fix internal compiler error when a code generation error should be reported instead.
+ * General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
+ * SMTChecker: Fix SMT logic error when initializing a fixed-sized-bytes array using string literals.
+ * Standard JSON Interface: Fix ``generatedSources`` and ``sourceMap`` being generated internally even when not requested.
+ * Yul: Fix internal compiler error when a code generation error should be reported instead.
 
 
 ### 0.8.28 (2024-10-09)

libsolidity/formal/SMTEncoder.cpp

@@ -428,9 +428,11 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 	{
 		// Add constraints for the length and values as it is known.
 		auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
-		solAssert(symbArray, "");
-
-		addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
+		smtAssert(symbArray, "Inline array must be represented with SymbolicArrayVariable");
+		auto originalType = symbArray->originalType();
+		auto arrayType = dynamic_cast<ArrayType const*>(originalType);
+		smtAssert(arrayType, "Type of inline array must be ArrayType");
+		addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c, arrayType->baseType()); }));
 	}
 	else
 	{

test/libsolidity/smtCheckerTests/typecast/fixed_bytes_array_from_strig_inline_array.sol

@@ -0,0 +1,14 @@
+contract D {
+    function test() public pure {
+        bytes7[2] memory dummyBytes = [bytes7("A"), "B"];
+        assert(uint56(dummyBytes[0]) == 0x41000000000000);
+        assert(uint56(dummyBytes[1]) == 0x42000000000000);
+        assert(uint56(dummyBytes[1]) == 0x41000000000000); // Should fail
+    }
+}
+// ====
+// SMTEngine: chc
+// SMTTargets: assert
+// ----
+// Warning 6328: (231-280): CHC: Assertion violation happens here.\nCounterexample:\n\ndummyBytes = [0x41000000000000, 0x42000000000000]\n\nTransaction trace:\nD.constructor()\nD.test()
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.