Merge pull request #13761 from ethereum/smt_fix_user

Fix internal error when using user defined value types in map/struct

Changelog.md

@@ -26,6 +26,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when a public library function is called internally.
  * SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries.
  * SMTChecker: Fix internal error on chain assignments using static fully specified state variables.
+ * SMTChecker: Fix internal error when using user defined types as mapping indices or struct members.
 
 
 ### 0.8.17 (2022-09-08)

libsolidity/formal/SMTEncoder.cpp

@@ -1403,7 +1403,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		{
 			if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
 			{
-				defineExpr(_memberAccess, currentValue(*var));
+				if (var->isConstant())
+					defineExpr(_memberAccess, constantExpr(_memberAccess, *var));
+				else
+					defineExpr(_memberAccess, currentValue(*var));
 				return false;
 			}
 		}

libsolidity/formal/SymbolicTypes.cpp

@@ -35,6 +35,9 @@ namespace solidity::frontend::smt
 
 SortPointer smtSort(frontend::Type const& _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(&_type))
+		return smtSort(userType->underlyingType());
+
 	switch (smtKind(_type))
 	{
 	case Kind::Int:
@@ -194,6 +197,9 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::Type const*> const&
 
 Kind smtKind(frontend::Type const& _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(&_type))
+		return smtKind(userType->underlyingType());
+
 	if (isNumber(_type))
 		return Kind::Int;
 	else if (isBool(_type))
@@ -210,6 +216,9 @@ Kind smtKind(frontend::Type const& _type)
 
 bool isSupportedType(frontend::Type const& _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(&_type))
+		return isSupportedType(userType->underlyingType());
+
 	return isNumber(_type) ||
 		isBool(_type) ||
 		isMapping(_type) ||
@@ -402,6 +411,9 @@ smtutil::Expression minValue(frontend::IntegerType const& _type)
 
 smtutil::Expression minValue(frontend::Type const* _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return minValue(&userType->underlyingType());
+
 	solAssert(isNumber(*_type), "");
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
 		return intType->minValue();
@@ -424,6 +436,9 @@ smtutil::Expression maxValue(frontend::IntegerType const& _type)
 
 smtutil::Expression maxValue(frontend::Type const* _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return maxValue(&userType->underlyingType());
+
 	solAssert(isNumber(*_type), "");
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
 		return intType->maxValue();
@@ -455,6 +470,10 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::Type const* _type
 smtutil::Expression zeroValue(frontend::Type const* _type)
 {
 	solAssert(_type, "");
+
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return zeroValue(&userType->underlyingType());
+
 	if (isSupportedType(*_type))
 	{
 		if (isNumber(*_type))
@@ -507,6 +526,9 @@ smtutil::Expression zeroValue(frontend::Type const* _type)
 
 bool isSigned(frontend::Type const* _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return isSigned(&userType->underlyingType());
+
 	solAssert(smt::isNumber(*_type), "");
 	bool isSigned = false;
 	if (auto const* numberType = dynamic_cast<RationalNumberType const*>(_type))
@@ -530,6 +552,9 @@ bool isSigned(frontend::Type const* _type)
 
 pair<unsigned, bool> typeBvSizeAndSignedness(frontend::Type const* _type)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return typeBvSizeAndSignedness(&userType->underlyingType());
+
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
 		return {intType->numBits(), intType->isSigned()};
 	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
@@ -553,6 +578,10 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _t
 smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type)
 {
 	solAssert(_type, "");
+
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
+		return symbolicUnknownConstraints(std::move(_expr), &userType->underlyingType());
+
 	if (isEnum(*_type) || isInteger(*_type) || isAddress(*_type) || isFixedBytes(*_type))
 		return _expr >= minValue(_type) && _expr <= maxValue(_type);
 	else if (
@@ -569,6 +598,9 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
 
 optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to)
 {
+	if (auto userType = dynamic_cast<UserDefinedValueType const*>(_to))
+		return symbolicTypeConversion(_from, &userType->underlyingType());
+
 	if (_to && _from)
 		// StringLiterals are encoded as SMT arrays in the generic case,
 		// but they can also be compared/assigned to fixed bytes, in which

test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol

@@ -0,0 +1,16 @@
+contract C {
+    type T is address;
+    T[] arr;
+
+    function p() public {
+        arr.push(T.wrap(address(42)));
+    }
+
+    function inv(uint i) external view {
+        require(i < arr.length);
+        assert(T.unwrap(arr[i]) == address(42)); // should hold
+    }
+}
+// ----
+// Warning 6328: (204-243): CHC: Assertion violation might happen here.
+// Warning 4661: (204-243): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_2.sol

@@ -0,0 +1,16 @@
+contract C {
+    type T is address;
+    T[] arr;
+
+    function p() public {
+        arr.push(T.wrap(address(42)));
+    }
+
+    function inv2() external view {
+        if (arr.length > 0) {
+            assert(T.unwrap(arr[0]) == address(0)); // should fail
+        }
+    }
+}
+// ----
+// Warning 6328: (200-238): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.p()\nC.inv2()

test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_1.sol

@@ -0,0 +1,25 @@
+type T is bool;
+library L{
+    T constant c = T.wrap(true);
+    uint constant z = 42;
+}
+T constant g = T.wrap(true);
+
+contract C {
+    T constant b = T.wrap(true);
+    uint constant X = 42;
+
+    function f() external pure {
+        T x = T.wrap(true);
+        assert(T.unwrap(x)); // should hold
+
+        assert(L.z == 42); // should hold
+        assert(T.unwrap(L.c)); // should hold
+
+        assert(T.unwrap(g)); // should hold
+
+        assert(C.X == 42); // should hold
+        assert(T.unwrap(b)); // should hold
+        assert(T.unwrap(C.b)); // should hold
+    }
+}

test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_2.sol

@@ -0,0 +1,33 @@
+type T is bool;
+library L{
+    T constant c = T.wrap(false);
+    uint constant z = 43;
+}
+T constant g = T.wrap(false);
+
+contract C {
+    T constant b = T.wrap(false);
+    uint constant X = 43;
+
+    function f() external pure {
+        T x = T.wrap(false);
+        assert(T.unwrap(x)); // should fail
+
+        assert(L.z == 42); // should fail
+        assert(T.unwrap(L.c)); // should fail
+
+        assert(T.unwrap(g)); // should fail
+
+        assert(C.X == 42); // should fail
+        assert(T.unwrap(b)); // should fail
+        assert(T.unwrap(C.b)); // should fail
+    }
+}
+// ----
+// Warning 6328: (264-283): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (309-326): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (351-372): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (398-417): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (443-460): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (485-504): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()
+// Warning 6328: (529-550): CHC: Assertion violation happens here.\nCounterexample:\nX = 43\n\nTransaction trace:\nC.constructor()\nState: X = 43\nC.f()

test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_1.sol

@@ -0,0 +1,20 @@
+contract C {
+    type T is bool;
+    mapping (T => uint) s;
+
+    constructor() {
+        s[C.T.wrap(true)] = 42;
+        s[C.T.wrap(false)] = 2;
+    }
+
+    function f(bool b) external view {
+        assert(s[C.T.wrap(b)] > 0); // should hold
+    }
+
+    function g(T b) external view {
+        require(C.T.unwrap(b));
+        assert(s[b] == 2); // should fail
+    }
+}
+// ----
+// Warning 6328: (325-342): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\n\nTransaction trace:\nC.constructor()\nC.g(true)

test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_2.sol

@@ -0,0 +1,20 @@
+contract C {
+    type T is address;
+    mapping (T => uint) s;
+
+    constructor() {
+        s[T.wrap(address(0))] = 42;
+    }
+
+    function f(address a) external view {
+        require(a != address(0));
+        assert(s[C.T.wrap(a)] == 0); // should hold
+    }
+
+    function g(T a) external view {
+        require(C.T.unwrap(a) == address(0));
+        assert(s[a] != 42); // should fail
+    }
+}
+// ----
+// Warning 6328: (352-370): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)

test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol

@@ -0,0 +1,25 @@
+contract C {
+    type T is address;
+
+    struct S {
+        T a;
+        uint x;
+    }
+
+    mapping (T => S) m;
+
+    constructor() {
+        m[T.wrap(address(0))] = S(T.wrap(address(0)), 0);
+    }
+
+    function set(address _a) external {
+        m[T.wrap(_a)] = S(T.wrap(_a), 0);
+    }
+
+    function inv(T t) external view {
+        assert( // should hold
+            T.unwrap(m[t].a) == T.unwrap(t) ||
+            T.unwrap(m[t].a) == address(0)
+        );
+    }
+}