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   return createAtomicBoolValue();
70 }
71 
72 void DataflowAnalysisContext::addFlowConditionConstraint(
73     AtomicBoolValue &Token, BoolValue &Constraint) {
74   auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
75   if (!Res.second) {
76     Res.first->second =
77         &getOrCreateConjunctionValue(*Res.first->second, Constraint);
78   }
79 }
80 
81 AtomicBoolValue &
82 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
83   auto &ForkToken = makeFlowConditionToken();
84   FlowConditionDeps[&ForkToken].insert(&Token);
85   addFlowConditionConstraint(ForkToken, Token);
86   return ForkToken;
87 }
88 
89 AtomicBoolValue &
90 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
91                                             AtomicBoolValue &SecondToken) {
92   auto &Token = makeFlowConditionToken();
93   FlowConditionDeps[&Token].insert(&FirstToken);
94   FlowConditionDeps[&Token].insert(&SecondToken);
95   addFlowConditionConstraint(
96       Token, getOrCreateDisjunctionValue(FirstToken, SecondToken));
97   return Token;
98 }
99 
100 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
101                                                    BoolValue &Val) {
102   // Returns true if and only if truth assignment of the flow condition implies
103   // that `Val` is also true. We prove whether or not this property holds by
104   // reducing the problem to satisfiability checking. In other words, we attempt
105   // to show that assuming `Val` is false makes the constraints induced by the
106   // flow condition unsatisfiable.
107   llvm::DenseSet<BoolValue *> Constraints = {
108       &Token,
109       &getBoolLiteralValue(true),
110       &getOrCreateNegationValue(getBoolLiteralValue(false)),
111       &getOrCreateNegationValue(Val),
112   };
113   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
114   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
115   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
116 }
117 
118 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
119   // Returns true if and only if we cannot prove that the flow condition can
120   // ever be false.
121   llvm::DenseSet<BoolValue *> Constraints = {
122       &getBoolLiteralValue(true),
123       &getOrCreateNegationValue(getBoolLiteralValue(false)),
124       &getOrCreateNegationValue(Token),
125   };
126   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
127   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
128   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
129 }
130 
131 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
132     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
133     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
134   auto Res = VisitedTokens.insert(&Token);
135   if (!Res.second)
136     return;
137 
138   auto ConstraintsIT = FlowConditionConstraints.find(&Token);
139   if (ConstraintsIT == FlowConditionConstraints.end()) {
140     Constraints.insert(&Token);
141   } else {
142     // Bind flow condition token via `iff` to its set of constraints:
143     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
144     Constraints.insert(&getOrCreateConjunctionValue(
145         getOrCreateDisjunctionValue(
146             Token, getOrCreateNegationValue(*ConstraintsIT->second)),
147         getOrCreateDisjunctionValue(getOrCreateNegationValue(Token),
148                                     *ConstraintsIT->second)));
149   }
150 
151   auto DepsIT = FlowConditionDeps.find(&Token);
152   if (DepsIT != FlowConditionDeps.end()) {
153     for (AtomicBoolValue *DepToken : DepsIT->second) {
154       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
155                                             VisitedTokens);
156     }
157   }
158 }
159 
160 } // namespace dataflow
161 } // namespace clang
162 
163 using namespace clang;
164 
165 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
166   const Expr *Current = &E;
167   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {
168     Current = EWC->getSubExpr();
169     assert(Current != nullptr);
170   }
171   Current = Current->IgnoreParens();
172   assert(Current != nullptr);
173   return *Current;
174 }
175 
176 const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) {
177   if (auto *E = dyn_cast<Expr>(&S))
178     return ignoreCFGOmittedNodes(*E);
179   return S;
180 }
181