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 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
27   auto Res = std::make_pair(&LHS, &RHS);
28   if (&RHS < &LHS)
29     std::swap(Res.first, Res.second);
30   return Res;
31 }
32 
33 BoolValue &DataflowAnalysisContext::getOrCreateConjunction(BoolValue &LHS,
34                                                            BoolValue &RHS) {
35   if (&LHS == &RHS)
36     return LHS;
37 
38   auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
39                                          nullptr);
40   if (Res.second)
41     Res.first->second =
42         &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
43   return *Res.first->second;
44 }
45 
46 BoolValue &DataflowAnalysisContext::getOrCreateDisjunction(BoolValue &LHS,
47                                                            BoolValue &RHS) {
48   if (&LHS == &RHS)
49     return LHS;
50 
51   auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
52                                          nullptr);
53   if (Res.second)
54     Res.first->second =
55         &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
56   return *Res.first->second;
57 }
58 
59 BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
60   auto Res = NegationVals.try_emplace(&Val, nullptr);
61   if (Res.second)
62     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
63   return *Res.first->second;
64 }
65 
66 BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS,
67                                                            BoolValue &RHS) {
68   return &LHS == &RHS ? getBoolLiteralValue(true)
69                       : getOrCreateDisjunction(getOrCreateNegation(LHS), RHS);
70 }
71 
72 BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS,
73                                                    BoolValue &RHS) {
74   return &LHS == &RHS
75              ? getBoolLiteralValue(true)
76              : getOrCreateConjunction(getOrCreateImplication(LHS, RHS),
77                                       getOrCreateImplication(RHS, LHS));
78 }
79 
80 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
81   return createAtomicBoolValue();
82 }
83 
84 void DataflowAnalysisContext::addFlowConditionConstraint(
85     AtomicBoolValue &Token, BoolValue &Constraint) {
86   auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
87   if (!Res.second) {
88     Res.first->second = &getOrCreateConjunction(*Res.first->second, Constraint);
89   }
90 }
91 
92 AtomicBoolValue &
93 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
94   auto &ForkToken = makeFlowConditionToken();
95   FlowConditionDeps[&ForkToken].insert(&Token);
96   addFlowConditionConstraint(ForkToken, Token);
97   return ForkToken;
98 }
99 
100 AtomicBoolValue &
101 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
102                                             AtomicBoolValue &SecondToken) {
103   auto &Token = makeFlowConditionToken();
104   FlowConditionDeps[&Token].insert(&FirstToken);
105   FlowConditionDeps[&Token].insert(&SecondToken);
106   addFlowConditionConstraint(Token,
107                              getOrCreateDisjunction(FirstToken, SecondToken));
108   return Token;
109 }
110 
111 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
112                                                    BoolValue &Val) {
113   // Returns true if and only if truth assignment of the flow condition implies
114   // that `Val` is also true. We prove whether or not this property holds by
115   // reducing the problem to satisfiability checking. In other words, we attempt
116   // to show that assuming `Val` is false makes the constraints induced by the
117   // flow condition unsatisfiable.
118   llvm::DenseSet<BoolValue *> Constraints = {
119       &Token,
120       &getBoolLiteralValue(true),
121       &getOrCreateNegation(getBoolLiteralValue(false)),
122       &getOrCreateNegation(Val),
123   };
124   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
125   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
126   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
127 }
128 
129 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
130   // Returns true if and only if we cannot prove that the flow condition can
131   // ever be false.
132   llvm::DenseSet<BoolValue *> Constraints = {
133       &getBoolLiteralValue(true),
134       &getOrCreateNegation(getBoolLiteralValue(false)),
135       &getOrCreateNegation(Token),
136   };
137   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
138   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
139   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
140 }
141 
142 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
143     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
144     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
145   auto Res = VisitedTokens.insert(&Token);
146   if (!Res.second)
147     return;
148 
149   auto ConstraintsIT = FlowConditionConstraints.find(&Token);
150   if (ConstraintsIT == FlowConditionConstraints.end()) {
151     Constraints.insert(&Token);
152   } else {
153     // Bind flow condition token via `iff` to its set of constraints:
154     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
155     Constraints.insert(&getOrCreateIff(Token, *ConstraintsIT->second));
156   }
157 
158   auto DepsIT = FlowConditionDeps.find(&Token);
159   if (DepsIT != FlowConditionDeps.end()) {
160     for (AtomicBoolValue *DepToken : DepsIT->second) {
161       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
162                                             VisitedTokens);
163     }
164   }
165 }
166 
167 } // namespace dataflow
168 } // namespace clang
169 
170 using namespace clang;
171 
172 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
173   const Expr *Current = &E;
174   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {
175     Current = EWC->getSubExpr();
176     assert(Current != nullptr);
177   }
178   Current = Current->IgnoreParens();
179   assert(Current != nullptr);
180   return *Current;
181 }
182 
183 const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) {
184   if (auto *E = dyn_cast<Expr>(&S))
185     return ignoreCFGOmittedNodes(*E);
186   return S;
187 }
188