Module `LibASL.Tcheck`Source

Type inference and checker for ASL language

Sourcemodule PE = PPrintEngine

Sourcemodule PC = PPrintCombinators

Sourcemodule PP = Asl_parser_pp

Sourcemodule AST = Asl_ast

Sourcemodule Visitor = Asl_visitor

Sourceval verbose : bool

Exceptions thrown by typechecker

Sourceexception UnknownObject of AST.l * string * string

Sourceexception DoesNotMatch of AST.l * string * string * string

Sourceexception IsNotA of AST.l * string * string

Sourceexception Ambiguous of AST.l * string * string

Sourceexception TypeError of AST.l * string

Sourceexception InternalError of string

AST construction utilities

Sourceval type_unit : AST.ty

Sourceval type_integer : AST.ty

Sourceval type_bool : AST.ty

Sourceval type_real : AST.ty

Sourceval type_string : AST.ty

Sourceval type_bits : AST.expr -> AST.ty

Sourceval type_exn : AST.ty

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

Source

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

Source

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

Source

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

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

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

Source

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

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

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

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

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

Prettyprinting support

Sourceval binop_table : LibASL.Asl_utils.AST.binop Asl_utils.Bindings.t ref

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

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

Sourceval ppp_expr : AST.expr -> string

Very pretty print expression (resugaring expressions)

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

Very pretty print type (resugaring expressions)

Environment representing global and local objects

Sourcetype 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

Sourceval pp_typedef : typedef -> string

Source

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

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

Sourceval pp_funtype : funtype -> PE.document

Sourceval fv_funtype : funtype -> Asl_utils.IdentSet.t

Source

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

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

Sourceval pp_sfuntype : sfuntype -> PE.document

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

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

Source

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

Sourceval funtype_of_sfuntype : sfuntype -> funtype

Sourcemodule Operator1 : sig ... end

Sourcemodule Operators1 : sig ... end

Sourcemodule Operator2 : sig ... end

Sourcemodule Operators2 : sig ... end

Global Environment (aka the Global Symbol Table)

Sourcemodule GlobalEnv : sig ... end

Source

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

Source

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

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

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

Source

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

dereference typedef

Source

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

compare index types

Source

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

Sourcetype 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

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

Get fieldtype information for a record/register type

Source

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

Source

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

Source

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

Source

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)

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

Source

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

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

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

Sourceval 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".

Source

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

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

check that bs => cs

Unification support code

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

Unifier

Source

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.

Source

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

Unify two index types

Source

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

Source

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

Source

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

Source

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

Sourceval mkfresh_funtype : unifier -> funtype -> funtype

Replace all type variables in function type with fresh variables

Sourceval mkfresh_sfuntype : unifier -> sfuntype -> sfuntype

Replace all type variables in setter function type with fresh variables

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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'

Source

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'

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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'

Source

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

Source

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

Source

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

Source

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

Source

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

Typecheck list of types

Source

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

Typecheck type

Typecheck L-expressions

Source

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

Source

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

Source

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

Source

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

Typecheck list of statements

Source

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'

Source

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

Source

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'

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

Typecheck statement

Typecheck function definition

Source

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)

Source

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

Source

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

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

Typecheck setter procedure argument

Source

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

Typecheck list of setter procedure arguments

Source

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

Source

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

Source

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

Typecheck instruction encoding

Source

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

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

Source

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

Typecheck instruction decode pattern match

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

Typecheck instruction decode body

Source

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

Typecheck instruction decode case alternative

Source

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

Source

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

Typecheck global declaration, extending environment as needed

Source

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.

Sourceval env0 : GlobalEnv.t

Overall typechecking environment shared by all invocations of typechecker

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Tcheck/index.html

Module `LibASL.Tcheck`Source

Exceptions thrown by typechecker

AST construction utilities

Prettyprinting support

Environment representing global and local objects

Global Environment (aka the Global Symbol Table)

Field typechecking support

Environment (aka the Local+Global Symbol Table)

Unification

Expression simplification

Z3 support code

Unification support code

Type Unification

Disambiguation of functions and operators

Typecheck expressions

Typecheck L-expressions

Typecheck statements

Typecheck function definition

Typecheck instruction

Typecheck global declaration

package asli

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Tcheck/index.html

Module LibASL.TcheckSource

Exceptions thrown by typechecker

AST construction utilities

Prettyprinting support

Environment representing global and local objects

Global Environment (aka the Global Symbol Table)

Field typechecking support

Environment (aka the Local+Global Symbol Table)

Unification

Expression simplification

Z3 support code

Unification support code

Type Unification

Disambiguation of functions and operators

Typecheck expressions

Typecheck L-expressions

Typecheck statements

Typecheck function definition

Typecheck instruction

Typecheck global declaration

Module `LibASL.Tcheck`Source