|
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 is defined in Garoche, Gurfinkel, Kahsai,
|
|
13
|
HCSV'14 *)
|
|
14
|
|
|
15
|
open Format
|
|
16
|
open LustreSpec
|
|
17
|
open Corelang
|
|
18
|
open Machine_code
|
|
19
|
|
|
20
|
|
|
21
|
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
|
|
22
|
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
|
|
23
|
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
|
|
24
|
|
|
25
|
let pp_type fmt t =
|
|
26
|
match (Types.repr t).Types.tdesc with
|
|
27
|
| Types.Tbool -> Format.fprintf fmt "Bool"
|
|
28
|
| Types.Tint -> Format.fprintf fmt "Int"
|
|
29
|
| Types.Treal -> Format.fprintf fmt "Real"
|
|
30
|
| Types.Tclock _
|
|
31
|
| Types.Tarray _
|
|
32
|
| Types.Tstatic _
|
|
33
|
| Types.Tconst _
|
|
34
|
| Types.Tarrow _
|
|
35
|
| _ -> Format.eprintf "internal error: pp_type %a@."
|
|
36
|
Types.print_ty t; assert false
|
|
37
|
|
|
38
|
let pp_decl_var fmt id =
|
|
39
|
Format.fprintf fmt "(declare-var %s %a)"
|
|
40
|
id.var_id
|
|
41
|
pp_type id.var_type
|
|
42
|
|
|
43
|
let pp_var fmt id = Format.pp_print_string fmt id.var_id
|
|
44
|
|
|
45
|
|
|
46
|
let pp_conj pp fmt l =
|
|
47
|
match l with
|
|
48
|
[] -> assert false
|
|
49
|
| [x] -> pp fmt x
|
|
50
|
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
|
|
51
|
|
|
52
|
|
|
53
|
|
|
54
|
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
|
|
55
|
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
|
56
|
let rename_machine p = rename (fun n -> concat p n)
|
|
57
|
let rename_machine_list p = List.map (rename_machine p)
|
|
58
|
|
|
59
|
let rename_current = rename (fun n -> n ^ "_c")
|
|
60
|
let rename_current_list = List.map rename_current
|
|
61
|
let rename_next = rename (fun n -> n ^ "_x")
|
|
62
|
let rename_next_list = List.map rename_next
|
|
63
|
|
|
64
|
|
|
65
|
let get_machine machines node_name =
|
|
66
|
List.find (fun m -> m.mname.node_id = node_name) machines
|
|
67
|
|
|
68
|
let full_memory_vars machines machine =
|
|
69
|
let rec aux fst prefix m =
|
|
70
|
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
|
|
71
|
List.fold_left (fun accu (id, (n, _)) ->
|
|
72
|
let name = node_name n in
|
|
73
|
if name = "_arrow" then accu else
|
|
74
|
let machine_n = get_machine machines name in
|
|
75
|
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
|
|
76
|
) [] (m.minstances)
|
|
77
|
in
|
|
78
|
aux true machine.mname.node_id machine
|
|
79
|
|
|
80
|
let stateless_vars machines m =
|
|
81
|
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
|
|
82
|
(rename_machine_list m.mname.node_id m.mstep.step_outputs)
|
|
83
|
|
|
84
|
let step_vars machines m =
|
|
85
|
(stateless_vars machines m)@
|
|
86
|
(rename_current_list (full_memory_vars machines m)) @
|
|
87
|
(rename_next_list (full_memory_vars machines m))
|
|
88
|
|
|
89
|
let init_vars machines m =
|
|
90
|
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
|
|
91
|
|
|
92
|
(********************************************************************************************)
|
|
93
|
(* Instruction Printing functions *)
|
|
94
|
(********************************************************************************************)
|
|
95
|
|
|
96
|
let pp_horn_var m fmt id =
|
|
97
|
if Types.is_array_type id.var_type
|
|
98
|
then
|
|
99
|
assert false (* no arrays in Horn output *)
|
|
100
|
else
|
|
101
|
Format.fprintf fmt "%s" id.var_id
|
|
102
|
|
|
103
|
|
|
104
|
(* Used to print boolean constants *)
|
|
105
|
let pp_horn_tag fmt t =
|
|
106
|
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
|
|
107
|
|
|
108
|
(* Prints a constant value *)
|
|
109
|
let rec pp_horn_const fmt c =
|
|
110
|
match c with
|
|
111
|
| Const_int i -> pp_print_int fmt i
|
|
112
|
| Const_real r -> pp_print_string fmt r
|
|
113
|
| Const_float r -> pp_print_float fmt r
|
|
114
|
| Const_tag t -> pp_horn_tag fmt t
|
|
115
|
| _ -> assert false
|
|
116
|
|
|
117
|
(* Prints a value expression [v], with internal function calls only.
|
|
118
|
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
|
119
|
but an offset suffix may be added for array variables
|
|
120
|
*)
|
|
121
|
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
|
|
122
|
match v with
|
|
123
|
| Cst c -> pp_horn_const fmt c
|
|
124
|
| Array _
|
|
125
|
| Access _ -> assert false (* no arrays *)
|
|
126
|
| Power (v, n) -> assert false
|
|
127
|
| LocalVar v -> pp_var fmt (rename_machine self v)
|
|
128
|
| StateVar v ->
|
|
129
|
if Types.is_array_type v.var_type
|
|
130
|
then assert false
|
|
131
|
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
|
|
132
|
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
|
133
|
|
|
134
|
(* Prints a [value] indexed by the suffix list [loop_vars] *)
|
|
135
|
let rec pp_value_suffix self pp_value fmt value =
|
|
136
|
match value with
|
|
137
|
| Fun (n, vl) ->
|
|
138
|
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
|
|
139
|
| _ ->
|
|
140
|
pp_horn_val self pp_value fmt value
|
|
141
|
|
|
142
|
(* type_directed assignment: array vs. statically sized type
|
|
143
|
- [var_type]: type of variable to be assigned
|
|
144
|
- [var_name]: name of variable to be assigned
|
|
145
|
- [value]: assigned value
|
|
146
|
- [pp_var]: printer for variables
|
|
147
|
*)
|
|
148
|
let pp_assign m self pp_var fmt var_type var_name value =
|
|
149
|
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
|
|
150
|
|
|
151
|
let pp_instance_call
|
|
152
|
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
|
|
153
|
try (* stateful node instance *)
|
|
154
|
begin
|
|
155
|
let (n,_) = List.assoc i m.minstances in
|
|
156
|
match node_name n, inputs, outputs with
|
|
157
|
| "_arrow", [i1; i2], [o] -> begin
|
|
158
|
if init then
|
|
159
|
pp_assign
|
|
160
|
m
|
|
161
|
self
|
|
162
|
(pp_horn_var m)
|
|
163
|
fmt
|
|
164
|
o.var_type (LocalVar o) i1
|
|
165
|
else
|
|
166
|
pp_assign
|
|
167
|
m self (pp_horn_var m) fmt
|
|
168
|
o.var_type (LocalVar o) i2
|
|
169
|
|
|
170
|
end
|
|
171
|
| name, _, _ ->
|
|
172
|
begin
|
|
173
|
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
|
|
174
|
if init then
|
|
175
|
Format.fprintf fmt "(%a %a%t%a%t%a)"
|
|
176
|
pp_machine_init_name (node_name n)
|
|
177
|
(* inputs *)
|
|
178
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
179
|
inputs
|
|
180
|
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
181
|
(* outputs *)
|
|
182
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
183
|
(List.map (fun v -> LocalVar v) outputs)
|
|
184
|
(Utils.pp_final_char_if_non_empty " " outputs)
|
|
185
|
(* memories (next) *)
|
|
186
|
(Utils.fprintf_list ~sep:" " pp_var) (
|
|
187
|
rename_machine_list
|
|
188
|
(concat m.mname.node_id i)
|
|
189
|
(rename_next_list (full_memory_vars machines target_machine)
|
|
190
|
)
|
|
191
|
)
|
|
192
|
else
|
|
193
|
Format.fprintf fmt "(%a %a%t%a%t%a)"
|
|
194
|
pp_machine_step_name (node_name n)
|
|
195
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
|
|
196
|
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
197
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
198
|
(List.map (fun v -> LocalVar v) outputs)
|
|
199
|
(Utils.pp_final_char_if_non_empty " " outputs)
|
|
200
|
(Utils.fprintf_list ~sep:" " pp_var) (
|
|
201
|
(rename_machine_list
|
|
202
|
(concat m.mname.node_id i)
|
|
203
|
(rename_current_list (full_memory_vars machines target_machine))
|
|
204
|
) @
|
|
205
|
(rename_machine_list
|
|
206
|
(concat m.mname.node_id i)
|
|
207
|
(rename_next_list (full_memory_vars machines target_machine))
|
|
208
|
)
|
|
209
|
)
|
|
210
|
|
|
211
|
end
|
|
212
|
end
|
|
213
|
with Not_found -> ( (* stateless node instance *)
|
|
214
|
let (n,_) = List.assoc i m.mcalls in
|
|
215
|
Format.fprintf fmt "(%s %a%t%a)"
|
|
216
|
(node_name n)
|
|
217
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
218
|
inputs
|
|
219
|
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
220
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
221
|
(List.map (fun v -> LocalVar v) outputs)
|
|
222
|
)
|
|
223
|
|
|
224
|
let pp_machine_init (m: machine_t) self fmt inst =
|
|
225
|
let (node, static) = List.assoc inst m.minstances in
|
|
226
|
fprintf fmt "(%a %a%t%s->%s)"
|
|
227
|
pp_machine_init_name (node_name node)
|
|
228
|
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
|
|
229
|
(Utils.pp_final_char_if_non_empty " " static)
|
|
230
|
self inst
|
|
231
|
|
|
232
|
(* TODO *)
|
|
233
|
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el =
|
|
234
|
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
|
|
235
|
(pp_horn_val self (pp_horn_var m)) c
|
|
236
|
(Utils.pp_newline_if_non_empty tl)
|
|
237
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl
|
|
238
|
(Utils.pp_newline_if_non_empty el)
|
|
239
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el
|
|
240
|
|
|
241
|
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
|
|
242
|
match instr with
|
|
243
|
| MReset i ->
|
|
244
|
pp_machine_init m self fmt i
|
|
245
|
| MLocalAssign (i,v) ->
|
|
246
|
pp_assign
|
|
247
|
m self (pp_horn_var m) fmt
|
|
248
|
i.var_type (LocalVar i) v
|
|
249
|
| MStateAssign (i,v) ->
|
|
250
|
pp_assign
|
|
251
|
m self (pp_horn_var m) fmt
|
|
252
|
i.var_type (StateVar i) v
|
|
253
|
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
|
|
254
|
assert false (* This should not happen anymore *)
|
|
255
|
| MStep (il, i, vl) ->
|
|
256
|
pp_instance_call machines ~init:init m self fmt i vl il
|
|
257
|
| MBranch (g,hl) ->
|
|
258
|
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
|
|
259
|
then (* boolean case, needs special treatment in C because truth value is not unique *)
|
|
260
|
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
261
|
let tl = try List.assoc tag_true hl with Not_found -> [] in
|
|
262
|
let el = try List.assoc tag_false hl with Not_found -> [] in
|
|
263
|
pp_conditional machines ~init:init m self fmt g tl el
|
|
264
|
else assert false (* enum type case *)
|
|
265
|
|
|
266
|
|
|
267
|
(**************************************************************)
|
|
268
|
|
|
269
|
let is_stateless m = m.minstances = [] && m.mmemory = []
|
|
270
|
|
|
271
|
(* Print the machine m:
|
|
272
|
two functions: m_init and m_step
|
|
273
|
- m_init is a predicate over m memories
|
|
274
|
- m_step is a predicate over old_memories, inputs, new_memories, outputs
|
|
275
|
We first declare all variables then the two /rules/.
|
|
276
|
*)
|
|
277
|
let print_machine machines fmt m =
|
|
278
|
let pp_instr init = pp_machine_instr machines ~init:init m in
|
|
279
|
if m.mname.node_id = arrow_id then
|
|
280
|
(* We don't print arrow function *)
|
|
281
|
()
|
|
282
|
else
|
|
283
|
begin
|
|
284
|
Format.fprintf fmt "; %s@." m.mname.node_id;
|
|
285
|
|
|
286
|
(* Printing variables *)
|
|
287
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
|
288
|
((step_vars machines m)@
|
|
289
|
(rename_machine_list m.mname.node_id m.mstep.step_locals));
|
|
290
|
Format.pp_print_newline fmt ();
|
|
291
|
|
|
292
|
|
|
293
|
|
|
294
|
if is_stateless m then
|
|
295
|
begin
|
|
296
|
(* Declaring single predicate *)
|
|
297
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
|
298
|
pp_machine_stateless_name m.mname.node_id
|
|
299
|
(Utils.fprintf_list ~sep:" " pp_type)
|
|
300
|
(List.map (fun v -> v.var_type) (stateless_vars machines m));
|
|
301
|
|
|
302
|
(* Rule for single predicate *)
|
|
303
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
304
|
(pp_conj (pp_instr
|
|
305
|
true (* In this case, the boolean init can be set to true or false.
|
|
306
|
The node is stateless. *)
|
|
307
|
m.mname.node_id)
|
|
308
|
)
|
|
309
|
m.mstep.step_instrs
|
|
310
|
pp_machine_stateless_name m.mname.node_id
|
|
311
|
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
|
|
312
|
end
|
|
313
|
else
|
|
314
|
begin
|
|
315
|
(* Declaring predicate *)
|
|
316
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
|
317
|
pp_machine_init_name m.mname.node_id
|
|
318
|
(Utils.fprintf_list ~sep:" " pp_type)
|
|
319
|
(List.map (fun v -> v.var_type) (init_vars machines m));
|
|
320
|
|
|
321
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
|
322
|
pp_machine_step_name m.mname.node_id
|
|
323
|
(Utils.fprintf_list ~sep:" " pp_type)
|
|
324
|
(List.map (fun v -> v.var_type) (step_vars machines m));
|
|
325
|
|
|
326
|
Format.pp_print_newline fmt ();
|
|
327
|
|
|
328
|
(* Rule for init *)
|
|
329
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
330
|
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
331
|
pp_machine_init_name m.mname.node_id
|
|
332
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
|
333
|
|
|
334
|
(* Rule for step *)
|
|
335
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
336
|
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
337
|
pp_machine_step_name m.mname.node_id
|
|
338
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
|
|
339
|
|
|
340
|
(* Adding assertions *)
|
|
341
|
(match m.mstep.step_asserts with
|
|
342
|
| [] -> ()
|
|
343
|
| assertsl -> begin
|
|
344
|
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
|
|
345
|
|
|
346
|
Format.fprintf fmt "; Asserts@.";
|
|
347
|
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
|
|
348
|
(pp_conj pp_val) assertsl;
|
|
349
|
|
|
350
|
(** TEME: the following code is the one we described. But it generates a segfault in z3
|
|
351
|
Format.fprintf fmt "; Asserts for init@.";
|
|
352
|
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
|
|
353
|
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
354
|
pp_machine_init_name m.mname.node_id
|
|
355
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
|
|
356
|
(pp_conj pp_val) assertsl;
|
|
357
|
|
|
358
|
Format.fprintf fmt "; Asserts for step@.";
|
|
359
|
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
|
|
360
|
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
361
|
|
|
362
|
pp_machine_step_name m.mname.node_id
|
|
363
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m)
|
|
364
|
(pp_conj pp_val) assertsl
|
|
365
|
*)
|
|
366
|
end
|
|
367
|
);
|
|
368
|
|
|
369
|
(*
|
|
370
|
match m.mspec with
|
|
371
|
None -> () (* No node spec; we do nothing *)
|
|
372
|
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
373
|
(
|
|
374
|
(* For the moment, we only deal with simple case: single ensures, no other parameters *)
|
|
375
|
()
|
|
376
|
|
|
377
|
)
|
|
378
|
| _ -> () (* Other cases give nothing *)
|
|
379
|
*)
|
|
380
|
end
|
|
381
|
end
|
|
382
|
|
|
383
|
|
|
384
|
|
|
385
|
let collecting_semantics machines fmt node machine =
|
|
386
|
Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
|
|
387
|
(* We print the types of the main node "memory tree" TODO: add the output *)
|
|
388
|
let main_output =
|
|
389
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
|
390
|
in
|
|
391
|
let main_output_dummy =
|
|
392
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
|
393
|
in
|
|
394
|
let main_memory_next =
|
|
395
|
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
|
|
396
|
main_output
|
|
397
|
in
|
|
398
|
let main_memory_current =
|
|
399
|
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
|
|
400
|
main_output_dummy
|
|
401
|
in
|
|
402
|
|
|
403
|
(* Special case when the main node is stateless *)
|
|
404
|
let init_name, step_name =
|
|
405
|
if is_stateless machine then
|
|
406
|
pp_machine_stateless_name, pp_machine_stateless_name
|
|
407
|
else
|
|
408
|
pp_machine_init_name, pp_machine_step_name
|
|
409
|
in
|
|
410
|
|
|
411
|
Format.fprintf fmt "(declare-rel MAIN (%a))@."
|
|
412
|
(Utils.fprintf_list ~sep:" " pp_type)
|
|
413
|
(List.map (fun v -> v.var_type) main_memory_next);
|
|
414
|
|
|
415
|
Format.fprintf fmt "; Initial set@.";
|
|
416
|
Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
|
|
417
|
Format.fprintf fmt "(rule INIT_STATE)@.";
|
|
418
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
419
|
init_name node
|
|
420
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
|
|
421
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
|
422
|
|
|
423
|
Format.fprintf fmt "; Inductive def@.";
|
|
424
|
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
|
|
425
|
Format.fprintf fmt
|
|
426
|
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
427
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current
|
|
428
|
step_name node
|
|
429
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
|
|
430
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
|
|
431
|
|
|
432
|
let check_prop machines fmt node machine =
|
|
433
|
let main_output =
|
|
434
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
|
435
|
in
|
|
436
|
let main_memory_next =
|
|
437
|
(rename_next_list (full_memory_vars machines machine)) @ main_output
|
|
438
|
in
|
|
439
|
Format.fprintf fmt "; Property def@.";
|
|
440
|
Format.fprintf fmt "(declare-rel ERR ())@.";
|
|
441
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
|
|
442
|
(pp_conj pp_var) main_output
|
|
443
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
|
|
444
|
;
|
|
445
|
if !Options.horn_queries then
|
|
446
|
Format.fprintf fmt "(query ERR)@."
|
|
447
|
|
|
448
|
|
|
449
|
let cex_computation machines fmt node machine =
|
|
450
|
Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
|
|
451
|
(* We print the types of the cex node "memory tree" TODO: add the output *)
|
|
452
|
let cex_input =
|
|
453
|
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
|
|
454
|
in
|
|
455
|
let cex_input_dummy =
|
|
456
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
|
|
457
|
in
|
|
458
|
let cex_output =
|
|
459
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
|
460
|
in
|
|
461
|
let cex_output_dummy =
|
|
462
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
|
463
|
in
|
|
464
|
let cex_memory_next =
|
|
465
|
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
|
|
466
|
in
|
|
467
|
let cex_memory_current =
|
|
468
|
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
|
|
469
|
in
|
|
470
|
|
|
471
|
(* Special case when the cex node is stateless *)
|
|
472
|
let init_name, step_name =
|
|
473
|
if is_stateless machine then
|
|
474
|
pp_machine_stateless_name, pp_machine_stateless_name
|
|
475
|
else
|
|
476
|
pp_machine_init_name, pp_machine_step_name
|
|
477
|
in
|
|
478
|
|
|
479
|
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
|
|
480
|
(Utils.fprintf_list ~sep:" " pp_type)
|
|
481
|
(List.map (fun v -> v.var_type) cex_memory_next);
|
|
482
|
|
|
483
|
Format.fprintf fmt "; Initial set@.";
|
|
484
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
|
|
485
|
init_name node
|
|
486
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
|
|
487
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
|
|
488
|
|
|
489
|
Format.fprintf fmt "; Inductive def@.";
|
|
490
|
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
|
|
491
|
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
|
|
492
|
Format.fprintf fmt "(declare-var cexcpt Int)@.";
|
|
493
|
Format.fprintf fmt
|
|
494
|
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
|
|
495
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
|
|
496
|
step_name node
|
|
497
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
|
|
498
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
|
|
499
|
|
|
500
|
let get_cex machines fmt node machine =
|
|
501
|
let cex_input =
|
|
502
|
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
|
|
503
|
in
|
|
504
|
let cex_output =
|
|
505
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
|
506
|
in
|
|
507
|
let cex_memory_next =
|
|
508
|
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
|
|
509
|
in
|
|
510
|
Format.fprintf fmt "; Property def@.";
|
|
511
|
Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
|
|
512
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
|
|
513
|
(pp_conj pp_var) cex_output
|
|
514
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
|
|
515
|
;
|
|
516
|
if !Options.horn_queries then
|
|
517
|
Format.fprintf fmt "(query CEXTRACE)@."
|
|
518
|
|
|
519
|
|
|
520
|
let main_print machines fmt =
|
|
521
|
if !Options.main_node <> "" then
|
|
522
|
begin
|
|
523
|
let node = !Options.main_node in
|
|
524
|
let machine = get_machine machines node in
|
|
525
|
|
|
526
|
|
|
527
|
collecting_semantics machines fmt node machine;
|
|
528
|
check_prop machines fmt node machine;
|
|
529
|
if !Options.horn_cex then(
|
|
530
|
cex_computation machines fmt node machine;
|
|
531
|
get_cex machines fmt node machine)
|
|
532
|
end
|
|
533
|
|
|
534
|
|
|
535
|
let translate fmt basename prog machines =
|
|
536
|
List.iter (print_machine machines fmt) (List.rev machines);
|
|
537
|
|
|
538
|
main_print machines fmt
|
|
539
|
|
|
540
|
|
|
541
|
let traces_file fmt basename prog machines =
|
|
542
|
Format.fprintf fmt
|
|
543
|
"; Horn code traceability generated by %s@.; SVN version number %s@.@."
|
|
544
|
(Filename.basename Sys.executable_name)
|
|
545
|
Version.number;
|
|
546
|
|
|
547
|
(* We extract the annotation dealing with traceability *)
|
|
548
|
let machines_traces = List.map (fun m ->
|
|
549
|
let traces : (ident * expr) list=
|
|
550
|
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
|
|
551
|
let filtered =
|
|
552
|
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
|
|
553
|
in
|
|
554
|
let content = List.map snd filtered in
|
|
555
|
(* Elements are supposed to be a pair (tuple): variable, expression *)
|
|
556
|
List.map (fun ee ->
|
|
557
|
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
|
|
558
|
| [], Expr_tuple [v;e] -> (
|
|
559
|
match v.expr_desc with
|
|
560
|
| Expr_ident vid -> vid, e
|
|
561
|
| _ -> assert false )
|
|
562
|
| _ -> assert false)
|
|
563
|
content
|
|
564
|
in
|
|
565
|
|
|
566
|
m, traces
|
|
567
|
|
|
568
|
) machines
|
|
569
|
in
|
|
570
|
|
|
571
|
(* Compute memories associated to each machine *)
|
|
572
|
let compute_mems m =
|
|
573
|
let rec aux fst prefix m =
|
|
574
|
(List.map (fun mem -> (prefix, mem)) m.mmemory) @
|
|
575
|
List.fold_left (fun accu (id, (n, _)) ->
|
|
576
|
let name = node_name n in
|
|
577
|
if name = "_arrow" then accu else
|
|
578
|
let machine_n = get_machine machines name in
|
|
579
|
( aux false ((id,machine_n)::prefix) machine_n )
|
|
580
|
@ accu
|
|
581
|
) [] m.minstances
|
|
582
|
in
|
|
583
|
aux true [] m
|
|
584
|
in
|
|
585
|
|
|
586
|
List.iter (fun m ->
|
|
587
|
Format.fprintf fmt "; Node %s@." m.mname.node_id;
|
|
588
|
|
|
589
|
let memories_old =
|
|
590
|
List.map (fun (p, v) ->
|
|
591
|
let machine = match p with | [] -> m | (_,m')::_ -> m' in
|
|
592
|
let traces = List.assoc machine machines_traces in
|
|
593
|
if List.mem_assoc v.var_id traces then
|
|
594
|
(* We take the expression associated to variable v in the trace info *)
|
|
595
|
p, List.assoc v.var_id traces
|
|
596
|
else
|
|
597
|
(* We keep the variable as is: we create an expression v *)
|
|
598
|
p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
|
|
599
|
|
|
600
|
) (compute_mems m)
|
|
601
|
in
|
|
602
|
let memories_next = (* We remove the topest pre in each expression *)
|
|
603
|
List.map
|
|
604
|
(fun (prefix, ee) ->
|
|
605
|
match ee.expr_desc with
|
|
606
|
| Expr_pre e -> prefix, e
|
|
607
|
| _ -> Format.eprintf
|
|
608
|
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
|
|
609
|
(Utils.fprintf_list ~sep:","
|
|
610
|
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
|
|
611
|
(List.rev prefix)
|
|
612
|
Printers.pp_expr ee;
|
|
613
|
assert false)
|
|
614
|
memories_old
|
|
615
|
in
|
|
616
|
|
|
617
|
let pp_prefix_rev fmt prefix =
|
|
618
|
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
|
|
619
|
in
|
|
620
|
|
|
621
|
Format.fprintf fmt "; Init predicate@.";
|
|
622
|
|
|
623
|
Format.fprintf fmt "; horn encoding@.";
|
|
624
|
Format.fprintf fmt "(%a %a)@."
|
|
625
|
pp_machine_init_name m.mname.node_id
|
|
626
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
|
627
|
|
|
628
|
Format.fprintf fmt "; original expressions@.";
|
|
629
|
Format.fprintf fmt "(%a %a%t%a)@."
|
|
630
|
pp_machine_init_name m.mname.node_id
|
|
631
|
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
|
|
632
|
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
|
|
633
|
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
|
|
634
|
|
|
635
|
Format.pp_print_newline fmt ();
|
|
636
|
Format.fprintf fmt "; Step predicate@.";
|
|
637
|
|
|
638
|
Format.fprintf fmt "; horn encoding@.";
|
|
639
|
Format.fprintf fmt "(%a %a)@."
|
|
640
|
pp_machine_step_name m.mname.node_id
|
|
641
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
|
|
642
|
Format.fprintf fmt "; original expressions@.";
|
|
643
|
Format.fprintf fmt "(%a %a%t%a)@."
|
|
644
|
pp_machine_step_name m.mname.node_id
|
|
645
|
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
|
|
646
|
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
|
|
647
|
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
|
|
648
|
Format.pp_print_newline fmt ();
|
|
649
|
) (List.rev machines);
|
|
650
|
|
|
651
|
|
|
652
|
(* Local Variables: *)
|
|
653
|
(* compile-command:"make -C .." *)
|
|
654
|
(* End: *)
|