|
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' ?(ghost = false) pp fmt x =
|
|
45
|
let op = if ghost then "" else "*" in
|
|
46
|
let cl = if ghost then "@" else "*" in
|
|
47
|
fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
|
|
48
|
|
|
49
|
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
|
|
50
|
|
|
51
|
let pp_requires pp fmt = fprintf fmt "requires %a;" pp
|
|
52
|
|
|
53
|
let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
|
|
54
|
|
|
55
|
let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
|
|
56
|
|
|
57
|
let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
|
|
58
|
|
|
59
|
let pp_assigns pp =
|
|
60
|
pp_comma_list
|
|
61
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
|
|
62
|
~pp_epilogue:pp_print_semicolon'
|
|
63
|
pp
|
|
64
|
|
|
65
|
let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
|
|
66
|
|
|
67
|
let pp_assert pp fmt = fprintf fmt "assert %a;" pp
|
|
68
|
|
|
69
|
let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
|
|
70
|
|
|
71
|
let pp_mem_valid pp_var fmt (name, var) =
|
|
72
|
fprintf fmt "%s_valid(%a)" name pp_var var
|
|
73
|
|
|
74
|
let pp_mem_valid' = pp_mem_valid pp_print_string
|
|
75
|
|
|
76
|
let pp_ref pp fmt = fprintf fmt "&%a" pp
|
|
77
|
|
|
78
|
let pp_ref' = pp_ref pp_print_string
|
|
79
|
|
|
80
|
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
|
|
81
|
fprintf fmt "%a->%a" pp_ptr ptr pp_field field
|
|
82
|
|
|
83
|
let pp_indirect' = pp_indirect pp_print_string pp_print_string
|
|
84
|
|
|
85
|
let pp_access pp_stru pp_field fmt (stru, field) =
|
|
86
|
fprintf fmt "%a.%a" pp_stru stru pp_field field
|
|
87
|
|
|
88
|
let pp_access' = pp_access pp_print_string pp_print_string
|
|
89
|
|
|
90
|
let pp_var_decl fmt v = pp_print_string fmt v.var_id
|
|
91
|
|
|
92
|
let pp_reg self fmt field =
|
|
93
|
pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
|
|
94
|
|
|
95
|
let pp_true fmt () = pp_print_string fmt "\\true"
|
|
96
|
|
|
97
|
let pp_true_c_bool fmt () = pp_print_string fmt "(_Bool) 1"
|
|
98
|
|
|
99
|
let pp_false fmt () = pp_print_string fmt "\\false"
|
|
100
|
|
|
101
|
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
|
|
102
|
|
|
103
|
let pp_null fmt () = pp_print_string fmt "\\null"
|
|
104
|
|
|
105
|
let pp_stdout fmt () = pp_print_string fmt "stdout"
|
|
106
|
|
|
107
|
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
|
|
108
|
|
|
109
|
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
|
|
110
|
|
|
111
|
let find_machine f = List.find (fun m -> m.mname.node_id = f)
|
|
112
|
|
|
113
|
let instances machines m =
|
|
114
|
let open List in
|
|
115
|
let grow paths i td mems =
|
|
116
|
match paths with
|
|
117
|
| [] ->
|
|
118
|
[ [ i, (td, mems) ] ]
|
|
119
|
| _ ->
|
|
120
|
map (cons (i, (td, mems))) paths
|
|
121
|
in
|
|
122
|
let rec aux paths m =
|
|
123
|
map
|
|
124
|
(fun (i, (td, _)) ->
|
|
125
|
try
|
|
126
|
let m = find_machine (node_name td) machines in
|
|
127
|
aux (grow paths i td m.mmemory) m
|
|
128
|
with Not_found -> grow paths i td [])
|
|
129
|
m.minstances
|
|
130
|
|> flatten
|
|
131
|
in
|
|
132
|
aux [] m |> map rev
|
|
133
|
|
|
134
|
let memories insts =
|
|
135
|
List.(
|
|
136
|
map
|
|
137
|
(fun path ->
|
|
138
|
let _, (_, mems) = hd (rev path) in
|
|
139
|
map (fun mem -> path, mem) mems)
|
|
140
|
insts
|
|
141
|
|> flatten)
|
|
142
|
|
|
143
|
let pp_instance ?(indirect = true) pp ptr =
|
|
144
|
pp_print_list
|
|
145
|
~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
|
|
146
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
|
147
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
|
148
|
|
|
149
|
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
|
|
150
|
pp_access
|
|
151
|
((if indirect then pp_indirect else pp_access)
|
|
152
|
(pp_instance ~indirect pp_print_string ptr)
|
|
153
|
pp_print_string)
|
|
154
|
pp_var_decl
|
|
155
|
fmt
|
|
156
|
((path, "_reg"), mem)
|
|
157
|
|
|
158
|
let prefixes l =
|
|
159
|
let rec pref acc = function
|
|
160
|
| x :: l ->
|
|
161
|
pref ([ x ] :: List.map (List.cons x) acc) l
|
|
162
|
| [] ->
|
|
163
|
acc
|
|
164
|
in
|
|
165
|
pref [] (List.rev l)
|
|
166
|
|
|
167
|
let powerset_instances paths =
|
|
168
|
List.map prefixes paths |> List.flatten |> remove_duplicates
|
|
169
|
|
|
170
|
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
|
|
171
|
fprintf
|
|
172
|
fmt
|
|
173
|
"\\separated(@[<v>%a, %a%a%a@])"
|
|
174
|
pp_self
|
|
175
|
self
|
|
176
|
pp_mem
|
|
177
|
mem
|
|
178
|
(pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))
|
|
179
|
paths
|
|
180
|
(pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
|
|
181
|
ptrs
|
|
182
|
|
|
183
|
let pp_separated' self mem fmt (paths, ptrs) =
|
|
184
|
pp_separated
|
|
185
|
pp_print_string
|
|
186
|
pp_print_string
|
|
187
|
pp_var_decl
|
|
188
|
fmt
|
|
189
|
(self, mem, paths, ptrs)
|
|
190
|
|
|
191
|
let pp_separated'' =
|
|
192
|
pp_comma_list
|
|
193
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
|
|
194
|
~pp_epilogue:pp_print_cpar
|
|
195
|
pp_var_decl
|
|
196
|
|
|
197
|
let pp_forall pp_l pp_r fmt (l, r) =
|
|
198
|
fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
|
|
199
|
|
|
200
|
let pp_exists pp_l pp_r fmt (l, r) =
|
|
201
|
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
|
|
202
|
|
|
203
|
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
|
|
204
|
|
|
205
|
let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r
|
|
206
|
|
|
207
|
let pp_implies pp_l pp_r fmt (l, r) =
|
|
208
|
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
|
|
209
|
|
|
210
|
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
|
|
211
|
|
|
212
|
let pp_and_l pp_v fmt =
|
|
213
|
pp_print_list
|
|
214
|
~pp_open_box:pp_open_vbox0
|
|
215
|
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
|
|
216
|
~pp_nil:pp_true
|
|
217
|
pp_v
|
|
218
|
fmt
|
|
219
|
|
|
220
|
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
|
|
221
|
|
|
222
|
let pp_or_l pp_v fmt =
|
|
223
|
pp_print_list
|
|
224
|
~pp_open_box:pp_open_vbox0
|
|
225
|
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
|
|
226
|
pp_v
|
|
227
|
fmt
|
|
228
|
|
|
229
|
let pp_not pp fmt = fprintf fmt "!%a" pp
|
|
230
|
|
|
231
|
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
|
|
232
|
|
|
233
|
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
|
|
234
|
|
|
235
|
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
|
|
236
|
|
|
237
|
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
|
|
238
|
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
|
|
239
|
|
|
240
|
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
|
|
241
|
|
|
242
|
let pp_initialization pp_mem fmt (name, mem) =
|
|
243
|
fprintf fmt "%s_initialization(%a)" name pp_mem mem
|
|
244
|
|
|
245
|
let pp_init pp_mem fmt (name, mem) = fprintf fmt "%s_init(%a)" name pp_mem mem
|
|
246
|
|
|
247
|
let pp_initialization' = pp_initialization pp_print_string
|
|
248
|
|
|
249
|
let pp_local m =
|
|
250
|
pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
|
|
251
|
|
|
252
|
let pp_locals m =
|
|
253
|
pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
|
|
254
|
|
|
255
|
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
|
|
256
|
|
|
257
|
let pp_basic_assign_spec ?(pp_op=pp_equal) pp_l pp_r fmt typ var_name value =
|
|
258
|
if Types.is_real_type typ && !Options.mpfr then assert false
|
|
259
|
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
|
|
260
|
else pp_op pp_l pp_r fmt (var_name, value)
|
|
261
|
|
|
262
|
let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
|
|
263
|
(var_type, var_name, value) =
|
|
264
|
let depth = expansion_depth value in
|
|
265
|
let loop_vars = mk_loop_variables m var_type depth in
|
|
266
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
|
267
|
let aux typ fmt vars =
|
|
268
|
match vars with
|
|
269
|
| [] ->
|
|
270
|
pp_basic_assign_spec ?pp_op
|
|
271
|
(pp_value_suffix
|
|
272
|
~indirect:indirect_l
|
|
273
|
m
|
|
274
|
self_l
|
|
275
|
var_type
|
|
276
|
loop_vars
|
|
277
|
pp_var_l)
|
|
278
|
(pp_value_suffix
|
|
279
|
~indirect:indirect_r
|
|
280
|
m
|
|
281
|
self_r
|
|
282
|
var_type
|
|
283
|
loop_vars
|
|
284
|
pp_var_r)
|
|
285
|
fmt
|
|
286
|
typ
|
|
287
|
var_name
|
|
288
|
value
|
|
289
|
| (_d, LVar _i) :: _q ->
|
|
290
|
assert false
|
|
291
|
(* let typ' = Types.array_element_type typ in
|
|
292
|
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
293
|
* i i i pp_c_dimension d i
|
|
294
|
* (aux typ') q *)
|
|
295
|
| (_d, LInt _r) :: _q ->
|
|
296
|
assert false
|
|
297
|
(* let typ' = Types.array_element_type typ in
|
|
298
|
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
|
299
|
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
|
300
|
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
|
|
301
|
| _ ->
|
|
302
|
assert false
|
|
303
|
in
|
|
304
|
reset_loop_counter ();
|
|
305
|
aux var_type fmt reordered_loop_vars
|
|
306
|
|
|
307
|
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
|
|
308
|
fprintf
|
|
309
|
fmt
|
|
310
|
"%s_pack%a(@[<hov>%a,@ %a@])"
|
|
311
|
name
|
|
312
|
(pp_print_option pp_print_int)
|
|
313
|
i
|
|
314
|
pp_mem
|
|
315
|
mem
|
|
316
|
pp_self
|
|
317
|
self
|
|
318
|
|
|
319
|
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
|
|
320
|
pp_memory_pack_aux
|
|
321
|
?i:mp.mpindex
|
|
322
|
pp_mem
|
|
323
|
pp_self
|
|
324
|
fmt
|
|
325
|
(mp.mpname.node_id, mem, self)
|
|
326
|
|
|
327
|
let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt
|
|
328
|
(name, vars, mem_in, mem_out) =
|
|
329
|
fprintf
|
|
330
|
fmt
|
|
331
|
"%s_transition%a(@[<hov>%t%a%t@])"
|
|
332
|
name
|
|
333
|
(pp_print_option pp_print_int)
|
|
334
|
i
|
|
335
|
(fun fmt -> if not stateless then pp_mem_in fmt mem_in)
|
|
336
|
(pp_comma_list
|
|
337
|
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
|
|
338
|
pp_var)
|
|
339
|
vars
|
|
340
|
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
|
|
341
|
|
|
342
|
let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out)
|
|
343
|
=
|
|
344
|
pp_transition_aux
|
|
345
|
?i:t.tindex
|
|
346
|
stateless
|
|
347
|
pp_mem_in
|
|
348
|
pp_mem_out
|
|
349
|
pp_var
|
|
350
|
fmt
|
|
351
|
(t.tname.node_id, t.tvars, mem_in, mem_out)
|
|
352
|
|
|
353
|
let pp_transition_aux' ?i m =
|
|
354
|
let stateless = fst (get_stateless_status m) in
|
|
355
|
pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->
|
|
356
|
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
|
|
357
|
|
|
358
|
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
|
|
359
|
fprintf
|
|
360
|
fmt
|
|
361
|
"%s_reset_cleared(@[<hov>%a,@ %a@])"
|
|
362
|
name
|
|
363
|
pp_mem_in
|
|
364
|
mem_in
|
|
365
|
pp_mem_out
|
|
366
|
mem_out
|
|
367
|
|
|
368
|
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
|
|
369
|
|
|
370
|
let pp_functional_update mems insts fmt mem =
|
|
371
|
let rec aux fmt = function
|
|
372
|
| [] ->
|
|
373
|
pp_print_string fmt mem
|
|
374
|
| (x, is_mem) :: fields ->
|
|
375
|
fprintf
|
|
376
|
fmt
|
|
377
|
"{ @[<hov>%a@ \\with .%s%s = %s@] }"
|
|
378
|
aux
|
|
379
|
fields
|
|
380
|
(if is_mem then "_reg." else "")
|
|
381
|
x
|
|
382
|
x
|
|
383
|
in
|
|
384
|
aux
|
|
385
|
fmt
|
|
386
|
(List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
|
|
387
|
@ List.map (fun x -> x, true) (Utils.ISet.elements mems))
|
|
388
|
|
|
389
|
module PrintSpec = struct
|
|
390
|
type mode =
|
|
391
|
| MemoryPackMode
|
|
392
|
| TransitionMode
|
|
393
|
| TransitionFootprintMode
|
|
394
|
| ResetIn
|
|
395
|
| ResetOut
|
|
396
|
| InstrMode of ident
|
|
397
|
|
|
398
|
let pp_reg mem fmt = function
|
|
399
|
| ResetFlag ->
|
|
400
|
fprintf fmt "%s.%s" mem reset_flag_name
|
|
401
|
| StateVar x ->
|
|
402
|
fprintf fmt "%s.%a" mem pp_var_decl x
|
|
403
|
|
|
404
|
let pp_expr :
|
|
405
|
type a.
|
|
406
|
?test_output:bool ->
|
|
407
|
machine_t ->
|
|
408
|
ident ->
|
|
409
|
formatter ->
|
|
410
|
(value_t, a) expression_t ->
|
|
411
|
unit =
|
|
412
|
fun ?(test_output = false) m mem fmt -> function
|
|
413
|
| Val v ->
|
|
414
|
pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
|
|
415
|
| Tag t ->
|
|
416
|
pp_print_string fmt t
|
|
417
|
| Var v ->
|
|
418
|
pp_var_decl fmt v
|
|
419
|
| Memory r ->
|
|
420
|
pp_reg mem fmt r
|
|
421
|
|
|
422
|
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
|
|
423
|
let test_output, mem_update =
|
|
424
|
match mode with
|
|
425
|
| InstrMode _ ->
|
|
426
|
true, false
|
|
427
|
| TransitionFootprintMode ->
|
|
428
|
false, true
|
|
429
|
| _ ->
|
|
430
|
false, false
|
|
431
|
in
|
|
432
|
let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
|
|
433
|
=
|
|
434
|
fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
|
|
435
|
in
|
|
436
|
match p with
|
|
437
|
| Transition (stateless, f, inst, i, vars, r, mems, insts) ->
|
|
438
|
let pp_mem_in, pp_mem_out =
|
|
439
|
match inst with
|
|
440
|
| None ->
|
|
441
|
( pp_print_string,
|
|
442
|
if mem_update then pp_functional_update mems insts
|
|
443
|
else pp_print_string )
|
|
444
|
| Some inst ->
|
|
445
|
( (fun fmt mem_in ->
|
|
446
|
if r then pp_print_string fmt mem_in
|
|
447
|
else pp_access' fmt (mem_in, inst)),
|
|
448
|
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
|
|
449
|
in
|
|
450
|
pp_transition_aux
|
|
451
|
?i
|
|
452
|
stateless
|
|
453
|
pp_mem_in
|
|
454
|
pp_mem_out
|
|
455
|
(pp_expr test_output)
|
|
456
|
fmt
|
|
457
|
(f, vars, mem_in', mem_out')
|
|
458
|
| Reset (_f, inst, r) ->
|
|
459
|
pp_ite
|
|
460
|
(pp_c_val m mem_in (pp_c_var_read m))
|
|
461
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
|
462
|
(pp_equal pp_print_string pp_access')
|
|
463
|
fmt
|
|
464
|
(r, (mem_out, 1), (mem_out, (mem_in, inst)))
|
|
465
|
| MemoryPack (f, inst, i) ->
|
|
466
|
let pp_mem, pp_self =
|
|
467
|
match inst with
|
|
468
|
| None ->
|
|
469
|
pp_print_string, pp_print_string
|
|
470
|
| Some inst ->
|
|
471
|
( (fun fmt mem -> pp_access' fmt (mem, inst)),
|
|
472
|
fun fmt self -> pp_indirect' fmt (self, inst) )
|
|
473
|
in
|
|
474
|
pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
|
|
475
|
| ResetCleared f ->
|
|
476
|
pp_reset_cleared' fmt (f, mem_in, mem_out)
|
|
477
|
(* fprintf fmt "ResetCleared_%a" pp_print_string f *)
|
|
478
|
| Initialization ->
|
|
479
|
()
|
|
480
|
|
|
481
|
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
|
|
482
|
|
|
483
|
let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
|
|
484
|
| Val v ->
|
|
485
|
v
|
|
486
|
| Tag t ->
|
|
487
|
id_to_tag t
|
|
488
|
| Var v ->
|
|
489
|
vdecl_to_val v
|
|
490
|
| Memory (StateVar v) ->
|
|
491
|
vdecl_to_val v
|
|
492
|
| Memory ResetFlag ->
|
|
493
|
vdecl_to_val reset_flag
|
|
494
|
|
|
495
|
let find_arrow m =
|
|
496
|
try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
|
|
497
|
with Not_found ->
|
|
498
|
eprintf "Internal error: arrow not found";
|
|
499
|
raise Not_found
|
|
500
|
|
|
501
|
let rec has_memory_val m v =
|
|
502
|
let has_mem = has_memory_val m in
|
|
503
|
match v.value_desc with
|
|
504
|
| Var v ->
|
|
505
|
is_memory m v
|
|
506
|
| Array vl | Fun (_, vl) ->
|
|
507
|
List.exists has_mem vl
|
|
508
|
| Access (t, i) | Power (t, i) ->
|
|
509
|
has_mem t || has_mem i
|
|
510
|
| _ ->
|
|
511
|
false
|
|
512
|
|
|
513
|
let has_memory : type a. machine_t -> (value_t, a) expression_t -> bool =
|
|
514
|
fun m -> function Val v -> has_memory_val m v | _ -> false
|
|
515
|
|
|
516
|
let pp_spec mode m =
|
|
517
|
let rec pp_spec mode fmt f =
|
|
518
|
let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
|
|
519
|
let self = mk_self m in
|
|
520
|
let mem = mk_mem m in
|
|
521
|
let mem_in = mk_mem_in m in
|
|
522
|
let mem_out = mk_mem_out m in
|
|
523
|
let mem_reset = mk_mem_reset m in
|
|
524
|
match mode with
|
|
525
|
| MemoryPackMode ->
|
|
526
|
self, self, true, mem, mem, false
|
|
527
|
| TransitionMode ->
|
|
528
|
mem_in, mem_in, false, mem_out, mem_out, false
|
|
529
|
| TransitionFootprintMode ->
|
|
530
|
mem_in, mem_in, false, mem_out, mem_out, false
|
|
531
|
| ResetIn ->
|
|
532
|
mem_reset, mem_reset, false, mem_out, mem_out, false
|
|
533
|
| ResetOut ->
|
|
534
|
mem_in, mem_in, false, mem_reset, mem_reset, false
|
|
535
|
| InstrMode self ->
|
|
536
|
let mem = "*" ^ mem in
|
|
537
|
fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
|
|
538
|
self, flush_str_formatter (), false, mem, mem, false
|
|
539
|
in
|
|
540
|
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
|
541
|
fun fmt e -> pp_expr m mem_out fmt e
|
|
542
|
in
|
|
543
|
let pp_spec' = pp_spec mode in
|
|
544
|
match f with
|
|
545
|
| True ->
|
|
546
|
pp_true fmt ()
|
|
547
|
| False ->
|
|
548
|
pp_false fmt ()
|
|
549
|
| Equal (a, b) ->
|
|
550
|
let pp_eq fmt () =
|
|
551
|
pp_assign_spec
|
|
552
|
m
|
|
553
|
mem_out
|
|
554
|
(pp_c_var_read ~test_output:false m)
|
|
555
|
indirect_l
|
|
556
|
mem_in
|
|
557
|
(pp_c_var_read ~test_output:false m)
|
|
558
|
indirect_r
|
|
559
|
fmt
|
|
560
|
(type_of_l_value a, val_of_expr a, val_of_expr b)
|
|
561
|
in
|
|
562
|
if has_memory m b then
|
|
563
|
let inst = find_arrow m in
|
|
564
|
pp_paren
|
|
565
|
(pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
|
|
566
|
fmt
|
|
567
|
((Arrow.arrow_id, (mem_in, inst)), ())
|
|
568
|
else pp_eq fmt ()
|
|
569
|
| GEqual (a, b) ->
|
|
570
|
pp_assign_spec ~pp_op:pp_gequal
|
|
571
|
m
|
|
572
|
mem_out
|
|
573
|
(pp_c_var_read ~test_output:false m)
|
|
574
|
indirect_l
|
|
575
|
mem_in
|
|
576
|
(pp_c_var_read ~test_output:false m)
|
|
577
|
indirect_r
|
|
578
|
fmt
|
|
579
|
(type_of_l_value a, val_of_expr a, val_of_expr b)
|
|
580
|
| And fs ->
|
|
581
|
pp_and_l pp_spec' fmt fs
|
|
582
|
| Or fs ->
|
|
583
|
pp_or_l pp_spec' fmt fs
|
|
584
|
| Imply (a, b) ->
|
|
585
|
pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
|
|
586
|
| Exists (xs, a) ->
|
|
587
|
pp_exists (pp_locals m) pp_spec' fmt (xs, a)
|
|
588
|
| Forall (xs, a) ->
|
|
589
|
pp_forall (pp_locals m) pp_spec' fmt (xs, a)
|
|
590
|
| Ternary (e, a, b) ->
|
|
591
|
pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
|
|
592
|
| Predicate p ->
|
|
593
|
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
|
|
594
|
| StateVarPack ResetFlag ->
|
|
595
|
let r = vdecl_to_val reset_flag in
|
|
596
|
pp_assign_spec
|
|
597
|
m
|
|
598
|
mem_out
|
|
599
|
(pp_c_var_read ~test_output:false m)
|
|
600
|
indirect_l
|
|
601
|
mem_in
|
|
602
|
(pp_c_var_read ~test_output:false m)
|
|
603
|
indirect_r
|
|
604
|
fmt
|
|
605
|
(Type_predef.type_bool, r, r)
|
|
606
|
| StateVarPack (StateVar v) ->
|
|
607
|
let v' = vdecl_to_val v in
|
|
608
|
let inst = find_arrow m in
|
|
609
|
pp_paren
|
|
610
|
(pp_implies
|
|
611
|
(pp_not (pp_initialization pp_access'))
|
|
612
|
(pp_assign_spec
|
|
613
|
m
|
|
614
|
mem_out
|
|
615
|
(pp_c_var_read ~test_output:false m)
|
|
616
|
indirect_l
|
|
617
|
mem_in
|
|
618
|
(pp_c_var_read ~test_output:false m)
|
|
619
|
indirect_r))
|
|
620
|
fmt
|
|
621
|
((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
|
|
622
|
| ExistsMem (f, rc, tr) ->
|
|
623
|
pp_exists
|
|
624
|
(pp_machine_decl' ~ghost:true)
|
|
625
|
(pp_and (pp_spec ResetOut) (pp_spec ResetIn))
|
|
626
|
fmt
|
|
627
|
((f, mk_mem_reset m), (rc, tr))
|
|
628
|
| Value v ->
|
|
629
|
pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
|
|
630
|
in
|
|
631
|
|
|
632
|
pp_spec mode
|
|
633
|
end
|
|
634
|
|
|
635
|
let pp_predicate pp_l pp_r fmt (l, r) =
|
|
636
|
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
|
|
637
|
|
|
638
|
let pp_lemma pp_l pp_r fmt (l, r) =
|
|
639
|
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
|
|
640
|
|
|
641
|
let pp_axiomatic pp_l pp_r fmt (l, r) =
|
|
642
|
fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
|
|
643
|
|
|
644
|
let pp_axiom pp_l pp_r fmt (l, r) =
|
|
645
|
fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
|
|
646
|
|
|
647
|
let pp_mem_valid_def fmt m =
|
|
648
|
if not (fst (get_stateless_status m) || m.mis_contract) then
|
|
649
|
let name = m.mname.node_id in
|
|
650
|
let self = mk_self m in
|
|
651
|
pp_acsl
|
|
652
|
(pp_predicate
|
|
653
|
(pp_mem_valid (pp_machine_decl pp_ptr))
|
|
654
|
(pp_and
|
|
655
|
(pp_and_l (fun fmt (inst, (td, _)) ->
|
|
656
|
if Arrow.td_is_arrow td then
|
|
657
|
pp_valid pp_indirect' fmt [ self, inst ]
|
|
658
|
else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
|
|
659
|
(pp_valid pp_print_string)))
|
|
660
|
fmt
|
|
661
|
((name, (name, self)), (m.minstances, [ self ]))
|
|
662
|
|
|
663
|
let pp_memory_pack_def m fmt mp =
|
|
664
|
if not (fst (get_stateless_status m) || m.mis_contract) then
|
|
665
|
let name = mp.mpname.node_id in
|
|
666
|
let self = mk_self m in
|
|
667
|
let mem = mk_mem m in
|
|
668
|
pp_acsl_cut
|
|
669
|
(pp_predicate
|
|
670
|
(pp_memory_pack
|
|
671
|
(pp_machine_decl' ~ghost:true)
|
|
672
|
(pp_machine_decl pp_ptr))
|
|
673
|
(PrintSpec.pp_spec MemoryPackMode m))
|
|
674
|
fmt
|
|
675
|
((mp, (name, mem), (name, self)), mp.mpformula)
|
|
676
|
|
|
677
|
let pp_machine_ghost_struct fmt m =
|
|
678
|
pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
|
|
679
|
|
|
680
|
let pp_memory_pack_defs fmt m =
|
|
681
|
if not (fst (get_stateless_status m)) then
|
|
682
|
fprintf
|
|
683
|
fmt
|
|
684
|
"%a@,%a"
|
|
685
|
pp_machine_ghost_struct
|
|
686
|
m
|
|
687
|
(pp_print_list
|
|
688
|
~pp_sep:pp_print_nothing
|
|
689
|
~pp_epilogue:pp_print_cut
|
|
690
|
~pp_open_box:pp_open_vbox0
|
|
691
|
(pp_memory_pack_def m))
|
|
692
|
m.mspec.mmemory_packs
|
|
693
|
|
|
694
|
let pp_transition_def m fmt t =
|
|
695
|
let name = t.tname.node_id in
|
|
696
|
let mem_in = mk_mem_in m in
|
|
697
|
let mem_out = mk_mem_out m in
|
|
698
|
let stateless = fst (get_stateless_status m) in
|
|
699
|
pp_acsl
|
|
700
|
(pp_predicate
|
|
701
|
(pp_transition
|
|
702
|
stateless
|
|
703
|
(pp_machine_decl' ~ghost:true)
|
|
704
|
(pp_machine_decl' ~ghost:true)
|
|
705
|
(pp_local m))
|
|
706
|
(PrintSpec.pp_spec TransitionMode m))
|
|
707
|
fmt
|
|
708
|
((t, (name, mem_in), (name, mem_out)), t.tformula)
|
|
709
|
|
|
710
|
let pp_transition_defs fmt m =
|
|
711
|
pp_print_list
|
|
712
|
~pp_epilogue:pp_print_cut
|
|
713
|
~pp_open_box:pp_open_vbox0
|
|
714
|
(pp_transition_def m)
|
|
715
|
fmt
|
|
716
|
m.mspec.mtransitions
|
|
717
|
|
|
718
|
let pp_transition_footprint fmt t =
|
|
719
|
fprintf
|
|
720
|
fmt
|
|
721
|
"%s_transition%a_footprint"
|
|
722
|
t.tname.node_id
|
|
723
|
(pp_print_option pp_print_int)
|
|
724
|
t.tindex
|
|
725
|
|
|
726
|
let pp_transition_footprint_lemma m fmt t =
|
|
727
|
let name = t.tname.node_id in
|
|
728
|
let mem_in = mk_mem_in m in
|
|
729
|
let mem_out = mk_mem_out m in
|
|
730
|
let stateless = fst (get_stateless_status m) in
|
|
731
|
let mems =
|
|
732
|
ISet.(
|
|
733
|
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
|
|
734
|
in
|
|
735
|
let insts =
|
|
736
|
IMap.(
|
|
737
|
diff
|
|
738
|
(of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
|
|
739
|
t.tinst_footprint)
|
|
740
|
in
|
|
741
|
let memories =
|
|
742
|
List.map
|
|
743
|
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
|
|
744
|
(List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
|
|
745
|
in
|
|
746
|
let mems_empty = ISet.is_empty mems in
|
|
747
|
let insts_empty = IMap.is_empty insts in
|
|
748
|
let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
|
|
749
|
let tr ?mems ?insts () =
|
|
750
|
Spec_common.mk_transition
|
|
751
|
?mems
|
|
752
|
?insts
|
|
753
|
?i:t.tindex
|
|
754
|
stateless
|
|
755
|
name
|
|
756
|
(vdecls_to_vals t.tvars)
|
|
757
|
in
|
|
758
|
if not ((mems_empty && insts_empty) || m.mis_contract) then
|
|
759
|
pp_acsl_cut
|
|
760
|
(pp_lemma
|
|
761
|
pp_transition_footprint
|
|
762
|
(pp_forall
|
|
763
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
|
764
|
((if insts_empty then fun pp fmt (_, x) -> pp fmt x
|
|
765
|
else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
|
|
766
|
((if mems_empty then fun pp fmt (_, x) -> pp fmt x
|
|
767
|
else pp_forall (pp_locals m))
|
|
768
|
(PrintSpec.pp_spec TransitionFootprintMode m)))))
|
|
769
|
fmt
|
|
770
|
( t,
|
|
771
|
( (m.mname.node_id, [ mem_in; mem_out ]),
|
|
772
|
( instances,
|
|
773
|
(memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
|
|
774
|
)
|
|
775
|
|
|
776
|
let pp_transition_footprint_lemmas fmt m =
|
|
777
|
pp_print_list
|
|
778
|
~pp_epilogue:pp_print_cut
|
|
779
|
~pp_open_box:pp_open_vbox0
|
|
780
|
~pp_sep:pp_print_nothing
|
|
781
|
(pp_transition_footprint_lemma m)
|
|
782
|
fmt
|
|
783
|
(List.filter
|
|
784
|
(fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
|
785
|
m.mspec.mtransitions)
|
|
786
|
|
|
787
|
let pp_initialization_def fmt m =
|
|
788
|
if not (fst (get_stateless_status m)) then
|
|
789
|
let name = m.mname.node_id in
|
|
790
|
let mem_in = mk_mem_in m in
|
|
791
|
pp_acsl
|
|
792
|
(pp_predicate
|
|
793
|
(pp_initialization (pp_machine_decl' ~ghost:true))
|
|
794
|
(pp_and_l (fun fmt (i, (td, _)) ->
|
|
795
|
if Arrow.td_is_arrow td then
|
|
796
|
pp_initialization pp_access' fmt (node_name td, (mem_in, i))
|
|
797
|
else
|
|
798
|
pp_equal
|
|
799
|
(pp_reset_flag ~indirect:false pp_access')
|
|
800
|
pp_print_int
|
|
801
|
fmt
|
|
802
|
((mem_in, i), 1))))
|
|
803
|
fmt
|
|
804
|
((name, (name, mem_in)), m.minstances)
|
|
805
|
|
|
806
|
let pp_reset_cleared_def fmt m =
|
|
807
|
if not (fst (get_stateless_status m)) then
|
|
808
|
let name = m.mname.node_id in
|
|
809
|
let mem_in = mk_mem_in m in
|
|
810
|
let mem_out = mk_mem_out m in
|
|
811
|
pp_acsl
|
|
812
|
(pp_predicate
|
|
813
|
(pp_reset_cleared
|
|
814
|
(pp_machine_decl' ~ghost:true)
|
|
815
|
(pp_machine_decl' ~ghost:true))
|
|
816
|
(pp_ite
|
|
817
|
(pp_reset_flag' ~indirect:false)
|
|
818
|
(pp_and
|
|
819
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
|
820
|
pp_initialization')
|
|
821
|
(pp_equal pp_print_string pp_print_string)))
|
|
822
|
fmt
|
|
823
|
( (name, (name, mem_in), (name, mem_out)),
|
|
824
|
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
|
|
825
|
|
|
826
|
let pp_register_chain ?(indirect = true) ptr =
|
|
827
|
pp_print_list
|
|
828
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
|
829
|
~pp_epilogue:(fun fmt () ->
|
|
830
|
fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
|
|
831
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
|
832
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
|
833
|
|
|
834
|
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
|
|
835
|
pp_print_list
|
|
836
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
|
837
|
~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
|
|
838
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
|
839
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
|
840
|
fmt
|
|
841
|
mems
|
|
842
|
|
|
843
|
let pp_arrow_reset_ghost mem fmt inst =
|
|
844
|
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
|
|
845
|
|
|
846
|
module GhostProto : MODIFIERS_GHOST_PROTO = struct
|
|
847
|
let pp_ghost_parameters ?(cut = true) fmt vs =
|
|
848
|
fprintf
|
|
849
|
fmt
|
|
850
|
"%a%a"
|
|
851
|
(if cut then pp_print_cut else pp_print_nothing)
|
|
852
|
()
|
|
853
|
(pp_acsl_line'
|
|
854
|
(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
|
|
855
|
vs
|
|
856
|
end
|
|
857
|
|
|
858
|
module HdrMod = struct
|
|
859
|
module GhostProto = GhostProto
|
|
860
|
|
|
861
|
let pp_machine_decl_prefix _ _ = ()
|
|
862
|
|
|
863
|
let pp_import_arrow fmt () =
|
|
864
|
fprintf
|
|
865
|
fmt
|
|
866
|
"#include \"%s/arrow_spec.h%s\""
|
|
867
|
(Arrow.arrow_top_decl ()).top_decl_owner
|
|
868
|
(if !Options.cpp then "pp" else "")
|
|
869
|
|
|
870
|
let pp_predicates fmt machines =
|
|
871
|
let pp_preds comment pp =
|
|
872
|
pp_print_list
|
|
873
|
~pp_open_box:pp_open_vbox0
|
|
874
|
~pp_prologue:(pp_print_endcut comment)
|
|
875
|
pp
|
|
876
|
~pp_epilogue:pp_print_cutcut
|
|
877
|
in
|
|
878
|
fprintf
|
|
879
|
fmt
|
|
880
|
"%a%a"
|
|
881
|
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
|
|
882
|
machines
|
|
883
|
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
|
|
884
|
machines
|
|
885
|
|
|
886
|
let pp_machine_alloc_decl fmt m =
|
|
887
|
pp_machine_decl_prefix fmt m;
|
|
888
|
if not (fst (get_stateless_status m)) then
|
|
889
|
if !Options.static_mem then
|
|
890
|
(* Static allocation *)
|
|
891
|
let macro = m, mk_attribute m, mk_instance m in
|
|
892
|
fprintf
|
|
893
|
fmt
|
|
894
|
"%a@,%a@,%a"
|
|
895
|
(pp_static_declare_macro ~ghost:true)
|
|
896
|
macro
|
|
897
|
(pp_static_link_macro ~ghost:true)
|
|
898
|
macro
|
|
899
|
(pp_static_alloc_macro ~ghost:true)
|
|
900
|
macro
|
|
901
|
else
|
|
902
|
(* Dynamic allocation *)
|
|
903
|
(* TODO: handle dynamic alloc *)
|
|
904
|
assert false
|
|
905
|
(* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
|
|
906
|
* (m.mname.node_id, m.mstatic)
|
|
907
|
* pp_dealloc_prototype m.mname.node_id *)
|
|
908
|
end
|
|
909
|
|
|
910
|
module SrcMod = struct
|
|
911
|
module GhostProto = GhostProto
|
|
912
|
|
|
913
|
let pp_predicates fmt machines =
|
|
914
|
let pp_preds comment pp =
|
|
915
|
pp_print_list
|
|
916
|
~pp_open_box:pp_open_vbox0
|
|
917
|
~pp_prologue:(pp_print_endcut comment)
|
|
918
|
pp
|
|
919
|
~pp_epilogue:pp_print_cutcut
|
|
920
|
in
|
|
921
|
fprintf
|
|
922
|
fmt
|
|
923
|
"%a%a%a%a%a%a"
|
|
924
|
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
|
|
925
|
machines
|
|
926
|
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
|
|
927
|
machines
|
|
928
|
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
|
|
929
|
machines
|
|
930
|
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
|
|
931
|
machines
|
|
932
|
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
|
|
933
|
machines
|
|
934
|
(pp_preds
|
|
935
|
"/* ACSL transition memory footprints lemmas */"
|
|
936
|
pp_transition_footprint_lemmas)
|
|
937
|
machines
|
|
938
|
|
|
939
|
let pp_clear_reset_spec fmt self mem m =
|
|
940
|
let name = m.mname.node_id in
|
|
941
|
let arws, narws =
|
|
942
|
List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
|
|
943
|
in
|
|
944
|
let mk_insts = List.map (fun x -> [ x ]) in
|
|
945
|
pp_acsl_cut
|
|
946
|
(fun fmt () ->
|
|
947
|
fprintf
|
|
948
|
fmt
|
|
949
|
"%a@,\
|
|
950
|
%a@,\
|
|
951
|
%a@,\
|
|
952
|
%a@,\
|
|
953
|
%a@,\
|
|
954
|
%a@,\
|
|
955
|
%a@,\
|
|
956
|
%a@,\
|
|
957
|
%a@,\
|
|
958
|
%a@,\
|
|
959
|
@[<v 2>behavior reset:@;\
|
|
960
|
%a@,\
|
|
961
|
%a@]@,\
|
|
962
|
@[<v 2>behavior no_reset:@;\
|
|
963
|
%a@,\
|
|
964
|
%a@]@,\
|
|
965
|
complete behaviors;@,\
|
|
966
|
disjoint behaviors;"
|
|
967
|
(pp_requires pp_mem_valid')
|
|
968
|
(name, self)
|
|
969
|
(pp_requires (pp_separated' self mem))
|
|
970
|
(mk_insts m.minstances, [])
|
|
971
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
|
972
|
(name, mem, self)
|
|
973
|
(pp_ensures
|
|
974
|
(pp_memory_pack_aux
|
|
975
|
~i:(List.length m.mspec.mmemory_packs - 2)
|
|
976
|
pp_ptr
|
|
977
|
pp_print_string))
|
|
978
|
(name, mem, self)
|
|
979
|
(pp_assigns pp_reset_flag')
|
|
980
|
[ self ]
|
|
981
|
(pp_assigns (pp_register_chain self))
|
|
982
|
(mk_insts arws)
|
|
983
|
(pp_assigns (pp_reset_flag_chain self))
|
|
984
|
(mk_insts narws)
|
|
985
|
(pp_assigns pp_reset_flag')
|
|
986
|
[ mem ]
|
|
987
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
|
988
|
(mk_insts arws)
|
|
989
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
|
990
|
(mk_insts narws)
|
|
991
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
|
992
|
(mem, 1)
|
|
993
|
(pp_ensures (pp_initialization pp_ptr))
|
|
994
|
(name, mem)
|
|
995
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
|
996
|
(mem, 0)
|
|
997
|
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
|
|
998
|
(mem, mem))
|
|
999
|
fmt
|
|
1000
|
()
|
|
1001
|
|
|
1002
|
let pp_set_reset_spec fmt self mem m =
|
|
1003
|
let name = m.mname.node_id in
|
|
1004
|
pp_acsl_cut
|
|
1005
|
(fun fmt () ->
|
|
1006
|
fprintf
|
|
1007
|
fmt
|
|
1008
|
"%a@,%a@,%a"
|
|
1009
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
|
1010
|
(name, mem, self)
|
|
1011
|
(pp_ensures (pp_equal pp_reset_flag' pp_print_int))
|
|
1012
|
(mem, 1)
|
|
1013
|
(pp_assigns pp_reset_flag')
|
|
1014
|
[ self; mem ])
|
|
1015
|
fmt
|
|
1016
|
()
|
|
1017
|
|
|
1018
|
let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
|
|
1019
|
|
|
1020
|
let pp_contract m fmt c =
|
|
1021
|
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
|
|
1022
|
|
|
1023
|
let contract_of machines m =
|
|
1024
|
match m.mspec.mnode_spec with
|
|
1025
|
| Some spec -> (
|
|
1026
|
match spec with
|
|
1027
|
| Contract c ->
|
|
1028
|
Some c, None
|
|
1029
|
| NodeSpec f -> (
|
|
1030
|
let m_f = find_machine f machines in
|
|
1031
|
match m_f.mspec.mnode_spec with
|
|
1032
|
| Some (Contract c) ->
|
|
1033
|
Some c, Some m_f
|
|
1034
|
| _ ->
|
|
1035
|
None, None))
|
|
1036
|
| None ->
|
|
1037
|
None, None
|
|
1038
|
|
|
1039
|
let pp_init_def fmt m =
|
|
1040
|
let name = m.mname.node_id in
|
|
1041
|
let mem = mk_mem m in
|
|
1042
|
pp_predicate
|
|
1043
|
(pp_init (pp_machine_decl' ~ghost:true))
|
|
1044
|
(pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
|
|
1045
|
fmt
|
|
1046
|
((name, (name, mem)), ((name, mem), mem))
|
|
1047
|
|
|
1048
|
let rename n x = sprintf "%s_%d" x n
|
|
1049
|
|
|
1050
|
let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
|
|
1051
|
|
|
1052
|
let rec rename_value n v =
|
|
1053
|
{
|
|
1054
|
v with
|
|
1055
|
value_desc =
|
|
1056
|
(match v.value_desc with
|
|
1057
|
| Machine_code_types.Var v ->
|
|
1058
|
Machine_code_types.Var (rename_var_decl n v)
|
|
1059
|
| Fun (f, vs) ->
|
|
1060
|
Fun (f, List.map (rename_value n) vs)
|
|
1061
|
| Array vs ->
|
|
1062
|
Array (List.map (rename_value n) vs)
|
|
1063
|
| Access (v1, v2) ->
|
|
1064
|
Access (rename_value n v1, rename_value n v2)
|
|
1065
|
| Power (v1, v2) ->
|
|
1066
|
Power (rename_value n v1, rename_value n v2)
|
|
1067
|
| v ->
|
|
1068
|
v);
|
|
1069
|
}
|
|
1070
|
|
|
1071
|
let rename_expression :
|
|
1072
|
type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t =
|
|
1073
|
fun n -> function
|
|
1074
|
| Val v ->
|
|
1075
|
Val (rename_value n v)
|
|
1076
|
| Var v ->
|
|
1077
|
Var (rename_var_decl n v)
|
|
1078
|
| e ->
|
|
1079
|
e
|
|
1080
|
|
|
1081
|
let rename_predicate n = function
|
|
1082
|
| Transition (s, f, inst, i, es, r, mf, mif) ->
|
|
1083
|
Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif)
|
|
1084
|
| p ->
|
|
1085
|
p
|
|
1086
|
|
|
1087
|
let rec rename_formula n = function
|
|
1088
|
| Equal (e1, e2) ->
|
|
1089
|
Equal (rename_expression n e1, rename_expression n e2)
|
|
1090
|
| And fs ->
|
|
1091
|
And (List.map (rename_formula n) fs)
|
|
1092
|
| Or fs ->
|
|
1093
|
Or (List.map (rename_formula n) fs)
|
|
1094
|
| Imply (f1, f2) ->
|
|
1095
|
Imply (rename_formula n f1, rename_formula n f2)
|
|
1096
|
| Exists (xs, f) ->
|
|
1097
|
Exists (List.map (rename_var_decl n) xs, rename_formula n f)
|
|
1098
|
| Forall (xs, f) ->
|
|
1099
|
Forall (List.map (rename_var_decl n) xs, rename_formula n f)
|
|
1100
|
| Ternary (e, t, f) ->
|
|
1101
|
Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
|
|
1102
|
| Predicate p ->
|
|
1103
|
Predicate (rename_predicate n p)
|
|
1104
|
| ExistsMem (x, f1, f2) ->
|
|
1105
|
ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
|
|
1106
|
| Value v ->
|
|
1107
|
Value (rename_value n v)
|
|
1108
|
| f ->
|
|
1109
|
f
|
|
1110
|
|
|
1111
|
let rename_contract n c =
|
|
1112
|
{
|
|
1113
|
c with
|
|
1114
|
mc_pre = rename_formula n c.mc_pre;
|
|
1115
|
mc_post = rename_formula n c.mc_post;
|
|
1116
|
}
|
|
1117
|
|
|
1118
|
let but_last l = List.(rev (tl (rev l)))
|
|
1119
|
|
|
1120
|
let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt
|
|
1121
|
(n, mem_in, mem_out) =
|
|
1122
|
let name = m.mname.node_id in
|
|
1123
|
let inputs = m.mstep.step_inputs in
|
|
1124
|
let outputs = m.mstep.step_outputs in
|
|
1125
|
fprintf
|
|
1126
|
fmt
|
|
1127
|
"%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
|
|
1128
|
name
|
|
1129
|
case
|
|
1130
|
n
|
|
1131
|
pp_mem_in
|
|
1132
|
mem_in
|
|
1133
|
pp_vars
|
|
1134
|
(inputs @ outputs)
|
|
1135
|
pp_mem_out
|
|
1136
|
mem_out
|
|
1137
|
|
|
1138
|
let pp_k_induction_base_case m = pp_k_induction_case "base" m
|
|
1139
|
|
|
1140
|
let pp_k_induction_inductive_case m = pp_k_induction_case "inductive" m
|
|
1141
|
|
|
1142
|
let pp_base_cases m fmt (c, m_c, k) =
|
|
1143
|
let name = m.mname.node_id in
|
|
1144
|
let name_c = m_c.mname.node_id in
|
|
1145
|
let mem = mk_mem m in
|
|
1146
|
let mem_c = mk_mem_c m in
|
|
1147
|
let inputs = m.mstep.step_inputs in
|
|
1148
|
let outputs = m.mstep.step_outputs in
|
|
1149
|
let stateless = fst (get_stateless_status m) in
|
|
1150
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1151
|
let l = List.init (k - 1) (fun n -> n + 1) in
|
|
1152
|
pp_print_list
|
|
1153
|
~pp_open_box:pp_open_vbox0
|
|
1154
|
~pp_sep:pp_print_cutcut
|
|
1155
|
(fun fmt n ->
|
|
1156
|
let l = List.init (n + 1) (fun n -> n) in
|
|
1157
|
let pp fmt =
|
|
1158
|
let pp =
|
|
1159
|
pp_implies
|
|
1160
|
(pp_and_l (fun fmt -> function
|
|
1161
|
| 0 ->
|
|
1162
|
let pp = pp_init pp_print_string in
|
|
1163
|
(if stateless_c then fun fmt (x, _) -> pp fmt x
|
|
1164
|
else pp_and pp pp)
|
|
1165
|
fmt
|
|
1166
|
((name, rename 0 mem), (name_c, rename 0 mem_c))
|
|
1167
|
| n' ->
|
|
1168
|
let pp_var_c fmt (out, vd) =
|
|
1169
|
if out && n' < n then pp_true_c_bool fmt ()
|
|
1170
|
else pp_var_decl fmt vd
|
|
1171
|
in
|
|
1172
|
let c_inputs =
|
|
1173
|
List.map
|
|
1174
|
(fun v -> false, rename_var_decl n' v)
|
|
1175
|
m_c.mstep.step_inputs
|
|
1176
|
in
|
|
1177
|
let c_outputs =
|
|
1178
|
List.map
|
|
1179
|
(fun v -> true, rename_var_decl n' v)
|
|
1180
|
m_c.mstep.step_outputs
|
|
1181
|
in
|
|
1182
|
let pp stateless pp_var =
|
|
1183
|
pp_transition_aux
|
|
1184
|
stateless
|
|
1185
|
pp_print_string
|
|
1186
|
pp_print_string
|
|
1187
|
pp_var
|
|
1188
|
in
|
|
1189
|
pp_and
|
|
1190
|
(pp stateless pp_var_decl)
|
|
1191
|
(pp stateless_c pp_var_c)
|
|
1192
|
fmt
|
|
1193
|
( ( name,
|
|
1194
|
List.map (rename_var_decl n') (inputs @ outputs),
|
|
1195
|
rename (n' - 1) mem,
|
|
1196
|
rename n' mem ),
|
|
1197
|
( name_c,
|
|
1198
|
c_inputs @ c_outputs,
|
|
1199
|
rename (n' - 1) mem_c,
|
|
1200
|
rename n' mem_c ) )))
|
|
1201
|
(pp_contract m)
|
|
1202
|
in
|
|
1203
|
if stateless_c then pp fmt
|
|
1204
|
else fun x ->
|
|
1205
|
pp_forall
|
|
1206
|
(pp_machine_decl
|
|
1207
|
~ghost:true
|
|
1208
|
(pp_comma_list (fun fmt n ->
|
|
1209
|
pp_print_string fmt (rename n mem_c))))
|
|
1210
|
pp
|
|
1211
|
fmt
|
|
1212
|
((name_c, l), x)
|
|
1213
|
in
|
|
1214
|
pp_predicate
|
|
1215
|
(pp_k_induction_base_case
|
|
1216
|
m
|
|
1217
|
(pp_machine_decl' ~ghost:true)
|
|
1218
|
(pp_machine_decl' ~ghost:true)
|
|
1219
|
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
|
|
1220
|
(pp_forall
|
|
1221
|
(pp_locals m)
|
|
1222
|
(if n > 1 then
|
|
1223
|
pp_forall
|
|
1224
|
(fun fmt l ->
|
|
1225
|
fprintf
|
|
1226
|
fmt
|
|
1227
|
"%a@,%a"
|
|
1228
|
(pp_machine_decl
|
|
1229
|
~ghost:true
|
|
1230
|
(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
|
|
1231
|
pp_print_string fmt (rename n mem))))
|
|
1232
|
(name, but_last l)
|
|
1233
|
(pp_locals m)
|
|
1234
|
(List.flatten
|
|
1235
|
(List.map
|
|
1236
|
(fun n ->
|
|
1237
|
List.map (rename_var_decl n) (inputs @ outputs))
|
|
1238
|
(List.tl l))))
|
|
1239
|
pp
|
|
1240
|
else fun fmt (_, x) -> pp fmt x))
|
|
1241
|
fmt
|
|
1242
|
( (n, (name, rename (n - 1) mem), (name, rename n mem)),
|
|
1243
|
( List.map (rename_var_decl n) m_c.mstep.step_outputs,
|
|
1244
|
(but_last l, (l, rename_contract n c)) ) ))
|
|
1245
|
fmt
|
|
1246
|
l
|
|
1247
|
|
|
1248
|
let pp_inductive_case m fmt (c, m_c, k) =
|
|
1249
|
let name = m.mname.node_id in
|
|
1250
|
let mem = mk_mem m in
|
|
1251
|
let mem_c = mk_mem_c m_c in
|
|
1252
|
let inputs = m.mstep.step_inputs in
|
|
1253
|
let outputs = m.mstep.step_outputs in
|
|
1254
|
let stateless = fst (get_stateless_status m) in
|
|
1255
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1256
|
let l = List.init k (fun n -> n + 1) in
|
|
1257
|
let l' = 0 :: l in
|
|
1258
|
let pp fmt =
|
|
1259
|
let pp =
|
|
1260
|
pp_implies
|
|
1261
|
(pp_and_l (fun fmt n ->
|
|
1262
|
let pp_var_c fmt (out, vd) =
|
|
1263
|
if out && n < k then pp_true_c_bool fmt ()
|
|
1264
|
else pp_var_decl fmt vd
|
|
1265
|
in
|
|
1266
|
let c_inputs =
|
|
1267
|
List.map
|
|
1268
|
(fun v -> false, rename_var_decl n v)
|
|
1269
|
m_c.mstep.step_inputs
|
|
1270
|
in
|
|
1271
|
let c_outputs =
|
|
1272
|
List.map
|
|
1273
|
(fun v -> true, rename_var_decl n v)
|
|
1274
|
m_c.mstep.step_outputs
|
|
1275
|
in
|
|
1276
|
pp_and
|
|
1277
|
(pp_transition_aux
|
|
1278
|
stateless
|
|
1279
|
pp_print_string
|
|
1280
|
pp_print_string
|
|
1281
|
pp_var_decl)
|
|
1282
|
(pp_transition_aux
|
|
1283
|
stateless_c
|
|
1284
|
pp_print_string
|
|
1285
|
pp_print_string
|
|
1286
|
pp_var_c)
|
|
1287
|
fmt
|
|
1288
|
( ( name,
|
|
1289
|
List.map (rename_var_decl n) (inputs @ outputs),
|
|
1290
|
rename (n - 1) mem,
|
|
1291
|
rename n mem ),
|
|
1292
|
( m_c.mname.node_id,
|
|
1293
|
c_inputs @ c_outputs,
|
|
1294
|
rename (n - 1) mem_c,
|
|
1295
|
rename n mem_c ) )))
|
|
1296
|
(pp_contract m)
|
|
1297
|
in
|
|
1298
|
if stateless_c then pp fmt
|
|
1299
|
else fun x ->
|
|
1300
|
pp_forall
|
|
1301
|
(pp_machine_decl
|
|
1302
|
~ghost:true
|
|
1303
|
(pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
|
|
1304
|
pp
|
|
1305
|
fmt
|
|
1306
|
((m_c.mname.node_id, l'), x)
|
|
1307
|
in
|
|
1308
|
pp_predicate
|
|
1309
|
(pp_k_induction_inductive_case
|
|
1310
|
m
|
|
1311
|
(pp_machine_decl' ~ghost:true)
|
|
1312
|
(pp_machine_decl' ~ghost:true)
|
|
1313
|
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
|
|
1314
|
(pp_forall
|
|
1315
|
(pp_locals m)
|
|
1316
|
(if k > 1 then
|
|
1317
|
pp_forall
|
|
1318
|
(fun fmt l ->
|
|
1319
|
fprintf
|
|
1320
|
fmt
|
|
1321
|
"%a@,%a"
|
|
1322
|
(pp_machine_decl
|
|
1323
|
~ghost:true
|
|
1324
|
(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
|
|
1325
|
pp_print_string fmt (rename (n - 1) mem))))
|
|
1326
|
(name, but_last l)
|
|
1327
|
(pp_locals m)
|
|
1328
|
(List.flatten
|
|
1329
|
(List.map
|
|
1330
|
(fun n ->
|
|
1331
|
List.map (rename_var_decl (n - 1)) (inputs @ outputs))
|
|
1332
|
(List.tl l))))
|
|
1333
|
pp
|
|
1334
|
else fun fmt (_, x) -> pp fmt x))
|
|
1335
|
fmt
|
|
1336
|
( (k, (name, rename (k - 1) mem), (name, rename k mem)),
|
|
1337
|
( List.map (rename_var_decl k) m_c.mstep.step_outputs,
|
|
1338
|
(l, (l, rename_contract k c)) ) )
|
|
1339
|
|
|
1340
|
let pp_k_induction_lemmas m fmt k =
|
|
1341
|
let name = m.mname.node_id in
|
|
1342
|
let mem_in = mk_mem_in m in
|
|
1343
|
let mem_out = mk_mem_out m in
|
|
1344
|
let inputs = m.mstep.step_inputs in
|
|
1345
|
let outputs = m.mstep.step_outputs in
|
|
1346
|
let l = List.init k (fun n -> n + 1) in
|
|
1347
|
pp_print_list
|
|
1348
|
~pp_open_box:pp_open_vbox0
|
|
1349
|
~pp_sep:pp_print_cutcut
|
|
1350
|
(fun fmt n ->
|
|
1351
|
pp_lemma
|
|
1352
|
(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
|
|
1353
|
(pp_forall
|
|
1354
|
(fun fmt () ->
|
|
1355
|
fprintf
|
|
1356
|
fmt
|
|
1357
|
"%a,@;%a"
|
|
1358
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
|
1359
|
(name, [ mem_in; mem_out ])
|
|
1360
|
(pp_locals m)
|
|
1361
|
(inputs @ outputs))
|
|
1362
|
((if n = k then pp_k_induction_inductive_case
|
|
1363
|
else pp_k_induction_base_case)
|
|
1364
|
m
|
|
1365
|
pp_print_string
|
|
1366
|
pp_print_string
|
|
1367
|
(pp_comma_list pp_var_decl)))
|
|
1368
|
fmt
|
|
1369
|
(n, ((), (n, mem_in, mem_out))))
|
|
1370
|
fmt
|
|
1371
|
l
|
|
1372
|
|
|
1373
|
let pp_k_induction_axiom m fmt (c, m_c, k) =
|
|
1374
|
let name = m.mname.node_id in
|
|
1375
|
let mem_in = mk_mem_in m in
|
|
1376
|
let mem_out = mk_mem_out m in
|
|
1377
|
let mem_in_c = mk_mem_in_c m_c in
|
|
1378
|
let mem_out_c = mk_mem_out_c m_c in
|
|
1379
|
let inputs = m.mstep.step_inputs in
|
|
1380
|
let outputs = m.mstep.step_outputs in
|
|
1381
|
let stateless = fst (get_stateless_status m) in
|
|
1382
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1383
|
let l = List.init k (fun n -> n + 1) in
|
|
1384
|
let pp =
|
|
1385
|
pp_implies
|
|
1386
|
(pp_and_l (fun fmt n ->
|
|
1387
|
(if n = k then pp_k_induction_inductive_case
|
|
1388
|
else pp_k_induction_base_case)
|
|
1389
|
m
|
|
1390
|
pp_print_string
|
|
1391
|
pp_print_string
|
|
1392
|
(pp_comma_list pp_var_decl)
|
|
1393
|
fmt
|
|
1394
|
(n, mem_in, mem_out)))
|
|
1395
|
(pp_forall
|
|
1396
|
(pp_locals m)
|
|
1397
|
(pp_implies
|
|
1398
|
(pp_and
|
|
1399
|
(pp_transition_aux
|
|
1400
|
stateless
|
|
1401
|
pp_print_string
|
|
1402
|
pp_print_string
|
|
1403
|
pp_var_decl)
|
|
1404
|
(pp_transition_aux
|
|
1405
|
stateless_c
|
|
1406
|
pp_print_string
|
|
1407
|
pp_print_string
|
|
1408
|
pp_var_decl))
|
|
1409
|
(pp_contract m)))
|
|
1410
|
in
|
|
1411
|
pp_axiomatic
|
|
1412
|
(fun fmt () -> fprintf fmt "%s_k_Induction" name)
|
|
1413
|
(pp_axiom
|
|
1414
|
(fun fmt () -> fprintf fmt "%s_k_induction" name)
|
|
1415
|
(pp_forall
|
|
1416
|
(fun fmt () ->
|
|
1417
|
fprintf
|
|
1418
|
fmt
|
|
1419
|
"%a,@;%a"
|
|
1420
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
|
1421
|
(name, [ mem_in; mem_out ])
|
|
1422
|
(pp_locals m)
|
|
1423
|
(inputs @ outputs))
|
|
1424
|
(if stateless_c then pp
|
|
1425
|
else fun fmt x ->
|
|
1426
|
pp_forall
|
|
1427
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
|
1428
|
pp
|
|
1429
|
fmt
|
|
1430
|
((m_c.mname.node_id, [ mem_in_c; mem_out_c ]), x))))
|
|
1431
|
fmt
|
|
1432
|
( (),
|
|
1433
|
( (),
|
|
1434
|
( (),
|
|
1435
|
( l,
|
|
1436
|
( m_c.mstep.step_outputs,
|
|
1437
|
( ( (name, inputs @ outputs, mem_in, mem_out),
|
|
1438
|
( m_c.mname.node_id,
|
|
1439
|
m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
|
|
1440
|
mem_in_c,
|
|
1441
|
mem_out_c ) ),
|
|
1442
|
c ) ) ) ) ) )
|
|
1443
|
|
|
1444
|
let pp_k_induction m fmt ((_, m_c, k) as c_m_k) =
|
|
1445
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1446
|
pp_acsl_cut
|
|
1447
|
(fun fmt () ->
|
|
1448
|
fprintf
|
|
1449
|
fmt
|
|
1450
|
"%a@,@,%a@,@,%a@,@,%a@,@,%a@,@,%a"
|
|
1451
|
pp_init_def
|
|
1452
|
m
|
|
1453
|
(if stateless_c then pp_print_nothing else pp_init_def)
|
|
1454
|
m_c
|
|
1455
|
(pp_base_cases m)
|
|
1456
|
c_m_k
|
|
1457
|
(pp_inductive_case m)
|
|
1458
|
c_m_k
|
|
1459
|
(pp_k_induction_lemmas m)
|
|
1460
|
k
|
|
1461
|
(pp_k_induction_axiom m)
|
|
1462
|
c_m_k)
|
|
1463
|
fmt
|
|
1464
|
()
|
|
1465
|
|
|
1466
|
let pp_proof_annotation m m_c fmt c =
|
|
1467
|
let pp m_c fmt = function
|
|
1468
|
| Kinduction k ->
|
|
1469
|
pp_k_induction m fmt (c, m_c, k)
|
|
1470
|
in
|
|
1471
|
match m_c with
|
|
1472
|
| Some m_c ->
|
|
1473
|
pp_print_option (pp m_c) fmt c.mc_proof
|
|
1474
|
| None ->
|
|
1475
|
()
|
|
1476
|
|
|
1477
|
let pp_step_spec fmt machines self mem m =
|
|
1478
|
let name = m.mname.node_id in
|
|
1479
|
let insts = instances machines m in
|
|
1480
|
let insts' = powerset_instances insts in
|
|
1481
|
let insts'' =
|
|
1482
|
List.(
|
|
1483
|
filter
|
|
1484
|
(fun l -> l <> [])
|
|
1485
|
(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
|
|
1486
|
in
|
|
1487
|
let inputs = m.mstep.step_inputs in
|
|
1488
|
let outputs = m.mstep.step_outputs in
|
|
1489
|
let stateless = fst (get_stateless_status m) in
|
|
1490
|
let pp_if_outputs pp = if outputs = [] then pp_print_nothing else pp in
|
|
1491
|
let c, m_c = contract_of machines m in
|
|
1492
|
let pp_spec =
|
|
1493
|
pp_print_option
|
|
1494
|
(if m.mis_contract then pp_print_nothing
|
|
1495
|
else fun fmt c ->
|
|
1496
|
pp_print_option
|
|
1497
|
(fun fmt m_c ->
|
|
1498
|
let mem_in = mk_mem_in_c m_c in
|
|
1499
|
let mem_out = mk_mem_out_c m_c in
|
|
1500
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1501
|
pp_ensures
|
|
1502
|
(pp_implies
|
|
1503
|
(pp_transition_aux
|
|
1504
|
stateless_c
|
|
1505
|
pp_print_string
|
|
1506
|
pp_print_string
|
|
1507
|
(fun fmt v ->
|
|
1508
|
(if is_output m v then pp_ptr_decl else pp_var_decl)
|
|
1509
|
fmt
|
|
1510
|
v))
|
|
1511
|
(pp_contract m))
|
|
1512
|
fmt
|
|
1513
|
( ( m_c.mname.node_id,
|
|
1514
|
m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
|
|
1515
|
mem_in,
|
|
1516
|
mem_out ),
|
|
1517
|
c ))
|
|
1518
|
fmt
|
|
1519
|
m_c)
|
|
1520
|
in
|
|
1521
|
let pp_spec_vars =
|
|
1522
|
match m_c with
|
|
1523
|
| Some m_c ->
|
|
1524
|
let mem_in = mk_mem_in_c m_c in
|
|
1525
|
let mem_out = mk_mem_out_c m_c in
|
|
1526
|
let stateless_c = fst (get_stateless_status m_c) in
|
|
1527
|
pp_acsl_cut
|
|
1528
|
(pp_ghost (fun fmt () ->
|
|
1529
|
fprintf
|
|
1530
|
fmt
|
|
1531
|
"@;<0 2>@[<v>%a%a@]"
|
|
1532
|
(pp_print_list
|
|
1533
|
~pp_open_box:pp_open_vbox0
|
|
1534
|
~pp_sep:pp_print_semicolon
|
|
1535
|
~pp_eol:pp_print_semicolon
|
|
1536
|
(pp_c_decl_local_var m))
|
|
1537
|
m_c.mstep.step_outputs
|
|
1538
|
(if stateless_c then pp_print_nothing
|
|
1539
|
else
|
|
1540
|
pp_machine_decl
|
|
1541
|
~ghost:true
|
|
1542
|
(pp_comma_list ~pp_eol:pp_print_semicolon pp_print_string))
|
|
1543
|
(m_c.mname.node_id, [ mem_in; mem_out ])))
|
|
1544
|
| _ ->
|
|
1545
|
pp_print_nothing
|
|
1546
|
in
|
|
1547
|
pp_print_option (pp_proof_annotation m m_c) fmt c;
|
|
1548
|
pp_spec_vars fmt ();
|
|
1549
|
pp_acsl_cut
|
|
1550
|
(fun fmt () ->
|
|
1551
|
if stateless then
|
|
1552
|
fprintf
|
|
1553
|
fmt
|
|
1554
|
"%a@,%a@,%a@,%a@,%a"
|
|
1555
|
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
|
|
1556
|
outputs
|
|
1557
|
(pp_if_outputs (pp_requires pp_separated''))
|
|
1558
|
outputs
|
|
1559
|
(pp_assigns pp_ptr_decl)
|
|
1560
|
outputs
|
|
1561
|
(pp_ensures (pp_transition_aux' m))
|
|
1562
|
(name, inputs @ outputs, "", "")
|
|
1563
|
pp_spec
|
|
1564
|
c
|
|
1565
|
else
|
|
1566
|
fprintf
|
|
1567
|
fmt
|
|
1568
|
"%a@,\
|
|
1569
|
%a@,\
|
|
1570
|
%a@,\
|
|
1571
|
%a@,\
|
|
1572
|
%a@,\
|
|
1573
|
%a@,\
|
|
1574
|
%a@,\
|
|
1575
|
%a@,\
|
|
1576
|
%a@,\
|
|
1577
|
%a@,\
|
|
1578
|
%a@,\
|
|
1579
|
%a@,\
|
|
1580
|
%a@,\
|
|
1581
|
%a@,\
|
|
1582
|
%a@,\
|
|
1583
|
%a@,\
|
|
1584
|
%a@,\
|
|
1585
|
%a"
|
|
1586
|
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
|
|
1587
|
outputs
|
|
1588
|
(pp_requires pp_mem_valid')
|
|
1589
|
(name, self)
|
|
1590
|
(pp_requires (pp_separated' self mem))
|
|
1591
|
(insts', outputs)
|
|
1592
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
|
1593
|
(name, mem, self)
|
|
1594
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
|
1595
|
(name, mem, self)
|
|
1596
|
(pp_ensures
|
|
1597
|
(pp_transition_aux stateless (pp_old pp_ptr) pp_ptr (fun fmt v ->
|
|
1598
|
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
|
|
1599
|
(name, inputs @ outputs, mem, mem)
|
|
1600
|
pp_spec
|
|
1601
|
c
|
|
1602
|
(pp_assigns pp_ptr_decl)
|
|
1603
|
outputs
|
|
1604
|
(pp_assigns (pp_reg self))
|
|
1605
|
m.mmemory
|
|
1606
|
(pp_assigns pp_reset_flag')
|
|
1607
|
[ self ]
|
|
1608
|
(pp_assigns (pp_memory self))
|
|
1609
|
(memories insts')
|
|
1610
|
(pp_assigns (pp_register_chain self))
|
|
1611
|
insts
|
|
1612
|
(pp_assigns (pp_reset_flag_chain self))
|
|
1613
|
insts''
|
|
1614
|
(pp_assigns (pp_reg mem))
|
|
1615
|
m.mmemory
|
|
1616
|
(pp_assigns pp_reset_flag')
|
|
1617
|
[ mem ]
|
|
1618
|
(pp_assigns (pp_memory ~indirect:false mem))
|
|
1619
|
(memories insts')
|
|
1620
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
|
1621
|
insts
|
|
1622
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
|
1623
|
insts'')
|
|
1624
|
fmt
|
|
1625
|
()
|
|
1626
|
|
|
1627
|
let pp_ghost_instr_code m self fmt instr =
|
|
1628
|
match instr.instr_desc with
|
|
1629
|
| MStateAssign (x, v) ->
|
|
1630
|
fprintf
|
|
1631
|
fmt
|
|
1632
|
"@,%a"
|
|
1633
|
(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
|
|
1634
|
(x, v)
|
|
1635
|
| MResetAssign b ->
|
|
1636
|
fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
|
|
1637
|
| MSetReset inst ->
|
|
1638
|
let td, _ = List.assoc inst m.minstances in
|
|
1639
|
if Arrow.td_is_arrow td then
|
|
1640
|
fprintf
|
|
1641
|
fmt
|
|
1642
|
"@,%a;"
|
|
1643
|
(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
|
|
1644
|
inst
|
|
1645
|
| _ ->
|
|
1646
|
()
|
|
1647
|
|
|
1648
|
let pp_step_instr_spec m self mem fmt instr =
|
|
1649
|
let ghost = m.mis_contract in
|
|
1650
|
fprintf
|
|
1651
|
fmt
|
|
1652
|
"%a%a"
|
|
1653
|
(pp_ghost_instr_code m mem)
|
|
1654
|
instr
|
|
1655
|
(pp_print_list
|
|
1656
|
~pp_open_box:pp_open_vbox0
|
|
1657
|
~pp_prologue:pp_print_cut
|
|
1658
|
(pp_acsl_line'
|
|
1659
|
~ghost
|
|
1660
|
(pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
|
|
1661
|
instr.instr_spec
|
|
1662
|
|
|
1663
|
let pp_ghost_parameter mem fmt inst =
|
|
1664
|
GhostProto.pp_ghost_parameters
|
|
1665
|
~cut:false
|
|
1666
|
fmt
|
|
1667
|
(match inst with
|
|
1668
|
| Some inst ->
|
|
1669
|
[ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
|
|
1670
|
| None ->
|
|
1671
|
[ mem, pp_print_string ])
|
|
1672
|
|
|
1673
|
let pp_contract fmt machines _self mem m =
|
|
1674
|
let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
|
|
1675
|
match contract_of machines m with
|
|
1676
|
| Some c, Some _ ->
|
|
1677
|
pp_print_option
|
|
1678
|
(pp_acsl_cut (fun fmt -> function
|
|
1679
|
| Kinduction k ->
|
|
1680
|
let l = List.init k (fun n -> n + 1) in
|
|
1681
|
let pp_mem_in = pp_at_pre pp_ptr in
|
|
1682
|
let pp_mem_out = pp_ptr in
|
|
1683
|
pp_assert
|
|
1684
|
(pp_and_l (fun fmt n ->
|
|
1685
|
(if n = k then pp_k_induction_inductive_case
|
|
1686
|
else pp_k_induction_base_case)
|
|
1687
|
m
|
|
1688
|
pp_mem_in
|
|
1689
|
pp_mem_out
|
|
1690
|
pp_vars
|
|
1691
|
fmt
|
|
1692
|
(n, mem, mem)))
|
|
1693
|
fmt
|
|
1694
|
l))
|
|
1695
|
fmt
|
|
1696
|
c.mc_proof
|
|
1697
|
| _, _ ->
|
|
1698
|
()
|
|
1699
|
end
|
|
1700
|
|
|
1701
|
module MainMod = struct
|
|
1702
|
let main_mem_ghost = "main_mem_ghost"
|
|
1703
|
|
|
1704
|
let pp_declare_ghost_state fmt name =
|
|
1705
|
pp_acsl_line'_cut
|
|
1706
|
(pp_ghost (fun fmt () ->
|
|
1707
|
fprintf
|
|
1708
|
fmt
|
|
1709
|
"%a(,%s);"
|
|
1710
|
(pp_machine_static_alloc_name ~ghost:true)
|
|
1711
|
name
|
|
1712
|
main_mem_ghost))
|
|
1713
|
fmt
|
|
1714
|
()
|
|
1715
|
|
|
1716
|
let pp_ghost_state_parameter fmt () =
|
|
1717
|
GhostProto.pp_ghost_parameters
|
|
1718
|
~cut:false
|
|
1719
|
fmt
|
|
1720
|
[ main_mem_ghost, pp_ref pp_print_string ]
|
|
1721
|
|
|
1722
|
let pp_main_loop_invariants main_mem machines fmt m =
|
|
1723
|
let name = m.mname.node_id in
|
|
1724
|
let insts = powerset_instances (instances machines m) in
|
|
1725
|
pp_acsl_cut
|
|
1726
|
(fun fmt () ->
|
|
1727
|
fprintf
|
|
1728
|
fmt
|
|
1729
|
"%a@,%a@,%a@,%a"
|
|
1730
|
(pp_loop_invariant pp_mem_valid')
|
|
1731
|
(name, main_mem)
|
|
1732
|
(pp_loop_invariant
|
|
1733
|
(pp_memory_pack_aux pp_print_string pp_print_string))
|
|
1734
|
(name, main_mem_ghost, main_mem)
|
|
1735
|
(pp_loop_invariant
|
|
1736
|
(pp_separated
|
|
1737
|
(pp_paren pp_print_string)
|
|
1738
|
pp_ref'
|
|
1739
|
(pp_ref pp_var_decl)))
|
|
1740
|
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
|
|
1741
|
(pp_loop_invariant
|
|
1742
|
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
|
|
1743
|
((), ((), ())))
|
|
1744
|
fmt
|
|
1745
|
()
|
|
1746
|
|
|
1747
|
let pp_main_spec fmt =
|
|
1748
|
pp_acsl_cut
|
|
1749
|
(fun fmt () ->
|
|
1750
|
fprintf
|
|
1751
|
fmt
|
|
1752
|
"%a@,%a@,%a@,%a"
|
|
1753
|
(pp_requires
|
|
1754
|
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
|
|
1755
|
((), ((), ()))
|
|
1756
|
(pp_terminates pp_false)
|
|
1757
|
()
|
|
1758
|
(pp_ensures pp_false)
|
|
1759
|
()
|
|
1760
|
(pp_assigns pp_nothing)
|
|
1761
|
[ () ])
|
|
1762
|
fmt
|
|
1763
|
()
|
|
1764
|
end
|
|
1765
|
|
|
1766
|
(**************************************************************************)
|
|
1767
|
(* MAKEFILE *)
|
|
1768
|
(**************************************************************************)
|
|
1769
|
|
|
1770
|
module MakefileMod = struct
|
|
1771
|
let pp_print_dependencies = C_backend_makefile.fprintf_dependencies "_spec"
|
|
1772
|
|
|
1773
|
let pp_arrow_o fmt () = pp_print_string fmt "arrow_spec.o"
|
|
1774
|
|
|
1775
|
let other_targets fmt basename _nodename dependencies =
|
|
1776
|
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
|
|
1777
|
(* EACSL version of library file . c *)
|
|
1778
|
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
|
|
1779
|
fprintf
|
|
1780
|
fmt
|
|
1781
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
|
|
1782
|
e-acsl -print -ocode %s_eacsl.c@."
|
|
1783
|
basename
|
|
1784
|
basename;
|
|
1785
|
fprintf fmt "@.";
|
|
1786
|
fprintf fmt "@.";
|
|
1787
|
|
|
1788
|
(* EACSL version of library file . c + main .c *)
|
|
1789
|
fprintf
|
|
1790
|
fmt
|
|
1791
|
"%s_main_eacsl.c: %s.c %s.h %s_main.c@."
|
|
1792
|
basename
|
|
1793
|
basename
|
|
1794
|
basename
|
|
1795
|
basename;
|
|
1796
|
fprintf
|
|
1797
|
fmt
|
|
1798
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
|
|
1799
|
-then-on e-acsl -print -ocode %s_main_eacsl.i@."
|
|
1800
|
basename
|
|
1801
|
basename
|
|
1802
|
basename;
|
|
1803
|
(* Ugly hack to deal with eacsl bugs *)
|
|
1804
|
fprintf
|
|
1805
|
fmt
|
|
1806
|
"\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
|
|
1807
|
basename
|
|
1808
|
basename;
|
|
1809
|
fprintf fmt "@.";
|
|
1810
|
fprintf fmt "@.";
|
|
1811
|
|
|
1812
|
(* EACSL version of binary *)
|
|
1813
|
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
|
|
1814
|
fprintf
|
|
1815
|
fmt
|
|
1816
|
"\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
|
|
1817
|
basename;
|
|
1818
|
(* compiling instrumented lib + main *)
|
|
1819
|
pp_print_dependencies fmt dependencies;
|
|
1820
|
fprintf
|
|
1821
|
fmt
|
|
1822
|
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
|
|
1823
|
%s_main_eacsl.o %a@."
|
|
1824
|
basename
|
|
1825
|
(pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
|
|
1826
|
(C_backend_makefile.compiled_dependencies dependencies)
|
|
1827
|
("${FRAMACEACSL}/e_acsl.c "
|
|
1828
|
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
|
1829
|
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
|
1830
|
basename
|
|
1831
|
(pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
|
|
1832
|
(C_backend_makefile.lib_dependencies dependencies);
|
|
1833
|
fprintf fmt "@."
|
|
1834
|
end
|
|
1835
|
|
|
1836
|
(* Local Variables: *)
|
|
1837
|
(* compile-command:"make -C ../../.." *)
|
|
1838
|
(* End: *)
|