diff --git a/include/arrow_spec.h b/include/arrow_spec.h
index 66c5dd29140d370c7bee6ced4a503ca5ba2ee234..99acd13829296f240bcc73d864872e611371aca2 100644
--- a/include/arrow_spec.h
+++ b/include/arrow_spec.h
@@ -37,8 +37,8 @@ extern void _arrow_dealloc (struct _arrow_mem *);
*/
/*@ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
- struct _arrow_mem_ghost mem_out,
- _Bool out) =
+ _Bool out,
+ struct _arrow_mem_ghost mem_out) =
out == mem_in._reg._first
&& (mem_in._reg._first ? (mem_out._reg._first == 0)
: (mem_out._reg._first == mem_in._reg._first));
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index fe72e4c3752bb4b87a414ed39239c9ab972ae89a..2c355abeabde974b647160635e2a92f8d9dddc74 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -258,40 +258,32 @@ let pp_memory_pack_aux' ?i fmt =
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
-let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
- (name, inputs, locals, outputs, mem_in, mem_out) =
+let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
+ (name, vars, mem_in, mem_out) =
let stateless = fst (get_stateless_status m) in
- fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
+ fprintf fmt "%s_transition%a(@[<hov>%t%a%t@])" name
(pp_print_option pp_print_int)
i
(fun fmt -> if not stateless then pp_mem_in fmt mem_in)
(pp_comma_list
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
- pp_input)
- inputs
- (pp_print_option (fun fmt _ ->
- pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
- i
+ pp_var)
+ vars
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
- (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
- outputs
-let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
- (t, mem_in, mem_out) =
- pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
- (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
+let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
+ pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_var fmt
+ (t.tname.node_id, t.tvars, mem_in, mem_out)
let pp_transition_aux' ?i m =
- pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
+ pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl
let pp_transition_aux'' ?i m =
- pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
+ pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
+ (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
let pp_transition' m =
- pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
-
-let pp_transition'' m =
- pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
+ pp_transition m pp_print_string pp_print_string pp_var_decl
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
@@ -329,15 +321,15 @@ module PrintSpec = struct
let pp_expr :
type a.
- ?output:bool ->
+ ?test_output:bool ->
machine_t ->
ident ->
formatter ->
(value_t, a) expression_t ->
unit =
- fun ?(output = false) m mem fmt -> function
+ fun ?(test_output = false) m mem fmt -> function
| Val v ->
- pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
+ pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
| Tag t ->
pp_print_string fmt t
| Var v ->
@@ -346,7 +338,7 @@ module PrintSpec = struct
pp_reg mem fmt r
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
- let output, mem_update =
+ let test_output, mem_update =
match mode with
| InstrMode _ ->
true, false
@@ -355,12 +347,12 @@ module PrintSpec = struct
| _ ->
false, false
in
- let pp_expr :
- type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
- fun ?output fmt e -> pp_expr ?output m mem_out fmt e
+ let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
+ =
+ fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
in
match p with
- | Transition (f, inst, i, inputs, locals, outputs, r, mems, insts) ->
+ | Transition (f, inst, i, vars, r, mems, insts) ->
let pp_mem_in, pp_mem_out =
match inst with
| None ->
@@ -373,8 +365,8 @@ module PrintSpec = struct
else pp_access' fmt (mem_in, inst)),
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
in
- pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
- (f, inputs, locals, outputs, mem_in', mem_out')
+ pp_transition_aux ?i m pp_mem_in pp_mem_out (pp_expr test_output) fmt
+ (f, vars, mem_in', mem_out')
| Reset (_f, inst, r) ->
pp_ite
(pp_c_val m mem_in (pp_c_var_read m))
@@ -555,7 +547,7 @@ let pp_transition_def m fmt t =
(pp_transition m
(pp_machine_decl' ~ghost:true)
(pp_machine_decl' ~ghost:true)
- (pp_local m) (pp_local m))
+ (pp_local m))
(PrintSpec.pp_spec TransitionMode m))
fmt
((t, (name, mem_in), (name, mem_out)), t.tformula)
@@ -593,8 +585,7 @@ let pp_transition_footprint_lemma m fmt t =
let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
let tr ?mems ?insts () =
Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
- (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
- (vdecls_to_vals t.toutputs)
+ (vdecls_to_vals t.tvars)
in
if not (mems_empty && insts_empty) then
pp_acsl
@@ -610,10 +601,8 @@ let pp_transition_footprint_lemma m fmt t =
( t,
( (m.mname.node_id, [ mem_in; mem_out ]),
( instances,
- ( memories,
- Forall
- ( t.tinputs @ t.tlocals @ t.toutputs,
- Imply (tr (), tr ~mems ~insts ()) ) ) ) ) )
+ (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
+ )
let pp_transition_footprint_lemmas fmt m =
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
@@ -824,7 +813,7 @@ module SrcMod = struct
(pp_requires pp_separated')
outputs (pp_assigns pp_ptr_decl) outputs
(pp_ensures (pp_transition_aux'' m))
- (name, inputs, [], outputs, "", "")
+ (name, inputs @ outputs, "", "")
else
fprintf fmt
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
@@ -839,9 +828,9 @@ module SrcMod = struct
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
(name, mem, self)
(pp_ensures
- (pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl
- pp_ptr_decl))
- (name, inputs, [], outputs, mem, mem)
+ (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
+ (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
+ (name, inputs @ outputs, mem, mem)
(pp_assigns pp_ptr_decl) outputs
(pp_assigns (pp_reg self))
m.mmemory
diff --git a/src/machine_code.ml b/src/machine_code.ml
index cf324c94324ed58f21966f27b0a5411cd07b0400..d550720eb5a1711f1636072981bdd8f04d9d9307 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -186,11 +186,7 @@ type machine_ctx = {
(* Transition spec *)
t :
(var_decl list
- (* inputs *)
- * var_decl list
- (* locals *)
- * var_decl list
- (* outputs *)
+ (* vars *)
* ISet.t (* memory footprint *)
* ident IMap.t
(* memory instances footprint *)
@@ -247,18 +243,15 @@ let translate_eq env ctx nd inputs locals outputs i eq =
let outputs_i = Lustre_live.inter_live_i_with id i outputs in
let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in
let pred_t ctx a =
- ( inputs,
- locals_i,
- outputs_i,
+ ( inputs @ locals_i @ outputs_i,
ctx.m,
IMap.map (fun (td, _) -> node_name td) ctx.j,
Exists
( Lustre_live.existential_vars id i eq (locals @ outputs),
And
[
- mk_transition ~i:(i - 1) id (vdecls_to_vals inputs)
- (vdecls_to_vals locals_pi)
- (vdecls_to_vals outputs_pi);
+ mk_transition ~i:(i - 1) id
+ (vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
a;
] ) )
:: ctx.t
@@ -274,8 +267,8 @@ let translate_eq env ctx nd inputs locals outputs i eq =
(if fst (get_stateless_status_node nd) then []
else [ mk_memory_pack ~i id ])
@ [
- mk_transition ~i id (vdecls_to_vals inputs)
- (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
+ mk_transition ~i id
+ (vdecls_to_vals (inputs @ locals_i @ outputs_i));
];
}
:: ctx.s;
@@ -304,7 +297,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
ctl
(MStep ([ var_x ], inst, [ c1; c2 ]))
(mk_memory_pack ~inst (node_name td))
- (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
+ (mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
{ ctx with j = IMap.add inst (td, []) ctx.j }
in
{ ctx with si = mkinstr (MSetReset inst) :: ctx.si }
@@ -332,7 +325,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
}
| p, Expr_appl (f, arg, r)
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
- let var_p = List.map (fun v -> env.get_var v) p in
+ let var_p = List.map env.get_var p in
let el = expr_list_of_expr arg in
let vl = List.map translate_expr el in
let node_f = node_from_name f in
@@ -351,7 +344,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
ctl ~ck:call_ck
(MStep (var_p, inst, vl))
(mk_memory_pack ~inst (node_name node_f))
- (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
+ (mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
{
ctx with
j = IMap.add inst call_f ctx.j;
@@ -472,9 +465,7 @@ let transition_0 nd =
{
tname = nd;
tindex = Some 0;
- tinputs = nd.node_inputs;
- tlocals = [];
- toutputs = [];
+ tvars = nd.node_inputs;
tformula = True;
tmem_footprint = ISet.empty;
tinst_footprint = IMap.empty;
@@ -483,16 +474,12 @@ let transition_0 nd =
let transition_toplevel nd i =
let tr =
mk_transition nd.node_id ~i
- (vdecls_to_vals nd.node_inputs)
- []
- (vdecls_to_vals nd.node_outputs)
+ (vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
in
{
tname = nd;
tindex = None;
- tinputs = nd.node_inputs;
- tlocals = [];
- toutputs = nd.node_outputs;
+ tvars = nd.node_inputs @ nd.node_outputs;
tformula =
(if fst (get_stateless_status_node nd) then tr
else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
@@ -564,13 +551,11 @@ let translate_decl nd sch =
transition_0 nd
::
List.mapi
- (fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) ->
+ (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
{
tname = nd;
tindex = Some (i + 1);
- tinputs;
- tlocals;
- toutputs;
+ tvars;
tformula = red f;
tmem_footprint;
tinst_footprint;
@@ -583,9 +568,7 @@ let translate_decl nd sch =
~instr_spec:
((if fst (get_stateless_status_node nd) then []
else [ mk_memory_pack ~i:0 nd.node_id ])
- @ [
- mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
- ])
+ @ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
MClearReset
in
{
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index af44a8ec969ca118fe20bc97a9a8a3b95678c72c..d8361c0228183a1298f247e475ce76b31fa81379 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -58,7 +58,7 @@ module PrintSpec = struct
fun fmt e -> pp_expr m fmt e
in
match p with
- | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
+ | Transition (f, inst, i, vars, _r, _mems, _insts) ->
fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
(pp_print_option
~none:(fun fmt () -> pp_print_string fmt "SELF")
@@ -67,7 +67,7 @@ module PrintSpec = struct
(pp_print_option pp_print_int)
i
(pp_print_parenthesized pp_expr)
- (inputs @ locals @ outputs)
+ vars
| Reset (f, inst, r) ->
fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst
(pp_val m) r
@@ -239,8 +239,7 @@ let pp_transition m fmt t =
(pp_print_option pp_print_int)
t.tindex
(pp_print_parenthesized pp_vdecl)
- (t.tinputs @ t.tlocals @ t.toutputs)
- (PrintSpec.pp_spec m) t.tformula
+ t.tvars (PrintSpec.pp_spec m) t.tformula
let pp_transitions m fmt =
if !Options.spec <> "no" then
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 5de389e9035e9e36d09f3214d838ef5df17dff38..2f9d14acf6d03bf4f57da5655669354b45bb2682 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -11,6 +11,7 @@
open Utils
open Lustre_types
+open Spec_types
open Machine_code_types
open Corelang
open Causality
@@ -597,36 +598,75 @@ let rec value_replace_var fvar value =
| Power (v, n) ->
{ value with value_desc = Power (value_replace_var fvar v, n) }
-let rec instr_replace_var fvar instr cont =
- match get_instr_desc instr with
- | MLocalAssign (i, v) ->
- instr_cons
- (update_instr_desc instr
- (MLocalAssign (fvar i, value_replace_var fvar v)))
- cont
- | MStateAssign (i, v) ->
- instr_cons
- (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
- cont
- | MSetReset _
- | MNoReset _
- | MClearReset
- | MResetAssign _
- | MSpec _
- | MComment _ ->
- instr_cons instr cont
- | MStep (il, i, vl) ->
- instr_cons
- (update_instr_desc instr
- (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
- cont
- | MBranch (g, hl) ->
- instr_cons
- (update_instr_desc instr
- (MBranch
- ( value_replace_var fvar g,
- List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
- cont
+let expr_spec_replace :
+ type a.
+ (var_decl -> var_decl) ->
+ (value_t, a) expression_t ->
+ (value_t, a) expression_t =
+ fun fvar -> function
+ | Val v ->
+ Val (value_replace_var fvar v)
+ | Var v ->
+ Var (fvar v)
+ | e ->
+ e
+
+let predicate_spec_replace fvar = function
+ | Transition (f, inst, i, vars, r, mems, insts) ->
+ Transition
+ (f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
+ | p ->
+ p
+
+let rec instr_spec_replace fvar =
+ let aux instr = instr_spec_replace fvar instr in
+ function
+ | Equal (e1, e2) ->
+ Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
+ | And f ->
+ And (List.map aux f)
+ | Or f ->
+ Or (List.map aux f)
+ | Imply (a, b) ->
+ Imply (aux a, aux b)
+ | Exists (xs, a) ->
+ let fvar v = if List.mem v xs then v else fvar v in
+ Exists (xs, instr_spec_replace fvar a)
+ | Forall (xs, a) ->
+ let fvar v = if List.mem v xs then v else fvar v in
+ Forall (xs, instr_spec_replace fvar a)
+ | Ternary (e, a, b) ->
+ Ternary (expr_spec_replace fvar e, aux a, aux b)
+ | Predicate p ->
+ Predicate (predicate_spec_replace fvar p)
+ | ExistsMem (f, a, b) ->
+ ExistsMem (f, aux a, aux b)
+ | f ->
+ f
+
+let rec instr_replace_var fvar instr =
+ let instr_desc =
+ match instr.instr_desc with
+ | MLocalAssign (i, v) ->
+ MLocalAssign (fvar i, value_replace_var fvar v)
+ | MStateAssign (i, v) ->
+ MStateAssign (i, value_replace_var fvar v)
+ | MStep (il, i, vl) ->
+ MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
+ | MBranch (g, hl) ->
+ MBranch
+ ( value_replace_var fvar g,
+ List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
+ | MSetReset _
+ | MNoReset _
+ | MClearReset
+ | MResetAssign _
+ | MSpec _
+ | MComment _ ->
+ instr.instr_desc
+ in
+ let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
+ instr_cons { instr with instr_desc; instr_spec }
and instrs_replace_var fvar instrs cont =
List.fold_right (instr_replace_var fvar) instrs cont
@@ -657,15 +697,13 @@ let step_replace_var fvar step =
let machine_replace_variables fvar m =
{ m with mstep = step_replace_var fvar m.mstep }
-let machine_reuse_variables m reuse =
+let machine_reuse_variables reuse m =
let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
machine_replace_variables fvar m
-let machines_reuse_variables prog reuse_tables =
- List.map
- (fun m ->
- machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
- prog
+let machines_reuse_variables reuse_tables =
+ List.map (fun m ->
+ machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
let rec instr_assign res instr =
match get_instr_desc instr with
@@ -723,19 +761,18 @@ and instrs_reduce branches instrs cont =
i1 :: instrs_reduce branches (i2 :: q) cont
let rec instrs_fusion instrs =
- match instrs, List.map get_instr_desc instrs with
- | [], [] | [ _ ], [ _ ] ->
+ match instrs with
+ | [] | [ _ ] ->
instrs
- | i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
- when instr_constant_assign v i1 ->
- instr_reduce
- (List.map (fun (h, b) -> h, instrs_fusion b) hl)
- i1 (instrs_fusion q)
- | i1 :: i2 :: q, _ ->
- i1 :: instrs_fusion (i2 :: q)
- | _ ->
- assert false
-(* Other cases should not happen since both lists are of same size *)
+ | i1 :: i2 :: q -> (
+ match i2.instr_desc with
+ | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
+ instr_reduce
+ (List.map (fun (h, b) -> h, instrs_fusion b) hl)
+ { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
+ (instrs_fusion q)
+ | _ ->
+ i1 :: instrs_fusion (i2 :: q))
let step_fusion step =
{ step with step_instrs = instrs_fusion step.step_instrs }
@@ -897,7 +934,7 @@ let optimize params prog node_schs machine_code =
Scheduling.remove_prog_inlined_locals removed_table node_schs
in
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
- machines_fusion (machines_reuse_variables machine_code reuse_tables))
+ machines_fusion (machines_reuse_variables reuse_tables machine_code))
else machine_code
in
diff --git a/src/spec_common.ml b/src/spec_common.ml
index 6f3c9373bb641f05fedaea2dcbfd9298bbc3e6da..eeee85194ed451777c94b5cb33ef63cfa3a80cf1 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -79,17 +79,15 @@ let vals vs = List.map (fun v -> Val v) vs
let mk_pred_call pred = Predicate pred
-let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id
- inputs locals outputs =
+let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id vars
+ =
let tr =
mk_pred_call
(Transition
( id,
inst,
i,
- vals inputs,
- vals locals,
- vals outputs,
+ vals vars,
(match r with Some _ -> true | None -> false),
mems,
insts ))
diff --git a/src/spec_types.ml b/src/spec_types.ml
index c1201c3a138b98171a008ae892c320d86ebddac8..fc3dfeed01acb0544f1647a2a75caa4a72d10415 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -22,8 +22,6 @@ let type_of_l_value : type a. (a, left_v) expression_t -> Types.type_expr =
| Memory (StateVar v) ->
v.var_type
-type ('a, 'b) expressions_t = ('a, 'b) expression_t list
-
type 'a predicate_t =
| Transition :
ident (* node name *)
@@ -31,12 +29,8 @@ type 'a predicate_t =
(* instance *)
* int option
(* transition index *)
- * ('a, 'b) expressions_t
- (* inputs *)
- * ('a, 'b) expressions_t
- (* locals *)
- * ('a, 'b) expressions_t
- (* outputs *)
+ * ('a, 'b) expression_t list
+ (* variables *)
* bool (* reset *)
* Utils.ISet.t (* memory footprint *)
* ident Utils.IMap.t
@@ -78,9 +72,7 @@ type 'a memory_pack_t = {
type 'a transition_t = {
tname : node_desc;
tindex : int option;
- tinputs : var_decl list;
- tlocals : var_decl list;
- toutputs : var_decl list;
+ tvars : var_decl list;
tformula : 'a formula_t;
tmem_footprint : Utils.ISet.t;
tinst_footprint : ident Utils.IMap.t;