Module bytecode::read_write_set_analysis

The read/write set analysis is a compositional analysis that starts from the leaves of the call graph and analyzes each procedure once. The result is a summary of the abstract paths read/written by each procedure and the value(s) returned by the procedure.

When the analysis encounters a call, it fetches the summary for the callee and applies it to the current state. This logic (implemented in apply_summary) is by far the most complex part of themove analysis.

Structs

• ReadWriteSetProcessor
• ReadWriteSetState
  A record of the glocals and locals accessed by the current procedure + the address values stored by locals or globals
• ReadWriteSetStateDisplay
• SpecializedReadWriteSetState
  A abstract ReadWriteSetState that has been (fully or partially) concretized by substituting concrete values. Represented as a separate type to avoid confusion/comparison with an overapproximate ReadWriteSet

Functions

• format_read_write_set_annotation
  Return a string representation of the summary for target
• get_read_write_set