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