Project

General

Profile

Revision a703ed0c

View differences:

TODO.org
69 69
else {}
70 70

  
71 71
x = if c then expr else x
72
* Seal
73

  
74
The Seal library should be available from LustreV
75

  
76
lustrev -seal -node foo bar.lus 
77

  
78
shall inline completely the node foo in bar.lus and compile it as a
79
piecewise system: 
80
- Memories have to be identified and one needs to separate the update
81
  of the memories and the production of the output.
82
- The update block should be normalized so that any ite occuring in
83
  the definition of a memory should not define a local flow used in
84
  basic operations.  In other words, the definitions should look like
85
  mem_x = if g then e1 else e2 where e1 and e2 are either ite
86
  expression or expressions without ite. As soon as a not-ite
87
  expression is selected it cannot depend on the output of an ite.
88

  
89
In a first step this normalized update shall be printed in
90
stdout. Later it will associated to a SEAL datastructure through SEAL
91
API.
92

  
93
** Algorithm
94

  
95
*** 1. Computation of update block
96
- First we inline the node
97
- After normalization the memories are the variables defined by a pre
98
- Do we have to deal with arrows and reset?
99
- Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
100
- one can also slice the expressions on the output variables
101

  
102
*** 2. Normalization: piecewise system
103
 ie. all ite pushed at the beginning
104

  
105
- use the scheduling to obtain the dependencies amongs eqs
106
- one can then iterate through eqs from the bottom to the top
107
  if the eq looks like x = if g then e1 else e2
108
  then tag x as ite(g,e1,e2)
109
  if the parent expr y = if g2 then x else ... make 
110
** More general use
111
Some ideas
112
- One could request multiple nodes: how to deal with these? Acting as
113
  as many calls to the basic procedure?
114
- Shall we keep the flatten update structure to the node? Another
115
  property on input could be propagated.
116
- The analysis will depend on bounds on input flows. Can we specialize
117
  the update blocks based on input values, ie. disabling some branches
118
  of the ite-tree?
119
- 
120

  
121
** TODO list
122

  
123
* Salsa
124
* 
src/causality.ml
85 85
let new_graph () =
86 86
  IdentDepGraph.create ()
87 87

  
88
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
89
let slice_graph gr v =
90
  begin
91
    let gr' = new_graph () in
92
    IdentDepGraph.add_vertex gr' v;
93
    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;
94
    gr'
95
  end
96

  
88 97
    
89 98
module ExprDep = struct
90 99
  let get_node_eqs nd =
......
374 383
	   
375 384
      ) prog g in
376 385
    g   
377

  
378
  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
379
  let slice_graph gr v =
380
    begin
381
      let gr' = new_graph () in
382
      IdentDepGraph.add_vertex gr' v;
383
      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;
384
      gr'
385
    end
386 386
      
387 387
  let rec filter_static_inputs inputs args =
388 388
    match inputs, args with
src/scheduling_type.ml
1
open Utils
2
open Lustre_types
3

  
4
type schedule_report =
5
{
6
  (* the scheduled node *)
7
  node : node_desc;
8
  (* a schedule computed wrt the dependency graph *)
9
  schedule : ident list list;
10
  (* the set of unused variables (no output or mem depends on them) *)
11
  unused_vars : ISet.t;
12
  (* the table mapping each local var to its in-degree *)
13
  fanin_table : (ident, int) Hashtbl.t;
14
  (* the dependency graph *)
15
  dep_graph   : IdentDepGraph.t;
16
  (* the table mapping each assignment to a reusable variable *)
17
  (*reuse_table : (ident, var_decl) Hashtbl.t*)
18
}
19
 
src/tools/seal_utils.ml
1
open Lustre_types
2
open Utils
3
   
4

  
5
let compute_sliced_vars vars_to_keep deps nd =
6
  let is_variable vid = 
7
    List.exists
8
      (fun v -> v.var_id = vid)
9
      nd.node_locals
10
  in
11
  let find_variable vid = 
12
      List.find
13
        (fun v -> v.var_id = vid)
14
        nd.node_locals
15
  in  
16

  
17
  (* Returns the vars required to compute v. 
18
     Memories are specifically identified. *)
19
  let coi_var v =
20
    let vname = v.var_id in
21
    let sliced_deps =
22
      Causality.slice_graph deps vname
23
    in
24
    Format.eprintf "sliced graph for %a: %a@."
25
      Printers.pp_var v
26
      Causality.pp_dep_graph sliced_deps;
27
    let vset, memset =
28
      IdentDepGraph.fold_vertex
29
        (fun vname (vset,memset)  ->
30
          if Causality.ExprDep.is_read_var vname
31
          then
32
            let vname' = String.sub vname 1 (-1 + String.length vname) in
33
            if is_variable vname' then
34
              ISet.add vname' vset,
35
              ISet.add vname' memset
36
            else
37
              vset, memset
38
          else
39
            ISet.add vname vset, memset
40
        )
41
        sliced_deps
42
        (ISet.singleton vname, ISet.empty)
43
    in
44
    Format.eprintf "COI of var %s: (%a // %a)@."
45
      v.var_id
46
      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
47
      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
48
    ;
49
      vset, memset
50
  in
51

  
52
  (* Computes the variables required to compute
53
     vl. Variables /seen/ do not need to 
54
     be computed *) 
55
  let rec coi_vars vl seen = 
56
    List.fold_left
57
      (fun accu v ->
58
        let vset, memset = coi_var v in
59
        (* We handle the new mems 
60
           discovered in  the coi *)
61
        let memset =
62
          ISet.filter (
63
              fun vid ->
64
              not
65
                (List.exists
66
                   (fun v -> v.var_id = vid)
67
                   vl
68
                ) 
69
            ) memset
70
        in
71
        let memset_vars = 
72
          ISet.fold (
73
              fun vid accu ->
74
              (find_variable vid)::accu
75
            ) memset [] 
76
        in
77
        let vset' =
78
          coi_vars memset_vars (vl@seen)
79
        in
80
        ISet.union accu (ISet.union vset vset')
81
      )
82
      ISet.empty
83
      (List.filter
84
         (fun v -> not (List.mem v seen))
85
         vl
86
      )
87
  in
88
  ISet.elements (coi_vars vars_to_keep []) 
89

  
90

  
91
  (* If existing outputs are included in vars_to_keep, just slice the content.
92
   Otherwise outputs are replaced by vars_to_keep *)
93
let slice_node vars_to_keep deps nd =
94
  let coi_vars =
95
    compute_sliced_vars vars_to_keep deps nd
96
  in
97
  Format.eprintf "COI Vars: %a@."
98
    (Utils.fprintf_list ~sep:"," Format.pp_print_string)
99
     coi_vars;
100
  let outputs =
101
    List.filter
102
      (
103
        fun v -> List.mem v.var_id coi_vars 
104
      ) nd.node_outputs
105
  in
106
  let outputs = match outputs with
107
      [] -> (
108
      Format.eprintf "No visible output variable, subtituting with provided vars@ ";
109
      vars_to_keep
110
    )
111
    | l -> l
112
  in
113
  let locals =
114
    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
115
  in
116
  let stmts =
117
    List.filter (
118
        fun stmt ->
119
        match stmt with
120
        | Aut _ -> assert false
121
        | Eq eq -> (
122
          match eq.eq_lhs with
123
            [vid] -> List.mem vid coi_vars
124
          | _ -> assert false
125
        (* should not happen after inlining and normalization *)
126
        )
127
      ) nd.node_stmts
128
  in
129
  { nd
130
  with
131
    node_outputs = outputs;
132
    node_locals = locals;
133
    node_stmts = stmts 
134
  }
src/tools/seal_verifier.ml
1
open Seal_utils
2

  
1 3
let active = ref false
2 4

  
5
(* Select the appropriate node, should have been inlined already and
6
   extract update/output functions. *)
7
let seal_run basename prog machines =
8
  let node_name =
9
    match !Options.main_node with
10
    | "" -> assert false
11
    | s -> s
12
  in
13
  let m = Machine_code_common.get_machine machines node_name in
14
  let nd = m.mname in
15
  Format.eprintf "Node %a@." Printers.pp_node nd; 
16
  let mems = m.mmemory in
17
  Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems;
18
  let msch = Utils.desome m.msch in
19
  let deps = msch.Scheduling_type.dep_graph in
20
  Format.eprintf "graph: %a@." Causality.pp_dep_graph deps;
21
  let sliced_nd = slice_node mems deps nd in
22
  Format.eprintf "Node %a@." Printers.pp_node sliced_nd; 
23
  ()
24
  
3 25
module Verifier =
4 26
  (struct
5 27
    include VerifierType.Default
6 28
    let name = "seal"
7 29
    let options = []
8
    let activate () = active := true
30
    let activate () =
31
      active := true;
32
      Options.global_inline := true
33
      
9 34
    let is_active () = !active
10
    let run basename prog machines = ()
35
    let run = seal_run
36
      
11 37
                    
12 38
  end: VerifierType.S)
13 39
    
src/utils.ml
35 35
module IMap = Map.Make(IdentModule)
36 36
    
37 37
module ISet = Set.Make(IdentModule)
38
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
38
module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)
39 39
module TopologicalDepGraph = Topological.Make(IdentDepGraph)
40

  
40
module ComponentsDepGraph = Components.Make(IdentDepGraph) 
41
                           
41 42
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)
42 43
module Bfs = Traverse.Bfs (IdentDepGraph)
43 44

  

Also available in: Unified diff