package libsail

  1. Overview
  2. Docs
Sail is a language for describing the instruction semantics of processors

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (10)

Authors

  1. A
    Alasdair Armstrong
  2. T
    Thomas Bauereiss
  3. B
    Brian Campbell
  4. S
    Shaked Flur
  5. J
    Jonathan French
  6. K
    Kathy Gray
  7. R
    Robert Norton
  8. C
    Christopher Pulte
  9. P
    Peter Sewell
  10. M
    Mark Wassell

Maintainers

  1. S
    Sail Devs <cl-sail-dev@lists.cam.ac.uk>

Sources

sail-0.20.3.tbz
sha256=0b223ed83f521ad87eaacd88186390fbaf0b944f63c6a04a3ebdf96a1ff5a60c
sha512=83298218175c7a9ff7f0a304021287a2b9c20523cb16e1b8bf0ede81fa8e256a32b309626bc1553a5b46d68e44821524c27a5de0fb2f2d7f013025f61ce76519

doc/libsail/Libsail/Anf/index.html

Module Libsail.AnfSource

The A-normal form (ANF) grammar

The first step in compiling Sail into Jib IR is converting the Sail expression grammar into A-normal form (ANF). Essentially this converts expressions such as f(g(x), h(y)) into something like:

let v0 = g(x) in let v1 = h(x) in f(v0, v1)

Essentially the arguments to every function must be trivial, and complex expressions must be let bound to new variables, or used in a block, assignment, or control flow statement (if, for, and while/until loops). The aexp datatype represents these expressions, while aval represents the trivial values.

The convention is that the type of an aexp is given by last argument to a constructor. It is omitted where it is obvious - for example all for loops have unit as their type. If some constituent part of the aexp has an annotation, the it refers to the previous argument, so in

AE_let (id, typ1, _, body, typ2)

typ1 is the type of the bound identifer, whereas typ2 is the type of the whole let expression (and therefore also the body). The type is represented as a generic parameter 'a, so we can represent both typed and untyped ANF expressions.

See Flanagan et al's The Essence of Compiling with Continuations.

Sourcetype function_id =
  1. | Sail_function of Ast.id
  2. | Newtype_wrapper of Ast.id
  3. | Pure_extern of Ast.id * Ast.typ option
  4. | Extern of Ast.id * Ast.typ option
Sourcetype constructor_id =
  1. | Constructor of Ast.id
  2. | Newtype_wrapper of Ast.id
Sourcetype anf_annot = {
  1. loc : Ast.l;
  2. env : Type_check.Env.t;
  3. uannot : Ast_util.uannot;
}

Each ANF expression has an annotation which contains the location of the original Sail expression, it's typing environment, and the uannot type containing any attributes attached to the original expression.

Sourcetype 'a aexp =
  1. | AE_aux of 'a aexp_aux * anf_annot
Sourceand 'a aexp_aux =
  1. | AE_val of 'a aval
  2. | AE_app of function_id * 'a aval list * 'a
  3. | AE_typ of 'a aexp * 'a
  4. | AE_assign of 'a alexp * 'a aexp
  5. | AE_let of Ast_util.mut * Jib.name * 'a * 'a aexp * 'a aexp * 'a
  6. | AE_block of 'a aexp list * 'a aexp * 'a
  7. | AE_return of 'a aval * 'a
  8. | AE_exit of 'a aval * 'a
  9. | AE_throw of 'a aval * 'a
  10. | AE_if of 'a aval * 'a aexp * 'a aexp * 'a
  11. | AE_field of 'a aval * Ast.id * 'a
  12. | AE_match of 'a aval * ('a apat * 'a aexp * 'a aexp * Ast_util.uannot) list * 'a
  13. | AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp * Ast_util.uannot) list * 'a
  14. | AE_struct_update of 'a aval * 'a aval Ast_compare.Bindings.t * 'a
  15. | AE_for of Jib.name * 'a aexp * 'a aexp * 'a aexp * Ast.order * 'a aexp
  16. | AE_loop of Ast.loop * 'a aexp * 'a aexp
  17. | AE_short_circuit of sc_op * 'a aval * 'a aexp
    (*

    A short circuting operator (either and or or) must have only its first argument reduced to a trivial value in the ANF representation.

    *)
Sourceand sc_op =
  1. | SC_and
  2. | SC_or
Sourceand 'a apat =
  1. | AP_aux of 'a apat_aux * anf_annot
Sourceand 'a apat_aux =
  1. | AP_tuple of 'a apat list
  2. | AP_id of Jib.name * 'a
  3. | AP_global of Ast.id * 'a
  4. | AP_app of constructor_id * 'a apat * 'a
  5. | AP_cons of 'a apat * 'a apat
  6. | AP_as of 'a apat * Jib.name * 'a
  7. | AP_struct of (Ast.id * 'a apat) list * 'a
  8. | AP_vector_concat of (int * 'a apat) list * 'a
  9. | AP_nil of 'a
  10. | AP_wild of 'a
Sourceand 'a aval =
  1. | AV_lit of Ast.lit * 'a
  2. | AV_id of Jib.name * 'a Ast_util.lvar
  3. | AV_abstract of Ast.id * 'a
  4. | AV_ref of Ast.id * 'a Ast_util.lvar
  5. | AV_tuple of 'a aval list
  6. | AV_list of 'a aval list * 'a
  7. | AV_vector of 'a aval list * 'a
  8. | AV_record of 'a aval Ast_compare.Bindings.t * 'a
  9. | AV_cval of Jib.cval * 'a
  10. | AV_undef of 'a

We allow ANF->ANF optimization to insert fragments of Jib IR directly in the ANF grammar via AV_cval. Such fragments must be side-effect free expressions.

Sourceand 'a alexp =
  1. | AL_id of Jib.name * 'a
  2. | AL_addr of Jib.name * 'a
  3. | AL_field of 'a alexp * Ast.id
Sourceval aexp_loc : 'a aexp -> Parse_ast.l

Get the location from an aexp's annotation

Functions for transforming and querying ANF expressions

Sourceval aval_typ : Ast.typ aval -> Ast.typ
Sourceval aexp_typ : Ast.typ aexp -> Ast.typ
Sourceval map_aval : (anf_annot -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp

Map over all values in an ANF expression

Sourceval map_functions : (anf_annot -> function_id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp

Map over all function calls in an ANF expression

Sourceval fold_aexp : ('a aexp -> 'a aexp) -> 'a aexp -> 'a aexp

This function 'folds' an aexp applying the provided function to all leaf subexpressions, then applying the function to their containing expression, and so on recursively in a bottom-up order.

Sourceval aexp_bindings : 'a aexp -> Jib_util.NameSet.t
Sourceval is_pure_aexp : Effects.side_effect_info -> 'a aexp -> bool
Sourceval is_pure_case : Effects.side_effect_info -> ('a apat * 'a aexp * 'a aexp * Ast_util.uannot) -> bool
Sourceval no_shadow : Jib_util.NameSet.t -> 'a aexp -> 'a aexp

Remove all variable shadowing in an ANF expression

Sourceval apat_globals : 'a apat -> (Ast.id * Type_check.Env.t * 'a) list
Sourceval apat_types : 'a apat -> 'a Jib_util.NameMap.t
Sourceval is_dead_aexp : 'a aexp -> bool

Returns true if an ANF expression is dead due to flow typing implying it is unreachable. Note: This function calls SMT.

Compiling to ANF expressions

Sourceval anf_pat : ?global:bool -> Type_check.tannot Ast.pat -> Ast.typ apat

Pretty printing ANF expressions