| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before we just had a map that people would access with localGraph.getSetses[get],
while now it is a call localGraph.getSets(get), which more nicely hides the internal
implementation details.
Also rename getSetses => getSetsMap.
This will allow a later PR to optimize the internals of this API.
This is performance-neutral as far as I can measure. (We do replace a direct read
from a data structure with a call, but the call is in a header and should always get
inlined.)
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
Update the C++20 builder to use Ubuntu 20.04 to catch problems building with its
system compiler. Also fix such a problem in wasm-fuzz-lattices.cpp.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Simplify the monotone analyzer by replacing all the state it used to store in
`BlockState` with a simple vector of lattice elements. Use simple indices to
refer to both blocks and their associated states in the vector. Remove the
ability for transfer functions to control the initial enqueued order of basic
blocks since that was a leaky abstraction. Replace the worklist with a
UniqueDeferredQueue since that has generally proven to be more efficient in
smiilarly contexts, and more importantly, it has a nicer API. Make miscellaneous
simplifications to other code as well.
Delete a few unit tests that exposed the order in which blocks were analyzed
because they printed intermediate results. These tests should be replaced with
tests of analyses' public APIs in the future.
|
| |
|
|
|
|
|
|
|
| |
Factor the static assertions for transfer functions out into a new
transfer-function.h header. The concept requires the `getDependents` method to
return an input range of basic blocks, and to satisfy that requirement, fix up
_indirect_ptr_iterator in cfg-impl.h so that it is a proper iterator. Remove
part of the lattice fuzzer that was using a placeholder transfer function in a
way that does not satisfy the new type constraints; most of that code will be
overhauled in the future anyway.
|
| |
|
| |
Also shorten various names in the implementation to improve readability.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Replace the static assertions ensuring that Lattice types have the necessary
operations with a C++20 concept called `Lattice`. To avoid name conflicts with
the new concept, rename existing type parameters named `Lattice` to `L`. When
not building with C++20, `Lattice` is a macro that resolves to `typename` so the
code continues compiling and has the same behavior, but without any eager checks
of the requirements on lattices.
Add a new C++20 builder to CI to ensure that future changes compile with both
C++17 and C++20. Once we switch to C++20 by default, the new builder can be
removed. Update the lint builder to use a recent clang-format that understands
concepts.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This change introduces StackLattice, a lattice to model stack-related
behavior. It is templated on a separate lattice whose elements model
some property of individual values on the stack. The StackLattice
allows users to access the top of the stack, push abstract values, and
pop them. Comparisons and least upper bound operations are done on a
value by value basis starting from the top of the stack and moving
toward the bottom. This is because it allows stacks from different
scopes to be joined easily.
An application of StackLattice is to model the wasm value stack. The goal
is to organize lattice elements representing individual stack values in a
natural way which mirrors the wasm value stack. Transfer functions operate
on each stack value individually. The stack lattice is an intermediate
structure which is not intended to be directly operated on. Rather, it
simulates the push and pop behavior of instructions.
|
|
|
This change adds a fuzzer which checks the following properties in
abstract interpretation static analyses.
- Transfer Function Monotonicity
- Lattice Element Reflexivity
- Lattice Element Transitivity
- Lattice Element Anti-Symmetry
This is done by randomly generating a module and using its functions as
transfer function inputs, along with randomly generated lattice elements
(states). Lattice element properties are fuzzed from the randomly
generated states also.
|
