Fix SMT logic error when assigning to an array of contracts or functions (#15322)

Author: pgebal

Changelog.md

@@ -28,6 +28,7 @@ Bugfixes:
  * SMTChecker: Fix error that reports invalid number of verified checks for BMC and CHC engines.
  * SMTChecker: Fix formatting of unary minus expressions in invariants.
  * SMTChecker: Fix internal compiler error when reporting proved targets for BMC engine.
+ * SMTChecker: Fix SMT logic error when assigning to an array of contracts or functions.
  * TypeChecker: Fix segfault when assigning nested tuple to tuple.
  * Yul AST: Fix ``nativeSrc`` attributes in optimized IR AST referring to locations in unoptimized IR.
  * Yul IR Code Generation: Deterministic order of Yul subobjects.

libsolidity/formal/SymbolicTypes.cpp

@@ -110,6 +110,14 @@ SortPointer smtSort(frontend::Type const& _type)
 			// in the tuple's name.
 			if (auto tupleSort = std::dynamic_pointer_cast<TupleSort>(array->range))
 				tupleName = tupleSort->name;
+			else if (isContract(*baseType))
+				// use a common sort for contracts so inheriting contracts do not cause conflicting SMT types
+				// solc handles types mismtach
+				tupleName = "contract";
+			else if (isFunction(*baseType))
+				// use a common sort for functions so pure and view modifier do not cause conflicting SMT types
+				// solc handles types mismtach
+				tupleName = "function";
 			else if (
 				baseType->category() == frontend::Type::Category::Integer ||
 				baseType->category() == frontend::Type::Category::FixedPoint

test/libsolidity/smtCheckerTests/types/array_of_contracts.sol

@@ -0,0 +1,17 @@
+contract A {}
+
+contract B is A {}
+
+contract C {
+	A[10] a;
+	B[10] b;
+
+	function f() public returns(address) {
+		a = b;
+		return address(a[0]);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_of_functions.sol

@@ -0,0 +1,16 @@
+contract C {
+	function() external returns(uint)[1] a;
+
+	function b() external pure returns(uint) {
+		return 1;
+	}
+
+	function test() public returns(uint) {
+		a = [this.b];
+		return a[0]();
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.