package herdtools7

  1. Overview
  2. Docs

This module provides some tools to work on ASL ASTs.

Identifiers utils

module ISet : sig ... end

An extended identifier set.

module IMap : sig ... end

An extended identifier map.

Position utils

val dummy_pos : Lexing.position

A dummy position.

val default_version : AST.version

The default version, V1.

val 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.

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

desc v is v.desc

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

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

val dummy_annotated : unit AST.annotated

A dummy annotation

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

Removes the value from an annotated record.

val 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.

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

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

val 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.

val 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

val integer : AST.ty

The ASL unconstrained integer type.

val integer' : AST.type_desc

integer, without the position annotation.

val integer_exact : AST.expr -> AST.ty

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

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

integer_exact' e is integer_exact e without the position annotation.

val boolean : AST.ty

The ASL boolean type.

val string : AST.ty

The ASL string type.

val real : AST.ty

The ASL real type.

val default_t_bits : AST.type_desc
val default_array_ty : AST.type_desc

Constructor helpers

val s_pass : AST.stmt

An ASL pass statement.

val s_then : AST.stmt -> AST.stmt -> AST.stmt

s_then s1 s2 is s1; s2 in ASL.

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

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

val expr_of_int : int -> AST.expr

expr_of_int i is the literal expression containing i.

val literal : AST.literal -> AST.expr

literal v is the expression evaluated to v.

val var_ : AST.identifier -> AST.expr

var_ x is the expression x.

val binop : AST.binop -> AST.expr -> AST.expr -> AST.expr

Builds a binary operation from to subexpressions.

val unop : AST.unop -> AST.expr -> AST.expr

Builds a unary operation from its subexpression.

val expr_of_z : Z.t -> AST.expr

expr_of_z z is the integer literal for z.

val zero_expr : AST.expr

The integer literal for 0.

val one_expr : AST.expr

The integer literal for 1.

val minus_one_expr : AST.expr

The integer literal for -1.

val expr_of_rational : Q.t -> AST.expr

expr_of_rational q is the rational literal for q.

val mul_expr : AST.expr -> AST.expr -> AST.expr

mul_expr e1 e2 is an expression representing e1 * e2.

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

pow_expr e i is an expression representing e ^ i.

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

div_expr e z is an expression representing e DIV z.

val 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.

val conj_expr : AST.expr -> AST.expr -> AST.expr

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

val 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.

val fresh_var : string -> AST.identifier

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

val global_ignored : unit -> AST.identifier

Creates a fresh dummy variable for a global ignored variable.

val string_starts_with : prefix:string -> string -> bool

A copy of String.starts_with out of stdlib 4.12

val 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

val mask_from_set_bits_positions : int -> int list -> string

Builds a mask from specified positions.

val inv_mask : string -> string

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

val 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.

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

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

val bitfield_get_name : AST.bitfield -> string

Returns the name of the bitfield in question.

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

Returns the slices corresponding to this bitfield.

val 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.

val 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.

val 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.

module Infix : sig ... end

Infix utils.

Equality helpers

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

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

Transformers

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

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

val 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")])

val 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.

val 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

val use_e : AST.expr -> ISet.t -> ISet.t
val use_ty : AST.ty -> ISet.t -> ISet.t
val 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.

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

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

Standard functions

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

pair a b is (a, b).

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

pair' b a is (b, a).

val 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.

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

An element wise comparaison for lists.

val 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.

val 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.

val 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.

val 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.

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

Same as List.fold_left but takes a index.

val 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.

val 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.

val uniq : 'a list -> 'a list

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

val 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.

val list_is_empty : 'a list -> bool

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

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

Generalisation of List.split for 3-uples.

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

Composition of List.map and List.split.

val 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.

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

Returns the transitive closure of the graph.

val 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.

OCaml

Innovation. Community. Security.