1 | //===- Formula.h - Boolean formulas -----------------------------*- 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 | #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H |
10 | #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H |
11 | |
12 | #include "clang/Basic/LLVM.h" |
13 | #include "llvm/ADT/ArrayRef.h" |
14 | #include "llvm/ADT/DenseMap.h" |
15 | #include "llvm/ADT/DenseMapInfo.h" |
16 | #include "llvm/Support/Allocator.h" |
17 | #include "llvm/Support/raw_ostream.h" |
18 | #include <cassert> |
19 | #include <string> |
20 | |
21 | namespace clang::dataflow { |
22 | |
23 | /// Identifies an atomic boolean variable such as "V1". |
24 | /// |
25 | /// This often represents an assertion that is interesting to the analysis but |
26 | /// cannot immediately be proven true or false. For example: |
27 | /// - V1 may mean "the program reaches this point", |
28 | /// - V2 may mean "the parameter was null" |
29 | /// |
30 | /// We can use these variables in formulas to describe relationships we know |
31 | /// to be true: "if the parameter was null, the program reaches this point". |
32 | /// We also express hypotheses as formulas, and use a SAT solver to check |
33 | /// whether they are consistent with the known facts. |
34 | enum class Atom : unsigned {}; |
35 | |
36 | /// A boolean expression such as "true" or "V1 & !V2". |
37 | /// Expressions may refer to boolean atomic variables. These should take a |
38 | /// consistent true/false value across the set of formulas being considered. |
39 | /// |
40 | /// (Formulas are always expressions in terms of boolean variables rather than |
41 | /// e.g. integers because our underlying model is SAT rather than e.g. SMT). |
42 | /// |
43 | /// Simple formulas such as "true" and "V1" are self-contained. |
44 | /// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or' |
45 | /// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as |
46 | /// trailing objects. |
47 | /// For this reason, Formulas are Arena-allocated and over-aligned. |
48 | class Formula; |
49 | class alignas(const Formula *) Formula { |
50 | public: |
51 | enum Kind : unsigned { |
52 | /// A reference to an atomic boolean variable. |
53 | /// We name these e.g. "V3", where 3 == atom identity == Value. |
54 | AtomRef, |
55 | /// Constant true or false. |
56 | Literal, |
57 | |
58 | Not, /// True if its only operand is false |
59 | |
60 | // These kinds connect two operands LHS and RHS |
61 | And, /// True if LHS and RHS are both true |
62 | Or, /// True if either LHS or RHS is true |
63 | Implies, /// True if LHS is false or RHS is true |
64 | Equal, /// True if LHS and RHS have the same truth value |
65 | }; |
66 | Kind kind() const { return FormulaKind; } |
67 | |
68 | Atom getAtom() const { |
69 | assert(kind() == AtomRef); |
70 | return static_cast<Atom>(Value); |
71 | } |
72 | |
73 | bool literal() const { |
74 | assert(kind() == Literal); |
75 | return static_cast<bool>(Value); |
76 | } |
77 | |
78 | bool isLiteral(bool b) const { |
79 | return kind() == Literal && static_cast<bool>(Value) == b; |
80 | } |
81 | |
82 | ArrayRef<const Formula *> operands() const { |
83 | return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), |
84 | numOperands(K: kind())); |
85 | } |
86 | |
87 | using AtomNames = llvm::DenseMap<Atom, std::string>; |
88 | // Produce a stable human-readable representation of this formula. |
89 | // For example: (V3 | !(V1 & V2)) |
90 | // If AtomNames is provided, these override the default V0, V1... names. |
91 | void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const; |
92 | |
93 | // Allocate Formulas using Arena rather than calling this function directly. |
94 | static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, |
95 | ArrayRef<const Formula *> Operands, |
96 | unsigned Value = 0); |
97 | |
98 | private: |
99 | Formula() = default; |
100 | Formula(const Formula &) = delete; |
101 | Formula &operator=(const Formula &) = delete; |
102 | |
103 | static unsigned numOperands(Kind K) { |
104 | switch (K) { |
105 | case AtomRef: |
106 | case Literal: |
107 | return 0; |
108 | case Not: |
109 | return 1; |
110 | case And: |
111 | case Or: |
112 | case Implies: |
113 | case Equal: |
114 | return 2; |
115 | } |
116 | llvm_unreachable("Unhandled Formula::Kind enum" ); |
117 | } |
118 | |
119 | Kind FormulaKind; |
120 | // Some kinds of formula have scalar values, e.g. AtomRef's atom number. |
121 | unsigned Value; |
122 | }; |
123 | |
124 | // The default names of atoms are V0, V1 etc in order of creation. |
125 | inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) { |
126 | return OS << 'V' << static_cast<unsigned>(A); |
127 | } |
128 | inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) { |
129 | F.print(OS); |
130 | return OS; |
131 | } |
132 | |
133 | } // namespace clang::dataflow |
134 | namespace llvm { |
135 | template <> struct DenseMapInfo<clang::dataflow::Atom> { |
136 | using Atom = clang::dataflow::Atom; |
137 | using Underlying = std::underlying_type_t<Atom>; |
138 | |
139 | static inline Atom getEmptyKey() { return Atom(Underlying(-1)); } |
140 | static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); } |
141 | static unsigned getHashValue(const Atom &Val) { |
142 | return DenseMapInfo<Underlying>::getHashValue(Val: Underlying(Val)); |
143 | } |
144 | static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; } |
145 | }; |
146 | } // namespace llvm |
147 | #endif |
148 | |