178 lines · 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-exception6//7//===----------------------------------------------------------------------===//8 9#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"10#include "llvm/ADT/EquivalenceClasses.h"11 12namespace clang {13namespace dataflow {14 15// Substitutes all occurrences of a given atom in `F` by a given formula and16// returns the resulting formula.17static const Formula &18substitute(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 their49// equivalence class in `EquivalentAtoms`.50// Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted51// into it as single-member equivalence classes.52static llvm::DenseSet<Atom>53projectToLeaders(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 by64// `LeaderIt`.65static llvm::SmallVector<Atom>66atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,67 const Atom &At) {68 llvm::SmallVector<Atom> Result;69 for (auto MemberIt = EquivalentAtoms.findLeader(At);70 MemberIt != EquivalentAtoms.member_end(); ++MemberIt)71 Result.push_back(*MemberIt);72 return Result;73}74 75void 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 (const auto &E : EquivalentAtoms) {115 Atom TheAtom = E->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 (const auto &E : EquivalentAtoms) {155 if (!E->isLeader())156 continue;157 Atom At = *EquivalentAtoms.findLeader(*E);158 if (TrueAtoms.contains(At) || FalseAtoms.contains(At))159 continue;160 llvm::SmallVector<Atom> Atoms =161 atomsInEquivalenceClass(EquivalentAtoms, At);162 if (Atoms.size() == 1)163 continue;164 std::sort(Atoms.begin(), Atoms.end());165 Info->EquivalentAtoms.push_back(std::move(Atoms));166 }167 for (Atom At : TrueAtoms)168 Info->TrueAtoms.append(atomsInEquivalenceClass(EquivalentAtoms, At));169 std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());170 for (Atom At : FalseAtoms)171 Info->FalseAtoms.append(atomsInEquivalenceClass(EquivalentAtoms, At));172 std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());173 }174}175 176} // namespace dataflow177} // namespace clang178