diff options
Diffstat (limited to 'test')
22 files changed, 290 insertions, 7 deletions
diff --git a/test/boostTest.cpp b/test/boostTest.cpp index d27ba1f6..34eeaec9 100644 --- a/test/boostTest.cpp +++ b/test/boostTest.cpp @@ -145,6 +145,13 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] ) "yulOptimizerTests", dev::yul::test::YulOptimizerTest::create ) > 0, "no Yul Optimizer tests found"); + if (!dev::test::Options::get().disableSMT) + solAssert(registerTests( + master, + dev::test::Options::get().testPath / "libsolidity", + "smtCheckerTests", + SyntaxTest::create + ) > 0, "no SMT checker tests found"); if (dev::test::Options::get().disableIPC) { for (auto suite: { diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 1f6f765f..c7e60256 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -137,16 +137,17 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) { string text = R"( contract C { - function f() public { + function g() public pure {} + function f() public view { uint a = 3; - this.f(); + this.g(); assert(a == 3); - f(); + g(); assert(a == 3); } } )"; - CHECK_SUCCESS_NO_WARNINGS(text); + CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); } BOOST_AUTO_TEST_CASE(branches_merge_variables) @@ -569,7 +570,10 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_WARNING(text, "Condition is always true"); + CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ + "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 { @@ -577,7 +581,10 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_WARNING(text, "Condition is always false"); + CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ + "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 { @@ -586,7 +593,7 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_SUCCESS_NO_WARNINGS(text); + CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); } diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol new file mode 100644 index 00000000..25a42db6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(42); + assert(x > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol new file mode 100644 index 00000000..a70aaf61 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(0); + assert(x > 0); + } +} + +// ---- +// Warning: (161-174): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol new file mode 100644 index 00000000..aff24b03 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return k(x); + } + + function k(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(2); + assert(x > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol new file mode 100644 index 00000000..9baeb935 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return k(x); + } + + function k(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(0); + assert(x > 0); + } +} + +// ---- +// Warning: (229-242): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol new file mode 100644 index 00000000..3793f411 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = (h)(42); + assert(x > 0); + } +} + +// ---- diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol new file mode 100644 index 00000000..e3c80594 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = (h)(0); + assert(x > 0); + } +} + +// ---- +// Warning: (163-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol new file mode 100644 index 00000000..d2f8ab1d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function g() public { + if (a > 0) + { + a = a - 1; + g(); + } + else + assert(a == 0); + } +} + +// ---- +// Warning: (111-114): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol new file mode 100644 index 00000000..d5b83f00 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f() public { + if (a > 0) + { + a = a - 1; + g(); + } + else + assert(a == 0); + } + function g() public { + if (a > 0) + { + a = a - 1; + f(); + } + else + assert(a == 0); + } +} +// ---- +// Warning: (206-209): Assertion checker does not support recursive function calls. +// Warning: (111-114): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol new file mode 100644 index 00000000..2f7563dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + assert(a > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol new file mode 100644 index 00000000..ad735768 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(0); + assert(a > 0); + } +} + +// ---- +// Warning: (144-157): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol new file mode 100644 index 00000000..2f95d8af --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + f(42); + assert(a > 1); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol new file mode 100644 index 00000000..5d972f96 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + f(0); + assert(a > 0); + } +} + +// ---- +// Warning: (152-165): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol new file mode 100644 index 00000000..7693ad81 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); for (;x;) {} } +} +// ---- +// Warning: (98-99): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol new file mode 100644 index 00000000..ed1ad73a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { for (;x;) {} } + function g() public pure { f(true); } +} diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol new file mode 100644 index 00000000..364fe8d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C +{ + function f(bool x) public pure { require(x); if (x) {} } +} +// ---- +// Warning: (95-96): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol new file mode 100644 index 00000000..e76badf2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { x = true; require(x); } +} +// ---- +// Warning: (98-99): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol new file mode 100644 index 00000000..5cae940b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); } + function g() public pure { f(true); } +} diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol new file mode 100644 index 00000000..66396dd8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); while (x) {} } +} +// ---- +// Warning: (99-100): While loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol new file mode 100644 index 00000000..5000eeb6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { while (x) {} } + function g() public pure { f(true); } +} diff --git a/test/tools/isoltest.cpp b/test/tools/isoltest.cpp index bdc89fb3..1b6fd54a 100644 --- a/test/tools/isoltest.cpp +++ b/test/tools/isoltest.cpp @@ -328,6 +328,7 @@ int main(int argc, char *argv[]) TestTool::editor = "/usr/bin/editor"; fs::path testPath; + bool disableSMT = false; bool formatted = true; po::options_description options( R"(isoltest, tool for interactively managing test contracts. @@ -340,6 +341,7 @@ Allowed options)", options.add_options() ("help", "Show this help screen.") ("testpath", po::value<fs::path>(&testPath), "path to test files") + ("no-smt", "disable SMT checker") ("no-color", "don't use colors") ("editor", po::value<string>(&TestTool::editor), "editor for opening contracts"); @@ -360,6 +362,9 @@ Allowed options)", formatted = false; po::notify(arguments); + + if (arguments.count("no-smt")) + disableSMT = true; } catch (std::exception const& _exception) { @@ -395,6 +400,20 @@ Allowed options)", else return 1; + if (!disableSMT) + { + if (auto stats = runTestSuite( + "SMT Checker", + testPath / "libsolidity", + "smtCheckerTests", + SyntaxTest::create, + formatted + )) + global_stats += *stats; + else + return 1; + } + cout << endl << "Summary: "; FormattedScope(cout, formatted, {BOLD, global_stats ? GREEN : RED}) << global_stats.successCount << "/" << global_stats.testCount; |