Merge pull request #14980 from ethereum/smt-int-sorts-compatibility

SMTChecker: Relax assertions regarding sort compatibility when creating expressions

Author: blishko

Diff for: Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * 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 bitwise operators with an array element as argument.
 
 

Diff for: libsmtutil/SolverInterface.h

@@ -189,10 +189,7 @@ class Expression
 
 	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
 	{
-		if (_trueValue.sort->kind == Kind::Int)
-			smtAssert(_trueValue.sort->kind == _falseValue.sort->kind, "");
-		else
-			smtAssert(*_trueValue.sort == *_falseValue.sort, "");
+		smtAssert(areCompatible(*_trueValue.sort, *_falseValue.sort));
 		SortPointer sort = _trueValue.sort;
 		return Expression("ite", std::vector<Expression>{
 			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
@@ -216,10 +213,7 @@ class Expression
 		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		smtAssert(arraySort, "");
 		smtAssert(_index.sort, "");
-		if (arraySort->domain->kind == Kind::Int)
-			smtAssert(arraySort->domain->kind == _index.sort->kind, "");
-		else
-			smtAssert(*arraySort->domain == *_index.sort, "");
+		smtAssert(areCompatible(*arraySort->domain, *_index.sort));
 		return Expression(
 			"select",
 			std::vector<Expression>{std::move(_array), std::move(_index)},
@@ -235,11 +229,8 @@ class Expression
 		smtAssert(arraySort, "");
 		smtAssert(_index.sort, "");
 		smtAssert(_element.sort, "");
-		smtAssert(*arraySort->domain == *_index.sort, "");
-		if (arraySort->domain->kind == Kind::Int)
-			smtAssert(arraySort->range->kind == _element.sort->kind, "");
-		else
-			smtAssert(*arraySort->range == *_element.sort, "");
+		smtAssert(areCompatible(*arraySort->domain, *_index.sort));
+		smtAssert(areCompatible(*arraySort->range, *_element.sort));
 		return Expression(
 			"store",
 			std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
@@ -254,10 +245,7 @@ class Expression
 		auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
 		smtAssert(sortSort && arraySort, "");
 		smtAssert(_value.sort, "");
-		if (arraySort->domain->kind == Kind::Int)
-			smtAssert(arraySort->range->kind == _value.sort->kind, "");
-		else
-			smtAssert(*arraySort->range == *_value.sort, "");
+		smtAssert(areCompatible(*arraySort->range, *_value.sort));
 		return Expression(
 			"const_array",
 			std::vector<Expression>{std::move(_sort), std::move(_value)},
@@ -501,6 +489,12 @@ class Expression
 	SortPointer sort;
 
 private:
+	/// Helper method for checking sort compatibility when creating expressions
+	/// Signed and unsigned Int sorts are compatible even though they are not same
+	static bool areCompatible(Sort const& s1, Sort const& s2)
+	{
+		return s1.kind == Kind::Int ? s1.kind == s2.kind : s1 == s2;
+	}
 	/// Manual constructors, should only be used by SolverInterface and this class itself.
 	Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
 		Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}

Diff for: test/libsolidity/smtCheckerTests/types/mapping_integer_signedness_compatibility.sol

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: GPL-3.0
+
+
+// Regression for handling signedness, see issue #14792
+contract C {
+    mapping(int => int) v1;
+    mapping(int => uint) v2;
+    mapping(uint => int) v3;
+    mapping(uint => uint) v4;
+    mapping(bytes12 => int) v5;
+    uint[5] a1;
+    int[5] a2;
+
+    function f() public {
+        delete v1[0];
+        delete v2[0];
+        delete v3[0];
+        delete v4[0];
+        delete v5[0];
+        delete a1[0];
+        delete a2[0];
+    }
+}
+// ----
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.