Module Mlang.Mir
type execution_number
=
{
rule_number : int;
Written in the name of the rule or verification condition
seq_number : int;
Index in the sequence of the definitions in the rule
pos : Pos.t;
}
type cat_computed
=
|
Base
|
GivenBack
module CatCompSet : SetExt.T with type T.elt = cat_computed
type cat_variable
=
|
CatInput of Mlang.StrSet.t
|
CatComputed of CatCompSet.t
val pp_cat_variable : Stdlib.Format.formatter -> cat_variable -> unit
val compare_cat_variable : cat_variable -> cat_variable -> int
module CatVarSet : SetExt.T with type T.elt = cat_variable
module CatVarMap : MapExt.T with type T.key = cat_variable
type variable
=
{
name : string Pos.marked;
The position is the variable declaration
execution_number : execution_number;
The number associated with the rule of verification condition in which the variable is defined
alias : string option;
Input variable have an alias
id : variable_id;
descr : string Pos.marked;
Description taken from the variable declaration
attributes : Mast.variable_attribute list;
origin : variable option;
If the variable is an SSA duplication, refers to the original (declared) variable
cats : CatVarSet.t;
is_table : int option;
}
type local_variable
=
{
id : int;
}
type typ
=
|
Real
Type of MIR values
type literal
=
|
Float of float
|
Undefined
type func
=
MIR only supports a restricted set of functions
type 'variable expression_
=
|
Unop of Mast.unop * 'variable expression_ Pos.marked
|
Comparison of Mast.comp_op Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
|
Binop of Mast.binop Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
|
Index of 'variable Pos.marked * 'variable expression_ Pos.marked
|
Conditional of 'variable expression_ Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
|
FunctionCall of func * 'variable expression_ Pos.marked list
|
Literal of literal
|
Var of 'variable
|
LocalVar of local_variable
|
Error
|
LocalLet of local_variable * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
type expression
= variable expression_
module VariableMap : MapExt.T with type T.key = variable
MIR programs are just mapping from variables to their definitions, and make a massive use of
VariableMap
.
module VariableDict : Dict.S with type key = variable_id and type elt = variable
module LocalVariableMap : sig ... end
module IndexMap : IntMap.T
type 'variable index_def
=
|
IndexTable of 'variable expression_ Pos.marked IndexMap.t
|
IndexGeneric of 'variable * 'variable expression_ Pos.marked
type 'variable variable_def_
=
|
SimpleVar of 'variable expression_ Pos.marked
|
TableVar of int * 'variable index_def
|
InputVar
type variable_def
= variable variable_def_
type io
=
|
Input
|
Output
|
Regular
type 'variable variable_data_
=
{
var_definition : 'variable variable_def_;
var_typ : typ option;
The typing info here comes from the variable declaration in the source program
var_io : io;
}
type variable_data
= variable variable_data_
type rov_id
=
|
RuleID of int
|
VerifID of int
type 'a domain
=
{
dom_id : Mlang.Mast.DomainId.t;
dom_names : Mlang.Mast.DomainIdSet.t;
dom_by_default : bool;
dom_min : Mlang.Mast.DomainIdSet.t;
dom_max : Mlang.Mast.DomainIdSet.t;
dom_data : 'a;
}
type rule_domain_data
=
{
rdom_computable : bool;
}
type rule_domain
= rule_domain_data domain
type rule_data
=
{
rule_domain : rule_domain;
rule_chain : (string * rule_domain) option;
rule_vars : (variable_id * variable_data) list;
rule_number : rov_id Pos.marked;
}
type error_descr
=
{
kind : string Pos.marked;
major_code : string Pos.marked;
minor_code : string Pos.marked;
description : string Pos.marked;
isisf : string Pos.marked;
}
Errors are first-class objects
type error
=
{
name : string Pos.marked;
The position is the variable declaration
id : int;
Each variable has an unique ID
descr : error_descr;
Description taken from the variable declaration
typ : Mast.error_typ;
}
type verif_domain_data
=
{
vdom_auth : CatVarSet.t;
}
type verif_domain
= verif_domain_data domain
type 'variable condition_data_
=
{
cond_seq_id : int;
cond_number : rov_id Pos.marked;
cond_domain : verif_domain;
cond_expr : 'variable expression_ Pos.marked;
cond_error : error * 'variable option;
cond_cats : int CatVarMap.t;
}
type condition_data
= variable condition_data_
type idmap
= variable list Mlang.Pos.VarNameToID.t
We translate string variables into first-class unique
Mir.variable
, so we need to keep a mapping between the two. A name is mapped to a list of variables because variables can be redefined in different rules
type exec_pass
=
{
exec_pass_set_variables : literal Pos.marked VariableMap.t;
}
type program
=
{
program_var_categories : Pos.t Mlang.StrMap.t Pos.marked CatVarMap.t;
program_rule_domains : rule_domain Mlang.Mast.DomainIdMap.t;
program_verif_domains : verif_domain Mlang.Mast.DomainIdMap.t;
program_chainings : rule_domain Mlang.Mast.ChainingMap.t;
program_vars : VariableDict.t;
A static register of all variables that can be used during a calculation
program_rules : rule_data RuleMap.t;
Definitions of variables, some may be removed during optimization passes
program_conds : condition_data RuleMap.t;
Conditions are affected to dummy variables containing informations about actual variables in the conditions
program_idmap : idmap;
program_exec_passes : exec_pass list;
}
module Variable : sig ... end
module LocalVariable : sig ... end
Local variables don't appear in the M source program but can be introduced by let bindings when translating to MIR. They should be De Bruijn indices but instead are unique globals identifiers out of laziness.
module Error : sig ... end
val false_literal : literal
val true_literal : literal
val num_of_rule_or_verif_id : rov_id -> int
val same_execution_number : execution_number -> execution_number -> bool
val find_var_name_by_alias : program -> string Pos.marked -> string
val map_expr_var : ('v -> 'v2) -> 'v expression_ -> 'v2 expression_
val fold_expr_var : ('a -> 'v -> 'a) -> 'a -> 'v expression_ -> 'a
val map_var_def_var : ('v -> 'v2) -> 'v variable_def_ -> 'v2 variable_def_
val map_cond_data_var : ('v -> 'v2) -> 'v condition_data_ -> 'v2 condition_data_
val cond_cats_to_set : int CatVarMap.t -> CatVarSet.t
val fold_vars : (variable -> variable_data -> 'a -> 'a) -> program -> 'a -> 'a
val map_vars : (variable -> variable_data -> variable_data) -> program -> program
val compare_execution_number : execution_number -> execution_number -> int
val find_var_definition : program -> variable -> rule_data * variable_data
val is_candidate_valid : execution_number -> execution_number -> bool -> bool
val sort_by_lowest_exec_number : Variable.t -> Variable.t -> int
val get_max_var_sorted_by_execution_number : (Variable.t -> Variable.t -> int) -> string -> Variable.t list Mlang.Pos.VarNameToID.t -> Variable.t
val fresh_rule_num : unit -> int
val initial_undef_rule_id : rov_id
val find_var_by_name : program -> string Pos.marked -> variable
Get a variable for a given name or alias, because of SSA multiple variables share a name or alias. If an alias is provided, the variable returned is that with the lowest execution number. When a name is provided, then the variable with the highest execution number is returned.
val is_dummy_variable : Variable.t -> bool
val find_vars_by_io : program -> io -> VariableDict.t
Returns a VariableDict.t containing all the variables that have a given io type, only one variable per name is entered in the VariableDict.t, this function chooses the one with the highest execution number
val mast_to_catvars : 'a CatVarMap.t -> string Pos.marked list Pos.marked -> CatVarSet.t
val mast_to_catvar : 'a CatVarMap.t -> string Pos.marked list Pos.marked -> cat_variable