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 namespace solidity::frontend::smt 24 { 25 26 class EncodingContext; 27 28 /** 29 * This file represents the specification for building CHC predicate instances. 30 * The predicates follow the specification in PredicateSort.h. 31 * */ 32 33 smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); 34 35 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); 36 37 smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx); 38 39 smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context); 40 smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context); 41 42 smtutil::Expression function( 43 Predicate const& _pred, 44 ContractDefinition const* _contract, 45 EncodingContext& _context 46 ); 47 48 smtutil::Expression functionCall( 49 Predicate const& _pred, 50 ContractDefinition const* _contract, 51 EncodingContext& _context 52 ); 53 54 smtutil::Expression functionBlock( 55 Predicate const& _pred, 56 FunctionDefinition const& _function, 57 ContractDefinition const* _contract, 58 EncodingContext& _context 59 ); 60 61 /// Helpers 62 63 std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context); 64 65 std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context); 66 67 std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context); 68 69 std::vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contract, EncodingContext& _context); 70 71 std::vector<smtutil::Expression> currentFunctionVariablesForDefinition( 72 FunctionDefinition const& _function, 73 ContractDefinition const* _contract, 74 EncodingContext& _context 75 ); 76 77 std::vector<smtutil::Expression> currentFunctionVariablesForCall( 78 FunctionDefinition const& _function, 79 ContractDefinition const* _contract, 80 EncodingContext& _context 81 ); 82 83 std::vector<smtutil::Expression> currentBlockVariables( 84 FunctionDefinition const& _function, 85 ContractDefinition const* _contract, 86 EncodingContext& _context 87 ); 88 89 } 90