/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/Analysis/FlowSensitive/Solver.h
Line | Count | Source (jump to first uncovered line) |
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 | 337 | Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) { |
50 | 337 | return Result(Status::Satisfiable, std::move(Solution)); |
51 | 337 | } |
52 | | |
53 | | /// Constructs a result indicating that the queried boolean formula is |
54 | | /// unsatisfiable. |
55 | 379 | 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 | 0 | static Result TimedOut() { return Result(Status::TimedOut, {}); } |
60 | | |
61 | | /// Returns the status of satisfiability checking on the queried boolean |
62 | | /// formula. |
63 | 716 | 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 | 28 | getSolution() const { |
69 | 28 | return Solution; |
70 | 28 | } |
71 | | |
72 | | private: |
73 | | Result( |
74 | | enum Status SATCheckStatus, |
75 | | llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution) |
76 | 716 | : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {} |
77 | | |
78 | | Status SATCheckStatus; |
79 | | llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution; |
80 | | }; |
81 | | |
82 | 447 | 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 |