Module LineageShape.Cell

Cells correspond to variable fields for which no subfield will be considered by the analysis, either because they semantically have none, or because the abstract domain decides that considering them would lead to too deep or too wide field structures.

A field path of a cell:

If one of these conditions happens, then the cell field path will be truncated before reaching a "scalar" field and the cell will be "abstract".

To make sure that the aforementioned properties hold, one cannot construct cells directly, but should access them through the Summary.fold_cells and Summary.fold_cell_pairs functions.

The lineage graph is built on cells.

type t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
include Sexplib0.Sexpable.S with type t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
val pp : t Fmt.t
val var : t -> IR.Var.t
val field_path : t -> FieldPath.t
val is_abstract : t -> bool
val var_appears_in_source_code : t -> bool
val path_from_origin : origin:VarPath.t -> t -> FieldPath.t

Assuming the cell represents a component of the origin variable path, returns the sub-path subscriptable from this origin path to reach the cell component.

Raises if the cell and the origin path are incompatible (eg. their variables are different or the cell path and the origin path are incomatible).

If the cell is larger than the origin path (eg. because the origin path is longer than the limit and the cells groups it with other paths), returns an empty path. The rationale is that the result of this function can be seen as the subpath which, when extracted from the origin, will cover all the components of that origin stored in the cell. If the cell is larger than the origin then all the components of the origin are in the cell.

Raises if the cell and the origin path are incompatible (eg. their variables are different).

Examples assuming a depth limit of 3:

  • origin: X#a ; cell: X#a#b#c ; result : #b#c
  • origin: X#a#b#c ; cell : X#a#b#c ; result : empty
  • origin: X#a#b#c ; cell : X#a#b#d ; result : raises
  • origin: X#a#b#c ; cell : X#a#b#d ; result : raises
  • origin: X#a#b#c#d ; cell : X#a#b#c ; result : empty