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 /// Produces 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 /// Allocates 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
98 /// Count of operands (sub-formulas) associated with Formulas of kind `K`.
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
115private:
116 Formula() = default;
117 Formula(const Formula &) = delete;
118 Formula &operator=(const Formula &) = delete;
119
120 Kind FormulaKind;
121 // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
122 unsigned Value;
123};
124
125// The default names of atoms are V0, V1 etc in order of creation.
126inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
127 return OS << 'V' << static_cast<unsigned>(A);
128}
129inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
130 F.print(OS);
131 return OS;
132}
133
134} // namespace clang::dataflow
135namespace llvm {
136template <> struct DenseMapInfo<clang::dataflow::Atom> {
137 using Atom = clang::dataflow::Atom;
138 using Underlying = std::underlying_type_t<Atom>;
139
140 static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
141 static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
142 static unsigned getHashValue(const Atom &Val) {
143 return DenseMapInfo<Underlying>::getHashValue(Val: Underlying(Val));
144 }
145 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
146};
147} // namespace llvm
148#endif
149