Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.

TODO.org

@@ -69,3 +69,56 @@ if c then
 else {}
 
 x = if c then expr else x
+* Seal
+
+The Seal library should be available from LustreV
+
+lustrev -seal -node foo bar.lus 
+
+shall inline completely the node foo in bar.lus and compile it as a
+piecewise system: 
+- Memories have to be identified and one needs to separate the update
+  of the memories and the production of the output.
+- The update block should be normalized so that any ite occuring in
+  the definition of a memory should not define a local flow used in
+  basic operations.  In other words, the definitions should look like
+  mem_x = if g then e1 else e2 where e1 and e2 are either ite
+  expression or expressions without ite. As soon as a not-ite
+  expression is selected it cannot depend on the output of an ite.
+
+In a first step this normalized update shall be printed in
+stdout. Later it will associated to a SEAL datastructure through SEAL
+API.
+
+** Algorithm
+
+*** 1. Computation of update block
+- First we inline the node
+- After normalization the memories are the variables defined by a pre
+- Do we have to deal with arrows and reset?
+- Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
+- one can also slice the expressions on the output variables
+
+*** 2. Normalization: piecewise system
+ ie. all ite pushed at the beginning
+
+- use the scheduling to obtain the dependencies amongs eqs
+- one can then iterate through eqs from the bottom to the top
+  if the eq looks like x = if g then e1 else e2
+  then tag x as ite(g,e1,e2)
+  if the parent expr y = if g2 then x else ... make 
+** More general use
+Some ideas
+- One could request multiple nodes: how to deal with these? Acting as
+  as many calls to the basic procedure?
+- Shall we keep the flatten update structure to the node? Another
+  property on input could be propagated.
+- The analysis will depend on bounds on input flows. Can we specialize
+  the update blocks based on input values, ie. disabling some branches
+  of the ite-tree?
+- 
+
+** TODO list
+
+* Salsa
+* 

src/causality.ml

@@ -85,6 +85,15 @@ let add_vertices vtc g =
 let new_graph () =
   IdentDepGraph.create ()
 
+(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
+let slice_graph gr v =
+  begin
+    let gr' = new_graph () in
+    IdentDepGraph.add_vertex gr' v;
+    Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v;
+    gr'
+  end
+
     
 module ExprDep = struct
   let get_node_eqs nd =
@@ -374,15 +383,6 @@ module NodeDep = struct
 	   
       ) prog g in
     g   
-
-  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
-  let slice_graph gr v =
-    begin
-      let gr' = new_graph () in
-      IdentDepGraph.add_vertex gr' v;
-      Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v;
-      gr'
-    end
       
   let rec filter_static_inputs inputs args =
     match inputs, args with

src/scheduling_type.ml

+open Utils
+open Lustre_types
+
+type schedule_report =
+{
+  (* the scheduled node *)
+  node : node_desc;
+  (* a schedule computed wrt the dependency graph *)
+  schedule : ident list list;
+  (* the set of unused variables (no output or mem depends on them) *)
+  unused_vars : ISet.t;
+  (* the table mapping each local var to its in-degree *)
+  fanin_table : (ident, int) Hashtbl.t;
+  (* the dependency graph *)
+  dep_graph   : IdentDepGraph.t;
+  (* the table mapping each assignment to a reusable variable *)
+  (*reuse_table : (ident, var_decl) Hashtbl.t*)
+}
+ 

src/tools/seal_utils.ml

+open Lustre_types
+open Utils
+   
+
+let compute_sliced_vars vars_to_keep deps nd =
+  let is_variable vid = 
+    List.exists
+      (fun v -> v.var_id = vid)
+      nd.node_locals
+  in
+  let find_variable vid = 
+      List.find
+        (fun v -> v.var_id = vid)
+        nd.node_locals
+  in  
+
+  (* Returns the vars required to compute v. 
+     Memories are specifically identified. *)
+  let coi_var v =
+    let vname = v.var_id in
+    let sliced_deps =
+      Causality.slice_graph deps vname
+    in
+    Format.eprintf "sliced graph for %a: %a@."
+      Printers.pp_var v
+      Causality.pp_dep_graph sliced_deps;
+    let vset, memset =
+      IdentDepGraph.fold_vertex
+        (fun vname (vset,memset)  ->
+          if Causality.ExprDep.is_read_var vname
+          then
+            let vname' = String.sub vname 1 (-1 + String.length vname) in
+            if is_variable vname' then
+              ISet.add vname' vset,
+              ISet.add vname' memset
+            else
+              vset, memset
+          else
+            ISet.add vname vset, memset
+        )
+        sliced_deps
+        (ISet.singleton vname, ISet.empty)
+    in
+    Format.eprintf "COI of var %s: (%a // %a)@."
+      v.var_id
+      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
+      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
+    ;
+      vset, memset
+  in
+
+  (* Computes the variables required to compute
+     vl. Variables /seen/ do not need to 
+     be computed *) 
+  let rec coi_vars vl seen = 
+    List.fold_left
+      (fun accu v ->
+        let vset, memset = coi_var v in
+        (* We handle the new mems 
+           discovered in  the coi *)
+        let memset =
+          ISet.filter (
+              fun vid ->
+              not
+                (List.exists
+                   (fun v -> v.var_id = vid)
+                   vl
+                ) 
+            ) memset
+        in
+        let memset_vars = 
+          ISet.fold (
+              fun vid accu ->
+              (find_variable vid)::accu
+            ) memset [] 
+        in
+        let vset' =
+          coi_vars memset_vars (vl@seen)
+        in
+        ISet.union accu (ISet.union vset vset')
+      )
+      ISet.empty
+      (List.filter
+         (fun v -> not (List.mem v seen))
+         vl
+      )
+  in
+  ISet.elements (coi_vars vars_to_keep []) 
+
+
+  (* If existing outputs are included in vars_to_keep, just slice the content.
+   Otherwise outputs are replaced by vars_to_keep *)
+let slice_node vars_to_keep deps nd =
+  let coi_vars =
+    compute_sliced_vars vars_to_keep deps nd
+  in
+  Format.eprintf "COI Vars: %a@."
+    (Utils.fprintf_list ~sep:"," Format.pp_print_string)
+     coi_vars;
+  let outputs =
+    List.filter
+      (
+        fun v -> List.mem v.var_id coi_vars 
+      ) nd.node_outputs
+  in
+  let outputs = match outputs with
+      [] -> (
+      Format.eprintf "No visible output variable, subtituting with provided vars@ ";
+      vars_to_keep
+    )
+    | l -> l
+  in
+  let locals =
+    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
+  in
+  let stmts =
+    List.filter (
+        fun stmt ->
+        match stmt with
+        | Aut _ -> assert false
+        | Eq eq -> (
+          match eq.eq_lhs with
+            [vid] -> List.mem vid coi_vars
+          | _ -> assert false
+        (* should not happen after inlining and normalization *)
+        )
+      ) nd.node_stmts
+  in
+  { nd
+  with
+    node_outputs = outputs;
+    node_locals = locals;
+    node_stmts = stmts 
+  }

src/tools/seal_verifier.ml

+open Seal_utils
+
 let active = ref false
 
+(* Select the appropriate node, should have been inlined already and
+   extract update/output functions. *)
+let seal_run basename prog machines =
+  let node_name =
+    match !Options.main_node with
+    | "" -> assert false
+    | s -> s
+  in
+  let m = Machine_code_common.get_machine machines node_name in
+  let nd = m.mname in
+  Format.eprintf "Node %a@." Printers.pp_node nd; 
+  let mems = m.mmemory in
+  Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems;
+  let msch = Utils.desome m.msch in
+  let deps = msch.Scheduling_type.dep_graph in
+  Format.eprintf "graph: %a@." Causality.pp_dep_graph deps;
+  let sliced_nd = slice_node mems deps nd in
+  Format.eprintf "Node %a@." Printers.pp_node sliced_nd; 
+  ()
+  
 module Verifier =
   (struct
     include VerifierType.Default
     let name = "seal"
     let options = []
-    let activate () = active := true
+    let activate () =
+      active := true;
+      Options.global_inline := true
+      
     let is_active () = !active
-    let run basename prog machines = ()
+    let run = seal_run
+      
                     
   end: VerifierType.S)
     

src/utils.ml

@@ -35,9 +35,10 @@ end
 module IMap = Map.Make(IdentModule)
     
 module ISet = Set.Make(IdentModule)
-module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
+module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)
 module TopologicalDepGraph = Topological.Make(IdentDepGraph)
-
+module ComponentsDepGraph = Components.Make(IdentDepGraph) 
+                           
 (*module DotGraph = Graphviz.Dot (IdentDepGraph)*)
 module Bfs = Traverse.Bfs (IdentDepGraph)