/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
Line | Count | Source (jump to first uncovered line) |
1 | | //===-- DataflowAnalysisContext.cpp -----------------------------*- 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 | | // This file defines a DataflowAnalysisContext class that owns objects that |
10 | | // encompass the state of a program and stores context that is used during |
11 | | // dataflow analysis. |
12 | | // |
13 | | //===----------------------------------------------------------------------===// |
14 | | |
15 | | #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h" |
16 | | #include "clang/AST/ExprCXX.h" |
17 | | #include "clang/Analysis/FlowSensitive/Value.h" |
18 | | #include <cassert> |
19 | | #include <memory> |
20 | | #include <utility> |
21 | | |
22 | | namespace clang { |
23 | | namespace dataflow { |
24 | | |
25 | | static std::pair<BoolValue *, BoolValue *> |
26 | 382k | makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) { |
27 | 382k | auto Res = std::make_pair(&LHS, &RHS); |
28 | 382k | if (&RHS < &LHS) |
29 | 91.1k | std::swap(Res.first, Res.second); |
30 | 382k | return Res; |
31 | 382k | } |
32 | | |
33 | | BoolValue & |
34 | | DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS, |
35 | 75 | BoolValue &RHS) { |
36 | 75 | if (&LHS == &RHS) |
37 | 1 | return LHS; |
38 | | |
39 | 74 | auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), |
40 | 74 | nullptr); |
41 | 74 | if (Res.second) |
42 | 60 | Res.first->second = |
43 | 60 | &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS)); |
44 | 74 | return *Res.first->second; |
45 | 75 | } |
46 | | |
47 | | BoolValue & |
48 | | DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS, |
49 | 382k | BoolValue &RHS) { |
50 | 382k | if (&LHS == &RHS) |
51 | 1 | return LHS; |
52 | | |
53 | 382k | auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), |
54 | 382k | nullptr); |
55 | 382k | if (Res.second) |
56 | 382k | Res.first->second = |
57 | 382k | &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS)); |
58 | 382k | return *Res.first->second; |
59 | 382k | } |
60 | | |
61 | 361k | BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) { |
62 | 361k | auto Res = NegationVals.try_emplace(&Val, nullptr); |
63 | 361k | if (Res.second) |
64 | 202k | Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val)); |
65 | 361k | return *Res.first->second; |
66 | 361k | } |
67 | | |
68 | 201k | AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() { |
69 | 201k | AtomicBoolValue &Token = createAtomicBoolValue(); |
70 | 201k | FlowConditionRemainingConjuncts[&Token] = {}; |
71 | 201k | FlowConditionFirstConjuncts[&Token] = &Token; |
72 | 201k | return Token; |
73 | 201k | } |
74 | | |
75 | | void DataflowAnalysisContext::addFlowConditionConstraint( |
76 | 180k | AtomicBoolValue &Token, BoolValue &Constraint) { |
77 | 180k | FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue( |
78 | 180k | Constraint, getOrCreateNegationValue(Token))); |
79 | 180k | FlowConditionFirstConjuncts[&Token] = |
80 | 180k | &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token], |
81 | 180k | getOrCreateNegationValue(Constraint)); |
82 | 180k | } |
83 | | |
84 | | AtomicBoolValue & |
85 | 157k | DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) { |
86 | 157k | auto &ForkToken = makeFlowConditionToken(); |
87 | 157k | FlowConditionDeps[&ForkToken].insert(&Token); |
88 | 157k | addFlowConditionConstraint(ForkToken, Token); |
89 | 157k | return ForkToken; |
90 | 157k | } |
91 | | |
92 | | AtomicBoolValue & |
93 | | DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, |
94 | 22.0k | AtomicBoolValue &SecondToken) { |
95 | 22.0k | auto &Token = makeFlowConditionToken(); |
96 | 22.0k | FlowConditionDeps[&Token].insert(&FirstToken); |
97 | 22.0k | FlowConditionDeps[&Token].insert(&SecondToken); |
98 | 22.0k | addFlowConditionConstraint( |
99 | 22.0k | Token, getOrCreateDisjunctionValue(FirstToken, SecondToken)); |
100 | 22.0k | return Token; |
101 | 22.0k | } |
102 | | |
103 | | bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, |
104 | 422 | BoolValue &Val) { |
105 | | // Returns true if and only if truth assignment of the flow condition implies |
106 | | // that `Val` is also true. We prove whether or not this property holds by |
107 | | // reducing the problem to satisfiability checking. In other words, we attempt |
108 | | // to show that assuming `Val` is false makes the constraints induced by the |
109 | | // flow condition unsatisfiable. |
110 | 422 | llvm::DenseSet<BoolValue *> Constraints = { |
111 | 422 | &Token, |
112 | 422 | &getBoolLiteralValue(true), |
113 | 422 | &getOrCreateNegationValue(getBoolLiteralValue(false)), |
114 | 422 | &getOrCreateNegationValue(Val), |
115 | 422 | }; |
116 | 422 | llvm::DenseSet<AtomicBoolValue *> VisitedTokens; |
117 | 422 | addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); |
118 | 422 | return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable; |
119 | 422 | } |
120 | | |
121 | 5 | bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { |
122 | | // Returns true if and only if we cannot prove that the flow condition can |
123 | | // ever be false. |
124 | 5 | llvm::DenseSet<BoolValue *> Constraints = { |
125 | 5 | &getBoolLiteralValue(true), |
126 | 5 | &getOrCreateNegationValue(getBoolLiteralValue(false)), |
127 | 5 | &getOrCreateNegationValue(Token), |
128 | 5 | }; |
129 | 5 | llvm::DenseSet<AtomicBoolValue *> VisitedTokens; |
130 | 5 | addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); |
131 | 5 | return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable; |
132 | 5 | } |
133 | | |
134 | | void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( |
135 | | AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, |
136 | 2.16k | llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const { |
137 | 2.16k | auto Res = VisitedTokens.insert(&Token); |
138 | 2.16k | if (!Res.second) |
139 | 28 | return; |
140 | | |
141 | 2.13k | auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token); |
142 | 2.13k | if (FirstConjunctIT != FlowConditionFirstConjuncts.end()) |
143 | 2.13k | Constraints.insert(FirstConjunctIT->second); |
144 | 2.13k | auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token); |
145 | 2.13k | if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end()) |
146 | 2.13k | Constraints.insert(RemainingConjunctsIT->second.begin(), |
147 | 2.13k | RemainingConjunctsIT->second.end()); |
148 | | |
149 | 2.13k | auto DepsIT = FlowConditionDeps.find(&Token); |
150 | 2.13k | if (DepsIT != FlowConditionDeps.end()) { |
151 | 1.70k | for (AtomicBoolValue *DepToken : DepsIT->second) |
152 | 1.74k | addTransitiveFlowConditionConstraints(*DepToken, Constraints, |
153 | 1.74k | VisitedTokens); |
154 | 1.70k | } |
155 | 2.13k | } |
156 | | |
157 | | } // namespace dataflow |
158 | | } // namespace clang |
159 | | |
160 | | using namespace clang; |
161 | | |
162 | 9.59k | const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) { |
163 | 9.59k | const Expr *Current = &E; |
164 | 9.59k | if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) { |
165 | 278 | Current = EWC->getSubExpr(); |
166 | 278 | assert(Current != nullptr); |
167 | 278 | } |
168 | 0 | Current = Current->IgnoreParens(); |
169 | 9.59k | assert(Current != nullptr); |
170 | 0 | return *Current; |
171 | 9.59k | } |
172 | | |
173 | 48 | const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) { |
174 | 48 | if (auto *E = dyn_cast<Expr>(&S)) |
175 | 48 | return ignoreCFGOmittedNodes(*E); |
176 | 0 | return S; |
177 | 48 | } |