Module Checker.Location

the module for locations, a compile-time notion of memory locations. This is the object that the borrow checker use to represent and track values at compile-time This module also contains some important location-related helper data structures.

type location = {
root : root;
path : path;
}

location is a compile-time notion of memory locations. locations start with a root, and can be refined further via a path. Example:

            x   .field1.field2
      root ^^^
      path      ^^^^^^^^^^^^^^

            ( *    y  ) .field
      root        ^^^
      path   ^^^        ^^^^^^
and root =
| Var of IR.variable
| Abs of abstract_loc

roots of locations can either be concrete program variables (via Var), or abstract locations (via Abs), which are abstract tokens that represent a set of other locations.

Locations starting with program variables (Var) are called "concrete", and locations starting with abstract locations (Abs) are called "abstract".

The Var constructor accepts an abstract location rather than a variable name. This helps avoid issues with name clash. A mapping between variable names and the corresponding abstract locations should be maintained elsewhere

and abstract_loc = private int
and path = IR.path
val absloc_generator : < generate : abstract_loc; reset : unit; >
val gen_absloc : unit -> abstract_loc

generate a new fresh abstract location. A wrapper of absloc_generator

val var_to_loc : IR.variable -> location

create a location starting with a program variable with an empty path

val abs_to_loc : abstract_loc -> location

create a location starting with an abstract location with an empty path

val lvalue_to_loc : IR.lvalue -> location

create a location corresponding to a lvalue

type relation =
| Eq
| Irr
| Lt of path
| Gt of path

the relation between two locations or paths. The intuition behind the notion of "large" and "small" is how much a location covers. Detailed meaning of each case is:

  • a `Eq` b means that a and b are exactly identical
  • a `Irr` b means that a and b are disjoint
  • a `Lt path` b means that a refers to a part of b, i.e. a = b.path
  • a `Gt path` b means that b refers to a part of a, i.e. b = a.path
val compare_path : path -> path -> relation

calculate the relation between two paths

val compare : location -> location -> relation

calculate the relation between two locations

module PathMap : sig ... end

the PathMap submodule provides special maps with paths as keys

module Map : sig ... end

the Map submodule provides special maps with locations as keys

module ConstrSet : sig ... end

the ConstrSet submodule provides a data type for tracking constraints on abstract locations. Let l1, l2 be two locations. Here l2 must start with an abstract location, hence represents a set of locations. Now constraints are of the form l1 in l2, meaning that the set of locations denoted by l2 must contain l1. l2 is called the superset and l1 is called the subset in the constraint