clang 20.0.0git
SimplifyConstraints.cpp
Go to the documentation of this file.
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
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 &
19 const llvm::DenseMap<Atom, const Formula *> &Substitutions,
20 Arena &arena) {
21 switch (F.kind()) {
23 if (auto iter = Substitutions.find(F.getAtom());
24 iter != Substitutions.end())
25 return *iter->second;
26 return F;
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));
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.
54 llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
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`.
66atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,
67 llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
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()) {
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;
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)
170 EquivalentAtoms, EquivalentAtoms.findValue(At)));
171 std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());
172 for (Atom At : FalseAtoms)
174 EquivalentAtoms, EquivalentAtoms.findValue(At)));
175 std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());
176 }
177}
178
179} // namespace dataflow
180} // namespace clang
The Arena owns the objects that model data within an analysis.
Definition: Arena.h:21
const Formula & makeEquals(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS <=> RHS.
Definition: Arena.cpp:91
const Formula & makeAtomRef(Atom A)
Returns a formula for the variable A.
Definition: Arena.cpp:34
const Formula & makeNot(const Formula &Val)
Returns a formula for the negation of Val.
Definition: Arena.cpp:67
const Formula & makeOr(const Formula &LHS, const Formula &RHS)
Returns a formula for the disjunction of LHS and RHS.
Definition: Arena.cpp:54
const Formula & makeAnd(const Formula &LHS, const Formula &RHS)
Returns a formula for the conjunction of LHS and RHS.
Definition: Arena.cpp:41
const Formula & makeImplies(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS => RHS.
Definition: Arena.cpp:78
const Formula & makeLiteral(bool Value)
Returns a formula for a literal true/false.
Definition: Arena.h:111
ArrayRef< const Formula * > operands() const
Definition: Formula.h:82
bool isLiteral(bool b) const
Definition: Formula.h:78
Atom getAtom() const
Definition: Formula.h:68
@ Equal
True if LHS is false or RHS is true.
Definition: Formula.h:64
@ Implies
True if either LHS or RHS is true.
Definition: Formula.h:63
@ AtomRef
A reference to an atomic boolean variable.
Definition: Formula.h:54
@ Literal
Constant true or false.
Definition: Formula.h:56
@ Or
True if LHS and RHS are both true.
Definition: Formula.h:62
@ And
True if its only operand is false.
Definition: Formula.h:61
Kind kind() const
Definition: Formula.h:66
static llvm::SmallVector< Atom > atomsInEquivalenceClass(const llvm::EquivalenceClasses< Atom > &EquivalentAtoms, llvm::EquivalenceClasses< Atom >::iterator LeaderIt)
Atom
Identifies an atomic boolean variable such as "V1".
Definition: Formula.h:34
void simplifyConstraints(llvm::SetVector< const Formula * > &Constraints, Arena &arena, SimplifyConstraintsInfo *Info=nullptr)
Simplifies a set of constraints (implicitly connected by "and") in a way that does not change satisfi...
static llvm::DenseSet< Atom > projectToLeaders(const llvm::DenseSet< Atom > &Atoms, llvm::EquivalenceClasses< Atom > &EquivalentAtoms)
static const Formula & substitute(const Formula &F, const llvm::DenseMap< Atom, const Formula * > &Substitutions, Arena &arena)
The JSON file list parser is used to communicate input to InstallAPI.
@ Result
The result type of a method or function.
Information on the way a set of constraints was simplified.
llvm::SmallVector< Atom > TrueAtoms
Atoms that the original constraints imply must be true.
llvm::SmallVector< llvm::SmallVector< Atom > > EquivalentAtoms
List of equivalence classes of atoms.
llvm::SmallVector< Atom > FalseAtoms
Atoms that the original constraints imply must be false.