From c35de73b71b6578752eb4f2328c1f91c907fe6e1 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 14 Nov 2018 18:18:06 -0800
Subject: [PATCH] Pretty serious update: - a bug in regressio ntest
Simulink/integrator_ext_IC_matrix_test revealed the following (serious
issue): when building the list of instruction (in the machine code) the
access to variable were hardcoded to LocalVar or StateVAr depending whether
the variables was part of the identified memories. Un fortunately the set
of memories is only known after iterating through all definitions. A read
access to a memory which was scheduled before its update was generating a non
compilable C code: the access to the memory x which should be written as
mem->x was written as a local access "x". But x was not declared as a local
variable: hence gcc compile error.
The current commit is pretty involved. It goes through all the code:
- LocalVar and StateVar have been merged in Var in machine instructions (rhs ie expressions)
- any possible print or access to these shall be given access to the machine (ie its memories)
so a lot of functions have been enriched with a machine first argument.
Regression tests performed well showing no additional bug introduced. The only Unstable->Broken changes are the DIFF which could not be run at all before.
---
src/backends/C/c_backend_common.ml | 58 +++----
src/backends/C/c_backend_header.ml | 2 +-
src/backends/C/c_backend_main.ml | 2 +-
src/backends/C/c_backend_src.ml | 79 ++++-----
src/backends/EMF/EMF_backend.ml | 13 +-
src/backends/EMF/EMF_common.ml | 13 +-
src/backends/EMF/EMF_library_calls.ml | 2 +-
src/backends/Horn/horn_backend_printers.ml | 63 +++----
src/backends/Java/java_backend.ml | 14 +-
src/corelang.ml | 11 +-
src/corelang.mli | 5 +-
src/machine_code.ml | 13 +-
src/machine_code_common.ml | 72 ++++----
src/machine_code_common.mli | 6 +-
src/machine_code_types.ml | 3 +-
src/normalization.ml | 10 ++
src/optimize_machine.ml | 189 +++++++++++----------
src/plugins/salsa/machine_salsa_opt.ml | 33 ++--
src/plugins/salsa/salsaDatatypes.ml | 10 +-
src/plugins/scopes/scopes.ml | 2 +-
20 files changed, 312 insertions(+), 288 deletions(-)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index ae3c5cb9..11e823e1 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 1b796e0f..7a23dc82 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 e1f85364..90f3862e 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 29506130..d7d1eaaa 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 4d736e27..9f2c2f4a 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 381df16d..bb9f47e2 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 353dbf59..d34eb965 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 cbd28ba5..62e291da 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 5708cb42..8783933b 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 300713c3..081647ec 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 05a62bdc..9b9343bf 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 b2205dbc..e670ddac 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 e35e3286..6faaab31 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 2cb9f48c..2532298f 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 378af262..bcbd889f 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 f47fbff5..e84ac596 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 dbdb4a83..ab89af1c 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 659b6b16..2527d198 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 572ad9eb..9a8fe8c2 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 60dd2546..01c60f4a 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 *)
--
GitLab