Mlang.Bir
type rov_id = Mir.rov_id
module ROVMap = Mir.RuleMap
module VariableMap : MapExt.T with type key = variable
module VariableSet : SetExt.T with type elt = variable
type expression = variable Mir.expression_
type condition_data = variable Mir.condition_data_
type variable_def = variable Mir.variable_def_
and stmt = stmt_kind Pos.marked
and stmt_kind =
| SAssign of variable * variable_def |
| SConditional of expression * stmt list * stmt list |
| SVerifBlock of stmt list |
| SRovCall of rov_id |
| SFunctionCall of function_name * Mir.Variable.t list |
| SPrint of Mast.print_std * variable Mir.print_arg list |
| SIterate of variable * Mir.CatVarSet.t * expression * stmt list |
| SRestore of VariableSet.t
* (variable * Mir.CatVarSet.t * expression) list
* stmt list |
| SRaiseError of Mir.error * string option |
| SCleanErrors |
| SExportErrors |
| SFinalizeErrors |
module FunctionMap : MapExt.T with type key = function_name
This record allows to store statements generated from the m_spec file without modifying the Bir.program
function map. Thus the map reflects the computation strictly as described in M and MPP.
Bir module public interface can then provide access to the statements associated with the declared main function either:
Initialisation of the variables at the Bir
level including unused variables is necessary to the Bir.interpreter
but frowned upon in code generation backends where the data structure size incites to use idiomatic efficient methods of initialisation instead of resting upon a row of assignments.
type program = {
mpp_functions : mpp_function FunctionMap.t; |
targets : target_function Mir.TargetMap.t; |
rules_and_verifs : rule_or_verif ROVMap.t; |
main_function : function_name; |
idmap : Mir.idmap; |
mir_program : Mir.program; |
}
val default_tgv : tgv_id
val var_from_mir : tgv_id -> Mir.Variable.t -> variable
val var_to_mir : variable -> Mir.Variable.t
val map_from_mir_map : tgv_id -> 'a Mir.VariableMap.t -> 'a VariableMap.t
val set_from_mir_dict : tgv_id -> Mir.VariableDict.t -> VariableSet.t
val rule_or_verif_as_statements : rule_or_verif -> stmt list
In order to handle backends with limited function / method capacity, such as Java's 64kB of bytecode per method, class, etc, this funciton allows a program
to be split into chunks of an arbitrary size using the string argument as a suffix to the new function / method name. We piggyback on the existing rules semantics, with these chunks being rule definitions and inserting rule calls in their place
val get_assigned_variables : program -> VariableSet.t
val get_local_variables : program -> unit Mir.LocalVariableMap.t
val get_locals_size : program -> int
val get_used_variables_ :
expression Pos.marked ->
VariableSet.t ->
VariableSet.t
val get_used_variables : expression Pos.marked -> VariableSet.t