Project

General

Profile

Download (54.8 KB) Statistics
| Branch: | Tag: | Revision:
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 other_targets fmt basename _nodename dependencies =
1772
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1773
    (* EACSL version of library file . c *)
1774
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1775
    fprintf
1776
      fmt
1777
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1778
       e-acsl -print -ocode %s_eacsl.c@."
1779
      basename
1780
      basename;
1781
    fprintf fmt "@.";
1782
    fprintf fmt "@.";
1783

    
1784
    (* EACSL version of library file . c + main .c *)
1785
    fprintf
1786
      fmt
1787
      "%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1788
      basename
1789
      basename
1790
      basename
1791
      basename;
1792
    fprintf
1793
      fmt
1794
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1795
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
1796
      basename
1797
      basename
1798
      basename;
1799
    (* Ugly hack to deal with eacsl bugs *)
1800
    fprintf
1801
      fmt
1802
      "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1803
      basename
1804
      basename;
1805
    fprintf fmt "@.";
1806
    fprintf fmt "@.";
1807

    
1808
    (* EACSL version of binary *)
1809
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1810
    fprintf
1811
      fmt
1812
      "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1813
      basename;
1814
    (* compiling instrumented lib + main *)
1815
    C_backend_makefile.fprintf_dependencies fmt dependencies;
1816
    fprintf
1817
      fmt
1818
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1819
       %s_main_eacsl.o %a@."
1820
      basename
1821
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1822
      (C_backend_makefile.compiled_dependencies dependencies)
1823
      ("${FRAMACEACSL}/e_acsl.c "
1824
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1825
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1826
      basename
1827
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1828
      (C_backend_makefile.lib_dependencies dependencies);
1829
    fprintf fmt "@."
1830
end
1831

    
1832
(* Local Variables: *)
1833
(* compile-command:"make -C ../../.." *)
1834
(* End: *)
(15-15/18)