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 Solver::Result
112 DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
113   Constraints.insert(&getBoolLiteralValue(true));
114   Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
115   return S->solve(std::move(Constraints));
116 }
117 
118 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
119                                                    BoolValue &Val) {
120   // Returns true if and only if truth assignment of the flow condition implies
121   // that `Val` is also true. We prove whether or not this property holds by
122   // reducing the problem to satisfiability checking. In other words, we attempt
123   // to show that assuming `Val` is false makes the constraints induced by the
124   // flow condition unsatisfiable.
125   llvm::DenseSet<BoolValue *> Constraints = {&Token, &getOrCreateNegation(Val)};
126   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
127   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
128   return isUnsatisfiable(std::move(Constraints));
129 }
130 
131 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
132   // Returns true if and only if we cannot prove that the flow condition can
133   // ever be false.
134   llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
135   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
136   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
137   return isUnsatisfiable(std::move(Constraints));
138 }
139 
140 bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
141                                                    BoolValue &Val2) {
142   llvm::DenseSet<BoolValue *> Constraints = {
143       &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
144   return isUnsatisfiable(Constraints);
145 }
146 
147 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
148     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
149     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
150   auto Res = VisitedTokens.insert(&Token);
151   if (!Res.second)
152     return;
153 
154   auto ConstraintsIT = FlowConditionConstraints.find(&Token);
155   if (ConstraintsIT == FlowConditionConstraints.end()) {
156     Constraints.insert(&Token);
157   } else {
158     // Bind flow condition token via `iff` to its set of constraints:
159     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
160     Constraints.insert(&getOrCreateIff(Token, *ConstraintsIT->second));
161   }
162 
163   auto DepsIT = FlowConditionDeps.find(&Token);
164   if (DepsIT != FlowConditionDeps.end()) {
165     for (AtomicBoolValue *DepToken : DepsIT->second) {
166       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
167                                             VisitedTokens);
168     }
169   }
170 }
171 
172 } // namespace dataflow
173 } // namespace clang
174 
175 using namespace clang;
176 
177 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
178   const Expr *Current = &E;
179   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {
180     Current = EWC->getSubExpr();
181     assert(Current != nullptr);
182   }
183   Current = Current->IgnoreParens();
184   assert(Current != nullptr);
185   return *Current;
186 }
187 
188 const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) {
189   if (auto *E = dyn_cast<Expr>(&S))
190     return ignoreCFGOmittedNodes(*E);
191   return S;
192 }
193