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