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/Value.h" 18 #include "llvm/ADT/DenseMap.h" 19 #include "llvm/ADT/DenseSet.h" 20 #include "llvm/ADT/Optional.h" 21 22 namespace clang { 23 namespace dataflow { 24 25 /// An interface for a SAT solver that can be used by dataflow analyses. 26 class Solver { 27 public: 28 struct Result { 29 enum class Status { 30 /// Indicates that there exists a satisfying assignment for a boolean 31 /// formula. 32 Satisfiable, 33 34 /// Indicates that there is no satisfying assignment for a boolean 35 /// formula. 36 Unsatisfiable, 37 38 /// Indicates that the solver gave up trying to find a satisfying 39 /// assignment for a boolean formula. 40 TimedOut, 41 }; 42 43 /// A boolean value is set to true or false in a truth assignment. 44 enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 }; 45 46 /// Constructs a result indicating that the queried boolean formula is 47 /// satisfiable. The result will hold a solution found by the solver. 48 static Result 49 Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) { 50 return Result(Status::Satisfiable, std::move(Solution)); 51 } 52 53 /// Constructs a result indicating that the queried boolean formula is 54 /// unsatisfiable. 55 static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); } 56 57 /// Constructs a result indicating that satisfiability checking on the 58 /// queried boolean formula was not completed. 59 static Result TimedOut() { return Result(Status::TimedOut, {}); } 60 61 /// Returns the status of satisfiability checking on the queried boolean 62 /// formula. 63 Status getStatus() const { return SATCheckStatus; } 64 65 /// Returns a truth assignment to boolean values that satisfies the queried 66 /// boolean formula if available. Otherwise, an empty optional is returned. 67 llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> 68 getSolution() const { 69 return Solution; 70 } 71 72 private: 73 Result( 74 enum Status SATCheckStatus, 75 llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution) 76 : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {} 77 78 Status SATCheckStatus; 79 llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution; 80 }; 81 82 virtual ~Solver() = default; 83 84 /// Checks if the conjunction of `Vals` is satisfiable and returns the 85 /// corresponding result. 86 /// 87 /// Requirements: 88 /// 89 /// All elements in `Vals` must not be null. 90 virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0; 91 }; 92 93 } // namespace dataflow 94 } // namespace clang 95 96 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H 97