diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 0edfc27ff..9e31d7fc9 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -78,6 +78,9 @@ CHC::CHC( void CHC::analyze(SourceUnit const& _source) { + if (!shouldAnalyze(_source)) + return; + if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2) { if (!m_noSolverWarning) @@ -137,6 +140,9 @@ vector CHC::unhandledQueries() const bool CHC::visit(ContractDefinition const& _contract) { + if (!shouldAnalyze(_contract)) + return false; + resetContractAnalysis(); initContract(_contract); clearIndices(&_contract); @@ -152,6 +158,9 @@ bool CHC::visit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract) { + if (!shouldAnalyze(_contract)) + return; + for (auto base: _contract.annotation().linearizedBaseContracts) { if (auto constructor = base->constructor()) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 68545f4f6..b42e9b355 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1035,6 +1035,12 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) } } +bool SMTEncoder::shouldAnalyze(SourceUnit const& _source) const +{ + return m_settings.contracts.isDefault() || + m_settings.contracts.has(*_source.annotation().path); +} + bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const { if (!_contract.canBeDeployed()) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 7ca19358d..fe84189be 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -223,6 +223,8 @@ protected: /// @returns true if @param _contract is set for analysis in the settings /// and it is not abstract. bool shouldAnalyze(ContractDefinition const& _contract) const; + /// @returns true if @param _source is set for analysis in the settings. + bool shouldAnalyze(SourceUnit const& _source) const; bool isPublicGetter(Expression const& _expr); diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol index 96223b7e9..313da678e 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol @@ -16,5 +16,5 @@ contract C { // ---- // Warning 1218: (131-165): CHC: Error trying to invoke SMT solver. // Warning 6328: (131-165): CHC: Assertion violation might happen here. -// Info 1180: Reentrancy property(ies) for :C:\n(!( >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n +// Info 1180: Reentrancy property(ies) for :C:\n(!( >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n // Warning 4661: (131-165): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol index f16964501..49d2eb33b 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol @@ -17,5 +17,4 @@ contract C { // ==== // SMTEngine: all // SMTIgnoreOS: macos -// ---- -// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!((t + ((- 1) * address(this))) = 0) || ( <= 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n((!( >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this) == t)\n = 2 -> Assertion failed at assert(a == t)\n +// SMTIgnoreInv: yes diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol index f0b5d48e1..805a75bbb 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol @@ -24,5 +24,6 @@ contract D is C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (286-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\nTransaction trace:\nD.constructor(1) +// Warning 6328: (286-300): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol index 4b51d9d9e..f6c833858 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol @@ -14,5 +14,5 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (150-186): CHC: Assertion violation might happen here. -// Warning 6328: (205-240): CHC: Assertion violation happens here. +// Warning 6328: (205-240): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 0}() -- untrusted external call // Warning 4661: (150-186): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index 3a3b295e4..c2f55fa98 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -25,4 +25,4 @@ contract C // SMTIgnoreOS: macos // ---- // Warning 6328: (234-253): CHC: Assertion violation happens here. -// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && (((map'[1] + ((- 1) * map'[0])) <= 0) || !((map[1] + ((- 1) * map[0])) <= 0)) && !( = 2))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol index 1affbb6ca..923147d49 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol @@ -25,4 +25,4 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 2072: (255-261): Unused local variable. -// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (!(x' <= 0) || !(x >= 2)) && ( <= 0) && (!(x <= 2) || !(x' >= 3)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n +// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol index 71608eabd..175b68410 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 1236\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 1 } -- reentrant call\n _i.f() -- untrusted external call +// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 32278 } -- reentrant call\n _i.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol index 206d95c46..81de958b3 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 69 }\n _i.f{ value: 100 }() -- untrusted external call +// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 83 }\n _i.f{ value: 100 }() -- untrusted external call