clang: include/clang/Analysis/FlowSensitive/Formula.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
10#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
11
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
19#include
20
22
23
24
25
26
27
28
29
30
31
32
33
34enum class Atom : unsigned {};
35
36
37
38
39
40
41
42
43
44
45
46
47
48class Formula;
49class alignas(const Formula *) Formula {
50public:
66 Kind kind() const { return FormulaKind; }
67
70 return static_cast<Atom>(Value);
71 }
72
75 return static_cast<bool>(Value);
76 }
77
79 return kind() == Literal && static_cast<bool>(Value) == b;
80 }
81
83 return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
85 }
86
87 using AtomNames = llvm::DenseMap<Atom, std::string>;
88
89
90
91 void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
92
93
94 static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
96 unsigned Value = 0);
97
98
100 switch (K) {
103 return 0;
104 case Not:
105 return 1;
106 case And:
107 case Or:
110 return 2;
111 }
112 llvm_unreachable("Unhandled Formula::Kind enum");
113 }
114
115private:
119
120 Kind FormulaKind;
121
123};
124
125
126inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
127 return OS << 'V' << static_cast(A);
128}
129inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
131 return OS;
132}
133
134}
135namespace llvm {
136template <> struct DenseMapInfo<clang::dataflow::Atom> {
139
143 return DenseMapInfo::getHashValue(Underlying(Val));
144 }
145 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
146};
147}
148#endif
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
void print(llvm::raw_ostream &OS, const AtomNames *=nullptr) const
Produces a stable human-readable representation of this formula.
ArrayRef< const Formula * > operands() const
Definition Formula.h:82
bool isLiteral(bool b) const
Definition Formula.h:78
Atom getAtom() const
Definition Formula.h:68
llvm::DenseMap< Atom, std::string > AtomNames
Definition Formula.h:87
Kind
Definition Formula.h:51
@ Equal
True if LHS is false or RHS is true.
Definition Formula.h:64
@ Implies
True if either LHS or RHS is true.
Definition Formula.h:63
@ AtomRef
A reference to an atomic boolean variable.
Definition Formula.h:54
@ Literal
Constant true or false.
Definition Formula.h:56
@ Not
Definition Formula.h:58
@ Or
True if LHS and RHS are both true.
Definition Formula.h:62
@ And
True if its only operand is false.
Definition Formula.h:61
static const Formula & create(llvm::BumpPtrAllocator &Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value=0)
Allocates Formulas using Arena rather than calling this function directly.
bool literal() const
Definition Formula.h:73
Kind kind() const
Definition Formula.h:66
static unsigned numOperands(Kind K)
Count of operands (sub-formulas) associated with Formulas of kind K.
Definition Formula.h:99
Base class for all values computed by abstract interpretation.
Dataflow Directional Tag Classes.
Atom
Identifies an atomic boolean variable such as "V1".
Definition Formula.h:34
llvm::raw_ostream & operator<<(llvm::raw_ostream &OS, Atom A)
Definition Formula.h:126
The JSON file list parser is used to communicate input to InstallAPI.
Diagnostic wrappers for TextAPI types for error reporting.
static bool isEqual(const Atom &LHS, const Atom &RHS)
Definition Formula.h:145
static unsigned getHashValue(const Atom &Val)
Definition Formula.h:142
std::underlying_type_t< Atom > Underlying
Definition Formula.h:138
clang::dataflow::Atom Atom
Definition Formula.h:137
static Atom getTombstoneKey()
Definition Formula.h:141
static Atom getEmptyKey()
Definition Formula.h:140