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.
54 AtomRef,
55 /// Constant true or false.
56 Literal,
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
78 bool isLiteral(bool b) const {
79 return kind() == Literal && static_cast<bool>(Value) == b;
80 }
81
82 ArrayRef<const Formula *> operands() const {
83 return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
84 numOperands(K: kind()));
85 }
86
87 using AtomNames = llvm::DenseMap<Atom, std::string>;
88 // Produce a stable human-readable representation of this formula.
89 // For example: (V3 | !(V1 & V2))
90 // If AtomNames is provided, these override the default V0, V1... names.
91 void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
92
93 // Allocate Formulas using Arena rather than calling this function directly.
94 static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
95 ArrayRef<const Formula *> Operands,
96 unsigned Value = 0);
97
98private:
99 Formula() = default;
100 Formula(const Formula &) = delete;
101 Formula &operator=(const Formula &) = delete;
102
103 static unsigned numOperands(Kind K) {
104 switch (K) {
105 case AtomRef:
106 case Literal:
107 return 0;
108 case Not:
109 return 1;
110 case And:
111 case Or:
112 case Implies:
113 case Equal:
114 return 2;
115 }
116 llvm_unreachable("Unhandled Formula::Kind enum");
117 }
118
119 Kind FormulaKind;
120 // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
121 unsigned Value;
122};
123
124// The default names of atoms are V0, V1 etc in order of creation.
125inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
126 return OS << 'V' << static_cast<unsigned>(A);
127}
128inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
129 F.print(OS);
130 return OS;
131}
132
133} // namespace clang::dataflow
134namespace llvm {
135template <> struct DenseMapInfo<clang::dataflow::Atom> {
136 using Atom = clang::dataflow::Atom;
137 using Underlying = std::underlying_type_t<Atom>;
138
139 static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
140 static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
141 static unsigned getHashValue(const Atom &Val) {
142 return DenseMapInfo<Underlying>::getHashValue(Val: Underlying(Val));
143 }
144 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
145};
146} // namespace llvm
147#endif
148

source code of clang/include/clang/Analysis/FlowSensitive/Formula.h