Files
clang-p2996/clang/lib/Analysis/FlowSensitive/Arena.cpp
Sam McCall fc9821a877 Reland "[dataflow] Add dedicated representation of boolean formulas"
This reverts commit 7a72ce9822.

Test problems were due to unspecified order of function arg evaluation.

Reland "[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)"

This properly frees the Value hierarchy from managing boolean formulas.

We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.

We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.

For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.

The data structures around flow conditions are updated:
- flow condition tokens are Atom, rather than AtomicBoolValue*
- conditions are Formula, rather than BoolValue
Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.

The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.

Differential Revision: https://reviews.llvm.org/D153469
2023-07-07 11:58:33 +02:00

99 lines
3.0 KiB
C++

//===-- Arena.cpp ---------------------------------------------------------===//
//
// 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/Arena.h"
#include "clang/Analysis/FlowSensitive/Value.h"
namespace clang::dataflow {
static std::pair<const Formula *, const Formula *>
canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
auto Res = std::make_pair(&LHS, &RHS);
if (&RHS < &LHS) // FIXME: use a deterministic order instead
std::swap(Res.first, Res.second);
return Res;
}
const Formula &Arena::makeAtomRef(Atom A) {
auto [It, Inserted] = AtomRefs.try_emplace(A);
if (Inserted)
It->second =
&Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
return *It->second;
}
const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
auto [It, Inserted] =
Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
if (Inserted)
It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
return *It->second;
}
const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
auto [It, Inserted] =
Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
if (Inserted)
It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
return *It->second;
}
const Formula &Arena::makeNot(const Formula &Val) {
auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
if (Inserted)
It->second = &Formula::create(Alloc, Formula::Not, {&Val});
return *It->second;
}
const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
auto [It, Inserted] =
Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
if (Inserted)
It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
return *It->second;
}
const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
auto [It, Inserted] =
Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
if (Inserted)
It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
return *It->second;
}
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
auto [It, Inserted] = IntegerLiterals.try_emplace(Value, nullptr);
if (Inserted)
It->second = &create<IntegerValue>();
return *It->second;
}
BoolValue &Arena::makeBoolValue(const Formula &F) {
auto [It, Inserted] = FormulaValues.try_emplace(&F);
if (Inserted)
It->second = (F.kind() == Formula::AtomRef)
? (BoolValue *)&create<AtomicBoolValue>(F)
: &create<FormulaBoolValue>(F);
return *It->second;
}
} // namespace clang::dataflow