Module value_analysis

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 an interpret::Place (a memory location).

The default methods of ValueAnalysis (prefixed with super_ instead of handle_) 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 ConstAnalysis.

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.

Notes

• 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_idx assumes 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.

Structs

• Children 🔒
• Map
  Partial mapping from Place to PlaceIndex, where some places also have a ValueIndex.
• PlaceCollector 🔒
• PlaceIndex
  This index uniquely identifies a place.
• PlaceInfo 🔒
  This is the information tracked for every PlaceIndex and is stored by Map.
• StateData
  See State.
• ValueAnalysisWrapper
• ValueIndex 🔒
  This index uniquely identifies a tracked place and therefore a slot in State.

Enums

• State
  The dataflow state for an instance of ValueAnalysis.
• TrackElem
  The set of projection elements that can be used by a tracked place.
• ValueOrPlace
  Used as the result of an operand or r-value.

Traits

• ValueAnalysis

Functions

• debug_with_context 🔒
• debug_with_context_rec 🔒
• excluded_locals
  Returns all locals with projections that have their reference or address taken.
• iter_fields
  Invokes f on all direct fields of ty.