Skip to content
Snippets Groups Projects
Commit 7db425aa authored by Temesghen Kahsai's avatar Temesghen Kahsai
Browse files

adding missing stuff

parent fc476249
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/global.ml 0 → 100644
+ 21
− 0
View file @ 7db425aa
let type_env : (Types.type_expr Env.t) ref = ref Env.initial
let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
let basename = ref ""
let main_node = ref ""
module TypeEnv =
struct
let lookup_value ident = Env.lookup_value !type_env ident
let exists_value ident = Env.exists_value !type_env ident
let iter f = Env.iter !type_env f
let pp pp_fun fmt () = Env.pp_env pp_fun fmt !type_env
end
let initialize () =
begin
main_node := !Options.main_node;
end
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
src/mpfr.ml 0 → 100755
+ 265
− 0
View file @ 7db425aa
(********************************************************************)
(* *)
(* The LustreC compiler toolset / The LustreC Development Team *)
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
(* *)
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
(* under the terms of the GNU Lesser General Public License *)
(* version 2.1. *)
(* *)
(********************************************************************)
open Utils
open LustreSpec
open Corelang
open Normalization
open Machine_code
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
let mpfr_rnd () = "MPFR_RNDN"
let mpfr_prec () = !Options.mpfr_prec
let inject_id = "MPFRId"
let inject_copy_id = "mpfr_set"
let inject_real_id = "mpfr_set_flt"
let inject_init_id = "mpfr_init2"
let inject_clear_id = "mpfr_clear"
let mpfr_t = "mpfr_t"
let unfoldable_value value =
not (Types.is_real_type value.value_type && is_const_value value)
let inject_id_id expr =
let e = mkpredef_call expr.expr_loc inject_id [expr] in
{ e with
expr_type = Type_predef.type_real;
expr_clock = expr.expr_clock;
}
let pp_inject_real pp_var pp_val fmt var value =
Format.fprintf fmt "%s(%a, %a, %s);"
inject_real_id
pp_var var
pp_val value
(mpfr_rnd ())
let inject_assign expr =
let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
{ e with
expr_type = Type_predef.type_real;
expr_clock = expr.expr_clock;
}
let pp_inject_copy pp_var fmt var value =
Format.fprintf fmt "%s(%a, %a, %s);"
inject_copy_id
pp_var var
pp_var value
(mpfr_rnd ())
let rec pp_inject_assign pp_var fmt var value =
if is_const_value value
then
pp_inject_real pp_var pp_var fmt var value
else
pp_inject_copy pp_var fmt var value
let pp_inject_init pp_var fmt var =
Format.fprintf fmt "%s(%a, %i);"
inject_init_id
pp_var var
(mpfr_prec ())
let pp_inject_clear pp_var fmt var =
Format.fprintf fmt "%s(%a);"
inject_clear_id
pp_var var
let base_inject_op id =
match id with
| "+" -> "MPFRPlus"
| "-" -> "MPFRMinus"
| "*" -> "MPFRTimes"
| "/" -> "MPFRDiv"
| "uminus" -> "MPFRUminus"
| "<=" -> "MPFRLe"
| "<" -> "MPFRLt"
| ">=" -> "MPFRGe"
| ">" -> "MPFRGt"
| "=" -> "MPFREq"
| "!=" -> "MPFRNeq"
| _ -> raise Not_found
let inject_op id =
try
base_inject_op id
with Not_found -> id
let homomorphic_funs =
List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
let is_homomorphic_fun id =
List.mem id homomorphic_funs
let inject_call expr =
match expr.expr_desc with
| Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
{ expr with expr_desc = Expr_appl (inject_op id, args, None) }
| _ -> expr
let expr_of_const_array expr =
match expr.expr_desc with
| Expr_const (Const_array cl) ->
let typ = Types.array_element_type expr.expr_type in
let expr_of_const c =
{ expr_desc = Expr_const c;
expr_type = typ;
expr_clock = expr.expr_clock;
expr_loc = expr.expr_loc;
expr_delay = Delay.new_var ();
expr_annot = None;
expr_tag = new_tag ();
}
in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
| _ -> assert false
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
let rec inject_list alias node inject_element defvars elist =
List.fold_right
(fun t (defvars, qlist) ->
let defvars, norm_t = inject_element alias node defvars t in
(defvars, norm_t :: qlist)
) elist (defvars, [])
let rec inject_expr ?(alias=true) node defvars expr =
let res=
match expr.expr_desc with
| Expr_const (Const_real _) -> mk_expr_alias_opt alias node defvars expr
| Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
| Expr_const (Const_struct _) -> assert false
| Expr_ident _
| Expr_const _ -> defvars, expr
| Expr_array elist ->
let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
defvars, norm_expr
| Expr_power (e1, d) ->
let defvars, norm_e1 = inject_expr node defvars e1 in
let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
defvars, norm_expr
| Expr_access (e1, d) ->
let defvars, norm_e1 = inject_expr node defvars e1 in
let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
defvars, norm_expr
| Expr_tuple elist ->
let defvars, norm_elist =
inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
defvars, norm_expr
| Expr_appl (id, args, r) ->
let defvars, norm_args = inject_expr node defvars args in
let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
mk_expr_alias_opt alias node defvars (inject_call norm_expr)
| Expr_arrow _ -> defvars, expr
| Expr_pre e ->
let defvars, norm_e = inject_expr node defvars e in
let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
defvars, norm_expr
| Expr_fby (e1, e2) ->
let defvars, norm_e1 = inject_expr node defvars e1 in
let defvars, norm_e2 = inject_expr node defvars e2 in
let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
defvars, norm_expr
| Expr_when (e, c, l) ->
let defvars, norm_e = inject_expr node defvars e in
let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
defvars, norm_expr
| Expr_ite (c, t, e) ->
let defvars, norm_c = inject_expr node defvars c in
let defvars, norm_t = inject_expr node defvars t in
let defvars, norm_e = inject_expr node defvars e in
let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
defvars, norm_expr
| Expr_merge (c, hl) ->
let defvars, norm_hl = inject_branches node defvars hl in
let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
defvars, norm_expr
in
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
res
and inject_branches node defvars hl =
List.fold_right
(fun (t, h) (defvars, norm_q) ->
let (defvars, norm_h) = inject_expr node defvars h in
defvars, (t, norm_h) :: norm_q
)
hl (defvars, [])
let rec inject_eq node defvars eq =
let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
let norm_eq = { eq with eq_rhs = norm_rhs } in
norm_eq::defs', vars'
(** normalize_node node returns a normalized node,
ie.
- updated locals
- new equations
-
*)
let inject_node node =
cpt_fresh := 0;
let inputs_outputs = node.node_inputs@node.node_outputs in
let is_local v =
List.for_all ((!=) v) inputs_outputs in
let orig_vars = inputs_outputs@node.node_locals in
let defs, vars =
List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in
(* Normalize the asserts *)
let vars, assert_defs, asserts =
List.fold_left (
fun (vars, def_accu, assert_accu) assert_ ->
let assert_expr = assert_.assert_expr in
let (defs, vars'), expr =
inject_expr
~alias:false
node
([], vars) (* defvar only contains vars *)
assert_expr
in
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
) (vars, [], []) node.node_asserts in
let new_locals = List.filter is_local vars in
(* Compute traceability info:
- gather newly bound variables
- compute the associated expression without aliases
*)
(* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
let node =
{ node with
node_locals = new_locals;
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
}
in ((*Printers.pp_node Format.err_formatter node;*) node)
let inject_decl decl =
match decl.top_decl_desc with
| Node nd ->
{decl with top_decl_desc = Node (inject_node nd)}
| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
let inject_prog decls =
List.map inject_decl decls
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
src/plugins.ml 0 → 100644
+ 35
− 0
View file @ 7db425aa
open LustreSpec
module type PluginType =
sig
end
let inline_annots rename_var_fun annot_list =
List.map (
fun ann ->
{ ann with
annots = List.fold_left (
fun accu (sl, eexpr) ->
let items =
match sl with
| plugin_name::args ->
if plugin_name = "salsa" then
match args with
| ["ranges";varname] ->
[["salsa";"ranges";(rename_var_fun varname)], eexpr]
| _ -> [(sl, eexpr)]
else
[(sl, eexpr)]
| _ -> assert false
in
items@accu
) [] ann.annots
}
) annot_list
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
src/plugins/scopes/scopes.ml 0 → 100644
+ 319
− 0
View file @ 7db425aa
open LustreSpec
open Corelang
open Machine_code
(* (variable, node name, node instance) *)
type scope_t = (var_decl * string * string option) list * var_decl
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 get_node name prog =
let node_opt = List.fold_left
(fun res top ->
match res, top.top_decl_desc with
| Some _, _ -> res
| None, Node nd ->
(* Format.eprintf "Checking node %s = %s: %b@." nd.node_id name (nd.node_id = name); *)
if nd.node_id = name then Some nd else res
| _ -> None)
None prog
in
try
Utils.desome node_opt
with Utils.DeSome -> raise Not_found
let get_machine name machines =
try
List.find (fun m -> m.mname.node_id = name) machines
with Not_found -> raise Not_found
let rec compute_scopes prog main_node : scope_t list =
(* Format.eprintf "Compute scope of %s@." main_node; *)
try
let node = get_node main_node prog in
let all_vars = node.node_inputs @ node.node_locals @ node.node_outputs in
let local_vars = node.node_inputs @ node.node_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 (Utils.fprintf_list ~sep:"," 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 print_scopes =
Utils.fprintf_list ~sep:"@ "
(fun fmt ((_, v) as s) -> Format.fprintf fmt "%a: %a"
(Utils.fprintf_list ~sep:"." Format.pp_print_string )(scope_to_sl s)
Types.print_ty v.var_type)
(* let print_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 @ node.node_locals )
with Not_found ->
Format.eprintf "Cannot find variable %s in node %s@." name node.node_id;
assert false
let scope_path main_node_name prog machines all_scopes sl : scope_t =
let rec get_path node id_list accu =
match id_list, accu with
| [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
| varid::nodename::id_list_tl, _ -> (
let e_machine = get_machine node.node_id machines in
(* Format.eprintf "Looking for def %s in call %s in machine %a@." *)
(* varid nodename *)
(* Machine_code.pp_machine e_machine; *)
let find_var = (fun v -> v.var_id = varid) in
let instance =
List.find
(fun i -> match i with
| MStep(p, o, _) -> List.exists find_var p
| _ -> false
)
e_machine.mstep.step_instrs
in
try
let variable, instance_node, instance_id =
match 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
in
let all_scopes_as_sl = List.map scope_to_sl all_scopes in
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 = (* Special treatment of first level flow *)
match sl with
| [flow] -> let flow_var = get_node_vdecl_of_name flow main_node in
[], flow_var
| _ -> get_path main_node sl []
in
(* Format.eprintf "computed path: %a.%s@." print_path path flow.var_id; *)
path, flow
)
let check_scopes main_node_name prog machines all_scopes scopes =
List.map
(fun sl ->
sl, scope_path main_node_name prog machines all_scopes sl
) scopes
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 true
let option_mem_scopes = ref false
let option_input_scopes = ref false
let scopes_map : (LustreSpec.ident list * scope_t) list ref = ref []
let register_scopes s =
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 := scope_list
let register_inputs s =
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
(* 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 pp_scopes fmt scopes =
let rec scope_path (path, flow) accu =
match path with
| [] -> accu ^ "_reg." ^ flow.var_id, flow.var_type
| (_, _, Some instance_id)::tl -> scope_path (tl, flow) ( accu ^ instance_id ^ "->" )
| _ -> assert false
in
let scopes_vars =
List.map
(fun (sl, scope) ->
String.concat "." sl, scope_path scope "main_mem.")
scopes
in
List.iter (fun (id, (var, typ)) ->
match (Types.repr typ).Types.tdesc with
| Types.Tint -> Format.fprintf fmt "_put_int(\"%s\", %s);@ " id var
| Types.Tbool -> Format.fprintf fmt "_put_bool(\"%s\", %s);@ " id var
| Types.Treal when !Options.mpfr ->
Format.fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s));@ " id var (Mpfr.mpfr_rnd ())
| Types.Treal -> Format.fprintf fmt "_put_double(\"%s\", %s);@ " id var
| _ -> Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty typ; assert false
) scopes_vars
let update_machine machine =
let stateassign vdecl =
MStateAssign (vdecl, mk_val (LocalVar vdecl) vdecl.var_type)
in
let local_decls = machine.mstep.step_inputs
(* @ machine.mstep.step_outputs *)
@ machine.mstep.step_locals
in
{ machine with
mmemory = machine.mmemory @ local_decls;
mstep = {
machine.mstep with
step_instrs = machine.mstep.step_instrs
@ (MComment "Registering all flows")::(List.map stateassign local_decls)
}
}
module Plugin =
struct
let name = "scopes"
let is_active () =
!option_scopes
let show_scopes () =
!option_show_scopes && (
Compiler_common.check_main ();
true)
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.Set option_all_scopes, "select all possible variables to log";
"-select-mem", Arg.Set option_mem_scopes, "select all memory variables to log";
"-select-inputs", Arg.Set option_input_scopes, "select all input variables to log";
]
let activate () =
option_scopes := true;
Options.optimization := 0; (* no optimization *)
Options.salsa_enabled := false; (* No salsa *)
()
let rec is_valid_path path nodename prog machines =
let nodescopes = compute_scopes prog nodename in
let m = get_machine nodename machines in
match path with
| [] -> assert false
| [vid] -> let res = List.exists (fun v -> v.var_id = vid) (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
| inst::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 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@." (Utils.fprintf_list ~sep:"." Format.pp_print_string) sl;
res
)
selected_scopes
in
scopes_map := check_scopes main_node prog machines all_scopes selected_scopes;
(* Each machine is updated with fresh memories and declared as stateful *)
let machines = List.map update_machine machines in
machines
let pp fmt = pp_scopes fmt !scopes_map
end
(* Local Variables: *)
(* compile-command:"make -C ../.." *)
(* End: *)
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