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