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 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
121     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
122     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
123   auto Res = VisitedTokens.insert(&Token);
124   if (!Res.second)
125     return;
126 
127   auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
128   if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
129     Constraints.insert(FirstConjunctIT->second);
130   auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
131   if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
132     Constraints.insert(RemainingConjunctsIT->second.begin(),
133                        RemainingConjunctsIT->second.end());
134 
135   auto DepsIT = FlowConditionDeps.find(&Token);
136   if (DepsIT != FlowConditionDeps.end()) {
137     for (AtomicBoolValue *DepToken : DepsIT->second)
138       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
139                                             VisitedTokens);
140   }
141 }
142 
143 } // namespace dataflow
144 } // namespace clang
145