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 }; kind()66 Kind kind() const { return FormulaKind; } 67 getAtom()68 Atom getAtom() const { 69 assert(kind() == AtomRef); 70 return static_cast<Atom>(Value); 71 } 72 literal()73 bool literal() const { 74 assert(kind() == Literal); 75 return static_cast<bool>(Value); 76 } 77 isLiteral(bool b)78 bool isLiteral(bool b) const { 79 return kind() == Literal && static_cast<bool>(Value) == b; 80 } 81 operands()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 numOperands(Kind K)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