aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-09-29 16:30:12 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2017-11-22 10:35:34 +0800
commite5de4a66eda8211bb38b874f7683534d6cfc1c24 (patch)
tree76fca6d49a3aaf8cfef89a89bf936d8df89d7cb1
parentb37377641dd1cac7d1b5d5307ea6f7517c0f321f (diff)
downloaddexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar.gz
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar.bz2
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar.lz
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar.xz
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.tar.zst
dexon-solidity-e5de4a66eda8211bb38b874f7683534d6cfc1c24.zip
Tests.
-rw-r--r--libsolidity/formal/SMTChecker.cpp5
-rw-r--r--test/libsolidity/SMTChecker.cpp240
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()
}