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;
alignas(const 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(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(Underlying(Val));
143 }
144 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
145 };
146 } // namespace llvm
147 #endif
148