Project

General

Profile

Download (8.45 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handle reset *)
16

    
17
open Utils
18
open Format
19
open Lustre_types
20
open Corelang
21
open Machine_code_types
22
open Horn_backend_common
23
open Horn_backend_printers
24

    
25
let pp_traces =
26
  pp_comma_list (fun fmt (v, e) -> fprintf fmt "%s -> %a" v Printers.pp_expr e)
27

    
28
(* Compute memories associated to each machine *)
29
let compute_mems machines m =
30
  let rec aux prefix m =
31
    List.map (fun mem -> prefix, mem) m.mmemory
32
    @ List.fold_left
33
        (fun accu (id, (n, _)) ->
34
          let name = node_name n in
35
          if name = "_arrow" then accu
36
          else
37
            let machine_n = get_machine machines name in
38
            aux ((id, machine_n) :: prefix) machine_n @ accu)
39
        [] m.minstances
40
  in
41
  aux [] m
42

    
43
(* We extract the annotation dealing with traceability *)
44
let machines_traces machines =
45
  List.map
46
    (fun m ->
47
      let traces : (ident * expr) list =
48
        let all_annots =
49
          List.flatten (List.map (fun ann -> ann.annots) m.mannot)
50
        in
51
        let filtered =
52
          List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots
53
        in
54
        (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot)
55
           (m.mannot); *)
56
        let content = List.map snd filtered in
57
        (* Elements are supposed to be a pair (tuple): variable, expression *)
58
        List.map
59
          (fun ee ->
60
            match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
61
            | [], Expr_tuple [ v; e ] -> (
62
              match v.expr_desc with
63
              | Expr_ident vid ->
64
                vid, e
65
              | _ ->
66
                assert false)
67
            | _ ->
68
              assert false)
69
          content
70
      in
71
      (* eprintf "Build traces: %a@." pp_traces traces; *)
72
      m, traces)
73
    machines
74

    
75
let memories_old machines m =
76
  List.map
77
    (fun (p, v) ->
78
      let machine = match p with [] -> m | (_, m') :: _ -> m' in
79
      let traces = List.assoc machine (machines_traces machines) in
80
      if List.mem_assoc v.var_id traces then
81
        ( (* We take the expression associated to variable v in the trace info *)
82

    
83
          (* eprintf "Found variable %a in traces: %a@." Printers.pp_var v *
84
             Printers.pp_expr (List.assoc v.var_id traces); *)
85
          p,
86
          List.assoc v.var_id traces )
87
      else
88
        ( (* We keep the variable as is: we create an expression v *)
89

    
90
          (* eprintf "Unable to found variable %a in traces (%a)@."
91
             Printers.pp_var v * pp_traces traces; *)
92
          p,
93
          mkexpr Location.dummy (Expr_ident v.var_id) ))
94
    (compute_mems machines m)
95

    
96
let memories_next machines m =
97
  (* We remove the topest pre in each expression *)
98
  List.map
99
    (fun (prefix, ee) ->
100
      let m = match prefix with [] -> m | (_, m') :: _ -> m' in
101
      match ee.expr_desc with
102
      | Expr_pre e ->
103
        prefix, e
104
      | Expr_ident var_id ->
105
        (* This memory was not introduced through normalization. It shall then
106
           be a regular x = pre y expression. Otherwise it would have been
107
           rewritten. We have to get its definition and extract the argument of
108
           the pre *)
109
        let selected_def =
110
          try
111
            List.find
112
              (fun def ->
113
                match def with
114
                | Eq eq -> (
115
                  match eq.eq_lhs with [ v ] -> v = var_id | _ -> assert false)
116
                | _ ->
117
                  false)
118
              m.mname.node_stmts
119
          with _ ->
120
            eprintf
121
              "Unable to find definition of %s in stmts %a@.prefix=%a@.@?"
122
              var_id Printers.pp_node_stmts m.mname.node_stmts
123
              (pp_comma_list (fun fmt (id, n) ->
124
                   fprintf fmt "(%s,%s)" id n.mname.node_id))
125
              (List.rev prefix);
126

    
127
            assert false
128
        in
129
        let def =
130
          match selected_def with
131
          | Eq eq -> (
132
            match eq.eq_lhs, eq.eq_rhs.expr_desc with
133
            | [ single_var ], Expr_pre e ->
134
              if single_var = var_id then e else assert false
135
            | _ ->
136
              assert false)
137
          | _ ->
138
            assert false
139
        in
140
        prefix, def
141
      | _ ->
142
        eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
143
          (pp_comma_list (fun fmt (id, n) ->
144
               fprintf fmt "(%s,%s)" id n.mname.node_id))
145
          (List.rev prefix) Printers.pp_expr ee;
146
        assert false)
147
    (memories_old machines m)
148

    
149
let pp_prefix_rev fmt prefix =
150
  pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
151
    (fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
152
    fmt (List.rev prefix)
153

    
154
let traces_file fmt machines =
155
  let pp_l = pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " | ") in
156
  fprintf fmt "<?xml version=\"1.0\"?>@.";
157
  fprintf fmt
158
    "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
159
  fprintf fmt "@[<v 5>@ %a@ @]@."
160
    (pp_print_list (fun fmt m ->
161
         let pp_var = pp_horn_var m in
162
         let memories_old = memories_old machines m in
163
         let memories_next = memories_next machines m in
164

    
165
         (* fprintf fmt "; Node %s@." m.mname.node_id; *)
166
         fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
167

    
168
         let input_vars =
169
           rename_machine_list m.mname.node_id m.mstep.step_inputs
170
         in
171
         let output_vars =
172
           rename_machine_list m.mname.node_id m.mstep.step_outputs
173
         in
174
         fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
175
           (pp_l (pp_horn_var m)) input_vars
176
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) input_vars
177
           (pp_l (pp_horn_var m)) m.mstep.step_inputs;
178

    
179
         fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
180
           (pp_l pp_var) output_vars
181
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) output_vars
182
           (pp_l pp_var) m.mstep.step_outputs;
183

    
184
         let local_vars =
185
           try full_memory_vars ~without_arrow:true machines m
186
           with Not_found ->
187
             eprintf "machine %s@.@?" m.mname.node_id;
188
             assert false
189
         in
190
         let init_local_vars = rename_next_list local_vars in
191
         let step_local_vars = rename_current_list local_vars in
192

    
193
         fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ "
194
           (pp_l pp_var)
195
           init_local_vars
196
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
197
           (fun fmt ->
198
             match memories_next with [] -> () | _ -> fprintf fmt "")
199
           (pp_l (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee))
200
           memories_next;
201

    
202
         fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
203
           (pp_l pp_var) step_local_vars
204
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
205
           (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
206
           (pp_l (fun fmt (_, ee) -> fprintf fmt "(%a)" pp_xml_expr ee))
207
           memories_old;
208

    
209
         let arrow_vars = arrow_vars machines m in
210
         let arrow_vars_curr = rename_current_list arrow_vars
211
         and arrow_vars_mid = rename_mid_list arrow_vars
212
         and arrow_vars_next = rename_next_list arrow_vars in
213
         pp_print_list (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
214
           fmt
215
           (arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next);
216
         fprintf fmt "@]@ </Node>"))
217
    (List.rev machines);
218
  fprintf fmt "</Traces>@."
219

    
220
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a"
221
   pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
222
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
223
(* pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
224

    
225
(* Local Variables: *)
226
(* compile-command:"make -C ../.." *)
227
(* End: *)
(9-9/10)