From ff76c989acc69e452144469898868e296674ef4a Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 11 Jan 2021 13:35:12 +0100 Subject: [PATCH] addressing review comments --- libsolidity/formal/BMC.cpp | 3 +- libsolidity/formal/CHC.cpp | 35 +++++++------------ .../smtCheckerTests/try_catch/try_4.sol | 6 ++-- .../try_string_literal_to_bytes_array.sol | 17 +++++++++ .../try_string_literal_to_fixed_bytes.sol | 17 +++++++++ 5 files changed, 53 insertions(+), 25 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol create mode 100644 test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 0d1364bce..52dc06e62 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -354,7 +354,8 @@ bool BMC::visit(TryStatement const& _tryStatement) auto callExpr = expr(*externalCall); if (_tryStatement.successClause()->parameters()) tryCatchAssignment( - _tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)); + _tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall) + ); smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort); auto const& clauses = _tryStatement.clauses(); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 0795189b8..22bf62dbf 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -548,38 +548,29 @@ bool CHC::visit(TryStatement const& _tryStatement) solAssert(m_currentFunction, ""); auto tryHeaderBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_header_"); - auto tryAfterCallSuccessBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_success_"); - auto tryAfterCallFailBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_fail_"); auto afterTryBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock); - connectBlocks(m_currentBlock, predicate(*tryHeaderBlock)); - setCurrentBlock(*tryHeaderBlock); - // fine-grained control over how the external call is visited - // cannot use "_tryStatement.externalCall().accept(*this);" since we need to insert the "connectBlocks" - // visit(*externalCall); currently there is nothing to do here, so it's commented out - externalCall->expression().accept(*this); - ASTNode::listAccept(externalCall->arguments(), *this); - connectBlocks(m_currentBlock, predicate(*tryAfterCallFailBlock)); - endVisit(*externalCall); - - if (_tryStatement.successClause()->parameters()) - tryCatchAssignment( - _tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)); - - connectBlocks(m_currentBlock, predicate(*tryAfterCallSuccessBlock)); - auto const& clauses = _tryStatement.clauses(); solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause"); auto clauseBlocks = applyMap(clauses, [this](ASTPointer clause) { return createBlock(clause.get(), PredicateType::FunctionBlock, "try_clause_" + std::to_string(clause->id())); }); - setCurrentBlock(*tryAfterCallSuccessBlock); - connectBlocks(m_currentBlock, predicate(*clauseBlocks[0])); - - setCurrentBlock(*tryAfterCallFailBlock); + connectBlocks(m_currentBlock, predicate(*tryHeaderBlock)); + setCurrentBlock(*tryHeaderBlock); + // Visit everything, except the actual external call. + externalCall->expression().accept(*this); + ASTNode::listAccept(externalCall->arguments(), *this); + // Branch directly to all catch clauses, since in these cases, any effects of the external call are reverted. for (size_t i = 1; i < clauseBlocks.size(); ++i) connectBlocks(m_currentBlock, predicate(*clauseBlocks[i])); + // Only now visit the actual call to record its effects and connect to the success clause. + endVisit(*externalCall); + if (_tryStatement.successClause()->parameters()) + tryCatchAssignment( + _tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall) + ); + connectBlocks(m_currentBlock, predicate(*clauseBlocks[0])); for (size_t i = 0; i < clauses.size(); ++i) { diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol index c10624db4..f3ee44dfb 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol @@ -23,6 +23,8 @@ contract C { } } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (211-225): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() -// Warning 6328: (351-365): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() +// Warning 6328: (211-225): CHC: Assertion violation happens here. +// Warning 6328: (351-365): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol new file mode 100644 index 000000000..06cae9d5d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C { + + function g() public pure returns (bytes memory) { + return hex"ffff"; + } + + function f() public view { + try this.g() returns (bytes memory b) { + assert(b[0] == bytes1(uint8(255)) && b[1] == bytes1(uint8(255))); // should hold + assert(b[0] == bytes1(uint8(0)) || b[1] == bytes1(uint8(0))); // should fail + } catch { + } + } +} +// ---- +// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol new file mode 100644 index 000000000..8375aff96 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C { + + function g() public pure returns (bytes2) { + return hex"ffff"; + } + + function f() public view { + try this.g() returns (bytes2 b) { + assert(uint8(b[0]) == 255 && uint8(b[1]) == 255); // should hold + assert(uint8(b[0]) == 0 || uint8(b[1]) == 0); // should fail + } catch { + } + } +} +// ---- +// Warning 6328: (250-294): CHC: Assertion violation happens here.