This module provides a framework on top of the normal MIR dataflow framework to simplify the
implementation of analyses that track information about the values stored in certain places.
We are using the term “place” here to refer to a
mir::Place (a place expression) instead of
interpret::Place (a memory location).
The default methods of
ValueAnalysis (prefixed with
super_ instead of
provide some behavior that should be valid for all abstract domains that are based only on the
value stored in a certain place. On top of these default rules, an implementation should
override some of the
handle_ methods. For an example, see
An implementation must also provide a
Map. Before the analysis begins, all places that
should be tracked during the analysis must be registered. During the analysis, no new places
can be registered. The
State can be queried to retrieve the abstract value stored for a
certain place by passing the map.
This framework is currently experimental. Originally, it supported shared references and enum variants. However, it was discovered that both of these were unsound, and especially references had subtle but serious issues. In the future, they could be added back in, but we should clarify the rules for optimizations that rely on the aliasing model first.
The bottom state denotes uninitialized memory. Because we are only doing a sound approximation of the actual execution, we can also use this state for places where access would be UB.
The assignment logic in
State::insert_place_idxassumes that the places are non-overlapping, or identical. Note that this refers to place expressions, not memory locations.
Currently, places that have their reference taken cannot be tracked. Although this would be possible, it has to rely on some aliasing model, which we are not ready to commit to yet. Because of that, we can assume that the only way to change the value behind a tracked place is by direct assignment.
- Children 🔒
- This index uniquely identifies a place.
- The dataflow state for an instance of
- This index uniquely identifies a tracked place and therefore a slot in
- The set of projection elements that can be used by a tracked place.
- Used as the result of an operand or r-value.
- Returns all locals with projections that have their reference or address taken.
fon all direct fields of