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 annotated : 'a -> AST.position -> AST.position -> 'a AST.annotated

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

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

desc v is v.desc

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

Add a dummy location annotation to a value.

val dummy_annotated : unit AST.annotated

A dummy location

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 with_pos_from : 'a AST.annotated -> 'b AST.annotated -> 'b AST.annotated

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

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

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 sub-expressions.

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 is_global_ignored : AST.identifier -> bool

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

val constraint_binop : AST.binop -> AST.int_constraint list -> AST.int_constraint list -> AST.int_constraints

constraint_binop PLUS cs1 cs2 is the set of constraints given by the element wise application of PLUS.

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 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 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 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
val scope_equal : AST.scope -> AST.scope -> bool
val scope_compare : AST.scope -> AST.scope -> int

Transformers

val lid_of_lexpr : AST.lexpr -> AST.local_decl_item option
val expr_of_lexpr : AST.lexpr -> AST.expr
val case_to_conds : AST.stmt -> AST.stmt
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 : ISet.t -> AST.expr -> ISet.t
val use_ty : ISet.t -> AST.ty -> ISet.t
val use_constant_decl : ISet.t -> AST.decl -> ISet.t

use_constant_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_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_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.

OCaml

Innovation. Community. Security.