From b46b827c30584968c6815b456b8c0c775c35ae48 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 18 Oct 2018 15:03:52 +0200 Subject: [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash --- test/libsolidity/SMTChecker.cpp | 17 --------------- .../smtCheckerTests/special/blockhash.sol | 14 ++++++++++++ .../smtCheckerTests/special/gasleft.sol | 10 +++++++++ test/libsolidity/smtCheckerTests/special/many.sol | 25 ++++++++++++++++++++++ .../smtCheckerTests/special/msg_data.sol | 14 ++++++++++++ .../smtCheckerTests/special/msg_sender_1.sol | 10 +++++++++ .../smtCheckerTests/special/msg_sender_2.sol | 14 ++++++++++++ .../smtCheckerTests/special/msg_sender_fail_1.sol | 13 +++++++++++ .../smtCheckerTests/special/msg_sig.sol | 14 ++++++++++++ 9 files changed, 114 insertions(+), 17 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/blockhash.sol create mode 100644 test/libsolidity/smtCheckerTests/special/gasleft.sol create mode 100644 test/libsolidity/smtCheckerTests/special/many.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_data.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_2.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sig.sol (limited to 'test') diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index c7e60256..195004cb 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -133,23 +133,6 @@ BOOST_AUTO_TEST_CASE(assignment_in_declaration) CHECK_SUCCESS_NO_WARNINGS(text); } -BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) -{ - string text = R"( - contract C { - function g() public pure {} - function f() public view { - uint a = 3; - this.g(); - assert(a == 3); - g(); - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); -} - BOOST_AUTO_TEST_CASE(branches_merge_variables) { // Branch does not touch variable a diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol new file mode 100644 index 00000000..d0f263eb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(blockhash(2) > 0); + } +} +// ---- +// Warning: (86-98): Assertion checker does not yet support this special variable. +// Warning: (86-98): Assertion checker does not yet implement this type. +// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons +// Warning: (86-102): Internal error: Expression undefined for SMT solver. +// Warning: (79-103): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol new file mode 100644 index 00000000..ec56d957 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + assert(gasleft() > 0); + } +} +// ---- +// Warning: (76-97): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol new file mode 100644 index 00000000..40e5d987 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/many.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sender == block.coinbase); + assert(block.difficulty == block.gaslimit); + assert(block.number == block.timestamp); + assert(tx.gasprice == msg.value); + assert(tx.origin == msg.sender); + uint x = block.number; + assert(x + 2 > block.number); + assert(now > 10); + assert(gasleft() > 100); + } +} +// ---- +// Warning: (79-115): Assertion violation happens here +// Warning: (119-161): Assertion violation happens here +// Warning: (165-204): Assertion violation happens here +// Warning: (208-240): Assertion violation happens here +// Warning: (244-275): Assertion violation happens here +// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (336-352): Assertion violation happens here +// Warning: (356-379): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol new file mode 100644 index 00000000..7e748f09 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.data.length > 0); + } +} +// ---- +// Warning: (86-101): Assertion checker does not yet support this expression. +// Warning: (86-94): Assertion checker does not yet support this special variable. +// Warning: (86-94): Assertion checker does not yet implement this type. +// Warning: (86-101): Internal error: Expression undefined for SMT solver. +// Warning: (79-106): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol new file mode 100644 index 00000000..dd2366e2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol new file mode 100644 index 00000000..ad45d076 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + require(msg.sender != address(0)); + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} +// ---- +// Warning: (98-108): Assertion checker does not yet implement this expression. +// Warning: (98-108): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol new file mode 100644 index 00000000..9a4eefd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address c) public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + assert(c == msg.sender); + } +} +// ---- +// Warning: (155-178): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol new file mode 100644 index 00000000..6f832179 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sig == 0x00000000); + } +} +// ---- +// Warning: (86-93): Assertion checker does not yet support this special variable. +// Warning: (86-93): Assertion checker does not yet implement this type. +// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons +// Warning: (86-107): Internal error: Expression undefined for SMT solver. +// Warning: (79-108): Assertion violation happens here -- cgit From e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 22 Oct 2018 18:19:11 +0200 Subject: Add gasleft constraint and use full member access name --- test/libsolidity/smtCheckerTests/special/difficulty.sol | 10 ++++++++++ test/libsolidity/smtCheckerTests/special/gasleft.sol | 4 ++++ 2 files changed, 14 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/special/difficulty.sol (limited to 'test') diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol new file mode 100644 index 00000000..4469d4e5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint difficulty) public view { + assert(block.difficulty == difficulty); + } +} +// ---- +// Warning: (91-129): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol index ec56d957..857230fe 100644 --- a/test/libsolidity/smtCheckerTests/special/gasleft.sol +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -4,7 +4,11 @@ contract C { function f() public view { assert(gasleft() > 0); + uint g = gasleft(); + assert(g < gasleft()); + assert(g >= gasleft()); } } // ---- // Warning: (76-97): Assertion violation happens here +// Warning: (123-144): Assertion violation happens here -- cgit