From 8d91ccf0284b4baa00f4438ad099f9f44a5ff8f1 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 12 Oct 2021 11:12:18 +0200 Subject: [PATCH] [SMTChecker] Add a new trusted mode which assumes that code that is available at compile time is trusted. --- Changelog.md | 1 + docs/smtchecker.rst | 182 +++++++ docs/using-the-compiler.rst | 4 + libsolidity/formal/BMC.cpp | 6 +- libsolidity/formal/CHC.cpp | 492 ++++++++++++++---- libsolidity/formal/CHC.h | 23 + libsolidity/formal/ModelCheckerSettings.cpp | 9 + libsolidity/formal/ModelCheckerSettings.h | 17 + libsolidity/formal/Predicate.cpp | 10 + libsolidity/formal/Predicate.h | 4 + libsolidity/formal/PredicateInstance.cpp | 11 +- libsolidity/formal/PredicateInstance.h | 12 +- libsolidity/formal/SMTEncoder.cpp | 47 +- libsolidity/formal/SMTEncoder.h | 15 +- libsolidity/formal/SymbolicState.cpp | 200 ++++++- libsolidity/formal/SymbolicState.h | 57 +- libsolidity/formal/SymbolicTypes.cpp | 22 + libsolidity/formal/SymbolicTypes.h | 4 + libsolidity/interface/StandardCompiler.cpp | 12 +- solc/CommandLineParser.cpp | 17 + .../err | 26 + .../model_checker_contracts_only_one/err | 2 +- .../model_checker_ext_calls_empty_arg/args | 1 + .../model_checker_ext_calls_empty_arg/err | 1 + .../model_checker_ext_calls_empty_arg/exit | 1 + .../input.sol | 15 + .../model_checker_ext_calls_trusted_chc/args | 1 + .../model_checker_ext_calls_trusted_chc/err | 5 + .../input.sol | 15 + .../args | 1 + .../model_checker_ext_calls_untrusted_chc/err | 14 + .../input.sol | 13 + .../model_checker_ext_calls_wrong_arg/args | 1 + .../model_checker_ext_calls_wrong_arg/err | 1 + .../model_checker_ext_calls_wrong_arg/exit | 1 + .../input.sol | 15 + .../output.json | 68 +++ .../output.json | 4 +- .../output.json | 4 +- .../input.json | 30 ++ .../output.json | 12 + .../input.json | 30 ++ .../output.json | 32 ++ .../input.json | 28 + .../output.json | 50 ++ .../input.json | 30 ++ .../output.json | 12 + .../input.json | 30 ++ .../output.json | 12 + .../output.json | 62 +-- test/libsolidity/SMTCheckerTest.cpp | 15 +- .../length_1d_struct_array_2d_1.sol | 2 +- .../length_same_after_assignment_3_fail.sol | 2 +- .../array_members/push_as_lhs_1d.sol | 1 + .../array_members/push_as_lhs_2d.sol | 1 + .../complex/slither/external_function.sol | 4 +- .../deployment/deploy_bmc_trusted.sol | 18 + .../deployment/deploy_bmc_untrusted.sol | 17 + .../deployment/deploy_trusted.sol | 16 + .../deployment/deploy_trusted_addresses.sol | 19 + .../deployment/deploy_trusted_flow.sol | 32 ++ ...eploy_trusted_keep_storage_constraints.sol | 17 + .../deployment/deploy_trusted_state_flow.sol | 24 + .../deploy_trusted_state_flow_2.sol | 20 + .../deploy_trusted_state_flow_3.sol | 21 + .../deploy_trusted_state_flow_4.sol | 20 + .../deployment/deploy_untrusted.sol | 17 + .../deployment/deploy_untrusted_addresses.sol | 22 + ...oy_untrusted_erase_storage_constraints.sol | 17 + .../deployment_trusted_with_value_1.sol | 20 + .../call_abstract_constructor_trusted_1.sol | 28 + .../call_abstract_constructor_trusted_2.sol | 25 + .../call_abstract_trusted_1.sol | 28 + .../call_abstract_trusted_2.sol | 25 + .../call_abstract_trusted_3.sol | 29 ++ .../external_calls/call_reentrancy_view.sol | 2 +- ...ternal_call_from_constructor_1_trusted.sol | 21 + ...ternal_call_from_constructor_2_trusted.sol | 17 + ...ternal_call_from_constructor_3_trusted.sol | 25 + .../external_call_indirect_1.sol | 41 ++ .../external_call_indirect_2.sol | 52 ++ .../external_call_indirect_3.sol | 45 ++ .../external_call_indirect_4.sol | 48 ++ .../external_call_indirect_5.sol | 50 ++ .../external_call_semantic_this_1.sol | 17 + .../external_call_semantic_this_2.sol | 16 + .../external_call_semantic_this_3.sol | 17 + ..._address_inside_array_struct_trusted_1.sol | 23 + ..._address_inside_array_struct_trusted_2.sol | 24 + ...ate_var_address_inside_array_trusted_1.sol | 21 + ...ate_var_address_inside_array_trusted_2.sol | 20 + ...te_var_address_inside_struct_trusted_1.sol | 24 + ...te_var_address_inside_struct_trusted_2.sol | 23 + ...te_var_address_inside_struct_trusted_3.sol | 26 + ...te_var_address_inside_struct_trusted_4.sol | 27 + ...contract_inside_array_struct_trusted_1.sol | 23 + ...contract_inside_array_struct_trusted_2.sol | 24 + ...te_var_contract_inside_array_trusted_1.sol | 21 + ...te_var_contract_inside_array_trusted_2.sol | 21 + ...e_var_contract_inside_struct_trusted_1.sol | 24 + ...e_var_contract_inside_struct_trusted_2.sol | 24 + ...e_var_contract_inside_struct_trusted_3.sol | 27 + ...e_var_contract_inside_struct_trusted_4.sol | 27 + .../external_call_this_with_value_1.sol | 2 +- .../external_call_this_with_value_2.sol | 6 +- .../external_hash_known_code_pure_trusted.sol | 33 ++ ..._known_code_state_reentrancy_2_trusted.sol | 47 ++ ...code_state_reentrancy_indirect_trusted.sol | 56 ++ ...sh_known_code_state_reentrancy_trusted.sol | 38 ++ ...n_code_state_reentrancy_unsafe_trusted.sol | 44 ++ ...external_hash_known_code_state_trusted.sol | 36 ++ ...l_hash_known_code_state_unsafe_trusted.sol | 40 ++ .../external_calls/external_reentrancy_2.sol | 2 +- .../external_calls/external_safe.sol | 2 + .../token_trusted_transfer_correct.sol | 64 +++ .../token_trusted_transfer_wrong.sol | 68 +++ .../file_level/new_operator.sol | 2 +- .../functions/functions_external_2.sol | 2 +- .../functions/getters/external_getter_1.sol | 22 + .../functions/getters/external_getter_2.sol | 33 ++ .../getters/external_getter_this_1.sol | 18 + .../getters/external_getter_this_2.sol | 19 + ...virtual_function_called_by_constructor.sol | 2 +- .../smtCheckerTests/imports/ExtCall.sol | 2 +- .../imports/import_as_module_2.sol | 1 + .../operators/compound_mul_mapping.sol | 3 +- .../operators/conditional_assignment_6.sol | 2 +- .../special/tx_vars_reentrancy_1.sol | 1 + .../smtCheckerTests/try_catch/try_new.sol | 4 +- .../typecast/bytes_to_fixed_bytes_1.sol | 3 + .../typecast/string_to_bytes_push_1.sol | 2 +- .../smtCheckerTests/types/bool_simple_2.sol | 1 + .../user_type_as_struct_member_1.sol | 1 - test/solc/CommandLineParser.cpp | 2 + test/tools/fuzzer_common.cpp | 1 + 135 files changed, 3156 insertions(+), 235 deletions(-) create mode 100644 test/cmdlineTests/model_checker_ext_calls_empty_arg/args create mode 100644 test/cmdlineTests/model_checker_ext_calls_empty_arg/err create mode 100644 test/cmdlineTests/model_checker_ext_calls_empty_arg/exit create mode 100644 test/cmdlineTests/model_checker_ext_calls_empty_arg/input.sol create mode 100644 test/cmdlineTests/model_checker_ext_calls_trusted_chc/args create mode 100644 test/cmdlineTests/model_checker_ext_calls_trusted_chc/err create mode 100644 test/cmdlineTests/model_checker_ext_calls_trusted_chc/input.sol create mode 100644 test/cmdlineTests/model_checker_ext_calls_untrusted_chc/args create mode 100644 test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err create mode 100644 test/cmdlineTests/model_checker_ext_calls_untrusted_chc/input.sol create mode 100644 test/cmdlineTests/model_checker_ext_calls_wrong_arg/args create mode 100644 test/cmdlineTests/model_checker_ext_calls_wrong_arg/err create mode 100644 test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit create mode 100644 test/cmdlineTests/model_checker_ext_calls_wrong_arg/input.sol create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/input.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/output.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/input.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/output.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/input.json create mode 100644 test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/output.json create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol diff --git a/Changelog.md b/Changelog.md index 7619fbd40..5ce4057a4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,7 @@ Language Features: Compiler Features: + * SMTChecker: New trusted mode that assumes that any compile-time available code is the actual used code even in external calls. This can be used via the CLI option ``--model-checker-ext-calls trusted`` or the JSON field ``settings.modelChecker.extCalls: "trusted"``. Bugfixes: diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index c16a3e5d7..276f9c33a 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -518,6 +518,188 @@ which has the following form: "source2.sol": ["contract2", "contract3"] } +Trusted External Calls +====================== + +By default, the SMTChecker does not assume that compile-time available code +is the same as the runtime code for external calls. Take the following contracts +as an example: + +.. code-block:: solidity + + // SPDX-License-Identifier: GPL-3.0 + pragma solidity >=0.8.0; + + contract Ext { + uint public x; + function setX(uint _x) public { x = _x; } + } + contract MyContract { + function callExt(Ext _e) public { + _e.setX(42); + assert(_e.x() == 42); + } + } + +When ``MyContract.callExt`` is called, an address is given as the argument. +At deployment time, we cannot know for sure that address ``_e`` actually +contains a deployment of contract ``Ext``. +Therefore, the SMTChecker will warn that the assertion above can be violated, +which is true, if ``_e`` contains another contract than ``Ext``. + +However, it can be useful to treat these external calls as trusted, for example, +to test that different implementations of an interface conform to the same property. +This means assuming that address ``_e`` indeed was deployed as contract ``Ext``. +This mode can be enabled via the CLI option ``--model-checker-ext-calls=trusted`` +or the JSON field ``settings.modelChecker.extCalls: "trusted"``. + +Please be aware that enabling this mode can make the SMTChecker analysis much more +computationally costly. + +An important part of this mode is that it is applied to contract types and high +level external calls to contracts, and not low level calls such as ``call`` and +``delegatecall``. The storage of an address is stored per contract type, and +the SMTChecker assumes that an externally called contract has the type of the +caller expression. Therefore, casting an ``address`` or a contract to +different contract types will yield different storage values and can give +unsound results if the assumptions are inconsistent, such as the example below: + +.. code-block:: solidity + + // SPDX-License-Identifier: GPL-3.0 + pragma solidity >=0.8.0; + + contract D { + constructor(uint _x) { x = _x; } + uint public x; + function setX(uint _x) public { x = _x; } + } + + contract E { + constructor() { x = 2; } + uint public x; + function setX(uint _x) public { x = _x; } + } + + contract C { + function f() public { + address d = address(new D(42)); + + // `d` was deployed as `D`, so its `x` should be 42 now. + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 43); // should fail + + // E and D have the same interface, so the following + // call would also work at runtime. + // However, the change to `E(d)` is not reflected in `D(d)`. + E(d).setX(1024); + + // Reading from `D(d)` now will show old values. + // The assertion below should fail at runtime, + // but succeeds in this mode's analysis (unsound). + assert(D(d).x() == 42); + // The assertion below should succeed at runtime, + // but fails in this mode's analysis (false positive). + assert(D(d).x() == 1024); + } + } + +Due to the above, make sure that the trusted external calls to a certain +variable of ``address`` or ``contract`` type always have the same caller +expression type. + +It is also helpful to cast the called contract's variable as the type of the +most derived type in case of inheritance. + + .. code-block:: solidity + + // SPDX-License-Identifier: GPL-3.0 + pragma solidity >=0.8.0; + + interface Token { + function balanceOf(address _a) external view returns (uint); + function transfer(address _to, uint _amt) external; + } + + contract TokenCorrect is Token { + mapping (address => uint) balance; + constructor(address _a, uint _b) { + balance[_a] = _b; + } + function balanceOf(address _a) public view override returns (uint) { + return balance[_a]; + } + function transfer(address _to, uint _amt) public override { + require(balance[msg.sender] >= _amt); + balance[msg.sender] -= _amt; + balance[_to] += _amt; + } + } + + contract Test { + function property_transfer(address _token, address _to, uint _amt) public { + require(_to != address(this)); + + TokenCorrect t = TokenCorrect(_token); + + uint xPre = t.balanceOf(address(this)); + require(xPre >= _amt); + uint yPre = t.balanceOf(_to); + + t.transfer(_to, _amt); + uint xPost = t.balanceOf(address(this)); + uint yPost = t.balanceOf(_to); + + assert(xPost == xPre - _amt); + assert(yPost == yPre + _amt); + } + } + +Note that in function ``property_transfer``, the external calls are +performed on variable ``t`` + +Another caveat of this mode are calls to state variables of contract type +outside the analyzed contract. In the code below, even though ``B`` deploys +``A``, it is also possible for the address stored in ``B.a`` to be called by +anyone outside of ``B`` in between transactions to ``B`` itself. To reflect the +possible changes to ``B.a``, the encoding allows an unbounded number of calls +to be made to ``B.a`` externally. The encoding will keep track of ``B.a``'s +storage, therefore assertion (2) should hold. However, currently the encoding +allows such calls to be made from ``B`` conceptually, therefore assertion (3) +fails. Making the encoding stronger logically is an extension of the trusted +mode and is under development. Note that the encoding does not keep track of +storage for ``address`` variables, therefore if ``B.a`` had type ``address`` +the encoding would assume that its storage does not change in between +transactions to ``B``. + + .. code-block:: solidity + + pragma solidity >=0.8.0; + + contract A { + uint public x; + address immutable public owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + } + + contract B { + A a; + constructor() { + a = new A(); + assert(a.x() == 0); // (1) should hold + } + function g() public view { + assert(a.owner() == address(this)); // (2) should hold + assert(a.x() == 0); // (3) should hold, but fails due to a false positive + } + } + Reported Inferred Inductive Invariants ====================================== diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 6d6264e1a..251a2c053 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -433,6 +433,10 @@ Input Description "divModNoSlacks": false, // Choose which model checker engine to use: all (default), bmc, chc, none. "engine": "chc", + // Choose whether external calls should be considered trusted in case the + // code of the called function is available at compile-time. + // For details see the SMTChecker section. + "extCalls": "trusted", // Choose which types of invariants should be reported to the user: contract, reentrancy. "invariants": ["contract", "reentrancy"], // Choose whether to output all unproved targets. The default is `false`. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 0b4f34781..d17b5c93a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -82,7 +82,7 @@ void BMC::analyze(SourceUnit const& _source, map(*_funCall.expression().annotation().type); if (funType.kind() == FunctionType::Kind::External) - return isTrustedExternalCall(&_funCall.expression()); + return isExternalCallToThis(&_funCall.expression()); else if (funType.kind() != FunctionType::Kind::Internal) return false; @@ -567,7 +567,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract)) inlineFunctionCall(_funCall); - else if (isPublicGetter(_funCall.expression())) + else if (publicGetter(_funCall.expression())) { // Do nothing here. // The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 83602ace3..db6742625 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -104,7 +104,7 @@ void CHC::analyze(SourceUnit const& _source) auto sources = sourceDependencies(_source); collectFreeFunctions(sources); createFreeConstants(sources); - state().prepareForSourceUnit(_source); + state().prepareForSourceUnit(_source, encodeExternalCallsAsTrusted()); for (auto const* source: sources) defineInterfacesAndSummaries(*source); @@ -175,15 +175,30 @@ void CHC::endVisit(ContractDefinition const& _contract) smtutil::Expression zeroes(true); for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract)) zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type()); + + smtutil::Expression newAddress = encodeExternalCallsAsTrusted() ? + !state().addressActive(state().thisAddress()) : + smtutil::Expression(true); + // The contract's address might already have funds before deployment, // so the balance must be at least `msg.value`, but not equals. auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value"); addRule(smtutil::Expression::implies( - initialConstraints(_contract) && zeroes && initialBalanceConstraint, + initialConstraints(_contract) && zeroes && newAddress && initialBalanceConstraint, predicate(entry) ), entry.functor().name); + setCurrentBlock(entry); + if (encodeExternalCallsAsTrusted()) + { + auto const& entryAfterAddress = *createConstructorBlock(_contract, "implicit_constructor_entry_after_address"); + state().setAddressActive(state().thisAddress(), true); + + connectBlocks(m_currentBlock, predicate(entryAfterAddress)); + setCurrentBlock(entryAfterAddress); + } + solAssert(!m_errorDest, ""); m_errorDest = m_constructorSummaries.at(&_contract); // We need to evaluate the base constructor calls (arguments) from derived -> base @@ -220,6 +235,9 @@ void CHC::endVisit(ContractDefinition const& _contract) m_context.addAssertion(errorFlag().currentValue() == 0); } + if (encodeExternalCallsAsTrusted()) + state().writeStateVars(_contract, state().thisAddress()); + connectBlocks(m_currentBlock, summary(_contract)); setCurrentBlock(*m_constructorSummaries.at(&_contract)); @@ -550,10 +568,12 @@ void CHC::endVisit(FunctionCall const& _funCall) externalFunctionCall(_funCall); SMTEncoder::endVisit(_funCall); break; + case FunctionType::Kind::Creation: + visitDeployment(_funCall); + break; case FunctionType::Kind::DelegateCall: case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: - case FunctionType::Kind::Creation: SMTEncoder::endVisit(_funCall); unknownFunctionCall(_funCall); break; @@ -717,6 +737,19 @@ void CHC::visitAssert(FunctionCall const& _funCall) verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition); } +void CHC::visitPublicGetter(FunctionCall const& _funCall) +{ + createExpr(_funCall); + if (encodeExternalCallsAsTrusted()) + { + auto const& access = dynamic_cast(_funCall.expression()); + auto const& contractType = dynamic_cast(*access.expression().annotation().type); + state().writeStateVars(*m_currentContract, state().thisAddress()); + state().readStateVars(contractType.contractDefinition(), expr(access.expression())); + } + SMTEncoder::visitPublicGetter(_funCall); +} + void CHC::visitAddMulMod(FunctionCall const& _funCall) { solAssert(_funCall.arguments().at(2), ""); @@ -726,6 +759,66 @@ void CHC::visitAddMulMod(FunctionCall const& _funCall) SMTEncoder::visitAddMulMod(_funCall); } +void CHC::visitDeployment(FunctionCall const& _funCall) +{ + if (!encodeExternalCallsAsTrusted()) + { + SMTEncoder::endVisit(_funCall); + unknownFunctionCall(_funCall); + return; + } + + auto [callExpr, callOptions] = functionCallExpression(_funCall); + auto funType = dynamic_cast(callExpr->annotation().type); + ContractDefinition const* contract = + &dynamic_cast(*funType->returnParameterTypes().front()).contractDefinition(); + + // copy state variables from m_currentContract to state.storage. + state().writeStateVars(*m_currentContract, state().thisAddress()); + errorFlag().increaseIndex(); + + Expression const* value = valueOption(callOptions); + if (value) + decreaseBalanceFromOptionsValue(*value); + + auto originalTx = state().tx(); + newTxConstraints(value); + + auto prevThisAddr = state().thisAddress(); + auto newAddr = state().newThisAddress(); + + if (auto constructor = contract->constructor()) + { + auto const& args = _funCall.sortedArguments(); + auto const& params = constructor->parameters(); + solAssert(args.size() == params.size(), ""); + for (auto [arg, param]: ranges::zip_view(args, params)) + m_context.addAssertion(expr(*arg) == m_context.variable(*param)->currentValue()); + } + for (auto var: stateVariablesIncludingInheritedAndPrivate(*contract)) + m_context.variable(*var)->increaseIndex(); + Predicate const& constructorSummary = *m_constructorSummaries.at(contract); + m_context.addAssertion(smt::constructorCall(constructorSummary, m_context, false)); + + solAssert(m_errorDest, ""); + connectBlocks( + m_currentBlock, + predicate(*m_errorDest), + errorFlag().currentValue() > 0 + ); + m_context.addAssertion(errorFlag().currentValue() == 0); + + m_context.addAssertion(state().newThisAddress() == prevThisAddr); + + // copy state variables from state.storage to m_currentContract. + state().readStateVars(*m_currentContract, state().thisAddress()); + + state().newTx(); + m_context.addAssertion(originalTx == state().tx()); + + defineExpr(_funCall, newAddr); +} + void CHC::internalFunctionCall(FunctionCall const& _funCall) { solAssert(m_currentContract, ""); @@ -750,6 +843,53 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(errorFlag().currentValue() == 0); } +void CHC::addNondetCalls(ContractDefinition const& _contract) +{ + for (auto var: _contract.stateVariables()) + if (auto contractType = dynamic_cast(var->type())) + { + auto const& symbVar = m_context.variable(*var); + m_context.addAssertion(symbVar->currentValue() == symbVar->valueAtIndex(0)); + nondetCall(contractType->contractDefinition(), *var); + } +} + +void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var) +{ + auto address = m_context.variable(_var)->currentValue(); + // Load the called contract's state variables from the global state. + state().readStateVars(_contract, address); + + m_context.addAssertion(state().state() == state().state(0)); + auto preCallState = vector{state().state()} + currentStateVariables(_contract); + + state().newState(); + for (auto const* var: _contract.stateVariables()) + m_context.variable(*var)->increaseIndex(); + + auto error = errorFlag().increaseIndex(); + + Predicate const& callPredicate = *createSymbolicBlock( + nondetInterfaceSort(_contract, state()), + "nondet_call_" + uniquePrefix(), + PredicateType::FunctionSummary, + &_var, + m_currentContract + ); + auto postCallState = vector{state().state()} + currentStateVariables(_contract); + vector stateExprs{error, address, state().abi(), state().crypto()}; + + auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState); + auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); + + addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name); + + m_context.addAssertion(nondetCall); + + // Load the called contract's state variables into the global state. + state().writeStateVars(_contract, address); +} + void CHC::externalFunctionCall(FunctionCall const& _funCall) { /// In external function calls we do not add a "predicate call" @@ -757,15 +897,10 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) /// so we just add the nondet_interface predicate. solAssert(m_currentContract, ""); + auto [callExpr, callOptions] = functionCallExpression(_funCall); - - if (isTrustedExternalCall(callExpr)) - { - externalFunctionCallToTrustedCode(_funCall); - return; - } - FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); + auto kind = funType.kind(); solAssert( kind == FunctionType::Kind::External || @@ -774,37 +909,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) "" ); - bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall; - solAssert(m_currentContract, ""); - auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - if (function) + // Only consider high level external calls in trusted mode. + if ( + kind == FunctionType::Kind::External && + (encodeExternalCallsAsTrusted() || isExternalCallToThis(callExpr)) + ) { - usesStaticCall |= function->stateMutability() == StateMutability::Pure || - function->stateMutability() == StateMutability::View; - for (auto var: function->returnParameters()) - m_context.variable(*var)->increaseIndex(); + externalFunctionCallToTrustedCode(_funCall); + return; } + // Low level calls are still encoded nondeterministically. + + auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); + if (function) + for (auto var: function->returnParameters()) + m_context.variable(*var)->increaseIndex(); + + // If we see a low level call in trusted mode, + // we need to havoc the global state. + if ( + kind == FunctionType::Kind::BareCall && + encodeExternalCallsAsTrusted() + ) + state().newStorage(); + + // No reentrancy from constructor calls. if (!m_currentFunction || m_currentFunction->isConstructor()) return; - if (callOptions) - { - optional valueIndex; - for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate) - if (name && *name == "value") - { - valueIndex = i; - break; - } - if (valueIndex) - state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex))); - } + if (Expression const* value = valueOption(callOptions)) + decreaseBalanceFromOptionsValue(*value); auto preCallState = vector{state().state()} + currentStateVariables(); - if (!usesStaticCall) + if (!usesStaticCall(_funCall)) { state().newState(); for (auto const* var: m_stateVariables) @@ -843,8 +983,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) { + if (publicGetter(_funCall.expression())) + visitPublicGetter(_funCall); + solAssert(m_currentContract, ""); - FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + + auto [callExpr, callOptions] = functionCallExpression(_funCall); + FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); + auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); @@ -854,14 +1000,25 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) // External call creates a new transaction. auto originalTx = state().tx(); - auto txOrigin = state().txMember("tx.origin"); - state().newTx(); - // set the transaction sender as this contract - m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress()); - // set the transaction value as 0 - m_context.addAssertion(state().txMember("msg.value") == 0); - // set the origin to be the current transaction origin - m_context.addAssertion(state().txMember("tx.origin") == txOrigin); + Expression const* value = valueOption(callOptions); + newTxConstraints(value); + + auto calledAddress = contractAddressValue(_funCall); + if (value) + { + decreaseBalanceFromOptionsValue(*value); + state().addBalance(calledAddress, expr(*value)); + } + + if (encodeExternalCallsAsTrusted()) + { + // The order here is important!! Write should go first. + + // Load the caller contract's state variables into the global state. + state().writeStateVars(*m_currentContract, state().thisAddress()); + // Load the called contract's state variables from the global state. + state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall)); + } smtutil::Expression pred = predicate(_funCall); @@ -878,6 +1035,17 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) (errorFlag().currentValue() > 0) ); m_context.addAssertion(errorFlag().currentValue() == 0); + + if (!usesStaticCall(_funCall)) + if (encodeExternalCallsAsTrusted()) + { + // The order here is important!! Write should go first. + + // Load the called contract's state variables into the global state. + state().writeStateVars(*function->annotation().contract, contractAddressValue(_funCall)); + // Load the caller contract's state variables from the global state. + state().readStateVars(*m_currentContract, state().thisAddress()); + } } void CHC::unknownFunctionCall(FunctionCall const&) @@ -1088,6 +1256,14 @@ set CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot) return verificationTargetsIds; } +bool CHC::usesStaticCall(FunctionCall const& _funCall) +{ + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + auto kind = funType.kind(); + auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); + return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall; +} + optional CHC::natspecOptionFromString(string const& _option) { static map options{ @@ -1128,6 +1304,11 @@ SortPointer CHC::sort(FunctionDefinition const& _function) return functionBodySort(_function, m_currentContract, state()); } +bool CHC::encodeExternalCallsAsTrusted() +{ + return m_settings.externalCalls.isTrusted(); +} + SortPointer CHC::sort(ASTNode const* _node) { if (auto funDef = dynamic_cast(_node)) @@ -1232,6 +1413,62 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256())); state().addBalance(state().thisAddress(), k.currentValue()); + if (encodeExternalCallsAsTrusted()) + { + // If the contract has state variables that are addresses to other contracts, + // we need to encode the fact that those contracts may have been called in between + // transactions to _contract. + // + // We do that by adding nondet_interface constraints for those contracts, + // in the last line of this if block. + // + // If there are state variables of container types like structs or arrays + // that indirectly contain contract types, we havoc the state for simplicity, + // in the first part of this block. + // TODO: This could actually be supported. + // For structs: simply collect the SMT expressions of all the indirect contract type members. + // For arrays: more involved, needs to traverse the array symbolically and do the same for each contract. + // For mappings: way more complicated if the element type is a contract. + auto hasContractOrAddressSubType = [&](VariableDeclaration const* _var) -> bool { + bool foundContract = false; + solidity::util::BreadthFirstSearch bfs{{_var->type()}}; + bfs.run([&](auto _type, auto&& _addChild) { + if ( + _type->category() == Type::Category::Address || + _type->category() == Type::Category::Contract + ) + { + foundContract = true; + bfs.abort(); + } + if (auto const* mapType = dynamic_cast(_type)) + _addChild(mapType->valueType()); + else if (auto const* arrayType = dynamic_cast(_type)) + _addChild(arrayType->baseType()); + else if (auto const* structType = dynamic_cast(_type)) + for (auto const& member: structType->nativeMembers(nullptr)) + _addChild(member.type); + }); + return foundContract; + }; + bool found = false; + for (auto var: m_currentContract->stateVariables()) + if ( + var->type()->category() != Type::Category::Address && + var->type()->category() != Type::Category::Contract && + hasContractOrAddressSubType(var) + ) + { + found = true; + break; + } + + if (found) + state().newStorage(); + else + addNondetCalls(*m_currentContract); + } + errorFlag().increaseIndex(); m_context.addAssertion(summaryCall(_function)); @@ -1308,28 +1545,28 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); } -smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract) -{ - return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); -} - -smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract) -{ - return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context); -} - smtutil::Expression CHC::summary(FunctionDefinition const& _function) { solAssert(m_currentContract, ""); return summary(_function, *m_currentContract); } +smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); +} + smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function) { solAssert(m_currentContract, ""); return summaryCall(_function, *m_currentContract); } +smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context); +} + smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function) { solAssert(m_currentContract, ""); @@ -1516,18 +1753,19 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), ""); - bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; + if (kind == FunctionType::Kind::Internal) + contract = m_currentContract; - args += currentStateVariables(*m_currentContract); - args += symbolicArguments(_funCall, m_currentContract); - if (!m_currentContract->isLibrary() && !usesStaticCall) + args += currentStateVariables(*contract); + args += symbolicArguments(_funCall, contract); + if (!usesStaticCall(_funCall)) { state().newState(); - for (auto const& var: m_stateVariables) + for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract)) m_context.variable(*var)->increaseIndex(); } args += vector{state().state()}; - args += currentStateVariables(*m_currentContract); + args += currentStateVariables(*contract); for (auto var: function->parameters() + function->returnParameters()) { @@ -1538,14 +1776,14 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) args.push_back(currentValue(*var)); } - Predicate const& summary = *m_summaries.at(m_currentContract).at(function); - auto from = smt::function(summary, m_currentContract, m_context); + Predicate const& summary = *m_summaries.at(contract).at(function); + auto from = smt::function(summary, contract, m_context); Predicate const& callPredicate = *createSummaryBlock( *function, - *m_currentContract, + *contract, kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted ); - auto to = smt::function(callPredicate, m_currentContract, m_context); + auto to = smt::function(callPredicate, contract, m_context); addRule(smtutil::Expression::implies(from, to), to.name); return callPredicate(args); @@ -1910,60 +2148,63 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name); auto const& summaryArgs = summaryNode.arguments; - auto stateVars = summaryPredicate->stateVariables(); - solAssert(stateVars.has_value(), ""); - auto stateValues = summaryPredicate->summaryStateValues(summaryArgs); - solAssert(stateValues.size() == stateVars->size(), ""); - - if (first) + if (!summaryPredicate->programVariable()) { - first = false; - /// Generate counterexample message local to the failed target. - localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n"; + auto stateVars = summaryPredicate->stateVariables(); + solAssert(stateVars.has_value(), ""); + auto stateValues = summaryPredicate->summaryStateValues(summaryArgs); + solAssert(stateValues.size() == stateVars->size(), ""); - if (auto calledFun = summaryPredicate->programFunction()) + if (first) { - auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs); - auto const& inParams = calledFun->parameters(); - if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty()) - localState += inStr + "\n"; - auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs); - auto const& outParams = calledFun->returnParameters(); - if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty()) - localState += outStr + "\n"; + first = false; + /// Generate counterexample message local to the failed target. + localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n"; - optional localErrorId; - solidity::util::BreadthFirstSearch bfs{{summaryId}}; - bfs.run([&](auto _nodeId, auto&& _addChild) { - auto const& children = _graph.edges.at(_nodeId); - if ( - children.size() == 1 && - nodePred(children.front())->isFunctionErrorBlock() - ) - { - localErrorId = children.front(); - bfs.abort(); - } - ranges::for_each(children, _addChild); - }); - - if (localErrorId.has_value()) + if (auto calledFun = summaryPredicate->programFunction()) { - auto const* localError = nodePred(*localErrorId); - solAssert(localError && localError->isFunctionErrorBlock(), ""); - auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId)); - if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty()) - localState += localStr + "\n"; + auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs); + auto const& inParams = calledFun->parameters(); + if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty()) + localState += inStr + "\n"; + auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs); + auto const& outParams = calledFun->returnParameters(); + if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty()) + localState += outStr + "\n"; + + optional localErrorId; + solidity::util::BreadthFirstSearch bfs{{summaryId}}; + bfs.run([&](auto _nodeId, auto&& _addChild) { + auto const& children = _graph.edges.at(_nodeId); + if ( + children.size() == 1 && + nodePred(children.front())->isFunctionErrorBlock() + ) + { + localErrorId = children.front(); + bfs.abort(); + } + ranges::for_each(children, _addChild); + }); + + if (localErrorId.has_value()) + { + auto const* localError = nodePred(*localErrorId); + solAssert(localError && localError->isFunctionErrorBlock(), ""); + auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId)); + if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty()) + localState += localStr + "\n"; + } } } - } - else - { - auto modelMsg = formatVariableModel(*stateVars, stateValues, ", "); - /// We report the state after every tx in the trace except for the last, which is reported - /// first in the code above. - if (!modelMsg.empty()) - path.emplace_back("State: " + modelMsg); + else + { + auto modelMsg = formatVariableModel(*stateVars, stateValues, ", "); + /// We report the state after every tx in the trace except for the last, which is reported + /// first in the code above. + if (!modelMsg.empty()) + path.emplace_back("State: " + modelMsg); + } } string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider); @@ -1992,6 +2233,12 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (calls.size() > callTraceSize + 1) calls.front() += ", synthesized as:"; } + else if (pred->programVariable()) + { + calls.front() += "-- action on external contract in state variable \"" + pred->programVariable()->name() + "\""; + if (calls.size() > callTraceSize + 1) + calls.front() += ", synthesized as:"; + } else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted()) calls.front() += " -- reentrant call"; }; @@ -2047,7 +2294,8 @@ map> CHC::summaryCalls(CHCSolverInterface::CexGraph c nodePred->isInternalCall() || nodePred->isExternalCallTrusted() || nodePred->isExternalCallUntrusted() || - rootPred->isExternalCallUntrusted() + rootPred->isExternalCallUntrusted() || + rootPred->programVariable() )) { calls[root].push_back(node); @@ -2105,3 +2353,31 @@ SymbolicIntVariable& CHC::errorFlag() { return state().errorFlag(); } + +void CHC::newTxConstraints(Expression const* _value) +{ + auto txOrigin = state().txMember("tx.origin"); + state().newTx(); + // set the transaction sender as this contract + m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress()); + // set the origin to be the current transaction origin + m_context.addAssertion(state().txMember("tx.origin") == txOrigin); + + if (_value) + // set the msg value + m_context.addAssertion(state().txMember("msg.value") == expr(*_value)); +} + +frontend::Expression const* CHC::valueOption(FunctionCallOptions const* _options) +{ + if (_options) + for (auto&& [i, name]: _options->names() | ranges::views::enumerate) + if (name && *name == "value") + return _options->options().at(i).get(); + return nullptr; +} + +void CHC::decreaseBalanceFromOptionsValue(Expression const& _value) +{ + state().addBalance(state().thisAddress(), 0 - expr(_value)); +} diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8b81ffb59..c113f8583 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -110,10 +110,14 @@ private: void popInlineFrame(CallableDeclaration const& _callable) override; void visitAssert(FunctionCall const& _funCall); + void visitPublicGetter(FunctionCall const& _funCall) override; void visitAddMulMod(FunctionCall const& _funCall) override; + void visitDeployment(FunctionCall const& _funCall); void internalFunctionCall(FunctionCall const& _funCall); void externalFunctionCall(FunctionCall const& _funCall); void externalFunctionCallToTrustedCode(FunctionCall const& _funCall); + void addNondetCalls(ContractDefinition const& _contract); + void nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var); void unknownFunctionCall(FunctionCall const& _funCall); void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override; @@ -135,6 +139,7 @@ private: void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; void setCurrentBlock(Predicate const& _block); std::set transactionVerificationTargetsIds(ASTNode const* _txRoot); + bool usesStaticCall(FunctionCall const& _funCall); //@} /// SMT Natspec and abstraction helpers. @@ -148,6 +153,10 @@ private: /// @returns true if _function is Natspec annotated to be abstracted by /// nondeterministic values. bool abstractAsNondet(FunctionDefinition const& _function); + + /// @returns true if external calls should be considered trusted. + /// If that's the case, their code is used if available at compile time. + bool encodeExternalCallsAsTrusted(); //@} /// Sort helpers. @@ -310,6 +319,20 @@ private: unsigned newErrorId(); smt::SymbolicIntVariable& errorFlag(); + + /// Adds to the solver constraints that + /// - propagate tx.origin + /// - set the current contract as msg.sender + /// - set the msg.value as _value, if not nullptr + void newTxConstraints(Expression const* _value); + + /// @returns the expression representing the value sent in + /// an external call if present, + /// and nullptr otherwise. + frontend::Expression const* valueOption(FunctionCallOptions const* _options); + + /// Adds constraints that decrease the balance of the caller by _value. + void decreaseBalanceFromOptionsValue(Expression const& _value); //@} /// Predicates. diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp index 274571a15..d1e383d63 100644 --- a/libsolidity/formal/ModelCheckerSettings.cpp +++ b/libsolidity/formal/ModelCheckerSettings.cpp @@ -130,3 +130,12 @@ std::optional ModelCheckerContracts::fromString(string co return ModelCheckerContracts{chosen}; } + +std::optional ModelCheckerExtCalls::fromString(string const& _mode) +{ + if (_mode == "untrusted") + return ModelCheckerExtCalls{Mode::UNTRUSTED}; + if (_mode == "trusted") + return ModelCheckerExtCalls{Mode::TRUSTED}; + return {}; +} diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index 2c86993b9..3c1f623a0 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -140,6 +140,21 @@ struct ModelCheckerTargets std::set targets; }; +struct ModelCheckerExtCalls +{ + enum class Mode + { + UNTRUSTED, + TRUSTED + }; + + Mode mode = Mode::UNTRUSTED; + + static std::optional fromString(std::string const& _mode); + + bool isTrusted() const { return mode == Mode::TRUSTED; } +}; + struct ModelCheckerSettings { ModelCheckerContracts contracts = ModelCheckerContracts::Default(); @@ -151,6 +166,7 @@ struct ModelCheckerSettings /// might prefer the precise encoding. bool divModNoSlacks = false; ModelCheckerEngine engine = ModelCheckerEngine::None(); + ModelCheckerExtCalls externalCalls = {}; ModelCheckerInvariants invariants = ModelCheckerInvariants::Default(); bool showUnproved = false; smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3(); @@ -164,6 +180,7 @@ struct ModelCheckerSettings contracts == _other.contracts && divModNoSlacks == _other.divModNoSlacks && engine == _other.engine && + externalCalls.mode == _other.externalCalls.mode && invariants == _other.invariants && showUnproved == _other.showUnproved && solvers == _other.solvers && diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 918728d86..7119a59e8 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -144,6 +144,11 @@ FunctionCall const* Predicate::programFunctionCall() const return dynamic_cast(m_node); } +VariableDeclaration const* Predicate::programVariable() const +{ + return dynamic_cast(m_node); +} + optional> Predicate::stateVariables() const { if (m_contractContext) @@ -214,6 +219,9 @@ string Predicate::formatSummaryCall( { solAssert(isSummary(), ""); + if (programVariable()) + return {}; + if (auto funCall = programFunctionCall()) { if (funCall->location().hasText()) @@ -348,6 +356,8 @@ vector> Predicate::summaryStateValues(vector(stateVars->size()); stateLast = stateFirst + static_cast(stateVars->size()); } + else if (programVariable()) + return {}; else solAssert(false, ""); diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 16af42f45..d7ac0da35 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -115,6 +115,10 @@ public: /// or nullptr otherwise. FunctionCall const* programFunctionCall() const; + /// @returns the VariableDeclaration that this predicate represents + /// or nullptr otherwise. + VariableDeclaration const* programVariable() const; + /// @returns the program state variables in the scope of this predicate. std::optional> stateVariables() const; diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index aff6aa19b..5e057efe3 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -70,14 +70,14 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context)); } -smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context) +smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal) { auto const& contract = dynamic_cast(*_pred.programNode()); if (auto const* constructor = contract.constructor()) - return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context)); + return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; + vector stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; state.newState(); stateExprs += vector{state.state()}; stateExprs += currentStateVariables(contract, _context); @@ -166,11 +166,12 @@ vector currentFunctionVariablesForDefinition( vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, - EncodingContext& _context + EncodingContext& _context, + bool _internal ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; + vector exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h index 2f6c77381..42a9e2040 100644 --- a/libsolidity/formal/PredicateInstance.h +++ b/libsolidity/formal/PredicateInstance.h @@ -37,7 +37,14 @@ smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx); smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context); -smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context); +/// The encoding of the deployment procedure includes adding constraints +/// for base constructors if inheritance is used. +/// From the predicate point of view this is not different, +/// but some of the arguments are different. +/// @param _internal = true means that this constructor call is used in the +/// deployment procedure, whereas false means it is used in the deployment +/// of a contract. +smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal = true); smtutil::Expression function( Predicate const& _pred, @@ -77,7 +84,8 @@ std::vector currentFunctionVariablesForDefinition( std::vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, - EncodingContext& _context + EncodingContext& _context, + bool _internal = true ); std::vector currentBlockVariables( diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 810b53351..c3286fa04 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -637,7 +637,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) visitGasLeft(_funCall); break; case FunctionType::Kind::External: - if (isPublicGetter(_funCall.expression())) + if (publicGetter(_funCall.expression())) visitPublicGetter(_funCall); break; case FunctionType::Kind::ABIDecode: @@ -696,10 +696,18 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::ObjectCreation: visitObjectCreation(_funCall); return; + case FunctionType::Kind::Creation: + if (!m_settings.engine.chc || !m_settings.externalCalls.isTrusted()) + m_errorReporter.warning( + 8729_error, + _funCall.location(), + "Contract deployment is only supported in the trusted mode for external calls" + " with the CHC engine." + ); + break; case FunctionType::Kind::DelegateCall: case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: - case FunctionType::Kind::Creation: default: m_errorReporter.warning( 4588_error, @@ -978,9 +986,8 @@ vector structGetterReturnedMembers(StructType const& _structType) void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) { - MemberAccess const& access = dynamic_cast(_funCall.expression()); - auto var = dynamic_cast(access.annotation().referencedDeclaration); - solAssert(var, ""); + auto var = publicGetter(_funCall.expression()); + solAssert(var && var->isStateVariable(), ""); solAssert(m_context.knownExpression(_funCall), ""); auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes()); auto actualArguments = _funCall.arguments(); @@ -1054,7 +1061,7 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const return false; return m_settings.contracts.isDefault() || - m_settings.contracts.has(_contract.sourceUnitName(), _contract.name()); + m_settings.contracts.has(_contract.sourceUnitName()); } void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) @@ -2789,16 +2796,24 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const return nullptr; } -bool SMTEncoder::isPublicGetter(Expression const& _expr) { - if (!isTrustedExternalCall(&_expr)) - return false; - auto varDecl = dynamic_cast( - dynamic_cast(_expr).annotation().referencedDeclaration - ); - return varDecl != nullptr; +smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f) +{ + FunctionType const& funType = dynamic_cast(*_f.expression().annotation().type); + if (funType.kind() == FunctionType::Kind::Internal) + return state().thisAddress(); + auto [funExpr, funOptions] = functionCallExpression(_f); + if (MemberAccess const* callBase = dynamic_cast(funExpr)) + return expr(callBase->expression()); + solAssert(false, "Unreachable!"); } -bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) { +VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const { + if (auto memberAccess = dynamic_cast(&_expr)) + return dynamic_cast(memberAccess->annotation().referencedDeclaration); + return nullptr; +} + +bool SMTEncoder::isExternalCallToThis(Expression const* _expr) { auto memberAccess = dynamic_cast(_expr); if (!memberAccess) return false; @@ -3060,7 +3075,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr) return nullptr; } -set SMTEncoder::collectABICalls(ASTNode const* _node) +set> SMTEncoder::collectABICalls(ASTNode const* _node) { struct ABIFunctions: public ASTConstVisitor { @@ -3082,7 +3097,7 @@ set SMTEncoder::collectABICalls(ASTNode const* _node) } } - set abiCalls; + set> abiCalls; }; return ABIFunctions(_node).abiCalls; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 2ba491a0b..06b03a7eb 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -123,7 +123,7 @@ public: /// RationalNumberType or can be const evaluated, and nullptr otherwise. static RationalNumberType const* isConstant(Expression const& _expr); - static std::set collectABICalls(ASTNode const* _node); + static std::set> collectABICalls(ASTNode const* _node); /// @returns all the sources that @param _source depends on, /// including itself. @@ -219,7 +219,7 @@ protected: void visitTypeConversion(FunctionCall const& _funCall); void visitStructConstructorCall(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); - void visitPublicGetter(FunctionCall const& _funCall); + virtual void visitPublicGetter(FunctionCall const& _funCall); /// @returns true if @param _contract is set for analysis in the settings /// and it is not abstract. @@ -227,7 +227,12 @@ protected: /// @returns true if @param _source is set for analysis in the settings. bool shouldAnalyze(SourceUnit const& _source) const; - bool isPublicGetter(Expression const& _expr); + /// @returns the state variable returned by a public getter if + /// @a _expr is a call to a public getter, + /// otherwise nullptr. + VariableDeclaration const* publicGetter(Expression const& _expr) const; + + smtutil::Expression contractAddressValue(FunctionCall const& _f); /// Encodes a modifier or function body according to the modifier /// visit depth. @@ -392,9 +397,9 @@ protected: /// otherwise nullptr. MemberAccess const* isEmptyPush(Expression const& _expr) const; - /// @returns true if the given identifier is a contract which is known and trusted. + /// @returns true if the given expression is `this`. /// This means we don't have to abstract away effects of external function calls to this contract. - static bool isTrustedExternalCall(Expression const* _expr); + static bool isExternalCallToThis(Expression const* _expr); /// Creates symbolic expressions for the returned values /// and set them as the components of the symbolic tuple. diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 3afde0dcf..68bd9b646 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -22,8 +22,13 @@ #include #include +#include + +#include + using namespace std; using namespace solidity; +using namespace solidity::util; using namespace solidity::smtutil; using namespace solidity::frontend::smt; @@ -58,16 +63,8 @@ smtutil::Expression BlockchainVariable::member(string const& _member) const smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value) { - vector args; - for (auto const& m: m_members) - if (m.first == _member) - args.emplace_back(_value); - else - args.emplace_back(member(m.first)); - m_tuple->increaseIndex(); - auto tuple = m_tuple->currentValue(); - auto sortExpr = smtutil::Expression(make_shared(tuple.sort), tuple.name); - m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args)); + smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}}); + m_context.addAssertion(m_tuple->increaseIndex() == newTuple); return m_tuple->currentValue(); } @@ -75,16 +72,19 @@ void SymbolicState::reset() { m_error.resetIndex(); m_thisAddress.resetIndex(); - m_state.reset(); m_tx.reset(); m_crypto.reset(); if (m_abi) m_abi->reset(); + /// We don't reset nor clear these pointers on purpose, + /// since it only helps to keep the already generated types. + if (m_state) + m_state->reset(); } smtutil::Expression SymbolicState::balances() const { - return m_state.member("balances"); + return m_state->member("balances"); } smtutil::Expression SymbolicState::balance() const @@ -107,24 +107,94 @@ void SymbolicState::newBalances() auto tupleSort = dynamic_pointer_cast(stateSort()); auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances")); SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context); - m_state.assignMember("balances", newBalances.currentValue()); + m_state->assignMember("balances", newBalances.currentValue()); } void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { - unsigned indexBefore = m_state.index(); + unsigned indexBefore = m_state->index(); addBalance(_from, 0 - _value); addBalance(_to, std::move(_value)); - unsigned indexAfter = m_state.index(); + unsigned indexAfter = m_state->index(); solAssert(indexAfter > indexBefore, ""); - m_state.newVar(); + m_state->newVar(); /// Do not apply the transfer operation if _from == _to. auto newState = smtutil::Expression::ite( std::move(_from) == std::move(_to), - m_state.value(indexBefore), - m_state.value(indexAfter) + m_state->value(indexBefore), + m_state->value(indexAfter) ); - m_context.addAssertion(m_state.value() == newState); + m_context.addAssertion(m_state->value() == newState); +} + +smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract) const +{ + return smt::member(m_state->member("storage"), contractStorageKey(_contract)); +} + +smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract, smtutil::Expression _address) const +{ + return smtutil::Expression::select(storage(_contract), std::move(_address)); +} + +smtutil::Expression SymbolicState::addressActive(smtutil::Expression _address) const +{ + return smtutil::Expression::select(m_state->member("isActive"), std::move(_address)); +} + +void SymbolicState::setAddressActive( + smtutil::Expression _address, + bool _active +) +{ + m_state->assignMember("isActive", smtutil::Expression::store( + m_state->member("isActive"), + std::move(_address), + smtutil::Expression(_active)) + ); +} + +void SymbolicState::newStorage() +{ + auto newStorageVar = SymbolicTupleVariable( + m_state->member("storage").sort, + "havoc_storage_" + to_string(m_context.newUniqueId()), + m_context + ); + m_state->assignMember("storage", newStorageVar.currentValue()); +} + +void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address) +{ + auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); + if (stateVars.empty()) + return; + + map values; + for (auto var: stateVars) + values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue()); + + smtutil::Expression thisStorage = storage(_contract, _address); + smtutil::Expression newStorage = smt::assignMember(thisStorage, values); + auto newContractStorage = smtutil::Expression::store( + storage(_contract), std::move(_address), newStorage + ); + smtutil::Expression newAllStorage = smt::assignMember(m_state->member("storage"), {{contractStorageKey(_contract), newContractStorage}}); + m_state->assignMember("storage", newAllStorage); +} + +void SymbolicState::readStateVars(ContractDefinition const& _contract, smtutil::Expression _address) +{ + auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); + if (stateVars.empty()) + return; + + auto contractStorage = storage(_contract, std::move(_address)); + for (auto var: stateVars) + m_context.addAssertion( + m_context.variable(*var)->increaseIndex() == + smt::member(contractStorage, stateVarStorageKey(*var, _contract)) + ); } void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) @@ -134,7 +204,7 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _address, balance(_address) + std::move(_value) ); - m_state.assignMember("balances", newBalances); + m_state->assignMember("balances", newBalances); } smtutil::Expression SymbolicState::txMember(string const& _member) const @@ -194,17 +264,99 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons return conj; } -void SymbolicState::prepareForSourceUnit(SourceUnit const& _source) +void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storage) { - set abiCalls = SMTEncoder::collectABICalls(&_source); - for (auto const& source: _source.referencedSourceUnits(true)) + auto allSources = _source.referencedSourceUnits(true); + allSources.insert(&_source); + set> abiCalls; + set> contracts; + for (auto const& source: allSources) + { abiCalls += SMTEncoder::collectABICalls(source); + for (auto node: source->nodes()) + if (auto contract = dynamic_cast(node.get())) + contracts.insert(contract); + } + buildState(contracts, _storage); buildABIFunctions(abiCalls); } /// Private helpers. -void SymbolicState::buildABIFunctions(set const& _abiFunctions) +string SymbolicState::contractSuffix(ContractDefinition const& _contract) const +{ + return "_" + _contract.name() + "_" + to_string(_contract.id()); +} + +string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const +{ + return "storage" + contractSuffix(_contract); +} + +string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const +{ + return _var.name() + "_" + to_string(_var.id()) + contractSuffix(_contract); +} + +void SymbolicState::buildState(set> const& _contracts, bool _allStorages) +{ + map stateMembers{ + {"balances", make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)} + }; + + if (_allStorages) + { + vector memberNames; + vector memberSorts; + for (auto contract: _contracts) + { + string suffix = contractSuffix(*contract); + + // z3 doesn't like empty tuples, so if the contract has 0 + // state vars we can't put it there. + auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract); + if (stateVars.empty()) + continue; + + auto names = applyMap(stateVars, [&](auto var) { + return var->name() + "_" + to_string(var->id()) + suffix; + }); + auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); }); + + string name = "storage" + suffix; + auto storageTuple = make_shared( + name + "_type", names, sorts + ); + + auto storageSort = make_shared( + smtSort(*TypeProvider::address()), + storageTuple + ); + + memberNames.emplace_back(name); + memberSorts.emplace_back(storageSort); + } + + stateMembers.emplace( + "isActive", + make_shared(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort) + ); + stateMembers.emplace( + "storage", + make_shared( + "storage_type", memberNames, memberSorts + ) + ); + } + + m_state = make_unique( + "state", + std::move(stateMembers), + m_context + ); +} + +void SymbolicState::buildABIFunctions(set> const& _abiFunctions) { map functions; diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 45c129c1b..7fe5b028d 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -62,7 +62,8 @@ private: * - this (the address of the currently executing contract) * - state, represented as a tuple of: * - balances - * - TODO: potentially storage of contracts + * - array of address => bool representing whether an address is used by a contract + * - storage of contracts * - block and transaction properties, represented as a tuple of: * - blockhash * - block basefee @@ -99,29 +100,41 @@ public: /// @returns the symbolic value of the currently executing contract's address. smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); } smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); } + smtutil::Expression newThisAddress() { return m_thisAddress.increaseIndex(); } smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); } //@} /// Blockchain state. //@{ - smtutil::Expression state() const { return m_state.value(); } - smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); } - smtutil::SortPointer const& stateSort() const { return m_state.sort(); } - void newState() { m_state.newVar(); } + smtutil::Expression state() const { solAssert(m_state, ""); return m_state->value(); } + smtutil::Expression state(unsigned _idx) const { solAssert(m_state, ""); return m_state->value(_idx); } + smtutil::SortPointer const& stateSort() const { solAssert(m_state, ""); return m_state->sort(); } + void newState() { solAssert(m_state, ""); m_state->newVar(); } void newBalances(); + + /// Balance. /// @returns the symbolic balances. smtutil::Expression balances() const; /// @returns the symbolic balance of address `this`. smtutil::Expression balance() const; /// @returns the symbolic balance of an address. smtutil::Expression balance(smtutil::Expression _address) const; - /// Transfer _value from _from to _to. void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); /// Adds _value to _account's balance. void addBalance(smtutil::Expression _account, smtutil::Expression _value); + + /// Storage. + smtutil::Expression storage(ContractDefinition const& _contract) const; + smtutil::Expression storage(ContractDefinition const& _contract, smtutil::Expression _address) const; + smtutil::Expression addressActive(smtutil::Expression _address) const; + void setAddressActive(smtutil::Expression _address, bool _active); + + void newStorage(); + void writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address); + void readStateVars(ContractDefinition const& _contract, smtutil::Expression _address); //@} /// Transaction data. @@ -149,11 +162,15 @@ public: smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); } //@} + /// Calls the internal methods that build + /// - the symbolic ABI functions based on the abi.* calls + /// in _source and referenced sources. + /// - the symbolic storages for all contracts in _source and + /// referenced sources. + void prepareForSourceUnit(SourceUnit const& _source, bool _storage); + /// ABI functions. //@{ - /// Calls the internal methods that build the symbolic ABI functions - /// based on the abi.* calls in _source and referenced sources. - void prepareForSourceUnit(SourceUnit const& _source); smtutil::Expression abiFunction(FunctionCall const* _funCall); using SymbolicABIFunction = std::tuple< std::string, @@ -169,8 +186,15 @@ public: //@} private: + std::string contractSuffix(ContractDefinition const& _contract) const; + std::string contractStorageKey(ContractDefinition const& _contract) const; + std::string stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const; + + /// Builds state.storage based on _contracts. + void buildState(std::set> const& _contracts, bool _allStorages); + /// Builds m_abi based on the abi.* calls _abiFunctions. - void buildABIFunctions(std::set const& _abiFunctions); + void buildABIFunctions(std::set> const& _abiFunctions); EncodingContext& m_context; @@ -186,11 +210,14 @@ private: m_context }; - BlockchainVariable m_state{ - "state", - {{"balances", std::make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}}, - m_context - }; + /// m_state is a tuple of + /// - balances: array of address to balance of address. + /// - isActive: array of address to Boolean, where element is true iff address is used. + /// - storage: tuple containing the storage of every contract, where + /// each element of the tuple represents a contract, + /// and is defined by an array where the index is the contract's address + /// and the element is a tuple containing the state variables of that contract. + std::unique_ptr m_state; BlockchainVariable m_tx{ "tx", diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index d40b51cea..ccabebcc3 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -618,4 +618,26 @@ optional symbolicTypeConversion(frontend::Type const* _from return std::nullopt; } +smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member) +{ + TupleSort const& _sort = dynamic_cast(*_tuple.sort); + return smtutil::Expression::tuple_get( + _tuple, + _sort.memberToIndex.at(_member) + ); +} + +smtutil::Expression assignMember(smtutil::Expression const _tuple, map const& _values) +{ + TupleSort const& _sort = dynamic_cast(*_tuple.sort); + vector args; + for (auto const& m: _sort.members) + if (auto* value = util::valueOrNullptr(_values, m)) + args.emplace_back(*value); + else + args.emplace_back(member(_tuple, m)); + auto sortExpr = smtutil::Expression(make_shared(_tuple.sort), _tuple.name); + return smtutil::Expression::tuple_constructor(sortExpr, args); +} + } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 312e8581a..747e27b7e 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -82,4 +82,8 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _t smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type); std::optional symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to); + +smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member); +smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map const& _values); + } diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 27fa1c989..b08e8fbf6 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -445,7 +445,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"}; + static set keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showUnproved", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -1016,6 +1016,16 @@ std::variant StandardCompiler: ret.modelCheckerSettings.engine = *engine; } + if (modelCheckerSettings.isMember("extCalls")) + { + if (!modelCheckerSettings["extCalls"].isString()) + return formatFatalError(Error::Type::JSONError, "settings.modelChecker.extCalls must be a string."); + std::optional extCalls = ModelCheckerExtCalls::fromString(modelCheckerSettings["extCalls"].asString()); + if (!extCalls) + return formatFatalError(Error::Type::JSONError, "Invalid model checker extCalls requested."); + ret.modelCheckerSettings.externalCalls = *extCalls; + } + if (modelCheckerSettings.isMember("invariants")) { auto const& invariantsArray = modelCheckerSettings["invariants"]; diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 37ceca1d4..eb03831be 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -69,6 +69,7 @@ static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strModelCheckerContracts = "model-checker-contracts"; static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks"; static string const g_strModelCheckerEngine = "model-checker-engine"; +static string const g_strModelCheckerExtCalls = "model-checker-ext-calls"; static string const g_strModelCheckerInvariants = "model-checker-invariants"; static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved"; static string const g_strModelCheckerSolvers = "model-checker-solvers"; @@ -831,6 +832,12 @@ General Information)").c_str(), po::value()->value_name("all,bmc,chc,none")->default_value("none"), "Select model checker engine." ) + ( + g_strModelCheckerExtCalls.c_str(), + po::value()->value_name("untrusted,trusted")->default_value("untrusted"), + "Select whether to assume (trusted) that external calls always invoke" + " the code given by the type of the contract, if that code is available." + ) ( g_strModelCheckerInvariants.c_str(), po::value()->value_name("default,all,contract,reentrancy")->default_value("default"), @@ -1289,6 +1296,15 @@ void CommandLineParser::processArgs() m_options.modelChecker.settings.engine = *engine; } + if (m_args.count(g_strModelCheckerExtCalls)) + { + string mode = m_args[g_strModelCheckerExtCalls].as(); + optional extCallsMode = ModelCheckerExtCalls::fromString(mode); + if (!extCallsMode) + solThrow(CommandLineValidationError, "Invalid option for --" + g_strModelCheckerExtCalls + ": " + mode); + m_options.modelChecker.settings.externalCalls = *extCallsMode; + } + if (m_args.count(g_strModelCheckerInvariants)) { string invsStr = m_args[g_strModelCheckerInvariants].as(); @@ -1327,6 +1343,7 @@ void CommandLineParser::processArgs() m_args.count(g_strModelCheckerContracts) || m_args.count(g_strModelCheckerDivModNoSlacks) || m_args.count(g_strModelCheckerEngine) || + m_args.count(g_strModelCheckerExtCalls) || m_args.count(g_strModelCheckerInvariants) || m_args.count(g_strModelCheckerShowUnproved) || m_args.count(g_strModelCheckerSolvers) || diff --git a/test/cmdlineTests/model_checker_contracts_inexistent_contract/err b/test/cmdlineTests/model_checker_contracts_inexistent_contract/err index 6326537e9..00b97763f 100644 --- a/test/cmdlineTests/model_checker_contracts_inexistent_contract/err +++ b/test/cmdlineTests/model_checker_contracts_inexistent_contract/err @@ -1 +1,27 @@ Warning: Requested contract "C" does not exist in source "model_checker_contracts_inexistent_contract/input.sol". + +Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +B.constructor() +B.f(0) + --> model_checker_contracts_inexistent_contract/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ + +Warning: CHC: Assertion violation happens here. +Counterexample: + +y = 0 + +Transaction trace: +A.constructor() +A.g(0) + --> model_checker_contracts_inexistent_contract/input.sol:10:3: + | +10 | assert(y > 0); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_contracts_only_one/err b/test/cmdlineTests/model_checker_contracts_only_one/err index 9c8ade693..2088e19c7 100644 --- a/test/cmdlineTests/model_checker_contracts_only_one/err +++ b/test/cmdlineTests/model_checker_contracts_only_one/err @@ -4,7 +4,7 @@ Counterexample: x = 0 Transaction trace: -A.constructor() +B.constructor() B.f(0) --> model_checker_contracts_only_one/input.sol:5:3: | diff --git a/test/cmdlineTests/model_checker_ext_calls_empty_arg/args b/test/cmdlineTests/model_checker_ext_calls_empty_arg/args new file mode 100644 index 000000000..b0c065ef7 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_empty_arg/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-ext-calls diff --git a/test/cmdlineTests/model_checker_ext_calls_empty_arg/err b/test/cmdlineTests/model_checker_ext_calls_empty_arg/err new file mode 100644 index 000000000..7d7481c80 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_empty_arg/err @@ -0,0 +1 @@ +No input files given. If you wish to use the standard input please specify "-" explicitly. diff --git a/test/cmdlineTests/model_checker_ext_calls_empty_arg/exit b/test/cmdlineTests/model_checker_ext_calls_empty_arg/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_empty_arg/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_ext_calls_empty_arg/input.sol b/test/cmdlineTests/model_checker_ext_calls_empty_arg/input.sol new file mode 100644 index 000000000..bd341cea6 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_empty_arg/input.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + +contract Ext { + function f() public view returns (uint) { + return 42; + } +} + +contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_ext_calls_trusted_chc/args b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/args new file mode 100644 index 000000000..a6240ee19 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-ext-calls trusted diff --git a/test/cmdlineTests/model_checker_ext_calls_trusted_chc/err b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/err new file mode 100644 index 000000000..a07e1575d --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/err @@ -0,0 +1,5 @@ +Warning: Function state mutability can be restricted to pure + --> model_checker_ext_calls_trusted_chc/input.sol:5:2: + | +5 | function f() public view returns (uint) { + | ^ (Relevant source part starts here and spans across multiple lines). diff --git a/test/cmdlineTests/model_checker_ext_calls_trusted_chc/input.sol b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/input.sol new file mode 100644 index 000000000..bd341cea6 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_trusted_chc/input.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + +contract Ext { + function f() public view returns (uint) { + return 42; + } +} + +contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/args b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/args new file mode 100644 index 000000000..e249f0250 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-ext-calls untrusted diff --git a/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err new file mode 100644 index 000000000..b06333e43 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err @@ -0,0 +1,14 @@ +Warning: CHC: Assertion violation happens here. +Counterexample: + +e = 0 +x = 1 + +Transaction trace: +test.constructor() +test.g(0) + e.f() -- untrusted external call + --> model_checker_ext_calls_untrusted_chc/input.sol:11:3: + | +11 | assert(x == 0); + | ^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/input.sol b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/input.sol new file mode 100644 index 000000000..0d28d1c18 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_untrusted_chc/input.sol @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + +abstract contract Ext { + function f() virtual public view returns (uint); +} + +contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_ext_calls_wrong_arg/args b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/args new file mode 100644 index 000000000..478aa5e1d --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-ext-calls what diff --git a/test/cmdlineTests/model_checker_ext_calls_wrong_arg/err b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/err new file mode 100644 index 000000000..746a0b525 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/err @@ -0,0 +1 @@ +Invalid option for --model-checker-ext-calls: what diff --git a/test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_ext_calls_wrong_arg/input.sol b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/input.sol new file mode 100644 index 000000000..bd341cea6 --- /dev/null +++ b/test/cmdlineTests/model_checker_ext_calls_wrong_arg/input.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + +contract Ext { + function f() public view returns (uint) { + return 42; + } +} + +contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json b/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json index e3714e8e6..7ff30950c 100644 --- a/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json +++ b/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json @@ -10,6 +10,74 @@ "message": "Requested contract \"C\" does not exist in source \"Source\".", "severity": "warning", "type": "Warning" + }, + { + "component": "general", + "errorCode": "6328", + "formattedMessage": "Warning: CHC: Assertion violation happens here. +Counterexample: + +y = 0 + +Transaction trace: +B.constructor() +B.g(0) + --> Source:5:7: + | +5 | \t\t\t\t\t\tassert(y > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^ + +", + "message": "CHC: Assertion violation happens here. +Counterexample: + +y = 0 + +Transaction trace: +B.constructor() +B.g(0)", + "severity": "warning", + "sourceLocation": + { + "end": 137, + "file": "Source", + "start": 124 + }, + "type": "Warning" + }, + { + "component": "general", + "errorCode": "6328", + "formattedMessage": "Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +A.constructor() +A.f(0) + --> Source:10:7: + | +10 | \t\t\t\t\t\tassert(x > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^ + +", + "message": "CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +A.constructor() +A.f(0)", + "severity": "warning", + "sourceLocation": + { + "end": 231, + "file": "Source", + "start": 218 + }, + "type": "Warning" } ], "sources": diff --git a/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json b/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json index a87566581..cb18875e1 100644 --- a/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json +++ b/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json @@ -10,7 +10,7 @@ Counterexample: y = 0 Transaction trace: -A.constructor() +B.constructor() B.g(0) --> Source:5:7: | @@ -24,7 +24,7 @@ Counterexample: y = 0 Transaction trace: -A.constructor() +B.constructor() B.g(0)", "severity": "warning", "sourceLocation": diff --git a/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json b/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json index 57c4f10fa..b4bfd66b8 100644 --- a/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json +++ b/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json @@ -10,7 +10,7 @@ Counterexample: y = 0 Transaction trace: -A.constructor() +B.constructor() B.g(0) --> Source:5:7: | @@ -24,7 +24,7 @@ Counterexample: y = 0 Transaction trace: -A.constructor() +B.constructor() B.g(0)", "severity": "warning", "sourceLocation": diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/input.json b/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/input.json new file mode 100644 index 000000000..073516ddb --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/input.json @@ -0,0 +1,30 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0; + contract Ext { + function f() public view returns (uint) { + return 42; + } + } + + contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "extCalls": "" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/output.json b/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/output.json new file mode 100644 index 000000000..4e214a37b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_empty_arg/output.json @@ -0,0 +1,12 @@ +{ + "errors": + [ + { + "component": "general", + "formattedMessage": "Invalid model checker extCalls requested.", + "message": "Invalid model checker extCalls requested.", + "severity": "error", + "type": "JSONError" + } + ] +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/input.json b/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/input.json new file mode 100644 index 000000000..a03b77f2b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/input.json @@ -0,0 +1,30 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0; + contract Ext { + function f() public view returns (uint) { + return 42; + } + } + + contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "extCalls": "trusted" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/output.json b/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/output.json new file mode 100644 index 000000000..93d73d1c4 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_trusted_chc/output.json @@ -0,0 +1,32 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "2018", + "formattedMessage": "Warning: Function state mutability can be restricted to pure + --> A:4:7: + | +4 | \t\t\t\t\t\tfunction f() public view returns (uint) { + | \t\t\t\t\t\t^ (Relevant source part starts here and spans across multiple lines). + +", + "message": "Function state mutability can be restricted to pure", + "severity": "warning", + "sourceLocation": + { + "end": 152, + "file": "A", + "start": 85 + }, + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/input.json b/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/input.json new file mode 100644 index 000000000..9fadd08fa --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/input.json @@ -0,0 +1,28 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0; + abstract contract Ext { + function f() virtual public view returns (uint); + } + + contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "extCalls": "untrusted" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/output.json b/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/output.json new file mode 100644 index 000000000..c6b072a85 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_untrusted_chc/output.json @@ -0,0 +1,50 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "6328", + "formattedMessage": "Warning: CHC: Assertion violation happens here. +Counterexample: + +e = 0 +x = 1 + +Transaction trace: +test.constructor() +test.g(0) + e.f() -- untrusted external call + --> A:10:8: + | +10 | \t\t\t\t\t\t\tassert(x == 0); + | \t\t\t\t\t\t\t^^^^^^^^^^^^^^ + +", + "message": "CHC: Assertion violation happens here. +Counterexample: + +e = 0 +x = 1 + +Transaction trace: +test.constructor() +test.g(0) + e.f() -- untrusted external call", + "severity": "warning", + "sourceLocation": + { + "end": 254, + "file": "A", + "start": 240 + }, + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/input.json b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/input.json new file mode 100644 index 000000000..15113c5ad --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/input.json @@ -0,0 +1,30 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0; + contract Ext { + function f() public view returns (uint) { + return 42; + } + } + + contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "extCalls": "what" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/output.json b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/output.json new file mode 100644 index 000000000..4e214a37b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_1/output.json @@ -0,0 +1,12 @@ +{ + "errors": + [ + { + "component": "general", + "formattedMessage": "Invalid model checker extCalls requested.", + "message": "Invalid model checker extCalls requested.", + "severity": "error", + "type": "JSONError" + } + ] +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/input.json b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/input.json new file mode 100644 index 000000000..cda245e7f --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/input.json @@ -0,0 +1,30 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0; + contract Ext { + function f() public view returns (uint) { + return 42; + } + } + + contract test { + function g(Ext e) public view { + uint x = e.f(); + assert(x == 42); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "extCalls": 2 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/output.json b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/output.json new file mode 100644 index 000000000..e869637ed --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_ext_calls_wrong_arg_2/output.json @@ -0,0 +1,12 @@ +{ + "errors": + [ + { + "component": "general", + "formattedMessage": "settings.modelChecker.extCalls must be a string.", + "message": "settings.modelChecker.extCalls must be a string.", + "severity": "error", + "type": "JSONError" + } + ] +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json index fa8726d55..85a221d4c 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json +++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json @@ -3,14 +3,41 @@ { "smtlib2queries": { - "0x0ebc730de380833af1e52ed063befb32994bc637929c942b7fd089b7cd3ba64e": "(set-logic HORN) - + "0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true) +(set-logic ALL) +(declare-fun |x_3_3| () Int) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-fun |x_3_4| () Int) +(declare-fun |x_3_0| () Int) +(declare-fun |expr_7_0| () Int) +(declare-fun |expr_8_0| () Int) +(declare-fun |expr_9_1| () Bool) + +(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_3_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +", + "0xfb06d3f02a20bd362abded9ab80638bdc9dd43ccbf644517f3006206c0c47f67": "(set-logic HORN) + (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) (declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) (declare-fun |interface_0_C_14_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) (declare-fun |nondet_interface_1_C_14_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) (declare-fun |summary_constructor_2_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) @@ -97,7 +124,7 @@ (declare-fun |implicit_constructor_entry_13_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) (assert (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) +(=> (and (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) (assert @@ -124,34 +151,7 @@ (assert (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) (=> error_target_3_0 false))) -(check-sat)", - "0xcb822e6220a39244d26887a0fa6f62b06718359056555679fb06dd7dff18bb86": "(set-option :produce-models true) -(set-logic ALL) -(declare-fun |x_3_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-fun |x_3_4| () Int) -(declare-fun |x_3_0| () Int) -(declare-fun |expr_7_0| () Int) -(declare-fun |expr_8_0| () Int) -(declare-fun |expr_9_1| () Bool) - -(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_3_0)) -(check-sat) -(get-value (|EVALEXPR_0| )) -" +(check-sat)" } }, "errors": diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index e3e52491d..93590994a 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -33,6 +33,12 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E if (!contract.empty()) m_modelCheckerSettings.contracts.contracts[""] = {contract}; + auto extCallsMode = ModelCheckerExtCalls::fromString(m_reader.stringSetting("SMTExtCalls", "untrusted")); + if (extCallsMode) + m_modelCheckerSettings.externalCalls = *extCallsMode; + else + BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT external calls mode.")); + auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes"); if (showUnproved == "no") m_modelCheckerSettings.showUnproved = false; @@ -51,8 +57,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E m_modelCheckerSettings.solvers &= ModelChecker::availableSolvers(); /// Underflow and Overflow are not enabled by default for Solidity >=0.8.7, - /// so we explicitly enable all targets for the tests. - m_modelCheckerSettings.targets = ModelCheckerTargets::All(); + /// so we explicitly enable all targets for the tests, + /// if the targets were not explicitly set by the test. + auto targets = ModelCheckerTargets::fromString(m_reader.stringSetting("SMTTargets", "all")); + if (targets) + m_modelCheckerSettings.targets = *targets; + else + BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT targets.")); auto engine = ModelCheckerEngine::fromString(m_reader.stringSetting("SMTEngine", "all")); if (engine) diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol index ddda215df..7950c8612 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol @@ -22,4 +22,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n +// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0) && ((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol index 7a7db383b..7af3af40d 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol @@ -31,4 +31,4 @@ contract C { // Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() // Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() // Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() -// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n +// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol index 0d16306b7..aea10a376 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol @@ -18,5 +18,6 @@ contract C { // ==== // SMTEngine: all // SMTIgnoreOS: macos +// SMTIgnoreCex: yes // ---- // Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol index bbd5589a4..34b439e3a 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol @@ -20,5 +20,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- // Warning 6328: (362-420): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 3f5096a3b..936ad1703 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,6 +83,6 @@ contract InternalCall { // Warning 2018: (1111-1173): Function state mutability can be restricted to pure // Warning 2018: (1179-1241): Function state mutability can be restricted to pure // Warning 2018: (1247-1309): Function state mutability can be restricted to pure -// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call. -// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call. +// Warning 8729: (681-716): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (854-886): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. // Warning 5729: (1370-1375): BMC does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol new file mode 100644 index 000000000..81ddc515e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol @@ -0,0 +1,18 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in BMC + } +} +// ==== +// SMTEngine: bmc +// SMTExtCalls: trusted +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 4661: (153-167): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol new file mode 100644 index 000000000..f69a8d6c7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol @@ -0,0 +1,17 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 4661: (153-167): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol new file mode 100644 index 000000000..388b0b0db --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol @@ -0,0 +1,16 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should hold in ext calls trusted mode + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol new file mode 100644 index 000000000..cf43dbda2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol @@ -0,0 +1,19 @@ +contract D { + uint x; +} + +contract C { + function f() public { + D d1 = new D(); + D d2 = new D(); + + assert(d1 != d2); // should hold in ext calls trusted mode + assert(address(this) != address(d1)); // should hold in ext calls trusted mode + assert(address(this) != address(d2)); // should hold in ext calls trusted mode + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n(:var 0).isActive[address(this)]\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol new file mode 100644 index 000000000..ddd4b41e6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -0,0 +1,32 @@ +contract D { + uint x; + function inc() public { ++x; } + function f() public view returns (uint) { return x; } +} + +contract C { + function f() public { + D d = new D(); + assert(d.f() == 0); // should hold + d.inc(); + assert(d.f() == 1); // should hold + d = new D(); + assert(d.f() == 0); // should hold + assert(d.f() == 1); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 6328: (167-185): CHC: Assertion violation might happen here. +// Warning 6328: (215-233): CHC: Assertion violation might happen here. +// Warning 6328: (267-285): CHC: Assertion violation might happen here. +// Warning 6328: (304-322): CHC: Assertion violation might happen here. +// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (167-185): BMC: Assertion violation happens here. +// Warning 4661: (215-233): BMC: Assertion violation happens here. +// Warning 4661: (267-285): BMC: Assertion violation happens here. +// Warning 4661: (304-322): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol new file mode 100644 index 000000000..b2aa7ac98 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol @@ -0,0 +1,17 @@ +contract D { + uint x; +} + +contract C { + uint y; + function g() public { + D d = new D(); + assert(y == 0); // should hold + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 2072: (72-75): Unused local variable. +// Info 1180: Contract invariant(s) for :C:\n(y <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol new file mode 100644 index 000000000..4b3367b11 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol @@ -0,0 +1,24 @@ +contract D { + uint x; + function inc() public { ++x; } + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + assert(d.f() == 0); // should hold + } + function g() public view { + assert(d.f() == 0); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 6328: (233-251): CHC: Assertion violation happens here. +// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol new file mode 100644 index 000000000..66684df8c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol @@ -0,0 +1,20 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + assert(d.f() == 0); // should hold + } + function g() public view { + assert(d.f() == 0); // should hold + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((:var 1).storage.storage_D_12[d].x_3_D_12 <= 0)\nReentrancy property(ies) for :D:\n((x' <= 0) || !(x <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol new file mode 100644 index 000000000..260909b87 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol @@ -0,0 +1,21 @@ +contract D { + uint x; + function s(uint _x) public { x = _x; } + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + } + function g() public view { + assert(d.f() == 0); // should fail + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (204-222): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol new file mode 100644 index 000000000..5bd27c3b8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol @@ -0,0 +1,20 @@ +contract D { + bool b; + function s() public { b = true; } + function f() public view returns (bool) { return b; } +} + +contract C { + D d; + constructor() { + d = new D(); + } + function g() public view { + assert(d.f()); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = (- 1)\n\nTransaction trace:\nC.constructor()\nState: d = (- 1)\nC.g()\n D.f() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol new file mode 100644 index 000000000..a28d46210 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol @@ -0,0 +1,17 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (153-167): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.g()\n d.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol new file mode 100644 index 000000000..c934e152b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol @@ -0,0 +1,22 @@ +contract D { + uint x; +} + +contract C { + function f() public { + D d1 = new D(); + D d2 = new D(); + + assert(d1 != d2); // should fail in ext calls untrusted mode + assert(address(this) != address(d1)); // should fail in ext calls untrusted mode + assert(address(this) != address(d2)); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 8729: (70-77): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (88-95): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (100-116): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 0\nd2 = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (163-199): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (246-282): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol new file mode 100644 index 000000000..be18b33f6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol @@ -0,0 +1,17 @@ +contract D { + uint x; +} + +contract C { + uint y; + function g() public { + D d = new D(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2072: (72-75): Unused local variable. +// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (89-103): CHC: Assertion violation happens here.\nCounterexample:\ny = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: y = 0\nC.g() diff --git a/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol b/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol new file mode 100644 index 000000000..92195221e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol @@ -0,0 +1,20 @@ +contract A { + constructor() payable {} +} + +contract B { + function f() public payable { + require(address(this).balance == 100); + A a = new A{value: 50}(); + assert(address(this).balance == 50); // should hold + assert(address(this).balance == 60); // should fail + assert(address(a).balance >= 50); // should hold + assert(address(a).balance == 50); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (211-246): CHC: Assertion violation happens here. +// Warning 6328: (316-348): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol new file mode 100644 index 000000000..7905d5b4f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol @@ -0,0 +1,28 @@ +contract D { + constructor(uint _x) { x = _x; } + uint public x; +} + +contract E { + constructor() { x = 2; } + uint public x; +} + +contract C { + constructor() { + address d = address(new D(42)); + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 43); // should fail + uint y = E(d).x(); + assert(y == 2); // should fail, it would still call D.x() == 42 + assert(y == 42); // should hold, but fails due to false positive + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (231-253): CHC: Assertion violation happens here. +// Warning 6328: (293-307): CHC: Assertion violation happens here. +// Warning 6328: (359-374): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol new file mode 100644 index 000000000..25cccead4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol @@ -0,0 +1,25 @@ +contract D { + constructor(uint _x) { x = _x; } + function setD(uint _x) public { x = _x; } + uint public x; +} + +contract C { + constructor() { + address d = address(new D(42)); + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 21); // should fail + d.call(abi.encodeCall(D.setD, (21))); + assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely + assert(D(d).x() == 42); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreCex: yes +// ---- +// Warning 9302: (257-293): Return value of low-level calls not used. +// Warning 6328: (216-238): CHC: Assertion violation happens here. +// Warning 6328: (297-319): CHC: Assertion violation happens here. +// Warning 6328: (404-426): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol new file mode 100644 index 000000000..2dc5dd0fb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol @@ -0,0 +1,28 @@ +contract D { + constructor(uint _x) { x = _x; } + uint public x; +} + +contract E { + constructor() { x = 2; } + uint public x; +} + +contract C { + function f() public { + address d = address(new D(42)); + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 43); // should fail + uint y = E(d).x(); + assert(y == 2); // should fail, it would still call D.x() == 42 + assert(y == 42); // should hold, but fails due to false positive + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (237-259): CHC: Assertion violation happens here. +// Warning 6328: (299-313): CHC: Assertion violation happens here. +// Warning 6328: (365-380): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol new file mode 100644 index 000000000..9c36bfc74 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol @@ -0,0 +1,25 @@ +contract D { + constructor(uint _x) { x = _x; } + function setD(uint _x) public { x = _x; } + uint public x; +} + +contract C { + function f() public { + address d = address(new D(42)); + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 21); // should fail + d.call(abi.encodeCall(D.setD, (21))); + assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely + assert(D(d).x() == 42); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreCex: yes +// ---- +// Warning 9302: (263-299): Return value of low-level calls not used. +// Warning 6328: (222-244): CHC: Assertion violation happens here. +// Warning 6328: (303-325): CHC: Assertion violation happens here. +// Warning 6328: (410-432): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol new file mode 100644 index 000000000..317fde003 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol @@ -0,0 +1,29 @@ +contract D { + constructor(uint _x) { x = _x; } + function setD(uint _x) public { x = _x; } + uint public x; +} + +contract C { + uint x; + + function f() public { + x = 666; + address d = address(new D(42)); + assert(D(d).x() == 42); // should hold + assert(D(d).x() == 21); // should fail + d.call(abi.encodeCall(D.setD, (21))); + assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely + assert(D(d).x() == 42); // should fail + assert(x == 666); // should hold, C's storage should not have been havoced + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreCex: yes +// ---- +// Warning 9302: (284-320): Return value of low-level calls not used. +// Warning 6328: (243-265): CHC: Assertion violation happens here. +// Warning 6328: (324-346): CHC: Assertion violation happens here. +// Warning 6328: (431-453): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol index 87a9e2261..f0f844fff 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol @@ -15,4 +15,4 @@ contract C { // Warning 2519: (106-112): This declaration shadows an existing declaration. // Warning 2072: (106-112): Unused local variable. // Warning 2072: (114-131): Unused local variable. -// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (( <= 0) || !(x <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol new file mode 100644 index 000000000..8c7b589d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol @@ -0,0 +1,21 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); // should fail + return _x; + } +} +contract C { + State s; + uint z = s.f(2); + + function f() public view { + assert(z == 2); // should hold in trusted mode + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// SMTIgnoreInv: yes +// ---- +// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol new file mode 100644 index 000000000..a81422729 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol @@ -0,0 +1,17 @@ +contract C { + uint z = this.g(2); + + function g(uint _x) public pure returns (uint) { + assert(_x > 0); // should fail + return _x; + } + + function f() public view { + assert(z == 2); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol new file mode 100644 index 000000000..8ff241e72 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol @@ -0,0 +1,25 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); // should fail + return _x; + } +} +contract C { + State s; + uint z; + + constructor() { + z = s.f(2); + } + + function f() public view { + assert(z == 2); // should hold in trusted mode + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol new file mode 100644 index 000000000..b7a161ac9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol @@ -0,0 +1,41 @@ +contract A { + uint x; + function setX(uint _x) public { + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public view { + assert(a.getX() == 0); // should fail because A.setX() can be called without B + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail because A.setX() can be called without A + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (256-277): CHC: Assertion violation happens here. +// Warning 6328: (533-554): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol new file mode 100644 index 000000000..e65d1b1e7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol @@ -0,0 +1,52 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public view { + assert(a.getX() == 0); // should hold, but fails because + // the nondet_interface constraint added for `A a` in between + // txs of `B` does not have the constraint that `msg.sender != address(this)` + // so `A.setX` is allowed with `msg.sender = address(this)` inside + // the current rules defining nondet_interface. + // If we want to support that, we likely need a new type of nondet_interface + // `nondet_interface_with_tx` that contains tx data as well as restricts + // every further `nondet_interface_with_tx` to not have that `msg.sender`. + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should hold + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (434-455): CHC: Assertion violation happens here. +// Warning 6328: (1270-1291): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol new file mode 100644 index 000000000..60bfd1660 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol @@ -0,0 +1,45 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public { + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (561-582): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol new file mode 100644 index 000000000..4e86c7b2b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol @@ -0,0 +1,48 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + address immutable owner; + constructor() { + owner = msg.sender; + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public { + require(msg.sender == owner); + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should hold + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (641-662): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol new file mode 100644 index 000000000..54566b85f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol @@ -0,0 +1,50 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + address immutable owner; + constructor() { + owner = msg.sender; + a = new A(); + } + function g() public { + require(msg.sender == owner); + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail + } + function h() public { + b.g(); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (601-622): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol new file mode 100644 index 000000000..582d967f3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol @@ -0,0 +1,17 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + this.i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol new file mode 100644 index 000000000..0f05a8b73 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol @@ -0,0 +1,16 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + ((this)).i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol new file mode 100644 index 000000000..1b95859af --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol @@ -0,0 +1,17 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + C c = this; + c.i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (158-172): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol new file mode 100644 index 000000000..c4bab9c75 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol @@ -0,0 +1,23 @@ +contract D { + uint public x; +} + +contract C { + struct S { + address d; + } + S[] ss; + constructor() { + ss.push(S(address(new D()))); + assert(D(ss[0].d).x() == 0); // should hold + } + function f() public view { + assert(D(ss[0].d).x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (210-237): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol new file mode 100644 index 000000000..522c840f5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol @@ -0,0 +1,24 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + address d; + } + S[] ss; + constructor() { + ss.push(S(address(new D()))); + assert(D(ss[0].d).x() == 0); // should hold + } + function f() public view { + assert(D(ss[0].d).x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (253-280): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 0x4706}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 0x4706}]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol new file mode 100644 index 000000000..541999b9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol @@ -0,0 +1,21 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + address[] ds; + constructor() { + ds.push(address(new D())); + assert(D(ds[0]).x() == 0); // should hold + } + function f() public view { + assert(D(ds[0]).x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (226-251): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x0]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x0]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol new file mode 100644 index 000000000..f7e31bf74 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol @@ -0,0 +1,20 @@ +contract D { + uint public x; +} + +contract C { + address[] ds; + constructor() { + ds.push(address(new D())); + assert(D(ds[0]).x() == 0); // should hold + } + function f() public view { + assert(D(ds[0]).x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (183-208): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x25]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x25]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol new file mode 100644 index 000000000..2ac70b33d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol @@ -0,0 +1,24 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + address d; + } + S s; + constructor() { + s.d = address(new D()); + assert(D(s.d).x() == 0); // should hold + } + function f() public view { + assert(D(s.d).x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (240-263): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol new file mode 100644 index 000000000..e527c5bc0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol @@ -0,0 +1,23 @@ +contract D { + uint public x; +} + +contract C { + struct S { + address d; + } + S s; + constructor() { + s.d = address(new D()); + assert(D(s.d).x() == 0); // should hold + } + function f() public view { + assert(D(s.d).x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (197-220): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol new file mode 100644 index 000000000..fff8a9718 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol @@ -0,0 +1,26 @@ +contract D { + uint public x; +} + +contract C { + struct S { + address d; + } + struct T { + S s; + } + T t; + constructor() { + t.s.d = address(new D()); + assert(D(t.s.d).x() == 0); // should hold + } + function f() public view { + assert(D(t.s.d).x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (223-248): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol new file mode 100644 index 000000000..63d026e52 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol @@ -0,0 +1,27 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + address d; + } + struct T { + S s; + } + T t; + constructor() { + t.s.d = address(new D()); + assert(D(t.s.d).x() == 0); // should hold + } + function f() public view { + assert(D(t.s.d).x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (266-291): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol new file mode 100644 index 000000000..0b8cd8e59 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol @@ -0,0 +1,23 @@ +contract D { + uint public x; +} + +contract C { + struct S { + D d; + } + S[] ss; + constructor() { + ss.push(S(new D())); + assert(ss[0].d.x() == 0); // should hold + } + function f() public view { + assert(ss[0].d.x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (192-216): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol new file mode 100644 index 000000000..97f61fa04 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol @@ -0,0 +1,24 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + D d; + } + S[] ss; + constructor() { + ss.push(S(new D())); + assert(ss[0].d.x() == 0); // should hold + } + function f() public view { + assert(ss[0].d.x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (235-259): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 20819}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 20819}]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol new file mode 100644 index 000000000..475c39184 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol @@ -0,0 +1,21 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + D[] ds; + constructor() { + ds.push(new D()); + assert(ds[0].x() == 0); // should hold + } + function f() public view { + assert(ds[0].x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (208-230): CHC: Assertion violation happens here.\nCounterexample:\nds = [39]\n\nTransaction trace:\nC.constructor()\nState: ds = [39]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol new file mode 100644 index 000000000..baeddda08 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol @@ -0,0 +1,21 @@ +contract D { + uint public x; +} + +contract C { + D[] ds; + constructor() { + ds.push(new D()); + assert(ds[0].x() == 0); // should hold + } + function f() public view { + assert(ds[0].x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (165-187): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol new file mode 100644 index 000000000..293c22304 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol @@ -0,0 +1,24 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + D d; + } + S s; + constructor() { + s.d = new D(); + assert(s.d.x() == 0); // should hold + } + function f() public view { + assert(s.d.x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (222-242): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 20819}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 20819}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol new file mode 100644 index 000000000..59381960c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol @@ -0,0 +1,24 @@ +contract D { + uint public x; +} + +contract C { + struct S { + D d; + } + S s; + constructor() { + s.d = new D(); + assert(s.d.x() == 0); // should hold + } + function f() public view { + assert(s.d.x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (179-199): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol new file mode 100644 index 000000000..06cd20cfe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol @@ -0,0 +1,27 @@ +contract D { + uint public x; +} + +contract C { + struct S { + D d; + } + struct T { + S s; + } + T t; + constructor() { + t.s.d = new D(); + assert(t.s.d.x() == 0); // should hold + } + function f() public view { + assert(t.s.d.x() == 0); // should hold, but fails because we havoc the state + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (205-227): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol new file mode 100644 index 000000000..6a1fb2274 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol @@ -0,0 +1,27 @@ +contract D { + uint public x; + function setD(uint _x) public { x = _x; } +} + +contract C { + struct S { + D d; + } + struct T { + S s; + } + T t; + constructor() { + t.s.d = new D(); + assert(t.s.d.x() == 0); // should hold + } + function f() public view { + assert(t.s.d.x() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (248-270): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 20819}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 20819}}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol index 06390b12c..c52e0773f 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (157-192): CHC: Assertion violation happens here. +// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol index fc2d844d9..f804078cd 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol @@ -1,7 +1,11 @@ contract C { function g(uint i) public { require(address(this).balance == 100); + // if called address is same as this, don't do anything with the value stuff + // or fix the receiving end this.h{value: i}(); + uint x = address(this).balance; + assert(x == 100); // should hold assert(address(this).balance == 100); // should hold assert(address(this).balance == 90); // should fail } @@ -12,4 +16,4 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (162-197): CHC: Assertion violation happens here. +// Warning 6328: (340-375): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol new file mode 100644 index 000000000..6c634d4ef --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol @@ -0,0 +1,33 @@ +contract Crypto { + function hash(bytes32) external pure returns (bytes32) { + return bytes32(0); + } +} + +contract C { + address owner; + bytes32 sig_1; + bytes32 sig_2; + Crypto d; + + constructor() { + owner = msg.sender; + } + + function f1(bytes32 _msg) public { + address prevOwner = owner; + sig_1 = d.hash(_msg); + sig_2 = d.hash(_msg); + assert(prevOwner == owner); + } + + function inv() public view { + assert(sig_1 == sig_2); + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((sig_1 <= 0) && (sig_2 <= 0))\nReentrancy property(ies) for :Crypto:\n( = 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(sig_1 == sig_2)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol new file mode 100644 index 000000000..62f53b64c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol @@ -0,0 +1,47 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + bool insidef; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function zz() public { + require(insidef); + z = 3; + } + + function f() public { + require(!insidef); + address prevOwner = owner; + insidef = true; + s.f(); + assert(z == y); + assert(prevOwner == owner); + insidef = false; + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((y <= 0) && (insidef || (z <= 0)))\nReentrancy property(ies) for :State:\n( = 0)\n = 0 -> no errors\n = 2 -> Assertion failed at assert(z == y)\n = 3 -> Assertion failed at assert(prevOwner == owner)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol new file mode 100644 index 000000000..8000b3267 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol @@ -0,0 +1,56 @@ +contract Other { + C c; + constructor(C _c) { + c = _c; + } + function h() public { + c.setOwner(address(0)); + } +} + +contract State { + uint x; + Other o; + C c; + constructor(C _c) { + c = _c; + o = new Other(_c); + } + function f() public returns (uint) { + o.h(); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); // should hold + assert(prevOwner == owner); // should not hold because of reentrancy + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (531-545): CHC: Assertion violation might happen here. +// Warning 6328: (564-590): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol new file mode 100644 index 000000000..ee373e293 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol @@ -0,0 +1,38 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function f() public view { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); + assert(prevOwner == owner); + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (314-328): CHC: Assertion violation might happen here. +// Info 1180: Reentrancy property(ies) for :State:\n( = 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(z == y)\n = 2 -> Assertion failed at assert(prevOwner == owner)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol new file mode 100644 index 000000000..4d179ddf8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol @@ -0,0 +1,44 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public returns (uint) { + c.setOwner(address(0)); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); // should hold + assert(prevOwner == owner); // should not hold because of reentrancy + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (396-410): CHC: Assertion violation might happen here. +// Warning 6328: (429-455): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol new file mode 100644 index 000000000..1c557f7a6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol @@ -0,0 +1,36 @@ +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() { + s = new State(); + owner = msg.sender; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + assert(y != z); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (355-381): CHC: Assertion violation might happen here. +// Warning 6328: (385-399): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol new file mode 100644 index 000000000..7d217e145 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol @@ -0,0 +1,40 @@ +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() { + owner = msg.sender; + s = new State(); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + assert(y != z); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (421-447): CHC: Assertion violation might happen here. +// Warning 6328: (451-465): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol index 19ff2bbad..268db82b4 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -13,4 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call +// Warning 6328: (117-131): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index b50185449..550e17b61 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -18,3 +18,5 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- +// Warning 6328: (167-181): CHC: Assertion violation might happen here. +// Warning 4661: (167-181): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol new file mode 100644 index 000000000..438feae21 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol @@ -0,0 +1,64 @@ +interface Token { + function balanceOf(address _a) external view returns (uint); + function transfer(address _to, uint _amt) external; +} + +contract TokenCorrect is Token { + mapping (address => uint) balance; + constructor(address _a, uint _b) { + balance[_a] = _b; + } + function balanceOf(address _a) public view override returns (uint) { + return balance[_a]; + } + function transfer(address _to, uint _amt) public override { + require(balance[msg.sender] >= _amt); + balance[msg.sender] -= _amt; + balance[_to] += _amt; + } +} + +contract Test { + function property_transfer(address _token, address _to, uint _amt) public { + require(_to != address(this)); + + TokenCorrect t = TokenCorrect(_token); + + uint xPre = t.balanceOf(address(this)); + require(xPre >= _amt); + uint yPre = t.balanceOf(_to); + + t.transfer(_to, _amt); + uint xPost = t.balanceOf(address(this)); + uint yPost = t.balanceOf(_to); + + assert(xPost == xPre - _amt); + assert(yPost == yPre + _amt); + } + + function test_concrete() public { + TokenCorrect t = new TokenCorrect(address(this), 1000); + + uint b = t.balanceOf(address(this)); + assert(b == 1000); + + address other = address(0x333); + require(address(this) != other); + + uint c = t.balanceOf(other); + assert(c == 0); + + t.transfer(other, 100); + + uint d = t.balanceOf(address(this)); + assert(d == 900); + + uint e = t.balanceOf(other); + assert(e == 100); + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTContract: Test +// SMTTargets: assert diff --git a/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol new file mode 100644 index 000000000..6bb6074b2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol @@ -0,0 +1,68 @@ +interface Token { + function balanceOf(address _a) external view returns (uint); + function transfer(address _to, uint _amt) external; +} + +contract TokenWrong is Token { + mapping (address => uint) balance; + constructor(address _a, uint _b) { + balance[_a] = _b; + } + function balanceOf(address _a) public view override returns (uint) { + return balance[_a]; + } + function transfer(address _to, uint _amt) public override { + require(balance[msg.sender] >= _amt); + // Commented out to make this token implementation wrong. + //balance[msg.sender] -= _amt; + balance[_to] += _amt; + } +} + +contract Test { + function property_transfer(address _token, address _to, uint _amt) public { + require(_to != address(this)); + + TokenWrong t = TokenWrong(_token); + + uint xPre = t.balanceOf(address(this)); + require(xPre >= _amt); + uint yPre = t.balanceOf(_to); + + t.transfer(_to, _amt); + uint xPost = t.balanceOf(address(this)); + uint yPost = t.balanceOf(_to); + + assert(xPost == xPre - _amt); // should fail + assert(yPost == yPre + _amt); + } + + function test_concrete() public { + TokenWrong t = new TokenWrong(address(this), 1000); + + uint b = t.balanceOf(address(this)); + assert(b == 1000); + + address other = address(0x333); + require(address(this) != other); + + uint c = t.balanceOf(other); + assert(c == 0); + + t.transfer(other, 100); + + uint d = t.balanceOf(address(this)); + assert(d == 900); // should fail + + uint e = t.balanceOf(other); + assert(e == 100); + } +} +// ==== +// SMTContract: Test +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (950-978): CHC: Assertion violation happens here. +// Warning 6328: (1370-1386): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol index 8a0f118ae..925f53bc9 100644 --- a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol +++ b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol @@ -14,5 +14,5 @@ contract D { // ==== // SMTEngine: all // ---- -// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call. +// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. // Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call\n (new C()).x() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index 5efcb2da1..3a3b295e4 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'[1] + ((- 1) * map'[0])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 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)) && !( = 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 diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol new file mode 100644 index 000000000..00bfb35ca --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol @@ -0,0 +1,22 @@ +contract D { + uint public d; + function g() public { + ++d; + } +} + +contract C { + function f() public { + D a = new D(); + assert(a.d() == 0); // should hold + a.g(); + assert(a.d() == 1); // should hold + assert(a.d() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (203-221): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol new file mode 100644 index 000000000..5da279fc9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol @@ -0,0 +1,33 @@ +contract E { + uint public e; + function setE(uint _e) public { + e = _e; + } +} + +contract D { + E e; + constructor(E _e) { + e = _e; + } + function setE(uint x) public { + e.setE(x); + } +} + +contract C { + function f() public { + E e = new E(); + D d = new D(e); + assert(e.e() == 0); // should hold + d.setE(42); + assert(e.e() == 42); // should hold + assert(e.e() == 2); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (344-362): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol new file mode 100644 index 000000000..b7673203e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol @@ -0,0 +1,18 @@ +contract C { + uint public x; + + function f() public { + x = 2; + x = 3; + uint y = this.x(); + assert(y == 3); // should hold + assert(y == 2); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (127-141): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol new file mode 100644 index 000000000..b3dfe04ad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol @@ -0,0 +1,19 @@ +contract C { + uint public x; + + function f() public { + x = 2; + x = 3; + C c = this; + uint y = c.x(); + assert(y == 3); // should hold + assert(y == 2); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (138-152): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol index 0117f9b49..e30a5e743 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol @@ -27,4 +27,4 @@ contract C is A { // ---- // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i() // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i() -// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n +// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n diff --git a/test/libsolidity/smtCheckerTests/imports/ExtCall.sol b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol index 047148a90..7675bc42e 100644 --- a/test/libsolidity/smtCheckerTests/imports/ExtCall.sol +++ b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol @@ -39,4 +39,4 @@ contract ExtCallTest { // SMTIgnoreCex: yes // ---- // Warning 6328: (ExtCall.sol:362-381): CHC: Assertion violation happens here. -// Warning 4588: (ExtCall.t.sol:110-123): Assertion checker does not yet implement this type of function call. +// Warning 8729: (ExtCall.t.sol:110-123): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol index 8ddef2da9..1298f1f09 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol @@ -17,6 +17,7 @@ function f(uint _x) pure { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call // Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol index 42775cc9b..b7b06b1fc 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol @@ -11,5 +11,6 @@ contract C } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0) +// Warning 6328: (164-183): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol index b26fcbd93..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)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(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 0f511a05d..7af8c96c8 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -11,6 +11,7 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- // Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 5892\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 11 }\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/try_catch/try_new.sol b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol index e7075e076..5c98c279d 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_new.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol @@ -28,5 +28,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4588: (231-245): Assertion checker does not yet implement this type of function call. -// Warning 4588: (492-507): Assertion checker does not yet implement this type of function call. +// Warning 8729: (231-245): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (492-507): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol index 1d00e7fe3..ffd6304c9 100644 --- a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol @@ -11,4 +11,7 @@ contract C { assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold } } +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes // ---- diff --git a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol index 4910c417e..33546b49c 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s() +// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s() diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol index 44daa8912..7e23d77d6 100644 --- a/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol @@ -5,5 +5,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- // Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = true\ny = false\n\nTransaction trace:\nC.constructor()\nC.f(true, false) diff --git a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol index 5cb307385..1a72cad3d 100644 --- a/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol +++ b/test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol @@ -23,4 +23,3 @@ contract C { ); } } -// ---- diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index e8206e483..bd51fe920 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -145,6 +145,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-div-mod-no-slacks", "--model-checker-engine=bmc", + "--model-checker-ext-calls=trusted", "--model-checker-invariants=contract,reentrancy", "--model-checker-show-unproved", "--model-checker-solvers=z3,smtlib2", @@ -211,6 +212,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, true, {true, false}, + {ModelCheckerExtCalls::Mode::TRUSTED}, {{InvariantType::Contract, InvariantType::Reentrancy}}, true, {false, false, true, true}, diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 895957f4d..47ab7e49c 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -108,6 +108,7 @@ void FuzzerUtil::testCompiler( frontend::ModelCheckerContracts::Default(), /*divModWithSlacks*/true, frontend::ModelCheckerEngine::All(), + frontend::ModelCheckerExtCalls{}, frontend::ModelCheckerInvariants::All(), /*showUnproved=*/false, smtutil::SMTSolverChoice::All(),