Module Asllib.AST

An Abstract Syntax Tree for ASL.

Utils

type version =
  1. | V0
  2. | V1
type position = Lexing.position
type 'a annotated = {
  1. desc : 'a;
  2. pos_start : position;
  3. pos_end : position;
  4. version : version;
}
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

    *)
  24. | BV_CONCAT
    (*

    Bit vector concatenation

    *)

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
  6. | L_Label of string
    (*

    An enumeration label, given by its name.

    *)

Main value type, parametric on its base values

Expressions

type subprogram_type =
  1. | ST_Procedure
    (*

    A procedure is a subprogram without return type, called from a statement.

    *)
  2. | ST_Function
    (*

    A function is a subprogram with a return type, called from an expression.

    *)
  3. | ST_Getter
    (*

    A getter is a special function called with a syntax similar to slices.

    *)
  4. | ST_EmptyGetter
    (*

    An empty getter is a special function called with a syntax similar to a variable. This is relevant only for V0.

    *)
  5. | ST_Setter
    (*

    A setter is a special procedure called with a syntax similar to slice assignment.

    *)
  6. | ST_EmptySetter
    (*

    An empty setter is a special procedure called with a syntax similar to an assignment to a variable. This is relevant only for V0.

    *)
type expr_desc =
  1. | E_Literal of literal
  2. | E_Var of identifier
  3. | E_ATC of expr * ty
    (*

    Asserted type conversion

    *)
  4. | E_Binop of binop * expr * expr
  5. | E_Unop of unop * expr
  6. | E_Call of call
  7. | E_Slice of expr * slice list
  8. | E_Cond of expr * expr * expr
  9. | E_GetArray of expr * expr
    (*

    E_GetArray base index Represents an access to an array given by the expression base at index index. When this node appears in the untyped AST, the index may either be integer-typed or enumeration-typed. When this node appears in the typed AST, the index can only be integer-typed.

    *)
  10. | E_GetEnumArray of expr * expr
    (*

    Access an array with an enumeration index. This constructor is only part of the typed AST.

    *)
  11. | E_GetField of expr * identifier
  12. | E_GetFields of expr * identifier list
  13. | E_GetItem of expr * int
  14. | E_Record of ty * (identifier * expr) list
    (*

    Represents a record or an exception construction expression.

    *)
  15. | E_Tuple of expr list
  16. | E_Array of {
    1. length : expr;
    2. value : expr;
    }
    (*

    Initial value for an array of size length and of content value at each array cell.

    This expression constructor is only part of the typed AST, i.e. it is only built by the type-checker, not any parser.

    *)
  17. | E_EnumArray of {
    1. enum : identifier;
    2. labels : identifier list;
    3. value : expr;
    }
    (*

    Initial value for an array where the index is the enumeration enum, which declares the list of labels labels, and the content of each cell is given by value. enum is only used for pretty-printing.

    This expression constructor is only part of the typed AST, i.e. it is only built by the type-checker, not any parser.

    *)
  18. | E_Arbitrary of ty
  19. | E_Pattern of expr * pattern

Expressions. Parametric on the type of literals.

and expr = expr_desc annotated
and pattern_desc =
  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 pattern = pattern_desc annotated
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.

    *)

Slices define lists of indices into arrays and bitvectors.

All positions mentioned above are inclusive.

and call = {
  1. name : identifier;
  2. params : expr list;
  3. args : expr list;
  4. call_type : subprogram_type;
}

Types

and type_desc =
  1. | T_Int of constraint_kind
  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 inclusive range of these two statically evaluable values.

    *)

A constraint on an integer part.

and constraint_kind =
  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. | PendingConstrained
    (*

    An integer type whose constraint will be inferred during type-checking.

    *)
  4. | Parameterized of uid * identifier
    (*

    A parameterized integer, the default type for parameters of function at compile time, with a unique identifier and the variable bearing its name.

    *)

The constraint_kind constrains an 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 * identifier list
    (*

    An enumeration name and its list of labels.

    *)

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
    (*

    LE_SetArray base index represents a write to an array given by the expression base at index index. When this node appears in the untyped AST, the index may either be integer-typed or enumeration-typed. When this node appears in the typed AST, the index can only be integer-typed.

    *)
  5. | LE_SetEnumArray of lexpr * expr
    (*

    Represents a write to an array with an enumeration index. This constructor is only part of the typed AST.

    *)
  6. | LE_SetField of lexpr * identifier
  7. | LE_SetFields of lexpr * identifier list * (int * int) list
    (*

    LE_SetFields (le, fields, _) unpacks the various fields. Third argument is a type annotation.

    *)
  8. | LE_Destructuring of lexpr list

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_Var of identifier
    (*

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

    let x = 42;

    .

    *)
  2. | LDI_Tuple of identifier list
    (*

    LDI_Tuple names is the tuple declarations of names, for example:

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

    We expect the list to contain at least 2 items.

    *)

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 stmt_desc =
  1. | S_Pass
  2. | S_Seq of stmt * stmt
  3. | S_Decl of local_decl_keyword * local_decl_item * ty option * expr option
  4. | S_Assign of lexpr * expr
  5. | S_Call of call
  6. | S_Return of expr option
  7. | S_Cond of expr * stmt * stmt
  8. | S_Assert of expr
  9. | S_For of {
    1. index_name : identifier;
    2. start_e : expr;
    3. dir : for_direction;
    4. end_e : expr;
    5. body : stmt;
    6. limit : expr option;
    }
  10. | S_While of expr * expr option * stmt
  11. | S_Repeat of stmt * expr * expr option
  12. | 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. It is always None for the untyped AST and never None for the typed AST. The outer option is used to represent the implicit throw, such as throw;.

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

    The stmt option is the optional otherwise guard.

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

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

    newline indicates if the print statement should add an extra new line after printing all the arguments. debug indicates if the print statement has been made using the ASLRef specific function __debug.

    *)
  15. | S_Unreachable
    (*

    The unreachable statement, as an explicit node as it has a specific control-flow behaviour.

    *)
  16. | S_Pragma of identifier * expr list
    (*

    A pragma statement, as an explicit node to be used by tools which need AST level hints.

    *)
and stmt = stmt_desc annotated
and case_alt_desc = {
  1. pattern : pattern;
  2. where : expr option;
  3. stmt : stmt;
}
and case_alt = case_alt_desc 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_body =
  1. | SB_ASL of stmt
    (*

    A normal body of a subprogram

    *)
  2. | SB_Primitive of bool
    (*

    Whether or not this primitive is side-effecting

    *)

Represents the different types of subprogram bodies.

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;
  7. recurse_limit : expr option;
  8. builtin : bool;
    (*

    Builtin functions are treated specially when checking parameters at call sites - see Typing.insert_stdlib_param.

    *)
}

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
  4. | D_Pragma of identifier * expr list
    (*

    A global pragma, as an explicit node to be used by tools which need AST level hints.

    *)

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

type decl = decl_desc annotated
type t = decl list

Main AST type.