Merge pull request #11860 from ethereum/smt_static_array

[SMTChecker] Add static array length constraint

Author: Leonardo

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

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.

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.

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.

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.

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

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

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

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

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