| //===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===// |
| // |
| // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
| // See https://llvm.org/LICENSE.txt for license information. |
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
| // |
| //===----------------------------------------------------------------------===// |
| |
| #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H |
| #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H |
| |
| #include "clang/Basic/LLVM.h" |
| #include "llvm/ADT/ArrayRef.h" |
| #include "llvm/ADT/DenseMap.h" |
| #include "llvm/ADT/DenseMapInfo.h" |
| #include "llvm/Support/Allocator.h" |
| #include "llvm/Support/raw_ostream.h" |
| #include <cassert> |
| #include <string> |
| |
| namespace clang::dataflow { |
| |
| /// Identifies an atomic boolean variable such as "V1". |
| /// |
| /// This often represents an assertion that is interesting to the analysis but |
| /// cannot immediately be proven true or false. For example: |
| /// - V1 may mean "the program reaches this point", |
| /// - V2 may mean "the parameter was null" |
| /// |
| /// We can use these variables in formulas to describe relationships we know |
| /// to be true: "if the parameter was null, the program reaches this point". |
| /// We also express hypotheses as formulas, and use a SAT solver to check |
| /// whether they are consistent with the known facts. |
| enum class Atom : unsigned {}; |
| |
| /// A boolean expression such as "true" or "V1 & !V2". |
| /// Expressions may refer to boolean atomic variables. These should take a |
| /// consistent true/false value across the set of formulas being considered. |
| /// |
| /// (Formulas are always expressions in terms of boolean variables rather than |
| /// e.g. integers because our underlying model is SAT rather than e.g. SMT). |
| /// |
| /// Simple formulas such as "true" and "V1" are self-contained. |
| /// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or' |
| /// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as |
| /// trailing objects. |
| /// For this reason, Formulas are Arena-allocated and over-aligned. |
| class Formula; |
| class alignas(const Formula *) Formula { |
| public: |
| enum Kind : unsigned { |
| /// A reference to an atomic boolean variable. |
| /// We name these e.g. "V3", where 3 == atom identity == Value. |
| AtomRef, |
| /// Constant true or false. |
| Literal, |
| |
| Not, /// True if its only operand is false |
| |
| // These kinds connect two operands LHS and RHS |
| And, /// True if LHS and RHS are both true |
| Or, /// True if either LHS or RHS is true |
| Implies, /// True if LHS is false or RHS is true |
| Equal, /// True if LHS and RHS have the same truth value |
| }; |
| Kind kind() const { return FormulaKind; } |
| |
| Atom getAtom() const { |
| assert(kind() == AtomRef); |
| return static_cast<Atom>(Value); |
| } |
| |
| bool literal() const { |
| assert(kind() == Literal); |
| return static_cast<bool>(Value); |
| } |
| |
| bool isLiteral(bool b) const { |
| return kind() == Literal && static_cast<bool>(Value) == b; |
| } |
| |
| ArrayRef<const Formula *> operands() const { |
| return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), |
| numOperands(kind())); |
| } |
| |
| using AtomNames = llvm::DenseMap<Atom, std::string>; |
| // Produce a stable human-readable representation of this formula. |
| // For example: (V3 | !(V1 & V2)) |
| // If AtomNames is provided, these override the default V0, V1... names. |
| void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const; |
| |
| // Allocate Formulas using Arena rather than calling this function directly. |
| static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, |
| ArrayRef<const Formula *> Operands, |
| unsigned Value = 0); |
| |
| private: |
| Formula() = default; |
| Formula(const Formula &) = delete; |
| Formula &operator=(const Formula &) = delete; |
| |
| static unsigned numOperands(Kind K) { |
| switch (K) { |
| case AtomRef: |
| case Literal: |
| return 0; |
| case Not: |
| return 1; |
| case And: |
| case Or: |
| case Implies: |
| case Equal: |
| return 2; |
| } |
| llvm_unreachable("Unhandled Formula::Kind enum"); |
| } |
| |
| Kind FormulaKind; |
| // Some kinds of formula have scalar values, e.g. AtomRef's atom number. |
| unsigned Value; |
| }; |
| |
| // The default names of atoms are V0, V1 etc in order of creation. |
| inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) { |
| return OS << 'V' << static_cast<unsigned>(A); |
| } |
| inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) { |
| F.print(OS); |
| return OS; |
| } |
| |
| } // namespace clang::dataflow |
| namespace llvm { |
| template <> struct DenseMapInfo<clang::dataflow::Atom> { |
| using Atom = clang::dataflow::Atom; |
| using Underlying = std::underlying_type_t<Atom>; |
| |
| static inline Atom getEmptyKey() { return Atom(Underlying(-1)); } |
| static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); } |
| static unsigned getHashValue(const Atom &Val) { |
| return DenseMapInfo<Underlying>::getHashValue(Underlying(Val)); |
| } |
| static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; } |
| }; |
| } // namespace llvm |
| #endif |