diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index ae3c5cb9f8eed9b39578300a745f54da06a5da72..11e823e1588c66184edcbb5f492b1ba5af8c9b9c 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -233,25 +233,29 @@ let rec pp_c_const fmt c =
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
| Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
-
+
(* Prints a value expression [v], with internal function calls only.
[pp_var] is a printer for variables (typically [pp_c_var_read]),
but an offset suffix may be added for array variables
*)
-let rec pp_c_val self pp_var fmt v =
+let rec pp_c_val m self pp_var fmt v =
+ let pp_c_val = pp_c_val m self pp_var in
match v.value_desc with
| Cst c -> pp_c_const fmt c
- | Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
- | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
- | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
- | LocalVar v -> pp_var fmt v
- | StateVar v ->
- (* array memory vars are represented by an indirection to a local var with the right type,
- in order to avoid casting everywhere. *)
- if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
- then fprintf fmt "%a" pp_var v
- else fprintf fmt "%s->_reg.%a" self pp_var v
- | Fun (n, vl) -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (pp_c_val self pp_var) fmt vl
+ | Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " pp_c_val) vl
+ | Access (t, i) -> fprintf fmt "%a[%a]" pp_c_val t pp_c_val i
+ | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." (pp_val m) v; assert false)
+ | Var v ->
+ if is_memory m v then (
+ (* array memory vars are represented by an indirection to a local var with the right type,
+ in order to avoid casting everywhere. *)
+ if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
+ then fprintf fmt "%a" pp_var v
+ else fprintf fmt "%s->_reg.%a" self pp_var v
+ )
+ else
+ pp_var fmt v
+ | Fun (n, vl) -> pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
(* Access to the value of a variable:
- if it's not a scalar output, then its name is enough
@@ -318,7 +322,7 @@ let pp_c_decl_local_var m fmt id =
then
Format.fprintf fmt "%a = %a"
(pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
- (pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
+ (pp_c_val m "" (pp_c_var_read m)) (get_const_assign m id)
else
Format.fprintf fmt "%a"
(pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
@@ -347,7 +351,7 @@ let pp_c_checks self fmt m =
fprintf fmt
"@[<v>%a@,assert (%a);@]@,"
Location.pp_c_loc loc
- (pp_c_val self (pp_c_var_read m)) check
+ (pp_c_val m self (pp_c_var_read m)) check
)
fmt
m.mstep.step_checks
@@ -512,24 +516,20 @@ let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list
then
fprintf fmt "%a (%a%t%a);"
pp_machine_step_name mname
- (Utils.fprintf_list ~sep:", " (pp_c_val self pp_c_main_var_input)) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
else
fprintf fmt "%a (%a%t%a%t%s);"
pp_machine_step_name mname
- (Utils.fprintf_list ~sep:", " (pp_c_val self pp_c_main_var_input)) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
(Utils.pp_final_char_if_non_empty ", " outputs)
self
let pp_c_var m self pp_var fmt var =
- if is_memory m var
- then
- pp_c_val self pp_var fmt (mk_val (StateVar var) var.var_type)
- else
- pp_c_val self pp_var fmt (mk_val (LocalVar var) var.var_type)
+ pp_c_val m self pp_var fmt (mk_val (Var var) var.var_type)
let pp_array_suffix fmt loop_vars =
@@ -560,8 +560,8 @@ let pp_initialize m self pp_var fmt var =
aux [] fmt var.var_type
end
-let pp_const_initialize pp_var fmt const =
- let var = mk_val (LocalVar (Corelang.var_decl_of_const const)) const.const_type in
+let pp_const_initialize m pp_var fmt const =
+ let var = mk_val (Var (Corelang.var_decl_of_const const)) const.const_type in
let rec aux indices value fmt typ =
if Types.is_array_type typ
then
@@ -576,7 +576,7 @@ let pp_const_initialize pp_var fmt const =
else
let indices = List.rev indices in
let pp_var_suffix fmt var =
- fprintf fmt "%a%a" (pp_c_val "" pp_var) var pp_array_suffix indices in
+ fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
begin
Mpfr.pp_inject_init pp_var_suffix fmt var;
fprintf fmt "@,";
@@ -644,7 +644,7 @@ let pp_call m self pp_read pp_write fmt i (inputs: Machine_code_types.value_t li
let (n,_) = List.assoc i m.minstances in
fprintf fmt "%a (%a%t%a%t%s->%s);"
pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self pp_read)) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " pp_write) outputs
(Utils.pp_final_char_if_non_empty ", " outputs)
@@ -654,7 +654,7 @@ let pp_call m self pp_read pp_write fmt i (inputs: Machine_code_types.value_t li
let (n,_) = List.assoc i m.mcalls in
fprintf fmt "%a (%a%t%a);"
pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self pp_read)) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " pp_write) outputs
@@ -665,7 +665,7 @@ let pp_basic_instance_call m self fmt i (inputs: Machine_code_types.value_t list
let (n,_) = List.assoc i m.minstances in
fprintf fmt "%a (%a%t%a%t%s->%s);"
pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
(Utils.pp_final_char_if_non_empty ", " outputs)
@@ -675,7 +675,7 @@ let pp_basic_instance_call m self fmt i (inputs: Machine_code_types.value_t list
let (n,_) = List.assoc i m.mcalls in
fprintf fmt "%a (%a%t%a);"
pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs
(Utils.pp_final_char_if_non_empty ", " inputs)
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
*)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 1b796e0f1c8563996bb5160e61cccbf45dfc43be..7a23dc8226c8ad5c3aee2da94ed35f828a60b7bf 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -54,7 +54,7 @@ let print_import_standard fmt =
let rec print_static_val pp_var fmt v =
match v.value_desc with
| Cst c -> pp_c_const fmt c
- | LocalVar v -> pp_var fmt v
+ | Var v -> pp_var fmt v
| Fun (n, vl) -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (print_static_val pp_var) fmt vl
| _ -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index e1f85364f6cb9a6e2e11793c7fb89934c7da86e0..90f3862e692349810c6438ffa064c0a05c9421bc 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -115,7 +115,7 @@ let print_main_clear mname main_mem fmt m =
let print_main_loop mname main_mem fmt m =
let input_values =
- List.map (fun v -> mk_val (LocalVar v) v.var_type)
+ List.map (fun v -> mk_val (Var v) v.var_type)
m.mstep.step_inputs in
begin
fprintf fmt "@ ISATTY = isatty(0);@ ";
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 29506130dc18bc05ac90f25fe1be61cecf0798ce..d7d1eaaab5ce3ae066bb124935d4622dc6160693 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -38,8 +38,7 @@ struct
let rec expansion_depth v =
match v.value_desc with
| Cst cst -> expansion_depth_cst cst
- | LocalVar _
- | StateVar _ -> 0
+ | Var _ -> 0
| Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
| Access (v, i) -> max 0 (expansion_depth v - 1)
@@ -59,8 +58,7 @@ struct
let rec static_loop_profile v =
match v.value_desc with
| Cst cst -> static_loop_profile_cst cst
- | LocalVar _
- | StateVar _ -> []
+ | Var _ -> []
| Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
| Array vl -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
| Access (v, i) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
@@ -90,7 +88,7 @@ let rec value_offsets v offsets =
| Cst (Const_array cl) , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
| Fun (f, vl) , _ -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
| _ , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
- | _ , LVar i :: q -> value_offsets (Access (v, LocalVar i)) q
+ | _ , LVar i :: q -> value_offsets (Access (v, Var i)) q
*)
(* Computes the list of nested loop variables together with their dimension bounds.
- LInt r stands for loop expansion (no loop variable, but int loop index)
@@ -114,15 +112,15 @@ let reorder_loop_variables loop_vars =
var_loops @ int_loops
(* Prints a one loop variable suffix for arrays *)
-let pp_loop_var fmt lv =
+let pp_loop_var m fmt lv =
match snd lv with
| LVar v -> fprintf fmt "[%s]" v
| LInt r -> fprintf fmt "[%d]" !r
- | LAcc i -> fprintf fmt "[%a]" pp_val i
+ | LAcc i -> fprintf fmt "[%a]" (pp_val m) i
(* Prints a suffix of loop variables for arrays *)
-let pp_suffix fmt loop_vars =
- Utils.fprintf_list ~sep:"" pp_loop_var fmt loop_vars
+let pp_suffix m fmt loop_vars =
+ Utils.fprintf_list ~sep:"" (pp_loop_var m) fmt loop_vars
(* Prints a value expression [v], with internal function calls only.
[pp_var] is a printer for variables (typically [pp_c_var_read]),
@@ -142,49 +140,54 @@ let rec pp_c_const_suffix var_type fmt c =
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
-let rec pp_value_suffix self var_type loop_vars pp_value fmt value =
+let rec pp_value_suffix m self var_type loop_vars pp_value fmt value =
(*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
+ let pp_suffix = pp_suffix m in
(
match loop_vars, value.value_desc with
| (x, LAcc i) :: q, _ when is_const_index i ->
let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
- pp_value_suffix self var_type ((x, LInt r)::q) pp_value fmt value
+ pp_value_suffix m self var_type ((x, LInt r)::q) pp_value fmt value
| (_, LInt r) :: q, Cst (Const_array cl) ->
let var_type = Types.array_element_type var_type in
- pp_value_suffix self var_type q pp_value fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
+ pp_value_suffix m self var_type q pp_value fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
| (_, LInt r) :: q, Array vl ->
let var_type = Types.array_element_type var_type in
- pp_value_suffix self var_type q pp_value fmt (List.nth vl !r)
+ pp_value_suffix m self var_type q pp_value fmt (List.nth vl !r)
| loop_var :: q, Array vl ->
let var_type = Types.array_element_type var_type in
- Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type q pp_value)) vl pp_suffix [loop_var]
+ Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type q pp_value)) vl pp_suffix [loop_var]
| [] , Array vl ->
let var_type = Types.array_element_type var_type in
- Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type [] pp_value)) vl
+ Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type [] pp_value)) vl
| _ :: q, Power (v, n) ->
- pp_value_suffix self var_type q pp_value fmt v
+ pp_value_suffix m self var_type q pp_value fmt v
| _ , Fun (n, vl) ->
- pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
+ pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix m self var_type loop_vars pp_value) fmt vl
| _ , Access (v, i) ->
let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
- pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
- | _ , LocalVar v -> Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
- | _ , StateVar v ->
- (* array memory vars are represented by an indirection to a local var with the right type,
- in order to avoid casting everywhere. *)
- if Types.is_array_type v.var_type
- then Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
- else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v pp_suffix loop_vars
+ pp_value_suffix m self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
+ | _ , Var v ->
+ if is_memory m v then (
+ (* array memory vars are represented by an indirection to a local var with the right type,
+ in order to avoid casting everywhere. *)
+ if Types.is_array_type v.var_type
+ then Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
+ else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v pp_suffix loop_vars
+ )
+ else (
+ Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
+ )
| _ , Cst cst -> pp_c_const_suffix var_type fmt cst
- | _ , _ -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type pp_val value pp_suffix loop_vars; assert false)
+ | _ , _ -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type (pp_val m) value pp_suffix loop_vars; assert false)
)
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
which may yield constant arrays in expressions.
Type is needed to correctly print constant arrays.
*)
-let pp_c_val self pp_var fmt v =
- pp_value_suffix self v.value_type [] pp_var fmt v
+let pp_c_val m self pp_var fmt v =
+ pp_value_suffix m self v.value_type [] pp_var fmt v
let pp_basic_assign pp_var fmt typ var_name value =
if Types.is_real_type typ && !Options.mpfr
@@ -209,7 +212,7 @@ let pp_assign m self pp_var fmt var_type var_name value =
let rec aux typ fmt vars =
match vars with
| [] ->
- pp_basic_assign (pp_value_suffix self var_type loop_vars pp_var) fmt typ var_name value
+ pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var) fmt typ var_name value
| (d, LVar i) :: q ->
let typ' = Types.array_element_type typ in
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
@@ -308,7 +311,7 @@ let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs:
let inputs = List.combine input_types inputs in
if has_c_prototype i dependencies
then (* external C function *)
- let outputs = List.map2 (fun t v -> t, LocalVar v) output_types outputs in
+ let outputs = List.map2 (fun t v -> t, Var v) output_types outputs in
fprintf fmt "%a = %s(%a);"
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) outputs
i
@@ -322,7 +325,7 @@ let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs:
*)
let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
- (pp_c_val self (pp_c_var_read m)) c
+ (pp_c_val m self (pp_c_var_read m)) c
(Utils.pp_newline_if_non_empty tl)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) tl
(Utils.pp_newline_if_non_empty el)
@@ -336,24 +339,24 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
| MLocalAssign (i,v) ->
pp_assign
m self (pp_c_var_read m) fmt
- i.var_type (mk_val (LocalVar i) i.var_type) v
+ i.var_type (mk_val (Var i) i.var_type) v
| MStateAssign (i,v) ->
pp_assign
m self (pp_c_var_read m) fmt
- i.var_type (mk_val (StateVar i) i.var_type) v
+ i.var_type (mk_val (Var i) i.var_type) v
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
pp_machine_instr dependencies m self fmt
(update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
| MStep ([i0], i, vl) when has_c_prototype i dependencies ->
fprintf fmt "%a = %s(%a);"
- (pp_c_val self (pp_c_var_read m)) (mk_val (LocalVar i0) i0.var_type)
+ (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
i
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) vl
+ (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) vl
| MStep (il, i, vl) when Mpfr.is_homomorphic_fun i ->
pp_instance_call m self fmt i vl il
| MStep (il, i, vl) ->
pp_basic_instance_call m self fmt i vl il
- | MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." pp_instr instr; assert false)
+ | MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false)
| MBranch (g, hl) ->
if let t = fst (List.hd hl) in t = tag_true || t = tag_false
then (* boolean case, needs special treatment in C because truth value is not unique *)
@@ -364,7 +367,7 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
else (* enum type case *)
(*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
- (pp_c_val self (pp_c_var_read m)) g
+ (pp_c_val m self (pp_c_var_read m)) g
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
| MComment s ->
fprintf fmt "/*%s*/@ " s
@@ -612,7 +615,7 @@ let print_global_init_code fmt basename prog dependencies =
print_global_init_prototype baseNAME
(pp_c_basic_type_desc Type_predef.type_bool)
(* constants *)
- (Utils.fprintf_list ~sep:"@," (pp_const_initialize (pp_c_var_read empty_machine))) constants
+ (Utils.fprintf_list ~sep:"@," (pp_const_initialize empty_machine (pp_c_var_read empty_machine))) constants
(Utils.pp_final_char_if_non_empty "@," dependencies)
(* dependencies initialization *)
(Utils.fprintf_list ~sep:"@," print_import_init) dependencies
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 4d736e2799683776bfab41657f37813270207d2a..9f2c2f4a250a020fd3afd6c8bd69b8699c679d17 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -260,15 +260,14 @@ let rec pp_emf_instr m fmt i =
fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
fun_id
- pp_emf_cst_or_var_list vl
+ (pp_emf_cst_or_var_list m) vl
)
| Array _ | Access _ | Power _ -> assert false (* No array expression allowed yet *)
| Cst _
- | LocalVar _
- | StateVar _ -> (
+ | Var _ -> (
fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
pp_var_name lhs
- pp_emf_cst_or_var expr
+ (pp_emf_cst_or_var m) expr
)) )
| MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
@@ -276,7 +275,7 @@ let rec pp_emf_instr m fmt i =
-> (
fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
pp_var_name lhs
- pp_emf_cst_or_var expr
+ (pp_emf_cst_or_var m) expr
)
| MReset id
@@ -307,7 +306,7 @@ let rec pp_emf_instr m fmt i =
(* ; *)
fprintf fmt "\"kind\": \"branch\",@ ";
- fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *)
+ fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g; (* it has to be a variable or a constant *)
fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
(* (let guard_inputs = get_expr_vars g in
@@ -348,7 +347,7 @@ let rec pp_emf_instr m fmt i =
f;
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
- pp_emf_cst_or_var_list inputs;
+ (pp_emf_cst_or_var_list m) inputs;
if is_stateful then
fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
(reset_name f)
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index 381df16d22aef1037104ada3f8a0b5e4b6889546..bb9f47e2e0bc019724cc018f3dce8f49ff8bc857 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -14,7 +14,7 @@ let rec get_idx x l =
let rec get_expr_vars v =
match v.value_desc with
| Cst c -> VSet.empty
- | LocalVar v | StateVar v -> VSet.singleton v
+ | Var v -> VSet.singleton v
| Fun (_, args) -> List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args
| _ -> assert false (* Invalid argument *)
@@ -210,22 +210,21 @@ let pp_emf_cst fmt c =
)
-let pp_emf_cst_or_var fmt v =
+let pp_emf_cst_or_var m fmt v =
match v.value_desc with
| Cst c -> pp_emf_cst fmt c
- | LocalVar v
- | StateVar v -> (
+ | Var v -> (
fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
pp_var_name v;
(* fprintf fmt "\"original_name\": \"%a\",@ " Printers.pp_var_name v; *)
fprintf fmt "\"datatype\": \"%a\"@ " pp_var_type v;
fprintf fmt "@]}"
)
- | _ -> eprintf "Not of cst or var: %a@." pp_val v ; assert false (* Invalid argument *)
+ | _ -> eprintf "Not of cst or var: %a@." (pp_val m) v ; assert false (* Invalid argument *)
-let pp_emf_cst_or_var_list =
- Utils.fprintf_list ~sep:",@ " pp_emf_cst_or_var
+let pp_emf_cst_or_var_list m =
+ Utils.fprintf_list ~sep:",@ " (pp_emf_cst_or_var m)
(* Printer lustre expr and eexpr *)
diff --git a/src/backends/EMF/EMF_library_calls.ml b/src/backends/EMF/EMF_library_calls.ml
index 353dbf59aab947a8cd3231e236657cf0ec0b1e5a..d34eb96524ff035c8bd94b2d03f4e83566c30559 100644
--- a/src/backends/EMF/EMF_library_calls.ml
+++ b/src/backends/EMF/EMF_library_calls.ml
@@ -18,7 +18,7 @@ let pp_call fmt m f outputs inputs =
name lib;
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
(Utils.fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" Printers.pp_var_name v)) outputs
- pp_emf_cst_or_var_list inputs
+ (pp_emf_cst_or_var_list m) inputs
)
| _ ->
Format.eprintf "Calls to function %s in library %s are not handled yet.@."
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index cbd28ba5f01985d1e79513ced6d092af52fe1996..62e291da0051713ee5c05fc1dff539510d8089c1 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -116,7 +116,7 @@ let pp_basic_lib_fun i pp_val fmt vl =
[pp_var] is a printer for variables (typically [pp_c_var_read]),
but an offset suffix may be added for array variables
*)
-let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
+let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
match v.value_desc with
| Cst c -> pp_horn_const fmt c
@@ -142,32 +142,35 @@ let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
fprintf fmt "(store %a %i %a)"
print (t, (x+1))
x
- (pp_horn_val ~is_lhs:is_lhs self pp_var) h
+ (pp_horn_val ~is_lhs:is_lhs m self pp_var) h
in
print fmt (il, 0)
| Access(tab,index) ->
fprintf fmt "(select %a %a)"
- (pp_horn_val ~is_lhs:is_lhs self pp_var) tab
- (pp_horn_val ~is_lhs:is_lhs self pp_var) index
+ (pp_horn_val ~is_lhs:is_lhs m self pp_var) tab
+ (pp_horn_val ~is_lhs:is_lhs m self pp_var) index
(* Code specific for arrays *)
| Power (v, n) -> assert false
- | LocalVar v -> pp_var fmt (rename_machine self v)
- | StateVar v ->
- if Types.is_array_type v.var_type
- then assert false
- else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
- | Fun (n, vl) -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val self pp_var)) vl
+ | Var v ->
+ if is_memory m v then
+ if Types.is_array_type v.var_type
+ then assert false
+ else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
+ else
+ pp_var fmt (rename_machine self v)
+
+ | Fun (n, vl) -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
(* Prints a [value] indexed by the suffix list [loop_vars] *)
-let rec pp_value_suffix self pp_value fmt value =
+let rec pp_value_suffix m self pp_value fmt value =
match value.value_desc with
| Fun (n, vl) ->
- pp_basic_lib_fun n (pp_value_suffix self pp_value) fmt vl
+ pp_basic_lib_fun n (pp_value_suffix m self pp_value) fmt vl
| _ ->
- pp_horn_val self pp_value fmt value
+ pp_horn_val m self pp_value fmt value
(* type_directed assignment: array vs. statically sized type
- [var_type]: type of variable to be assigned
@@ -178,8 +181,8 @@ let rec pp_value_suffix self pp_value fmt value =
let pp_assign m pp_var fmt var_name value =
let self = m.mname.node_id in
fprintf fmt "(= %a %a)"
- (pp_horn_val ~is_lhs:true self pp_var) var_name
- (pp_value_suffix self pp_var) value
+ (pp_horn_val ~is_lhs:true m self pp_var) var_name
+ (pp_value_suffix m self pp_var) value
(* In case of no reset call, we define mid_mem = current_mem *)
@@ -254,10 +257,10 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
fprintf fmt "@[<v 5>(and ";
fprintf fmt "(= %a (ite %a %a %a))"
- (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
+ (pp_horn_val ~is_lhs:true m self (pp_horn_var m)) (mk_val (Var o) o.var_type) (* output var *)
(pp_horn_var m) mem_m
- (pp_horn_val self (pp_horn_var m)) i1
- (pp_horn_val self (pp_horn_var m)) i2
+ (pp_horn_val m self (pp_horn_var m)) i1
+ (pp_horn_val m self (pp_horn_var m)) i2
;
fprintf fmt "@ ";
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
@@ -267,10 +270,10 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
| node_name_n -> begin
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
+ (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
(Utils.pp_final_char_if_non_empty "@ " outputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
@@ -280,11 +283,11 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
let (n,_) = List.assoc i m.mcalls in
fprintf fmt "(%a @[<v 0>%a%t%a)@]"
pp_machine_stateless_name (node_name n)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
+ (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
)
@@ -301,12 +304,12 @@ let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ide
| MLocalAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- (mk_val (LocalVar i) i.var_type) v;
+ (mk_val (Var i) i.var_type) v;
reset_instances
| MStateAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- (mk_val (StateVar i) i.var_type) v;
+ (mk_val (Var i) i.var_type) v;
reset_instances
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
assert false (* This should not happen anymore *)
@@ -335,7 +338,7 @@ let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ide
may cause trouble. I have hard time
producing a MWE, so I'll just keep the
fix here as (not a) or b *)
- (pp_horn_val self (pp_horn_var m)) g
+ (pp_horn_val m self (pp_horn_var m)) g
pp_horn_tag tag;
let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in
fprintf fmt "@])";
@@ -446,7 +449,7 @@ let print_machine machines fmt m =
end
| assertsl ->
begin
- let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
+ let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
fprintf fmt "; Stateless step rule with Assertions @.";
(*Rule for step*)
@@ -493,7 +496,7 @@ let print_machine machines fmt m =
end
| assertsl ->
begin
- let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
+ let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
(* print_string pp_val; *)
fprintf fmt "; Step rule with Assertions @.";
@@ -599,7 +602,7 @@ let get_sf_info() =
end
| assertsl ->
begin
- let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
+ let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
(* print_string pp_val; *)
fprintf fmt "; with Assertions @.";
diff --git a/src/backends/Java/java_backend.ml b/src/backends/Java/java_backend.ml
index 5708cb42ad4b47e8f30d490452d394918d7cde58..8783933b74e16260cf41aca99994f1768bb8eb31 100644
--- a/src/backends/Java/java_backend.ml
+++ b/src/backends/Java/java_backend.ml
@@ -51,12 +51,14 @@ let rec pp_const fmt c =
let rec pp_val m fmt v =
match v with
| Cst c -> pp_const fmt c
- | LocalVar v ->
- if List.exists (fun o -> o.var_id = v) m.mstep.step_outputs then
- fprintf fmt "*%s" v
- else
- pp_print_string fmt v
- | StateVar v -> fprintf fmt "%s" v
+ | Var v ->
+ if is_state_vars m.memories v then
+ fprintf fmt "%s" v
+ else
+ if List.exists (fun o -> o.var_id = v) m.mstep.step_outputs then
+ fprintf fmt "*%s" v
+ else
+ pp_print_string fmt v
| Fun (n, vl) -> if Basic_library.is_internal_fun n then
Basic_library.pp_java n (pp_val m) fmt vl
else
diff --git a/src/corelang.ml b/src/corelang.ml
index 300713c3485d0a0b34481d08bce6f40fe141d972..081647ec03ab05bce264b409b024d3a13d43ca99 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -25,8 +25,15 @@ end
module VMap = Map.Make(VDeclModule)
-module VSet : Set.S with type elt = var_decl = Set.Make(VDeclModule)
-
+module VSet: sig
+ include Set.S
+ val pp: Format.formatter -> t -> unit
+end with type elt = var_decl =
+ struct
+ include Set.Make(VDeclModule)
+ let pp fmt s =
+ Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s)
+ end
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
diff --git a/src/corelang.mli b/src/corelang.mli
index 05a62bdc748d2ffa6bdb13696d29bd23197c7465..9b9343bf38a9e02e7ae0627cea3268de223c077a 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -13,7 +13,10 @@
open Lustre_types
exception Error of Location.t * Error.error_kind
-module VSet: Set.S with type elt = Lustre_types.var_decl
+module VSet: sig
+ include Set.S
+ val pp: Format.formatter -> t -> unit
+end with type elt = Lustre_types.var_decl
val dummy_type_dec: type_dec
val dummy_clock_dec: clock_dec
diff --git a/src/machine_code.ml b/src/machine_code.ml
index b2205dbcba54dbc41f7eb11f60f15c04d95f780b..e670ddacac33b11dbde5229f87c38c9a5edc3fa7 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -19,6 +19,7 @@ open Causality
exception NormalizationError
+
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
(* the context contains m : state aka memory variables *)
(* si : initialization instructions *)
@@ -29,19 +30,11 @@ let translate_ident node (m, si, j, d, s) id =
(* Format.eprintf "trnaslating ident: %s@." id; *)
try (* id is a node var *)
let var_id = get_node_var id node in
- if VSet.exists (fun v -> v.var_id = id) m
- then (
- (* Format.eprintf "a STATE VAR@."; *)
- mk_val (StateVar var_id) var_id.var_type
- )
- else (
- (* Format.eprintf "a LOCAL VAR@."; *)
- mk_val (LocalVar var_id) var_id.var_type
- )
+ mk_val (Var var_id) var_id.var_type
with Not_found ->
try (* id is a constant *)
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
- mk_val (LocalVar vdecl) vdecl.var_type
+ mk_val (Var vdecl) vdecl.var_type
with Not_found ->
(* id is a tag *)
(* DONE construire une liste des enum declarés et alors chercher dedans la liste
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index e35e3286a3d8693f3ae5cce0cbaa5a8c1c1369af..6faaab317277ce35524a4d21272dbdd00f40ccbf 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -4,26 +4,32 @@ open Corelang
let print_statelocaltag = true
-let rec pp_val fmt v =
+let is_memory m id =
+ List.exists (fun o -> o.var_id = id.var_id) m.mmemory
+
+let rec pp_val m fmt v =
+ let pp_val = pp_val m in
match v.value_desc with
- | Cst c -> Printers.pp_const fmt c
- | LocalVar v ->
+ | Cst c -> Printers.pp_const fmt c
+ | Var v ->
+ if is_memory m v then
if print_statelocaltag then
- Format.fprintf fmt "%s(L)" v.var_id
+ Format.fprintf fmt "%s(S)" v.var_id
else
- Format.pp_print_string fmt v.var_id
-
- | StateVar v ->
+ Format.pp_print_string fmt v.var_id
+ else
if print_statelocaltag then
- Format.fprintf fmt "%s(S)" v.var_id
+ Format.fprintf fmt "%s(L)" v.var_id
else
Format.pp_print_string fmt v.var_id
- | Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
- | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
- | Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
- | Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
-
-let rec pp_instr fmt i =
+ | Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
+ | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
+ | Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
+ | Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
+
+let rec pp_instr m fmt i =
+ let pp_val = pp_val m and
+ pp_branch = pp_branch m in
let _ =
match i.instr_desc with
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
@@ -51,11 +57,11 @@ let rec pp_instr fmt i =
in
()
-and pp_branch fmt (t, h) =
- Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
+and pp_branch m fmt (t, h) =
+ Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," (pp_instr m)) h
-and pp_instrs fmt il =
- Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il
+and pp_instrs m fmt il =
+ Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m)) il
(* merge log: get_node_def was in c0f8 *)
@@ -75,14 +81,14 @@ let get_node_def id m =
(* merge log: machine_vars was in 44686 *)
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
-let pp_step fmt s =
+let pp_step m fmt s =
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
- (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks
- (Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs
- (Utils.fprintf_list ~sep:", " pp_val) s.step_asserts
+ (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val m fmt c)) s.step_checks
+ (Utils.fprintf_list ~sep:"@ " (pp_instr m)) s.step_instrs
+ (Utils.fprintf_list ~sep:", " (pp_val m)) s.step_asserts
let pp_static_call fmt (node, args) =
@@ -96,9 +102,9 @@ let pp_machine fmt m =
m.mname.node_id
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
- (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
- (Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst
- pp_step m.mstep
+ (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
+ (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
+ (pp_step m) m.mstep
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
@@ -122,8 +128,6 @@ let is_input m id =
let is_output m id =
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
-let is_memory m id =
- List.exists (fun o -> o.var_id = id.var_id) m.mmemory
let mk_conditional ?lustre_eq c t e =
mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
@@ -156,12 +160,12 @@ let arrow_machine =
step_outputs = Arrow.arrow_desc.node_outputs;
step_locals = [];
step_checks = [];
- step_instrs = [mk_conditional (mk_val (StateVar var_state) Type_predef.type_bool)
+ step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
(List.map mkinstr
[MStateAssign(var_state, cst false);
- MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)])
+ MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
(List.map mkinstr
- [MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ];
+ [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
step_asserts = [];
};
mspec = None;
@@ -248,15 +252,15 @@ let value_of_ident loc m id =
(* is is a state var *)
try
let v = List.find (fun v -> v.var_id = id) m.mmemory
- in mk_val (StateVar v) v.var_type
+ in mk_val (Var v) v.var_type
with Not_found ->
try (* id is a node var *)
let v = get_node_var id m.mname
- in mk_val (LocalVar v) v.var_type
+ in mk_val (Var v) v.var_type
with Not_found ->
try (* id is a constant *)
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
- in mk_val (LocalVar c) c.var_type
+ in mk_val (Var c) c.var_type
with Not_found ->
(* id is a tag *)
let t = Const_tag id
@@ -290,7 +294,7 @@ let rec dimension_of_value value =
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i
- | LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id
+ | Var v -> Dimension.mkdim_ident Location.dummy_loc v.var_id
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
| _ -> assert false
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 2cb9f48c55dfd787fb7b7f9e395a5c6aa5c66953..2532298f41a6273296e58a9a7865ffbbbf72ee40 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -1,4 +1,4 @@
-val pp_val: Format.formatter -> Machine_code_types.value_t -> unit
+val pp_val: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.value_t -> unit
val is_memory: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
val is_output: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
val is_const_value: Machine_code_types.value_t -> bool
@@ -11,8 +11,8 @@ val arrow_machine: Machine_code_types.machine_t
val new_instance: Lustre_types.node_desc -> Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
val value_of_dimension: Machine_code_types.machine_t -> Dimension.dim_expr -> Machine_code_types.value_t
val dimension_of_value:Machine_code_types.value_t -> Dimension.dim_expr
-val pp_instr: Format.formatter -> Machine_code_types.instr_t -> unit
-val pp_instrs: Format.formatter -> Machine_code_types.instr_t list -> unit
+val pp_instr: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.instr_t -> unit
+val pp_instrs: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.instr_t list -> unit
val pp_machines: Format.formatter -> Machine_code_types.machine_t list -> unit
val get_machine_opt: string -> Machine_code_types.machine_t list -> Machine_code_types.machine_t option
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 378af262b5b004a3b73d78bf4eb24b1ed49045c7..bcbd889f5ba78549bb846ead9ba9265a92337ac2 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -9,8 +9,7 @@ type value_t =
}
and value_t_desc =
| Cst of constant
- | LocalVar of var_decl
- | StateVar of var_decl
+ | Var of var_decl
| Fun of ident * value_t list
| Array of value_t list
| Access of value_t * value_t
diff --git a/src/normalization.ml b/src/normalization.ml
index f47fbff5e0ec44adaf5a09e7bbf4f0c08a09d050..e84ac596fcd4051baadc8a227a4138113085f732 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -135,9 +135,19 @@ let mk_expr_alias_opt opt node (defs, vars) expr =
| _ ->
match get_expr_alias defs expr with
| Some eq ->
+ (* Format.eprintf "Found a preexisting definition@."; *)
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
(defs, vars), replace_expr aliases expr
| None ->
+ (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
+ * Format.eprintf "existing defs are: @[[%a@]]@."
+ * (fprintf_list ~sep:"@ "(fun fmt eq ->
+ * Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
+ * Clocks.print_ck eq.eq_rhs.expr_clock
+ * (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
+ * (is_eq_expr eq.eq_rhs expr)
+ * Printers.pp_node_eq eq))
+ * defs; *)
if opt
then
let new_aliases =
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index dbdb4a83a4d774acf78d123433c5db3aaf3948ad..ab89af1c150c2797c7339b1e9ee38fe5f981a928 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -18,15 +18,15 @@ open Machine_code_common
open Dimension
-let pp_elim fmt elim =
+let pp_elim m fmt elim =
begin
Format.fprintf fmt "@[{ /* elim table: */@ ";
- IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v pp_val expr) elim;
+ IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v (pp_val m) expr) elim;
Format.fprintf fmt "}@ @]";
end
-let rec eliminate elim instr =
- let e_expr = eliminate_expr elim in
+let rec eliminate m elim instr =
+ let e_expr = eliminate_expr m elim in
match get_instr_desc instr with
| MComment _ -> instr
| MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
@@ -39,20 +39,21 @@ let rec eliminate elim instr =
MBranch
(e_expr g,
(List.map
- (fun (l, il) -> l, List.map (eliminate elim) il)
+ (fun (l, il) -> l, List.map (eliminate m elim) il)
hl
)
)
)
-and eliminate_expr elim expr =
+and eliminate_expr m elim expr =
+ let eliminate_expr = eliminate_expr m in
match expr.value_desc with
- | LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr)
+ | Var v -> if is_memory m v then expr else (try IMap.find v.var_id elim with Not_found -> expr)
| Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
| Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
| Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
| Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
- | Cst _ | StateVar _ -> expr
+ | Cst _ -> expr
let eliminate_dim elim dim =
Dimension.expr_replace_expr
@@ -95,8 +96,7 @@ let simplify_expr_offset m expr =
| _ , Fun (id, vl) when Basic_library.is_value_internal_fun expr
-> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
| _ , Fun _
- | _ , StateVar _
- | _ , LocalVar _ -> unfold_expr_offset m offset expr
+ | _ , Var _ -> unfold_expr_offset m offset expr
| _ , Cst cst -> simplify_cst_expr m offset expr.value_type cst
| _ , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
| [] , _ -> expr
@@ -151,8 +151,7 @@ let is_unfoldable_expr fanin expr =
let rec unfold offset expr =
match offset, expr.value_desc with
| _ , Cst cst -> unfold_const offset cst
- | _ , LocalVar _
- | _ , StateVar _ -> true
+ | _ , Var _ -> true
| [] , Power _
| [] , Array _ -> false
| Index i :: q, Power (v, _) -> unfold q v
@@ -188,28 +187,28 @@ let merge_elim elim1 elim2 =
(* see if elim has to take in account the provided instr:
if so, update elim and return the remove flag,
otherwise, the expression should be kept and elim is left untouched *)
-let rec instrs_unfold fanin elim instrs =
+let rec instrs_unfold m fanin elim instrs =
let elim, rev_instrs =
List.fold_left (fun (elim, instrs) instr ->
(* each subexpression in instr that could be rewritten by the elim set is
rewritten *)
- let instr = eliminate elim instr in
+ let instr = eliminate m elim instr in
(* if instr is a simple local assign, then (a) elim is simplified with it (b) it
is stored as the elim set *)
- instr_unfold fanin instrs elim instr
+ instr_unfold m fanin instrs elim instr
) (elim, []) instrs
in elim, List.rev rev_instrs
-and instr_unfold fanin instrs elim instr =
+and instr_unfold m fanin instrs elim instr =
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
match get_instr_desc instr with
(* Simple cases*)
| MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
- -> instr_unfold fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
+ -> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
| MLocalAssign(v, expr) when unfoldable_assign fanin v expr
-> (IMap.add v.var_id expr elim, instrs)
| MBranch(g, hl) when false
- -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold fanin elim l)) hl in
+ -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold m fanin elim l)) hl in
let (elim, branches) =
List.fold_right
(fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches))
@@ -238,10 +237,10 @@ let static_call_unfold elim (inst, (n, args)) =
*)
let machine_unfold fanin elim machine =
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*)
- let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in
- let elim_vars, instrs = instrs_unfold fanin elim_consts machine.mstep.step_instrs in
+ let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
+ let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
let instrs = simplify_instrs_offset machine instrs in
- let checks = List.map (fun (loc, check) -> loc, eliminate_expr elim_vars check) machine.mstep.step_checks in
+ let checks = List.map (fun (loc, check) -> loc, eliminate_expr machine elim_vars check) machine.mstep.step_checks in
let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
@@ -269,7 +268,7 @@ let instr_of_const top_const =
let machines_unfold consts node_schs machines =
List.fold_right (fun m (machines, removed) ->
let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in
- let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts) in
+ let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
let (m, removed_m) = machine_unfold fanin elim_consts m in
(m::machines, IMap.add m.mname.node_id removed_m removed)
)
@@ -278,8 +277,8 @@ let machines_unfold consts node_schs machines =
let get_assign_lhs instr =
match get_instr_desc instr with
- | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type
- | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type
+ | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
+ | MStateAssign(v, e) -> mk_val (Var v) e.value_type
| _ -> assert false
let get_assign_rhs instr =
@@ -294,10 +293,9 @@ let is_assign instr =
| MStateAssign _ -> true
| _ -> false
-let mk_assign v e =
+let mk_assign m v e =
match v.value_desc with
- | LocalVar v -> MLocalAssign(v, e)
- | StateVar v -> MStateAssign(v, e)
+ | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
| _ -> assert false
let rec assigns_instr instr assign =
@@ -314,8 +312,7 @@ and assigns_instrs instrs assign =
(*
and substitute_expr subst expr =
match expr with
- | StateVar v
- | LocalVar v -> (try IMap.find expr subst with Not_found -> expr)
+ | Var v -> (try IMap.find expr subst with Not_found -> expr)
| Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
| Array(vl) -> Array(List.map (substitute_expr subst) vl)
| Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
@@ -326,54 +323,67 @@ and substitute_expr subst expr =
i.e. another instr' with the same rhs expression.
Then substitute this expression with the first assigned var
*)
-let subst_instr subst instrs instr =
+let subst_instr m subst instrs instr =
(*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*)
- let instr = eliminate subst instr in
- let v = get_assign_lhs instr in
- let e = get_assign_rhs instr in
- (* Difficulties to merge with unstable. Here is the other code:
-
-try
- let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
- match v.value_desc with
- | LocalVar v ->
- IMap.add v.var_id (get_assign_lhs instr') subst, instrs
- | StateVar v ->
- let lhs' = get_assign_lhs instr' in
- let typ' = lhs'.value_type in
- (match lhs'.value_desc with
- | LocalVar v' ->
- let instr = eliminate subst (mk_assign (mk_val (StateVar v) typ') (mk_val (LocalVar v') typ')) in
- subst, instr :: instrs
- | StateVar v' ->
- let subst_v' = IMap.add v'.var_id (mk_val (StateVar v) typ') IMap.empty in
-let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
- IMap.add v'.var_id (mk_val (StateVar v) typ') subst, instr :: instrs'
- | _ -> assert false)
- | _ -> assert false
- with Not_found -> subst, instr :: instrs
-
-*)
-
-try
- let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
- match v.value_desc with
- | LocalVar v ->
- IMap.add v.var_id (get_assign_lhs instr') subst, instrs
- | StateVar stv ->
- let lhs = get_assign_lhs instr' in
- (match lhs.value_desc with
- | LocalVar v' ->
- let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in
- subst, instr :: instrs
- | StateVar stv' ->
- let subst_v' = IMap.add stv'.var_id v IMap.empty in
- let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
- IMap.add stv'.var_id v subst, instr :: instrs'
- | _ -> assert false)
+ let instr = eliminate m subst instr in
+ let instr_v = get_assign_lhs instr in
+ let instr_e = get_assign_rhs instr in
+ try
+ (* Searching for equivalent asssign *)
+ let instr' = List.find (fun instr' -> is_assign instr' &&
+ get_assign_rhs instr' = instr_e) instrs in
+ (* Registering the instr_v as instr'_v while replacing *)
+ match instr_v.value_desc with
+ | Var v ->
+ if not (is_memory m v) then
+ (* The current instruction defines a local variables, ie not
+ memory, we can just record the relationship and continue
+ *)
+ IMap.add v.var_id (get_assign_lhs instr') subst, instrs
+ else (
+ (* The current instruction defines a memory. We need to keep
+ the definition, simplified *)
+ let instr'_v = get_assign_lhs instr' in
+ (match instr'_v.value_desc with
+ | Var v' ->
+ if not (is_memory m v') then
+ (* We define v' = v. Don't need to update the records. *)
+ let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in
+ subst, instr :: instrs
+ else ( (* Last case, v', the lhs of the previous similar
+ definition is, itself, a memory *)
+
+ (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
+ (* Filtering out the list of instructions:
+ - we copy in the same order the list of instr in instrs (fold_right)
+ - if the current instr is this instr' then apply
+ the elimination with v' -> v on instr' before recording it as an instruction.
+ *)
+ let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
+ let instrs' =
+ snd
+ (List.fold_right
+ (fun instr (ok, instrs) ->
+ (ok || instr = instr',
+ if ok then
+ instr :: instrs
+ else
+ if instr = instr' then
+ instrs
+ else
+ eliminate m subst_v' instr :: instrs))
+ instrs (false, []))
+ in
+ IMap.add v'.var_id instr_v subst, instr :: instrs'
+ )
+ | _ -> assert false)
+ )
| _ -> assert false
- with Not_found -> subst, instr :: instrs
-
+
+ with Not_found ->
+ (* No such equivalent expr: keeping the definition *)
+ subst, instr :: instrs
+
(** Common sub-expression elimination for machine instructions *)
(* - [subst] : hashtable from ident to (simple) definition
it is an equivalence table
@@ -381,22 +391,22 @@ try
- [instrs] : previous instructions, which [instr] is compared against
- [instr] : current instruction, normalized by [subst]
*)
-let rec instr_cse (subst, instrs) instr =
+let rec instr_cse m (subst, instrs) instr =
match get_instr_desc instr with
(* Simple cases*)
| MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
- -> instr_cse (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
+ -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
| MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
-> (IMap.add v.var_id expr subst, instr :: instrs)
| _ when is_assign instr
- -> subst_instr subst instrs instr
+ -> subst_instr m subst instrs instr
| _ -> (subst, instr :: instrs)
(** Apply common sub-expression elimination to a sequence of instrs
*)
-let rec instrs_cse subst instrs =
+let instrs_cse m subst instrs =
let subst, rev_instrs =
- List.fold_left instr_cse (subst, []) instrs
+ List.fold_left (instr_cse m) (subst, []) instrs
in subst, List.rev rev_instrs
(** Apply common sub-expression elimination to a machine
@@ -404,7 +414,7 @@ let rec instrs_cse subst instrs =
*)
let machine_cse subst machine =
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
- let subst, instrs = instrs_cse subst machine.mstep.step_instrs in
+ let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in
let assigned = assigns_instrs instrs VSet.empty
in
{
@@ -427,8 +437,8 @@ let machines_cse machines =
(* checks whether an [instr] is skip and can be removed from program *)
let rec instr_is_skip instr =
match get_instr_desc instr with
- | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true
- | MStateAssign (i, { value_desc = StateVar v; _}) when i = v -> true
+ | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
+ | MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
| MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
| _ -> false
and instrs_are_skip instrs =
@@ -439,8 +449,8 @@ let instr_cons instr cont =
let rec instr_remove_skip instr cont =
match get_instr_desc instr with
- | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont
- | MStateAssign (i, { value_desc = StateVar v; _ }) when i = v -> cont
+ | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
+ | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
| MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
| _ -> instr::cont
@@ -450,8 +460,7 @@ and instrs_remove_skip instrs cont =
let rec value_replace_var fvar value =
match value.value_desc with
| Cst c -> value
- | LocalVar v -> { value with value_desc = LocalVar (fvar v) }
- | StateVar v -> value
+ | Var v -> { value with value_desc = Var (fvar v) }
| Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
| Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
| Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
@@ -547,10 +556,8 @@ let rec instrs_fusion instrs =
| [], []
| [_], [_] ->
instrs
- | i1::i2::q, i1_desc::(MBranch ({ value_desc = LocalVar v; _}, hl))::q_desc when instr_constant_assign v i1 ->
+ | i1::i2::q, i1_desc::(MBranch ({ value_desc = Var v; _}, hl))::q_desc 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_desc::(MBranch ({ value_desc = StateVar v; _}, hl))::q_desc 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 *)
@@ -592,7 +599,7 @@ let optimize prog node_schs machine_code =
".. machines optimization: const. inlining (partial eval. with const)@,");
let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
- (pp_imap pp_elim) removed_table);
+ (pp_imap (pp_elim empty_machine)) removed_table);
Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "pp_machines machine_code);
machine_code, removed_table
end
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
index 659b6b16de89a48702b89d30b371b49f0575adff..2527d19883ecad43a1cad57414f83a132131fb56 100644
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -31,8 +31,8 @@ let called_node_id m id =
let rec get_expr_real_vars e =
let open MT in
match e.value_desc with
- | LocalVar v | StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
- | LocalVar _| StateVar _
+ | Var v when Types.is_real_type v.LT.var_type -> Vars.singleton v
+ | Var _
| Cst _ -> Vars.empty
| Fun (_, args) ->
List.fold_left
@@ -94,7 +94,7 @@ let rec get_written_vars instrs =
(* Optimize a given expression. It returns another expression and a computed range. *)
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * (MT.instr_t list) =
- let rec opt_expr vars_env ranges formalEnv e =
+ let rec opt_expr m vars_env ranges formalEnv e =
let open MT in
match e.value_desc with
| Cst cst ->
@@ -103,15 +103,14 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
constant *)
let typ = Typing.type_const Location.dummy_loc cst in
if Types.is_real_type typ then
- opt_num_expr vars_env ranges formalEnv e
+ opt_num_expr m vars_env ranges formalEnv e
else e, None, []
- | LocalVar v
- | StateVar v ->
+ | Var v ->
if not (Vars.mem v printed_vars) &&
(* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
(Types.is_real_type e.value_type || Types.is_real_type v.LT.var_type)
then
- opt_num_expr vars_env ranges formalEnv e
+ opt_num_expr m vars_env ranges formalEnv e
else
e, None, [] (* Nothing to optimize for expressions containing a single non real variable *)
(* (\* optimize only numerical vars *\) *)
@@ -121,20 +120,20 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
(* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
(* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
if Types.is_real_type e.value_type then
- opt_num_expr vars_env ranges formalEnv e
+ opt_num_expr m vars_env ranges formalEnv e
else (
(* We do not care for computed local ranges. *)
- let args', il = List.fold_right (fun arg (al, il) -> let arg', _, arg_il = opt_expr vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], []) in
+ let args', il = List.fold_right (fun arg (al, il) -> let arg', _, arg_il = opt_expr m vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], []) in
{ e with value_desc = Fun(fun_id, args')}, None, il
)
)
| Array _
| Access _
| Power _ -> assert false
- and opt_num_expr vars_env ranges formalEnv e =
+ and opt_num_expr m vars_env ranges formalEnv e =
if !debug then (
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Optimizing expression %a@ "
- MC.pp_val e);
+ (MC.pp_val m) e);
);
(* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e; *)
let fresh_id = "toto" in (* TODO more meaningful name *)
@@ -182,7 +181,7 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
if Vars.cardinal free_vars > 0 then (
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ "
Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)
- MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
+ (MC.pp_val m) (salsa_expr2value_t vars_env constEnv e_salsa));
if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Some free vars, not optimizing@ ");
if !debug then Log.report ~level:3 (fun fmt -> Format.fprintf fmt " ranges: %a@ "
RangesInt.pp ranges);
@@ -198,7 +197,7 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
try
if !debug then
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Analyzing expression %a with ranges: @[<v>%a@ @]@ "
- (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
+ (C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv)
;
@@ -286,9 +285,9 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
Format.fprintf fmt "Improved!";
Format.fprintf fmt
" @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ "
- MC.pp_val e
+ (MC.pp_val m) e
RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv [])
- MC.pp_val new_e
+ (MC.pp_val m) new_e
RangesInt.pp_val e_val
)
| false, true -> Format.eprintf "Error; new range is worse!@.@?"; assert false
@@ -297,7 +296,7 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
new_e, Some e_val, List.rev rev_def_tmp_instrs
with (* Not_found -> *)
| Salsa.Epeg_types.EPEGError _ -> (
- Log.report ~level:2 (fun fmt -> Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e);
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " (MC.pp_val m) e);
e, None, []
)
)
@@ -305,7 +304,7 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
in
- opt_expr vars_env ranges formalEnv e
+ opt_expr m vars_env ranges formalEnv e
(* Returns a list of assign, for each var in vars_to_print, that produce the
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
index 572ad9eb285afbf8ff8a56878c54b41b8d0df5ce..9a8fe8c22a0a042f5873fc571f7a59fa4e98af93 100644
--- a/src/plugins/salsa/salsaDatatypes.ml
+++ b/src/plugins/salsa/salsaDatatypes.ml
@@ -173,8 +173,7 @@ let rec value_t2salsa_expr constEnv vt =
(* raise (Salsa.Prelude.Error ("Entschuldigung6, constant tag not yet implemented")) *)
(* ) *)
| MT.Cst(cst) -> (* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst; *)FloatIntSalsa.inject cst
- | MT.LocalVar(v)
- | MT.StateVar(v) -> (* Format.eprintf "v2s: var %s@." v.LT.var_id; *)
+ | MT.Var(v) -> (* Format.eprintf "v2s: var %s@." v.LT.var_id; *)
let sel_fun = (fun (vname, _) -> v.LT.var_id = vname) in
if List.exists sel_fun constEnv then
let _, cst = List.find sel_fun constEnv in
@@ -295,10 +294,7 @@ let rec salsa_expr2value_t vars_env cst_env e =
(* MC.Cst(LT.Const_tag(get_const salsa_label)) *)
(* else *)
let var_id = try get_var vars_env id with Not_found -> assert false in
- if var_id.is_local then
- MC.mk_val (MT.LocalVar(var_id.vdecl)) var_id.vdecl.LT.var_type
- else
- MC.mk_val (MT.StateVar(var_id.vdecl)) var_id.vdecl.LT.var_type
+ MC.mk_val (MT.Var(var_id.vdecl)) var_id.vdecl.LT.var_type
| ST.Plus(x, y, _) -> binop "+" x y Type_predef.type_real
| ST.Minus(x, y, _) -> binop "-" x y Type_predef.type_real
| ST.Times(x, y, _) -> binop "*" x y Type_predef.type_real
@@ -368,7 +364,7 @@ struct
let empty (): fe_t = Hashtbl.create 13
- let pp fmt env = pp_hash ~sep:";@ " (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k MC.pp_val v) fmt env
+ let pp m fmt env = pp_hash ~sep:";@ " (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k (MC.pp_val m) v) fmt env
let get_sort_fun env =
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 60dd25461c92a111e6ef94cc969987197001e1da..01c60f4ae8b46893de88dc153f148fcf420f6258 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -221,7 +221,7 @@ let pp_scopes fmt scopes =
let update_machine machine =
let stateassign vdecl =
mkinstr
- (MStateAssign (vdecl, mk_val (LocalVar vdecl) vdecl.var_type))
+ (MStateAssign (vdecl, mk_val (Var vdecl) vdecl.var_type))
in
let local_decls = machine.mstep.step_inputs
(* @ machine.mstep.step_outputs *)