================ @@ -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 +// 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 +// 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 && ---------------- martinboehme wrote:
Good call. Done. https://github.com/llvm/llvm-project/pull/70848 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
