Module move_stackless_bytecode::access_path

This file contains an abstraction of concrete access paths, which are canonical names for a particular cell in memory. Some examples of concrete paths are:

• 0x7/M::T/f (i.e., the field f of the M::T resource stored at address 0x7
• Formal(0)/[2] (i.e., the value stored at index 2 of the array bound the 0th formal of the current procedure) An abstract path is similar; it consists of the following components:
• A root, which is either an abstract address or a local
• Zero or more offsets, where an offset is a field, an unknown vector index, or an abstract struct type

Abstract addresses are a set containing constants and abstract access paths read from the environment. For example, in the following Move code:

 struct S { f: u64 }

 fun foo(x: S) {
   let a = if (*) { 0x1 } else { *&x.f }
    ... // program point 1
 }

, the value of a will be { 0x1, Footprint(x/f) } at program point 1.

Structs

AbsAddrDisplay

AbsStructType

Fully qualified type identifier base bound to type actuals types

AbsStructTypeDisplay

AccessPath

A unique identifier for a memory cell: root followed by zero or more offsets

AccessPathDisplay

AddrDisplay

GlobalKey

Abstraction of a key of type addr::ty in global storage

GlobalKeyDisplay

OffsetDisplay

RootDisplay

Enums

Addr

Building block for abstraction of addresses

Offset

Offset of an access path: either a field, vector index, or global key

Root

Root of an access path: a global, local, or return variable

Traits

AccessPathMap

Trait for a domain that can be viewed as a partial map from access paths to values and values can be deleted using their access paths

FootprintDomain

Trait for an abstract domain that can represent footprint values

Type Definitions

AbsAddr

Abstraction of an address: non-empty set of constant or footprint address values