-
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
Merged
martinboehme
merged 2 commits into
llvm:main
from
martinboehme:piper_export_cl_577149430
Nov 7, 2023
Merged
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
49 changes: 49 additions & 0 deletions
49
clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
//===-- 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 | ||
// | ||
//===----------------------------------------------------------------------===// | ||
|
||
#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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
179 changes: 179 additions & 0 deletions
179
clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,179 @@ | ||
//===-- 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 | ||
// | ||
//===----------------------------------------------------------------------===// | ||
|
||
#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h" | ||
#include "llvm/ADT/EquivalenceClasses.h" | ||
|
||
namespace clang { | ||
namespace dataflow { | ||
|
||
// Substitutes all occurrences of a given atom in `F` by a given formula and | ||
// 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: { | ||
ArrayRef<const Formula *> operands = Constraint->operands(); | ||
if (operands[0]->kind() == Formula::AtomRef && | ||
operands[1]->kind() == Formula::AtomRef) { | ||
EquivalentAtoms.unionSets(operands[0]->getAtom(), | ||
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; | ||
} | ||
NewConstraints.insert(&NewConstraint); | ||
} | ||
|
||
if (NewConstraints == Constraints) | ||
break; | ||
Constraints = std::move(NewConstraints); | ||
} | ||
|
||
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
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 comment
The 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
Constraints
array another time), and the code is simpler this way. So I think I'll keep it this way for now.