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/SymbolicVariables.h> 22 #include <libsolidity/formal/SymbolicVariables.h> 23 24 #include <libsolidity/ast/AST.h> 25 26 #include <libsmtutil/Sorts.h> 27 28 #include <map> 29 #include <optional> 30 #include <vector> 31 32 namespace solidity::langutil 33 { 34 class CharStreamProvider; 35 } 36 37 namespace solidity::frontend 38 { 39 40 enum class PredicateType 41 { 42 Interface, 43 NondetInterface, 44 ConstructorSummary, 45 FunctionSummary, 46 FunctionBlock, 47 FunctionErrorBlock, 48 InternalCall, 49 ExternalCallTrusted, 50 ExternalCallUntrusted, 51 Error, 52 Custom 53 }; 54 55 /** 56 * Represents a predicate used by the CHC engine. 57 */ 58 class Predicate 59 { 60 public: 61 static Predicate const* create( 62 smtutil::SortPointer _sort, 63 std::string _name, 64 PredicateType _type, 65 smt::EncodingContext& _context, 66 ASTNode const* _node = nullptr, 67 ContractDefinition const* _contractContext = nullptr, 68 std::vector<ScopeOpener const*> _scopeStack = {} 69 ); 70 71 Predicate( 72 smt::SymbolicFunctionVariable&& _predicate, 73 PredicateType _type, 74 ASTNode const* _node = nullptr, 75 ContractDefinition const* _contractContext = nullptr, 76 std::vector<ScopeOpener const*> _scopeStack = {} 77 ); 78 79 /// Predicate should not be copiable. 80 Predicate(Predicate const&) = delete; 81 Predicate& operator=(Predicate const&) = delete; 82 83 /// @returns the Predicate associated with _name. 84 static Predicate const* predicate(std::string const& _name); 85 86 /// Resets all the allocated predicates. 87 static void reset(); 88 89 /// @returns a function application of the predicate over _args. 90 smtutil::Expression operator()(std::vector<smtutil::Expression> const& _args) const; 91 92 /// @returns the function declaration of the predicate. 93 smtutil::Expression functor() const; 94 /// @returns the function declaration of the predicate with index _idx. 95 smtutil::Expression functor(unsigned _idx) const; 96 /// Increases the index of the function declaration of the predicate. 97 void newFunctor(); 98 99 /// @returns the program node this predicate represents. 100 ASTNode const* programNode() const; 101 102 /// @returns the ContractDefinition of the most derived contract 103 /// being analyzed. 104 ContractDefinition const* contextContract() const; 105 106 /// @returns the ContractDefinition that this predicate represents 107 /// or nullptr otherwise. 108 ContractDefinition const* programContract() const; 109 110 /// @returns the FunctionDefinition that this predicate represents 111 /// or nullptr otherwise. 112 FunctionDefinition const* programFunction() const; 113 114 /// @returns the FunctionCall that this predicate represents 115 /// or nullptr otherwise. 116 FunctionCall const* programFunctionCall() const; 117 118 /// @returns the program state variables in the scope of this predicate. 119 std::optional<std::vector<VariableDeclaration const*>> stateVariables() const; 120 121 /// @returns true if this predicate represents a summary. 122 bool isSummary() const; 123 124 /// @returns true if this predicate represents a function summary. 125 bool isFunctionSummary() const; 126 127 /// @returns true if this predicate represents a function block. 128 bool isFunctionBlock() const; 129 130 /// @returns true if this predicate represents a function error block. 131 bool isFunctionErrorBlock() const; 132 133 /// @returns true if this predicate represents an internal function call. 134 bool isInternalCall() const; 135 136 /// @returns true if this predicate represents a trusted external function call. 137 bool isExternalCallTrusted() const; 138 139 /// @returns true if this predicate represents an untrusted external function call. 140 bool isExternalCallUntrusted() const; 141 142 /// @returns true if this predicate represents a constructor summary. 143 bool isConstructorSummary() const; 144 145 /// @returns true if this predicate represents an interface. 146 bool isInterface() const; 147 148 /// @returns true if this predicate represents a nondeterministic interface. 149 bool isNondetInterface() const; 150 type()151 PredicateType type() const { return m_type; } 152 153 /// @returns a formatted string representing a call to this predicate 154 /// with _args. 155 std::string formatSummaryCall( 156 std::vector<smtutil::Expression> const& _args, 157 langutil::CharStreamProvider const& _charStreamProvider, 158 bool _appendTxVars = false 159 ) const; 160 161 /// @returns the values of the state variables from _args at the point 162 /// where this summary was reached. 163 std::vector<std::optional<std::string>> summaryStateValues(std::vector<smtutil::Expression> const& _args) const; 164 165 /// @returns the values of the function input variables from _args at the point 166 /// where this summary was reached. 167 std::vector<std::optional<std::string>> summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const; 168 169 /// @returns the values of the function output variables from _args at the point 170 /// where this summary was reached. 171 std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const; 172 173 /// @returns the values of the local variables used by this predicate. 174 std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> localVariableValues(std::vector<smtutil::Expression> const& _args) const; 175 176 /// @returns a substitution map from the arguments of _predExpr 177 /// to a Solidity-like expression. 178 std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExpr) const; 179 180 private: 181 /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. 182 std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<Type const*> const& _types) const; 183 184 /// @returns a string representation of the SMT expression based on a Solidity type. 185 std::optional<std::string> expressionToString(smtutil::Expression const& _expr, Type const* _type) const; 186 187 /// Recursively fills _array from _expr. 188 /// _expr should have the form `store(store(...(const_array(x_0), i_0, e_0), i_m, e_m), i_k, e_k)`. 189 /// @returns true if the construction worked, 190 /// and false if at least one element could not be built. 191 bool fillArray(smtutil::Expression const& _expr, std::vector<std::string>& _array, ArrayType const& _type) const; 192 193 std::map<std::string, std::optional<std::string>> readTxVars(smtutil::Expression const& _tx) const; 194 195 /// The actual SMT expression. 196 smt::SymbolicFunctionVariable m_predicate; 197 198 /// The type of this predicate. 199 PredicateType m_type; 200 201 /// The ASTNode that this predicate represents. 202 /// nullptr if this predicate is not associated with a specific program AST node. 203 ASTNode const* m_node = nullptr; 204 205 /// The ContractDefinition that contains this predicate. 206 /// nullptr if this predicate is not associated with a specific contract. 207 /// This is unfortunately necessary because of virtual resolution for 208 /// function nodes. 209 ContractDefinition const* m_contractContext = nullptr; 210 211 /// Maps the name of the predicate to the actual Predicate. 212 /// Used in counterexample generation. 213 static std::map<std::string, Predicate> m_predicates; 214 215 /// The scope stack when the predicate was created. 216 /// Used to identify the subset of variables in scope. 217 std::vector<ScopeOpener const*> const m_scopeStack; 218 }; 219 220 struct PredicateCompare 221 { operatorPredicateCompare222 bool operator()(Predicate const* lhs, Predicate const* rhs) const 223 { 224 // We cannot use m_node->id() because different predicates may 225 // represent the same program node. 226 // We use the symbolic name since it is unique per predicate and 227 // the order does not really matter. 228 return lhs->functor().name < rhs->functor().name; 229 } 230 }; 231 232 } 233