1
|
open Lustre_types
|
2
|
open Machine_code_types
|
3
|
open Corelang
|
4
|
|
5
|
let print_statelocaltag = true
|
6
|
|
7
|
let rec pp_val fmt v =
|
8
|
match v.value_desc with
|
9
|
| Cst c -> Printers.pp_const fmt c
|
10
|
| LocalVar v ->
|
11
|
if print_statelocaltag then
|
12
|
Format.fprintf fmt "%s(L)" v.var_id
|
13
|
else
|
14
|
Format.pp_print_string fmt v.var_id
|
15
|
|
16
|
| StateVar v ->
|
17
|
if print_statelocaltag then
|
18
|
Format.fprintf fmt "%s(S)" v.var_id
|
19
|
else
|
20
|
Format.pp_print_string fmt v.var_id
|
21
|
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
|
22
|
| Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
|
23
|
| Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
|
24
|
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
|
25
|
|
26
|
let rec pp_instr fmt i =
|
27
|
let _ =
|
28
|
match i.instr_desc with
|
29
|
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
|
30
|
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
|
31
|
| MReset i -> Format.fprintf fmt "reset %s" i
|
32
|
| MNoReset i -> Format.fprintf fmt "noreset %s" i
|
33
|
| MStep (il, i, vl) ->
|
34
|
Format.fprintf fmt "%a = %s (%a)"
|
35
|
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
|
36
|
i
|
37
|
(Utils.fprintf_list ~sep:", " pp_val) vl
|
38
|
| MBranch (g,hl) ->
|
39
|
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
|
40
|
pp_val g
|
41
|
(Utils.fprintf_list ~sep:"@," pp_branch) hl
|
42
|
| MComment s -> Format.pp_print_string fmt s
|
43
|
|
44
|
in
|
45
|
(* Annotation *)
|
46
|
(* let _ = *)
|
47
|
(* match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
|
48
|
(* in *)
|
49
|
let _ =
|
50
|
match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
|
51
|
in
|
52
|
()
|
53
|
|
54
|
and pp_branch fmt (t, h) =
|
55
|
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
|
56
|
|
57
|
and pp_instrs fmt il =
|
58
|
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il
|
59
|
|
60
|
|
61
|
(* merge log: get_node_def was in c0f8 *)
|
62
|
(* Returns the node/machine associated to id in m calls *)
|
63
|
let get_node_def id m =
|
64
|
try
|
65
|
let (decl, _) = List.assoc id m.mcalls in
|
66
|
Corelang.node_of_top decl
|
67
|
with Not_found -> (
|
68
|
(* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)
|
69
|
(* id *)
|
70
|
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *)
|
71
|
(* ; *)
|
72
|
raise Not_found
|
73
|
)
|
74
|
|
75
|
(* merge log: machine_vars was in 44686 *)
|
76
|
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
|
77
|
|
78
|
let pp_step fmt s =
|
79
|
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
|
80
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
|
81
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
|
82
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
|
83
|
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks
|
84
|
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs
|
85
|
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts
|
86
|
|
87
|
|
88
|
let pp_static_call fmt (node, args) =
|
89
|
Format.fprintf fmt "%s<%a>"
|
90
|
(node_name node)
|
91
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
|
92
|
|
93
|
let pp_machine fmt m =
|
94
|
Format.fprintf fmt
|
95
|
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "
|
96
|
m.mname.node_id
|
97
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
|
98
|
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
|
99
|
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
|
100
|
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst
|
101
|
pp_step m.mstep
|
102
|
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
|
103
|
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
|
104
|
|
105
|
let pp_machines fmt ml =
|
106
|
Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
|
107
|
|
108
|
|
109
|
let rec is_const_value v =
|
110
|
match v.value_desc with
|
111
|
| Cst _ -> true
|
112
|
| Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
|
113
|
| _ -> false
|
114
|
|
115
|
(* Returns the declared stateless status and the computed one. *)
|
116
|
let get_stateless_status m =
|
117
|
(m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
|
118
|
|
119
|
let is_input m id =
|
120
|
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
|
121
|
|
122
|
let is_output m id =
|
123
|
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
|
124
|
|
125
|
let is_memory m id =
|
126
|
List.exists (fun o -> o.var_id = id.var_id) m.mmemory
|
127
|
|
128
|
let mk_conditional ?lustre_eq c t e =
|
129
|
mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
|
130
|
|
131
|
|
132
|
|
133
|
let mk_val v t =
|
134
|
{ value_desc = v;
|
135
|
value_type = t;
|
136
|
value_annot = None }
|
137
|
|
138
|
let arrow_machine =
|
139
|
let state = "_first" in
|
140
|
let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
|
141
|
let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
|
142
|
let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
|
143
|
let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
|
144
|
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
|
145
|
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *)
|
146
|
{
|
147
|
mname = Arrow.arrow_desc;
|
148
|
mmemory = [var_state];
|
149
|
mcalls = [];
|
150
|
minstances = [];
|
151
|
minit = [mkinstr (MStateAssign(var_state, cst true))];
|
152
|
mstatic = [];
|
153
|
mconst = [];
|
154
|
mstep = {
|
155
|
step_inputs = Arrow.arrow_desc.node_inputs;
|
156
|
step_outputs = Arrow.arrow_desc.node_outputs;
|
157
|
step_locals = [];
|
158
|
step_checks = [];
|
159
|
step_instrs = [mk_conditional (mk_val (StateVar var_state) Type_predef.type_bool)
|
160
|
(List.map mkinstr
|
161
|
[MStateAssign(var_state, cst false);
|
162
|
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)])
|
163
|
(List.map mkinstr
|
164
|
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ];
|
165
|
step_asserts = [];
|
166
|
};
|
167
|
mspec = None;
|
168
|
mannot = [];
|
169
|
}
|
170
|
|
171
|
let empty_desc =
|
172
|
{
|
173
|
node_id = Arrow.arrow_id;
|
174
|
node_type = Types.bottom;
|
175
|
node_clock = Clocks.bottom;
|
176
|
node_inputs= [];
|
177
|
node_outputs= [];
|
178
|
node_locals= [];
|
179
|
node_gencalls = [];
|
180
|
node_checks = [];
|
181
|
node_asserts = [];
|
182
|
node_stmts= [];
|
183
|
node_dec_stateless = true;
|
184
|
node_stateless = Some true;
|
185
|
node_spec = None;
|
186
|
node_annot = []; }
|
187
|
|
188
|
let empty_machine =
|
189
|
{
|
190
|
mname = empty_desc;
|
191
|
mmemory = [];
|
192
|
mcalls = [];
|
193
|
minstances = [];
|
194
|
minit = [];
|
195
|
mstatic = [];
|
196
|
mconst = [];
|
197
|
mstep = {
|
198
|
step_inputs = [];
|
199
|
step_outputs = [];
|
200
|
step_locals = [];
|
201
|
step_checks = [];
|
202
|
step_instrs = [];
|
203
|
step_asserts = [];
|
204
|
};
|
205
|
mspec = None;
|
206
|
mannot = [];
|
207
|
}
|
208
|
|
209
|
let new_instance =
|
210
|
let cpt = ref (-1) in
|
211
|
fun caller callee tag ->
|
212
|
begin
|
213
|
let o =
|
214
|
if Stateless.check_node callee then
|
215
|
node_name callee
|
216
|
else
|
217
|
Printf.sprintf "ni_%d" (incr cpt; !cpt) in
|
218
|
let o =
|
219
|
if !Options.ansi && is_generic_node callee
|
220
|
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls)
|
221
|
else o in
|
222
|
o
|
223
|
end
|
224
|
|
225
|
|
226
|
let get_machine_opt name machines =
|
227
|
List.fold_left
|
228
|
(fun res m ->
|
229
|
match res with
|
230
|
| Some _ -> res
|
231
|
| None -> if m.mname.node_id = name then Some m else None)
|
232
|
None machines
|
233
|
|
234
|
let get_const_assign m id =
|
235
|
try
|
236
|
match get_instr_desc (List.find
|
237
|
(fun instr -> match get_instr_desc instr with
|
238
|
| MLocalAssign (v, _) -> v == id
|
239
|
| _ -> false)
|
240
|
m.mconst
|
241
|
) with
|
242
|
| MLocalAssign (_, e) -> e
|
243
|
| _ -> assert false
|
244
|
with Not_found -> assert false
|
245
|
|
246
|
|
247
|
let value_of_ident loc m id =
|
248
|
(* is is a state var *)
|
249
|
try
|
250
|
let v = List.find (fun v -> v.var_id = id) m.mmemory
|
251
|
in mk_val (StateVar v) v.var_type
|
252
|
with Not_found ->
|
253
|
try (* id is a node var *)
|
254
|
let v = get_node_var id m.mname
|
255
|
in mk_val (LocalVar v) v.var_type
|
256
|
with Not_found ->
|
257
|
try (* id is a constant *)
|
258
|
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
|
259
|
in mk_val (LocalVar c) c.var_type
|
260
|
with Not_found ->
|
261
|
(* id is a tag *)
|
262
|
let t = Const_tag id
|
263
|
in mk_val (Cst t) (Typing.type_const loc t)
|
264
|
|
265
|
(* type of internal fun used in dimension expression *)
|
266
|
let type_of_value_appl f args =
|
267
|
if List.mem f Basic_library.arith_funs
|
268
|
then (List.hd args).value_type
|
269
|
else Type_predef.type_bool
|
270
|
|
271
|
let rec value_of_dimension m dim =
|
272
|
match dim.Dimension.dim_desc with
|
273
|
| Dimension.Dbool b ->
|
274
|
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool
|
275
|
| Dimension.Dint i ->
|
276
|
mk_val (Cst (Const_int i)) Type_predef.type_int
|
277
|
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v
|
278
|
| Dimension.Dappl (f, args) ->
|
279
|
let vargs = List.map (value_of_dimension m) args
|
280
|
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
|
281
|
| Dimension.Dite (i, t, e) ->
|
282
|
(match List.map (value_of_dimension m) [i; t; e] with
|
283
|
| [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
|
284
|
| _ -> assert false)
|
285
|
| Dimension.Dlink dim' -> value_of_dimension m dim'
|
286
|
| _ -> assert false
|
287
|
|
288
|
let rec dimension_of_value value =
|
289
|
match value.value_desc with
|
290
|
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true
|
291
|
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false
|
292
|
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i
|
293
|
| LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id
|
294
|
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
|
295
|
| _ -> assert false
|
296
|
|
297
|
|
298
|
let rec join_branches hl1 hl2 =
|
299
|
match hl1, hl2 with
|
300
|
| [] , _ -> hl2
|
301
|
| _ , [] -> hl1
|
302
|
| (t1, h1)::q1, (t2, h2)::q2 ->
|
303
|
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
|
304
|
if t1 > t2 then (t2, h2) :: join_branches hl1 q2
|
305
|
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
|
306
|
|
307
|
and join_guards inst1 insts2 =
|
308
|
match get_instr_desc inst1, List.map get_instr_desc insts2 with
|
309
|
| _ , [] ->
|
310
|
[inst1]
|
311
|
| MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 ->
|
312
|
mkinstr
|
313
|
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
|
314
|
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
|
315
|
:: (List.tl insts2)
|
316
|
| _ -> inst1 :: insts2
|
317
|
|
318
|
let join_guards_list insts =
|
319
|
List.fold_right join_guards insts []
|