clang 18.0.0git
Arena.h
Go to the documentation of this file.
1//===-- Arena.h -------------------------------*- 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#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
9#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
10
14#include "llvm/ADT/StringRef.h"
15#include <vector>
16
17namespace clang::dataflow {
18
19/// The Arena owns the objects that model data within an analysis.
20/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
21class Arena {
22public:
23 Arena() : True(makeAtom()), False(makeAtom()) {}
24 Arena(const Arena &) = delete;
25 Arena &operator=(const Arena &) = delete;
26
27 /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to
28 /// the constructor, and returns a reference to it.
29 ///
30 /// The `DataflowAnalysisContext` takes ownership of the created object. The
31 /// object will be destroyed when the `DataflowAnalysisContext` is destroyed.
32 template <typename T, typename... Args>
33 std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
34 create(Args &&...args) {
35 // Note: If allocation of individual `StorageLocation`s turns out to be
36 // costly, consider creating specializations of `create<T>` for commonly
37 // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`.
38 return *cast<T>(
39 Locs.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
40 .get());
41 }
42
43 /// Creates a `T` (some subclass of `Value`), forwarding `args` to the
44 /// constructor, and returns a reference to it.
45 ///
46 /// The `DataflowAnalysisContext` takes ownership of the created object. The
47 /// object will be destroyed when the `DataflowAnalysisContext` is destroyed.
48 template <typename T, typename... Args>
49 std::enable_if_t<std::is_base_of<Value, T>::value, T &>
50 create(Args &&...args) {
51 // Note: If allocation of individual `Value`s turns out to be costly,
52 // consider creating specializations of `create<T>` for commonly used
53 // `Value` subclasses and make them use a `BumpPtrAllocator`.
54 return *cast<T>(
55 Vals.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
56 .get());
57 }
58
59 /// Creates a BoolValue wrapping a particular formula.
60 ///
61 /// Passing in the same formula will result in the same BoolValue.
62 /// FIXME: Interning BoolValues but not other Values is inconsistent.
63 /// Decide whether we want Value interning or not.
65
66 /// Creates a fresh atom and wraps in in an AtomicBoolValue.
67 /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
68 /// Stop relying on pointer identity and remove this guarantee.
70 return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
71 }
72
73 /// Creates a fresh Top boolean value.
75 // No need for deduplicating: there's no way to create aliasing Tops.
76 return create<TopBoolValue>(makeAtomRef(makeAtom()));
77 }
78
79 /// Returns a symbolic integer value that models an integer literal equal to
80 /// `Value`. These literals are the same every time.
81 /// Integer literals are not typed; the type is determined by the `Expr` that
82 /// an integer literal is associated with.
83 IntegerValue &makeIntLiteral(llvm::APInt Value);
84
85 // Factories for boolean formulas.
86 // Formulas are interned: passing the same arguments return the same result.
87 // For commutative operations like And/Or, interning ignores order.
88 // Simplifications are applied: makeOr(X, X) => X, etc.
89
90 /// Returns a formula for the conjunction of `LHS` and `RHS`.
91 const Formula &makeAnd(const Formula &LHS, const Formula &RHS);
92
93 /// Returns a formula for the disjunction of `LHS` and `RHS`.
94 const Formula &makeOr(const Formula &LHS, const Formula &RHS);
95
96 /// Returns a formula for the negation of `Val`.
97 const Formula &makeNot(const Formula &Val);
98
99 /// Returns a formula for `LHS => RHS`.
100 const Formula &makeImplies(const Formula &LHS, const Formula &RHS);
101
102 /// Returns a formula for `LHS <=> RHS`.
103 const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
104
105 /// Returns a formula for the variable A.
106 const Formula &makeAtomRef(Atom A);
107
108 /// Returns a formula for a literal true/false.
109 const Formula &makeLiteral(bool Value) {
110 return makeAtomRef(Value ? True : False);
111 }
112
113 // Parses a formula from its textual representation.
114 // This may refer to atoms that were not produced by makeAtom() yet!
116
117 /// Returns a new atomic boolean variable, distinct from any other.
118 Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
119
120 /// Creates a fresh flow condition and returns a token that identifies it. The
121 /// token can be used to perform various operations on the flow condition such
122 /// as adding constraints to it, forking it, joining it with another flow
123 /// condition, or checking implications.
125
126private:
127 llvm::BumpPtrAllocator Alloc;
128
129 // Storage for the state of a program.
130 std::vector<std::unique_ptr<StorageLocation>> Locs;
131 std::vector<std::unique_ptr<Value>> Vals;
132
133 // Indices that are used to avoid recreating the same integer literals and
134 // composite boolean values.
135 llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
136 using FormulaPair = std::pair<const Formula *, const Formula *>;
137 llvm::DenseMap<FormulaPair, const Formula *> Ands;
138 llvm::DenseMap<FormulaPair, const Formula *> Ors;
139 llvm::DenseMap<const Formula *, const Formula *> Nots;
140 llvm::DenseMap<FormulaPair, const Formula *> Implies;
141 llvm::DenseMap<FormulaPair, const Formula *> Equals;
142 llvm::DenseMap<Atom, const Formula *> AtomRefs;
143
144 llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
145 unsigned NextAtom = 0;
146
147 Atom True, False;
148};
149
150} // namespace clang::dataflow
151
152#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
The Arena owns the objects that model data within an analysis.
Definition: Arena.h:21
const Formula & makeEquals(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS <=> RHS.
Definition: Arena.cpp:73
const Formula & makeAtomRef(Atom A)
Returns a formula for the variable A.
Definition: Arena.cpp:25
Atom makeAtom()
Returns a new atomic boolean variable, distinct from any other.
Definition: Arena.h:118
IntegerValue & makeIntLiteral(llvm::APInt Value)
Returns a symbolic integer value that models an integer literal equal to Value.
Definition: Arena.cpp:84
const Formula & makeNot(const Formula &Val)
Returns a formula for the negation of Val.
Definition: Arena.cpp:55
std::enable_if_t< std::is_base_of< Value, T >::value, T & > create(Args &&...args)
Creates a T (some subclass of Value), forwarding args to the constructor, and returns a reference to ...
Definition: Arena.h:50
Atom makeFlowConditionToken()
Creates a fresh flow condition and returns a token that identifies it.
Definition: Arena.h:124
TopBoolValue & makeTopValue()
Creates a fresh Top boolean value.
Definition: Arena.h:74
const Formula & makeOr(const Formula &LHS, const Formula &RHS)
Returns a formula for the disjunction of LHS and RHS.
Definition: Arena.cpp:44
BoolValue & makeBoolValue(const Formula &)
Creates a BoolValue wrapping a particular formula.
Definition: Arena.cpp:92
const Formula & makeAnd(const Formula &LHS, const Formula &RHS)
Returns a formula for the conjunction of LHS and RHS.
Definition: Arena.cpp:33
AtomicBoolValue & makeAtomValue()
Creates a fresh atom and wraps in in an AtomicBoolValue.
Definition: Arena.h:69
const Formula & makeImplies(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS => RHS.
Definition: Arena.cpp:62
Arena(const Arena &)=delete
const Formula & makeLiteral(bool Value)
Returns a formula for a literal true/false.
Definition: Arena.h:109
llvm::Expected< const Formula & > parseFormula(llvm::StringRef)
Definition: Arena.cpp:182
std::enable_if_t< std::is_base_of< StorageLocation, T >::value, T & > create(Args &&...args)
Creates a T (some subclass of StorageLocation), forwarding args to the constructor,...
Definition: Arena.h:34
Arena & operator=(const Arena &)=delete
Models an atomic boolean.
Definition: Value.h:131
Models a boolean.
Definition: Value.h:92
Models an integer.
Definition: Value.h:158
A TopBoolValue represents a boolean that is explicitly unconstrained.
Definition: Value.h:114
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:35