1 //===- Solver.h -------------------------------------------------*- C++ -*-===// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 // 9 // This file defines an interface for a SAT solver that can be used by 10 // dataflow analyses. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H 15 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H 16 17 #include "clang/Analysis/FlowSensitive/Formula.h" 18 #include "clang/Basic/LLVM.h" 19 #include "llvm/ADT/ArrayRef.h" 20 #include "llvm/ADT/DenseMap.h" 21 #include <optional> 22 #include <vector> 23 24 namespace clang { 25 namespace dataflow { 26 27 /// An interface for a SAT solver that can be used by dataflow analyses. 28 class Solver { 29 public: 30 struct Result { 31 enum class Status { 32 /// Indicates that there exists a satisfying assignment for a boolean 33 /// formula. 34 Satisfiable, 35 36 /// Indicates that there is no satisfying assignment for a boolean 37 /// formula. 38 Unsatisfiable, 39 40 /// Indicates that the solver gave up trying to find a satisfying 41 /// assignment for a boolean formula. 42 TimedOut, 43 }; 44 45 /// A boolean value is set to true or false in a truth assignment. 46 enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 }; 47 48 /// Constructs a result indicating that the queried boolean formula is 49 /// satisfiable. The result will hold a solution found by the solver. SatisfiableResult50 static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) { 51 return Result(Status::Satisfiable, std::move(Solution)); 52 } 53 54 /// Constructs a result indicating that the queried boolean formula is 55 /// unsatisfiable. UnsatisfiableResult56 static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); } 57 58 /// Constructs a result indicating that satisfiability checking on the 59 /// queried boolean formula was not completed. TimedOutResult60 static Result TimedOut() { return Result(Status::TimedOut, {}); } 61 62 /// Returns the status of satisfiability checking on the queried boolean 63 /// formula. getStatusResult64 Status getStatus() const { return SATCheckStatus; } 65 66 /// Returns a truth assignment to boolean values that satisfies the queried 67 /// boolean formula if available. Otherwise, an empty optional is returned. getSolutionResult68 std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const { 69 return Solution; 70 } 71 72 private: ResultResult73 Result(Status SATCheckStatus, 74 std::optional<llvm::DenseMap<Atom, Assignment>> Solution) 75 : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {} 76 77 Status SATCheckStatus; 78 std::optional<llvm::DenseMap<Atom, Assignment>> Solution; 79 }; 80 81 virtual ~Solver() = default; 82 83 /// Checks if the conjunction of `Vals` is satisfiable and returns the 84 /// corresponding result. 85 /// 86 /// Requirements: 87 /// 88 /// All elements in `Vals` must not be null. 89 virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0; 90 91 // Did the solver reach its resource limit? 92 virtual bool reachedLimit() const = 0; 93 }; 94 95 llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &); 96 llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment); 97 98 } // namespace dataflow 99 } // namespace clang 100 101 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H 102