From 608b424afcd2339367ab60d24a591defc0ef8f68 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 29 Nov 2022 13:00:51 +0100 Subject: [PATCH] Fix internal error when using user defined value types as mapping indices or struct members. --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 5 ++- libsolidity/formal/SymbolicTypes.cpp | 32 ++++++++++++++++++ .../userTypes/user_type_as_array_elem_1.sol | 16 +++++++++ .../userTypes/user_type_as_array_elem_2.sol | 16 +++++++++ .../user_type_as_library_constant_1.sol | 25 ++++++++++++++ .../user_type_as_library_constant_2.sol | 33 +++++++++++++++++++ .../user_type_as_mapping_index_1.sol | 20 +++++++++++ .../user_type_as_mapping_index_2.sol | 20 +++++++++++ .../user_type_as_struct_member_1.sol | 25 ++++++++++++++ 10 files changed, 192 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_2.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_1.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_2.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_1.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_2.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol diff --git a/Changelog.md b/Changelog.md index a78a8a5c5..f075e4c32 100644 --- a/Changelog.md +++ b/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) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8d758e784..adae21412 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1403,7 +1403,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) { if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) { - defineExpr(_memberAccess, currentValue(*var)); + if (var->isConstant()) + defineExpr(_memberAccess, constantExpr(_memberAccess, *var)); + else + defineExpr(_memberAccess, currentValue(*var)); return false; } } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index e40ff9245..d40b51cea 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -35,6 +35,9 @@ namespace solidity::frontend::smt SortPointer smtSort(frontend::Type const& _type) { + if (auto userType = dynamic_cast(&_type)) + return smtSort(userType->underlyingType()); + switch (smtKind(_type)) { case Kind::Int: @@ -194,6 +197,9 @@ vector smtSortAbstractFunction(vector const& Kind smtKind(frontend::Type const& _type) { + if (auto userType = dynamic_cast(&_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(&_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(_type)) + return minValue(&userType->underlyingType()); + solAssert(isNumber(*_type), ""); if (auto const* intType = dynamic_cast(_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(_type)) + return maxValue(&userType->underlyingType()); + solAssert(isNumber(*_type), ""); if (auto const* intType = dynamic_cast(_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(_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(_type)) + return isSigned(&userType->underlyingType()); + solAssert(smt::isNumber(*_type), ""); bool isSigned = false; if (auto const* numberType = dynamic_cast(_type)) @@ -530,6 +552,9 @@ bool isSigned(frontend::Type const* _type) pair typeBvSizeAndSignedness(frontend::Type const* _type) { + if (auto userType = dynamic_cast(_type)) + return typeBvSizeAndSignedness(&userType->underlyingType()); + if (auto const* intType = dynamic_cast(_type)) return {intType->numBits(), intType->isSigned()}; else if (auto const* fixedType = dynamic_cast(_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(_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 symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to) { + if (auto userType = dynamic_cast(_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 diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol new file mode 100644 index 000000000..55a88fd7e --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_2.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_2.sol new file mode 100644 index 000000000..8ac649366 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_1.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_1.sol new file mode 100644 index 000000000..3088a894b --- /dev/null +++ b/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 + } +} diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_2.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_2.sol new file mode 100644 index 000000000..5b7ebe257 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_1.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_1.sol new file mode 100644 index 000000000..f1b6a7986 --- /dev/null +++ b/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) diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_2.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_2.sol new file mode 100644 index 000000000..1e53a3547 --- /dev/null +++ b/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) diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol new file mode 100644 index 000000000..1a72cad3d --- /dev/null +++ b/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) + ); + } +}