1 /* 2 This file is part of solidity. 3 4 solidity is free software: you can redistribute it and/or modify 5 it under the terms of the GNU General Public License as published by 6 the Free Software Foundation, either version 3 of the License, or 7 (at your option) any later version. 8 9 solidity is distributed in the hope that it will be useful, 10 but WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12 GNU General Public License for more details. 13 14 You should have received a copy of the GNU General Public License 15 along with solidity. If not, see <http://www.gnu.org/licenses/>. 16 */ 17 // SPDX-License-Identifier: GPL-3.0 18 19 #pragma once 20 21 #include <libsolidity/formal/Predicate.h> 22 23 #include <libsolidity/formal/SymbolicState.h> 24 25 #include <libsmtutil/Sorts.h> 26 27 namespace solidity::frontend::smt 28 { 29 30 /** 31 * This file represents the specification for CHC predicate sorts. 32 * Types of predicates: 33 * 34 * 1. Interface 35 * The idle state of a contract. Signature: 36 * interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables). 37 * 38 * 2. Nondet interface 39 * The nondeterminism behavior of a contract. Signature: 40 * nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables'). 41 * 42 * 3. Constructor entry/summary 43 * The summary of a contract's deployment procedure. 44 * Signature: 45 * If the contract has a constructor function, this is the same as the summary of that function. Otherwise: 46 * constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables'). 47 * 48 * 4. Function entry/summary 49 * The entry point of a function definition. Signature: 50 * function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). 51 * 52 * 5. Function body 53 * Use for any predicate within a function. Signature: 54 * function_body(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables). 55 */ 56 57 /// @returns the interface predicate sort for _contract. 58 smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state); 59 60 /// @returns the nondeterminisc interface predicate sort for _contract. 61 smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state); 62 63 /// @returns the constructor entry/summary predicate sort for _contract. 64 smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state); 65 66 /// @returns the function entry/summary predicate sort for _function contained in _contract. 67 smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state); 68 69 /// @returns the function body predicate sort for _function contained in _contract. 70 smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state); 71 72 /// @returns the sort of a predicate without parameters. 73 smtutil::SortPointer arity0FunctionSort(); 74 75 /// Helpers 76 77 std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract) ; 78 79 } 80