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 &
34 DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
35                                                      BoolValue &RHS) {
36   if (&LHS == &RHS)
37     return LHS;
38 
39   auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
40                                          nullptr);
41   if (Res.second)
42     Res.first->second =
43         &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
44   return *Res.first->second;
45 }
46 
47 BoolValue &
48 DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
49                                                      BoolValue &RHS) {
50   if (&LHS == &RHS)
51     return LHS;
52 
53   auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
54                                          nullptr);
55   if (Res.second)
56     Res.first->second =
57         &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
58   return *Res.first->second;
59 }
60 
61 BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
62   auto Res = NegationVals.try_emplace(&Val, nullptr);
63   if (Res.second)
64     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
65   return *Res.first->second;
66 }
67 
68 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
69   AtomicBoolValue &Token = createAtomicBoolValue();
70   FlowConditionRemainingConjuncts[&Token] = {};
71   FlowConditionFirstConjuncts[&Token] = &Token;
72   return Token;
73 }
74 
75 void DataflowAnalysisContext::addFlowConditionConstraint(
76     AtomicBoolValue &Token, BoolValue &Constraint) {
77   FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(
78       Constraint, getOrCreateNegationValue(Token)));
79   FlowConditionFirstConjuncts[&Token] =
80       &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],
81                                    getOrCreateNegationValue(Constraint));
82 }
83 
84 AtomicBoolValue &
85 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
86   auto &ForkToken = makeFlowConditionToken();
87   FlowConditionDeps[&ForkToken].insert(&Token);
88   addFlowConditionConstraint(ForkToken, Token);
89   return ForkToken;
90 }
91 
92 AtomicBoolValue &
93 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
94                                             AtomicBoolValue &SecondToken) {
95   auto &Token = makeFlowConditionToken();
96   FlowConditionDeps[&Token].insert(&FirstToken);
97   FlowConditionDeps[&Token].insert(&SecondToken);
98   addFlowConditionConstraint(
99       Token, getOrCreateDisjunctionValue(FirstToken, SecondToken));
100   return Token;
101 }
102 
103 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
104                                                    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   llvm::DenseSet<BoolValue *> Constraints = {
111       &Token,
112       &getBoolLiteralValue(true),
113       &getOrCreateNegationValue(getBoolLiteralValue(false)),
114       &getOrCreateNegationValue(Val),
115   };
116   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
117   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
118   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
119 }
120 
121 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   llvm::DenseSet<BoolValue *> Constraints = {
125       &getBoolLiteralValue(true),
126       &getOrCreateNegationValue(getBoolLiteralValue(false)),
127       &getOrCreateNegationValue(Token),
128   };
129   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
130   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
131   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
132 }
133 
134 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
135     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
136     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
137   auto Res = VisitedTokens.insert(&Token);
138   if (!Res.second)
139     return;
140 
141   auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
142   if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
143     Constraints.insert(FirstConjunctIT->second);
144   auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
145   if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
146     Constraints.insert(RemainingConjunctsIT->second.begin(),
147                        RemainingConjunctsIT->second.end());
148 
149   auto DepsIT = FlowConditionDeps.find(&Token);
150   if (DepsIT != FlowConditionDeps.end()) {
151     for (AtomicBoolValue *DepToken : DepsIT->second)
152       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
153                                             VisitedTokens);
154   }
155 }
156 
157 } // namespace dataflow
158 } // namespace clang
159 
160 using namespace clang;
161 
162 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
163   const Expr *Current = &E;
164   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {
165     Current = EWC->getSubExpr();
166     assert(Current != nullptr);
167   }
168   Current = Current->IgnoreParens();
169   assert(Current != nullptr);
170   return *Current;
171 }
172 
173 const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) {
174   if (auto *E = dyn_cast<Expr>(&S))
175     return ignoreCFGOmittedNodes(*E);
176   return S;
177 }
178