Module Asllib.ASTUtilsSource

This module provides some tools to work on ASL ASTs.

Identifiers utils

Sourcemodule ISet : sig ... end

An extended identifier set.

Sourcemodule IMap : sig ... end

An extended identifier map.

Position utils

Sourceval dummy_pos : Lexing.position

A dummy position.

Sourceval default_version : AST.version

The default version, V1.

Sourceval annotated : 'a -> AST.position -> AST.position -> AST.version -> 'a AST.annotated

annotated v start end version is v with location specified as from start to end and version specified by version.

Sourceval desc : 'a AST.annotated -> 'a

desc v is v.desc

Sourceval add_dummy_annotation : ?version:AST.version -> 'a -> 'a AST.annotated

Add a dummy annotation to a value. The default version is default_version.

Sourceval dummy_annotated : unit AST.annotated

A dummy annotation

Sourceval to_pos : 'a AST.annotated -> unit AST.annotated

Removes the value from an annotated record.

Sourceval add_pos_from_pos_of : ((string * int * int * int) * 'a) -> 'a AST.annotated

add_pos_from_pos_of (__POS_OF__ e) is annotated s s' e where s and s' correspond to e's position in the ocaml file.

Sourceval add_pos_from : 'a AST.annotated -> 'b -> 'b AST.annotated

add_pos_from loc v is v with the location data from loc.

Sourceval add_pos_from_st : 'a AST.annotated -> 'a -> 'a AST.annotated

add_pos_from_st a' a is a with the location from a'.

If both arguments are physically equal, then the result is also physically equal.

Sourceval map2_desc : ('a AST.annotated -> 'b AST.annotated -> 'c) -> 'a AST.annotated -> 'b AST.annotated -> 'c AST.annotated

Folder on two annotated types.

Type utils

Sourceval integer : AST.ty

The ASL unconstrained integer type.

Sourceval integer' : AST.type_desc

integer, without the position annotation.

Sourceval integer_exact : AST.expr -> AST.ty

integer_exact e is the integer type constrained to be equal to e.

Sourceval integer_exact' : AST.expr -> AST.type_desc

integer_exact' e is integer_exact e without the position annotation.

Sourceval boolean : AST.ty

The ASL boolean type.

Sourceval string : AST.ty

The ASL string type.

Sourceval real : AST.ty

The ASL real type.

Sourceval default_t_bits : AST.type_desc
Sourceval default_array_ty : AST.type_desc

Constructor helpers

Sourceval s_pass : AST.stmt

An ASL pass statement.

Sourceval s_then : AST.stmt -> AST.stmt -> AST.stmt

s_then s1 s2 is s1; s2 in ASL.

Sourceval stmt_from_list : AST.stmt list -> AST.stmt

stmt_from_list [s1; ... sn] is s1; ... sn in ASL.

Sourceval expr_of_int : int -> AST.expr

expr_of_int i is the literal expression containing i.

Sourceval literal : AST.literal -> AST.expr

literal v is the expression evaluated to v.

Sourceval var_ : AST.identifier -> AST.expr

var_ x is the expression x.

Builds a binary operation from to subexpressions.

Builds a unary operation from its subexpression.

Sourceval expr_of_z : Z.t -> AST.expr

expr_of_z z is the integer literal for z.

Sourceval zero_expr : AST.expr

The integer literal for 0.

Sourceval one_expr : AST.expr

The integer literal for 1.

Sourceval minus_one_expr : AST.expr

The integer literal for -1.

Sourceval expr_of_rational : Q.t -> AST.expr

expr_of_rational q is the rational literal for q.

Sourceval mul_expr : AST.expr -> AST.expr -> AST.expr

mul_expr e1 e2 is an expression representing e1 * e2.

Sourceval pow_expr : AST.expr -> int -> AST.expr

pow_expr e i is an expression representing e ^ i.

Sourceval div_expr : AST.expr -> Z.t -> AST.expr

div_expr e z is an expression representing e DIV z.

Sourceval add_expr : AST.expr -> (int * AST.expr) -> AST.expr

add_expr e1 (s, e2) is an expression representing e1 + sign(s) * e2. e2 is expected to be non-negative.

Sourceval conj_expr : AST.expr -> AST.expr -> AST.expr

conj_expr e1 e2 is an expression representing e1 && e2.

Sourceval cond_expr : AST.expr -> AST.expr -> AST.expr -> AST.expr

cond_expr e e1 e2 is an expression representing if e then e1 else e2.

Sourceval fresh_var : string -> AST.identifier

fresh_var "doc" is a fresh variable whose name begins with "doc".

Sourceval global_ignored : unit -> AST.identifier

Creates a fresh dummy variable for a global ignored variable.

Sourceval string_starts_with : prefix:string -> string -> bool

A copy of String.starts_with out of stdlib 4.12

Sourceval is_global_ignored : AST.identifier -> bool

is_global_ignored s is true iff s has been created with global_ignored ().

Fields, masks and slices handling

Sourceval mask_from_set_bits_positions : int -> int list -> string

Builds a mask from specified positions.

Sourceval inv_mask : string -> string

Flip all the 0/1 in the mask. Doesn't change the 'x'.

Sourceval slices_to_positions : ('a -> int) -> ('a * 'a) list -> int list

slices_to_positions as_int slices evaluates slices and returns a list of all queried positions in the correct order.

Sourceval canonical_fields : (string * 'a) list -> (string * 'a) list

Sorts the fields of a record to allow an element wise comparison.

Sourceval bitfield_get_name : AST.bitfield -> string

Returns the name of the bitfield in question.

Sourceval bitfield_get_slices : AST.bitfield -> AST.slice list

Returns the slices corresponding to this bitfield.

Sourceval bitfield_get_nested : AST.bitfield -> AST.bitfield list

Returns the list of bitfields listed in the given bitfield and an empty list if it is not a nested bitfield.

Sourceval find_bitfield_opt : string -> AST.bitfield list -> AST.bitfield option

bitfield_find_opt name bfs is Some (bf) if there exists bf in bfs with name, None otherwise.

Sourceval find_bitfields_slices_opt : string -> AST.bitfield list -> AST.slice list option

bitfields_find_slices_opt name bfs is Some (slices) if there exists a bitfield with name name and slices slices.

Sourcemodule Infix : sig ... end

Infix utils.

Equality helpers

Most of those take a cmp_expr argument that is the static analyser expression comparison.

Sourceval expr_equal : (AST.expr -> AST.expr -> bool) -> AST.expr -> AST.expr -> bool
Sourceval literal_equal : AST.literal -> AST.literal -> bool
Sourceval slice_equal : (AST.expr -> AST.expr -> bool) -> AST.slice -> AST.slice -> bool
Sourceval slices_equal : (AST.expr -> AST.expr -> bool) -> AST.slice list -> AST.slice list -> bool
Sourceval constraint_equal : (AST.expr -> AST.expr -> bool) -> AST.int_constraint -> AST.int_constraint -> bool
Sourceval constraints_equal : (AST.expr -> AST.expr -> bool) -> AST.int_constraint list -> AST.int_constraint list -> bool
Sourceval type_equal : (AST.expr -> AST.expr -> bool) -> AST.ty -> AST.ty -> bool
Sourceval array_length_equal : (AST.expr -> AST.expr -> bool) -> AST.array_index -> AST.array_index -> bool
Sourceval bitfield_equal : (AST.expr -> AST.expr -> bool) -> AST.bitfield -> AST.bitfield -> bool
Sourceval bitwidth_equal : (AST.expr -> AST.expr -> bool) -> AST.expr -> AST.expr -> bool

Transformers

Sourceval ldi_of_lexpr : AST.lexpr -> AST.local_decl_item option
Sourceval expr_of_lexpr : AST.lexpr -> AST.expr
Sourceval slice_is_single : AST.slice -> bool
Sourceval slice_as_single : AST.slice -> AST.expr
Sourceval patch : src:AST.t -> patches:AST.t -> AST.t

patch ~src ~patches replaces in src the global identifiers defined by patches.

Sourceval subst_expr : (AST.identifier * AST.expr) list -> AST.expr -> AST.expr

subst_expr substs e replaces the variables used inside e by their associated expression in substs, if any.

Warning: constants and statically-evaluated parts are not changed, for example: E_Slice (E_Var "y", [Slice_Single (E_Var "y")]) will become after subst_expr [("y", E_Var "x")]: E_Slice (E_Var "x", [Slice_Single (E_Var "y")])

Sourceval rename_locals : (AST.identifier -> AST.identifier) -> AST.t -> AST.t

rename_locals f ast is ast where all instances of variables x are replaced with f x.

Sourceval is_simple_expr : AST.expr -> bool

is_simple_expr e is true if e does not contain any call to any other subprogram. It has false negative.

Def/use analysis

Sourceval use_e : AST.expr -> ISet.t -> ISet.t
Sourceval use_ty : AST.ty -> ISet.t -> ISet.t
Sourceval use_decl : AST.decl -> ISet.t -> ISet.t

use_decl d is the set of other declared names required to have in the environment to be able to type-check d.

Sourceval used_identifiers : AST.decl list -> ISet.t
Sourceval used_identifiers_stmt : AST.stmt -> ISet.t
Sourceval identifier_of_decl : AST.decl -> AST.identifier

identifier_of_decl d is the name of the global element defined by d.

Standard functions

Sourceval pair : 'a -> 'b -> 'a * 'b

pair a b is (a, b).

Sourceval pair' : 'b -> 'a -> 'a * 'b

pair' b a is (b, a).

Sourceval list_equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

list_equal elt_equal li1 li2 is true iff li1 and li2 are element-wise equal.

Sourceval list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int

An element wise comparaison for lists.

Sourceval list_cross : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list

list_cross f [a1; ... an] [b1; ... bm] is the list of all f ai bj in a non-specified order.

Sourceval list_take : int -> 'a list -> 'a list

list_take n li is the list of the first n elements of li.

If li has less than n elements, list_take n li is li.

Sourceval list_flat_cross : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list

list_flat_cross f [a1; ... an] [b1; ... bm] is the concatenation of all f ai bj in a non-specified order.

Sourceval list_concat_map : ('a -> 'b list) -> 'a list -> 'b list

list_concat_map f l gives the same result as List.concat (List.map f l). Tail-recursive. Taken from stdlib 4.10.

Sourceval list_fold_lefti : (int -> 'acc -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc

Same as List.fold_left but takes a index.

Sourceval list_fold_left_map : ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list

fold_left_map is a combination of fold_left and map that threads an accumulator through calls to f. Taken from stdlib 4.11.

Sourceval list_coalesce_right : ('a -> 'a -> 'a option) -> 'a list -> 'a list

list_coalesce_right f l applies the coalescing function f to adjacent elements of l, using it to folding l in a right-to-left order.

  • parameter [f]

    is a function that, given two elements, either coalesces them into a single element or returns None, signalling that the elements cannot be coalesced.

Sourceval uniq : 'a list -> 'a list

uniq l returns the unique elements of l, in the order they appear

Sourceval get_first_duplicate : AST.identifier list -> AST.identifier option

get_first_duplicate ids returns None if all identifiers in ids are unique, otherwise it returns Some id where id is the first duplicate.

Sourceval list_is_empty : 'a list -> bool

list_is_empty li is true iff li is empty, false otherwise.

Sourceval list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list

Generalisation of List.split for 3-uples.

Sourceval list_map_split : ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list

Composition of List.map and List.split.

Sourceval list_iterated_op : empty:'a -> ('a -> 'a -> 'a) -> 'a list -> 'a

list_iterated_op ~empty op li computes the iterated binary operation op on the elements of li, with the assumption that op is associative.

If the list li, this function returns empty.

This considers that applying op to 2 elements is longer than iterating on the list, in particular that the complexity of op a b depends on the size of a and b, and the size of op a b increases with the size of a and the size of b.

Sourceval transitive_closure : ISet.t IMap.t -> ISet.t IMap.t

Returns the transitive closure of the graph.

Sourceval get_cycle : ISet.t IMap.t -> AST.identifier list option

get_cycle m is None if the graph whose transition function is given by m is acyclic, Some li if li is a cycle in m.