package asli

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Exceptions thrown by typechecker
AST construction utilities
Prettyprinting support
Environment representing global and local objects
Unification
Disambiguation of functions and operators
Typecheck expressions
Typecheck L-expressions
Typecheck statements
Typecheck function definition
Typecheck instruction
Typecheck global declaration

package asli

asli.libASL
- LibASL
  - Asl_ast
    
    Id
    
    StringSet
  - Asl_parser
  - Asl_parser_pp
  - Asl_utils
    
    Bindings
    
    IdentSet
    
    assignedVarsClass
    
    callsClass
    
    equivalences
    
    freevarClass
    
    localsClass
    
    replaceExprClass
    
    resugarClass
    
    substClass
    
    substFunClass
    
    typesClass
  - Asl_visitor
    
    aslVisitor
    
    nopAslVisitor
  - Cpu
  - Elf
  - Eval
    
    Env
    
    ImpDefs
  - Lexer
  - Lexersupport
  - LoadASL
  - Primops
    
    ImmutableArray
    
    Index
    
    Pages
  - Tcheck
    
    Env
    
    GlobalEnv
    
    Operator1
    
    Operator2
    
    Operators1
    
    Operators2
    
    unifier
  - Utils
  - Value
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

Type inference and checker for ASL language

module PE = PPrintEngine

module PC = PPrintCombinators

module PP = Asl_parser_pp

module AST = Asl_ast

module Visitor = Asl_visitor

val verbose : bool

Exceptions thrown by typechecker

exception UnknownObject of AST.l * string * string

exception DoesNotMatch of AST.l * string * string * string

exception IsNotA of AST.l * string * string

exception Ambiguous of AST.l * string * string

exception TypeError of AST.l * string

exception InternalError of string

AST construction utilities

val type_unit : AST.ty

val type_integer : AST.ty

val type_bool : AST.ty

val type_real : AST.ty

val type_string : AST.ty

val type_bits : AST.expr -> AST.ty

val type_exn : AST.ty

val type_bitsK : AST.intLit -> LibASL.Asl_utils.AST.ty

val mk_eq_int : 
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

Construct expression "eq_int(x, y)"

val mk_add_int : 
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

Construct expression "add_int(x, y)"

val mk_sub_int : 
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

Construct expression "sub_int(x, y)"

val mk_add_ints : LibASL.Asl_utils.AST.expr list -> LibASL.Asl_utils.AST.expr

Construct expression "(0 + x1) + ... + xn"

val mk_concat_ty : 
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty

val mk_concat_tys : LibASL.Asl_utils.AST.ty list -> LibASL.Asl_utils.AST.ty

val slice_width : LibASL.Asl_utils.AST.slice -> LibASL.Asl_utils.AST.expr

val slices_width : LibASL.Asl_utils.AST.slice list -> LibASL.Asl_utils.AST.expr

val ixtype_basetype : LibASL.Asl_utils.AST.ixtype -> LibASL.Asl_utils.AST.ty

Prettyprinting support

val binop_table : LibASL.Asl_utils.AST.binop Asl_utils.Bindings.t Stdlib.ref

Table of binary operators used for resugaring expressions when printing error messages.

val add_binop : AST.binop -> AST.ident -> unit

val ppp_expr : AST.expr -> string

Very pretty print expression (resugaring expressions)

val ppp_type : LibASL.Asl_utils.AST.ty -> string

Very pretty print type (resugaring expressions)

Environment representing global and local objects

type typedef =

| Type_Builtin of AST.ident
| Type_Forward
| Type_Record of (AST.ty * AST.ident) list
| Type_Enumeration of AST.ident list
| Type_Abbreviation of AST.ty

val pp_typedef : typedef -> string

type funtype =
  LibASL.Asl_utils.AST.ident
  * bool
  * LibASL.Asl_utils.AST.ident list
  * LibASL.Asl_utils.AST.expr list
  * (LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident) list
  * LibASL.Asl_utils.AST.ty

val ft_id : funtype -> LibASL.Asl_utils.AST.ident

val pp_funtype : funtype -> PE.document

val fv_funtype : funtype -> Asl_utils.IdentSet.t

type sfuntype =
  LibASL.Asl_utils.AST.ident
  * LibASL.Asl_utils.AST.ident list
  * LibASL.Asl_utils.AST.expr list
  * LibASL.Asl_utils.AST.sformal list
  * LibASL.Asl_utils.AST.ty

val sft_id : sfuntype -> LibASL.Asl_utils.AST.ident

val pp_sfuntype : sfuntype -> PE.document

val sformal_var : AST.sformal -> LibASL.Asl_utils.AST.ident

val sformal_type : AST.sformal -> LibASL.Asl_utils.AST.ty

val formal_of_sformal : 
  LibASL.Asl_utils.AST.sformal ->
  LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident

val funtype_of_sfuntype : sfuntype -> funtype

module Operator1 : sig ... end

module Operators1 : sig ... end

module Operator2 : sig ... end

module Operators2 : sig ... end

Global Environment (aka the Global Symbol Table)

module GlobalEnv : sig ... end

val subst_consts_expr : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

val subst_consts_type : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty

val isConstant : GlobalEnv.t -> LibASL.Asl_utils.AST.ident -> bool

val removeConsts : GlobalEnv.t -> Asl_utils.IdentSet.t -> Asl_utils.IdentSet.t

val derefType : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty

dereference typedef

val cmp_ixtype : 
  LibASL.Asl_utils.AST.ixtype ->
  LibASL.Asl_utils.AST.ixtype ->
  bool

compare index types

val cmp_type : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  bool

structural match on two types - ignoring the dependent type part

Field typechecking support

type fieldtypes =

| FT_Record of (AST.ty * AST.ident) list
| FT_Register of (LibASL.Asl_utils.AST.slice list * AST.ident) list

Field accesses can be either record fields or fields of registers

This type captures the information needed to typecheck either of these

a list of fieldname/type pairs for records
a list of fieldname/slice pairs for registers

val typeFields : GlobalEnv.t -> LibASL.Asl_utils.AST.l -> AST.ty -> fieldtypes

Get fieldtype information for a record/register type

val get_recordfield : 
  LibASL.Asl_utils.AST.l ->
  (AST.ty * AST.ident) list ->
  AST.ident ->
  LibASL.Asl_utils.AST.ty

Get fieldtype information for a named field of a record

val get_regfield_info : 
  LibASL.Asl_utils.AST.l ->
  (LibASL.Asl_utils.AST.slice list * AST.ident) list ->
  AST.ident ->
  LibASL.Asl_utils.AST.slice list

Get fieldtype information for a named field of a slice

val get_regfield : 
  LibASL.Asl_utils.AST.l ->
  (LibASL.Asl_utils.AST.slice list * AST.ident) list ->
  AST.ident ->
  LibASL.Asl_utils.AST.slice list * LibASL.Asl_utils.AST.ty

Get named field of a register and calculate type

val get_regfields : 
  LibASL.Asl_utils.AST.l ->
  (LibASL.Asl_utils.AST.slice list * AST.ident) list ->
  AST.ident list ->
  LibASL.Asl_utils.AST.slice list * LibASL.Asl_utils.AST.ty

Get named fields of a register and calculate type of concatenating them

Environment (aka the Local+Global Symbol Table)

type implicitVars = (LibASL.Asl_utils.AST.ident * LibASL.Asl_utils.AST.ty) list

val declare_implicits : 
  LibASL.Asl_utils.AST.l ->
  implicitVars ->
  LibASL.Asl_utils.AST.stmt list

module Env : sig ... end

Unification

Expression simplification

Perform simple constant folding of expression

It's primary role is to enable the 'DIV' hacks in z3_of_expr which rely on shallow syntactic transforms. It has a secondary benefit of sometimes causing constraints to become so trivial that we don't even need to invoke Z3 which gives a performance benefit.

val simplify_expr : LibASL.Asl_utils.AST.expr -> LibASL.Asl_utils.AST.expr

val simplify_type : LibASL.Asl_utils.AST.ty -> LibASL.Asl_utils.AST.ty

Perform simple constant folding of expressions within a type

Z3 support code

Convert ASL expression to Z3 expression. This only copes with a limited set of operations: ==, +, -, * and DIV. (It is possible that we will need to extend this list in the future but it is sufficient for the current ASL specifications.)

The support for DIV is not sound - it is a hack needed to cope with the way ASL code is written and generally needs a side condition that the division is exact (no remainder).

ufs is a mutable list of conversions used to handle subexpressions that cannot be translated. We treat such subexpressions as uninterpreted functions and add them to the 'ufs' list so that we can reason that "F(x) == F(x)" without knowing "F".

val z3_of_expr : 
  Z3.context ->
  (LibASL.Asl_utils.AST.expr * Z3.Expr.expr) list Stdlib.ref ->
  LibASL.Asl_utils.AST.expr ->
  Z3.Expr.expr

val check_constraints : AST.expr list -> AST.expr list -> bool

check that bs => cs

Unification support code

class unifier : LibASL.Asl_utils.AST.l -> AST.expr list -> object ... end

Unifier

val with_unify : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  (unifier -> 'a) ->
  AST.expr Asl_utils.Bindings.t * 'a

Create a fresh unifier, invoke a function that uses the unifier and check that the constraints are satisfied. Returns the synthesized bindings and result of function

Type Unification

Notes on how type inference works:

we use structural matching (ignoring the dependent type) to disambiguate each binop/unop/function/procedure call/getter/setter

as we construct each TApply node,
we insert fresh type variables $0, $1, ... for each of the type arguments (these are things we are going to solve for)
unification generates two kinds of constraints: 1. bindings for type variables whenever unification requires "$i == e" or "e == $i" for some type variable $i 2. constraints where there are multiple bindings for a single variable 3. constraints on type variables whenever unification requires "e1 == e2" where e1 is not a variable

after scanning an entire assignment/expression, we check: 1. do we have at least one binding for each variable? 2. are the bindings consistent with the constraints? Note that we could potentially give better (more localized) type errors if we check for consistency as we go along and if we check that a variable is bound as soon as the result type could not possibly involve the variable. (e.g., when checking "(e1 == e2 && Q) || R", any type variables associated with the equality check do not impact the && or || because "boolean" does not have any type parameters.)

Note that there is a choice of what type arguments to add to a function

bits(N) ZeroExtend(bits(M) x, integer N)

We can either:

add only the missing information "M" In effect, we are saying that missing type parameters are implicit parameters that are added by the type inference process and that the "type parameters" are basically just value expressions that are added by type inference.
add type arguments for both "M" and "N". In effect we are saying that type parameters are distinct from value parameters and we are in the strange situation that a function could have both a value parameter M and a type parameter N and they might be bound to different (but equivalent) arguments. This is what archex does.

val unify_ixtype : 
  unifier ->
  LibASL.Asl_utils.AST.ixtype ->
  LibASL.Asl_utils.AST.ixtype ->
  unit

Unify two index types

val unify_type : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  unit

Unify two types

This performs a structural match on two types - ignoring the dependent type part

val unify_subst_e : 
  AST.expr Asl_utils.Bindings.t ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

Apply substitutions to an expression

val unify_subst_le : 
  AST.expr Asl_utils.Bindings.t ->
  LibASL.Asl_utils.AST.lexpr ->
  LibASL.Asl_utils.AST.lexpr

Apply substitutions to an L-expression

val unify_subst_ty : 
  AST.expr Asl_utils.Bindings.t ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty

Apply substitutions to a type

val mkfresh_funtype : unifier -> funtype -> funtype

Replace all type variables in function type with fresh variables

val mkfresh_sfuntype : unifier -> sfuntype -> sfuntype

Replace all type variables in setter function type with fresh variables

val check_type : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  unit

Check that ty2 is a subtype of ty1: ty1 >= ty2

val check_type_exact : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  unit

Check that ty1 is identical to ty2

Disambiguation of functions and operators

val reportChoices : 
  LibASL.Asl_utils.AST.l ->
  string ->
  string ->
  LibASL.Asl_utils.AST.ty list ->
  funtype list ->
  unit

Generate error message when function disambiguation fails

val isCompatibleFunction : 
  GlobalEnv.t ->
  bool ->
  LibASL.Asl_utils.AST.ty list ->
  funtype ->
  bool

Check whether a list of function argument types is compatible with the type of a function.

One function type is compatible with another if they have the same number of arguments and each argument has the same base type

val chooseFunction : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.l ->
  string ->
  string ->
  bool ->
  LibASL.Asl_utils.AST.ty list ->
  funtype list ->
  funtype option

Disambiguate a function name based on the number and type of arguments

val isCompatibleSetterFunction : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.ty list ->
  sfuntype ->
  bool

Check whether a list of function argument types is compatible with the type of a setter function.

One function type is compatible with another if they have the same number of arguments and each argument has the same base type

val chooseSetterFunction : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.l ->
  string ->
  AST.ident ->
  LibASL.Asl_utils.AST.ty list ->
  sfuntype list ->
  sfuntype option

Disambiguate a setter function name based on the number and type of arguments

val instantiate_fun : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  funtype ->
  LibASL.Asl_utils.AST.expr list ->
  LibASL.Asl_utils.AST.ty list ->
  LibASL.Asl_utils.AST.ident
  * LibASL.Asl_utils.AST.expr list
  * LibASL.Asl_utils.AST.ty

Instantiate type of function using unifier 'u'

val instantiate_sfun : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  sfuntype ->
  LibASL.Asl_utils.AST.expr list ->
  LibASL.Asl_utils.AST.ty list ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ident * LibASL.Asl_utils.AST.expr list

Instantiate type of setter function using unifier 'u'

val tc_apply : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  string ->
  LibASL.Asl_utils.AST.ident ->
  LibASL.Asl_utils.AST.expr list ->
  LibASL.Asl_utils.AST.ty list ->
  LibASL.Asl_utils.AST.ident
  * LibASL.Asl_utils.AST.expr list
  * LibASL.Asl_utils.AST.ty

Disambiguate and typecheck application of a function to a list of arguments

val tc_unop : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  AST.unop ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ident
  * LibASL.Asl_utils.AST.expr list
  * LibASL.Asl_utils.AST.ty

Disambiguate and typecheck application of a unary operator to argument

val tc_binop : 
  GlobalEnv.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  AST.binop ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.ident
  * LibASL.Asl_utils.AST.expr list
  * LibASL.Asl_utils.AST.ty

Disambiguate and typecheck application of a binary operator to arguments

Typecheck expressions

val check_var : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ident ->
  LibASL.Asl_utils.AST.ident * LibASL.Asl_utils.AST.ty

Lookup a variable in environment

val tc_exprs : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.expr list ->
  (LibASL.Asl_utils.AST.expr * LibASL.Asl_utils.AST.ty) list

Typecheck list of expressions

val check_expr : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr

Typecheck expression and check that it is a subtype of ty

val tc_e_elsif : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.e_elsif ->
  LibASL.Asl_utils.AST.e_elsif * LibASL.Asl_utils.AST.ty

Typecheck 'if c then expr'

val tc_slice : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.slice ->
  LibASL.Asl_utils.AST.slice * LibASL.Asl_utils.AST.ty

Typecheck bitslice indices

val tc_pattern : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.pattern ->
  LibASL.Asl_utils.AST.pattern

Typecheck pattern against type ty

val tc_slice_expr : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  AST.expr ->
  (LibASL.Asl_utils.AST.slice * LibASL.Asl_utils.AST.ty) list ->
  LibASL.Asl_utils.AST.expr * LibASL.Asl_utils.AST.ty

Typecheck bitslice syntax This primarily consists of disambiguating between array indexing and bitslicing Note that this function is almost identical to tc_slice_lexpr

val tc_expr : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.expr ->
  LibASL.Asl_utils.AST.expr * LibASL.Asl_utils.AST.ty

Typecheck expression

val tc_types : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty list ->
  AST.ty list

Typecheck list of types

val tc_type : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  AST.ty ->
  LibASL.Asl_utils.AST.ty

Typecheck type

Typecheck L-expressions

val tc_slice_lexpr : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  AST.lexpr ->
  (LibASL.Asl_utils.AST.slice * LibASL.Asl_utils.AST.ty) list ->
  LibASL.Asl_utils.AST.lexpr * LibASL.Asl_utils.AST.ty

Typecheck bitslice syntax

This primarily consists of disambiguating between array indexing and bitslicing Note that this function is almost identical to tc_slice_expr

val tc_lexpr2 : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  AST.lexpr ->
  LibASL.Asl_utils.AST.lexpr * LibASL.Asl_utils.AST.ty

Typecheck left hand side of expression in context where type of right hand side is not yet known

Typecheck statements

val tc_lexpr : 
  Env.t ->
  unifier ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.lexpr ->
  LibASL.Asl_utils.AST.lexpr * implicitVars

Typecheck left hand side of expression and check that rhs type 'ty' is compatible. Return set of variables assigned to in this expression

val tc_stmts : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.stmt list ->
  AST.stmt list

Typecheck list of statements

val tc_s_elsif : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.s_elsif ->
  LibASL.Asl_utils.AST.s_elsif

Typecheck 'if expr then stmt'

val tc_alt : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ty ->
  LibASL.Asl_utils.AST.alt ->
  LibASL.Asl_utils.AST.alt

Typecheck case alternative

val tc_catcher : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.catcher ->
  LibASL.Asl_utils.AST.catcher

Typecheck exception catcher 'when expr stmt'

val tc_stmt : Env.t -> LibASL.Asl_utils.AST.stmt -> LibASL.Asl_utils.AST.stmt

Typecheck statement

Typecheck function definition

val tc_body : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.stmt list ->
  LibASL.Asl_utils.AST.stmt list

Typecheck function body (list of statements)

val tc_argument : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  (LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident) ->
  LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident

Typecheck function argument

val tc_arguments : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  (LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident) list ->
  (LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident) list

Typecheck list of function arguments

val tc_sformal : Env.t -> LibASL.Asl_utils.AST.l -> AST.sformal -> AST.sformal

Typecheck setter procedure argument

val tc_sformals : 
  Env.t ->
  LibASL.Asl_utils.AST.l ->
  AST.sformal list ->
  AST.sformal list

Typecheck list of setter procedure arguments

val addFunction : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ident ->
  bool ->
  Asl_utils.IdentSet.t ->
  (LibASL.Asl_utils.AST.ty * LibASL.Asl_utils.AST.ident) list ->
  LibASL.Asl_utils.AST.ty ->
  funtype

Add function definition to environment

val addSetterFunction : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.ident ->
  Asl_utils.IdentSet.t ->
  LibASL.Asl_utils.AST.sformal list ->
  LibASL.Asl_utils.AST.ty ->
  sfuntype

Typecheck instruction

val tc_encoding : 
  Env.t ->
  AST.encoding ->
  AST.encoding * (LibASL.Asl_utils.AST.ident * LibASL.Asl_utils.AST.ty) list

Typecheck instruction encoding

val tc_decode_slice : 
  int Asl_utils.Bindings.t ->
  LibASL.Asl_utils.AST.l ->
  LibASL.Asl_utils.AST.decode_slice ->
  LibASL.Asl_utils.AST.decode_slice * int

Typecheck bitslice of instruction opcode

val check_width : LibASL.Asl_utils.AST.l -> int -> int -> unit

val tc_decode_pattern : 
  LibASL.Asl_utils.AST.l ->
  int ->
  AST.decode_pattern ->
  AST.decode_pattern

Typecheck instruction decode pattern match

val tc_decode_body : GlobalEnv.t -> AST.decode_body -> AST.decode_body

Typecheck instruction decode body

val tc_decode_alt : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.l ->
  int list ->
  AST.decode_alt ->
  AST.decode_alt

Typecheck instruction decode case alternative

val tc_decode_case : 
  GlobalEnv.t ->
  AST.l ->
  AST.instr_field list ->
  AST.decode_case ->
  AST.decode_case

Typecheck instruction decode case

Typecheck global declaration

val tc_declaration : 
  GlobalEnv.t ->
  LibASL.Asl_utils.AST.declaration ->
  LibASL.Asl_utils.AST.declaration list

Typecheck global declaration, extending environment as needed

val genPrototypes : 
  LibASL.Asl_utils.AST.declaration list ->
  LibASL.Asl_utils.AST.declaration list * LibASL.Asl_utils.AST.declaration list

Generate function prototype declarations.

This allows function declarations within a translation unit to be placed in any order.

val env0 : GlobalEnv.t

Overall typechecking environment shared by all invocations of typechecker

val tc_declarations : 
  bool ->
  LibASL.Asl_utils.AST.declaration list ->
  LibASL.Asl_utils.AST.declaration list

Typecheck a list of declarations - main entrypoint into typechecker