From e5de4a66eda8211bb38b874f7683534d6cfc1c24 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 29 Sep 2017 10:30:12 +0200 Subject: Tests. --- libsolidity/formal/SMTChecker.cpp | 5 - test/libsolidity/SMTChecker.cpp | 240 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 240 insertions(+), 5 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 428afa9f..1cf5dc95 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -106,11 +106,6 @@ bool SMTChecker::visit(WhileStatement const& _node) { // TODO Check if condition is always true - // TODO Weird side effects like - // uint x = 1; - // while (x ++ > 0) { assert(x == 2); } - // solution: clear variables first, then execute and assert condition, then executed body. - auto touchedVariables = m_variableUsage->touchedVariables(_node); resetVariables(touchedVariables); if (_node.isDoWhile()) diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 8d712a80..400f696c 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -105,6 +105,246 @@ BOOST_AUTO_TEST_CASE(warn_on_struct) CHECK_WARNING_ALLOW_MULTI(text, ""); } +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 for"); +} + +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(use_before_declaration) +{ + string text = R"( + contract C { + function f() public pure { a = 3; uint a = 2; assert(a == 2); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f() public pure { assert(a == 0); uint a = 2; assert(a == 2); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) +{ + string text = R"( + contract C { + function f() public { + uint a = 3; + this.f(); + assert(a == 3); + f(); + assert(a == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(branches_clear_variables) +{ + // Only clears accessed variables + 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); + // It is just a plain clear and will not combine branches. + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 3; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Clear also works on the else branch + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } else { + a = 3; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Variable is not cleared, 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); +} + +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); +} + +BOOST_AUTO_TEST_CASE(ways_to_clear_variables) +{ + string text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a++; + } + assert(a == 3); + } + } + )"; + 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(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) public pure { + x = 7; + while ((x = 5) > 0) { + } + assert(x == 7); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); +} + + BOOST_AUTO_TEST_SUITE_END() } -- cgit