Skip to content

Commit 7c63672

Browse files
martinboehmemartinboehme
authored
[clang][dataflow] Simplify flow conditions displayed in HTMLLogger. (#70848)
This can make the flow condition significantly easier to interpret; see below for an example. I had hoped that adding the simplification as a preprocessing step before the SAT solver (in `DataflowAnalysisContext::querySolver()`) would also speed up SAT solving and maybe even eliminate SAT solver timeouts, but in my testing, this actually turns out to be a pessimization. It appears that these simplifications are easy enough for the SAT solver to perform itself. Nevertheless, the improvement in debugging alone makes this a worthwhile change. Example of flow condition output with these changes: ``` Flow condition token: V37 Constraints: (V16 = (((V15 & (V19 = V12)) & V22) & V25)) (V15 = ((V12 & ((V14 = V9) | (V14 = V4))) & (V13 = V14))) True atoms: (V0, V1, V2, V5, V6, V7, V29, V30, V32, V34, V35, V37) False atoms: (V3, V8, V17) Equivalent atoms: (V11, V15) Flow condition constraints before simplification: V37 ((!V3 & !V8) & !V17) (V37 = V34) (V34 = (V29 & (V35 = V30))) (V29 = (((V16 | V2) & V32) & (V30 = V32))) (V16 = (((V15 & (V19 = V12)) & V22) & V25)) (V15 = V11) (V11 = ((((V7 | V2) & V12) & ((V7 & (V14 = V9)) | (V2 & (V14 = V4)))) & (V13 = V14))) (V2 = V1) (V1 = V0) V0 (V7 = V6) (V6 = V5) (V5 = V2) ```
1 parent 9b24391 commit 7c63672

File tree

9 files changed

+449
-2
lines changed

9 files changed

+449
-2
lines changed

‎clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
//===-- SimplifyConstraints.h -----------------------------------*- 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+
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
10+
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
11+
12+
#include "clang/Analysis/FlowSensitive/Arena.h"
13+
#include "clang/Analysis/FlowSensitive/Formula.h"
14+
#include "llvm/ADT/SetVector.h"
15+
16+
namespace clang {
17+
namespace dataflow {
18+
19+
/// Information on the way a set of constraints was simplified.
20+
struct SimplifyConstraintsInfo {
21+
/// List of equivalence classes of atoms. For each equivalence class, the
22+
/// original constraints imply that all atoms in it must be equivalent.
23+
/// Simplification replaces all occurrences of atoms in an equivalence class
24+
/// with a single representative atom from the class.
25+
/// Does not contain equivalence classes with just one member or atoms
26+
/// contained in `TrueAtoms` or `FalseAtoms`.
27+
llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms;
28+
/// Atoms that the original constraints imply must be true.
29+
/// Simplification replaces all occurrences of these atoms by a true literal
30+
/// (which may enable additional simplifications).
31+
llvm::SmallVector<Atom> TrueAtoms;
32+
/// Atoms that the original constraints imply must be false.
33+
/// Simplification replaces all occurrences of these atoms by a false literal
34+
/// (which may enable additional simplifications).
35+
llvm::SmallVector<Atom> FalseAtoms;
36+
};
37+
38+
/// Simplifies a set of constraints (implicitly connected by "and") in a way
39+
/// that does not change satisfiability of the constraints. This does _not_ mean
40+
/// that the set of solutions is the same before and after simplification.
41+
/// `Info`, if non-null, will be populated with information about the
42+
/// simplifications that were made to the formula (e.g. to display to the user).
43+
void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
44+
Arena &arena, SimplifyConstraintsInfo *Info = nullptr);
45+
46+
} // namespace dataflow
47+
} // namespace clang
48+
49+
#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H

‎clang/lib/Analysis/FlowSensitive/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ add_clang_library(clangAnalysisFlowSensitive
77
HTMLLogger.cpp
88
Logger.cpp
99
RecordOps.cpp
10+
SimplifyConstraints.cpp
1011
Transfer.cpp
1112
TypeErasedDataflowAnalysis.cpp
1213
Value.cpp

‎clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

Lines changed: 39 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
1818
#include "clang/Analysis/FlowSensitive/Formula.h"
1919
#include "clang/Analysis/FlowSensitive/Logger.h"
20+
#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"
2021
#include "clang/Analysis/FlowSensitive/Value.h"
2122
#include "llvm/ADT/SetOperations.h"
2223
#include "llvm/ADT/SetVector.h"
@@ -205,13 +206,50 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
205206
}
206207
}
207208

209+
static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
210+
llvm::raw_ostream &OS) {
211+
OS << "(";
212+
for (size_t i = 0; i < Atoms.size(); ++i) {
213+
OS << Atoms[i];
214+
if (i + 1 < Atoms.size())
215+
OS << ", ";
216+
}
217+
OS << ")\n";
218+
}
219+
208220
void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
209221
llvm::raw_ostream &OS) {
210222
llvm::SetVector<const Formula *> Constraints;
211223
Constraints.insert(&arena().makeAtomRef(Token));
212224
addTransitiveFlowConditionConstraints(Token, Constraints);
213225

214-
for (const auto *Constraint : Constraints) {
226+
OS << "Flow condition token: " << Token << "\n";
227+
SimplifyConstraintsInfo Info;
228+
llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
229+
simplifyConstraints(Constraints, arena(), &Info);
230+
if (!Constraints.empty()) {
231+
OS << "Constraints:\n";
232+
for (const auto *Constraint : Constraints) {
233+
Constraint->print(OS);
234+
OS << "\n";
235+
}
236+
}
237+
if (!Info.TrueAtoms.empty()) {
238+
OS << "True atoms: ";
239+
printAtomList(Info.TrueAtoms, OS);
240+
}
241+
if (!Info.FalseAtoms.empty()) {
242+
OS << "False atoms: ";
243+
printAtomList(Info.FalseAtoms, OS);
244+
}
245+
if (!Info.EquivalentAtoms.empty()) {
246+
OS << "Equivalent atoms:\n";
247+
for (const llvm::SmallVector<Atom> Class : Info.EquivalentAtoms)
248+
printAtomList(Class, OS);
249+
}
250+
251+
OS << "\nFlow condition constraints before simplification:\n";
252+
for (const auto *Constraint : OriginalConstraints) {
215253
Constraint->print(OS);
216254
OS << "\n";
217255
}

‎clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -961,7 +961,7 @@ void Environment::dump(raw_ostream &OS) const {
961961
OS << " [" << L << ", " << V << ": " << *V << "]\n";
962962
}
963963

964-
OS << "FlowConditionToken:\n";
964+
OS << "\n";
965965
DACtx->dumpFlowCondition(FlowConditionToken, OS);
966966
}
967967

‎clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
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+
}
46+
47+
// Returns the result of replacing atoms in `Atoms` with the leader of their
48+
// equivalence class in `EquivalentAtoms`.
49+
// Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted
50+
// into it as single-member equivalence classes.
51+
static llvm::DenseSet<Atom>
52+
projectToLeaders(const llvm::DenseSet<Atom> &Atoms,
53+
llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
54+
llvm::DenseSet<Atom> Result;
55+
56+
for (Atom Atom : Atoms)
57+
Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));
58+
59+
return Result;
60+
}
61+
62+
// Returns the atoms in the equivalence class for the leader identified by
63+
// `LeaderIt`.
64+
static llvm::SmallVector<Atom>
65+
atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,
66+
llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
67+
llvm::SmallVector<Atom> Result;
68+
for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);
69+
MemberIt != EquivalentAtoms.member_end(); ++MemberIt)
70+
Result.push_back(*MemberIt);
71+
return Result;
72+
}
73+
74+
void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
75+
Arena &arena, SimplifyConstraintsInfo *Info) {
76+
auto contradiction = [&]() {
77+
Constraints.clear();
78+
Constraints.insert(&arena.makeLiteral(false));
79+
};
80+
81+
llvm::EquivalenceClasses<Atom> EquivalentAtoms;
82+
llvm::DenseSet<Atom> TrueAtoms;
83+
llvm::DenseSet<Atom> FalseAtoms;
84+
85+
while (true) {
86+
for (const auto *Constraint : Constraints) {
87+
switch (Constraint->kind()) {
88+
case Formula::AtomRef:
89+
TrueAtoms.insert(Constraint->getAtom());
90+
break;
91+
case Formula::Not:
92+
if (Constraint->operands()[0]->kind() == Formula::AtomRef)
93+
FalseAtoms.insert(Constraint->operands()[0]->getAtom());
94+
break;
95+
case Formula::Equal: {
96+
ArrayRef<const Formula *> operands = Constraint->operands();
97+
if (operands[0]->kind() == Formula::AtomRef &&
98+
operands[1]->kind() == Formula::AtomRef) {
99+
EquivalentAtoms.unionSets(operands[0]->getAtom(),
100+
operands[1]->getAtom());
101+
}
102+
break;
103+
}
104+
default:
105+
break;
106+
}
107+
}
108+
109+
TrueAtoms = projectToLeaders(TrueAtoms, EquivalentAtoms);
110+
FalseAtoms = projectToLeaders(FalseAtoms, EquivalentAtoms);
111+
112+
llvm::DenseMap<Atom, const Formula *> Substitutions;
113+
for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {
114+
Atom TheAtom = It->getData();
115+
Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);
116+
if (TrueAtoms.contains(Leader)) {
117+
if (FalseAtoms.contains(Leader)) {
118+
contradiction();
119+
return;
120+
}
121+
Substitutions.insert({TheAtom, &arena.makeLiteral(true)});
122+
} else if (FalseAtoms.contains(Leader)) {
123+
Substitutions.insert({TheAtom, &arena.makeLiteral(false)});
124+
} else if (TheAtom != Leader) {
125+
Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});
126+
}
127+
}
128+
129+
llvm::SetVector<const Formula *> NewConstraints;
130+
for (const auto *Constraint : Constraints) {
131+
const Formula &NewConstraint =
132+
substitute(*Constraint, Substitutions, arena);
133+
if (&NewConstraint == &arena.makeLiteral(true))
134+
continue;
135+
if (&NewConstraint == &arena.makeLiteral(false)) {
136+
contradiction();
137+
return;
138+
}
139+
if (NewConstraint.kind() == Formula::And) {
140+
NewConstraints.insert(NewConstraint.operands()[0]);
141+
NewConstraints.insert(NewConstraint.operands()[1]);
142+
continue;
143+
}
144+
NewConstraints.insert(&NewConstraint);
145+
}
146+
147+
if (NewConstraints == Constraints)
148+
break;
149+
Constraints = std::move(NewConstraints);
150+
}
151+
152+
if (Info) {
153+
for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();
154+
It != End; ++It) {
155+
if (!It->isLeader())
156+
continue;
157+
Atom At = *EquivalentAtoms.findLeader(It);
158+
if (TrueAtoms.contains(At) || FalseAtoms.contains(At))
159+
continue;
160+
llvm::SmallVector<Atom> Atoms =
161+
atomsInEquivalenceClass(EquivalentAtoms, It);
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(
169+
EquivalentAtoms, EquivalentAtoms.findValue(At)));
170+
std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());
171+
for (Atom At : FalseAtoms)
172+
Info->FalseAtoms.append(atomsInEquivalenceClass(
173+
EquivalentAtoms, EquivalentAtoms.findValue(At)));
174+
std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());
175+
}
176+
}
177+
178+
} // namespace dataflow
179+
} // namespace clang

‎clang/unittests/Analysis/FlowSensitive/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
1717
MultiVarConstantPropagationTest.cpp
1818
RecordOpsTest.cpp
1919
SignAnalysisTest.cpp
20+
SimplifyConstraintsTest.cpp
2021
SingleVarConstantPropagationTest.cpp
2122
SolverTest.cpp
2223
TestingSupport.cpp

0 commit comments

Comments
 (0)