some optimization in code optimization !!

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@449 041b043f-8d7c-46b2-b46e-ef0dd855326e

src/automata.ml

@@ -24,9 +24,6 @@ type aut_state =
       actual_s : var_decl
     }
 
-let cpvar_decl var_decl =
- mkvar_decl var_decl.var_loc ~orig:var_decl.var_orig (var_decl.var_id, var_decl.var_dec_type, var_decl.var_dec_clock, var_decl.var_dec_const, var_decl.var_dec_value)
-
 let as_clock var_decl =
   let tydec = var_decl.var_dec_type in
   { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
@@ -37,9 +34,15 @@ let mkbool loc b =
 let mkident loc id =
  mkexpr loc (Expr_ident id)
 
+let mkconst loc id =
+ mkexpr loc (Expr_const (Const_tag id))
+
 let mkfby loc e1 e2 =
  mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
 
+let mkpair loc e1 e2 =
+ mkexpr loc (Expr_tuple [e1; e2])
+
 let mkidentpair loc restart state =
  mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
 
@@ -126,8 +129,8 @@ let node_of_unless nused used node aut_id aut_state handler =
     node_id = node_id;
     node_type = Types.new_var ();
     node_clock = Clocks.new_var true;
-    node_inputs = List.map cpvar_decl var_inputs;
-    node_outputs = List.map cpvar_decl var_outputs;
+    node_inputs = List.map copy_var_decl var_inputs;
+    node_outputs = List.map copy_var_decl var_outputs;
     node_locals = [];
     node_gencalls = [];
     node_checks = [];
@@ -176,9 +179,9 @@ let node_of_assign_until nused used node aut_id aut_state handler =
     node_id = node_id;
     node_type = Types.new_var ();
     node_clock = Clocks.new_var true;
-    node_inputs = List.map cpvar_decl var_inputs;
-    node_outputs = List.map cpvar_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
-    node_locals = List.map cpvar_decl (new_var_locals @ handler.hand_locals);
+    node_inputs = List.map copy_var_decl var_inputs;
+    node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
+    node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
     node_gencalls = [];
     node_checks = [];
     node_asserts = handler.hand_asserts; 
@@ -209,7 +212,7 @@ let expand_automata nused used owner typedef node aut =
   let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
   let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
   let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
-  let fby_incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
+  let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
   let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
   let locals' = vars_of_aut_state aut_state in
   let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in

src/liveness.ml

@@ -121,7 +121,11 @@ let is_aliasable_input node var =
     | None           -> []
     | Some (_, args) -> List.fold_right (fun e r -> match e.expr_desc with Expr_ident id -> id::r | _ -> r) args [] in
   fun v -> is_aliasable v && List.mem v.var_id inputs_var
-
+(*
+    let res =
+is_aliasable v && List.mem v.var_id inputs_var
+    in (Format.eprintf "aliasable %s by %s = %B@." var v.var_id res; res)
+*)
 (* replace variable [v] by [v'] in graph [g].
    [v'] is a dead variable
 *)
@@ -171,44 +175,50 @@ let compute_evaluated heads ctx =
   end
 
 (* tests whether a variable [v] may be (re)used instead of [var]. The conditions are:
+   - [v] has been really used ([v] is its own representative)
    - same type
    - [v] is not an aliasable input of the equation defining [var]
    - [v] is not one of the current heads (which contain [var])
-   - the representative of [v] is not currently in use
+   - [v] is not currently in use
  *)
 let eligible node ctx heads var v =
-     Typing.eq_ground var.var_type v.var_type
+     Hashtbl.find ctx.policy v.var_id == v
+  && Typing.eq_ground (Types.unclock_type var.var_type) (Types.unclock_type v.var_type)
   && not (is_aliasable_input node var.var_id v)
   && not (List.exists (fun h -> h.var_id = v.var_id) heads)
-  && let repr_v = Hashtbl.find ctx.policy v.var_id
-     in not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id repr_v.var_id) ctx.evaluated)
+  && (*let repr_v = Hashtbl.find ctx.policy v.var_id*)
+     not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id) ctx.evaluated)
 
 let compute_reuse node ctx heads var =
   let disjoint = Hashtbl.find ctx.disjoint var.var_id in
   let locally_reusable v =
     IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in
   let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in
+  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles);
   let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in
+  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);
   try
     let disjoint_live = Disjunction.CISet.inter disjoint live in
+    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);
     let reuse = Disjunction.CISet.max_elt disjoint_live in
-    let reuse' = Hashtbl.find ctx.policy reuse.var_id in
+    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
     begin
       IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
-      if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;
-      Hashtbl.add ctx.policy var.var_id reuse';
+      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
+      Hashtbl.add ctx.policy var.var_id reuse;
       ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
       (*Format.eprintf "%s reused by live@." var.var_id;*)
     end
   with Not_found ->
   try
     let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
+    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);
     let reuse = Disjunction.CISet.choose dead in
-    let reuse' = Hashtbl.find ctx.policy reuse.var_id in
+    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
     begin
       IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
-      if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;
-      Hashtbl.add ctx.policy var.var_id reuse';
+      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
+      Hashtbl.add ctx.policy var.var_id reuse;
       ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
       (*Format.eprintf "%s reused by dead %a@." var.var_id Disjunction.pp_ciset dead;*)
     end
@@ -229,7 +239,7 @@ let compute_reuse_policy node schedule disjoint g =
     Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);
     let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in
     Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:");
-    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s " head.var_id)) heads;
+    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads;
     Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@.");
     Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@.");
     compute_dependencies heads ctx;

src/main_lustre_compiler.ml

@@ -164,7 +164,7 @@ let rec compile_source dirname basename extension =
   if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
     begin
       let orig = Corelang.copy_prog orig in
-      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file !@,");
+      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
       check_stateless_decls orig;
       let _ = Typing.type_prog type_env orig in
       let _ = Clock_calculus.clock_prog clock_env orig in
@@ -173,8 +173,7 @@ let rec compile_source dirname basename extension =
       Inliner.witness 
 	basename
 	!Options.main_node
-	orig prog type_env clock_env;
-      Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@,");
+	orig prog type_env clock_env
     end;
 
 (*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)

src/types.ml

@@ -214,6 +214,12 @@ let get_clock_base_type ty =
  | Tclock ty -> Some ty
  | _         -> None
 
+let unclock_type ty =
+  let ty = repr ty in
+  match ty.tdesc with
+  | Tclock ty' -> ty'
+  | _          -> ty
+
 let rec is_dimension_type ty =
  match (repr ty).tdesc with
  | Tint