| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
Implement binary and text parsing and printing of shared basic heap types and
incorporate them into the type hierarchy.
To avoid the massive amount of code duplication that would be necessary if we
were to add separate enum variants for each of the shared basic heap types, use
bit 0 to indicate whether the type is shared and replace `getBasic()` with
`getBasic(Unshared)`, which clears that bit. Update all the use sites to record
whether the original type was shared and produce shared or unshared output
without code duplication.
|
| |
|
|
|
|
|
|
|
|
|
| |
Class template argument deduction (CTAD) is a C++17 feature that allows
variables to be declared with class template types without specifying the
template parameters. Deduction guides are a mechanism by which template authors
can control how the template parameters are inferred when CTAD is used. The
Google style guide prohibits the use of CTAD except where template authors opt
in to supporting it by providing explicit deduction guides. For compatibility
with users adhering to Google style, set the compiler flag to check this
condition and add the necessary deduction guides to make the compiler happy
again.
|
| |
|
|
|
|
|
|
|
| |
Previously, modifying a single vector element of a `Shared<Vector>` element
required materializing a full vector to do the join. When there is just a single
element to update, materializing all the other elements with bottom value is
useless work. Add a `Vector<L>::SingletonElement` utility that represents but
does not materialize a vector with a single non-bottom element and allow it to
be passed to `Vector<L>::join`. Also update `Shared` and `Inverted` so that
`SingletonElement` joins still work on vectors wrapped in those other lattices.
|
| |
|
|
|
|
|
| |
Remove the ability to represent the top element of the stack lattice since it
isn't necessary. Also simplify the element type to be a simple vector, update
the lattice method implementations to be more consistent with implementations in
other lattices, and make the tests more consistent with the tests for other
lattices.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The analysis framework stores a separate lattice element for each basic block
being analyzed to represent the program state at the beginning of the block.
However, in many analyses a significant portion of program state is not
flow-sensitive, so does not benefit from having a separate copy per block. For
example, an analysis might track constraints on the types of locals that do not
vary across blocks, so it really only needs a single copy of the constrains for
each local. It would be correct to simply duplicate the state across blocks
anyway, but it would not be efficient.
To make it possible to share a single copy of a lattice element across basic
blocks, introduce a `Shared<L>` lattice. Mathematically, this lattice represents
a single ascending chain in the underlying lattice and its elements are ordered
according to sequence numbers corresponding to positions in that chain.
Concretely, though, the `Shared<L>` lattice only ever materializes a single,
monotonically increasing element of `L` and all of its elements provide access
to that shared underlying element.
`Shared<L>` will let us get the benefits of having mutable shared state in the
concrete implementation of analyses without losing the benefits of keeping those
analyses expressible purely in terms of the monotone framework.
|
| |
|
|
|
|
| |
Many of the lattice tests were essentially copy-pasted from one lattice to the
next because they all tested isomorphic subsets of the various lattices,
specifically in the shape of a diamond. Refactor the code so that all lattices
that have tests of this shape use the same utility test functions.
|
| |
|
|
|
|
| |
Add a lattice that is a thin wrapper around `wasm::Type` giving it the interface
of a lattice. As usual, `Type::unreachable` is the bottom element, but unlike in
the underlying API, we uniformly treat `Type::none` as the top type so that we
have a proper lattice.
|
| |
|
|
|
|
|
| |
This lattice combines any number of other lattices into a single lattice whose
elements are tuples of elements of the other lattices. This will be one of the
most important lattices in the analysis framework because it will be used to
combine information about different parts of the program, e.g. locals and the
value stack, into a single lattice.
|
| |
|
|
|
|
|
|
|
|
| |
The vector lattice is nearly identical to the array lattice, except that the
size of the elements is specified at runtime when the lattice object is created
rather than at compile time. The code and tests are largely copy-pasted and
fixed up from the array implementation, but there are a couple differences.
First, initializing vector elements does not need the template magic used to
initialize array elements. Second, the obvious implementations of join and meet
do not work for vectors of bools because they might be specialized to be bit
vectors, so we need workarounds for that particular case.
|
| |
|
|
|
| |
The elements of `Array<L, N>` lattice are arrays of length `N` of elements of
`L`, compared pairwise with each other. This lattice is a concrete
implementation of what would be written L^N with pen and paper.
|
| |
|
|
|
|
| |
Since these methods, which operate on lattice elements, moved to the lattice
types, it no longer makes much sense for their parameters to be called `self`
and `other`. Rename them to `joinee` and `joiner` for joins and `meetee` and
`meeter` for meets.
|
| |
|
|
|
|
|
|
|
|
| |
Implement new `RandomLattice` and `RandomFullLattice` utilities that are
lattices randomly created from other lattices. By recursively using themselves
as the parameter lattices for lattices like `Inverted` and `Lift`, these random
lattices can become arbitrarily nested.
Decouple the checking of lattice properties from the checking of transfer
function properties by creating a new, standalone `checkLatticeProperties`
function.
|
| |
|
|
| |
This lattice "lifts" another lattice by inserting a new bottom element
underneath it.
|
| |
|
|
|
| |
Given a type `T`, `Flat<T>` is the lattice where none of the values of `T` are
comparable except with themselves, but they are all greater than a common bottom
element not in `T` and less than a common top element also not in `T`.
|
| |
|
|
|
|
| |
The FullLattice concept extends the base Lattice with `getTop` and `meet`
operations. The `Inverted` lattice uses these operations to reverse the order of
an arbitrary full lattice, for example to create a lattice of integers ordered
by `>` rather than by `<`.
|
| |
|
| |
Implement a generic lattice template for integral types ordered by `<`.
|
| |
|
|
|
| |
This is a lattice with two elements: `false` is bottom and `true` is top.
Add a new gtest file for testing lattices.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lattice (#6035)
In general, the operation of taking the least upper bound of two lattice
elements may depend on some state stored in the lattice object rather than in
the elements themselves. To avoid forcing the elements to be larger and more
complicated in that case (by storing a parent pointer back to the lattice), move
the least upper bound operation to make it a method of the lattice rather than
the lattice element. This is also more consistent with where we put e.g. the
`compare` method.
While we are at it, rename `makeLeastUpperBound` to `join`, which is much
shorter and nicer. Usually we avoid using esoteric mathematical jargon like
this, but "join" as a normal verb actually describes the operation nicely, so I
think it is ok in this case.
|
| |
|
| |
Also shorten various names in the implementation to improve readability.
|
|
|
Move the powerset lattices out of lattice.h, which now only contains the Lattice
concept, to their own dedicated header in a new analysis/lattices directory.
|
