1
|
(* EMF backend *)
|
2
|
(* This backup is initially motivated by the need to express Spacer computed
|
3
|
invariants as Matlab Simulink executable evidences.
|
4
|
|
5
|
Therefore the input language is more restricted. We do not expect fancy
|
6
|
datastructure, complex function calls, etc.
|
7
|
|
8
|
In case of error, use -node foo -inline to eliminate function calls that are
|
9
|
not seriously handled yet.
|
10
|
|
11
|
|
12
|
In terms of algorithm, the process was initially based on printing normalized
|
13
|
code. We now rely on machine code printing. The old code is available in old
|
14
|
commits (eg in dd71e482a9d0).
|
15
|
|
16
|
|
17
|
A (normalized) node becomes a JSON struct
|
18
|
node foo (in1, in2: int) returns (out1, out2: int);
|
19
|
var x : int;
|
20
|
let
|
21
|
x = bar(in1, in2); -- a stateful node
|
22
|
out1 = x;
|
23
|
out2 = in2;
|
24
|
tel
|
25
|
|
26
|
Since foo contains a stateful node, it is stateful itself. Its prototype is
|
27
|
extended with a reset input. When the node is reset, each of its "pre" expression
|
28
|
is reset as well as all calls to stateful node it contains.
|
29
|
|
30
|
will produce the following JSON struct:
|
31
|
"foo": {"kind": "stateful",
|
32
|
inputs: [{name: "in1", type: "int"},
|
33
|
{name: "in2", type: "int"},
|
34
|
],
|
35
|
outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],
|
36
|
locals: [{name: "x", type: "int"}],
|
37
|
instrs: {
|
38
|
def_x: { lhs: ["x"],
|
39
|
rhs: {type: "statefulcall", name: "bar",
|
40
|
args: [in1, in2], reset: [ni4_reset] }
|
41
|
}
|
42
|
|
43
|
def_out1: { lhs: "out1", rhs: "x" } ,
|
44
|
def_out2: { lhs: "out2", rhs: "in2"}
|
45
|
}
|
46
|
}
|
47
|
|
48
|
Basically we have the following different definitions
|
49
|
1. local assign of a variable to another one:
|
50
|
def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" },
|
51
|
|
52
|
2. pre construct over a variable (this is a state assign):
|
53
|
def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" },
|
54
|
|
55
|
3. arrow constructs, while there is not specific input, it could be reset
|
56
|
by a specific signal. We register it as a fresh rhs var:
|
57
|
def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"}
|
58
|
|
59
|
2. call to a stateless function, typically an operator
|
60
|
def_x: { kind: "statelesscall", lhs: ["x"],
|
61
|
name: "bar", rhs: [in1, in2]}
|
62
|
|
63
|
or in the operator version
|
64
|
def_x: { kind: "operator", lhs: ["x"],
|
65
|
name: "+", rhs: [in1, in2]}
|
66
|
|
67
|
|
68
|
In Simulink this should introduce a subsystem in the first case or a
|
69
|
regular block in the second with card(lhs) outputs and card{args} inputs.
|
70
|
|
71
|
3. call to a stateful node. It is similar to the stateless above,
|
72
|
with the addition of the reset argument
|
73
|
{ def_x: { kind: "statefulcall", lhs: ["x"],
|
74
|
name: "bar", rhs: [in1, in2], reset: [ni4_reset] }
|
75
|
}
|
76
|
|
77
|
In lustrec compilation phases, a unique id is associated to this specific
|
78
|
instance of stateful node "bar", here ni4.
|
79
|
Instruction such as reset(ni4) or noreset(ni4) may -- or not -- reset this
|
80
|
specific node. This corresponds to "every c" suffix of a node call in lustre.
|
81
|
|
82
|
In Simulink this should introduce a subsystem that has this extra reset input.
|
83
|
The reset should be defined as an "OR" over (1) the input reset of the parent
|
84
|
node, __reset in the present example and (2) any occurence of reset(ni4) in
|
85
|
the instructions.
|
86
|
|
87
|
4. branching construct: (guard expr, (tag, instr list) list)
|
88
|
"merge_XX": { type: "branch", guard: "var_guard",
|
89
|
inputs: ["varx", "vary"],
|
90
|
outputs: ["vark", "varz"],
|
91
|
branches: {"tag1": {liste_of_definitions (1-4)}, ...}
|
92
|
}
|
93
|
|
94
|
|
95
|
In Simulink, this should become one IF block to produce enable ports
|
96
|
"var_guard == tag1", "var_guard == tag2", .... as well as one action
|
97
|
block per branch: each of these action block shall
|
98
|
|
99
|
*)
|
100
|
|
101
|
open Utils
|
102
|
open Lustre_types
|
103
|
open Corelang
|
104
|
open Machine_code_types
|
105
|
open Machine_code_common
|
106
|
open Format
|
107
|
open EMF_common
|
108
|
|
109
|
module ISet = Utils.ISet
|
110
|
|
111
|
(* XXX: UNUSED *)
|
112
|
(* exception Unhandled of string *)
|
113
|
|
114
|
(**********************************************)
|
115
|
(* Utility functions: arrow and lustre expr *)
|
116
|
(**********************************************)
|
117
|
|
118
|
(* detect whether the instruction i represents an ARROW, ie an arrow with true
|
119
|
-> false *)
|
120
|
let is_arrow_fun m i =
|
121
|
match Corelang.get_instr_desc i with
|
122
|
| MStep ([ _ ], i, vl) -> (
|
123
|
try
|
124
|
let name = (get_node_def i m).node_id in
|
125
|
match name, vl with
|
126
|
| "_arrow", [ v1; v2 ] -> (
|
127
|
match v1.value_desc, v2.value_desc with
|
128
|
| Cst c1, Cst c2 ->
|
129
|
if
|
130
|
c1 = Corelang.const_of_bool true
|
131
|
&& c2 = Corelang.const_of_bool false
|
132
|
then true
|
133
|
else assert false
|
134
|
(* only handle true -> false *)
|
135
|
| _ -> assert false)
|
136
|
| _ -> false
|
137
|
with Not_found ->
|
138
|
false
|
139
|
(* Not declared (should have been detected now, or
|
140
|
imported node) *))
|
141
|
| _ -> false
|
142
|
|
143
|
let is_resetable_fun lustre_eq =
|
144
|
(* We extract the clock if it exist from the original lustre equation *)
|
145
|
match lustre_eq with
|
146
|
| Some eq -> (
|
147
|
match eq.eq_rhs.expr_desc with
|
148
|
| Expr_appl (_, _, reset) -> (
|
149
|
match reset with None -> false | Some _ -> true)
|
150
|
| Expr_arrow _ -> true
|
151
|
| _ ->
|
152
|
Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs;
|
153
|
assert false)
|
154
|
| None -> assert false
|
155
|
(* should have been assigned to an original lustre equation *)
|
156
|
|
157
|
(**********************************************)
|
158
|
(* Printing machine code as EMF *)
|
159
|
(**********************************************)
|
160
|
|
161
|
let branch_cpt = ref 0
|
162
|
|
163
|
let get_instr_id fmt i =
|
164
|
match Corelang.get_instr_desc i with
|
165
|
| MLocalAssign (lhs, _) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
|
166
|
| MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
|
167
|
(* TODO: handle clear_reset *)
|
168
|
| MClearReset -> ()
|
169
|
| MBranch _ ->
|
170
|
incr branch_cpt;
|
171
|
fprintf fmt "branch_%i" !branch_cpt
|
172
|
| MStep (outs, id, _) ->
|
173
|
pp_protect fmt (fun fmt ->
|
174
|
fprintf fmt "%a_%s" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "_")
|
175
|
pp_var_name) outs id)
|
176
|
| _ -> ()
|
177
|
(* No name *)
|
178
|
|
179
|
let rec branch_block_vars m il =
|
180
|
List.fold_left
|
181
|
(fun (accu_all_def, accu_def, accu_read) i ->
|
182
|
let all_defined_vars, common_def_vars, read_vars =
|
183
|
branch_instr_vars m i
|
184
|
in
|
185
|
( ISet.union accu_all_def all_defined_vars,
|
186
|
ISet.union accu_def common_def_vars,
|
187
|
VSet.union accu_read read_vars ))
|
188
|
(ISet.empty, ISet.empty, VSet.empty)
|
189
|
il
|
190
|
|
191
|
and branch_instr_vars m i =
|
192
|
(* Returns all_outputs, outputs, inputs of the instruction. It is
|
193
|
only called on MBranch instructions but evaluate recursively
|
194
|
instructions appearing in branches.
|
195
|
|
196
|
It is used to gather the global input/output of a switch and
|
197
|
print it at the begin of the JSON subtree.
|
198
|
|
199
|
The set "All outputs" is used to filter out input variables
|
200
|
belong to that set. *)
|
201
|
match Corelang.get_instr_desc i with
|
202
|
| MLocalAssign (var, expr) | MStateAssign (var, expr) ->
|
203
|
ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
|
204
|
| MStep (vars, f, args) ->
|
205
|
let is_stateful = List.mem_assoc f m.minstances in
|
206
|
let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
|
207
|
let args_vars =
|
208
|
List.fold_left
|
209
|
(fun accu v -> VSet.union accu (get_expr_vars v))
|
210
|
VSet.empty args
|
211
|
in
|
212
|
|
213
|
( lhs,
|
214
|
lhs,
|
215
|
if is_stateful && is_resetable_fun i.lustre_eq then
|
216
|
let reset_var =
|
217
|
let loc = Location.dummy in
|
218
|
Corelang.mkvar_decl loc
|
219
|
( reset_name f,
|
220
|
Corelang.mktyp loc Tydec_bool,
|
221
|
Corelang.mkclock loc Ckdec_any,
|
222
|
false,
|
223
|
None,
|
224
|
None )
|
225
|
in
|
226
|
VSet.add reset_var args_vars
|
227
|
else args_vars )
|
228
|
| MBranch (g, (_, hd_il) :: tl) ->
|
229
|
(* We focus on variables defined in all branches *)
|
230
|
let read_guard = get_expr_vars g in
|
231
|
(* Bootstrapping with first item *)
|
232
|
let all_def_vars_hd, def_vars_hd, read_vars_hd =
|
233
|
branch_block_vars m hd_il
|
234
|
in
|
235
|
let all_def_vars, def_vars, read_vars =
|
236
|
List.fold_left
|
237
|
(fun (all_def_vars, def_vars, read_vars) (_, il) ->
|
238
|
(* We accumulate reads but intersect writes *)
|
239
|
let all_writes_il, writes_il, reads_il = branch_block_vars m il in
|
240
|
( ISet.union all_def_vars all_writes_il,
|
241
|
ISet.inter def_vars writes_il,
|
242
|
VSet.union read_vars reads_il ))
|
243
|
(all_def_vars_hd, def_vars_hd, read_vars_hd)
|
244
|
tl
|
245
|
in
|
246
|
|
247
|
(* all_def_vars correspond to variables written or defined in one
|
248
|
of the branch. It may happen that a variable is defined in one
|
249
|
but not in the other, because of reset for example.
|
250
|
|
251
|
def_vars are variables defined in all branches. *)
|
252
|
all_def_vars, def_vars, VSet.union read_guard read_vars
|
253
|
| MBranch _ ->
|
254
|
assert false (* branch instruction should admit at least one case *)
|
255
|
| MSetReset ni | MNoReset ni ->
|
256
|
let write = ISet.singleton (reset_name ni) in
|
257
|
write, write, VSet.empty
|
258
|
(* TODO: handle clear_reset and reset flag *)
|
259
|
| MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty
|
260
|
| MSpec _ | MComment _ -> assert false
|
261
|
(* not available for EMF output *)
|
262
|
|
263
|
(* XXX: UNUSED *)
|
264
|
(* A kind of super join_guards: all MBranch are postponed and sorted by
|
265
|
guards so they can be easier merged *)
|
266
|
(* let merge_branches instrs =
|
267
|
* let instrs, branches =
|
268
|
* List.fold_right
|
269
|
* (fun i (il, branches) ->
|
270
|
* match Corelang.get_instr_desc i with
|
271
|
* | MBranch _ -> il, i :: branches
|
272
|
* | _ -> i :: il, branches)
|
273
|
* instrs ([], [])
|
274
|
* in
|
275
|
* let sorting_branches b1 b2 =
|
276
|
* match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
|
277
|
* | MBranch (g1, _), MBranch (g2, _) -> compare g1 g2
|
278
|
* | _ -> assert false
|
279
|
* in
|
280
|
* let sorted_branches = List.sort sorting_branches branches in
|
281
|
* instrs @ join_guards_list sorted_branches *)
|
282
|
|
283
|
let rec pp_emf_instr m fmt i =
|
284
|
let pp_content fmt i =
|
285
|
match Corelang.get_instr_desc i with
|
286
|
| MLocalAssign (lhs, expr) -> (
|
287
|
match expr.value_desc with
|
288
|
| Fun (fun_id, vl) ->
|
289
|
(*
|
290
|
Thanks to normalization, vl shall only contain constant or
|
291
|
local/state vars but not calls to other functions *)
|
292
|
fprintf fmt "\"kind\": \"operator\",@ ";
|
293
|
fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
|
294
|
fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" fun_id
|
295
|
(pp_emf_cst_or_var_list m) vl
|
296
|
| Array _ | Access _ | Power _ | Cst _ | Var _ ->
|
297
|
fprintf fmt
|
298
|
"\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
|
299
|
pp_var_name lhs (pp_emf_cst_or_var m) expr
|
300
|
| ResetFlag ->
|
301
|
(* TODO: handle reset flag *)
|
302
|
assert false)
|
303
|
| MStateAssign (lhs, expr)
|
304
|
(* a Pre construct Shall only be defined by a
|
305
|
variable or a constant, no function anymore! *) ->
|
306
|
fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
|
307
|
pp_var_name lhs (pp_emf_cst_or_var m) expr
|
308
|
| MSetReset id ->
|
309
|
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
|
310
|
(reset_name id)
|
311
|
| MNoReset id ->
|
312
|
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
|
313
|
(reset_name id)
|
314
|
(* TODO: handle clear_reset and reset flag *)
|
315
|
| MClearReset | MResetAssign _ -> ()
|
316
|
| MBranch (g, hl) ->
|
317
|
let all_outputs, outputs, inputs = branch_instr_vars m i in
|
318
|
|
319
|
(* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
|
320
|
(* Machine_code.pp_instr i *)
|
321
|
(* (fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
|
322
|
(* (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
|
323
|
(* pp_emf_vars_decl *)
|
324
|
(* (VSet.elements inputs) *)
|
325
|
|
326
|
(* ; *)
|
327
|
let inputs =
|
328
|
VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs
|
329
|
in
|
330
|
|
331
|
(* Format.eprintf "Filtering in: %a@.@." *)
|
332
|
(* pp_emf_vars_decl *)
|
333
|
(* (VSet.elements inputs) *)
|
334
|
|
335
|
(* ; *)
|
336
|
fprintf fmt "\"kind\": \"branch\",@ ";
|
337
|
fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g;
|
338
|
(* it has to be a variable or a constant *)
|
339
|
fprintf fmt "\"outputs\": [%a],@ "
|
340
|
(pp_comma_list pp_var_string)
|
341
|
(ISet.elements outputs);
|
342
|
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
|
343
|
(*
|
344
|
(let guard_inputs = get_expr_vars g in
|
345
|
VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
|
346
|
remove guard's variable from inputs *)
|
347
|
(VSet.elements inputs);
|
348
|
fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
|
349
|
(pp_comma_list (fun fmt (tag, instrs_tag) ->
|
350
|
let branch_all_lhs, _, branch_inputs =
|
351
|
branch_block_vars m instrs_tag
|
352
|
in
|
353
|
let branch_inputs =
|
354
|
VSet.filter
|
355
|
(fun v -> not (ISet.mem v.var_id branch_all_lhs))
|
356
|
branch_inputs
|
357
|
in
|
358
|
fprintf fmt "@[<v 2>\"%a\": {@ " pp_protect (fun fmt ->
|
359
|
Format.pp_print_string fmt tag);
|
360
|
fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag;
|
361
|
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
|
362
|
(VSet.elements branch_inputs);
|
363
|
fprintf fmt "@[<v 2>\"instrs\": {@ ";
|
364
|
(pp_emf_instrs m) fmt instrs_tag;
|
365
|
fprintf fmt "@]@ }";
|
366
|
fprintf fmt "@]@ }"))
|
367
|
hl
|
368
|
| MStep ([ var ], f, _) when is_arrow_fun m i ->
|
369
|
(* Arrow case *)
|
370
|
fprintf fmt
|
371
|
"\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \
|
372
|
\"%s\""
|
373
|
f pp_var_name var (reset_name f)
|
374
|
| MStep (outputs, f, inputs) when not (is_imported_node f m) ->
|
375
|
let node_f = get_node_def f m in
|
376
|
let is_stateful = List.mem_assoc f m.minstances in
|
377
|
fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
|
378
|
(if is_stateful then "statefulcall" else "statelesscall")
|
379
|
pp_protect
|
380
|
(fun fmt -> pp_print_string fmt node_f.node_id)
|
381
|
f;
|
382
|
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
|
383
|
(pp_comma_list (fun fmt v ->
|
384
|
fprintf fmt "\"%a\"" pp_var_name v))
|
385
|
outputs (pp_emf_cst_or_var_list m) inputs;
|
386
|
if is_stateful then
|
387
|
fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
|
388
|
(reset_name f)
|
389
|
(is_resetable_fun i.lustre_eq)
|
390
|
else fprintf fmt "@ "
|
391
|
| MStep (outputs, f, inputs) ->
|
392
|
(* This is an imported node *)
|
393
|
EMF_library_calls.pp_call fmt m f outputs inputs
|
394
|
| MSpec _ | MComment _ ->
|
395
|
Format.eprintf "unhandled comment in EMF@.@?";
|
396
|
assert false
|
397
|
(* not available for EMF output *)
|
398
|
in
|
399
|
fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
|
400
|
fprintf fmt "%a" pp_content i;
|
401
|
fprintf fmt "@]@]@ }"
|
402
|
|
403
|
and pp_emf_instrs m fmt instrs =
|
404
|
pp_comma_list (pp_emf_instr m) fmt instrs
|
405
|
|
406
|
let pp_emf_annot cpt fmt (key, ee) =
|
407
|
let _ =
|
408
|
fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt
|
409
|
(pp_comma_list (fun fmt s -> fprintf fmt "\"%s\"" s))
|
410
|
key pp_emf_eexpr ee
|
411
|
in
|
412
|
incr cpt
|
413
|
|
414
|
let pp_emf_spec_mode fmt m =
|
415
|
fprintf fmt "{@[";
|
416
|
fprintf fmt "\"mode_id\": \"%s\",@ " m.mode_id;
|
417
|
fprintf fmt "\"ensure\": [%a],@ " pp_emf_eexprs m.ensure;
|
418
|
fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require;
|
419
|
fprintf fmt "@]}"
|
420
|
|
421
|
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
|
422
|
|
423
|
(* XXX: UNUSED *)
|
424
|
(* let pp_emf_spec_import fmt i =
|
425
|
* fprintf fmt "{@[";
|
426
|
* fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid;
|
427
|
* fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs;
|
428
|
* fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs;
|
429
|
* fprintf fmt "@]}"
|
430
|
*
|
431
|
* let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import *)
|
432
|
|
433
|
let pp_emf_spec fmt spec =
|
434
|
fprintf fmt "{ @[<hov 0>";
|
435
|
(* fprintf fmt "\"consts\": [%a],@ "
|
436
|
* pp_emf_consts spec.consts;
|
437
|
* fprintf fmt "\"locals\": [%a],@ "
|
438
|
* pp_emf_vars_decl spec.locals;
|
439
|
* fprintf fmt "\"stmts\": [%a],@ "
|
440
|
* pp_emf_stmts spec.stmts; *)
|
441
|
|
442
|
(* TODO *)
|
443
|
(* fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
|
444
|
* fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
|
445
|
* fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes; *)
|
446
|
|
447
|
(* fprintf fmt "\"imports\": [%a]@ "
|
448
|
* pp_emf_spec_imports spec.imports; *)
|
449
|
fprintf fmt "@] }"
|
450
|
|
451
|
let pp_emf_annots cpt fmt annots =
|
452
|
pp_comma_list (pp_emf_annot cpt) fmt annots.annots
|
453
|
|
454
|
let pp_emf_annots_list cpt fmt annots_list =
|
455
|
pp_comma_list (pp_emf_annots cpt) fmt annots_list
|
456
|
|
457
|
(* let pp_emf_contract fmt nd =
|
458
|
* let c = Printers.node_as_contract nd in
|
459
|
* fprintf fmt "@[<v 2>\"%a\": {@ "
|
460
|
* pp_protect (fun fmt -> pp_print_string fmt nd.node_id);
|
461
|
* fprintf fmt "\"contract\": %a@ "
|
462
|
* pp_emf_spec c;
|
463
|
* fprintf fmt "@]@ }" *)
|
464
|
|
465
|
let pp_machine fmt m =
|
466
|
let instrs =
|
467
|
(*merge_branches*)
|
468
|
m.mstep.step_instrs
|
469
|
in
|
470
|
(* try *)
|
471
|
fprintf fmt "@[<v 2>\"%a\": {@ " pp_protect (fun fmt ->
|
472
|
pp_print_string fmt m.mname.node_id);
|
473
|
(match m.mspec.mnode_spec with
|
474
|
| Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
|
475
|
| _ -> ());
|
476
|
fprintf fmt "\"imported\": \"false\",@ ";
|
477
|
fprintf fmt "\"kind\": %t,@ " (fun fmt ->
|
478
|
if not (snd (get_stateless_status m)) then fprintf fmt "\"stateful\""
|
479
|
else fprintf fmt "\"stateless\"");
|
480
|
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_inputs;
|
481
|
fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_outputs;
|
482
|
fprintf fmt "\"locals\": [%a],@ " pp_emf_vars_decl m.mstep.step_locals;
|
483
|
fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl m.mmemory;
|
484
|
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
|
485
|
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " (pp_emf_instrs m) instrs;
|
486
|
(match m.mspec.mnode_spec with
|
487
|
| None -> ()
|
488
|
| Some (Contract c) ->
|
489
|
(* TODO *)
|
490
|
(* assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []); *)
|
491
|
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
|
492
|
| Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
493
|
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"
|
494
|
(pp_emf_annots_list (ref 0))
|
495
|
m.mannot;
|
496
|
fprintf fmt "@]@ }"
|
497
|
(* XXX: UNUSED *)
|
498
|
(* with Unhandled msg ->
|
499
|
* eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
|
500
|
* m.mname.node_id;
|
501
|
* eprintf "%s@ " msg;
|
502
|
* eprintf "node skipped - no output generated@ @]@." *)
|
503
|
|
504
|
(*let pp_machine fmt m =
|
505
|
match m.mspec with
|
506
|
| None | Some (NodeSpec _) -> pp_machine fmt m
|
507
|
| Some (Contract _) -> pp_emf_contract fmt m
|
508
|
*)
|
509
|
|
510
|
let pp_emf_imported_node fmt top =
|
511
|
let ind = Corelang.imported_node_of_top top in
|
512
|
(* try *)
|
513
|
fprintf fmt "@[<v 2>\"%a\": {@ " pp_protect (fun fmt ->
|
514
|
pp_print_string fmt ind.nodei_id);
|
515
|
fprintf fmt "\"imported\": \"true\",@ ";
|
516
|
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl ind.nodei_inputs;
|
517
|
fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl ind.nodei_outputs;
|
518
|
fprintf fmt "\"original_name\": \"%s\"" ind.nodei_id;
|
519
|
(match ind.nodei_spec with
|
520
|
| None -> fprintf fmt "@ "
|
521
|
| Some (Contract _) -> assert false (* should have been processed *)
|
522
|
| Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
523
|
fprintf fmt "@]@ }"
|
524
|
(* XXX: UNUSED *)
|
525
|
(* with Unhandled msg ->
|
526
|
* eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
|
527
|
* ind.nodei_id;
|
528
|
* eprintf "%s@ " msg;
|
529
|
* eprintf "node skipped - no output generated@ @]@." *)
|
530
|
|
531
|
(****************************************************)
|
532
|
(* Main function: iterates over node and print them *)
|
533
|
(****************************************************)
|
534
|
let pp_meta fmt basename =
|
535
|
fprintf fmt "\"meta\": @[<v 0>{@ ";
|
536
|
Format.pp_comma_list
|
537
|
(fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
|
538
|
fmt
|
539
|
[
|
540
|
"compiler-name", Filename.basename Sys.executable_name;
|
541
|
"compiler-version", Version.number;
|
542
|
"command", String.concat " " (Array.to_list Sys.argv);
|
543
|
"source_file", basename;
|
544
|
];
|
545
|
fprintf fmt "@ @]},@ "
|
546
|
|
547
|
let translate fmt basename prog machines =
|
548
|
(* record_types prog; *)
|
549
|
fprintf fmt "@[<v 0>{@ ";
|
550
|
pp_meta fmt basename;
|
551
|
(* Typedef *)
|
552
|
fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
|
553
|
(pp_emf_list pp_emf_typedef)
|
554
|
(Corelang.get_typedefs prog);
|
555
|
fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
|
556
|
(pp_emf_list pp_emf_top_const)
|
557
|
(Corelang.get_consts prog);
|
558
|
fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
|
559
|
pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
|
560
|
fprintf fmt "}@],@ ";
|
561
|
fprintf fmt "\"nodes\": @[<v 0>{@ ";
|
562
|
(* Previous alternative: mapping normalized lustre to EMF:
|
563
|
pp_comma_list pp_decl fmt prog; *)
|
564
|
pp_emf_list pp_machine fmt machines;
|
565
|
fprintf fmt "}@]@ }";
|
566
|
fprintf fmt "@]@ }"
|
567
|
|
568
|
(* Local Variables: *)
|
569
|
(* compile-command: "make -C ../.." *)
|
570
|
(* End: *)
|