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
|
open Utils
|
12
|
open Format
|
13
|
open Lustre_types
|
14
|
open Machine_code_types
|
15
|
open C_backend_common
|
16
|
open Corelang
|
17
|
open Spec_types
|
18
|
open Machine_code_common
|
19
|
module Mpfr = Lustrec_mpfr
|
20
|
|
21
|
(**************************************************************************)
|
22
|
(* Printing spec for c *)
|
23
|
|
24
|
(**************************************************************************)
|
25
|
|
26
|
let pp_acsl_basic_type_desc t_desc =
|
27
|
if Types.is_bool_type t_desc then
|
28
|
(* if !Options.cpp then "bool" else "_Bool" *)
|
29
|
"_Bool"
|
30
|
else if Types.is_int_type t_desc then
|
31
|
(* !Options.int_type *)
|
32
|
if t_desc.tid = -1 then "int" else "integer"
|
33
|
else if Types.is_real_type t_desc then
|
34
|
if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
|
35
|
else assert false
|
36
|
(* Not a basic C type. Do not handle arrays or pointers *)
|
37
|
|
38
|
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
|
39
|
|
40
|
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
|
41
|
|
42
|
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
|
43
|
|
44
|
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp
|
45
|
|
46
|
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
|
47
|
|
48
|
let pp_requires pp fmt = fprintf fmt "requires %a;" pp
|
49
|
|
50
|
let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
|
51
|
|
52
|
let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
|
53
|
|
54
|
let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
|
55
|
|
56
|
let pp_assigns pp =
|
57
|
pp_comma_list
|
58
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
|
59
|
~pp_epilogue:pp_print_semicolon'
|
60
|
pp
|
61
|
|
62
|
let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
|
63
|
|
64
|
let pp_assert pp fmt = fprintf fmt "assert %a;" pp
|
65
|
|
66
|
let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
|
67
|
|
68
|
let pp_mem_valid pp_var fmt (name, var) =
|
69
|
fprintf fmt "%s_valid(%a)" name pp_var var
|
70
|
|
71
|
let pp_mem_valid' = pp_mem_valid pp_print_string
|
72
|
|
73
|
let pp_ref pp fmt = fprintf fmt "&%a" pp
|
74
|
|
75
|
let pp_ref' = pp_ref pp_print_string
|
76
|
|
77
|
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
|
78
|
fprintf fmt "%a->%a" pp_ptr ptr pp_field field
|
79
|
|
80
|
let pp_indirect' = pp_indirect pp_print_string pp_print_string
|
81
|
|
82
|
let pp_access pp_stru pp_field fmt (stru, field) =
|
83
|
fprintf fmt "%a.%a" pp_stru stru pp_field field
|
84
|
|
85
|
let pp_access' = pp_access pp_print_string pp_print_string
|
86
|
|
87
|
let pp_var_decl fmt v = pp_print_string fmt v.var_id
|
88
|
|
89
|
let pp_reg self fmt field =
|
90
|
pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
|
91
|
|
92
|
let pp_true fmt () = pp_print_string fmt "\\true"
|
93
|
|
94
|
let pp_false fmt () = pp_print_string fmt "\\false"
|
95
|
|
96
|
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
|
97
|
|
98
|
let pp_null fmt () = pp_print_string fmt "\\null"
|
99
|
|
100
|
let pp_stdout fmt () = pp_print_string fmt "stdout"
|
101
|
|
102
|
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
|
103
|
|
104
|
let instances machines m =
|
105
|
let open List in
|
106
|
let grow paths i td mems =
|
107
|
match paths with
|
108
|
| [] ->
|
109
|
[ [ i, (td, mems) ] ]
|
110
|
| _ ->
|
111
|
map (cons (i, (td, mems))) paths
|
112
|
in
|
113
|
let rec aux paths m =
|
114
|
map
|
115
|
(fun (i, (td, _)) ->
|
116
|
try
|
117
|
let m = find (fun m -> m.mname.node_id = node_name td) machines in
|
118
|
aux (grow paths i td m.mmemory) m
|
119
|
with Not_found -> grow paths i td [])
|
120
|
m.minstances
|
121
|
|> flatten
|
122
|
in
|
123
|
aux [] m |> map rev
|
124
|
|
125
|
let memories insts =
|
126
|
List.(
|
127
|
map
|
128
|
(fun path ->
|
129
|
let _, (_, mems) = hd (rev path) in
|
130
|
map (fun mem -> path, mem) mems)
|
131
|
insts
|
132
|
|> flatten)
|
133
|
|
134
|
let pp_instance ?(indirect = true) pp ptr =
|
135
|
pp_print_list
|
136
|
~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
|
137
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
138
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
139
|
|
140
|
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
|
141
|
pp_access
|
142
|
((if indirect then pp_indirect else pp_access)
|
143
|
(pp_instance ~indirect pp_print_string ptr)
|
144
|
pp_print_string)
|
145
|
pp_var_decl
|
146
|
fmt
|
147
|
((path, "_reg"), mem)
|
148
|
|
149
|
let prefixes l =
|
150
|
let rec pref acc = function
|
151
|
| x :: l ->
|
152
|
pref ([ x ] :: List.map (List.cons x) acc) l
|
153
|
| [] ->
|
154
|
acc
|
155
|
in
|
156
|
pref [] (List.rev l)
|
157
|
|
158
|
let powerset_instances paths =
|
159
|
List.map prefixes paths |> List.flatten |> remove_duplicates
|
160
|
|
161
|
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
|
162
|
fprintf
|
163
|
fmt
|
164
|
"\\separated(@[<v>%a, %a@;%a@;%a@])"
|
165
|
pp_self
|
166
|
self
|
167
|
pp_mem
|
168
|
mem
|
169
|
(pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance pp_self self))
|
170
|
paths
|
171
|
(pp_comma_list ~pp_prologue:pp_print_comma' pp_ptr)
|
172
|
ptrs
|
173
|
|
174
|
let pp_separated' self mem fmt (paths, ptrs) =
|
175
|
pp_separated
|
176
|
pp_print_string
|
177
|
pp_print_string
|
178
|
pp_var_decl
|
179
|
fmt
|
180
|
(self, mem, paths, ptrs)
|
181
|
|
182
|
let pp_separated'' =
|
183
|
pp_comma_list
|
184
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
|
185
|
~pp_epilogue:pp_print_cpar
|
186
|
pp_var_decl
|
187
|
|
188
|
let pp_forall pp_l pp_r fmt (l, r) =
|
189
|
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
|
190
|
|
191
|
let pp_exists pp_l pp_r fmt (l, r) =
|
192
|
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
|
193
|
|
194
|
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
|
195
|
|
196
|
let pp_implies pp_l pp_r fmt (l, r) =
|
197
|
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
|
198
|
|
199
|
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
|
200
|
|
201
|
let pp_and_l pp_v fmt =
|
202
|
pp_print_list
|
203
|
~pp_open_box:pp_open_vbox0
|
204
|
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
|
205
|
pp_v
|
206
|
fmt
|
207
|
|
208
|
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
|
209
|
|
210
|
let pp_or_l pp_v fmt =
|
211
|
pp_print_list
|
212
|
~pp_open_box:pp_open_vbox0
|
213
|
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
|
214
|
pp_v
|
215
|
fmt
|
216
|
|
217
|
let pp_not pp fmt = fprintf fmt "!%a" pp
|
218
|
|
219
|
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
|
220
|
|
221
|
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
|
222
|
|
223
|
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
|
224
|
|
225
|
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
|
226
|
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
|
227
|
|
228
|
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
|
229
|
|
230
|
let pp_initialization pp_mem fmt (name, mem) =
|
231
|
fprintf fmt "%s_initialization(%a)" name pp_mem mem
|
232
|
|
233
|
let pp_initialization' = pp_initialization pp_print_string
|
234
|
|
235
|
let pp_local m =
|
236
|
pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
|
237
|
|
238
|
let pp_locals m =
|
239
|
pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
|
240
|
|
241
|
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
|
242
|
|
243
|
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
|
244
|
if Types.is_real_type typ && !Options.mpfr then assert false
|
245
|
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
|
246
|
else pp_equal pp_l pp_r fmt (var_name, value)
|
247
|
|
248
|
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
|
249
|
(var_type, var_name, value) =
|
250
|
let depth = expansion_depth value in
|
251
|
let loop_vars = mk_loop_variables m var_type depth in
|
252
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
253
|
let aux typ fmt vars =
|
254
|
match vars with
|
255
|
| [] ->
|
256
|
pp_basic_assign_spec
|
257
|
(pp_value_suffix
|
258
|
~indirect:indirect_l
|
259
|
m
|
260
|
self_l
|
261
|
var_type
|
262
|
loop_vars
|
263
|
pp_var_l)
|
264
|
(pp_value_suffix
|
265
|
~indirect:indirect_r
|
266
|
m
|
267
|
self_r
|
268
|
var_type
|
269
|
loop_vars
|
270
|
pp_var_r)
|
271
|
fmt
|
272
|
typ
|
273
|
var_name
|
274
|
value
|
275
|
| (_d, LVar _i) :: _q ->
|
276
|
assert false
|
277
|
(* let typ' = Types.array_element_type typ in
|
278
|
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
279
|
* i i i pp_c_dimension d i
|
280
|
* (aux typ') q *)
|
281
|
| (_d, LInt _r) :: _q ->
|
282
|
assert false
|
283
|
(* let typ' = Types.array_element_type typ in
|
284
|
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
285
|
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
286
|
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
|
287
|
| _ ->
|
288
|
assert false
|
289
|
in
|
290
|
reset_loop_counter ();
|
291
|
aux var_type fmt reordered_loop_vars
|
292
|
|
293
|
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
|
294
|
fprintf
|
295
|
fmt
|
296
|
"%s_pack%a(@[<hov>%a,@ %a@])"
|
297
|
name
|
298
|
(pp_print_option pp_print_int)
|
299
|
i
|
300
|
pp_mem
|
301
|
mem
|
302
|
pp_self
|
303
|
self
|
304
|
|
305
|
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
|
306
|
pp_memory_pack_aux
|
307
|
?i:mp.mpindex
|
308
|
pp_mem
|
309
|
pp_self
|
310
|
fmt
|
311
|
(mp.mpname.node_id, mem, self)
|
312
|
|
313
|
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
|
314
|
(name, vars, mem_in, mem_out) =
|
315
|
let stateless = fst (get_stateless_status m) in
|
316
|
fprintf
|
317
|
fmt
|
318
|
"%s_transition%a(@[<hov>%t%a%t@])"
|
319
|
name
|
320
|
(pp_print_option pp_print_int)
|
321
|
i
|
322
|
(fun fmt -> if not stateless then pp_mem_in fmt mem_in)
|
323
|
(pp_comma_list
|
324
|
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
|
325
|
pp_var)
|
326
|
vars
|
327
|
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
|
328
|
|
329
|
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
|
330
|
pp_transition_aux
|
331
|
?i:t.tindex
|
332
|
m
|
333
|
pp_mem_in
|
334
|
pp_mem_out
|
335
|
pp_var
|
336
|
fmt
|
337
|
(t.tname.node_id, t.tvars, mem_in, mem_out)
|
338
|
|
339
|
let pp_transition_aux' ?i m =
|
340
|
pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
|
341
|
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
|
342
|
|
343
|
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
|
344
|
fprintf
|
345
|
fmt
|
346
|
"%s_reset_cleared(@[<hov>%a,@ %a@])"
|
347
|
name
|
348
|
pp_mem_in
|
349
|
mem_in
|
350
|
pp_mem_out
|
351
|
mem_out
|
352
|
|
353
|
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
|
354
|
|
355
|
let pp_functional_update mems insts fmt mem =
|
356
|
let rec aux fmt = function
|
357
|
| [] ->
|
358
|
pp_print_string fmt mem
|
359
|
| (x, is_mem) :: fields ->
|
360
|
fprintf
|
361
|
fmt
|
362
|
"{ @[<hov>%a@ \\with .%s%s = %s@] }"
|
363
|
aux
|
364
|
fields
|
365
|
(if is_mem then "_reg." else "")
|
366
|
x
|
367
|
x
|
368
|
in
|
369
|
aux
|
370
|
fmt
|
371
|
(List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
|
372
|
@ List.map (fun x -> x, true) (Utils.ISet.elements mems))
|
373
|
|
374
|
module PrintSpec = struct
|
375
|
type mode =
|
376
|
| MemoryPackMode
|
377
|
| TransitionMode
|
378
|
| TransitionFootprintMode
|
379
|
| ResetIn
|
380
|
| ResetOut
|
381
|
| InstrMode of ident
|
382
|
|
383
|
let pp_reg mem fmt = function
|
384
|
| ResetFlag ->
|
385
|
fprintf fmt "%s.%s" mem reset_flag_name
|
386
|
| StateVar x ->
|
387
|
fprintf fmt "%s.%a" mem pp_var_decl x
|
388
|
|
389
|
let pp_expr :
|
390
|
type a.
|
391
|
?test_output:bool ->
|
392
|
machine_t ->
|
393
|
ident ->
|
394
|
formatter ->
|
395
|
(value_t, a) expression_t ->
|
396
|
unit =
|
397
|
fun ?(test_output = false) m mem fmt -> function
|
398
|
| Val v ->
|
399
|
pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
|
400
|
| Tag t ->
|
401
|
pp_print_string fmt t
|
402
|
| Var v ->
|
403
|
pp_var_decl fmt v
|
404
|
| Memory r ->
|
405
|
pp_reg mem fmt r
|
406
|
|
407
|
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
|
408
|
let test_output, mem_update =
|
409
|
match mode with
|
410
|
| InstrMode _ ->
|
411
|
true, false
|
412
|
| TransitionFootprintMode ->
|
413
|
false, true
|
414
|
| _ ->
|
415
|
false, false
|
416
|
in
|
417
|
let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
|
418
|
=
|
419
|
fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
|
420
|
in
|
421
|
match p with
|
422
|
| Transition (f, inst, i, vars, r, mems, insts) ->
|
423
|
let pp_mem_in, pp_mem_out =
|
424
|
match inst with
|
425
|
| None ->
|
426
|
( pp_print_string,
|
427
|
if mem_update then pp_functional_update mems insts
|
428
|
else pp_print_string )
|
429
|
| Some inst ->
|
430
|
( (fun fmt mem_in ->
|
431
|
if r then pp_print_string fmt mem_in
|
432
|
else pp_access' fmt (mem_in, inst)),
|
433
|
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
|
434
|
in
|
435
|
pp_transition_aux
|
436
|
?i
|
437
|
m
|
438
|
pp_mem_in
|
439
|
pp_mem_out
|
440
|
(pp_expr test_output)
|
441
|
fmt
|
442
|
(f, vars, mem_in', mem_out')
|
443
|
| Reset (_f, inst, r) ->
|
444
|
pp_ite
|
445
|
(pp_c_val m mem_in (pp_c_var_read m))
|
446
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
447
|
(pp_equal pp_print_string pp_access')
|
448
|
fmt
|
449
|
(r, (mem_out, 1), (mem_out, (mem_in, inst)))
|
450
|
| MemoryPack (f, inst, i) ->
|
451
|
let pp_mem, pp_self =
|
452
|
match inst with
|
453
|
| None ->
|
454
|
pp_print_string, pp_print_string
|
455
|
| Some inst ->
|
456
|
( (fun fmt mem -> pp_access' fmt (mem, inst)),
|
457
|
fun fmt self -> pp_indirect' fmt (self, inst) )
|
458
|
in
|
459
|
pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
|
460
|
| ResetCleared f ->
|
461
|
pp_reset_cleared' fmt (f, mem_in, mem_out)
|
462
|
(* fprintf fmt "ResetCleared_%a" pp_print_string f *)
|
463
|
| Initialization ->
|
464
|
()
|
465
|
|
466
|
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
|
467
|
|
468
|
let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
|
469
|
| Val v ->
|
470
|
v
|
471
|
| Tag t ->
|
472
|
id_to_tag t
|
473
|
| Var v ->
|
474
|
vdecl_to_val v
|
475
|
| Memory (StateVar v) ->
|
476
|
vdecl_to_val v
|
477
|
| Memory ResetFlag ->
|
478
|
vdecl_to_val reset_flag
|
479
|
|
480
|
let find_arrow m =
|
481
|
try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
|
482
|
with Not_found ->
|
483
|
eprintf "Internal error: arrow not found";
|
484
|
raise Not_found
|
485
|
|
486
|
let pp_spec mode m =
|
487
|
let rec pp_spec mode fmt f =
|
488
|
let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
|
489
|
let self = mk_self m in
|
490
|
let mem = mk_mem m in
|
491
|
let mem_in = mk_mem_in m in
|
492
|
let mem_out = mk_mem_out m in
|
493
|
let mem_reset = mk_mem_reset m in
|
494
|
match mode with
|
495
|
| MemoryPackMode ->
|
496
|
self, self, true, mem, mem, false
|
497
|
| TransitionMode ->
|
498
|
mem_in, mem_in, false, mem_out, mem_out, false
|
499
|
| TransitionFootprintMode ->
|
500
|
mem_in, mem_in, false, mem_out, mem_out, false
|
501
|
| ResetIn ->
|
502
|
mem_reset, mem_reset, false, mem_out, mem_out, false
|
503
|
| ResetOut ->
|
504
|
mem_in, mem_in, false, mem_reset, mem_reset, false
|
505
|
| InstrMode self ->
|
506
|
let mem = "*" ^ mem in
|
507
|
fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
|
508
|
self, flush_str_formatter (), false, mem, mem, false
|
509
|
in
|
510
|
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
511
|
fun fmt e -> pp_expr m mem_out fmt e
|
512
|
in
|
513
|
let pp_spec' = pp_spec mode in
|
514
|
match f with
|
515
|
| True ->
|
516
|
pp_true fmt ()
|
517
|
| False ->
|
518
|
pp_false fmt ()
|
519
|
| Equal (a, b) ->
|
520
|
pp_assign_spec
|
521
|
m
|
522
|
mem_out
|
523
|
(pp_c_var_read ~test_output:false m)
|
524
|
indirect_l
|
525
|
mem_in
|
526
|
(pp_c_var_read ~test_output:false m)
|
527
|
indirect_r
|
528
|
fmt
|
529
|
(type_of_l_value a, val_of_expr a, val_of_expr b)
|
530
|
| And fs ->
|
531
|
pp_and_l pp_spec' fmt fs
|
532
|
| Or fs ->
|
533
|
pp_or_l pp_spec' fmt fs
|
534
|
| Imply (a, b) ->
|
535
|
pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
|
536
|
| Exists (xs, a) ->
|
537
|
pp_exists (pp_locals m) pp_spec' fmt (xs, a)
|
538
|
| Forall (xs, a) ->
|
539
|
pp_forall (pp_locals m) pp_spec' fmt (xs, a)
|
540
|
| Ternary (e, a, b) ->
|
541
|
pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
|
542
|
| Predicate p ->
|
543
|
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
|
544
|
| StateVarPack ResetFlag ->
|
545
|
let r = vdecl_to_val reset_flag in
|
546
|
pp_assign_spec
|
547
|
m
|
548
|
mem_out
|
549
|
(pp_c_var_read ~test_output:false m)
|
550
|
indirect_l
|
551
|
mem_in
|
552
|
(pp_c_var_read ~test_output:false m)
|
553
|
indirect_r
|
554
|
fmt
|
555
|
(Type_predef.type_bool, r, r)
|
556
|
| StateVarPack (StateVar v) ->
|
557
|
let v' = vdecl_to_val v in
|
558
|
let inst = find_arrow m in
|
559
|
pp_paren
|
560
|
(pp_implies
|
561
|
(pp_not (pp_initialization pp_access'))
|
562
|
(pp_assign_spec
|
563
|
m
|
564
|
mem_out
|
565
|
(pp_c_var_read ~test_output:false m)
|
566
|
indirect_l
|
567
|
mem_in
|
568
|
(pp_c_var_read ~test_output:false m)
|
569
|
indirect_r))
|
570
|
fmt
|
571
|
((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
|
572
|
| ExistsMem (f, rc, tr) ->
|
573
|
pp_exists
|
574
|
(pp_machine_decl' ~ghost:true)
|
575
|
(pp_and (pp_spec ResetOut) (pp_spec ResetIn))
|
576
|
fmt
|
577
|
((f, mk_mem_reset m), (rc, tr))
|
578
|
in
|
579
|
pp_spec mode
|
580
|
end
|
581
|
|
582
|
let pp_predicate pp_l pp_r fmt (l, r) =
|
583
|
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
|
584
|
|
585
|
let pp_lemma pp_l pp_r fmt (l, r) =
|
586
|
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
|
587
|
|
588
|
let pp_mem_valid_def fmt m =
|
589
|
if not (fst (get_stateless_status m)) then
|
590
|
let name = m.mname.node_id in
|
591
|
let self = mk_self m in
|
592
|
pp_acsl
|
593
|
(pp_predicate
|
594
|
(pp_mem_valid (pp_machine_decl pp_ptr))
|
595
|
(pp_and
|
596
|
(pp_and_l (fun fmt (inst, (td, _)) ->
|
597
|
if Arrow.td_is_arrow td then
|
598
|
pp_valid pp_indirect' fmt [ self, inst ]
|
599
|
else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
|
600
|
(pp_valid pp_print_string)))
|
601
|
fmt
|
602
|
((name, (name, self)), (m.minstances, [ self ]))
|
603
|
|
604
|
let pp_memory_pack_def m fmt mp =
|
605
|
let name = mp.mpname.node_id in
|
606
|
let self = mk_self m in
|
607
|
let mem = mk_mem m in
|
608
|
pp_acsl
|
609
|
(pp_predicate
|
610
|
(pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
|
611
|
(PrintSpec.pp_spec MemoryPackMode m))
|
612
|
fmt
|
613
|
((mp, (name, mem), (name, self)), mp.mpformula)
|
614
|
|
615
|
let pp_machine_ghost_struct fmt m =
|
616
|
pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
|
617
|
|
618
|
let pp_memory_pack_defs fmt m =
|
619
|
if not (fst (get_stateless_status m)) then
|
620
|
fprintf
|
621
|
fmt
|
622
|
"%a@,%a"
|
623
|
pp_machine_ghost_struct
|
624
|
m
|
625
|
(pp_print_list
|
626
|
~pp_epilogue:pp_print_cut
|
627
|
~pp_open_box:pp_open_vbox0
|
628
|
(pp_memory_pack_def m))
|
629
|
m.mspec.mmemory_packs
|
630
|
|
631
|
let pp_transition_def m fmt t =
|
632
|
let name = t.tname.node_id in
|
633
|
let mem_in = mk_mem_in m in
|
634
|
let mem_out = mk_mem_out m in
|
635
|
pp_acsl
|
636
|
(pp_predicate
|
637
|
(pp_transition
|
638
|
m
|
639
|
(pp_machine_decl' ~ghost:true)
|
640
|
(pp_machine_decl' ~ghost:true)
|
641
|
(pp_local m))
|
642
|
(PrintSpec.pp_spec TransitionMode m))
|
643
|
fmt
|
644
|
((t, (name, mem_in), (name, mem_out)), t.tformula)
|
645
|
|
646
|
let pp_transition_defs fmt m =
|
647
|
pp_print_list
|
648
|
~pp_epilogue:pp_print_cut
|
649
|
~pp_open_box:pp_open_vbox0
|
650
|
(pp_transition_def m)
|
651
|
fmt
|
652
|
m.mspec.mtransitions
|
653
|
|
654
|
let pp_transition_footprint fmt t =
|
655
|
fprintf
|
656
|
fmt
|
657
|
"%s_transition%a_footprint"
|
658
|
t.tname.node_id
|
659
|
(pp_print_option pp_print_int)
|
660
|
t.tindex
|
661
|
|
662
|
let pp_transition_footprint_lemma m fmt t =
|
663
|
let name = t.tname.node_id in
|
664
|
let mem_in = mk_mem_in m in
|
665
|
let mem_out = mk_mem_out m in
|
666
|
let mems =
|
667
|
ISet.(
|
668
|
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
|
669
|
in
|
670
|
let insts =
|
671
|
IMap.(
|
672
|
diff
|
673
|
(of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
|
674
|
t.tinst_footprint)
|
675
|
in
|
676
|
let memories =
|
677
|
List.map
|
678
|
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
|
679
|
(List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
|
680
|
in
|
681
|
let mems_empty = ISet.is_empty mems in
|
682
|
let insts_empty = IMap.is_empty insts in
|
683
|
let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
|
684
|
let tr ?mems ?insts () =
|
685
|
Spec_common.mk_transition
|
686
|
?mems
|
687
|
?insts
|
688
|
?i:t.tindex
|
689
|
name
|
690
|
(vdecls_to_vals t.tvars)
|
691
|
in
|
692
|
if not (mems_empty && insts_empty) then
|
693
|
pp_acsl
|
694
|
(pp_lemma
|
695
|
pp_transition_footprint
|
696
|
(pp_forall
|
697
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
698
|
((if insts_empty then fun pp fmt (_, x) -> pp fmt x
|
699
|
else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
|
700
|
((if mems_empty then fun pp fmt (_, x) -> pp fmt x
|
701
|
else pp_forall (pp_locals m))
|
702
|
(PrintSpec.pp_spec TransitionFootprintMode m)))))
|
703
|
fmt
|
704
|
( t,
|
705
|
( (m.mname.node_id, [ mem_in; mem_out ]),
|
706
|
( instances,
|
707
|
(memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
|
708
|
)
|
709
|
|
710
|
let pp_transition_footprint_lemmas fmt m =
|
711
|
pp_print_list
|
712
|
~pp_epilogue:pp_print_cut
|
713
|
~pp_open_box:pp_open_vbox0
|
714
|
(pp_transition_footprint_lemma m)
|
715
|
fmt
|
716
|
(List.filter
|
717
|
(fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
718
|
m.mspec.mtransitions)
|
719
|
|
720
|
let pp_initialization_def fmt m =
|
721
|
if not (fst (get_stateless_status m)) then
|
722
|
let name = m.mname.node_id in
|
723
|
let mem_in = mk_mem_in m in
|
724
|
pp_acsl
|
725
|
(pp_predicate
|
726
|
(pp_initialization (pp_machine_decl' ~ghost:true))
|
727
|
(pp_and_l (fun fmt (i, (td, _)) ->
|
728
|
if Arrow.td_is_arrow td then
|
729
|
pp_initialization pp_access' fmt (node_name td, (mem_in, i))
|
730
|
else
|
731
|
pp_equal
|
732
|
(pp_reset_flag ~indirect:false pp_access')
|
733
|
pp_print_int
|
734
|
fmt
|
735
|
((mem_in, i), 1))))
|
736
|
fmt
|
737
|
((name, (name, mem_in)), m.minstances)
|
738
|
|
739
|
let pp_reset_cleared_def fmt m =
|
740
|
if not (fst (get_stateless_status m)) then
|
741
|
let name = m.mname.node_id in
|
742
|
let mem_in = mk_mem_in m in
|
743
|
let mem_out = mk_mem_out m in
|
744
|
pp_acsl
|
745
|
(pp_predicate
|
746
|
(pp_reset_cleared
|
747
|
(pp_machine_decl' ~ghost:true)
|
748
|
(pp_machine_decl' ~ghost:true))
|
749
|
(pp_ite
|
750
|
(pp_reset_flag' ~indirect:false)
|
751
|
(pp_and
|
752
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
753
|
pp_initialization')
|
754
|
(pp_equal pp_print_string pp_print_string)))
|
755
|
fmt
|
756
|
( (name, (name, mem_in), (name, mem_out)),
|
757
|
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
|
758
|
|
759
|
let pp_register_chain ?(indirect = true) ptr =
|
760
|
pp_print_list
|
761
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
762
|
~pp_epilogue:(fun fmt () ->
|
763
|
fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
|
764
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
765
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
766
|
|
767
|
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
|
768
|
pp_print_list
|
769
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
770
|
~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
|
771
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
772
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
773
|
fmt
|
774
|
mems
|
775
|
|
776
|
let pp_arrow_reset_ghost mem fmt inst =
|
777
|
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
|
778
|
|
779
|
module GhostProto : MODIFIERS_GHOST_PROTO = struct
|
780
|
let pp_ghost_parameters ?(cut = true) fmt vs =
|
781
|
fprintf
|
782
|
fmt
|
783
|
"%a%a"
|
784
|
(if cut then pp_print_cut else pp_print_nothing)
|
785
|
()
|
786
|
(pp_acsl_line'
|
787
|
(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
|
788
|
vs
|
789
|
end
|
790
|
|
791
|
module HdrMod = struct
|
792
|
module GhostProto = GhostProto
|
793
|
|
794
|
let pp_machine_decl_prefix _ _ = ()
|
795
|
|
796
|
let pp_import_arrow fmt () =
|
797
|
fprintf
|
798
|
fmt
|
799
|
"#include \"%s/arrow_spec.h%s\""
|
800
|
(Arrow.arrow_top_decl ()).top_decl_owner
|
801
|
(if !Options.cpp then "pp" else "")
|
802
|
|
803
|
let pp_predicates fmt machines =
|
804
|
let pp_preds comment pp =
|
805
|
pp_print_list
|
806
|
~pp_open_box:pp_open_vbox0
|
807
|
~pp_prologue:(pp_print_endcut comment)
|
808
|
pp
|
809
|
~pp_epilogue:pp_print_cutcut
|
810
|
in
|
811
|
fprintf
|
812
|
fmt
|
813
|
"%a%a"
|
814
|
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
|
815
|
machines
|
816
|
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
|
817
|
machines
|
818
|
|
819
|
let pp_machine_alloc_decl fmt m =
|
820
|
pp_machine_decl_prefix fmt m;
|
821
|
if not (fst (get_stateless_status m)) then
|
822
|
if !Options.static_mem then
|
823
|
(* Static allocation *)
|
824
|
let macro = m, mk_attribute m, mk_instance m in
|
825
|
fprintf
|
826
|
fmt
|
827
|
"%a@,%a@,%a"
|
828
|
(pp_static_declare_macro ~ghost:true)
|
829
|
macro
|
830
|
(pp_static_link_macro ~ghost:true)
|
831
|
macro
|
832
|
(pp_static_alloc_macro ~ghost:true)
|
833
|
macro
|
834
|
else
|
835
|
(* Dynamic allocation *)
|
836
|
(* TODO: handle dynamic alloc *)
|
837
|
assert false
|
838
|
(* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
|
839
|
* (m.mname.node_id, m.mstatic)
|
840
|
* pp_dealloc_prototype m.mname.node_id *)
|
841
|
end
|
842
|
|
843
|
module SrcMod = struct
|
844
|
module GhostProto = GhostProto
|
845
|
|
846
|
let pp_predicates fmt machines =
|
847
|
let pp_preds comment pp =
|
848
|
pp_print_list
|
849
|
~pp_open_box:pp_open_vbox0
|
850
|
~pp_prologue:(pp_print_endcut comment)
|
851
|
pp
|
852
|
~pp_epilogue:pp_print_cutcut
|
853
|
in
|
854
|
fprintf
|
855
|
fmt
|
856
|
"%a%a%a%a%a%a"
|
857
|
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
|
858
|
machines
|
859
|
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
|
860
|
machines
|
861
|
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
|
862
|
machines
|
863
|
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
|
864
|
machines
|
865
|
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
|
866
|
machines
|
867
|
(pp_preds
|
868
|
"/* ACSL transition memory footprints lemmas */"
|
869
|
pp_transition_footprint_lemmas)
|
870
|
machines
|
871
|
|
872
|
let pp_clear_reset_spec fmt self mem m =
|
873
|
let name = m.mname.node_id in
|
874
|
let arws, narws =
|
875
|
List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
|
876
|
in
|
877
|
let mk_insts = List.map (fun x -> [ x ]) in
|
878
|
pp_acsl_cut
|
879
|
(fun fmt () ->
|
880
|
fprintf
|
881
|
fmt
|
882
|
"%a@,\
|
883
|
%a@,\
|
884
|
%a@,\
|
885
|
%a@,\
|
886
|
%a@,\
|
887
|
%a@,\
|
888
|
%a@,\
|
889
|
%a@,\
|
890
|
%a@,\
|
891
|
%a@,\
|
892
|
@[<v 2>behavior reset:@;\
|
893
|
%a@,\
|
894
|
%a@]@,\
|
895
|
@[<v 2>behavior no_reset:@;\
|
896
|
%a@,\
|
897
|
%a@]@,\
|
898
|
complete behaviors;@,\
|
899
|
disjoint behaviors;"
|
900
|
(pp_requires pp_mem_valid')
|
901
|
(name, self)
|
902
|
(pp_requires (pp_separated' self mem))
|
903
|
(mk_insts m.minstances, [])
|
904
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
905
|
(name, mem, self)
|
906
|
(pp_ensures
|
907
|
(pp_memory_pack_aux
|
908
|
~i:(List.length m.mspec.mmemory_packs - 2)
|
909
|
pp_ptr
|
910
|
pp_print_string))
|
911
|
(name, mem, self)
|
912
|
(pp_assigns pp_reset_flag')
|
913
|
[ self ]
|
914
|
(pp_assigns (pp_register_chain self))
|
915
|
(mk_insts arws)
|
916
|
(pp_assigns (pp_reset_flag_chain self))
|
917
|
(mk_insts narws)
|
918
|
(pp_assigns pp_reset_flag')
|
919
|
[ mem ]
|
920
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
921
|
(mk_insts arws)
|
922
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
923
|
(mk_insts narws)
|
924
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
925
|
(mem, 1)
|
926
|
(pp_ensures (pp_initialization pp_ptr))
|
927
|
(name, mem)
|
928
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
929
|
(mem, 0)
|
930
|
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
|
931
|
(mem, mem))
|
932
|
fmt
|
933
|
()
|
934
|
|
935
|
let pp_set_reset_spec fmt self mem m =
|
936
|
let name = m.mname.node_id in
|
937
|
pp_acsl_cut
|
938
|
(fun fmt () ->
|
939
|
fprintf
|
940
|
fmt
|
941
|
"%a@,%a@,%a"
|
942
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
943
|
(name, mem, self)
|
944
|
(pp_ensures (pp_equal pp_reset_flag' pp_print_int))
|
945
|
(mem, 1)
|
946
|
(pp_assigns pp_reset_flag')
|
947
|
[ self; mem ])
|
948
|
fmt
|
949
|
()
|
950
|
|
951
|
let pp_step_spec fmt machines self mem m =
|
952
|
let name = m.mname.node_id in
|
953
|
let insts = instances machines m in
|
954
|
let insts' = powerset_instances insts in
|
955
|
let insts'' =
|
956
|
List.(
|
957
|
filter
|
958
|
(fun l -> l <> [])
|
959
|
(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
|
960
|
in
|
961
|
let inputs = m.mstep.step_inputs in
|
962
|
let outputs = m.mstep.step_outputs in
|
963
|
pp_acsl_cut
|
964
|
(fun fmt () ->
|
965
|
if fst (get_stateless_status m) then
|
966
|
fprintf
|
967
|
fmt
|
968
|
"%a@,%a@,%a@,%a"
|
969
|
(pp_requires (pp_valid pp_var_decl))
|
970
|
outputs
|
971
|
(pp_requires pp_separated'')
|
972
|
outputs
|
973
|
(pp_assigns pp_ptr_decl)
|
974
|
outputs
|
975
|
(pp_ensures (pp_transition_aux' m))
|
976
|
(name, inputs @ outputs, "", "")
|
977
|
else
|
978
|
fprintf
|
979
|
fmt
|
980
|
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
|
981
|
(pp_requires (pp_valid pp_var_decl))
|
982
|
outputs
|
983
|
(pp_requires pp_mem_valid')
|
984
|
(name, self)
|
985
|
(pp_requires (pp_separated' self mem))
|
986
|
(insts', outputs)
|
987
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
988
|
(name, mem, self)
|
989
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
990
|
(name, mem, self)
|
991
|
(pp_ensures
|
992
|
(pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
|
993
|
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
|
994
|
(name, inputs @ outputs, mem, mem)
|
995
|
(pp_assigns pp_ptr_decl)
|
996
|
outputs
|
997
|
(pp_assigns (pp_reg self))
|
998
|
m.mmemory
|
999
|
(pp_assigns pp_reset_flag')
|
1000
|
[ self ]
|
1001
|
(pp_assigns (pp_memory self))
|
1002
|
(memories insts')
|
1003
|
(pp_assigns (pp_register_chain self))
|
1004
|
insts
|
1005
|
(pp_assigns (pp_reset_flag_chain self))
|
1006
|
insts''
|
1007
|
(pp_assigns (pp_reg mem))
|
1008
|
m.mmemory
|
1009
|
(pp_assigns pp_reset_flag')
|
1010
|
[ mem ]
|
1011
|
(pp_assigns (pp_memory ~indirect:false mem))
|
1012
|
(memories insts')
|
1013
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
1014
|
insts
|
1015
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
1016
|
insts'')
|
1017
|
fmt
|
1018
|
()
|
1019
|
|
1020
|
let pp_ghost_instr_code m self fmt instr =
|
1021
|
match instr.instr_desc with
|
1022
|
| MStateAssign (x, v) ->
|
1023
|
fprintf
|
1024
|
fmt
|
1025
|
"@,%a"
|
1026
|
(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
|
1027
|
(x, v)
|
1028
|
| MResetAssign b ->
|
1029
|
fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
|
1030
|
| MSetReset inst ->
|
1031
|
let td, _ = List.assoc inst m.minstances in
|
1032
|
if Arrow.td_is_arrow td then
|
1033
|
fprintf
|
1034
|
fmt
|
1035
|
"@,%a;"
|
1036
|
(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
|
1037
|
inst
|
1038
|
| _ ->
|
1039
|
()
|
1040
|
|
1041
|
let pp_step_instr_spec m self mem fmt instr =
|
1042
|
fprintf
|
1043
|
fmt
|
1044
|
"%a%a"
|
1045
|
(pp_ghost_instr_code m mem)
|
1046
|
instr
|
1047
|
(pp_print_list
|
1048
|
~pp_open_box:pp_open_vbox0
|
1049
|
~pp_prologue:pp_print_cut
|
1050
|
(pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
|
1051
|
instr.instr_spec
|
1052
|
|
1053
|
let pp_ghost_parameter mem fmt inst =
|
1054
|
GhostProto.pp_ghost_parameters
|
1055
|
~cut:false
|
1056
|
fmt
|
1057
|
(match inst with
|
1058
|
| Some inst ->
|
1059
|
[ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
|
1060
|
| None ->
|
1061
|
[ mem, pp_print_string ])
|
1062
|
end
|
1063
|
|
1064
|
module MainMod = struct
|
1065
|
let main_mem_ghost = "main_mem_ghost"
|
1066
|
|
1067
|
let pp_declare_ghost_state fmt name =
|
1068
|
pp_acsl_line'_cut
|
1069
|
(pp_ghost (fun fmt () ->
|
1070
|
fprintf
|
1071
|
fmt
|
1072
|
"%a(,%s);"
|
1073
|
(pp_machine_static_alloc_name ~ghost:true)
|
1074
|
name
|
1075
|
main_mem_ghost))
|
1076
|
fmt
|
1077
|
()
|
1078
|
|
1079
|
let pp_ghost_state_parameter fmt () =
|
1080
|
GhostProto.pp_ghost_parameters
|
1081
|
~cut:false
|
1082
|
fmt
|
1083
|
[ main_mem_ghost, pp_ref pp_print_string ]
|
1084
|
|
1085
|
let pp_main_loop_invariants main_mem machines fmt m =
|
1086
|
let name = m.mname.node_id in
|
1087
|
let insts = powerset_instances (instances machines m) in
|
1088
|
pp_acsl_cut
|
1089
|
(fun fmt () ->
|
1090
|
fprintf
|
1091
|
fmt
|
1092
|
"%a@,%a@,%a@,%a"
|
1093
|
(pp_loop_invariant pp_mem_valid')
|
1094
|
(name, main_mem)
|
1095
|
(pp_loop_invariant
|
1096
|
(pp_memory_pack_aux pp_print_string pp_print_string))
|
1097
|
(name, main_mem_ghost, main_mem)
|
1098
|
(pp_loop_invariant
|
1099
|
(pp_separated
|
1100
|
(pp_paren pp_print_string)
|
1101
|
pp_ref'
|
1102
|
(pp_ref pp_var_decl)))
|
1103
|
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
|
1104
|
(pp_loop_invariant
|
1105
|
(pp_or
|
1106
|
(pp_valid_read pp_stdout)
|
1107
|
(pp_equal pp_stdout pp_null)))
|
1108
|
((), ((), ())))
|
1109
|
fmt
|
1110
|
()
|
1111
|
|
1112
|
let pp_main_spec fmt =
|
1113
|
pp_acsl_cut
|
1114
|
(fun fmt () ->
|
1115
|
fprintf
|
1116
|
fmt
|
1117
|
"%a@,%a@,%a@,%a"
|
1118
|
(pp_requires
|
1119
|
(pp_or
|
1120
|
(pp_valid_read pp_stdout)
|
1121
|
(pp_equal pp_stdout pp_null)))
|
1122
|
((), ((), ()))
|
1123
|
(pp_terminates pp_false)
|
1124
|
()
|
1125
|
(pp_ensures pp_false)
|
1126
|
()
|
1127
|
(pp_assigns pp_nothing)
|
1128
|
[ () ])
|
1129
|
fmt
|
1130
|
()
|
1131
|
end
|
1132
|
|
1133
|
(**************************************************************************)
|
1134
|
(* MAKEFILE *)
|
1135
|
(**************************************************************************)
|
1136
|
|
1137
|
module MakefileMod = struct
|
1138
|
let other_targets fmt basename _nodename dependencies =
|
1139
|
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
|
1140
|
(* EACSL version of library file . c *)
|
1141
|
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
|
1142
|
fprintf
|
1143
|
fmt
|
1144
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
|
1145
|
e-acsl -print -ocode %s_eacsl.c@."
|
1146
|
basename
|
1147
|
basename;
|
1148
|
fprintf fmt "@.";
|
1149
|
fprintf fmt "@.";
|
1150
|
|
1151
|
(* EACSL version of library file . c + main .c *)
|
1152
|
fprintf
|
1153
|
fmt
|
1154
|
"%s_main_eacsl.c: %s.c %s.h %s_main.c@."
|
1155
|
basename
|
1156
|
basename
|
1157
|
basename
|
1158
|
basename;
|
1159
|
fprintf
|
1160
|
fmt
|
1161
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
|
1162
|
-then-on e-acsl -print -ocode %s_main_eacsl.i@."
|
1163
|
basename
|
1164
|
basename
|
1165
|
basename;
|
1166
|
(* Ugly hack to deal with eacsl bugs *)
|
1167
|
fprintf
|
1168
|
fmt
|
1169
|
"\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
|
1170
|
basename
|
1171
|
basename;
|
1172
|
fprintf fmt "@.";
|
1173
|
fprintf fmt "@.";
|
1174
|
|
1175
|
(* EACSL version of binary *)
|
1176
|
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
|
1177
|
fprintf
|
1178
|
fmt
|
1179
|
"\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
|
1180
|
basename;
|
1181
|
(* compiling instrumented lib + main *)
|
1182
|
C_backend_makefile.fprintf_dependencies fmt dependencies;
|
1183
|
fprintf
|
1184
|
fmt
|
1185
|
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
|
1186
|
%s_main_eacsl.o %a@."
|
1187
|
basename
|
1188
|
(pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
|
1189
|
(C_backend_makefile.compiled_dependencies dependencies)
|
1190
|
("${FRAMACEACSL}/e_acsl.c "
|
1191
|
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
1192
|
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
1193
|
basename
|
1194
|
(pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
|
1195
|
(C_backend_makefile.lib_dependencies dependencies);
|
1196
|
fprintf fmt "@."
|
1197
|
end
|
1198
|
|
1199
|
(* Local Variables: *)
|
1200
|
(* compile-command:"make -C ../../.." *)
|
1201
|
(* End: *)
|