clang 18.0.0git
Formula.h
Go to the documentation of this file.
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
21namespace 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.
34enum 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.
48class Formula;
49class alignas(const Formula *) Formula {
50public:
51 enum Kind : unsigned {
52 /// A reference to an atomic boolean variable.
53 /// We name these e.g. "V3", where 3 == atom identity == Value.
55 /// Constant true or false.
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 };
66 Kind kind() const { return FormulaKind; }
67
68 Atom getAtom() const {
69 assert(kind() == AtomRef);
70 return static_cast<Atom>(Value);
71 }
72
73 bool literal() const {
74 assert(kind() == Literal);
75 return static_cast<bool>(Value);
76 }
77
79 return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
80 numOperands(kind()));
81 }
82
83 using AtomNames = llvm::DenseMap<Atom, std::string>;
84 // Produce a stable human-readable representation of this formula.
85 // For example: (V3 | !(V1 & V2))
86 // If AtomNames is provided, these override the default V0, V1... names.
87 void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
88
89 // Allocate Formulas using Arena rather than calling this function directly.
90 static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
92 unsigned Value = 0);
93
94private:
95 Formula() = default;
96 Formula(const Formula &) = delete;
97 Formula &operator=(const Formula &) = delete;
98
99 static unsigned numOperands(Kind K) {
100 switch (K) {
101 case AtomRef:
102 case Literal:
103 return 0;
104 case Not:
105 return 1;
106 case And:
107 case Or:
108 case Implies:
109 case Equal:
110 return 2;
111 }
112 llvm_unreachable("Unhandled Formula::Kind enum");
113 }
114
115 Kind FormulaKind;
116 // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
117 unsigned Value;
118};
119
120// The default names of atoms are V0, V1 etc in order of creation.
121inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
122 return OS << 'V' << static_cast<unsigned>(A);
123}
124inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
125 F.print(OS);
126 return OS;
127}
128
129} // namespace clang::dataflow
130namespace llvm {
131template <> struct DenseMapInfo<clang::dataflow::Atom> {
133 using Underlying = std::underlying_type_t<Atom>;
134
135 static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
136 static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
137 static unsigned getHashValue(const Atom &Val) {
138 return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
139 }
140 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
141};
142} // namespace llvm
143#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
Definition: Formula.cpp:58
ArrayRef< const Formula * > operands() const
Definition: Formula.h:78
Atom getAtom() const
Definition: Formula.h:68
llvm::DenseMap< Atom, std::string > AtomNames
Definition: Formula.h:83
@ 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
@ 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)
Definition: Formula.cpp:20
bool literal() const
Definition: Formula.h:73
Kind kind() const
Definition: Formula.h:66
Base class for all values computed by abstract interpretation.
Definition: Value.h:33
Dataflow Directional Tag Classes.
Definition: Arena.h:17
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:121
uint32_t Literal
Literals are represented as positive integers.
YAML serialization mapping.
Definition: Dominators.h:30
static bool isEqual(const Atom &LHS, const Atom &RHS)
Definition: Formula.h:140
static unsigned getHashValue(const Atom &Val)
Definition: Formula.h:137
std::underlying_type_t< Atom > Underlying
Definition: Formula.h:133