Module Bidir.Absint

Abstract interpretation of the bidirectional language. Abstract interpretation is a generalisation of an interpreter. Instead of operating over concrete values, it interprets over sound approximations of the concrete behaviour. This approximation is defined as a lattice: a partially-ordered set equipped with meet and join operators. The meet and join operators each take two lattice points and combine them optimistically (meet) or pessimistically (join). Most commonly, join is invoked where two control-flow paths converge.

The functions in this library take a "spec" argument which parametrises the abstract interpretation. For instance, abstract_run_bidir requires a absint_spec argument containing a absint_spec.join function. This implements the join of the given abstract interpretation lattice.

Lenses for expressions

Simply put, a lens can be though of a first-class left-expression reference. It gives you the ability to load and store a possibly-nested expression. Here, we use it to interact with Types.expr objects, notably including the Types.expr.ETup tuples. This lets us easily use tuples as both right-expressions and left-expressions (i.e., as a destructuring target).

More information can be found on Wikipedia or on the internet (most lens tutorials online will approach the topic from Haskell - in OCaml, we are have access to fewer abstractions so we have to be a bit more explicit).

module StringMap = Lang.Common.StringMap
type 'a lens = ('a StringMap.t -> 'a) option * ('a -> 'a StringMap.t -> 'a StringMap.t)

A lens is a pair of a getter and a setter, parametrised by the value type. This is not a very general lens; it is specific to our use case.

In all cases, the lens extracts from/inserts into a StringMap.t. The getter may be None, indicating that the expression is a Types.expr.EWildcard and cannot be loaded.

type 'a lens_spec = {
  1. into_tuple : 'a list -> 'a;
    (*

    Given a list of abstract values, combines them into a single tupled abstract value.

    *)
  2. outof_tuple : 'a -> 'a list option;
    (*

    Given an abstract value, attempt to extract a list of values of it. This should return None if the given abstract value was not constructed from a tuple.

    *)
  3. wildcard_case : unit -> 'a lens;
    (*

    Defines the lens for the Types.expr.EWildcard case.

    *)
  4. lit_case : Types.value -> 'a lens;
    (*

    Defines the lens for the Types.expr.ELit case, given a particular literal.

    *)
}

Parameters for defining abstract interpretation of an expression to construct a lens. The type parameter is the lattice element type.

val abstract_lens_of_expr : 'a lens_spec -> Types.expr -> 'a lens

Abstract interpretation of an expression to obtain a lens. This function internally handles the interpretation of tuples, using the given lens_spec functions.

The returned lenses may throw in some cases, described below:

  • raises Stdlib.Invalid_argument

    in case of programmer error (e.g., attempt to assign non-tuple or tuple of mismatching length into tuple)

Abstract interpretation of Bidir statements

type ('i, 'a) absint_spec = {
  1. lens : Types.expr -> 'a lens;
    (*

    A function for constructing the lens of an expression. This can be constructed by abstract_lens_of_expr.

    *)
  2. intrinsic_impl : ('i, 'a) Intrinsics.intrinsic_impl;
    (*

    Function implementing the abstract interpretation of intrinsics.

    *)
  3. join : stmt:'i Types.bidir -> 'a -> 'a -> 'a;
    (*

    Join (least upper bound) of two lattice elements. A statement is given for debugging purposes only.

    *)
  4. bot : stmt:'i Types.bidir -> 'a StringMap.t;
    (*

    Bottom (least) element of the lattice. This must be an element of the map lattice, in contrast to join which is an element of the sublattice of map values.

    *)
}

Parameters for the abstract interpretation of Bidir statements. Type parameters are the intrinsic type and the lattice element type.

val abstract_run_bidir : ('i, 'a) absint_spec -> dir:Intrinsics.dir -> 'a StringMap.t -> 'i Types.bidir -> 'a StringMap.t

Performs the abstract interpretation of the bidirectional language, given the absint_spec configuration.