-
Notifications
You must be signed in to change notification settings - Fork 11.8k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[clang][dataflow] Simplify flow conditions displayed in HTMLLogger. #70848
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
//===-- SimplifyConstraints.h -----------------------------------*- C++ -*-===// | ||
// | ||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. | ||
// See https://llvm.org/LICENSE.txt for license information. | ||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | ||
// | ||
//===----------------------------------------------------------------------===// | ||
// | ||
// This file defines a DataflowAnalysisContext class that owns objects that | ||
// encompass the state of a program and stores context that is used during | ||
// dataflow analysis. | ||
// | ||
//===----------------------------------------------------------------------===// | ||
|
||
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H | ||
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H | ||
|
||
#include "clang/Analysis/FlowSensitive/Arena.h" | ||
#include "clang/Analysis/FlowSensitive/Formula.h" | ||
#include "llvm/ADT/SetVector.h" | ||
|
||
namespace clang { | ||
namespace dataflow { | ||
|
||
/// Information on the way a set of constraints was simplified. | ||
struct SimplifyConstraintsInfo { | ||
/// List of equivalence classes of atoms. For each equivalence class, the | ||
/// original constraints imply that all atoms in it must be equivalent. | ||
/// Simplification replaces all occurrences of atoms in an equivalence class | ||
/// with a single representative atom from the class. | ||
/// Does not contain equivalence classes with just one member or atoms | ||
/// contained in `TrueAtoms` or `FalseAtoms`. | ||
llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms; | ||
/// Atoms that the original constraints imply must be true. | ||
/// Simplification replaces all occurrences of these atoms by a true literal | ||
/// (which may enable additional simplifications). | ||
llvm::SmallVector<Atom> TrueAtoms; | ||
/// Atoms that the original constraints imply must be false. | ||
/// Simplification replaces all occurrences of these atoms by a false literal | ||
/// (which may enable additional simplifications). | ||
llvm::SmallVector<Atom> FalseAtoms; | ||
}; | ||
|
||
/// Simplifies a set of constraints (implicitly connected by "and") in a way | ||
/// that does not change satisfiability of the constraints. This does _not_ mean | ||
/// that the set of solutions is the same before and after simplification. | ||
/// `Info`, if non-null, will be populated with information about the | ||
/// simplifications that were made to the formula (e.g. to display to the user). | ||
void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints, | ||
Arena &arena, SimplifyConstraintsInfo *Info = nullptr); | ||
|
||
} // namespace dataflow | ||
} // namespace clang | ||
|
||
#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H |
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
@@ -0,0 +1,183 @@ | ||||||
//===-- SimplifyConstraints.cpp ---------------------------------*- C++ -*-===// | ||||||
// | ||||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. | ||||||
// See https://llvm.org/LICENSE.txt for license information. | ||||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | ||||||
// | ||||||
//===----------------------------------------------------------------------===// | ||||||
// | ||||||
// This file defines a DataflowAnalysisContext class that owns objects that | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. replace or delete. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Oops again. Done. |
||||||
// encompass the state of a program and stores context that is used during | ||||||
// dataflow analysis. | ||||||
// | ||||||
//===----------------------------------------------------------------------===// | ||||||
|
||||||
#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h" | ||||||
#include "llvm/ADT/EquivalenceClasses.h" | ||||||
|
||||||
namespace clang { | ||||||
namespace dataflow { | ||||||
|
||||||
// Substitute all occurrences of a given atom in `F` by a given formula and | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done. |
||||||
// returns the resulting formula. | ||||||
static const Formula & | ||||||
substitute(const Formula &F, | ||||||
const llvm::DenseMap<Atom, const Formula *> &Substitutions, | ||||||
Arena &arena) { | ||||||
switch (F.kind()) { | ||||||
case Formula::AtomRef: | ||||||
if (auto iter = Substitutions.find(F.getAtom()); | ||||||
iter != Substitutions.end()) | ||||||
return *iter->second; | ||||||
return F; | ||||||
case Formula::Literal: | ||||||
return F; | ||||||
case Formula::Not: | ||||||
return arena.makeNot(substitute(*F.operands()[0], Substitutions, arena)); | ||||||
case Formula::And: | ||||||
return arena.makeAnd(substitute(*F.operands()[0], Substitutions, arena), | ||||||
substitute(*F.operands()[1], Substitutions, arena)); | ||||||
case Formula::Or: | ||||||
return arena.makeOr(substitute(*F.operands()[0], Substitutions, arena), | ||||||
substitute(*F.operands()[1], Substitutions, arena)); | ||||||
case Formula::Implies: | ||||||
return arena.makeImplies( | ||||||
substitute(*F.operands()[0], Substitutions, arena), | ||||||
substitute(*F.operands()[1], Substitutions, arena)); | ||||||
case Formula::Equal: | ||||||
return arena.makeEquals(substitute(*F.operands()[0], Substitutions, arena), | ||||||
substitute(*F.operands()[1], Substitutions, arena)); | ||||||
} | ||||||
} | ||||||
|
||||||
// Returns the result of replacing atoms in `Atoms` with the leader of their | ||||||
// equivalence class in `EquivalentAtoms`. | ||||||
// Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted | ||||||
// into it as single-member equivalence classes. | ||||||
static llvm::DenseSet<Atom> | ||||||
projectToLeaders(const llvm::DenseSet<Atom> &Atoms, | ||||||
llvm::EquivalenceClasses<Atom> &EquivalentAtoms) { | ||||||
llvm::DenseSet<Atom> Result; | ||||||
|
||||||
for (Atom Atom : Atoms) | ||||||
Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom)); | ||||||
|
||||||
return Result; | ||||||
} | ||||||
|
||||||
// Returns the atoms in the equivalence class for the leader identified by | ||||||
// `LeaderIt`. | ||||||
static llvm::SmallVector<Atom> | ||||||
atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms, | ||||||
llvm::EquivalenceClasses<Atom>::iterator LeaderIt) { | ||||||
llvm::SmallVector<Atom> Result; | ||||||
for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt); | ||||||
MemberIt != EquivalentAtoms.member_end(); ++MemberIt) | ||||||
Result.push_back(*MemberIt); | ||||||
return Result; | ||||||
} | ||||||
|
||||||
void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints, | ||||||
Arena &arena, SimplifyConstraintsInfo *Info) { | ||||||
auto contradiction = [&]() { | ||||||
Constraints.clear(); | ||||||
Constraints.insert(&arena.makeLiteral(false)); | ||||||
}; | ||||||
|
||||||
llvm::EquivalenceClasses<Atom> EquivalentAtoms; | ||||||
llvm::DenseSet<Atom> TrueAtoms; | ||||||
llvm::DenseSet<Atom> FalseAtoms; | ||||||
|
||||||
while (true) { | ||||||
for (const auto *Constraint : Constraints) { | ||||||
switch (Constraint->kind()) { | ||||||
case Formula::AtomRef: | ||||||
TrueAtoms.insert(Constraint->getAtom()); | ||||||
break; | ||||||
case Formula::Not: | ||||||
if (Constraint->operands()[0]->kind() == Formula::AtomRef) | ||||||
FalseAtoms.insert(Constraint->operands()[0]->getAtom()); | ||||||
break; | ||||||
case Formula::Equal: | ||||||
if (Constraint->operands()[0]->kind() == Formula::AtomRef && | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. nit: bind There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Good call. Done. |
||||||
Constraint->operands()[1]->kind() == Formula::AtomRef) { | ||||||
EquivalentAtoms.unionSets(Constraint->operands()[0]->getAtom(), | ||||||
Constraint->operands()[1]->getAtom()); | ||||||
} | ||||||
break; | ||||||
default: | ||||||
break; | ||||||
} | ||||||
} | ||||||
|
||||||
TrueAtoms = projectToLeaders(TrueAtoms, EquivalentAtoms); | ||||||
FalseAtoms = projectToLeaders(FalseAtoms, EquivalentAtoms); | ||||||
|
||||||
llvm::DenseMap<Atom, const Formula *> Substitutions; | ||||||
for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) { | ||||||
Atom TheAtom = It->getData(); | ||||||
Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom); | ||||||
if (TrueAtoms.contains(Leader)) { | ||||||
if (FalseAtoms.contains(Leader)) { | ||||||
contradiction(); | ||||||
return; | ||||||
} | ||||||
Substitutions.insert({TheAtom, &arena.makeLiteral(true)}); | ||||||
} else if (FalseAtoms.contains(Leader)) { | ||||||
Substitutions.insert({TheAtom, &arena.makeLiteral(false)}); | ||||||
} else if (TheAtom != Leader) { | ||||||
Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)}); | ||||||
} | ||||||
} | ||||||
|
||||||
llvm::SetVector<const Formula *> NewConstraints; | ||||||
for (const auto *Constraint : Constraints) { | ||||||
const Formula &NewConstraint = | ||||||
substitute(*Constraint, Substitutions, arena); | ||||||
if (&NewConstraint == &arena.makeLiteral(true)) | ||||||
continue; | ||||||
if (&NewConstraint == &arena.makeLiteral(false)) { | ||||||
contradiction(); | ||||||
return; | ||||||
} | ||||||
if (NewConstraint.kind() == Formula::And) { | ||||||
NewConstraints.insert(NewConstraint.operands()[0]); | ||||||
NewConstraints.insert(NewConstraint.operands()[1]); | ||||||
continue; | ||||||
} | ||||||
Comment on lines
+139
to
+143
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. why do this step here rather than at the outset (for loop on line 92)? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I can't do it in the loop on line 92 -- because I already want that loop to "see" the "split conjunctions". So I'd have to add yet another loop. That might potentially be more efficient in some cases -- but it's not even clear to me that it would be a definite performance win (I'd be reallocating the |
||||||
NewConstraints.insert(&NewConstraint); | ||||||
} | ||||||
|
||||||
if (NewConstraints == Constraints) | ||||||
break; | ||||||
Constraints = NewConstraints; | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. std::move? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Of course. Thanks for catching! Done. |
||||||
} | ||||||
|
||||||
if (Info) { | ||||||
for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end(); | ||||||
It != End; ++It) { | ||||||
if (!It->isLeader()) | ||||||
continue; | ||||||
Atom At = *EquivalentAtoms.findLeader(It); | ||||||
if (TrueAtoms.contains(At) || FalseAtoms.contains(At)) | ||||||
continue; | ||||||
llvm::SmallVector<Atom> Atoms = | ||||||
atomsInEquivalenceClass(EquivalentAtoms, It); | ||||||
if (Atoms.size() == 1) | ||||||
continue; | ||||||
std::sort(Atoms.begin(), Atoms.end()); | ||||||
Info->EquivalentAtoms.push_back(std::move(Atoms)); | ||||||
} | ||||||
for (Atom At : TrueAtoms) | ||||||
Info->TrueAtoms.append(atomsInEquivalenceClass( | ||||||
EquivalentAtoms, EquivalentAtoms.findValue(At))); | ||||||
std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end()); | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. why sort? for output readability? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Exactly. |
||||||
for (Atom At : FalseAtoms) | ||||||
Info->FalseAtoms.append(atomsInEquivalenceClass( | ||||||
EquivalentAtoms, EquivalentAtoms.findValue(At))); | ||||||
std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end()); | ||||||
} | ||||||
} | ||||||
|
||||||
} // namespace dataflow | ||||||
} // namespace clang |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Replace/delete.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oops... thanks for catching. Done.