Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/Horn/horn_backend_traces.ml
12 12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13 13
   Kahsai, HCSV'14.
14 14

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

  
18 17
open Format
19 18
open Lustre_types
20 19
open Corelang
21 20
open Machine_code_types
22

  
23 21
open Horn_backend_common
24 22
open Horn_backend_printers
25 23

  
26
let pp_traces = (Utils.fprintf_list ~sep:", " (fun fmt (v,e) -> Format.fprintf fmt "%s -> %a"
27
                                                         v
28
                                                         Printers.pp_expr e))
24
let pp_traces =
25
  Utils.fprintf_list ~sep:", " (fun fmt (v, e) ->
26
      Format.fprintf fmt "%s -> %a" v Printers.pp_expr e)
29 27

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

  
44

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

  
68
  ) machines
69
  
71
      (* Format.eprintf "Build traces: %a@." pp_traces traces; *)
72
      m, traces)
73
    machines
74

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

  
79
	 (* eprintf "Found variable %a in traces: %a@."  Printers.pp_var v
80
	  *   Printers.pp_expr (List.assoc v.var_id traces);  *)
81
	p, List.assoc v.var_id traces
82
      )
83
    else 
84
      begin
85

  
86
	(* We keep the variable as is: we create an expression v *)
87

  
88
	 (* eprintf "Unable to found variable %a in traces (%a)@."  Printers.pp_var v
89
	  *   pp_traces traces;  *)
90

  
91
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
92
      end
93

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

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

  
153 148

  
154 149
let pp_prefix_rev fmt prefix =
155
  Utils.fprintf_list ~sep:"." 
156
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) 
157
    fmt 
158
    (List.rev prefix)
159
      
150
  Utils.fprintf_list ~sep:"."
151
    (fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
152
    fmt (List.rev prefix)
160 153

  
161 154
let traces_file fmt machines =
162 155
  fprintf fmt "<?xml version=\"1.0\"?>@.";
163
  fprintf fmt "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
156
  fprintf fmt
157
    "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
164 158
  fprintf fmt "@[<v 5>@ %a@ @]@."
165 159
    (Utils.fprintf_list ~sep:"@ " (fun fmt m ->
166
      let pp_var = pp_horn_var m in
167
      let memories_old = memories_old  machines m in
168
      let memories_next = memories_next  machines m in
169
      
170
      (* fprintf fmt "; Node %s@." m.mname.node_id; *)
171
      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
172
      
173
      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
174
      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
175
      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
176
	(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) input_vars
177
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
178
	(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) (m.mstep.step_inputs);
179

  
180
      fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
181
	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars
182
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
183
	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
184

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

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

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

  
207
      let arrow_vars = arrow_vars machines m in
208
      let arrow_vars_curr = rename_current_list arrow_vars and
209
          arrow_vars_mid = rename_mid_list arrow_vars and
210
	  arrow_vars_next = rename_next_list arrow_vars
211
      in
212
      Utils.fprintf_list ~sep:"@ "
213
      	(fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
214
      	fmt (arrow_vars_curr@arrow_vars_mid@arrow_vars_next);
215
      fprintf fmt "@]@ </Node>";
216
     )) (List.rev machines);
160
         let pp_var = pp_horn_var m in
161
         let memories_old = memories_old machines m in
162
         let memories_next = memories_next machines m in
163

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

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

  
182
         fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
183
           (Utils.fprintf_list ~sep:" | " pp_var)
184
           output_vars
185
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
186
                pp_type fmt id.var_type))
187
           output_vars
188
           (Utils.fprintf_list ~sep:" | " pp_var)
189
           m.mstep.step_outputs;
190

  
191
         let local_vars =
192
           try full_memory_vars ~without_arrow:true machines m
193
           with Not_found ->
194
             Format.eprintf "machine %s@.@?" m.mname.node_id;
195
             assert false
196
         in
197
         let init_local_vars = rename_next_list local_vars in
198
         let step_local_vars = rename_current_list local_vars in
199

  
200
         fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ "
201
           (Utils.fprintf_list ~sep:" | " pp_var)
202
           init_local_vars
203
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
204
                pp_type fmt id.var_type))
205
           init_local_vars
206
           (fun fmt ->
207
             match memories_next with [] -> () | _ -> fprintf fmt "")
208
           (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
209
                fprintf fmt "%a" pp_xml_expr ee))
210
           memories_next;
211

  
212
         fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
213
           (Utils.fprintf_list ~sep:" | " pp_var)
214
           step_local_vars
215
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
216
                pp_type fmt id.var_type))
217
           step_local_vars
218
           (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
219
           (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
220
                fprintf fmt "(%a)" pp_xml_expr ee))
221
           memories_old;
222

  
223
         let arrow_vars = arrow_vars machines m in
224
         let arrow_vars_curr = rename_current_list arrow_vars
225
         and arrow_vars_mid = rename_mid_list arrow_vars
226
         and arrow_vars_next = rename_next_list arrow_vars in
227
         Utils.fprintf_list ~sep:"@ "
228
           (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
229
           fmt
230
           (arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next);
231
         fprintf fmt "@]@ </Node>"))
232
    (List.rev machines);
217 233
  fprintf fmt "</Traces>@."
218
  
219 234

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

  
226

  
227 240
(* Local Variables: *)
228 241
(* compile-command:"make -C ../.." *)
229 242
(* End: *)

Also available in: Unified diff