cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix internal error when using user defined value types as mapping indices or struct members.

Browse Source
This commit is contained in:
Leo Alt 2022-11-29 13:00:51 +01:00
parent cc8baf7ea8
commit 608b424afc
10 changed files with 192 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -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)

5
libsolidity/formal/SMTEncoder.cpp
View File

@ -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;
}
}

32
libsolidity/formal/SymbolicTypes.cpp
View File

@ -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

16
test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol Normal file
View File

@ -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.

16
test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_2.sol Normal file
View File

@ -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()

25
test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_1.sol Normal file
View File

@ -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
}
}

33
test/libsolidity/smtCheckerTests/userTypes/user_type_as_library_constant_2.sol Normal file
View File

@ -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()

20
test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_1.sol Normal file
View File

@ -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)

20
test/libsolidity/smtCheckerTests/userTypes/user_type_as_mapping_index_2.sol Normal file
View File

@ -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)

25
test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol Normal file
View File

@ -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)
);
}
}