Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_traces.ml @ e4edf171

History | View | Annotate | Download (6.62 KB)

1 fea041c5 xthirioux
(********************************************************************)
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
18
open Format
19 8446bf03 ploc
open Lustre_types
20 fea041c5 xthirioux
open Corelang
21 089f94be ploc
open Machine_code_types
22 fea041c5 xthirioux
23
open Horn_backend_common
24
open Horn_backend_printers
25
26
(* Compute memories associated to each machine *)
27
let compute_mems machines m =
28
  let rec aux fst prefix m =
29
    (List.map (fun mem -> (prefix, mem)) m.mmemory) @
30
      List.fold_left (fun accu (id, (n, _)) ->
31
	let name = node_name n in
32
	if name = "_arrow" then accu else
33
	  let machine_n = get_machine machines name in
34
	  ( aux false ((id,machine_n)::prefix) machine_n )
35
	  @ accu
36
      ) [] m.minstances
37
  in
38
  aux true [] m
39
40
41
(* We extract the annotation dealing with traceability *)
42
let machines_traces machines = 
43
  List.map (fun m ->
44
    let traces : (ident * expr) list=
45
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
46
      let filtered =
47
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
48
      in
49
      let content = List.map snd filtered in
50
      (* Elements are supposed to be a pair (tuple): variable, expression *)
51
      List.map (fun ee ->
52
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
53
	| [], Expr_tuple [v;e] -> (
54
	  match v.expr_desc with
55
	  | Expr_ident vid -> vid, e
56
	  | _ -> assert false )
57
	| _ -> assert false)
58
	content
59
    in
60
61
    m, traces
62
63
  ) machines
64
  
65
let memories_old machines m =
66
  List.map (fun (p, v) ->
67
    let machine = match p with | [] -> m | (_,m')::_ -> m' in
68
    let traces = List.assoc machine (machines_traces machines) in
69
    if List.mem_assoc v.var_id traces then 
70
      (
71
	(* We take the expression associated to variable v in the trace
72
	   info *)
73
74
	(* eprintf "Found variable %a in traces: %a@."  pp_var v
75
	   Printers.pp_expr (List.assoc v.var_id traces); *)
76
	p, List.assoc v.var_id traces
77
      )
78
    else 
79
      begin
80
81
	(* We keep the variable as is: we create an expression v *)
82
83
	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
84
	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
85
	   traces); *)	    
86
87
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
88
      end
89
90
  ) (compute_mems machines m)
91
      
92
let memories_next  machines m = (* We remove the topest pre in each expression *)
93
  List.map
94
    (fun (prefix, ee) ->
95
      match ee.expr_desc with
96
      | Expr_pre e -> prefix, e
97
      | _ -> eprintf
98
      	"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
99
      	(Utils.fprintf_list ~sep:","
100
      	   (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
101
      	(List.rev prefix)
102
      	Printers.pp_expr ee;
103
      	assert false)
104
    (memories_old machines m)
105
      
106
107
108
let pp_prefix_rev fmt prefix =
109
  Utils.fprintf_list ~sep:"." 
110
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) 
111
    fmt 
112
    (List.rev prefix)
113
      
114
115
let traces_file fmt basename prog machines =
116
  fprintf fmt "<?xml version=\"1.0\"?>@.";
117
  fprintf fmt "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
118
  fprintf fmt "@[<v 5>@ %a@ @]@."
119
    (Utils.fprintf_list ~sep:"@ " (fun fmt m ->
120
      let pp_var = pp_horn_var m in
121
      let memories_old = memories_old  machines m in
122
      let memories_next = memories_next  machines m in
123
      
124
      (* fprintf fmt "; Node %s@." m.mname.node_id; *)
125
      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
126
      
127
      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
128
      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
129
      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
130
	(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) input_vars
131
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
132
	(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) (m.mstep.step_inputs);
133
134
      fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
135
	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars
136
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
137
	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
138
139 d7e04983 Ploc
      let local_vars =
140
	(try
141
	   full_memory_vars ~without_arrow:true machines m
142
	 with Not_found -> Format.eprintf "machine %s@.@?" m.mname.node_id; assert false
143
	)
144 fea041c5 xthirioux
      in
145 d7e04983 Ploc
      let init_local_vars = rename_next_list local_vars in
146
      let step_local_vars = rename_current_list local_vars in
147 fea041c5 xthirioux
148
      fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ "
149
	(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
150
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
151
	(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
152 397d5ae3 ploc
	(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" pp_xml_expr ee)) memories_next;
153 fea041c5 xthirioux
154
      fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
155
	(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
156
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
157
	(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
158
	(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
159 397d5ae3 ploc
          pp_xml_expr ee)) (memories_old);
160 fea041c5 xthirioux
161 d7e04983 Ploc
      let arrow_vars = arrow_vars machines m in
162 92ff8f1b Teme
      let arrow_vars_curr = rename_current_list arrow_vars and
163
          arrow_vars_mid = rename_mid_list arrow_vars and
164 d7e04983 Ploc
	  arrow_vars_next = rename_next_list arrow_vars
165
      in
166
      Utils.fprintf_list ~sep:"@ "
167
      	(fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
168 92ff8f1b Teme
      	fmt (arrow_vars_curr@arrow_vars_mid@arrow_vars_next);
169 fea041c5 xthirioux
      fprintf fmt "@]@ </Node>";
170
     )) (List.rev machines);
171
  fprintf fmt "</Traces>@."
172
  
173
174
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt
175
   "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
176
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt
177
   "%a(%a)" *)
178
(* pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
179
180
181
(* Local Variables: *)
182
(* compile-command:"make -C ../.." *)
183
(* End: *)