Module Asllib.AST

An Abstract Syntax Tree for ASL.

Utils

type position = Lexing.position
type 'a annotated = {
  1. desc : 'a;
  2. pos_start : position;
  3. pos_end : position;
}
type identifier = string

Type of local identifiers in the AST.

type uid = int

Unique identifiers

Operations

type unop =
  1. | BNOT
    (*

    Boolean inversion

    *)
  2. | NEG
    (*

    Integer or real negation

    *)
  3. | NOT
    (*

    Bitvector bitwise inversion

    *)

Operations on base value of arity one.

type binop =
  1. | AND
    (*

    Bitvector bitwise and

    *)
  2. | BAND
    (*

    Boolean and

    *)
  3. | BEQ
    (*

    Boolean equivalence

    *)
  4. | BOR
    (*

    Boolean or

    *)
  5. | DIV
    (*

    Integer division

    *)
  6. | DIVRM
    (*

    Inexact integer division, with rounding towards negative infinity.

    *)
  7. | EOR
    (*

    Bitvector bitwise exclusive or

    *)
  8. | EQ_OP
    (*

    Equality on two base values of same type

    *)
  9. | GT
    (*

    Greater than for int or reals

    *)
  10. | GEQ
    (*

    Greater or equal for int or reals

    *)
  11. | IMPL
    (*

    Boolean implication

    *)
  12. | LT
    (*

    Less than for int or reals

    *)
  13. | LEQ
    (*

    Less or equal for int or reals

    *)
  14. | MOD
    (*

    Remainder of integer division

    *)
  15. | MINUS
    (*

    Substraction for int or reals or bitvectors

    *)
  16. | MUL
    (*

    Multiplication for int or reals or bitvectors

    *)
  17. | NEQ
    (*

    Non equality on two base values of same type

    *)
  18. | OR
    (*

    Bitvector bitwise or

    *)
  19. | PLUS
    (*

    Addition for int or reals or bitvectors

    *)
  20. | POW
    (*

    Exponentiation for ints

    *)
  21. | RDIV
    (*

    Division for reals

    *)
  22. | SHL
    (*

    Shift left for ints

    *)
  23. | SHR
    (*

    Shift right for ints

    *)

Operations on base value of arity two.

Literals

Literals are the values written straight into ASL specifications. There is only literal constructors for a few concepts that could be encapsulated into an ASL value.

type literal =
  1. | L_Int of Z.t
  2. | L_Bool of bool
  3. | L_Real of Q.t
  4. | L_BitVector of Bitvector.t
  5. | L_String of string

Main value type, parametric on its base values

Expressions

type expr_desc =
  1. | E_Literal of literal
  2. | E_Var of identifier
  3. | E_CTC of expr * ty
  4. | E_Binop of binop * expr * expr
  5. | E_Unop of unop * expr
  6. | E_Call of identifier * expr list * (identifier * expr) list
  7. | E_Slice of expr * slice list
  8. | E_Cond of expr * expr * expr
  9. | E_GetArray of expr * expr
  10. | E_GetField of expr * identifier
  11. | E_GetFields of expr * identifier list
  12. | E_Record of ty * (identifier * expr) list
    (*

    Represents a record or an exception construction expression.

    *)
  13. | E_Concat of expr list
  14. | E_Tuple of expr list
  15. | E_Unknown of ty
  16. | E_Pattern of expr * pattern

Expressions. Parametric on the type of literals.

and expr = expr_desc annotated
and pattern =
  1. | Pattern_All
  2. | Pattern_Any of pattern list
  3. | Pattern_Geq of expr
  4. | Pattern_Leq of expr
  5. | Pattern_Mask of Bitvector.mask
  6. | Pattern_Not of pattern
  7. | Pattern_Range of expr * expr
  8. | Pattern_Single of expr
  9. | Pattern_Tuple of pattern list
and slice =
  1. | Slice_Single of expr
    (*

    Slice_Single i is the slice of length 1 at position i.

    *)
  2. | Slice_Range of expr * expr
    (*

    Slice_Range (j, i) denotes the slice from i to j - 1.

    *)
  3. | Slice_Length of expr * expr
    (*

    Slice_Length (i, n) denotes the slice starting at i of length n.

    *)
  4. | Slice_Star of expr * expr
    (*

    Slice_Start (factor, length) denotes the slice starting at factor * length of length n.

    *)

Indexes an array, a bitvector.

All position mentionned above are included.

Types

and type_desc =
  1. | T_Int of int_constraints
  2. | T_Bits of expr * bitfield list
  3. | T_Real
  4. | T_String
  5. | T_Bool
  6. | T_Enum of identifier list
  7. | T_Tuple of ty list
  8. | T_Array of array_index * ty
  9. | T_Record of field list
  10. | T_Exception of field list
  11. | T_Named of identifier
    (*

    A type variable.

    *)

Type descriptors.

and int_constraint =
  1. | Constraint_Exact of expr
    (*

    Exactly this value, as given by a statically evaluable expression.

    *)
  2. | Constraint_Range of expr * expr
    (*

    In the range of these two statically evaluable values.

    *)

A constraint on an integer part.

and int_constraints =
  1. | UnConstrained
    (*

    The normal, unconstrained, integer type.

    *)
  2. | WellConstrained of int_constraint list
    (*

    An integer type constrained from ASL syntax: it is the union of each constraint in the list.

    *)
  3. | UnderConstrained of uid * identifier
    (*

    An under-constrained integer, the default type for parameters of function at compile time, with a unique identifier and the variable bearing its name.

    *)

The int_constraints constraints the integer type to a certain subset.

and bitfield =
  1. | BitField_Simple of identifier * slice list
    (*

    A name and its corresponding slice

    *)
  2. | BitField_Nested of identifier * slice list * bitfield list
    (*

    A name, its corresponding slice and some nested bitfields.

    *)
  3. | BitField_Type of identifier * slice list * ty
    (*

    A name, its corresponding slice and the type of the bitfield.

    *)

Represent static slices on a given bitvector type.

and array_index =
  1. | ArrayLength_Expr of expr
    (*

    An integer expression giving the length of the array.

    *)
  2. | ArrayLength_Enum of identifier * int
    (*

    An enumeration name and its length.

    *)

The type of indexes for an array.

and field = identifier * ty

A field of a record-like structure.

and typed_identifier = identifier * ty

An identifier declared with its type.

Statements

type lexpr_desc =
  1. | LE_Discard
  2. | LE_Var of identifier
  3. | LE_Slice of lexpr * slice list
  4. | LE_SetArray of lexpr * expr
  5. | LE_SetField of lexpr * identifier
  6. | LE_SetFields of lexpr * identifier list
  7. | LE_Destructuring of lexpr list
  8. | LE_Concat of lexpr list * int list option
    (*

    LE_Concat (les, _) unpacks the various lexpr. Second argument is a type annotation.

    *)

Type of left-hand side of assignments.

and lexpr = lexpr_desc annotated
type local_decl_keyword =
  1. | LDK_Var
  2. | LDK_Constant
  3. | LDK_Let
type local_decl_item =
  1. | LDI_Discard
    (*

    LDI_Discard is the ignored local_decl_item, for example used in:

    let - = 42;

    .

    *)
  2. | LDI_Var of identifier
    (*

    LDI_Var x is the variable declaration of the variable x, used for example in: 

    let x = 42;

    .

    *)
  3. | LDI_Tuple of local_decl_item list
    (*

    LDI_Tuple ldis is the tuple declarations of the items in ldis, used for example in: 

    let (x, y, -, z) = (1, 2, 3, 4);

    Note that a the list here must be at least 2 items long.

    *)
  4. | LDI_Typed of local_decl_item * ty
    (*

    LDI_Typed (ldi, t) declares the item ldi with type t.

    *)

A left-hand side of a declaration statement. In the following example of a declaration statement, (2, 3, 4): (integer, integer, integer {0..32}) is the local declaration item:

  let (x, -, z): (integer, integer, integer {0..32}) = (2, 3, 4);
type for_direction =
  1. | Up
  2. | Down

Statements. Parametric on the type of literals in expressions.

type version =
  1. | V0
  2. | V1
type stmt_desc =
  1. | S_Pass
  2. | S_Seq of stmt * stmt
  3. | S_Decl of local_decl_keyword * local_decl_item * expr option
  4. | S_Assign of lexpr * expr * version
  5. | S_Call of identifier * expr list * (identifier * expr) list
  6. | S_Return of expr option
  7. | S_Cond of expr * stmt * stmt
  8. | S_Case of expr * case_alt list
  9. | S_Assert of expr
  10. | S_For of identifier * expr * for_direction * expr * stmt
  11. | S_While of expr * stmt
  12. | S_Repeat of stmt * expr
  13. | S_Throw of (expr * ty option) option
    (*

    The ty option is a type annotation added by the type-checker to be matched later with the catch guards. The bigger option is to represent the implicit throw, such as throw;.

    *)
  14. | S_Try of stmt * catcher list * stmt option
    (*

    The stmt option is the optional otherwise guard.

    *)
  15. | S_Print of {
    1. args : expr list;
    2. debug : bool;
    }
    (*

    A call to print, as an explicit node as it does not require type-checking.

    *)
and stmt = stmt_desc annotated
and case_alt = (pattern * stmt) annotated
and catcher = identifier option * ty * stmt

The optional name of the matched exception, the guard type and the statement to be executed if the guard matches.

Top-level declarations

type subprogram_type =
  1. | ST_Procedure
  2. | ST_Function
  3. | ST_Getter
  4. | ST_Setter
type subprogram_body =
  1. | SB_ASL of stmt
  2. | SB_Primitive
type func = {
  1. name : identifier;
  2. parameters : (identifier * ty option) list;
  3. args : typed_identifier list;
  4. body : subprogram_body;
  5. return_type : ty option;
  6. subprogram_type : subprogram_type;
}

Function types in the AST. For the moment, they represent getters, setters, functions, procedures and primitives.

type global_decl_keyword =
  1. | GDK_Constant
  2. | GDK_Config
  3. | GDK_Let
  4. | GDK_Var

Declaration keyword for global storage elements.

type global_decl = {
  1. keyword : global_decl_keyword;
  2. name : identifier;
  3. ty : ty option;
  4. initial_value : expr option;
}

Global declaration type

type decl_desc =
  1. | D_Func of func
  2. | D_GlobalStorage of global_decl
  3. | D_TypeDecl of identifier * ty * (identifier * field list) option

Declarations, ie. top level statement in a asl file.

type decl = decl_desc annotated
type t = decl list

Main AST type.

type scope =
  1. | Scope_Local of identifier * uid
    (*

    Local scope of a function given by its name and an uid of the call

    *)
  2. | Scope_Global of bool
    (*

    Global runtime scope, with whether it was during initialization or not

    *)

A scope is an unique identifier of the calling site.