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
12namespace clang {
13namespace dataflow {
14
15// Substitutes all occurrences of a given atom in `F` by a given formula and
16// 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 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.
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 by
64// `LeaderIt`.
65static llvm::SmallVector<Atom>
66atomsInEquivalenceClass(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
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 (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