diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/lustrec_mpfr.ml
similarity index 100%
rename from src/plugins/mpfr/lustrec_mpfr.ml
rename to src/lustrec_mpfr.ml
diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/lustrec_mpfr.mli
similarity index 100%
rename from src/plugins/mpfr/lustrec_mpfr.mli
rename to src/lustrec_mpfr.mli
diff --git a/src/plugins/pluginList.ml b/src/pluginList.ml
similarity index 100%
rename from src/plugins/pluginList.ml
rename to src/pluginList.ml
diff --git a/src/plugins/pluginList.mli b/src/pluginList.mli
similarity index 100%
rename from src/plugins/pluginList.mli
rename to src/pluginList.mli
diff --git a/src/plugins/pluginType.ml b/src/pluginType.ml
similarity index 100%
rename from src/plugins/pluginType.ml
rename to src/pluginType.ml
diff --git a/src/plugins/pluginType.mli b/src/pluginType.mli
similarity index 100%
rename from src/plugins/pluginType.mli
rename to src/pluginType.mli
diff --git a/src/plugins/plugins.ml b/src/plugins.ml
similarity index 100%
rename from src/plugins/plugins.ml
rename to src/plugins.ml
diff --git a/src/plugins/plugins.mli b/src/plugins.mli
similarity index 100%
rename from src/plugins/plugins.mli
rename to src/plugins.mli
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
deleted file mode 100644
index 1ebd7bfef8d389512b9c8f9651e406b6ef52d30d..0000000000000000000000000000000000000000
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ /dev/null
@@ -1,1067 +0,0 @@
-(* 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
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
deleted file mode 100644
index 624e47ab5b95991f5b481138050e7233dda08c2f..0000000000000000000000000000000000000000
--- a/src/plugins/salsa/salsaDatatypes.ml
+++ /dev/null
@@ -1,440 +0,0 @@
-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
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
deleted file mode 100644
index 92e247120d317956fe9b79d0c20c5cb1506ab7b9..0000000000000000000000000000000000000000
--- a/src/plugins/salsa/salsa_plugin.ml
+++ /dev/null
@@ -1,60 +0,0 @@
-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
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
deleted file mode 100644
index 3c8785a65e7c15723fd858af1a5fc26628842327..0000000000000000000000000000000000000000
--- a/src/plugins/scopes/scopes.ml
+++ /dev/null
@@ -1,468 +0,0 @@
-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
deleted file mode 100644
index b62815109922224074405290ff68406c9c484e2c..0000000000000000000000000000000000000000
--- a/src/plugins/scopes/scopes.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-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