diff --git a/Changelog.md b/Changelog.md index 2c8314750..add5e8648 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Compiler Features: * SMTChecker: Support ABI functions as uninterpreted functions. * SMTChecker: Use checked arithmetic by default and support ``unchecked`` blocks. * SMTChecker: Show contract name in counterexample function call. + * SMTChecker: Support try/catch statements. Bugfixes: * Code Generator: Fix length check when decoding malformed error data in catch clause. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 57f2c3c8a..52dc06e62 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -345,6 +345,44 @@ bool BMC::visit(ForStatement const& _node) return false; } +bool BMC::visit(TryStatement const& _tryStatement) +{ + FunctionCall const* externalCall = dynamic_cast(&_tryStatement.externalCall()); + solAssert(externalCall && externalCall->annotation().tryCall, ""); + + externalCall->accept(*this); + auto callExpr = expr(*externalCall); + if (_tryStatement.successClause()->parameters()) + tryCatchAssignment( + _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(); + m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size()); + solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause"); + vector> touchedVars; + vector> clausesVisitResults; + for (size_t i = 0; i < clauses.size(); ++i) + { + clausesVisitResults.push_back(visitBranch(clauses[i].get())); + touchedVars.push_back(touchedVariables(*clauses[i])); + } + + // merge the information from all clauses + smtutil::Expression pathCondition = clausesVisitResults.front().second; + auto currentIndices = clausesVisitResults[0].first; + for (size_t i = 1; i < clauses.size(); ++i) + { + mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == i, clausesVisitResults[i].first, currentIndices); + currentIndices = copyVariableIndices(); + pathCondition = pathCondition || clausesVisitResults[i].second; + } + setPathCondition(pathCondition); + + return false; +} + void BMC::endVisit(UnaryOperation const& _op) { SMTEncoder::endVisit(_op); diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 6d146abbe..5f6fbad85 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -91,6 +91,7 @@ private: void endVisit(UnaryOperation const& _node) override; void endVisit(FunctionCall const& _node) override; void endVisit(Return const& _node) override; + bool visit(TryStatement const& _node) override; //@} /// Visitor helpers. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 3e6e711a5..22bf62dbf 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -541,6 +541,48 @@ void CHC::endVisit(Return const& _return) m_currentBlock = predicate(*returnGhost); } +bool CHC::visit(TryStatement const& _tryStatement) +{ + FunctionCall const* externalCall = dynamic_cast(&_tryStatement.externalCall()); + solAssert(externalCall && externalCall->annotation().tryCall, ""); + solAssert(m_currentFunction, ""); + + auto tryHeaderBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_header_"); + auto afterTryBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock); + + 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())); + }); + + 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) + { + setCurrentBlock(*clauseBlocks[i]); + clauses[i]->accept(*this); + connectBlocks(m_currentBlock, predicate(*afterTryBlock)); + } + setCurrentBlock(*afterTryBlock); + + return false; +} + void CHC::pushInlineFrame(CallableDeclaration const& _callable) { m_returnDests.push_back(createBlock(&_callable, PredicateType::FunctionBlock, "return_")); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8cf5255c9..af338ec2e 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -84,6 +84,7 @@ private: void endVisit(Continue const& _node) override; void endVisit(IndexRangeAccess const& _node) override; void endVisit(Return const& _node) override; + bool visit(TryStatement const& _node) override; void pushInlineFrame(CallableDeclaration const& _callable) override; void popInlineFrame(CallableDeclaration const& _callable) override; diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 0cc31d75f..2e73a418f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -312,20 +312,6 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm) return false; } -bool SMTEncoder::visit(TryCatchClause const& _clause) -{ - if (auto params = _clause.parameters()) - for (auto const& var: params->parameters()) - createVariable(*var); - - m_errorReporter.warning( - 7645_error, - _clause.location(), - "Assertion checker does not support try/catch clauses." - ); - return false; -} - void SMTEncoder::pushInlineFrame(CallableDeclaration const&) { pushPathCondition(currentPathConditions()); @@ -2121,6 +2107,26 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment return values.first; } +void SMTEncoder::tryCatchAssignment(vector> const& _variables, smt::SymbolicVariable const& _rhs) +{ + if (_variables.size() > 1) + { + auto const* symbTuple = dynamic_cast(&_rhs); + solAssert(symbTuple, ""); + auto const& symbComponents = symbTuple->components(); + solAssert(symbComponents.size() == _variables.size(), ""); + for (unsigned i = 0; i < symbComponents.size(); ++i) + { + auto param = _variables.at(i); + solAssert(param, ""); + solAssert(m_context.knownVariable(*param), ""); + assignment(*param, symbTuple->component(i)); + } + } + else if (_variables.size() == 1) + assignment(*_variables.front(), _rhs.currentValue()); +} + void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value) { // In general, at this point, the SMT sorts of _variable and _value are the same, @@ -2688,7 +2694,29 @@ vector SMTEncoder::stateVariablesIncludingInheritedA vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) { - return _function.localVariables() + modifiersVariables(_function, _contract); + return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract); +} + +vector SMTEncoder::tryCatchVariables(FunctionDefinition const& _function) +{ + struct TryCatchVarsVisitor : public ASTConstVisitor + { + bool visit(TryCatchClause const& _catchClause) override + { + if (_catchClause.parameters()) + { + auto const& params = _catchClause.parameters()->parameters(); + for (auto param: params) + vars.push_back(param.get()); + } + + return false; + } + + vector vars; + } tryCatchVarsVisitor; + _function.accept(tryCatchVarsVisitor); + return tryCatchVarsVisitor.vars; } vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 308f17348..bc0a9482a 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -76,6 +76,7 @@ public: static std::vector localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract); static std::vector modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract); + static std::vector tryCatchVariables(FunctionDefinition const& _function); /// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr. static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract); @@ -130,7 +131,7 @@ protected: bool visit(InlineAssembly const& _node) override; void endVisit(Break const&) override {} void endVisit(Continue const&) override {} - bool visit(TryCatchClause const& _node) override; + bool visit(TryStatement const&) override { return false; } virtual void pushInlineFrame(CallableDeclaration const&); virtual void popInlineFrame(CallableDeclaration const&); @@ -237,6 +238,8 @@ protected: void tupleAssignment(Expression const& _left, Expression const& _right); /// Computes the right hand side of a compound assignment. smtutil::Expression compoundAssignment(Assignment const& _assignment); + /// Handles assignment of the result of external call in try statement to the parameters of success clause + void tryCatchAssignment(std::vector> const& _variables, smt::SymbolicVariable const& rhs); /// Maps a variable to an SSA index. using VariableIndices = std::unordered_map; diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol new file mode 100644 index 000000000..eb6fe4756 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; +contract C { + + function g() public pure {} + + function f() public view { + uint x = 0; + bool success = false; + try this.g() { + success = true; + x = 1; + } catch Error (string memory /*reason*/) { + x = 2; + } catch (bytes memory /*reason*/) { + x = 3; + } + assert(x > 0 && x < 4); // should hold + assert(x == 0); // should fail + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 4661: (338-352): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol new file mode 100644 index 000000000..136d96542 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; +contract C { + + struct S { + uint x; + int y; + } + + function g() public pure returns (bool b, S memory s) { + b = true; + s.x = 42; + s.y = -1; + } + + function f() public view { + bool success = false; + try this.g() returns (bool b, S memory s) { + success = true; + assert(b && s.x == 42 && s.y == -1); // should hold + } catch { + } + assert(success); // fails, not guaranteed that there will be no error + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 4661: (368-383): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol index 921aeea7b..9f15677dc 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol @@ -9,7 +9,3 @@ contract C { // EVMVersion: >=byzantium // ---- // Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 7645: (98-121): Assertion checker does not support try/catch clauses. -// Warning 7645: (124-159): Assertion checker does not support try/catch clauses. -// Warning 7645: (98-121): Assertion checker does not support try/catch clauses. -// Warning 7645: (124-159): Assertion checker does not support try/catch clauses. diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol index ed1971b4a..b0b9706fd 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol @@ -10,7 +10,3 @@ contract C { // ==== // EVMVersion: >=byzantium // ---- -// Warning 7645: (83-85): Assertion checker does not support try/catch clauses. -// Warning 7645: (88-122): Assertion checker does not support try/catch clauses. -// Warning 7645: (83-85): Assertion checker does not support try/catch clauses. -// Warning 7645: (88-122): Assertion checker does not support try/catch clauses. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_1.sol b/test/libsolidity/smtCheckerTests/try_catch/try_1.sol new file mode 100644 index 000000000..4f2755f80 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_1.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C { + int x; + + function g() public { + x = 42; + } + + function f() public { + x = 0; + bool success = false; + try this.g() { + success = true; + } catch (bytes memory s) { + assert(x == 0); // should hold + } + assert(success); // fails for now, since external call is over-approximated (both success and fail are considered possible) for now even for known code + } +} +// ---- +// Warning 5667: (195-209): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (253-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_2.sol new file mode 100644 index 000000000..8f80601e4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_2.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +contract C { + int x; + + function g() public { + x = 42; + } + + function f() public { + x = 0; + try this.g() { + assert(x == 42); // should hold + } catch (bytes memory s) { + assert(x == 0); // should hold + } + } +} +// ---- +// Warning 5667: (187-201): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol new file mode 100644 index 000000000..b3e7c7e1e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; +contract C { + int x; + + function g(int y) public pure returns (int) { + return y; + } + + function postinc() internal returns (int) { + x += 1; + return x; + } + + function f() public { + x = 0; + try this.g(postinc()) { + assert(x == 1); // should hold + } catch (bytes memory s) { + assert(x == 0); // should fail - state is reverted to the state after postinc(), but before the call to this.g() + } + } +} +// ---- +// Warning 5667: (291-305): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol new file mode 100644 index 000000000..f3ee44dfb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + + int x; + D d; + + function set(int n) public { + x = n; + } + + function f() public { + x = 0; + try d.d() { + assert(x == 0); // should fail, x can be anything here + } catch { + assert(x == 0); // should hold, all changes to x has been reverted + assert(x == 1); // should fail + } + } +} +// ==== +// SMTIgnoreCex: yes +// ---- +// 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_5.sol b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol new file mode 100644 index 000000000..2c7a68674 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + + int x; + D d; + + function set(int n) public { + require(n < 100); + x = n; + } + + function f() public { + x = 0; + try d.d() { + assert(x < 100); // should hold + } catch { + assert(x == 0); // should hold, all changes to x has been reverted + assert(x == 1); // should fail + } + } +} +// ---- +// Warning 6328: (348-362): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol b/test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol new file mode 100644 index 000000000..ec9ed22f1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + function g(bool b) public {} + function f(bool b) public returns (bytes memory txt) { + if (0==1) + try this.g(b) {} + catch (bytes memory s) { + txt = s; + } + } +} + +// ---- +// Warning 6838: (141-145): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol new file mode 100644 index 000000000..465773b7b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f() public returns (uint) { + while(1==1) + try this.f() returns (uint b) { + b = 2; + } catch { + } + } +} +// ---- +// Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. +// Warning 6838: (91-95): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol new file mode 100644 index 000000000..654396afd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; +contract C { + int x; + + function g() public { + x = 42; + } + + function f() public { + x = 1; + bool success = false; + try this.g() { + success = true; + assert(x == 42); // should hold + } catch Error (string memory /*reason*/) { + assert(x == 1); // should hold + } catch (bytes memory /*reason*/) { + assert(x == 1); // should hold + } + assert((success && x == 42) || (!success && x == 1)); // should hold + assert(success); // can fail + } +} +// ---- +// Warning 6328: (447-462): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol new file mode 100644 index 000000000..6aaabbc4a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C { + + function g() public pure {} + + function f() public view { + uint x = 0; + bool success = false; + try this.g() { + success = true; + x = 1; + } catch Error (string memory /*reason*/) { + x = 2; + } catch (bytes memory /*reason*/) { + x = 3; + } + assert(x > 0 && x < 4); // should hold + assert(x == 0); // should fail + } +} +// ---- +// Warning 6328: (338-352): 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_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol new file mode 100644 index 000000000..aeb76a4bc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual returns (uint x, bool b); +} + +contract C { + + int x; + D d; + + function f() public { + x = 0; + try d.d() returns (uint x, bool c) { + assert(x == 0); // should fail, x is the local variable shadowing the state variable + assert(!c); // should fail, c can be anything + } catch { + assert(x == 0); // should hold, x is the state variable + assert(x == 1); // should fail + } + } +} +// ---- +// Warning 2519: (197-203): This declaration shadows an existing declaration. +// Warning 6328: (218-232): 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: (306-316): 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: (426-440): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol new file mode 100644 index 000000000..e1294f417 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; +contract C { + + struct S { + uint x; + int y; + } + + function g() public pure returns (bool b, S memory s) { + b = true; + s.x = 42; + s.y = -1; + } + + function f() public view { + bool success = false; + try this.g() returns (bool b, S memory s) { + success = true; + assert(b && s.x == 42 && s.y == -1); + } catch { + } + assert(success); // fails, not guaranteed that there will be no error + } +} +// ---- +// Warning 6328: (353-368): 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_new.sol b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol new file mode 100644 index 000000000..563e2fdfe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; + +contract Reverts { + constructor(uint) { revert("test message."); } +} +contract Succeeds { + constructor(uint) { } +} + +contract C { + function f() public returns (Reverts x, string memory txt) { + uint i = 3; + try new Reverts(i) returns (Reverts r) { + x = r; + txt = "success"; + } catch Error(string memory s) { + txt = s; + } + } + function g() public returns (Succeeds x, string memory txt) { + uint i = 8; + try new Succeeds(i) returns (Succeeds r) { + x = r; + txt = "success"; + } catch Error(string memory s) { + txt = s; + } + } +} +// ---- +// Warning 4588: (264-278): Assertion checker does not yet implement this type of function call. +// Warning 4588: (525-540): Assertion checker does not yet implement this type of function call. +// Warning 4588: (264-278): Assertion checker does not yet implement this type of function call. +// Warning 4588: (525-540): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol new file mode 100644 index 000000000..5d044f5b7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + int public x; + + function f() public view { + try this.x() returns (int v) { + assert(x == v); // should hold + } catch { + assert(false); // this fails, because we over-approximate every external call in the way that it can both succeed and fail + } + } +} +// ---- +// Warning 6328: (171-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol new file mode 100644 index 000000000..908af50ce --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[]) public m; + + constructor() { + m[0].push(); + m[0].push(); + m[0][1] = 42; + } + + function f() public view { + try this.m(0,1) returns (uint y) { + assert(y == m[0][1]); // should hold + } + catch { + assert(m[0][1] == 42); // should hold + assert(m[0][1] == 1); // should fail + } + } +} +// ---- +// Warning 6328: (313-333): 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_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.