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 /** 20 * Model checker based on Constrained Horn Clauses. 21 * 22 * A Solidity contract's CFG is encoded into a system of Horn clauses where 23 * each block has a predicate and edges are rules. 24 * 25 * The entry block is the constructor which has no in-edges. 26 * The constructor has one out-edge to an artificial block named _Interface_ 27 * which has in/out-edges from/to all public functions. 28 * 29 * Loop invariants for Interface -> Interface' are state invariants. 30 */ 31 32 #pragma once 33 34 #include <libsolidity/formal/ModelCheckerSettings.h> 35 #include <libsolidity/formal/Predicate.h> 36 #include <libsolidity/formal/SMTEncoder.h> 37 38 #include <libsolidity/interface/ReadFile.h> 39 40 #include <libsmtutil/CHCSolverInterface.h> 41 42 #include <liblangutil/SourceLocation.h> 43 #include <liblangutil/UniqueErrorReporter.h> 44 45 #include <boost/algorithm/string/join.hpp> 46 47 #include <map> 48 #include <optional> 49 #include <set> 50 51 namespace solidity::frontend 52 { 53 54 class CHC: public SMTEncoder 55 { 56 public: 57 CHC( 58 smt::EncodingContext& _context, 59 langutil::UniqueErrorReporter& _errorReporter, 60 std::map<util::h256, std::string> const& _smtlib2Responses, 61 ReadCallback::Callback const& _smtCallback, 62 ModelCheckerSettings const& _settings, 63 langutil::CharStreamProvider const& _charStreamProvider 64 ); 65 66 void analyze(SourceUnit const& _sources); 67 68 struct ReportTargetInfo 69 { 70 langutil::ErrorId error; 71 langutil::SourceLocation location; 72 std::string message; 73 }; safeTargets()74 std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; } unsafeTargets()75 std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; } 76 77 /// This is used if the Horn solver is not directly linked into this binary. 78 /// @returns a list of inputs to the Horn solver that were not part of the argument to 79 /// the constructor. 80 std::vector<std::string> unhandledQueries() const; 81 82 enum class CHCNatspecOption 83 { 84 AbstractFunctionNondet 85 }; 86 87 private: 88 /// Visitor functions. 89 //@{ 90 bool visit(ContractDefinition const& _node) override; 91 void endVisit(ContractDefinition const& _node) override; 92 bool visit(FunctionDefinition const& _node) override; 93 void endVisit(FunctionDefinition const& _node) override; 94 bool visit(Block const& _block) override; 95 void endVisit(Block const& _block) override; 96 bool visit(IfStatement const& _node) override; 97 bool visit(WhileStatement const&) override; 98 bool visit(ForStatement const&) override; 99 void endVisit(ForStatement const&) override; 100 void endVisit(FunctionCall const& _node) override; 101 void endVisit(Break const& _node) override; 102 void endVisit(Continue const& _node) override; 103 void endVisit(IndexRangeAccess const& _node) override; 104 void endVisit(Return const& _node) override; 105 bool visit(TryCatchClause const&) override; 106 void endVisit(TryCatchClause const&) override; 107 bool visit(TryStatement const& _node) override; 108 109 void pushInlineFrame(CallableDeclaration const& _callable) override; 110 void popInlineFrame(CallableDeclaration const& _callable) override; 111 112 void visitAssert(FunctionCall const& _funCall); 113 void visitAddMulMod(FunctionCall const& _funCall) override; 114 void internalFunctionCall(FunctionCall const& _funCall); 115 void externalFunctionCall(FunctionCall const& _funCall); 116 void externalFunctionCallToTrustedCode(FunctionCall const& _funCall); 117 void unknownFunctionCall(FunctionCall const& _funCall); 118 void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; 119 void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override; 120 /// Creates underflow/overflow verification targets. 121 std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation( 122 Token _op, 123 smtutil::Expression const& _left, 124 smtutil::Expression const& _right, 125 Type const* _commonType, 126 Expression const& _expression 127 ) override; 128 //@} 129 130 /// Helpers. 131 //@{ 132 void resetSourceAnalysis(); 133 void resetContractAnalysis(); 134 void eraseKnowledge(); 135 void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; 136 void setCurrentBlock(Predicate const& _block); 137 std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot); 138 //@} 139 140 /// SMT Natspec and abstraction helpers. 141 //@{ 142 /// @returns a CHCNatspecOption enum if _option is a valid SMTChecker Natspec value 143 /// or nullopt otherwise. 144 static std::optional<CHCNatspecOption> natspecOptionFromString(std::string const& _option); 145 /// @returns which SMTChecker options are enabled by @a _function's Natspec via 146 /// `@custom:smtchecker <option>` or nullopt if none is used. 147 std::set<CHCNatspecOption> smtNatspecTags(FunctionDefinition const& _function); 148 /// @returns true if _function is Natspec annotated to be abstracted by 149 /// nondeterministic values. 150 bool abstractAsNondet(FunctionDefinition const& _function); 151 //@} 152 153 /// Sort helpers. 154 //@{ 155 smtutil::SortPointer sort(FunctionDefinition const& _function); 156 smtutil::SortPointer sort(ASTNode const* _block); 157 //@} 158 159 /// Predicate helpers. 160 //@{ 161 /// @returns a new block of given _sort and _name. 162 Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr, ContractDefinition const* _contractContext = nullptr); 163 164 /// Creates summary predicates for all functions of all contracts 165 /// in a given _source. 166 void defineInterfacesAndSummaries(SourceUnit const& _source); 167 168 /// Creates the rule 169 /// summary_function \land transaction_entry_constraints => external_summary_function 170 /// This is needed to add these transaction entry constraints which include 171 /// potential balance increase by external means, for example. 172 void defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract); 173 174 /// Creates a CHC system that, for a given contract, 175 /// - initializes its state variables (as 0 or given value, if any). 176 /// - "calls" the explicit constructor function of the contract, if any. 177 void defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext); 178 179 /// Interface predicate over current variables. 180 smtutil::Expression interface(); 181 smtutil::Expression interface(ContractDefinition const& _contract); 182 /// Error predicate over current variables. 183 smtutil::Expression error(); 184 smtutil::Expression error(unsigned _idx); 185 186 /// Creates a block for the given _node. 187 Predicate const* createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix = ""); 188 /// Creates a call block for the given function _function from contract _contract. 189 /// The contract is needed here because of inheritance. 190 /// There are different types of summaries, where the most common is FunctionSummary, 191 /// but other summaries are also used for internal and external function calls. 192 Predicate const* createSummaryBlock( 193 FunctionDefinition const& _function, 194 ContractDefinition const& _contract, 195 PredicateType _type = PredicateType::FunctionSummary 196 ); 197 198 /// @returns a block related to @a _contract's constructor. 199 Predicate const* createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix); 200 201 /// Creates a new error block to be used by an assertion. 202 /// Also registers the predicate. 203 void createErrorBlock(); 204 205 void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true)); 206 207 /// @returns The initial constraints that set up the beginning of a function. 208 smtutil::Expression initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function = nullptr); 209 210 /// @returns the symbolic values of the state variables at the beginning 211 /// of the current transaction. 212 std::vector<smtutil::Expression> initialStateVariables(); 213 std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index); 214 std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract); 215 /// @returns the current symbolic values of the current state variables. 216 std::vector<smtutil::Expression> currentStateVariables(); 217 std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract); 218 219 /// @returns \bigwedge currentValue(_vars[i]) == initialState(_var[i]) 220 smtutil::Expression currentEqualInitialVarsConstraints(std::vector<VariableDeclaration const*> const& _vars) const; 221 222 /// @returns the predicate name for a given node. 223 std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); 224 /// @returns a predicate application after checking the predicate's type. 225 smtutil::Expression predicate(Predicate const& _block); 226 /// @returns the summary predicate for the called function. 227 smtutil::Expression predicate(FunctionCall const& _funCall); 228 /// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext. 229 smtutil::Expression initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext); 230 /// @returns a predicate that defines a constructor summary. 231 smtutil::Expression summary(ContractDefinition const& _contract); 232 /// @returns a predicate that defines a function summary. 233 smtutil::Expression summary(FunctionDefinition const& _function); 234 smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract); 235 /// @returns a predicate that applies a function summary 236 /// over the constrained variables. 237 smtutil::Expression summaryCall(FunctionDefinition const& _function); 238 smtutil::Expression summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract); 239 /// @returns a predicate that defines an external function summary. 240 smtutil::Expression externalSummary(FunctionDefinition const& _function); 241 smtutil::Expression externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract); 242 //@} 243 244 /// Solver related. 245 //@{ 246 /// Adds Horn rule to the solver. 247 void addRule(smtutil::Expression const& _rule, std::string const& _ruleName); 248 /// @returns <true, invariant, empty> if query is unsatisfiable (safe). 249 /// @returns <false, Expression(true), model> otherwise. 250 std::tuple<smtutil::CheckResult, smtutil::Expression, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location); 251 252 void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTargetType _type, smtutil::Expression const& _errorCondition); 253 254 void checkVerificationTargets(); 255 // Forward declarations. Definitions are below. 256 struct CHCVerificationTarget; 257 struct CHCQueryPlaceholder; 258 void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target); 259 void checkAndReportTarget( 260 CHCVerificationTarget const& _target, 261 std::vector<CHCQueryPlaceholder> const& _placeholders, 262 langutil::ErrorId _errorReporterId, 263 std::string _satMsg, 264 std::string _unknownMsg = "" 265 ); 266 267 std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root); 268 269 /// @returns a call graph for function summaries in the counterexample graph. 270 /// The returned map also contains a key _root, whose value are the 271 /// summaries called by _root. 272 std::map<unsigned, std::vector<unsigned>> summaryCalls( 273 smtutil::CHCSolverInterface::CexGraph const& _graph, 274 unsigned _root 275 ); 276 277 /// @returns a set of pairs _var = _value separated by _separator. 278 template <typename T> formatVariableModel(std::vector<T> const & _variables,std::vector<std::optional<std::string>> const & _values,std::string const & _separator)279 std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::optional<std::string>> const& _values, std::string const& _separator) const 280 { 281 solAssert(_variables.size() == _values.size(), ""); 282 283 std::vector<std::string> assignments; 284 for (unsigned i = 0; i < _values.size(); ++i) 285 { 286 auto var = _variables.at(i); 287 if (var && _values.at(i)) 288 assignments.emplace_back(var->name() + " = " + *_values.at(i)); 289 } 290 291 return boost::algorithm::join(assignments, _separator); 292 } 293 294 /// @returns a DAG in the dot format. 295 /// Used for debugging purposes. 296 std::string cex2dot(smtutil::CHCSolverInterface::CexGraph const& _graph); 297 //@} 298 299 /// Misc. 300 //@{ 301 /// @returns a prefix to be used in a new unique block name 302 /// and increases the block counter. 303 std::string uniquePrefix(); 304 305 /// @returns a suffix to be used by contract related predicates. 306 std::string contractSuffix(ContractDefinition const& _contract); 307 308 /// @returns a new unique error id associated with _expr and stores 309 /// it into m_errorIds. 310 unsigned newErrorId(); 311 312 smt::SymbolicIntVariable& errorFlag(); 313 //@} 314 315 /// Predicates. 316 //@{ 317 /// Artificial Interface predicate. 318 /// Single entry block for all functions. 319 std::map<ContractDefinition const*, Predicate const*> m_interfaces; 320 321 /// Nondeterministic interfaces. 322 /// These are used when the analyzed contract makes external calls to unknown code, 323 /// which means that the analyzed contract can potentially be called 324 /// nondeterministically. 325 std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces; 326 327 std::map<ContractDefinition const*, Predicate const*> m_constructorSummaries; 328 std::map<ContractDefinition const*, std::map<ContractDefinition const*, Predicate const*>> m_contractInitializers; 329 330 /// Artificial Error predicate. 331 /// Single error block for all assertions. 332 Predicate const* m_errorPredicate = nullptr; 333 334 /// Function predicates. 335 std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries; 336 337 /// External function predicates. 338 std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_externalSummaries; 339 //@} 340 341 /// Variables. 342 //@{ 343 /// State variables. 344 /// Used to create all predicates. 345 std::vector<VariableDeclaration const*> m_stateVariables; 346 //@} 347 348 /// Verification targets. 349 //@{ 350 struct CHCVerificationTarget: VerificationTarget 351 { 352 unsigned const errorId; 353 ASTNode const* const errorNode; 354 }; 355 356 /// Query placeholder stores information necessary to create the final query edge in the CHC system. 357 /// It is combined with the unique error id (and error type) to create a complete Verification Target. 358 struct CHCQueryPlaceholder 359 { 360 smtutil::Expression const constraints; 361 smtutil::Expression const errorExpression; 362 smtutil::Expression const fromPredicate; 363 }; 364 365 /// Query placeholders for constructors, if the key has type ContractDefinition*, 366 /// or external functions, if the key has type FunctionDefinition*. 367 /// A placeholder is created for each possible context of a function (e.g. multiple contracts in contract inheritance hierarchy). 368 std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, smt::EncodingContext::IdCompare> m_queryPlaceholders; 369 370 /// Records verification conditions IDs per function encountered during an analysis of that function. 371 /// The key is the ASTNode of the function where the verification condition has been encountered, 372 /// or the ASTNode of the contract if the verification condition happens inside an implicit constructor. 373 std::map<ASTNode const*, std::vector<unsigned>, smt::EncodingContext::IdCompare> m_functionTargetIds; 374 /// Helper mapping unique IDs to actual verification targets. 375 std::map<unsigned, CHCVerificationTarget> m_verificationTargets; 376 377 /// Targets proved safe. 378 std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_safeTargets; 379 /// Targets proved unsafe. 380 std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets; 381 /// Targets not proved. 382 std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets; 383 384 /// Inferred invariants. 385 std::map<Predicate const*, std::set<std::string>, PredicateCompare> m_invariants; 386 //@} 387 388 /// Control-flow. 389 //@{ 390 FunctionDefinition const* m_currentFunction = nullptr; 391 392 std::map<ASTNode const*, std::set<ASTNode const*, smt::EncodingContext::IdCompare>, smt::EncodingContext::IdCompare> m_callGraph; 393 394 /// The current block. 395 smtutil::Expression m_currentBlock = smtutil::Expression(true); 396 397 /// Counter to generate unique block names. 398 unsigned m_blockCounter = 0; 399 400 /// Whether a function call was seen in the current scope. 401 bool m_unknownFunctionCallSeen = false; 402 403 /// Block where a loop break should go to. 404 Predicate const* m_breakDest = nullptr; 405 /// Block where a loop continue should go to. 406 Predicate const* m_continueDest = nullptr; 407 408 /// Block where an error condition should go to. 409 /// This can be: 410 /// 1) Constructor initializer summary, if error happens while evaluating initial values of state variables. 411 /// 2) Constructor summary, if error happens while evaluating base constructor arguments. 412 /// 3) Function summary, if error happens inside a function. 413 Predicate const* m_errorDest = nullptr; 414 415 /// Represents the stack of destinations where a `return` should go. 416 /// This is different from `m_errorDest` above: 417 /// - Constructor initializers and constructor summaries will never be `return` targets because they are artificial. 418 /// - Modifiers also have their own `return` target blocks, whereas they do not have their own error destination. 419 std::vector<Predicate const*> m_returnDests; 420 //@} 421 422 /// CHC solver. 423 std::unique_ptr<smtutil::CHCSolverInterface> m_interface; 424 }; 425 426 } 427