Module 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