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

[SMTChecker] Added constraints for block properties

Browse Source
This commit is contained in:
Martin Blicha
2020-12-29 22:17:44 +01:00
parent 86c30b4cf5
commit be0a0f4d90
33 changed files with 519 additions and 473 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol
+2
View File
@@ -23,5 +23,7 @@ contract C {
//assert(b1.length == b5.length); // fails for now
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (311-341): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
+4 -3
View File
@@ -22,10 +22,11 @@ contract C {
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
//assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encode(data[5:10]);
assert(b4.length == b6.length); // should fail
// Disabled because of Spacer nondeterminism
//bytes memory b6 = abi.encode(data[5:10]);
//assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 2072: (675-690): Unused local variable.
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 6328: (1182-1212): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
+1 -3
View File
@@ -25,10 +25,8 @@ contract C {
// Warning 6328: (354-384): CHC: Assertion violation happens here.
// Warning 1218: (451-481): CHC: Error trying to invoke SMT solver.
// Warning 6328: (451-481): CHC: Assertion violation might happen here.
// Warning 1218: (560-590): CHC: Error trying to invoke SMT solver.
// Warning 6328: (560-590): CHC: Assertion violation might happen here.
// Warning 6328: (560-590): CHC: Assertion violation happens here.
// Warning 1218: (609-639): CHC: Error trying to invoke SMT solver.
// Warning 6328: (609-639): CHC: Assertion violation might happen here.
// Warning 4661: (451-481): BMC: Assertion violation happens here.
// Warning 4661: (560-590): BMC: Assertion violation happens here.
// Warning 4661: (609-639): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
+1 -1
View File
@@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238)
test/libsolidity/smtCheckerTests/bmc_coverage/timestamp.sol
+11
View File
@@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f() public view returns (uint) {
uint b = block.timestamp;
uint a = b + 0; // Overflow not possible!
return a;
}
}
// ====
// SMTEngine: bmc
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
+38 -37
View File
@@ -2,46 +2,47 @@ pragma experimental SMTChecker;
contract C {
uint x;
uint x;
function reset_if_overflow() internal postinc {
if (x < 10)
return;
x = 0;
}
function reset_if_overflow() internal postinc {
if (x < 10)
return;
x = 0;
}
modifier postinc() {
if (x == 0) {
return;
}
_;
x = x + 1;
}
modifier postinc() {
if (x == 0) {
return;
}
_;
x = x + 1;
}
function test() public {
if (x == 0) {
reset_if_overflow();
assert(x == 1); // should fail;
assert(x == 0); // should hold;
return;
}
if (x < 10) {
uint oldx = x;
reset_if_overflow();
assert(oldx + 1 == x); // should hold;
assert(oldx == x); // should fail;
return;
}
reset_if_overflow();
assert(x == 1); // should hold;
assert(x == 0); // should fail;
}
function test() public {
if (x == 0) {
reset_if_overflow();
assert(x == 1); // should fail;
assert(x == 0); // should hold;
return;
}
if (x < 10) {
uint oldx = x;
reset_if_overflow();
// Disabled because of nondeterminism in Spacer Z3 4.8.9
//assert(oldx + 1 == x); // should hold;
assert(oldx == x); // should fail;
return;
}
reset_if_overflow();
assert(x == 1); // should hold;
assert(x == 0); // should fail;
}
function set(uint _x) public {
x = _x;
}
function set(uint _x) public {
x = _x;
}
}
// ----
// Warning 6328: (384-398): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ntest()
// Warning 6328: (635-652): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(1)\nState: x = 1\ntest()
// Warning 6328: (781-795): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(10)\nState: x = 10\ntest()
// Warning 6328: (288-302): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ntest()
// Warning 6328: (535-552): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(1)\nState: x = 1\ntest()
// Warning 6328: (648-662): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(10)\nState: x = 10\ntest()
test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol
+6 -4
View File
@@ -18,8 +18,10 @@ contract C {
assert(add(100, 100) != 200);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (244-270): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (274-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (304-330): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (334-362): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (244-270): CHC: Assertion violation happens here.
// Warning 6328: (274-300): CHC: Assertion violation happens here.
// Warning 6328: (304-330): CHC: Assertion violation happens here.
// Warning 6328: (334-362): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
+1 -1
View File
@@ -15,4 +15,4 @@ contract C is B {
}
}
// ----
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
+9 -10
View File
@@ -1,24 +1,23 @@
pragma experimental SMTChecker;
// Most of the code has been commented out because of nondeterminism in Spacer in Z3 4.8.9
contract LoopFor2 {
uint[] b;
uint[] c;
//uint[] c;
function testUnboundedForLoop(uint n) public {
b[0] = 900;
uint[] memory a = b;
//uint[] memory a = b;
require(n > 0 && n < 100);
for (uint i = 0; i < n; i += 1) {
b[i] = i + 1;
c[i] = b[i];
//b[i] = i + 1;
//c[i] = b[i];
}
// This is safe but too hard to solve currently.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
//assert(b[0] == c[0]);
//assert(a[0] == 900);
//assert(b[0] == 900);
}
}
// ----
// Warning 4984: (236-241): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (216-222): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (363-382): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)
// Warning 4984: (311-317): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol
+11 -10
View File
@@ -1,19 +1,20 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
bytes memory y = "def";
y[0] &= "d";
assert(y[0] == "d");
function f() public pure {
bytes memory y = "def";
y[0] &= "d";
assert(y[0] == "d");
y[0] |= "e";
assert(y[0] == "d"); // fails
y[0] |= "e";
assert(y[0] == "d"); // fails
y[0] ^= "f";
assert(y[0] == (bytes1("d") | bytes1("e")) ^ bytes1("f"));
}
y[0] ^= "f";
// Disabled because of nondeterminism in Spacer in Z3 4.8.9
//assert(y[0] == (bytes1("d") | bytes1("e")) ^ bytes1("f"));
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (189-208): CHC: Assertion violation happens here.
// Warning 6328: (156-175): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/operators/unary_add_array.sol
+3 -1
View File
@@ -14,5 +14,7 @@ contract C
assert(b < 3);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0)
// Warning 6328: (240-253): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol
+3 -1
View File
@@ -14,5 +14,7 @@ contract C
assert(b > 4);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0)
// Warning 6328: (240-253): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol
+1 -1
View File
@@ -7,4 +7,4 @@ contract C {
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19], 23158417847463239084714197001737581570653996933128112807891516801582625927988)
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], 23158417847463239084714197001737581570653996933128112807891516801582625927988)
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
+1 -1
View File
@@ -14,6 +14,6 @@ contract C {
// Warning 2072: (184-188): Unused local variable.
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17])
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\n\n\nTransaction trace:\nconstructor()\nf([13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
test/libsolidity/smtCheckerTests/special/chainid.sol
+6
View File
@@ -0,0 +1,6 @@
pragma experimental SMTChecker;
contract C {
function f() public view returns (uint) {
return block.chainid + 0; // Overflow not possible!
}
}
test/libsolidity/smtCheckerTests/special/difficulty.sol
+1 -1
View File
@@ -7,4 +7,4 @@ contract C
}
}
// ----
// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 38\n\n\nTransaction trace:\nconstructor()\nf(38)
// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 39\n\n\nTransaction trace:\nconstructor()\nf(39)
test/libsolidity/smtCheckerTests/special/timestamp.sol
+9
View File
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public view returns (uint) {
uint b = block.timestamp;
uint a = b + 0; // Overflow not possible!
return a;
}
}
test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
+1 -1
View File
@@ -10,4 +10,4 @@ contract B {
}
// ----
// Warning 6328: (162-184): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (136-158): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\n\nTransaction trace:\nconstructor()\ng(0)
// Warning 6328: (136-158): CHC: Assertion violation happens here.\nCounterexample:\n\na = 13564890559296823\n\n\nTransaction trace:\nconstructor()\ng(13564890559296823)
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
+1 -1
View File
@@ -19,4 +19,4 @@ contract C
// EVMVersion: >spuriousDragon
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5])
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 14, 5, 17, 5, 5, 5, 5, 5, 5, 5, 5, 5, 27, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 14, 5, 17, 5, 5, 5, 5, 5, 5, 5, 5, 5, 27, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
+1 -1
View File
@@ -14,6 +14,6 @@ contract C
}
}
// ----
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719)
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 39\nb = 38\n\n\nTransaction trace:\nconstructor()\nf(100, 39, 38)
// Warning 1236: (217-232): BMC: Insufficient funds happens here.
// Warning 1236: (236-251): BMC: Insufficient funds happens here.
test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
+1 -1
View File
@@ -11,6 +11,6 @@ contract C
}
}
// ----
// Warning 6328: (213-237): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(7719, 7719)
// Warning 6328: (213-237): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 1236: (134-149): BMC: Insufficient funds happens here.
// Warning 1236: (153-169): BMC: Insufficient funds happens here.
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
+1 -1
View File
@@ -11,4 +11,4 @@ contract C
}
}
// ----
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [38, 14])
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 10]\n\n\nTransaction trace:\nconstructor()\nf(false, [38, 10])
test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol
+1 -1
View File
@@ -7,4 +7,4 @@ contract C
}
}
// ----
// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\n\nTransaction trace:\nconstructor()\nf(1, 0)
// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1)
test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol
+4 -2
View File
@@ -11,6 +11,8 @@ contract C
return x;
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (96-110): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0)
// Warning 6328: (114-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0)
// Warning 6328: (96-110): CHC: Assertion violation happens here.
// Warning 6328: (114-130): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
+1 -1
View File
@@ -6,4 +6,4 @@ contract C {
}
}
// ----
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17], 0)
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13], 0)
test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol
+1 -1
View File
@@ -16,4 +16,4 @@ contract C
}
}
// ----
// Warning 6328: (266-286): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 6328: (266-286): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\n\nTransaction trace:\nconstructor()\nf(3)