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 <optional>
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     std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
68     getSolution() const {
69       return Solution;
70     }
71 
72   private:
73     Result(
74         enum Status SATCheckStatus,
75         std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
76         : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
77 
78     Status SATCheckStatus;
79     std::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