Analysis/FlowSensitive/Formula.h

0001 //===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008
0009 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
0010 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
0011
0012 #include "clang/Basic/LLVM.h"
0013 #include "llvm/ADT/ArrayRef.h"
0014 #include "llvm/ADT/DenseMap.h"
0015 #include "llvm/ADT/DenseMapInfo.h"
0016 #include "llvm/Support/Allocator.h"
0017 #include "llvm/Support/raw_ostream.h"
0018 #include <cassert>
0019 #include <string>
0020
0021 namespace clang::dataflow {
0022
0023 /// Identifies an atomic boolean variable such as "V1".
0024 ///
0025 /// This often represents an assertion that is interesting to the analysis but
0026 /// cannot immediately be proven true or false. For example:
0027 /// - V1 may mean "the program reaches this point",
0028 /// - V2 may mean "the parameter was null"
0029 ///
0030 /// We can use these variables in formulas to describe relationships we know
0031 /// to be true: "if the parameter was null, the program reaches this point".
0032 /// We also express hypotheses as formulas, and use a SAT solver to check
0033 /// whether they are consistent with the known facts.
0034 enum class Atom : unsigned {};
0035
0036 /// A boolean expression such as "true" or "V1 & !V2".
0037 /// Expressions may refer to boolean atomic variables. These should take a
0038 /// consistent true/false value across the set of formulas being considered.
0039 ///
0040 /// (Formulas are always expressions in terms of boolean variables rather than
0041 /// e.g. integers because our underlying model is SAT rather than e.g. SMT).
0042 ///
0043 /// Simple formulas such as "true" and "V1" are self-contained.
0044 /// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
0045 /// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
0046 /// trailing objects.
0047 /// For this reason, Formulas are Arena-allocated and over-aligned.
0048 class Formula;
0049 class alignas(const Formula *) Formula {
0050 public:
0051   enum Kind : unsigned {
0052     /// A reference to an atomic boolean variable.
0053     /// We name these e.g. "V3", where 3 == atom identity == Value.
0054     AtomRef,
0055     /// Constant true or false.
0056     Literal,
0057
0058     Not, /// True if its only operand is false
0059
0060     // These kinds connect two operands LHS and RHS
0061     And,     /// True if LHS and RHS are both true
0062     Or,      /// True if either LHS or RHS is true
0063     Implies, /// True if LHS is false or RHS is true
0064     Equal,   /// True if LHS and RHS have the same truth value
0065   };
0066   Kind kind() const { return FormulaKind; }
0067
0068   Atom getAtom() const {
0069     assert(kind() == AtomRef);
0070     return static_cast<Atom>(Value);
0071   }
0072
0073   bool literal() const {
0074     assert(kind() == Literal);
0075     return static_cast<bool>(Value);
0076   }
0077
0078   bool isLiteral(bool b) const {
0079     return kind() == Literal && static_cast<bool>(Value) == b;
0080   }
0081
0082   ArrayRef<const Formula *> operands() const {
0083     return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
0084                     numOperands(kind()));
0085   }
0086
0087   using AtomNames = llvm::DenseMap<Atom, std::string>;
0088   // Produce a stable human-readable representation of this formula.
0089   // For example: (V3 | !(V1 & V2))
0090   // If AtomNames is provided, these override the default V0, V1... names.
0091   void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
0092
0093   // Allocate Formulas using Arena rather than calling this function directly.
0094   static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
0095                                ArrayRef<const Formula *> Operands,
0096                                unsigned Value = 0);
0097
0098 private:
0099   Formula() = default;
0100   Formula(const Formula &) = delete;
0101   Formula &operator=(const Formula &) = delete;
0102
0103   static unsigned numOperands(Kind K) {
0104     switch (K) {
0105     case AtomRef:
0106     case Literal:
0107       return 0;
0108     case Not:
0109       return 1;
0110     case And:
0111     case Or:
0112     case Implies:
0113     case Equal:
0114       return 2;
0115     }
0116     llvm_unreachable("Unhandled Formula::Kind enum");
0117   }
0118
0119   Kind FormulaKind;
0120   // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
0121   unsigned Value;
0122 };
0123
0124 // The default names of atoms are V0, V1 etc in order of creation.
0125 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
0126   return OS << 'V' << static_cast<unsigned>(A);
0127 }
0128 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
0129   F.print(OS);
0130   return OS;
0131 }
0132
0133 } // namespace clang::dataflow
0134 namespace llvm {
0135 template <> struct DenseMapInfo<clang::dataflow::Atom> {
0136   using Atom = clang::dataflow::Atom;
0137   using Underlying = std::underlying_type_t<Atom>;
0138
0139   static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
0140   static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
0141   static unsigned getHashValue(const Atom &Val) {
0142     return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
0143   }
0144   static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
0145 };
0146 } // namespace llvm
0147 #endif