- Both of these constructs are used to represent structs, classes, and unions;
Clang uses the collective term "record" for these.
- The term "aggregate" in `AggregateStorageLocation` implies that, at some
point, the intention may have been to use it also for arrays, but it don't
think it's possible to use it for arrays. Records and arrays are very
different and therefore need to be modeled differently. Records have a fixed
set of named fields, which can have different type; arrays have a variable
number of elements, but they all have the same type.
- Futhermore, "aggregate" has a very specific meaning in C++
(https://en.cppreference.com/w/cpp/language/aggregate_initialization).
Aggregates of class type may not have any user-declared or inherited
constructors, no private or protected non-static data members, no virtual
member functions, and so on, but we use `AggregateStorageLocations` to model all objects of class type.
In addition, for consistency, we also rename the following:
- `getAggregateLoc()` (in `RecordValue`, formerly known as `StructValue`) to
simply `getLoc()`.
- `refreshStructValue()` to `refreshRecordValue()`
We keep the old names around as deprecated synonyms to enable clients to be migrated to the new names.
Reviewed By: ymandel, xazax.hun
Differential Revision: https://reviews.llvm.org/D156788
There are no remaining uses of this class in the framework.
This patch is part of the ongoing migration to strict handling of value categories (see https://discourse.llvm.org/t/70086 for details).
Reviewed By: ymandel, xazax.hun, gribozavr2
Differential Revision: https://reviews.llvm.org/D155922
This reverts commit 7a72ce98224be76d9328e65eee472381f7c8e7fe.
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
These changes are OK, but they break downstream stuff that needs more time to adapt :-(
This reverts commit 71579569f4399d3cf6bc618dcd449b5388d749cc.
This reverts commit 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1.
This reverts commit 1c3ac8dfa16c42a631968aadd0396cfe7f7778e0.
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
This is the first step in untangling the two current jobs of BoolValue.
=== Desired end-state: ===
- BoolValue will model C++ booleans e.g. held in StorageLocations.
this includes describing uncertainty (e.g. "top" is a Value concern)
- Formula describes analysis-level assertions in terms of SAT atoms.
These can still be linked together: a BoolValue may have a corresponding
SAT atom which is constrained by formulas.
=== Done in this patch: ===
BoolValue is left intact, Formula is just the input type to the
SAT solver, and we build formulas as needed to invoke the solver.
=== Incidental changes to debug string printing: ===
- variables renamed from B0 etc to V0 etc
B0 collides with the names of basic blocks, which is confusing when
debugging flow conditions.
- debug printing of formulas (Formula and Atom) uses operator<<
rather than debugString(), so works with gtest.
Therefore moved out of DebugSupport.h
- Did the same to Solver::Result, and some helper changes to SolverTest,
so that we get useful messages on unit test failures
- formulas are now printed as infix expressions on one line, rather than
wrapped/indented S-exprs. My experience is that this is easier to scan
FCs for small examples, and large ones are unreadable either way.
- most of the several debugString() functions for constraints/results
are unused, so removed them rather than updating tests.
Inlined the one that was actually used into its callsite.
Differential Revision: https://reviews.llvm.org/D153366
The SAT solver imported its constraints by iterating over an unordered DenseSet.
The path taken, and ultimately the runtime, the specific solution found, and
whether it would time out or complete could depend on the iteration order.
Instead, have the caller specify an ordered collection of constraints.
If this is built in a deterministic way, the system can have deterministic
behavior.
(The main alternative is to sort the constraints by value, but this option
is simpler today).
A lot of nondeterminism still appears to be remain in the framework, so today
the solver's inputs themselves are not deterministic yet.
Differential Revision: https://reviews.llvm.org/D153584
std::optional::value() has undesired exception checking semantics and is
unavailable in older Xcode (see _LIBCPP_AVAILABILITY_BAD_OPTIONAL_ACCESS). The
call sites block std::optional migration.
This makes `ninja check-clang` work in the absence of llvm::Optional::value.
Currently, our boolean formulas (`BoolValue`) don't form a lattice, since they
have no Top element. This patch adds such an element, thereby "completing" the
built-in model of bools to be a proper semi-lattice. It still has infinite
height, which is its own problem, but that can be solved separately, through
widening and the like.
Patch 1 for Issue #56931.
Differential Revision: https://reviews.llvm.org/D135397
Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugaring makes
debug output (Environment::dump()) less readable than it could be.
Therefore, it makes sense to keep the sugared representation of a
boolean formula, and desugar it in the solver.
Reviewed By: sgatev, xazax.hun, wyt
Differential Revision: https://reviews.llvm.org/D130519
