From 3addb23bd0208153f1bfc245f2256d3b9c3afd5d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Fri, 3 Mar 2023 15:41:15 +0900
Subject: [PATCH] fix removed plugins files by mistake...
---
src/plugins/salsa/machine_salsa_opt.ml | 1067 +++++++++++++++++++++++
src/plugins/salsa/machine_salsa_opt.mli | 0
src/plugins/salsa/salsaDatatypes.ml | 440 ++++++++++
src/plugins/salsa/salsaDatatypes.mli | 0
src/plugins/salsa/salsa_plugin.ml | 60 ++
src/plugins/salsa/salsa_plugin.mli | 0
src/plugins/scopes/scopes.ml | 468 ++++++++++
src/plugins/scopes/scopes.mli | 14 +
8 files changed, 2049 insertions(+)
create mode 100644 src/plugins/salsa/machine_salsa_opt.ml
create mode 100644 src/plugins/salsa/machine_salsa_opt.mli
create mode 100644 src/plugins/salsa/salsaDatatypes.ml
create mode 100644 src/plugins/salsa/salsaDatatypes.mli
create mode 100644 src/plugins/salsa/salsa_plugin.ml
create mode 100644 src/plugins/salsa/salsa_plugin.mli
create mode 100644 src/plugins/scopes/scopes.ml
create mode 100644 src/plugins/scopes/scopes.mli
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
new file mode 100644
index 00000000..1ebd7bfe
--- /dev/null
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -0,0 +1,1067 @@
+(* We try to avoid opening modules here *)
+module ST = Salsa.Types
+module SDT = SalsaDatatypes
+module LT = Lustre_types
+module MC = Machine_code
+
+(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
+open SalsaDatatypes
+
+let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level
+
+(******************************************************************)
+(* TODO Xavier: should those functions be declared more globally? *)
+
+let fun_types node =
+ try
+ match node.LT.top_decl_desc with
+ | LT.Node nd ->
+ let tin, tout = Types.split_arrow nd.LT.node_type in
+ Types.type_list_of_type tin, Types.type_list_of_type tout
+ | _ ->
+ Format.eprintf "%a is not a node@.@?" Printers.pp_decl node;
+ assert false
+ with Not_found ->
+ Format.eprintf
+ "Unable to find type def for function %s@.@?"
+ (Corelang.node_name node);
+ assert false
+
+let called_node_id m id =
+ let td, _ =
+ try List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *)
+ with Not_found -> assert false
+ in
+ td
+(******************************************************************)
+
+(* Returns the set of vars that appear in the expression *)
+let rec get_expr_real_vars e =
+ let open MT in
+ match e.value_desc with
+ | Var v when Types.is_real_type v.LT.var_type ->
+ Vars.singleton v
+ | Var _ | Cst _ ->
+ Vars.empty
+ | Fun (_, args) ->
+ List.fold_left
+ (fun acc e -> Vars.union acc (get_expr_real_vars e))
+ Vars.empty
+ args
+ | Array _ | Access _ | Power _ ->
+ assert false
+
+(* Extract the variables to appear as free variables in expressions (lhs) *)
+let rec get_read_vars instrs =
+ let open MT in
+ match instrs with
+ | [] ->
+ Vars.empty
+ | i :: tl -> (
+ let vars_tl = get_read_vars tl in
+ match Corelang.get_instr_desc i with
+ | MLocalAssign (_, e) | MStateAssign (_, e) ->
+ Vars.union (get_expr_real_vars e) vars_tl
+ | MStep (_, _, el) ->
+ List.fold_left
+ (fun accu e -> Vars.union (get_expr_real_vars e) accu)
+ vars_tl
+ el
+ | MBranch (e, branches) ->
+ let vars = Vars.union (get_expr_real_vars e) vars_tl in
+ List.fold_left
+ (fun vars (_, b) -> Vars.union vars (get_read_vars b))
+ vars
+ branches
+ | MReset _ | MNoReset _ | MSpec _ | MComment _ ->
+ Vars.empty)
+
+let rec get_written_vars instrs =
+ let open MT in
+ match instrs with
+ | [] ->
+ Vars.empty
+ | i :: tl -> (
+ let vars_tl = get_written_vars tl in
+ match Corelang.get_instr_desc i with
+ | MLocalAssign (v, _) | MStateAssign (v, _) ->
+ Vars.add v vars_tl
+ | MStep (vdl, _, _) ->
+ List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
+ | MBranch (_, branches) ->
+ List.fold_left
+ (fun vars (_, b) -> Vars.union vars (get_written_vars b))
+ vars_tl
+ branches
+ | MReset _ | MNoReset _ | MSpec _ | MComment _ ->
+ Vars.empty)
+
+(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *)
+(* let new_expr, new_range = *)
+(* Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv *)
+(* in *)
+(* Format.eprintf "New range: %a@." RangesInt.pp_val new_range; *)
+(* if Salsa.Float.errLt new_range old_range < 0 then *)
+
+(* iterTransformExpr fresh_id new_expr abstractEnv new_range *)
+(* else *)
+(* new_expr, new_range *)
+
+(* Takes as input a salsa expression and return an optimized one *)
+let opt_num_expr_sliced ranges e_salsa =
+ try
+ let fresh_id = "toto" in
+
+ (* TODO more meaningful name *)
+ let abstractEnv = RangesInt.to_abstract_env ranges in
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "Launching analysis: %s@ "
+ (Salsa.Print.printExpression e_salsa));
+ let new_e_salsa, e_val =
+ Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
+ in
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ " Analysis done: %s@ "
+ (Salsa.Print.printExpression new_e_salsa));
+
+ (* (\* Debug *\) *)
+ (* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *)
+ (* (Salsa.Print.printExpression e_salsa) *)
+ (* (Salsa.Print.printExpression new_e_salsa); *)
+ (* (\* Debug *\) *)
+ report ~level:2 (fun fmt ->
+ Format.fprintf fmt " Computing range progress@ ");
+
+ let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
+ let expr, expr_range =
+ match
+ RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val
+ with
+ | true, true ->
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "No improvement on abstract value %a@ "
+ RangesInt.pp_val
+ e_val);
+ e_salsa, Some old_val
+ | false, true ->
+ if !debug then
+ report ~level:2 (fun fmt -> Format.fprintf fmt "Improved!@ ");
+ new_e_salsa, Some e_val
+ | true, false ->
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "CAREFUL --- new range is worse!. Restoring provided expression@ ");
+ e_salsa, Some old_val
+ | false, false ->
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "Error; new range is not comparable with old end. It may need \
+ some investigation!@. ";
+ Format.fprintf
+ fmt
+ "old: %a@.new: %a@ "
+ RangesInt.pp_val
+ old_val
+ RangesInt.pp_val
+ e_val);
+
+ new_e_salsa, Some e_val
+ (* assert false *)
+ in
+ report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range done@ ");
+
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ " @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ \
+ range: %a@]@ @]@ "
+ (Salsa.Print.printExpression e_salsa)
+ (* MC.pp_val e *)
+ RangesInt.pp_val
+ old_val
+ (Salsa.Print.printExpression new_e_salsa)
+ (* MC.pp_val new_e *)
+ RangesInt.pp_val
+ e_val);
+ expr, expr_range
+ with (* Not_found -> *)
+ | Salsa.Epeg_types.EPEGError _ ->
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "BECAUSE OF AN ERROR, Expression %s was not optimized@ "
+ (Salsa.Print.printExpression e_salsa)
+ (* MC.pp_val e *));
+ e_salsa, None
+
+(* Optimize a given expression. It returns the modified expression, a computed
+ range and freshly defined variables. *)
+let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
+ MT.value_t * RangesInt.t option * MT.instr_t list * Vars.VarSet.t =
+ let rec opt_expr m vars_env ranges formalEnv e =
+ let open MT in
+ match e.value_desc with
+ | Cst cst ->
+ (* Format.eprintf "optmizing constant expr @ "; *)
+ (* the expression is a constant, we optimize it directly if it is a real
+ constant *)
+ let typ = Typing.type_const Location.dummy_loc cst in
+ if Types.is_real_type typ then opt_num_expr m vars_env ranges formalEnv e
+ else e, None, [], Vars.empty
+ | 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 m vars_env ranges formalEnv e
+ else e, None, [], Vars.empty
+ (* Nothing to optimize for expressions containing a single non real variable *)
+ (* (\* optimize only numerical vars *\) *)
+ (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges
+ formalEnv e *)
+ (* else e, None *)
+ | Fun (fun_id, args) ->
+ if
+ (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
+ (* if the return type is real then optimize it, otherwise call
+ recusrsively on arguments *)
+ Types.is_real_type e.value_type
+ then opt_num_expr m vars_env ranges formalEnv e
+ else
+ (* We do not care for computed local ranges. *)
+ let args', il, new_locals =
+ List.fold_right
+ (fun arg (al, il, nl) ->
+ let arg', _, arg_il, arg_nl =
+ opt_expr m vars_env ranges formalEnv arg
+ in
+ arg' :: al, arg_il @ il, Vars.union arg_nl nl)
+ args
+ ([], [], Vars.empty)
+ in
+ { e with value_desc = Fun (fun_id, args') }, None, il, new_locals
+ | Array _ | Access _ | Power _ ->
+ assert false
+ and opt_num_expr m vars_env ranges formalEnv e =
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "Optimizing expression @[<hov>%a@]@ "
+ (MC.pp_val m)
+ e);
+ (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ "
+ MC.pp_val e; *)
+ (* Convert expression *)
+ (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const
+ c) constEnv; *)
+ let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
+
+ (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val
+ (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ; *)
+
+ (* Convert formalEnv *)
+ (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp
+ formalEnv; *)
+ (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
+
+ (* Format.eprintf "Expression avant et apres substVars.@.Avant %a@."
+ MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *)
+
+ (* Substitute all occurences of variables by their definition in env *)
+ let (e_salsa : Salsa.Types.expression), _ =
+ Salsa.Rewrite.substVars e_salsa (FormalEnv.to_salsa constEnv formalEnv) 0
+ (* TODO: Nasrine, what is this integer value for ? *)
+ in
+
+ (* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env []
+ e_salsa) ; *)
+
+ (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
+ let abstractEnv = RangesInt.to_abstract_env ranges in
+ (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id)
+ abstractEnv; *)
+ (* The expression is partially evaluated by the available ranges
+ valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
+ garde evalPartExpr remplace les variables e qui sont dans env par la cst
+ - on garde *)
+ (* if !debug then Format.eprintf "avant avant eval part@ "; *)
+ (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t
+ vars_env constEnv e_salsa); *)
+ let e_salsa =
+ Salsa.Analyzer.evalPartExpr
+ e_salsa
+ (Salsa.Analyzer.valEnv2ExprEnv abstractEnv)
+ []
+ (* no blacklisted variables *) []
+ (* no arrays *)
+ in
+
+ (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t
+ vars_env constEnv e_salsa); *)
+ (* Checking if we have all necessary information *)
+ let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
+ if Vars.cardinal free_vars > 0 then (
+ 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 m)
+ (salsa_expr2value_t vars_env constEnv e_salsa));
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf fmt "Some free vars, not optimizing@ ");
+ if !debug then
+ report ~level:3 (fun fmt ->
+ Format.fprintf fmt " ranges: %a@ " RangesInt.pp ranges);
+
+ (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt
+ "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
+ let new_e =
+ try salsa_expr2value_t vars_env constEnv e_salsa
+ with Not_found -> assert false
+ in
+ new_e, None, [], Vars.empty)
+ else (
+ if !debug then
+ report ~level:3 (fun fmt ->
+ Format.fprintf
+ fmt
+ "@[<v 2>Analyzing expression %a@ with ranges: @[<v>%a@ @]@ @]@ "
+ (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);
+
+ (* Slicing expression *)
+ let e_salsa, seq =
+ try
+ Salsa.Rewrite.sliceExpr
+ e_salsa
+ 0
+ (Salsa.Types.Nop (Salsa.Types.Lab 0))
+ with _ ->
+ Format.eprintf
+ "Issues rewriting express %s@.@?"
+ (Salsa.Print.printExpression e_salsa);
+ assert false
+ in
+ let def_tmps = Salsa.Utils.flatten_seq seq [] in
+ (* Registering tmp ids in vars_env *)
+ let vars_env', new_local_vars =
+ List.fold_left
+ (fun (vs, vars) (id, _) ->
+ let vdecl =
+ Corelang.mk_fresh_var
+ (nodename.node_id, [])
+ (* TODO check that the empty env is ok. One may need to build or
+ access to the current env *)
+ Location.dummy_loc
+ e.MT.value_type
+ (Clocks.new_var true)
+ in
+
+ let vs' = VarEnv.add id { vdecl; is_local = true } vs in
+ let vars' = Vars.add vdecl vars in
+ vs', vars')
+ (vars_env, Vars.empty)
+ def_tmps
+ in
+ (* Debug *)
+ if !debug then
+ report ~level:3 (fun fmt ->
+ Format.fprintf
+ fmt
+ "List of slices: @[<v 0>%a@]@ "
+ (Utils.fprintf_list ~sep:"@ " (fun fmt (id, e_id) ->
+ Format.fprintf
+ fmt
+ "(%s,%a) -> %a"
+ id
+ Printers.pp_var
+ (get_var vars_env' id).vdecl
+ (C_backend_common.pp_c_val
+ m
+ ""
+ (C_backend_common.pp_c_var_read m))
+ (salsa_expr2value_t vars_env' constEnv e_id)))
+ def_tmps;
+ Format.fprintf
+ fmt
+ "Sliced expression: %a@ "
+ (C_backend_common.pp_c_val
+ m
+ ""
+ (C_backend_common.pp_c_var_read m))
+ (salsa_expr2value_t vars_env' constEnv e_salsa));
+
+ (* Debug *)
+
+ (* Optimize def tmp, and build the associated instructions. Update the
+ abstract Env with computed ranges *)
+ if !debug && List.length def_tmps >= 1 then
+ report ~level:3 (fun fmt ->
+ Format.fprintf fmt "@[<v 3>Optimizing sliced sub-expressions@ ");
+ let rev_def_tmp_instrs, ranges =
+ List.fold_left
+ (fun (accu_instrs, ranges) (id, e_id) ->
+ (* Format.eprintf "Cleaning/Optimizing %s@." id; *)
+ let e_id', e_range =
+ (*Salsa.MainEPEG.transformExpression id e_id abstractEnv*)
+ opt_num_expr_sliced ranges e_id
+ in
+ let new_e_id' =
+ try salsa_expr2value_t vars_env' constEnv e_id'
+ with Not_found -> assert false
+ in
+
+ let vdecl = (get_var vars_env' id).vdecl in
+
+ let new_local_assign =
+ (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
+ MT.MLocalAssign (vdecl, new_e_id')
+ in
+ let new_local_assign =
+ {
+ MT.instr_desc = new_local_assign;
+ MT.lustre_eq =
+ None
+ (* could be Corelang.mkeq Location.dummy_loc
+ ([vdecl.LT.var_id], e_id) provided it is converted as
+ Lustre expression rather than a Machine code value *);
+ }
+ in
+ let new_ranges =
+ match e_range with
+ | None ->
+ ranges
+ | Some e_range ->
+ RangesInt.add_def ranges id e_range
+ in
+ new_local_assign :: accu_instrs, new_ranges)
+ ([], ranges)
+ def_tmps
+ in
+ if !debug && List.length def_tmps >= 1 then
+ report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ");
+
+ (* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a"
+ (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *)
+ let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in
+ let expr =
+ try salsa_expr2value_t vars_env' constEnv expr_salsa
+ with Not_found -> assert false
+ in
+
+ expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars
+ (* ???? Bout de code dans unstable lors du merge avec salsa ? ====
+
+ let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa with
+ Not_found -> assert false in if !debug then Log.report ~level:2 (fun
+ fmt -> let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv []
+ in match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val
+ old_range with | true, true -> Format.fprintf fmt "No improvement on
+ abstract value %a@ " RangesInt.pp_val e_val | true, false -> (
+ 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 m) e RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa
+ abstractEnv []) (MC.pp_val m) new_e RangesInt.pp_val e_val ) | false,
+ true -> Format.eprintf "Error; new range is worse!@.@?"; assert false |
+ false, false -> Format.eprintf "Error; new range is not comparabe with
+ old end. This should not happen!@.@?"; assert false ); 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 m) e); e, None, [] ) >>>>>>> unstable *))
+ in
+
+ opt_expr m vars_env ranges formalEnv e
+
+(* Returns a list of assign, for each var in vars_to_print, that produce the
+ definition of it according to formalEnv, and driven by the ranges. *)
+let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv
+ vars_to_print =
+ (* We print thhe expression in the order of definition *)
+ let ordered_vars =
+ List.stable_sort
+ (FormalEnv.get_sort_fun formalEnv)
+ (Vars.elements vars_to_print)
+ in
+ if !debug then
+ report ~level:4 (fun fmt ->
+ Format.fprintf
+ fmt
+ "Printing vars in the following order: [%a]@ "
+ (Utils.fprintf_list ~sep:", " Printers.pp_var)
+ ordered_vars);
+
+ List.fold_right
+ (fun v (accu_instr, accu_ranges, accu_new_locals) ->
+ if !debug then
+ report ~level:4 (fun fmt ->
+ Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
+ try
+ (* Obtaining unfold expression of v in formalEnv *)
+ let v_def = FormalEnv.get_def formalEnv v in
+ let e, r, il, new_v_locals =
+ optimize_expr
+ nodename
+ m
+ constEnv
+ printed_vars
+ vars_env
+ ranges
+ formalEnv
+ v_def
+ in
+ let instr_desc =
+ if
+ try (get_var vars_env v.LT.var_id).is_local
+ with Not_found -> assert false
+ then MT.MLocalAssign (v, e)
+ else MT.MStateAssign (v, e)
+ in
+ ( il @ (Corelang.mkinstr instr_desc :: accu_instr),
+ (match r with
+ | None ->
+ ranges
+ | Some v_r ->
+ RangesInt.add_def ranges v.LT.var_id v_r),
+ Vars.union accu_new_locals new_v_locals )
+ with FormalEnv.NoDefinition _ ->
+ if
+ (* It should not happen with C backend, but may happen with Lustre
+ backend *)
+ !Options.output = "lustre"
+ then accu_instr, ranges, Vars.empty
+ else (
+ Format.eprintf "@?";
+ assert false))
+ ordered_vars
+ ([], ranges, Vars.empty)
+
+(* Main recursive function: modify the instructions list while preserving the
+ order of assigns for state variables. Returns a quintuple: (new_instrs,
+ ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
+let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv
+ printed_vars vars_to_print =
+ let formal_env_def = FormalEnv.def constEnv vars_env in
+ (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
+ let assign_vars = assign_vars nodename m constEnv vars_env in
+ (* if !debug then ( *)
+ (* Log.report ~level:3 (fun fmt -> Format.fprintf fmt *)
+ (* "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
+ (* Vars.pp printed_vars *)
+ (* Vars.pp vars_to_print *)
+ (* FormalEnv.pp formalEnv) *)
+ (* ); *)
+ match instrs with
+ | [] ->
+ (* End of instruction list: we produce the definition of each variable that
+ appears in vars_to_print. Each of them should be defined in formalEnv *)
+ (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp
+ vars_to_print; *)
+ let instrs, ranges', new_expr_locals =
+ assign_vars printed_vars ranges formalEnv vars_to_print
+ in
+ ( instrs,
+ ranges',
+ formalEnv,
+ Vars.union printed_vars vars_to_print,
+ (* We should have printed all required vars *)
+ [],
+ (* No more vars to be printed *)
+ Vars.empty )
+ | hd_instr :: tl_instrs ->
+ (* We reformulate hd_instr, producing or not a fresh instruction, updating
+ formalEnv, possibly ranges and vars_to_print *)
+ let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals
+ =
+ match Corelang.get_instr_desc hd_instr with
+ | MT.MLocalAssign (vd, vt)
+ when Types.is_real_type vd.LT.var_type
+ && not (Vars.mem vd vars_to_print) ->
+ (* LocalAssign are injected into formalEnv *)
+ (* if !debug then Format.eprintf "Registering local assign %a@ "
+ MC.pp_instr hd_instr; *)
+ (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
+ let formalEnv' = formal_env_def formalEnv vd vt in
+ (* formelEnv updated with vd = vt *)
+ ( [],
+ (* no instr generated *)
+ ranges,
+ (* no new range computed *)
+ formalEnv',
+ printed_vars,
+ (* no new printed vars *)
+ vars_to_print,
+ (* no more or less variables to print *)
+ Vars.empty )
+ (* no new locals *)
+ | MT.MLocalAssign (vd, vt)
+ when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
+ (* if !debug then Format.eprintf "Registering and producing state assign
+ %a@ " MC.pp_instr hd_instr; *)
+ (* if !debug then Format.eprintf "Registering and producing state assign
+ %a@ " MC.pp_instr hd_instr; *)
+ (* if !debug then ( *)
+ (* Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
+ (* Format.eprintf "Selected var %a: producing expression@ "
+ Printers.pp_var vd; *)
+ (* ); *)
+ let formalEnv' = formal_env_def formalEnv vd vt in
+ (* formelEnv updated with vd = vt *)
+ let instrs', ranges', expr_new_locals =
+ (* printing vd = optimized vt *)
+ assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
+ in
+ ( instrs',
+ ranges',
+ (* no new range computed *)
+ formalEnv',
+ (* formelEnv already updated *)
+ Vars.add vd printed_vars,
+ (* adding vd to new printed vars *)
+ Vars.remove vd vars_to_print,
+ (* removed vd from variables to print *)
+ expr_new_locals )
+ (* adding sliced vardecl to the list *)
+ | MT.MStateAssign (vd, vt)
+ when Types.is_real_type vd.LT.var_type
+ (* && Vars.mem vd vars_to_print *) ->
+ (* StateAssign are produced since they are required by the function. We
+ still keep their definition in the formalEnv in case it can optimize
+ later outputs. vd is removed from remaining vars_to_print *)
+ (* if !debug then Format.eprintf "Registering and producing state assign
+ %a@ " MC.pp_instr hd_instr; *)
+ (* if !debug then ( *)
+ (* Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
+ (* Format.eprintf "State assign %a: producing expression@ "
+ Printers.pp_var vd; *)
+ (* ); *)
+ let formalEnv' = formal_env_def formalEnv vd vt in
+ (* formelEnv updated with vd = vt *)
+ let instrs', ranges', expr_new_locals =
+ (* printing vd = optimized vt *)
+ assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
+ in
+ ( instrs',
+ ranges',
+ (* no new range computed *)
+ formalEnv,
+ (* formelEnv already updated *)
+ Vars.add vd printed_vars,
+ (* adding vd to new printed vars *)
+ Vars.remove vd vars_to_print,
+ (* removed vd from variables to print *)
+ expr_new_locals )
+ (* adding sliced vardecl to the list *)
+ | MT.MLocalAssign (vd, vt) | MT.MStateAssign (vd, vt) ->
+ (* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *)
+
+ (* We have to produce the instruction. But we may have to produce as
+ well its dependencies *)
+ let required_vars = get_expr_real_vars vt in
+ let required_vars = Vars.diff required_vars printed_vars in
+ (* remove already produced variables *)
+ (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
+ let required_vars =
+ Vars.diff required_vars (Vars.of_list m.MT.mmemory)
+ in
+ let prefix_instr, ranges, new_expr_dep_locals =
+ assign_vars printed_vars ranges formalEnv required_vars
+ in
+
+ let vt', _, il, expr_new_locals =
+ optimize_expr
+ nodename
+ m
+ constEnv
+ (Vars.union required_vars printed_vars)
+ vars_env
+ ranges
+ formalEnv
+ vt
+ in
+ let new_instr =
+ match Corelang.get_instr_desc hd_instr with
+ | MT.MLocalAssign _ ->
+ Corelang.update_instr_desc hd_instr (MT.MLocalAssign (vd, vt'))
+ | _ ->
+ Corelang.update_instr_desc hd_instr (MT.MStateAssign (vd, vt'))
+ in
+ let written_vars = Vars.add vd required_vars in
+ ( prefix_instr @ il @ [ new_instr ],
+ ranges,
+ (* no new range computed *)
+ formalEnv,
+ (* formelEnv untouched *)
+ Vars.union written_vars printed_vars,
+ (* adding vd + dependencies to new printed vars *)
+ Vars.diff vars_to_print written_vars,
+ (* removed vd + dependencies from variables to print *)
+ Vars.union new_expr_dep_locals expr_new_locals )
+ | MT.MStep (vdl, id, vtl) ->
+ (* Format.eprintf "step@."; *)
+
+ (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr
+ hd_instr; *)
+ (* Call of an external function. Input expressions have to be optimized,
+ their free variables produced. A fresh range has to be computed for
+ each output variable in vdl. Output of the function call are removed
+ from vars to be printed *)
+ let node = called_node_id m id in
+ let node_id = Corelang.node_name node in
+ let tin, tout =
+ (* special care for arrow *)
+ if node_id = "_arrow" then
+ match vdl with
+ | [ v ] ->
+ let t = v.LT.var_type in
+ [ t; t ], [ t ]
+ | _ ->
+ assert false (* should not happen *)
+ else fun_types node
+ in
+ (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
+ let vtl', vtl_ranges, il, args_new_locals =
+ List.fold_right2
+ (fun e typ_e (exprl, range_l, il_l, new_locals) ->
+ if Types.is_real_type typ_e then
+ let e', r', il, new_expr_locals =
+ optimize_expr
+ nodename
+ m
+ constEnv
+ printed_vars
+ vars_env
+ ranges
+ formalEnv
+ e
+ in
+ ( e' :: exprl,
+ r' :: range_l,
+ il @ il_l,
+ Vars.union new_locals new_expr_locals )
+ else e :: exprl, None :: range_l, il_l, new_locals)
+ vtl
+ tin
+ ([], [], [], Vars.empty)
+ in
+
+ (* if !debug then Format.eprintf "... done@ @]@ "; *)
+
+ (* let required_vars = *)
+ (* List.fold_left2 *)
+ (* (fun accu e typ_e -> *)
+ (* if Types.is_real_type typ_e then *)
+ (* Vars.union accu (get_expr_real_vars e) *)
+ (* else (\* we do not consider non real expressions *\) *)
+ (* accu *)
+ (* ) *)
+ (* Vars.empty *)
+ (* vtl' tin *)
+ (* in *)
+ (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars:
+ [%a]@ Remaining required vars: [%a]@ " *)
+ (* Vars.pp required_vars *)
+ (* Vars.pp printed_vars *)
+ (* Vars.pp (Vars.diff required_vars printed_vars) *)
+ (* ; *)
+ (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
+ (* already *)
+ (* produced *)
+ (* variables *\) *)
+ (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
+ (* let instrs', ranges' = assign_vars (Vars.union written_vars
+ printed_vars) ranges formalEnv required_vars in *)
+
+ (* instrs' @ [Corelang.update_instr_desc hd_instr
+ (MT.MStep(vdl,id,vtl'))], (* New instrs *) *)
+ let written_vars = Vars.of_list vdl in
+
+ ( il @ [ Corelang.update_instr_desc hd_instr (MT.MStep (vdl, id, vtl')) ],
+ (* New instrs *)
+ RangesInt.add_call ranges vdl id vtl_ranges,
+ (* add information bounding each vdl var *)
+ formalEnv,
+ Vars.union written_vars printed_vars,
+ (* adding vdl to new printed vars *)
+ Vars.diff vars_to_print written_vars,
+ args_new_locals )
+ | MT.MBranch (vt, branches) ->
+ (* Required variables to compute vt are introduced. Then each branch is
+ refactored specifically *)
+
+ (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr
+ hd_instr; *)
+ let required_vars = get_expr_real_vars vt in
+ let required_vars = Vars.diff required_vars printed_vars in
+ (* remove already produced variables *)
+ let vt', _, prefix_instr, prefix_new_locals =
+ optimize_expr
+ nodename
+ m
+ constEnv
+ printed_vars
+ vars_env
+ ranges
+ formalEnv
+ vt
+ in
+
+ let new_locals = prefix_new_locals in
+
+ (* let prefix_instr, ranges = *)
+ (* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv
+ required_vars in *)
+ let printed_vars = Vars.union printed_vars required_vars in
+
+ let read_vars_tl = get_read_vars tl_instrs in
+ (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
+ let branches', written_vars, merged_ranges, new_locals =
+ List.fold_right
+ (fun (b_l, b_instrs)
+ (new_branches, written_vars, merged_ranges, new_locals) ->
+ let b_write_vars = get_written_vars b_instrs in
+ let b_vars_to_print =
+ Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print)
+ in
+ let b_fe = formalEnv in
+ (* because of side effect data, we copy it for each branch *)
+ let ( b_instrs',
+ b_ranges,
+ b_formalEnv,
+ b_printed,
+ b_vars,
+ b_new_locals ) =
+ rewrite_instrs
+ nodename
+ m
+ constEnv
+ vars_env
+ m
+ b_instrs
+ ranges
+ b_fe
+ printed_vars
+ b_vars_to_print
+ in
+ (* b_vars should be empty *)
+ let _ = if b_vars != [] then assert false in
+
+ (* Producing the refactored branch *)
+ ( (b_l, b_instrs') :: new_branches,
+ Vars.union b_printed written_vars,
+ (* They should coincides. We use union instead of inter to ease
+ the bootstrap *)
+ RangesInt.merge merged_ranges b_ranges,
+ Vars.union new_locals b_new_locals ))
+ branches
+ ([], required_vars, ranges, new_locals)
+ in
+ (* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *)
+ ( prefix_instr
+ @ [
+ Corelang.update_instr_desc hd_instr (MT.MBranch (vt', branches'));
+ ],
+ merged_ranges,
+ (* Only step functions call within branches may have produced new
+ ranges. We merge this data by computing the join per variable *)
+ formalEnv,
+ (* Thanks to the computation of var_to_print in each branch, no new
+ definition should have been computed without being already
+ printed *)
+ Vars.union written_vars printed_vars,
+ Vars.diff vars_to_print written_vars
+ (* We remove vars that have been produced within branches *),
+ new_locals )
+ | MT.MReset _ | MT.MNoReset _ | MT.MSpec _ | MT.MComment _ ->
+ (* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr
+ hd_instr; *)
+
+ (* Untouched instruction *)
+ ( [ hd_instr ],
+ (* unmodified instr *)
+ ranges,
+ (* no new range computed *)
+ formalEnv,
+ (* no formelEnv update *)
+ printed_vars,
+ vars_to_print,
+ (* no more or less variables to print *)
+ Vars.empty )
+ (* no new slides vars *)
+ in
+
+ let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals
+ =
+ rewrite_instrs
+ nodename
+ m
+ constEnv
+ vars_env
+ m
+ tl_instrs
+ ranges
+ formalEnv
+ printed_vars
+ vars_to_print
+ in
+
+ ( hd_instrs @ tl_instrs,
+ ranges,
+ formalEnv,
+ printed_vars,
+ vars_to_print,
+ Vars.union hd_new_locals tl_new_locals )
+
+(* TODO: deal with new variables, ie. tmp *)
+let salsaStep constEnv m s =
+ let ranges =
+ RangesInt.empty
+ (* empty for the moment, should be build from machine annotations or
+ externally provided information *)
+ in
+ let annots =
+ List.fold_left
+ (fun accu annl ->
+ List.fold_left
+ (fun accu (key, range) ->
+ match key with
+ | [ "salsa"; "ranges"; var ] ->
+ (var, range) :: accu
+ | _ ->
+ accu)
+ accu
+ annl.LT.annots)
+ []
+ m.MT.mannot
+ in
+ let ranges =
+ List.fold_left
+ (fun ranges (v, value) ->
+ match value.LT.eexpr_qfexpr.LT.expr_desc with
+ | LT.Expr_tuple [ minv; maxv ] ->
+ let get_cst e =
+ match e.LT.expr_desc with
+ | LT.Expr_const (LT.Const_real r) ->
+ (* calculer la valeur c * 10^e *)
+ Real.to_num r
+ | _ ->
+ Format.eprintf
+ "Invalid salsa range: %a. It should be a pair of constant \
+ floats and %a is not a float.@."
+ Printers.pp_expr
+ value.LT.eexpr_qfexpr
+ Printers.pp_expr
+ e;
+ assert false
+ in
+ (* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
+ (* maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
+ (* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v
+ (Num.string_of_num minv) (Num.string_of_num maxv); *)
+ RangesInt.enlarge
+ ranges
+ v
+ (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
+ | _ ->
+ Format.eprintf
+ "Invalid salsa range: %a. It should be a pair of floats.@."
+ Printers.pp_expr
+ value.LT.eexpr_qfexpr;
+ assert false)
+ ranges
+ annots
+ in
+ let formal_env = FormalEnv.empty () in
+ let vars_to_print =
+ Vars.real_vars
+ (Vars.union (Vars.of_list m.MT.mmemory) (Vars.of_list s.MT.step_outputs))
+ in
+
+ (* TODO: should be at least step output + may be memories *)
+ let vars_env = compute_vars_env m in
+ (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; *)
+ let new_instrs, _, _, printed_vars, _, new_locals =
+ rewrite_instrs
+ m.MT.mname
+ m
+ constEnv
+ vars_env
+ m
+ s.MT.step_instrs
+ ranges
+ formal_env
+ (Vars.real_vars
+ (Vars.of_list
+ s.MT.step_inputs
+ (* printed_vars : real inputs are considered as already printed *)))
+ vars_to_print
+ in
+
+ let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
+ let unused = Vars.diff all_local_vars printed_vars in
+ let locals =
+ if not (Vars.is_empty unused) then (
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "Unused local vars: [%a]. Removing them.@ "
+ Vars.pp
+ unused);
+ List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals)
+ else s.MT.step_locals
+ in
+ let locals = locals @ Vars.elements new_locals in
+ { s with MT.step_instrs = new_instrs; MT.step_locals = locals }
+(* we have also to modify local variables to declare new vars *)
+
+let machine_t2machine_t_optimized_by_salsa constEnv mt =
+ try
+ if !debug then
+ report ~level:2 (fun fmt ->
+ Format.fprintf
+ fmt
+ "@[<v 3>Optimizing machine %s@ "
+ mt.MT.mname.LT.node_id);
+ let new_step = salsaStep constEnv mt mt.MT.mstep in
+ if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
+ { mt with MT.mstep = new_step }
+ with FormalEnv.NoDefinition v as exp ->
+ Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v;
+ raise exp
+
+(* Local Variables: *)
+(* compile-command:"make -C ../../.." *)
+(* End: *)
diff --git a/src/plugins/salsa/machine_salsa_opt.mli b/src/plugins/salsa/machine_salsa_opt.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
new file mode 100644
index 00000000..624e47ab
--- /dev/null
+++ b/src/plugins/salsa/salsaDatatypes.ml
@@ -0,0 +1,440 @@
+module LT = Lustre_types
+module MT = Machine_code_types
+module MC = Machine_code_common
+module ST = Salsa.Types
+
+let debug = ref false
+let _ = Salsa.Prelude.sliceSize := 5
+
+let pp_hash ~sep f fmt r =
+ Format.fprintf fmt "[@[<v>";
+ Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r;
+ Format.fprintf fmt "]@]"
+
+module type VALUE = sig
+ type t
+
+ val union : t -> t -> t
+ val pp : Format.formatter -> t -> unit
+ val leq : t -> t -> bool
+end
+
+module Ranges =
+functor
+ (Value : VALUE)
+ ->
+ struct
+ module Value = Value
+
+ type t = Value.t
+ type r_t = (LT.ident, Value.t) Hashtbl.t
+
+ let empty : r_t = Hashtbl.create 13
+
+ (* Look for def of node i with inputs living in vtl_ranges, reinforce ranges
+ to bound vdl: each output of node i *)
+ let add_call ranges vdl id vtl_ranges = ranges
+ (* TODO assert false. On est pas obligé de faire qqchose. On peut supposer
+ que les ranges sont donnés pour chaque noeud *)
+
+ let pp fmt r =
+ if Hashtbl.length r = 0 then Format.fprintf fmt "empty"
+ else
+ pp_hash
+ ~sep:";"
+ (fun k v fmt -> Format.fprintf fmt "%s -> %a" k Value.pp v)
+ fmt
+ r
+
+ let pp_val = Value.pp
+
+ let add_def ranges name r =
+ (* Format.eprintf "%s: declare %a@." *)
+ (* x.LT.var_id *)
+ (* Value.pp r ; *)
+ let fresh = Hashtbl.copy ranges in
+ Hashtbl.add fresh name r;
+ fresh
+
+ let enlarge ranges name r =
+ let fresh = Hashtbl.copy ranges in
+ if Hashtbl.mem fresh name then
+ Hashtbl.replace fresh name (Value.union r (Hashtbl.find fresh name))
+ else Hashtbl.add fresh name r;
+ fresh
+
+ (* Compute a join per variable *)
+ let merge ranges1 ranges2 =
+ (* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp
+ ranges2; *)
+ let ranges = Hashtbl.copy ranges1 in
+ Hashtbl.iter
+ (fun k v ->
+ if Hashtbl.mem ranges k then
+ (* Format.eprintf "%s: %a union %a = %a@." *)
+ (* k *)
+ (* Value.pp v *)
+ (* Value.pp (Hashtbl.find ranges k) *)
+ (* Value.pp (Value.union v (Hashtbl.find ranges k)); *)
+ Hashtbl.replace ranges k (Value.union v (Hashtbl.find ranges k))
+ else Hashtbl.add ranges k v)
+ ranges2;
+ (* Format.eprintf "Merge result %a@." pp ranges; *)
+ ranges
+
+ let to_abstract_env ranges =
+ Hashtbl.fold (fun id value accu -> (id, value) :: accu) ranges []
+ end
+
+module FloatIntSalsa = struct
+ type t = ST.abstractValue
+
+ let pp fmt ((f, r) : t) =
+ let fs, rs = Salsa.Float.Domain.print (f, r) in
+ Format.fprintf fmt "%s + %s" fs rs
+
+ (* match f, r with | ST.I(a,b), ST.J(c,d) -> Format.fprintf fmt "[%f, %f] +
+ [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d) | ST.I(a,b),
+ ST.JInfty -> Format.fprintf fmt "[%f, %f] + oo" a b | ST.Empty, _ ->
+ Format.fprintf fmt "???"
+
+ | _ -> assert false *)
+ let union v1 v2 = Salsa.Float.Domain.join v1 v2
+
+ (* match v1, v2 with |(ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1',
+ y2')) -> ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2')) | _ ->
+ Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false *)
+ let inject cst =
+ match cst with
+ | LT.Const_int i ->
+ Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
+ | LT.Const_real r ->
+ (* TODO: this is incorrect. We should rather compute the error associated
+ to the float *)
+ (* let f = float_of_string s in *)
+ let n = Real.to_q r in
+ Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n)
+ (* let r = Salsa.Prelude.r_of_f_aux r in *)
+ (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
+
+ (* let r = float_of_string s in *)
+ (* if r = 0. then *)
+ (* Salsa.Builder.mk_cst (ST.R(-. min_float, min_float),Float.ulp (ST.R(-.
+ min_float, min_float))) *)
+ (* else *)
+ (* Salsa.Builder.mk_cst
+ (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp
+ (ST.I(r,r))) *)
+ | _ ->
+ assert false
+
+ let leq =
+ (* Salsa.Float.feSseq *)
+ Salsa.Float.Domain.leq
+end
+
+module RangesInt = Ranges (FloatIntSalsa)
+
+module Vars = struct
+ module VarSet = Set.Make (struct
+ type t = LT.var_decl
+
+ let compare x y = compare x.LT.var_id y.LT.var_id
+ end)
+
+ let real_vars vs =
+ VarSet.filter (fun v -> Types.is_real_type v.LT.var_type) vs
+
+ let of_list = List.fold_left (fun s e -> VarSet.add e s) VarSet.empty
+
+ include VarSet
+
+ let remove_list (set : t) (v_list : elt list) : t =
+ List.fold_right VarSet.remove v_list set
+
+ let pp fmt vs =
+ Utils.fprintf_list ~sep:", " Printers.pp_var fmt (VarSet.elements vs)
+end
+
+(*************************************************************************************)
+(* Converting values back and forth *)
+(*************************************************************************************)
+
+let rec value_t2salsa_expr constEnv vt =
+ let value_t2salsa_expr = value_t2salsa_expr constEnv in
+ let res =
+ match vt.MT.value_desc with
+ (* | LT.Cst(LT.Const_tag(t) as c) -> *)
+ (* Format.eprintf "v2s: cst tag@."; *)
+ (* if List.mem_assoc t constEnv then ( *)
+ (* Format.eprintf "trouvé la constante %s: %a@ " t Printers.pp_const c; *)
+ (* FloatIntSalsa.inject (List.assoc t constEnv) *)
+ (* ) *)
+ (* else ( *)
+ (* Format.eprintf "Const tag %s unhandled@.@?" t ; *)
+ (* 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.Var v ->
+ (* Format.eprintf "v2s: var %s@." v.LT.var_id; *)
+ let sel_fun (vname, _) = v.LT.var_id = vname in
+ if List.exists sel_fun constEnv then
+ let _, cst = List.find sel_fun constEnv in
+ FloatIntSalsa.inject cst
+ else
+ let id = v.LT.var_id in
+ Salsa.Builder.mk_id id
+ | MT.Fun (binop, [ x; y ]) ->
+ let salsaX = value_t2salsa_expr x in
+ let salsaY = value_t2salsa_expr y in
+ let op =
+ let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in
+ match binop with
+ | "+" ->
+ Salsa.Builder.mk_plus
+ | "-" ->
+ Salsa.Builder.mk_minus
+ | "*" ->
+ Salsa.Builder.mk_times
+ | "/" ->
+ Salsa.Builder.mk_div
+ | "=" ->
+ pred Salsa.Builder.mk_eq
+ | "<" ->
+ pred Salsa.Builder.mk_lt
+ | ">" ->
+ pred Salsa.Builder.mk_gt
+ | "<=" ->
+ pred Salsa.Builder.mk_lte
+ | ">=" ->
+ pred Salsa.Builder.mk_gte
+ | _ ->
+ assert false
+ in
+ op salsaX salsaY
+ | MT.Fun (unop, [ x ]) ->
+ let salsaX = value_t2salsa_expr x in
+ Salsa.Builder.mk_uminus salsaX
+ | MT.Fun (f, _) ->
+ raise
+ (Salsa.Prelude.Error
+ ("Unhandled function " ^ f ^ " in conversion to salsa expression"))
+ | MT.Array _ | MT.Access _ | MT.Power _ ->
+ raise
+ (Salsa.Prelude.Error
+ "Unhandled construct in conversion to salsa expression")
+ in
+ (* if debug then *)
+ (* Format.eprintf "value_t2salsa_expr: %a -> %a@ " *)
+ (* MC.pp_val vt *)
+ (* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
+ res
+
+type var_decl = { vdecl : LT.var_decl; is_local : bool }
+
+module VarEnv = Map.Make (struct
+ type t = LT.ident
+
+ let compare = compare
+end)
+
+(* let is_local_var vars_env v = *)
+(* try *)
+(* (VarEnv.find v vars_env).is_local *)
+(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert
+ false *)
+
+let get_var vars_env v =
+ try VarEnv.find v vars_env
+ with Not_found ->
+ Format.eprintf
+ "Impossible to find var %s in var env %a@ "
+ v
+ (Utils.fprintf_list ~sep:", " (fun fmt (id, _) ->
+ Format.pp_print_string fmt id))
+ (VarEnv.bindings vars_env);
+ assert false
+
+let compute_vars_env m =
+ let env = VarEnv.empty in
+ let env =
+ List.fold_left
+ (fun accu v ->
+ VarEnv.add v.LT.var_id { vdecl = v; is_local = false } accu)
+ env
+ m.MT.mmemory
+ in
+ let env =
+ List.fold_left
+ (fun accu v -> VarEnv.add v.LT.var_id { vdecl = v; is_local = true } accu)
+ env
+ MC.(
+ m.MT.mstep.MT.step_inputs @ m.MT.mstep.MT.step_outputs
+ @ m.MT.mstep.MT.step_locals)
+ in
+ env
+
+let rec salsa_expr2value_t vars_env cst_env e =
+ (* let e = Float.evalPartExpr e [] [] in *)
+ let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in
+ let binop op e1 e2 t =
+ let x = salsa_expr2value_t e1 in
+ let y = salsa_expr2value_t e2 in
+ MC.mk_val (MT.Fun (op, [ x; y ])) t
+ in
+ match e with
+ | ST.Cst (abs_val, _) ->
+ (* We project ranges into constants. We forget about errors and provide the
+ mean/middle value of the interval *)
+ let new_float = Salsa.Float.Domain.to_float abs_val in
+ (* let new_float = Salsa.NumMartel.float_of_num c in *)
+ (* let new_float = *)
+ (* if f1 = f2 then *)
+ (* f1 *)
+ (* else *)
+ (* (f1 +. f2) /. 2.0 *)
+ (* in *)
+ (* Log.report ~level:3 *)
+ (* (fun fmt -> Format.fprintf fmt "projecting [%.45f, %.45f] -> %.45f@ " f1
+ f2 new_float); *)
+ let cst =
+ let s =
+ if new_float = 0. then "0."
+ else
+ (* We have to convert it into our format: int * int * real *)
+ (* string_of_float new_float *)
+ let _ = Format.flush_str_formatter () in
+ Format.fprintf Format.str_formatter "%.11f" new_float;
+ Format.flush_str_formatter ()
+ in
+ Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s)
+ in
+ MC.mk_val (MT.Cst cst) Type_predef.type_real
+ | ST.Id (id, _) ->
+ (* Format.eprintf "Looking for id=%s@.@?" id; *)
+ if List.mem_assoc id cst_env then
+ let cst = List.assoc id cst_env in
+ (* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *)
+ MC.mk_val (MT.Cst cst) Type_predef.type_real
+ else
+ (* if is_const salsa_label then *)
+ (* 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
+ 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
+ | ST.Div (x, y, _) ->
+ binop "/" x y Type_predef.type_real
+ | ST.Uminus (x, _) ->
+ let x = salsa_expr2value_t x in
+ MC.mk_val (MT.Fun ("uminus", [ x ])) Type_predef.type_real
+ | ST.IntOfBool (ST.Eq (x, y, _), _) ->
+ binop "=" x y Type_predef.type_bool
+ | ST.IntOfBool (ST.Lt (x, y, _), _) ->
+ binop "<" x y Type_predef.type_bool
+ | ST.IntOfBool (ST.Gt (x, y, _), _) ->
+ binop ">" x y Type_predef.type_bool
+ | ST.IntOfBool (ST.Lte (x, y, _), _) ->
+ binop "<=" x y Type_predef.type_bool
+ | ST.IntOfBool (ST.Gte (x, y, _), _) ->
+ binop ">=" x y Type_predef.type_bool
+ | _ ->
+ raise
+ (Salsa.Prelude.Error
+ "Entschuldigung, salsaExpr2value_t case not yet implemented")
+
+let rec get_salsa_free_vars vars_env constEnv absenv e =
+ let f = get_salsa_free_vars vars_env constEnv absenv in
+ match e with
+ | ST.Id (id, _) ->
+ if (not (List.mem_assoc id absenv)) && not (List.mem_assoc id constEnv) then
+ Vars.singleton
+ (try VarEnv.find id vars_env with Not_found -> assert false).vdecl
+ else Vars.empty
+ | ST.Plus (x, y, _)
+ | ST.Minus (x, y, _)
+ | ST.Times (x, y, _)
+ | ST.Div (x, y, _)
+ | ST.IntOfBool (ST.Eq (x, y, _), _)
+ | ST.IntOfBool (ST.Lt (x, y, _), _)
+ | ST.IntOfBool (ST.Gt (x, y, _), _)
+ | ST.IntOfBool (ST.Lte (x, y, _), _)
+ | ST.IntOfBool (ST.Gte (x, y, _), _) ->
+ Vars.union (f x) (f y)
+ | ST.Uminus (x, _) ->
+ f x
+ | ST.Cst _ ->
+ Vars.empty
+ | _ ->
+ assert false
+
+module FormalEnv = struct
+ type fe_t = (LT.ident, int * MT.value_t) Hashtbl.t
+
+ let cpt = ref 0
+
+ exception NoDefinition of LT.var_decl
+
+ (* Returns the expression associated to v in env *)
+ let get_def (env : fe_t) v =
+ try snd (Hashtbl.find env v.LT.var_id)
+ with Not_found -> raise (NoDefinition v)
+
+ let fold f = Hashtbl.fold (fun k (_, v) accu -> f k v accu)
+
+ let to_salsa constEnv formalEnv =
+ fold
+ (fun id expr accu -> (id, value_t2salsa_expr constEnv expr) :: accu)
+ formalEnv
+ []
+
+ let def constEnv vars_env (env : fe_t) d expr =
+ incr cpt;
+ let fresh = Hashtbl.copy env in
+ let expr_salsa = value_t2salsa_expr constEnv expr in
+ let salsa_env = to_salsa constEnv env in
+ let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in
+ let expr_salsa =
+ Salsa.Analyzer.evalPartExpr
+ expr_salsa
+ salsa_env
+ []
+ (* no blacklisted vars *)
+ []
+ (*no arrays *)
+ in
+ let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
+ Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec);
+ fresh
+
+ let empty () : fe_t = Hashtbl.create 13
+
+ 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 =
+ let order = Hashtbl.fold (fun k (cpt, _) accu -> (k, cpt) :: accu) env [] in
+ fun v1 v2 ->
+ if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order
+ then
+ if List.assoc v1.LT.var_id order <= List.assoc v2.LT.var_id order then
+ -1
+ else 1
+ else assert false
+end
+
+(* Local Variables: *)
+(* compile-command:"make -C ../../.." *)
+(* End: *)
diff --git a/src/plugins/salsa/salsaDatatypes.mli b/src/plugins/salsa/salsaDatatypes.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
new file mode 100644
index 00000000..92e24712
--- /dev/null
+++ b/src/plugins/salsa/salsa_plugin.ml
@@ -0,0 +1,60 @@
+open Format
+open Lustre_types
+
+let salsa_enabled = ref false
+
+(* "-salsa", Arg.Set salsa_enabled, "activate Salsa optimization <default>"; *)
+(* "-no-salsa", Arg.Clear salsa_enabled, "deactivate Salsa optimization"; *)
+
+module Plugin : PluginType.S = struct
+ include PluginType.Default
+
+ let name = "salsa"
+
+ let options =
+ [
+ "-debug", Arg.Set SalsaDatatypes.debug, "debug salsa plugin";
+ ( "-verbose",
+ Arg.Set_int Salsa.Log.verbose_level,
+ "salsa plugin verbose level (default is 0)" );
+ ( "-slice-depth",
+ Arg.Set_int Salsa.Prelude.sliceSize,
+ "salsa slice depth (default is 5)" );
+ "-disable", Arg.Clear salsa_enabled, "disable salsa";
+ ]
+
+ let activate () = salsa_enabled := true
+
+ let init () =
+ if !salsa_enabled then if !SalsaDatatypes.debug then Salsa.Log.debug := true
+
+ let refine_machine_code prog machine_code =
+ if !salsa_enabled then (
+ Compiler_common.check_main ();
+ Log.report ~level:1 (fun fmt ->
+ fprintf fmt ".. @[<v 0>salsa machines optimization@ ");
+ (* Selecting float constants for Salsa *)
+ let constEnv =
+ List.fold_left
+ (fun accu c_topdecl ->
+ match c_topdecl.top_decl_desc with
+ | Const c when Types.is_real_type c.const_type ->
+ (c.const_id, c.const_value) :: accu
+ | _ ->
+ accu)
+ []
+ (Corelang.get_consts prog)
+ in
+ let res =
+ List.map
+ (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
+ machine_code
+ in
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
+ res)
+ else machine_code
+end
+
+let () =
+ PluginList.registered :=
+ (module Plugin : PluginType.S) :: !PluginList.registered
diff --git a/src/plugins/salsa/salsa_plugin.mli b/src/plugins/salsa/salsa_plugin.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
new file mode 100644
index 00000000..3c8785a6
--- /dev/null
+++ b/src/plugins/scopes/scopes.ml
@@ -0,0 +1,468 @@
+open Utils
+open Lustre_types
+open Corelang
+open Machine_code_types
+open Machine_code_common
+
+(* (variable, node name, node instance) *)
+type scope_t = (var_decl * string * string option) list * var_decl
+
+(* Scope to string list *)
+let scope_to_sl ((sl, v) : scope_t) : string list =
+ List.fold_right
+ (fun (v, nodename, _) accu -> v.var_id :: nodename :: accu)
+ sl
+ [ v.var_id ]
+
+let rec compute_scopes ?(first = true) prog root_node : scope_t list =
+ let compute_scopes = compute_scopes ~first:false in
+ (* Format.eprintf "Compute scope of %s@." main_node; *)
+ try
+ let node = get_node root_node prog in
+ let locals = List.map fst node.node_locals in
+ let all_vars = node.node_inputs @ locals @ node.node_outputs in
+ let local_vars = if first then locals else node.node_inputs @ locals in
+ let local_scopes = List.map (fun x -> [], x) local_vars in
+ let sub_scopes =
+ let sub_nodes =
+ List.fold_left
+ (fun res s ->
+ match s with
+ | Eq
+ ({ eq_rhs = { expr_desc = Expr_appl (nodeid, _, _); _ }; _ } as
+ eq) -> (
+ (* Obtaining the var_del associated to the first var of eq_lhs *)
+ try
+ let query v = v.var_id = List.hd eq.eq_lhs in
+ let vid = List.find query all_vars in
+ (nodeid, vid) :: res
+ with Not_found ->
+ Format.eprintf
+ "eq=%a@.local_vars=%a@."
+ Printers.pp_node_eq
+ eq
+ (Format.pp_comma_list Printers.pp_var)
+ local_vars;
+ assert false)
+ | Eq _ ->
+ res
+ | _ ->
+ assert false
+ (* TODO deal with Automaton *))
+ []
+ node.node_stmts
+ in
+ List.map
+ (fun (nodeid, vid) ->
+ let scopes = compute_scopes prog nodeid in
+ List.map (fun (sl, v) -> (vid, nodeid, None) :: sl, v) scopes
+ (* instances are not yet known, hence the None *))
+ sub_nodes
+ in
+ local_scopes @ List.flatten sub_scopes
+ with Not_found -> []
+
+let pp_scopes =
+ Format.(
+ pp_print_list (fun fmt ((_, v) as s) ->
+ fprintf
+ fmt
+ "%a: %a"
+ (pp_print_list
+ ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
+ pp_print_string)
+ (scope_to_sl s)
+ Types.pp
+ v.var_type))
+
+(* let pp_path fmt p = *)
+(* Utils.fprintf_list ~sep:"." (fun fmt (id, _) -> Format.pp_print_string fmt
+ id) fmt p *)
+
+let get_node_vdecl_of_name name node =
+ try
+ List.find
+ (fun v -> v.var_id = name)
+ (node.node_inputs @ node.node_outputs @ List.map fst node.node_locals)
+ with Not_found ->
+ Format.eprintf "Cannot find variable %s in node %s@." name node.node_id;
+ assert false
+
+let rec get_path prog machines node id_list accu =
+ let get_path = get_path prog machines in
+ match id_list, accu with
+ | [ flow ], [] ->
+ (* Special treatment of first level flow: node is here main_node *)
+ let flow_var = get_node_vdecl_of_name flow node in
+ [], flow_var, node.node_id
+ | [ id ], (_, last_node, _) :: _ ->
+ (* last item, it should denote a local memory variable (local var, memory or
+ input *)
+ let id_vdecl = get_node_vdecl_of_name id (get_node last_node prog) in
+ List.rev accu, id_vdecl, last_node
+ | varid :: nodename :: id_list_tl, _ -> (
+ let e_machine = get_machine machines node.node_id in
+ (* Format.eprintf "Looking for def %s in call %s in machine %a@." *)
+ (* varid nodename *)
+ (* Machine_code.pp_machine e_machine; *)
+ let find_var v = v.var_id = varid in
+ let instance =
+ List.find
+ (fun i ->
+ match get_instr_desc i with
+ | MStep (p, _, _) ->
+ List.exists find_var p
+ | _ ->
+ false)
+ e_machine.mstep.step_instrs
+ in
+ try
+ let variable, instance_node, instance_id =
+ match get_instr_desc instance with
+ | MStep (p, o, _) ->
+ (* Format.eprintf "Looking for machine %s@.@?" o; *)
+ let o_fun, _ = List.assoc o e_machine.mcalls in
+ if node_name o_fun = nodename then List.hd p, o_fun, o
+ else assert false
+ | _ ->
+ assert false
+ in
+ let next_node = node_of_top instance_node in
+ let accu = (variable, nodename, Some instance_id) :: accu in
+ (* Format.eprintf "Calling get path on %s@.@?" next_node.node_id; *)
+ get_path next_node id_list_tl accu
+ with Not_found ->
+ Format.eprintf "toto@.";
+ assert false)
+ | _ ->
+ assert false
+
+let check_scope all_scopes =
+ let all_scopes_as_sl = List.map scope_to_sl all_scopes in
+ fun prog machines main_node_name sl ->
+ if not (List.mem sl all_scopes_as_sl) then (
+ Format.eprintf "%s is an invalid scope.@." (String.concat "." sl);
+ exit 1)
+ else
+ (* Format.eprintf "@.@.Required path: %s@." (String.concat "." sl) ; *)
+ let main_node = get_node main_node_name prog in
+ let path, flow, mid = get_path prog machines main_node sl [] in
+ (* Format.eprintf "computed path: %a.%s@." pp_path path flow.var_id; *)
+ path, flow, mid
+
+(* Build the two maps - (scope_name, variable) - (machine_name, list of selected
+ variables) *)
+let check_scopes main_node_name prog machines all_scopes scopes =
+ let check_scope = check_scope all_scopes prog machines in
+ List.fold_left
+ (fun (accu_sl, accu_m) sl ->
+ let path, flow, mid = check_scope main_node_name sl in
+ let accu_sl = (sl, (path, flow)) :: accu_sl in
+ let accu_m =
+ let flow_id = flow.var_id in
+ if List.mem_assoc mid accu_m then
+ (mid, flow_id :: List.assoc mid accu_m)
+ :: List.remove_assoc mid accu_m
+ else (mid, [ flow_id ]) :: accu_m
+ in
+ accu_sl, accu_m)
+ ([], [])
+ scopes
+
+let scope_var_name vid = vid ^ "__scope"
+
+(**********************************************************************)
+(* The following three functions are used in the main function to print the
+ value of the new memories, storing scopes values *)
+(**********************************************************************)
+
+(* TODO: recuperer le type de "flow" et appeler le print correspondant iterer
+ sur path pour construire la suite des xx_mem._reg.yy_mem._reg......flow par
+ ex main_mem->n8->n9->_reg.flow *)
+let extract_scopes_defs scopes =
+ let rec scope_path_name (path, flow) accu =
+ match path with
+ | [] ->
+ accu ^ "_reg." ^ scope_var_name flow.var_id, flow
+ | (_, _, Some instance_id) :: tl ->
+ scope_path_name (tl, flow) (accu ^ instance_id ^ "->")
+ | _ ->
+ assert false
+ in
+ List.map
+ (fun (sl, scope) -> String.concat "." sl, scope_path_name scope "main_mem.")
+ scopes
+
+let pp_scopes_files _basename _mname fmt scopes =
+ let scopes_vars = extract_scopes_defs scopes in
+ List.iteri
+ (fun idx _ (*(id, (var_path, var))*) ->
+ C_backend_common.pp_file_decl fmt "out_scopes" idx)
+ scopes_vars;
+ Format.fprintf fmt "@[<v 2>if (traces) {@ ";
+ List.iteri
+ (fun idx (id, (_, var)) ->
+ let file = C_backend_common.pp_file_open fmt "out_scopes" idx in
+ Format.fprintf fmt "fprintf(%s, \"# scope: %s\\n\");@ " file id;
+ Format.fprintf
+ fmt
+ "fprintf(%s, \"# node: %s\\n\");@ "
+ file
+ (Utils.desome var.var_parent_nodeid);
+ Format.fprintf fmt "fprintf(%s, \"# variable: %s\\n\");@ " file var.var_id)
+ scopes_vars;
+ Format.fprintf fmt "@]}@ "
+
+let pp_full_scopes fmt scopes =
+ let scopes_vars = extract_scopes_defs scopes in
+ List.iteri
+ (fun idx (id, (var_path, var)) ->
+ Format.fprintf fmt "@ %t;" (fun fmt ->
+ C_backend_common.pp_put_var
+ fmt
+ ("_scopes" ^ string_of_int (idx + 1))
+ id
+ (*var*) var.var_type
+ var_path))
+ scopes_vars
+
+(**********************************************************************)
+
+let update_machine main_node machine scopes =
+ let stateassign (vdecl_mem, vdecl_orig) =
+ mkinstr
+ (MStateAssign (vdecl_mem, mk_val (Var vdecl_orig) vdecl_orig.var_type))
+ in
+ let selection =
+ (* We only register inputs for non root node *)
+ (if machine.mname.node_id = main_node then []
+ else machine.mstep.step_inputs)
+ (* @ machine.mstep.step_outputs *)
+ @ List.map fst machine.mmemory
+ @ machine.mstep.step_locals
+ in
+ let selection =
+ List.filter
+ (fun v -> List.exists (fun vid -> vid = v.var_id) scopes)
+ selection
+ in
+ let new_mems =
+ List.map
+ (fun v ->
+ (* We could copy the variable but then we need to update its type let
+ new_v = copy_var_decl v in *)
+ let new_v = { v with var_id = scope_var_name v.var_id } in
+ new_v, v)
+ selection
+ in
+ {
+ machine with
+ mmemory = machine.mmemory @ List.map (fun (v, _) -> v, None) new_mems;
+ mstep =
+ {
+ machine.mstep with
+ step_instrs =
+ machine.mstep.step_instrs
+ @ mkinstr (MComment "Registering all flows")
+ :: List.map stateassign new_mems;
+ };
+ }
+
+let rec is_valid_path path nodename prog machines =
+ let nodescopes = compute_scopes prog nodename in
+ let m = get_machine machines nodename in
+ match path with
+ | [] ->
+ assert false
+ | [ vid ] ->
+ let res =
+ List.exists
+ (fun v -> v.var_id = vid)
+ (List.map fst m.mmemory @ m.mstep.step_inputs @ m.mstep.step_locals)
+ in
+ (* if not res then *)
+ (* Format.eprintf "Variable %s cannot be found in machine %s@.Local vars are
+ %a@." vid m.mname.node_id *)
+ (* (Utils.fprintf_list ~sep:", " Printers.pp_var) (m.mmemory @
+ m.mstep.step_inputs @ m.mstep.step_locals) *)
+ (* ; *)
+ res
+ | _ :: nodename :: path' ->
+ (* We use the scopes computed on the prog artifact *)
+ (* Format.eprintf "Path is %a@ Local scopes: @[<v>%a@ @]@." *)
+ (* (Utils.fprintf_list ~sep:"." Format.pp_print_string) path *)
+ (* (Utils.fprintf_list ~sep:";@ " *)
+ (* (fun fmt scope -> *)
+ (* Utils.fprintf_list ~sep:"." Format.pp_print_string fmt (scope_to_sl scope)) *)
+ (* ) *)
+ (* nodescopes; *)
+ if List.mem path (List.map scope_to_sl nodescopes) then
+ (* Format.eprintf "Valid local path, checking underneath@."; *)
+ is_valid_path path' nodename prog machines
+ else false
+
+(* let instok = List.exists (fun (inst', node) -> inst' = inst) m.minstances
+ in *)
+(* if not instok then Format.eprintf "inst = %s@." inst; *)
+(* instok && *)
+(* let instnode = fst (snd (List.find (fun (inst', node) -> inst' = inst)
+ m.minstances)) in *)
+(* is_valid_path path' (Corelang.node_of_top instnode).node_id prog machines *)
+
+(****************************************************)
+
+let scopes_def : string list list ref = ref []
+let inputs = ref []
+let option_show_scopes = ref false
+let option_scopes = ref false
+let option_all_scopes = ref false
+(* let option_mems_scopes = ref false
+ * let option_input_scopes = ref false *)
+
+let scopes_map : (ident list * scope_t) list ref = ref []
+
+let process_scopes main_node prog machines =
+ let all_scopes = compute_scopes prog !Options.main_node in
+ let selected_scopes =
+ if !option_all_scopes then List.map (fun s -> scope_to_sl s) all_scopes
+ else !scopes_def
+ in
+ (* Making sure all scopes are defined and were not removed by various
+ optmizationq *)
+ let selected_scopes =
+ List.filter
+ (fun sl ->
+ let res = is_valid_path sl main_node prog machines in
+ (if not res then
+ Format.(
+ eprintf
+ "Scope %a is cancelled due to variable removal@."
+ (pp_print_list
+ ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
+ pp_print_string)
+ sl));
+ res)
+ selected_scopes
+ in
+ let scopes_map', machines_scopes =
+ check_scopes main_node prog machines all_scopes selected_scopes
+ in
+ scopes_map := scopes_map';
+ (* Each machine is updated with fresh memories and declared as stateful *)
+ let machines =
+ List.map
+ (fun m ->
+ let mid = m.mname.node_id in
+ if List.mem_assoc mid machines_scopes then
+ let machine_scopes = List.assoc mid machines_scopes in
+ update_machine main_node m machine_scopes
+ else m)
+ machines
+ in
+ machines
+
+let activate () =
+ option_scopes := true;
+ Options.optimization := 0;
+ (* no optimization *)
+ ()
+
+let register_scopes s =
+ activate ();
+ option_all_scopes := false;
+ let scope_list = Str.split (Str.regexp ", *") s in
+ let scope_list =
+ List.map (fun scope -> Str.split (Str.regexp "\\.") scope) scope_list
+ in
+ scopes_def := List.rev scope_list
+
+let register_inputs s =
+ activate ();
+ let input_list = Str.split (Str.regexp "[;]") s in
+ let input_list =
+ List.map
+ (fun s ->
+ match Str.split (Str.regexp "=") s with
+ | [ v; e ] ->
+ v, e
+ | _ ->
+ raise (Invalid_argument ("Input list error: " ^ s)))
+ input_list
+ in
+ let input_list =
+ List.map (fun (v, e) -> v, Str.split (Str.regexp "[;]") e) input_list
+ in
+ inputs := input_list
+
+let register_all_scopes () =
+ activate ();
+ option_all_scopes := true
+
+module Plugin : sig
+ include PluginType.S
+
+ val show_scopes : unit -> bool
+end = struct
+ include PluginType.Default
+
+ let name = "scopes"
+ let is_active () = !option_scopes || !option_show_scopes || !option_all_scopes
+ (* || !option_mem_scopes || !option_input_scopes *)
+
+ let show_scopes () =
+ !option_show_scopes
+ &&
+ (Compiler_common.check_main ();
+ true)
+
+ let usage fmt =
+ let open Format in
+ fprintf
+ fmt
+ "@[<hov 0>Scopes@ enrich@ the@ internal@ memories@ to@ record@ all@ or@ \
+ a@ selection@ of@ internals.@ In@ conjunction@ with@ the@ trace@ \
+ option@ of@ the@ produced@ binary@ it@ can@ also@ record@ these@ flow@ \
+ values@ within@ separated@ log@ files.@]@ @ ";
+ fprintf fmt "Options are:@ "
+
+ let options =
+ [
+ "-select", Arg.String register_scopes, "specifies which variables to log";
+ "-input", Arg.String register_inputs, "specifies the simulation input";
+ ( "-show-possible-scopes",
+ Arg.Set option_show_scopes,
+ "list possible variables to log" );
+ ( "-select-all",
+ Arg.Unit register_all_scopes,
+ "select all possible variables to log" )
+ (* "-select-mems", Arg.Set option_mems_scopes, "select all memory variables to log";
+ * "-select-inputs", Arg.Set option_input_scopes, "select all input variables to log"; *);
+ ]
+
+ let activate = activate
+ let check_force_stateful () = is_active ()
+
+ let refine_machine_code prog machine_code =
+ if show_scopes () then (
+ let all_scopes = compute_scopes prog !Options.main_node in
+ (* Printing scopes *)
+ if !Options.verbose_level >= 1 then Format.printf "Possible scopes are:@ ";
+ Format.printf "@[<v 0>%a@ @]@.@?" pp_scopes all_scopes;
+ exit 0);
+ if is_active () then process_scopes !Options.main_node prog machine_code
+ else machine_code
+
+ let c_backend_main_loop_body_suffix fmt () =
+ if is_active () then Format.fprintf fmt "@ %a" pp_full_scopes !scopes_map
+
+ let c_backend_main_loop_body_prefix basename mname fmt () =
+ if is_active () then
+ Format.fprintf fmt "@ %a" (pp_scopes_files basename mname) !scopes_map
+end
+
+let () =
+ PluginList.registered :=
+ (module Plugin : PluginType.S) :: !PluginList.registered
+(* Local Variables: *)
+(* compile-command:"make -C ../.." *)
+(* End: *)
diff --git a/src/plugins/scopes/scopes.mli b/src/plugins/scopes/scopes.mli
new file mode 100644
index 00000000..b6281510
--- /dev/null
+++ b/src/plugins/scopes/scopes.mli
@@ -0,0 +1,14 @@
+open Utils
+open Lustre_types
+
+module Plugin : sig
+ include PluginType.S
+
+ val show_scopes : unit -> bool
+end
+
+(* (variable, node name, node instance) *)
+type scope_t = (var_decl * string * string option) list * var_decl
+
+val compute_scopes : ?first:bool -> program_t -> ident -> scope_t list
+val pp_scopes : Format.formatter -> scope_t list -> unit
--
GitLab