From ac528cfd1b3df08ccda9c3cb93d5ab3b9bf97891 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 30 Aug 2021 16:56:42 +0200 Subject: [PATCH] add static array length constraint --- libsolidity/formal/SymbolicTypes.cpp | 5 ++++ .../types/array_static_aliasing_memory_5.sol | 6 +---- .../types/array_static_aliasing_storage_5.sol | 5 ---- .../types/array_static_mapping_aliasing_1.sol | 3 --- .../types/array_static_mapping_aliasing_2.sol | 4 ---- .../types/static_array_length_1.sol | 12 ++++++++++ .../types/static_array_length_2.sol | 12 ++++++++++ .../types/static_array_length_3.sol | 13 +++++++++++ .../types/static_array_length_4.sol | 23 +++++++++++++++++++ .../types/static_array_length_5.sol | 13 +++++++++++ 10 files changed, 79 insertions(+), 17 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/static_array_length_1.sol create mode 100644 test/libsolidity/smtCheckerTests/types/static_array_length_2.sol create mode 100644 test/libsolidity/smtCheckerTests/types/static_array_length_3.sol create mode 100644 test/libsolidity/smtCheckerTests/types/static_array_length_4.sol create mode 100644 test/libsolidity/smtCheckerTests/types/static_array_length_5.sol diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index a4c46604c..ba82a1666 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -551,6 +551,11 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte solAssert(_type, ""); if (isEnum(*_type) || isInteger(*_type) || isAddress(*_type) || isFixedBytes(*_type)) return _expr >= minValue(_type) && _expr <= maxValue(_type); + else if ( + auto arrayType = dynamic_cast(_type); + arrayType && !arrayType->isDynamicallySized() + ) + return smtutil::Expression::tuple_get(_expr, 1) == arrayType->length(); else if (isArray(*_type) || isMapping(*_type)) /// Length cannot be negative. return smtutil::Expression::tuple_get(_expr, 1) >= 0; diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol index 15b7aed31..eb7ae6a35 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol @@ -1,9 +1,6 @@ contract C { function f(uint[2] memory a, uint[2] memory b, uint[2] memory c) public pure { - require(a.length > 0); - require(b.length > 0); - require(c.length > 0); require(c[0] == 42); require(a[0] == 2); b[0] = 1; @@ -19,5 +16,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6368: (467-471): CHC: Out of bounds access happens here. -// Warning 6328: (460-477): CHC: Assertion violation happens here. +// Warning 6328: (385-402): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol index 8841942d7..4592e9526 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol @@ -24,8 +24,3 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6368: (165-169): CHC: Out of bounds access happens here. -// Warning 6368: (178-182): CHC: Out of bounds access happens here. -// Warning 6368: (190-195): CHC: Out of bounds access happens here. -// Warning 6368: (314-318): CHC: Out of bounds access happens here. -// Warning 6368: (440-445): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol index 61b7a80f2..cde229e4f 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -27,7 +27,4 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6368: (353-369): CHC: Out of bounds access happens here. -// Warning 6368: (353-372): CHC: Out of bounds access happens here. -// Warning 6368: (463-477): CHC: Out of bounds access happens here. // Warning 6328: (456-487): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index 1c9b9e23b..8ebd7025d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -30,10 +30,6 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6368: (314-328): CHC: Out of bounds access happens here. -// Warning 6368: (367-383): CHC: Out of bounds access happens here. -// Warning 6368: (367-386): CHC: Out of bounds access happens here. -// Warning 6368: (497-511): CHC: Out of bounds access happens here. // Warning 6328: (860-880): CHC: Assertion violation happens here. // Warning 6368: (936-952): CHC: Out of bounds access might happen here. // Warning 6368: (936-955): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol new file mode 100644 index 000000000..dd7b8abd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol @@ -0,0 +1,12 @@ +contract C { + function f(address[2] memory a) public pure { + assert(a.length == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (102-122): CHC: Assertion violation happens here.\nCounterexample:\n\na = [9, 9]\n\nTransaction trace:\nC.constructor()\nC.f([9, 9]) +// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [9, 9]\n\nTransaction trace:\nC.constructor()\nC.f([9, 9]) diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol new file mode 100644 index 000000000..11ba621d2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol @@ -0,0 +1,12 @@ +contract C { + function f() public pure returns (address[2] memory a) { + assert(a.length == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (113-133): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (152-172): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol new file mode 100644 index 000000000..b5f47414c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol @@ -0,0 +1,13 @@ +contract C { + function f() public pure { + address[2] memory a; + assert(a.length == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (106-126): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (145-165): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_4.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_4.sol new file mode 100644 index 000000000..13efd8bb9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_4.sol @@ -0,0 +1,23 @@ +contract C { + uint[2] a; + uint x = f(); + constructor() { + assert(a.length == 2); // should hold + assert(x == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + } + function f() internal view returns (uint) { + assert(a.length == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + return a.length; + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (132-152): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0], x = 2\n\nTransaction trace:\nC.constructor() +// Warning 6328: (171-191): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0], x = 2\n\nTransaction trace:\nC.constructor() +// Warning 6328: (298-318): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0], x = 0\n\nTransaction trace:\nC.constructor() +// Warning 6328: (337-357): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0], x = 0\n\nTransaction trace:\nC.constructor() diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol new file mode 100644 index 000000000..f632f3bc8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol @@ -0,0 +1,13 @@ +contract C { + uint[2] a; + function f() public view { + assert(a.length == 2); // should hold + assert(a.length < 2); // should fail + assert(a.length > 2); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (95-115): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f() +// Warning 6328: (134-154): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f()