From 636da48e82f64224a8611dabad1b8a1a019fcfd4 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 1 Aug 2018 22:37:46 +0100 Subject: Move most of SMTChecker tests from C++ to isoltest But keep divison in C++ because results differ between different solvers --- test/libsolidity/SMTChecker.cpp | 593 --------------------- .../libsolidity/smtCheckerTests/001_smoke.test.sol | 3 + .../smtCheckerTests/002_simple_overflow.sol | 6 + .../smtCheckerTests/003_warn_on_typecast.sol | 8 + .../smtCheckerTests/004_warn_on_struct.sol | 12 + .../smtCheckerTests/005_simple_assert.sol | 6 + .../006_simple_assert_with_require.sol | 4 + .../007_assignment_in_declaration.sol | 4 + ...008_function_call_does_not_clear_local_vars.sol | 13 + .../009_branches_merge_variables.sol | 10 + .../010_branches_merge_variables.sol | 11 + .../011_branches_merge_variables.sol | 12 + .../012_branches_merge_variables.sol | 13 + .../013_branches_merge_variables.sol | 13 + .../014_branches_merge_variables.sol | 13 + .../015_branches_assert_condition.sol | 12 + .../016_branches_assert_condition.sol | 16 + .../017_ways_to_merge_variables.sol | 12 + .../018_ways_to_merge_variables.sol | 12 + .../019_ways_to_merge_variables.sol | 12 + .../smtCheckerTests/020_bool_simple.sol | 8 + .../smtCheckerTests/021_bool_simple.sol | 8 + .../smtCheckerTests/022_bool_simple.sol | 7 + .../smtCheckerTests/023_bool_simple.sol | 10 + .../smtCheckerTests/024_bool_simple.sol | 7 + .../smtCheckerTests/025_bool_simple.sol | 9 + .../smtCheckerTests/026_bool_int_mixed.sol | 9 + .../smtCheckerTests/027_bool_int_mixed.sol | 8 + .../smtCheckerTests/028_bool_int_mixed.sol | 21 + .../smtCheckerTests/029_storage_value_vars.sol | 22 + .../smtCheckerTests/030_storage_value_vars.sol | 12 + .../smtCheckerTests/031_storage_value_vars.sol | 25 + .../smtCheckerTests/032_storage_value_vars.sol | 10 + .../smtCheckerTests/033_while_loop_simple.sol | 13 + .../smtCheckerTests/034_while_loop_simple.sol | 9 + .../smtCheckerTests/035_while_loop_simple.sol | 11 + .../smtCheckerTests/036_while_loop_simple.sol | 11 + .../smtCheckerTests/037_while_loop_simple.sol | 12 + .../smtCheckerTests/038_constant_condition.sol | 9 + .../smtCheckerTests/039_constant_condition.sol | 9 + .../smtCheckerTests/040_constant_condition.sol | 9 + test/libsolidity/smtCheckerTests/041_for_loop.sol | 8 + test/libsolidity/smtCheckerTests/042_for_loop.sol | 8 + test/libsolidity/smtCheckerTests/043_for_loop.sol | 8 + test/libsolidity/smtCheckerTests/044_for_loop.sol | 10 + test/libsolidity/smtCheckerTests/045_for_loop.sol | 12 + test/libsolidity/smtCheckerTests/046_for_loop.sol | 12 + 47 files changed, 489 insertions(+), 593 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/001_smoke.test.sol create mode 100644 test/libsolidity/smtCheckerTests/002_simple_overflow.sol create mode 100644 test/libsolidity/smtCheckerTests/003_warn_on_typecast.sol create mode 100644 test/libsolidity/smtCheckerTests/004_warn_on_struct.sol create mode 100644 test/libsolidity/smtCheckerTests/005_simple_assert.sol create mode 100644 test/libsolidity/smtCheckerTests/006_simple_assert_with_require.sol create mode 100644 test/libsolidity/smtCheckerTests/007_assignment_in_declaration.sol create mode 100644 test/libsolidity/smtCheckerTests/008_function_call_does_not_clear_local_vars.sol create mode 100644 test/libsolidity/smtCheckerTests/009_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/010_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/011_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/012_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/013_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/014_branches_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/015_branches_assert_condition.sol create mode 100644 test/libsolidity/smtCheckerTests/016_branches_assert_condition.sol create mode 100644 test/libsolidity/smtCheckerTests/017_ways_to_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/018_ways_to_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/019_ways_to_merge_variables.sol create mode 100644 test/libsolidity/smtCheckerTests/020_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/021_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/022_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/023_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/024_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/025_bool_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/026_bool_int_mixed.sol create mode 100644 test/libsolidity/smtCheckerTests/027_bool_int_mixed.sol create mode 100644 test/libsolidity/smtCheckerTests/028_bool_int_mixed.sol create mode 100644 test/libsolidity/smtCheckerTests/029_storage_value_vars.sol create mode 100644 test/libsolidity/smtCheckerTests/030_storage_value_vars.sol create mode 100644 test/libsolidity/smtCheckerTests/031_storage_value_vars.sol create mode 100644 test/libsolidity/smtCheckerTests/032_storage_value_vars.sol create mode 100644 test/libsolidity/smtCheckerTests/033_while_loop_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/034_while_loop_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/035_while_loop_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/036_while_loop_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/037_while_loop_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/038_constant_condition.sol create mode 100644 test/libsolidity/smtCheckerTests/039_constant_condition.sol create mode 100644 test/libsolidity/smtCheckerTests/040_constant_condition.sol create mode 100644 test/libsolidity/smtCheckerTests/041_for_loop.sol create mode 100644 test/libsolidity/smtCheckerTests/042_for_loop.sol create mode 100644 test/libsolidity/smtCheckerTests/043_for_loop.sol create mode 100644 test/libsolidity/smtCheckerTests/044_for_loop.sol create mode 100644 test/libsolidity/smtCheckerTests/045_for_loop.sol create mode 100644 test/libsolidity/smtCheckerTests/046_for_loop.sol diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 13fcc5b4..a49618bd 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -56,599 +56,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(smoke_test) -{ - string text = R"( - contract C { } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(simple_overflow) -{ - string text = R"( - contract C { - function f(uint a, uint b) public pure returns (uint) { return a + b; } - } - )"; - CHECK_WARNING(text, "Overflow (resulting value larger than"); -} - -BOOST_AUTO_TEST_CASE(warn_on_typecast) -{ - string text = R"( - contract C { - function f() public pure returns (uint) { - return uint8(1); - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this expression."); -} - -BOOST_AUTO_TEST_CASE(warn_on_struct) -{ - string text = R"( - pragma experimental ABIEncoderV2; - contract C { - struct A { uint a; uint b; } - function f() public pure returns (A memory) { - return A({ a: 1, b: 2 }); - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector{ - "Experimental feature", - "Assertion checker does not yet implement this expression.", - "Assertion checker does not yet support the type of this variable." - })); -} - -BOOST_AUTO_TEST_CASE(simple_assert) -{ - string text = R"( - contract C { - function f(uint a) public pure { assert(a == 2); } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(simple_assert_with_require) -{ - string text = R"( - contract C { - function f(uint a) public pure { require(a < 10); assert(a < 20); } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(assignment_in_declaration) -{ - string text = R"( - contract C { - function f() public pure { uint a = 2; assert(a == 2); } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(branches_merge_variables) -{ - // Branch does not touch variable a - string text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Positive branch touches variable a, but assertion should still hold. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Negative branch touches variable a, but assertion should still hold. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - } else { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is not merged, if it is only read. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - assert(a == 3); - } else { - assert(a == 3); - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is reset in both branches - text = R"( - contract C { - function f(uint x) public pure { - uint a = 2; - if (x > 10) { - a = 3; - } else { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is reset in both branches - text = R"( - contract C { - function f(uint x) public pure { - uint a = 2; - if (x > 10) { - a = 3; - } else { - a = 4; - } - assert(a >= 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(branches_assert_condition) -{ - string text = R"( - contract C { - function f(uint x) public pure { - if (x > 10) { - assert(x > 9); - } - else - { - assert(x < 11); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - if (x > 10) { - assert(x > 9); - } - else if (x > 2) - { - assert(x <= 10 && x > 2); - } - else - { - assert(0 <= x && x <= 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(ways_to_merge_variables) -{ - string text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a++; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - ++a; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a = 5; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(bool_simple) -{ - string text = R"( - contract C { - function f(bool x) public pure { - assert(x); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(bool x, bool y) public pure { - assert(x == y); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(bool x, bool y) public pure { - bool z = x || y; - assert(!(x && y) || z); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - if (x) { - assert(x); - } else { - assert(!x); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - bool y = x; - assert(x == y); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - require(x); - bool y; - y = false; - assert(x || y); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(bool_int_mixed) -{ - string text = R"( - contract C { - function f(bool x) public pure { - uint a; - if (x) - a = 1; - assert(!x || a > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x, uint a) public pure { - require(!x || a > 0); - uint b = a; - assert(!x || b > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x, bool y) public pure { - uint a; - if (x) { - if (y) { - a = 0; - } else { - a = 1; - } - } else { - if (y) { - a = 1; - } else { - a = 0; - } - } - bool xor_x_y = (x && !y) || (!x && y); - assert(!xor_x_y || a > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(storage_value_vars) -{ - string text = R"( - contract C - { - address a; - bool b; - uint c; - function f(uint x) public { - if (x == 0) - { - a = 0x0000000000000000000000000000000000000100; - b = true; - } - else - { - a = 0x0000000000000000000000000000000000000200; - b = false; - } - assert(a > 0x0000000000000000000000000000000000000000 && b); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C - { - address a; - bool b; - uint c; - function f() public view { - assert(c > 0); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C - { - function f(uint x) public { - if (x == 0) - { - a = 0x0000000000000000000000000000000000000100; - b = true; - } - else - { - a = 0x0000000000000000000000000000000000000200; - b = false; - } - assert(b == (a < 0x0000000000000000000000000000000000000200)); - } - - function g() public view { - require(a < 0x0000000000000000000000000000000000000100); - assert(c >= 0); - } - address a; - bool b; - uint c; - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C - { - function f() public view { - assert(c > 0); - } - uint c; - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - -} - -BOOST_AUTO_TEST_CASE(while_loop_simple) -{ - // Check that variables are cleared - string text = R"( - contract C { - function f(uint x) public pure { - x = 2; - while (x > 1) { - x = 2; - } - assert(x == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that condition is assumed. - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - assert(x == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Check that condition is not assumed after the body anymore - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - } - assert(x == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that negation of condition is not assumed after the body anymore - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - } - assert(x != 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that side-effects of condition are taken into account - text = R"( - contract C { - function f(uint x, uint y) public pure { - x = 7; - while ((x = y) > 0) { - } - assert(x == 7); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(constant_condition) -{ - string text = R"( - contract C { - function f(uint x) public pure { - if (x >= 0) { revert(); } - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector{ - "Condition is always true", - "Assertion checker does not yet implement this type of function call" - })); - text = R"( - contract C { - function f(uint x) public pure { - if (x >= 10) { if (x < 10) { revert(); } } - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector{ - "Condition is always false", - "Assertion checker does not yet implement this type of function call" - })); - // a plain literal constant is fine - text = R"( - contract C { - function f(uint) public pure { - if (true) { revert(); } - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); -} - - -BOOST_AUTO_TEST_CASE(for_loop) -{ - string text = R"( - contract C { - function f(uint x) public pure { - require(x == 2); - for (;;) {} - assert(x == 2); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (; x == 2; ) { - assert(x == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (uint y = 2; x < 10; ) { - assert(y == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (uint y = 2; x < 10; y = 3) { - assert(y == 2); - } - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - function f(uint x) public pure { - uint y; - for (y = 2; x < 10; ) { - y = 3; - } - assert(y == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - function f(uint x) public pure { - uint y; - for (y = 2; x < 10; ) { - y = 3; - } - assert(y == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); -} - BOOST_AUTO_TEST_CASE(division) { string text = R"( diff --git a/test/libsolidity/smtCheckerTests/001_smoke.test.sol b/test/libsolidity/smtCheckerTests/001_smoke.test.sol new file mode 100644 index 00000000..8b7b77da --- /dev/null +++ b/test/libsolidity/smtCheckerTests/001_smoke.test.sol @@ -0,0 +1,3 @@ +pragma experimental SMTChecker; +contract C { +} diff --git a/test/libsolidity/smtCheckerTests/002_simple_overflow.sol b/test/libsolidity/smtCheckerTests/002_simple_overflow.sol new file mode 100644 index 00000000..894ff1a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/002_simple_overflow.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a, uint b) public pure returns (uint) { return a + b; } +} +// ---- +// Warning: (112-117): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here diff --git a/test/libsolidity/smtCheckerTests/003_warn_on_typecast.sol b/test/libsolidity/smtCheckerTests/003_warn_on_typecast.sol new file mode 100644 index 00000000..be785414 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/003_warn_on_typecast.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (uint) { + return uint8(1); + } +} +// ---- +// Warning: (106-114): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/004_warn_on_struct.sol b/test/libsolidity/smtCheckerTests/004_warn_on_struct.sol new file mode 100644 index 00000000..c50df07a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/004_warn_on_struct.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; +contract C { + struct A { uint a; uint b; } + function f() public pure returns (A memory) { + return A({ a: 1, b: 2 }); + } +} +// ---- +// Warning: (32-65): Experimental features are turned on. Do not use experimental features on live deployments. +// Warning: (150-158): Assertion checker does not yet support the type of this variable. +// Warning: (177-194): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/005_simple_assert.sol b/test/libsolidity/smtCheckerTests/005_simple_assert.sol new file mode 100644 index 00000000..8bd6e61a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/005_simple_assert.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a) public pure { assert(a == 2); } +} +// ---- +// Warning: (82-96): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/006_simple_assert_with_require.sol b/test/libsolidity/smtCheckerTests/006_simple_assert_with_require.sol new file mode 100644 index 00000000..b66ae245 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/006_simple_assert_with_require.sol @@ -0,0 +1,4 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a) public pure { require(a < 10); assert(a < 20); } +} diff --git a/test/libsolidity/smtCheckerTests/007_assignment_in_declaration.sol b/test/libsolidity/smtCheckerTests/007_assignment_in_declaration.sol new file mode 100644 index 00000000..0c701672 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/007_assignment_in_declaration.sol @@ -0,0 +1,4 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure { uint a = 2; assert(a == 2); } +} diff --git a/test/libsolidity/smtCheckerTests/008_function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/008_function_call_does_not_clear_local_vars.sol new file mode 100644 index 00000000..b4260224 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/008_function_call_does_not_clear_local_vars.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f() public { + uint a = 3; + this.f(); + assert(a == 3); + f(); + assert(a == 3); + } +} +// ---- +// Warning: (99-107): Assertion checker does not yet implement this type of function call. +// Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/009_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/009_branches_merge_variables.sol new file mode 100644 index 00000000..f93e32e4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/009_branches_merge_variables.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +// Branch does not touch variable a +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/010_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/010_branches_merge_variables.sol new file mode 100644 index 00000000..c00ef787 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/010_branches_merge_variables.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Positive branch touches variable a, but assertion should still hold. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/011_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/011_branches_merge_variables.sol new file mode 100644 index 00000000..4e18aa88 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/011_branches_merge_variables.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +// Negative branch touches variable a, but assertion should still hold. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } else { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/012_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/012_branches_merge_variables.sol new file mode 100644 index 00000000..e3a02704 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/012_branches_merge_variables.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is not merged, if it is only read. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + assert(a == 3); + } else { + assert(a == 3); + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/013_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/013_branches_merge_variables.sol new file mode 100644 index 00000000..0bd1cf3a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/013_branches_merge_variables.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is reset in both branches +contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/014_branches_merge_variables.sol b/test/libsolidity/smtCheckerTests/014_branches_merge_variables.sol new file mode 100644 index 00000000..8e477179 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/014_branches_merge_variables.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is reset in both branches +contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 4; + } + assert(a >= 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/015_branches_assert_condition.sol b/test/libsolidity/smtCheckerTests/015_branches_assert_condition.sol new file mode 100644 index 00000000..64f6e012 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/015_branches_assert_condition.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x > 10) { + assert(x > 9); + } + else + { + assert(x < 11); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/016_branches_assert_condition.sol b/test/libsolidity/smtCheckerTests/016_branches_assert_condition.sol new file mode 100644 index 00000000..e39ab844 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/016_branches_assert_condition.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x > 10) { + assert(x > 9); + } + else if (x > 2) + { + assert(x <= 10 && x > 2); + } + else + { + assert(0 <= x && x <= 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/017_ways_to_merge_variables.sol b/test/libsolidity/smtCheckerTests/017_ways_to_merge_variables.sol new file mode 100644 index 00000000..16d6fdfe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/017_ways_to_merge_variables.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a++; + } + assert(a == 3); + } +} +// ---- +// Warning: (159-173): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/018_ways_to_merge_variables.sol b/test/libsolidity/smtCheckerTests/018_ways_to_merge_variables.sol new file mode 100644 index 00000000..e25ab20f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/018_ways_to_merge_variables.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + ++a; + } + assert(a == 3); + } +} +// ---- +// Warning: (159-173): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/019_ways_to_merge_variables.sol b/test/libsolidity/smtCheckerTests/019_ways_to_merge_variables.sol new file mode 100644 index 00000000..03ae7216 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/019_ways_to_merge_variables.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 5; + } + assert(a == 3); + } +} +// ---- +// Warning: (161-175): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/020_bool_simple.sol b/test/libsolidity/smtCheckerTests/020_bool_simple.sol new file mode 100644 index 00000000..76b4b08b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/020_bool_simple.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + assert(x); + } +} +// ---- +// Warning: (90-99): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/021_bool_simple.sol b/test/libsolidity/smtCheckerTests/021_bool_simple.sol new file mode 100644 index 00000000..5c166c02 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/021_bool_simple.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + assert(x == y); + } +} +// ---- +// Warning: (98-112): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/022_bool_simple.sol b/test/libsolidity/smtCheckerTests/022_bool_simple.sol new file mode 100644 index 00000000..1d2ab49f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/022_bool_simple.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + bool z = x || y; + assert(!(x && y) || z); + } +} diff --git a/test/libsolidity/smtCheckerTests/023_bool_simple.sol b/test/libsolidity/smtCheckerTests/023_bool_simple.sol new file mode 100644 index 00000000..c40404a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/023_bool_simple.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + if(x) { + assert(x); + } else { + assert(!x); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/024_bool_simple.sol b/test/libsolidity/smtCheckerTests/024_bool_simple.sol new file mode 100644 index 00000000..4cecebbc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/024_bool_simple.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + bool y = x; + assert(x == y); + } +} diff --git a/test/libsolidity/smtCheckerTests/025_bool_simple.sol b/test/libsolidity/smtCheckerTests/025_bool_simple.sol new file mode 100644 index 00000000..90350bb6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/025_bool_simple.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + require(x); + bool y; + y = false; + assert(x || y); + } +} diff --git a/test/libsolidity/smtCheckerTests/026_bool_int_mixed.sol b/test/libsolidity/smtCheckerTests/026_bool_int_mixed.sol new file mode 100644 index 00000000..d611cc17 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/026_bool_int_mixed.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + uint a; + if(x) + a = 1; + assert(!x || a > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/027_bool_int_mixed.sol b/test/libsolidity/smtCheckerTests/027_bool_int_mixed.sol new file mode 100644 index 00000000..24640c5a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/027_bool_int_mixed.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, uint a) public pure { + require(!x || a > 0); + uint b = a; + assert(!x || b > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/028_bool_int_mixed.sol b/test/libsolidity/smtCheckerTests/028_bool_int_mixed.sol new file mode 100644 index 00000000..f872e82f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/028_bool_int_mixed.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + uint a; + if (x) { + if (y) { + a = 0; + } else { + a = 1; + } + } else { + if (y) { + a = 1; + } else { + a = 0; + } + } + bool xor_x_y = (x && !y) || (!x && y); + assert(!xor_x_y || a > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/029_storage_value_vars.sol b/test/libsolidity/smtCheckerTests/029_storage_value_vars.sol new file mode 100644 index 00000000..84f6c77e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/029_storage_value_vars.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C +{ + address a; + bool b; + uint c; + function f(uint x) public { + if (x == 0) + { + a = 0x0000000000000000000000000000000000000100; + b = true; + } + else + { + a = 0x0000000000000000000000000000000000000200; + b = false; + } + assert(a > 0x0000000000000000000000000000000000000000 && b); + } +} +// ---- +// Warning: (362-421): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/030_storage_value_vars.sol b/test/libsolidity/smtCheckerTests/030_storage_value_vars.sol new file mode 100644 index 00000000..bceddb38 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/030_storage_value_vars.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C +{ + address a; + bool b; + uint c; + function f() public view { + assert(c > 0); + } +} +// ---- +// Warning: (123-136): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/031_storage_value_vars.sol b/test/libsolidity/smtCheckerTests/031_storage_value_vars.sol new file mode 100644 index 00000000..39049b99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/031_storage_value_vars.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; +contract C +{ + function f(uint x) public { + if (x == 0) + { + a = 0x0000000000000000000000000000000000000100; + b = true; + } + else + { + a = 0x0000000000000000000000000000000000000200; + b = false; + } + assert(b == (a < 0x0000000000000000000000000000000000000200)); + } + + function g() public view { + require(a < 0x0000000000000000000000000000000000000100); + assert(c >= 0); + } + address a; + bool b; + uint c; +} diff --git a/test/libsolidity/smtCheckerTests/032_storage_value_vars.sol b/test/libsolidity/smtCheckerTests/032_storage_value_vars.sol new file mode 100644 index 00000000..88b6b0ae --- /dev/null +++ b/test/libsolidity/smtCheckerTests/032_storage_value_vars.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C +{ + function f() public view { + assert(c > 0); + } + uint c; +} +// ---- +// Warning: (84-97): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/033_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/033_while_loop_simple.sol new file mode 100644 index 00000000..074be86f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/033_while_loop_simple.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Check that variables are cleared +contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + x = 2; + } + assert(x == 2); + } +} +// ---- +// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/034_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/034_while_loop_simple.sol new file mode 100644 index 00000000..92a3f0fe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/034_while_loop_simple.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +// Check that condition is assumed. +contract C { + function f(uint x) public pure { + while (x == 2) { + assert(x == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/035_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/035_while_loop_simple.sol new file mode 100644 index 00000000..a37df888 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/035_while_loop_simple.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Check that condition is not assumed after the body anymore +contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x == 2); + } +} +// ---- +// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/036_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/036_while_loop_simple.sol new file mode 100644 index 00000000..f71da865 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/036_while_loop_simple.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Check that negation of condition is not assumed after the body anymore +contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x != 2); + } +} +// ---- +// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol new file mode 100644 index 00000000..41559c99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +// Check that side-effects of condition are taken into account +contract C { + function f(uint x, uint y) public pure { + x = 7; + while ((x = y) > 0) { + } + assert(x == 7); + } +} +// ---- +// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/038_constant_condition.sol b/test/libsolidity/smtCheckerTests/038_constant_condition.sol new file mode 100644 index 00000000..b9fae4ee --- /dev/null +++ b/test/libsolidity/smtCheckerTests/038_constant_condition.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x >= 0) { revert(); } + } +} +// ---- +// Warning: (94-100): Condition is always true. +// Warning: (104-112): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/039_constant_condition.sol b/test/libsolidity/smtCheckerTests/039_constant_condition.sol new file mode 100644 index 00000000..aaa613ea --- /dev/null +++ b/test/libsolidity/smtCheckerTests/039_constant_condition.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x >= 10) { if (x < 10) { revert(); } } + } +} +// ---- +// Warning: (109-115): Condition is always false. +// Warning: (119-127): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/040_constant_condition.sol b/test/libsolidity/smtCheckerTests/040_constant_condition.sol new file mode 100644 index 00000000..f22cd65e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/040_constant_condition.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +// a plain literal constant is fine +contract C { + function f(uint) public pure { + if (true) { revert(); } + } +} +// ---- +// Warning: (136-144): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/041_for_loop.sol b/test/libsolidity/smtCheckerTests/041_for_loop.sol new file mode 100644 index 00000000..8988efad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/041_for_loop.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (;;) {} + assert(x == 2); + } +} diff --git a/test/libsolidity/smtCheckerTests/042_for_loop.sol b/test/libsolidity/smtCheckerTests/042_for_loop.sol new file mode 100644 index 00000000..58c9f3a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/042_for_loop.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (; x == 2; ) { + assert(x == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/043_for_loop.sol b/test/libsolidity/smtCheckerTests/043_for_loop.sol new file mode 100644 index 00000000..8bf9bdc7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/043_for_loop.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (uint y = 2; x < 10; ) { + assert(y == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/044_for_loop.sol b/test/libsolidity/smtCheckerTests/044_for_loop.sol new file mode 100644 index 00000000..4d082026 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/044_for_loop.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (uint y = 2; x < 10; y = 3) { + assert(y == 2); + } + } +} +// ---- +// Warning: (136-150): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/045_for_loop.sol b/test/libsolidity/smtCheckerTests/045_for_loop.sol new file mode 100644 index 00000000..2c84960f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/045_for_loop.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint y; + for (y = 2; x < 10; ) { + y = 3; + } + assert(y == 3); + } +} +// ---- +// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/046_for_loop.sol b/test/libsolidity/smtCheckerTests/046_for_loop.sol new file mode 100644 index 00000000..90c4c328 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/046_for_loop.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint y; + for (y = 2; x < 10; ) { + y = 3; + } + assert(y == 2); + } +} +// ---- +// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). -- cgit v1.2.3