Added local inlining using the keyword (*! /inlining/:true *)

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

src/annotations.ml

+(********************************************************************)
+(*                                                                  *)
+(*  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 LustreSpec
+
+
+(* Associate to each annotation key the pair (node, expr tag) *)
+let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13
+let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13
+
+let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
+let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
+
+let get_expr_annotations key = Hashtbl.find_all expr_annotations key

src/corelang.ml

@@ -167,7 +167,10 @@ let merge_expr_annot ann1 ann2 =
       annot_loc = ann1.annot_loc
     }
 
-let update_expr_annot e annot =
+let update_expr_annot node_id e annot =
+  List.iter (fun (key, _) -> 
+    Annotations.add_expr_ann node_id e.expr_tag key
+  ) annot.annots;
   { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
 
 

src/corelang.mli

@@ -116,7 +116,6 @@ val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
 (** rename_prog f_node f_var f_const prog *)
 val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
 
-val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
 
 val substitute_expr: var_decl list -> eq list -> expr -> expr
 
@@ -124,7 +123,7 @@ val substitute_expr: var_decl list -> eq list -> expr -> expr
 val mkeexpr: Location.t ->  expr -> eexpr
 val merge_node_annot: node_annot -> node_annot -> node_annot 
 val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
-val update_expr_annot: expr -> expr_annot -> expr
+val update_expr_annot: ident -> expr -> LustreSpec.expr_annot -> expr
 (* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
 
 (* Local Variables: *)

src/inliner.ml

@@ -11,6 +11,16 @@
 
 open LustreSpec
 open Corelang
+open Utils
+
+(* Local annotations are declared with the following key /inlining/: true *)
+let keyword = ["inlining"]
+
+let is_inline_expr expr = 
+match expr.expr_annot with
+| Some ann -> 
+  List.exists (fun (key, value) -> key = keyword) ann.annots
+| None -> false
 
 let check_node_name id = (fun t -> 
   match t.top_decl_desc with 
@@ -90,7 +100,9 @@ let inline_call orig_expr args reset locals node =
    variables and the code of called node instance added to new_eqs
 
 *)
-let rec inline_expr expr locals nodes =
+let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
+  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
+  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
   let inline_tuple el = 
     List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
       let e', locals', eqs', asserts' = inline_expr e locals nodes in
@@ -109,13 +121,17 @@ let rec inline_expr expr locals nodes =
     | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
     | _ -> assert false
   in
-    
+  
   match expr.expr_desc with
   | Expr_appl (id, args, reset) ->
     let args', locals', eqs', asserts' = inline_expr args locals nodes in 
-    if List.exists (check_node_name id) nodes then 
+    if List.exists (check_node_name id) nodes && (* the current node call is provided
+						    as arguments nodes *)
+      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
+							      it is explicitely inlined here *)
+    then 
       (* The node should be inlined *)
-      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
+       let _ =     Format.eprintf "Inlining call to %s@." id in 
       let node = try List.find (check_node_name id) nodes 
 	with Not_found -> (assert false) in
       let node = node_of_top node in
@@ -164,7 +180,8 @@ let rec inline_expr expr locals nodes =
     let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
     let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
     { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
-and inline_node nd nodes = 
+and inline_node ?(selection_on_annotation=false) nd nodes = 
+  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
   let new_locals, eqs, asserts = 
     List.fold_left (fun (locals, eqs, asserts) eq ->
       let eq_rhs', locals', new_eqs', asserts' = 
@@ -319,6 +336,23 @@ let global_inline basename prog type_env clock_env =
   );
   res
 
+let local_inline basename prog type_env clock_env =
+  let local_anns = Annotations.get_expr_annotations keyword in
+  if local_anns != [] then (
+    let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
+    ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
+    List.fold_right (fun top accu -> 
+      ( match top.top_decl_desc with
+      | Node nd when ISet.mem nd.node_id nodes_with_anns ->
+	{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
+      | _ -> top
+      )::accu) prog []
+    
+)
+ else
+  prog
+
+
 (* Local Variables: *)
 (* compile-command:"make -C .." *)
 (* End: *)

src/main_lustre_compiler.ml

@@ -127,12 +127,12 @@ let rec compile_source dirname basename extension =
     if !Options.global_inline &&
       (match !Options.main_node with | "" -> false | _ -> true) then
       Inliner.global_inline basename prog type_env clock_env
-    else
-      prog
+    else (* if !Option.has_local_inline *)
+      Inliner.local_inline basename prog type_env clock_env
   in
 
   (* Delay calculus *)
-  (*
+  (* TO BE DONE LATER (Xavier)
     if(!Options.delay_calculus)
     then
     begin
@@ -146,18 +146,7 @@ let rec compile_source dirname basename extension =
     raise exc
     end;
   *)
-  (*
-    eprintf "Causality analysis@.@?";
-    (* Causality analysis *)
-    begin
-    try
-    Causality.check_causal_prog prog
-    with (Causality.Cycle v) as exc ->
-    Causality.pp_error err_formatter v;
-    raise exc
-    end;
-  *)
-
+  
   (* Creating destination directory if needed *)
   create_dest_dir ();
 

src/parserLustreSpec.mly

@@ -73,7 +73,7 @@
 %nonassoc UMINUS
 
 %start lustre_annot
-%type <LustreSpec.expr_annot> lustre_annot
+%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot
 
 %start lustre_spec
 %type <LustreSpec.node_annot> lustre_spec
@@ -287,7 +287,7 @@ const:
 | STRING {Const_string $1}
 
 lustre_annot:
-lustre_annot_list EOF { $1 }
+lustre_annot_list EOF { fun node_id -> $1 }
 
 lustre_annot_list:
   { [] } 

src/parser_lustre.mly

@@ -37,6 +37,12 @@ let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
 
 let mkannots annots = { annots = annots; annot_loc = get_loc () }
 
+let node_stack : ident list ref = ref []
+let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
+let push_node nd =  node_stack:= nd :: !node_stack
+let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
+let get_current_node () = try List.hd !node_stack with _ -> assert false
+
 %}
 
 %token <int> INT
@@ -118,6 +124,9 @@ node_ident:
   UIDENT { $1 }
 | IDENT  { $1 }
 
+node_ident_decl:
+ node_ident { push_node $1; $1 }
+
 vdecl_ident:
   UIDENT { $1 }
 | IDENT  { $1 }
@@ -176,6 +185,7 @@ top_decl_header:
 				  nodei_prototype = $13;
 				  nodei_in_lib = $14;})
      in
+     pop_node ();
      (*add_imported_node $3 nd;*) [nd] }
 
 prototype_opt:
@@ -188,27 +198,35 @@ in_lib_opt:
 
 top_decl:
 | CONST cdecl_list { List.rev ($2 false) }
-| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 
-    {let stmts, asserts, annots = $16 in
-     let nd = mktop_decl false (Node
-				  {node_id = $3;
-				   node_type = Types.new_var ();
-				   node_clock = Clocks.new_var true;
-				   node_inputs = List.rev $5;
-				   node_outputs = List.rev $10;
-				   node_locals = List.rev $14;
-				   node_gencalls = [];
-				   node_checks = [];
-				   node_asserts = asserts; 
-				   node_stmts = stmts;
-				   node_dec_stateless = $2;
-				   node_stateless = None;
-				   node_spec = $1;
-				   node_annot = annots})
-     in
+| nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 
+    {
+      let stmts, asserts, annots = $16 in
+      (* Declaring eqs annots *)
+      List.iter (fun ann -> 
+	List.iter (fun (key, _) -> 
+	  Annotations.add_node_ann $3 key
+	) ann.annots
+      ) annots;
+     (* Building the node *)
+      let nd = mktop_decl false (Node
+				   {node_id = $3;
+				    node_type = Types.new_var ();
+				    node_clock = Clocks.new_var true;
+				    node_inputs = List.rev $5;
+				    node_outputs = List.rev $10;
+				    node_locals = List.rev $14;
+				    node_gencalls = [];
+				    node_checks = [];
+				    node_asserts = asserts; 
+				    node_stmts = stmts;
+				    node_dec_stateless = $2;
+				    node_stateless = None;
+				    node_spec = $1;
+				    node_annot = annots})
+      in
      (*add_node $3 nd;*) [nd] }
-
-nodespec_list:
+    
+ nodespec_list:
  { None }
 | NODESPEC nodespec_list { 
   (function 
@@ -350,7 +368,7 @@ expr:
 | IDENT { mkexpr (Expr_ident $1) }
 | tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
 | LPAR ANNOT expr RPAR
-    {update_expr_annot $3 $2}
+    {update_expr_annot (get_current_node ()) $3 $2}
 | LPAR expr RPAR
     {$2}
 | LPAR tuple_expr RPAR