clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp

   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 == &arena.makeLiteral(true))
 135         continue;
 136       if (&NewConstraint == &arena.makeLiteral(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