From 880a2fffb6c2de874db8b9c5b03480a842c02c1f Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 3 May 2021 12:21:18 +0200 Subject: [PATCH] tests --- .../natspec/abstract_function_nondet_1.sol | 17 ++++++++ ...act_function_nondet_pow_no_abstraction.sol | 43 +++++++++++++++++++ ...t_function_nondet_pow_with_abstraction.sol | 35 +++++++++++++++ .../natspec/natspec_smtchecker_empty.sol | 11 +++++ .../natspec/natspec_smtchecker_error_1.sol | 11 +++++ .../natspec/safe_assert_false_positive.sol | 32 ++++++++++++++ .../safe_assert_false_positive_pure.sol | 29 +++++++++++++ .../natspec/unsafe_assert_remains_unsafe.sol | 27 ++++++++++++ .../conditional_assignment_statevar_1.sol | 1 - .../smtCheckerTests/types/array_literal_7.sol | 5 ++- 10 files changed, 208 insertions(+), 3 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol create mode 100644 test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol new file mode 100644 index 000000000..57f0707a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol @@ -0,0 +1,17 @@ +contract C { + /// @custom:smtchecker abstract-function-nondet + function f(uint x) internal pure returns (uint) { + return x; + } + function g(uint y) public pure { + uint z = f(y); + // Generally holds, but here it doesn't because function + // `f` has been abstracted by nondeterministic values. + assert(z == y); + } +} +// ==== +// SMTEngine: chc +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (297-311): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol new file mode 100644 index 000000000..f3a6581ca --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol @@ -0,0 +1,43 @@ +contract C { + function e(uint _e) public pure { + // Without abstracting function `pow` the solver + // fails to prove that `++i` does not overflow. + for (uint i = 0; i < _e; ++i) + pow(_e, _e); + } + + function pow(uint base, uint exponent) internal pure returns (uint) { + if (base == 0) { + return 0; + } + if (exponent == 0) { + return 1; + } + if (exponent == 1) { + return base; + } + uint y = 1; + while(exponent > 1) { + if(exponent % 2 == 0) { + base = base * base; + exponent = exponent / 2; + } else { + y = base * y; + base = base * base; + exponent = (exponent - 1) / 2; + } + } + return base * y; + } +} +// ==== +// SMTEngine: chc +// ---- +// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4281: (435-447): CHC: Division by zero might happen here. +// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4281: (495-507): CHC: Division by zero might happen here. +// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here. +// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol new file mode 100644 index 000000000..a80708d30 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol @@ -0,0 +1,35 @@ +contract C { + function e(uint _e) public pure { + // Without abstracting function `pow` the solver + // fails to prove that `++i` does not overflow. + for (uint i = 0; i < _e; ++i) + pow(_e, _e); + } + + /// @custom:smtchecker abstract-function-nondet + function pow(uint base, uint exponent) internal pure returns (uint) { + if (base == 0) { + return 0; + } + if (exponent == 0) { + return 1; + } + if (exponent == 1) { + return base; + } + uint y = 1; + while(exponent > 1) { + if(exponent % 2 == 0) { + base = base * base; + exponent = exponent / 2; + } else { + y = base * y; + base = base * base; + exponent = (exponent - 1) / 2; + } + } + return base * y; + } +} +// ==== +// SMTEngine: chc diff --git a/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol new file mode 100644 index 000000000..6b615f763 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol @@ -0,0 +1,11 @@ +contract C { + /// @custom:smtchecker + function f(uint x) internal pure returns (uint) { + return x; + } +} +// ==== +// SMTEngine: chc +// ---- +// Warning 3130: (38-102): Unknown option for "custom:smtchecker": "" +// Warning 3130: (38-102): Unknown option for "custom:smtchecker": "" diff --git a/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol new file mode 100644 index 000000000..6b42e2200 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol @@ -0,0 +1,11 @@ +contract C { + /// @custom:smtchecker abstract-function + function f(uint x) internal pure returns (uint) { + return x; + } +} +// ==== +// SMTEngine: chc +// ---- +// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function" +// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function" diff --git a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol new file mode 100644 index 000000000..62cd8e56b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol @@ -0,0 +1,32 @@ +contract C { + uint x; + uint y; + + function g(uint _x) public { + f1(_x); + // If the body of function `f` is ignored while keeping the state, + // the assertion is true and not reporting it would be a false negative. + // However, since `f` can change the state, the state variables are also + // assigned nondeterministic values after a call to `f`. + // Therefore the assertion below should fail. + assert(x == 0); + + f2(_x); + assert(y == 0); // should fail + } + + /// @custom:smtchecker abstract-function-nondet + function f1(uint _x) internal { + x = _x; + } + + function f2(uint _y) internal { + y = _y; + } + +} +// ==== +// SMTEngine: chc +// ---- +// Warning 6328: (400-414): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call +// Warning 6328: (429-443): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 1\n_x = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n C.f1(1) -- internal call\n C.f2(1) -- internal call diff --git a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol new file mode 100644 index 000000000..03dd24475 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol @@ -0,0 +1,29 @@ +contract C { + uint x; + uint y; + + function g(uint _x) public { + uint z = f1(_x); + assert(x == 0); // should hold because f1 is pure + assert(z == _x); // should hold but f1 was abstracted as nondet, so it fails + + uint t = f2(_x); + assert(y == 0); // should hold because f1 is pure and f2 is view + assert(t == _x); // should hold + } + + /// @custom:smtchecker abstract-function-nondet + function f1(uint _x) internal pure returns (uint) { + return _x; + } + + function f2(uint _y) internal view returns (uint) { + return _y; + } +} +// ==== +// SMTEngine: chc +// ---- +// Warning 2018: (33-335): Function state mutability can be restricted to view +// Warning 2018: (457-524): Function state mutability can be restricted to pure +// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol b/test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol new file mode 100644 index 000000000..1bb6caa42 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol @@ -0,0 +1,27 @@ +contract C { + uint x; + uint y; + + function g(uint _x) public { + f1(_x); + assert(x > 0); // should fail + + f2(_x); + assert(y > 0); // should fail + } + + /// @custom:smtchecker abstract-function-nondet + function f1(uint _x) internal { + x = _x; + } + + function f2(uint _y) internal { + y = _y; + } + +} +// ==== +// SMTEngine: chc +// ---- +// Warning 6328: (74-87): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call +// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call\n C.f2(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol index edd42e094..a7664cc78 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol @@ -14,7 +14,6 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 1218: (134-140): CHC: Error trying to invoke SMT solver. // Warning 4984: (134-140): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (143-146): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (134-140): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_7.sol b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol index ba81e3c9e..6a0c13e92 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_7.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol @@ -18,6 +18,7 @@ contract C } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (226-254): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() -// Warning 6328: (315-335): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() +// Warning 6328: (226-254): CHC: Assertion violation happens here. +// Warning 6328: (315-335): CHC: Assertion violation happens here.