Skip to content
Snippets Groups Projects
Commit 6bb00bf6 authored by BRUN Lelio's avatar BRUN Lelio
Browse files

cope with newer Dune version

parent 0750d5a1
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 2049 deletions
src/plugins/mpfr/lustrec_mpfr.ml → src/lustrec_mpfr.ml
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/mpfr/lustrec_mpfr.mli → src/lustrec_mpfr.mli
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/pluginList.ml → src/pluginList.ml
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/pluginList.mli → src/pluginList.mli
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/pluginType.ml → src/pluginType.ml
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/pluginType.mli → src/pluginType.mli
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/plugins.ml → src/plugins.ml
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/plugins.mli → src/plugins.mli
+ 0
− 0
View file @ 6bb00bf6
File moved
src/plugins/salsa/machine_salsa_opt.ml deleted 100644 → 0
+ 0
− 1067
View file @ 0750d5a1
This diff is collapsed.
src/plugins/salsa/machine_salsa_opt.mli deleted 100644 → 0
+ 0
− 0
View file @ 0750d5a1
src/plugins/salsa/salsaDatatypes.ml deleted 100644 → 0
+ 0
− 440
View file @ 0750d5a1
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: *)
src/plugins/salsa/salsaDatatypes.mli deleted 100644 → 0
+ 0
− 0
View file @ 0750d5a1
src/plugins/salsa/salsa_plugin.ml deleted 100644 → 0
+ 0
− 60
View file @ 0750d5a1
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
src/plugins/salsa/salsa_plugin.mli deleted 100644 → 0
+ 0
− 0
View file @ 0750d5a1
src/plugins/scopes/scopes.ml deleted 100644 → 0
+ 0
− 468
View file @ 0750d5a1
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: *)
src/plugins/scopes/scopes.mli deleted 100644 → 0
+ 0
− 14
View file @ 0750d5a1
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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment