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/Analysis/FlowSensitive/Value.h"
17 #include <cassert>
18 #include <memory>
19 #include <utility>
20 
21 namespace clang {
22 namespace dataflow {
23 
24 static std::pair<BoolValue *, BoolValue *>
25 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
26   auto Res = std::make_pair(&LHS, &RHS);
27   if (&RHS < &LHS)
28     std::swap(Res.first, Res.second);
29   return Res;
30 }
31 
32 BoolValue &
33 DataflowAnalysisContext::getOrCreateConjunctionValue(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 &
47 DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
48                                                      BoolValue &RHS) {
49   if (&LHS == &RHS)
50     return LHS;
51 
52   auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
53                                          nullptr);
54   if (Res.second)
55     Res.first->second =
56         &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
57   return *Res.first->second;
58 }
59 
60 BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
61   auto Res = NegationVals.try_emplace(&Val, nullptr);
62   if (Res.second)
63     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
64   return *Res.first->second;
65 }
66 
67 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
68   AtomicBoolValue &Token = createAtomicBoolValue();
69   FlowConditionRemainingConjuncts[&Token] = {};
70   FlowConditionFirstConjuncts[&Token] = &Token;
71   return Token;
72 }
73 
74 void DataflowAnalysisContext::addFlowConditionConstraint(
75     AtomicBoolValue &Token, BoolValue &Constraint) {
76   FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(
77       Constraint, getOrCreateNegationValue(Token)));
78   FlowConditionFirstConjuncts[&Token] =
79       &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],
80                                    getOrCreateNegationValue(Constraint));
81 }
82 
83 AtomicBoolValue &
84 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
85   auto &ForkToken = makeFlowConditionToken();
86   FlowConditionDeps[&ForkToken].insert(&Token);
87   addFlowConditionConstraint(ForkToken, Token);
88   return ForkToken;
89 }
90 
91 AtomicBoolValue &
92 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
93                                             AtomicBoolValue &SecondToken) {
94   auto &Token = makeFlowConditionToken();
95   FlowConditionDeps[&Token].insert(&FirstToken);
96   FlowConditionDeps[&Token].insert(&SecondToken);
97   addFlowConditionConstraint(
98       Token, getOrCreateDisjunctionValue(FirstToken, SecondToken));
99   return Token;
100 }
101 
102 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
103                                                    BoolValue &Val) {
104   // Returns true if and only if truth assignment of the flow condition implies
105   // that `Val` is also true. We prove whether or not this property holds by
106   // reducing the problem to satisfiability checking. In other words, we attempt
107   // to show that assuming `Val` is false makes the constraints induced by the
108   // flow condition unsatisfiable.
109   llvm::DenseSet<BoolValue *> Constraints = {
110       &Token,
111       &getBoolLiteralValue(true),
112       &getOrCreateNegationValue(getBoolLiteralValue(false)),
113       &getOrCreateNegationValue(Val),
114   };
115   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
116   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
117   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
118 }
119 
120 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
121   // Returns true if and only if we cannot prove that the flow condition can
122   // ever be false.
123   llvm::DenseSet<BoolValue *> Constraints = {
124       &getBoolLiteralValue(true),
125       &getOrCreateNegationValue(getBoolLiteralValue(false)),
126       &getOrCreateNegationValue(Token),
127   };
128   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
129   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
130   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
131 }
132 
133 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
134     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
135     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
136   auto Res = VisitedTokens.insert(&Token);
137   if (!Res.second)
138     return;
139 
140   auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
141   if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
142     Constraints.insert(FirstConjunctIT->second);
143   auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
144   if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
145     Constraints.insert(RemainingConjunctsIT->second.begin(),
146                        RemainingConjunctsIT->second.end());
147 
148   auto DepsIT = FlowConditionDeps.find(&Token);
149   if (DepsIT != FlowConditionDeps.end()) {
150     for (AtomicBoolValue *DepToken : DepsIT->second)
151       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
152                                             VisitedTokens);
153   }
154 }
155 
156 } // namespace dataflow
157 } // namespace clang
158