cerc-io/solidity
10
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

Merge pull request #11860 from ethereum/smt_static_array

Browse Source 
[SMTChecker] Add static array length constraint
This commit is contained in:
Leonardo 2021-08-30 19:07:21 +02:00 committed by GitHub
commit 78afd71ab7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 79 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SymbolicTypes.cpp
View File

@ -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<ArrayType const*>(_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;

6
test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol
View File

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

5
test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol
View File

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

3
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View File

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

4
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View File

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

12
test/libsolidity/smtCheckerTests/types/static_array_length_1.sol Normal file
View File

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

12
test/libsolidity/smtCheckerTests/types/static_array_length_2.sol Normal file
View File

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

13
test/libsolidity/smtCheckerTests/types/static_array_length_3.sol Normal file
View File

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

23
test/libsolidity/smtCheckerTests/types/static_array_length_4.sol Normal file
View File

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

13
test/libsolidity/smtCheckerTests/types/static_array_length_5.sol Normal file
View File

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