1 //===-- SimplifyConstraints.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 #include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"
10 #include "llvm/ADT/EquivalenceClasses.h"
11 
12 namespace clang {
13 namespace dataflow {
14 
15 // Substitutes all occurrences of a given atom in `F` by a given formula and
16 // returns the resulting formula.
17 static const Formula &
18 substitute(const Formula &F,
19            const llvm::DenseMap<Atom, const Formula *> &Substitutions,
20            Arena &arena) {
21   switch (F.kind()) {
22   case Formula::AtomRef:
23     if (auto iter = Substitutions.find(F.getAtom());
24         iter != Substitutions.end())
25       return *iter->second;
26     return F;
27   case Formula::Literal:
28     return F;
29   case Formula::Not:
30     return arena.makeNot(substitute(*F.operands()[0], Substitutions, arena));
31   case Formula::And:
32     return arena.makeAnd(substitute(*F.operands()[0], Substitutions, arena),
33                          substitute(*F.operands()[1], Substitutions, arena));
34   case Formula::Or:
35     return arena.makeOr(substitute(*F.operands()[0], Substitutions, arena),
36                         substitute(*F.operands()[1], Substitutions, arena));
37   case Formula::Implies:
38     return arena.makeImplies(
39         substitute(*F.operands()[0], Substitutions, arena),
40         substitute(*F.operands()[1], Substitutions, arena));
41   case Formula::Equal:
42     return arena.makeEquals(substitute(*F.operands()[0], Substitutions, arena),
43                             substitute(*F.operands()[1], Substitutions, arena));
44   }
45   llvm_unreachable("Unknown formula kind");
46 }
47 
48 // Returns the result of replacing atoms in `Atoms` with the leader of their
49 // equivalence class in `EquivalentAtoms`.
50 // Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted
51 // into it as single-member equivalence classes.
52 static llvm::DenseSet<Atom>
53 projectToLeaders(const llvm::DenseSet<Atom> &Atoms,
54                  llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
55   llvm::DenseSet<Atom> Result;
56 
57   for (Atom Atom : Atoms)
58     Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));
59 
60   return Result;
61 }
62 
63 // Returns the atoms in the equivalence class for the leader identified by
64 // `LeaderIt`.
65 static llvm::SmallVector<Atom>
66 atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,
67                         llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
68   llvm::SmallVector<Atom> Result;
69   for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);
70        MemberIt != EquivalentAtoms.member_end(); ++MemberIt)
71     Result.push_back(*MemberIt);
72   return Result;
73 }
74 
75 void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
76                          Arena &arena, SimplifyConstraintsInfo *Info) {
77   auto contradiction = [&]() {
78     Constraints.clear();
79     Constraints.insert(&arena.makeLiteral(false));
80   };
81 
82   llvm::EquivalenceClasses<Atom> EquivalentAtoms;
83   llvm::DenseSet<Atom> TrueAtoms;
84   llvm::DenseSet<Atom> FalseAtoms;
85 
86   while (true) {
87     for (const auto *Constraint : Constraints) {
88       switch (Constraint->kind()) {
89       case Formula::AtomRef:
90         TrueAtoms.insert(Constraint->getAtom());
91         break;
92       case Formula::Not:
93         if (Constraint->operands()[0]->kind() == Formula::AtomRef)
94           FalseAtoms.insert(Constraint->operands()[0]->getAtom());
95         break;
96       case Formula::Equal: {
97         ArrayRef<const Formula *> operands = Constraint->operands();
98         if (operands[0]->kind() == Formula::AtomRef &&
99             operands[1]->kind() == Formula::AtomRef) {
100           EquivalentAtoms.unionSets(operands[0]->getAtom(),
101                                     operands[1]->getAtom());
102         }
103         break;
104       }
105       default:
106         break;
107       }
108     }
109 
110     TrueAtoms = projectToLeaders(TrueAtoms, EquivalentAtoms);
111     FalseAtoms = projectToLeaders(FalseAtoms, EquivalentAtoms);
112 
113     llvm::DenseMap<Atom, const Formula *> Substitutions;
114     for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {
115       Atom TheAtom = It->getData();
116       Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);
117       if (TrueAtoms.contains(Leader)) {
118         if (FalseAtoms.contains(Leader)) {
119           contradiction();
120           return;
121         }
122         Substitutions.insert({TheAtom, &arena.makeLiteral(true)});
123       } else if (FalseAtoms.contains(Leader)) {
124         Substitutions.insert({TheAtom, &arena.makeLiteral(false)});
125       } else if (TheAtom != Leader) {
126         Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});
127       }
128     }
129 
130     llvm::SetVector<const Formula *> NewConstraints;
131     for (const auto *Constraint : Constraints) {
132       const Formula &NewConstraint =
133           substitute(*Constraint, Substitutions, arena);
134       if (NewConstraint.isLiteral(true))
135         continue;
136       if (NewConstraint.isLiteral(false)) {
137         contradiction();
138         return;
139       }
140       if (NewConstraint.kind() == Formula::And) {
141         NewConstraints.insert(NewConstraint.operands()[0]);
142         NewConstraints.insert(NewConstraint.operands()[1]);
143         continue;
144       }
145       NewConstraints.insert(&NewConstraint);
146     }
147 
148     if (NewConstraints == Constraints)
149       break;
150     Constraints = std::move(NewConstraints);
151   }
152 
153   if (Info) {
154     for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();
155          It != End; ++It) {
156       if (!It->isLeader())
157         continue;
158       Atom At = *EquivalentAtoms.findLeader(It);
159       if (TrueAtoms.contains(At) || FalseAtoms.contains(At))
160         continue;
161       llvm::SmallVector<Atom> Atoms =
162           atomsInEquivalenceClass(EquivalentAtoms, It);
163       if (Atoms.size() == 1)
164         continue;
165       std::sort(Atoms.begin(), Atoms.end());
166       Info->EquivalentAtoms.push_back(std::move(Atoms));
167     }
168     for (Atom At : TrueAtoms)
169       Info->TrueAtoms.append(atomsInEquivalenceClass(
170           EquivalentAtoms, EquivalentAtoms.findValue(At)));
171     std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());
172     for (Atom At : FalseAtoms)
173       Info->FalseAtoms.append(atomsInEquivalenceClass(
174           EquivalentAtoms, EquivalentAtoms.findValue(At)));
175     std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());
176   }
177 }
178 
179 } // namespace dataflow
180 } // namespace clang
181