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