Project

General

Profile

Download (50.4 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 ?(ghost=false) pp fmt x =
39
  let op = if ghost then "" else "*" in
40
  let cl = if ghost then "@" else "*" in
41
  fprintf fmt "@[<v>/%s%@ @[<v>%a@]@,%s/@]" op pp x cl
42

    
43
let pp_acsl_cut ?ghost pp fmt = fprintf fmt "%a@," (pp_acsl ?ghost pp)
44

    
45
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
46

    
47
let pp_acsl_line' ?(ghost=false) pp fmt x =
48
  let op = if ghost then "" else "*" in
49
  let cl = if ghost then "@" else "*" in
50
  fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
51

    
52
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
53

    
54
let pp_requires pp fmt = fprintf fmt "requires %a;" pp
55

    
56
let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
57

    
58
let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
59

    
60
let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
61

    
62
let pp_assigns pp =
63
  pp_comma_list
64
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
65
    ~pp_epilogue:pp_print_semicolon'
66
    pp
67

    
68
let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
69

    
70
let pp_assert pp fmt = fprintf fmt "assert %a;" pp
71

    
72
let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
73

    
74
let pp_mem_valid pp_var fmt (name, var) =
75
  fprintf fmt "%s_valid(%a)" name pp_var var
76

    
77
let pp_mem_valid' = pp_mem_valid pp_print_string
78

    
79
let pp_ref pp fmt = fprintf fmt "&%a" pp
80

    
81
let pp_ref' = pp_ref pp_print_string
82

    
83
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
84
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
85

    
86
let pp_indirect' = pp_indirect pp_print_string pp_print_string
87

    
88
let pp_access pp_stru pp_field fmt (stru, field) =
89
  fprintf fmt "%a.%a" pp_stru stru pp_field field
90

    
91
let pp_access' = pp_access pp_print_string pp_print_string
92

    
93
let pp_var_decl fmt v = pp_print_string fmt v.var_id
94

    
95
let pp_reg self fmt field =
96
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
97

    
98
let pp_true fmt () = pp_print_string fmt "\\true"
99

    
100
let pp_false fmt () = pp_print_string fmt "\\false"
101

    
102
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
103

    
104
let pp_null fmt () = pp_print_string fmt "\\null"
105

    
106
let pp_stdout fmt () = pp_print_string fmt "stdout"
107

    
108
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
109

    
110
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
111

    
112
let find_machine f =
113
  List.find (fun m -> m.mname.node_id = f)
114

    
115
let instances machines m =
116
  let open List in
117
  let grow paths i td mems =
118
    match paths with
119
    | [] ->
120
      [ [ i, (td, mems) ] ]
121
    | _ ->
122
      map (cons (i, (td, mems))) paths
123
  in
124
  let rec aux paths m =
125
    map
126
      (fun (i, (td, _)) ->
127
        try
128
          let m = find_machine (node_name td) machines in
129
          aux (grow paths i td m.mmemory) m
130
        with Not_found -> grow paths i td [])
131
      m.minstances
132
    |> flatten
133
  in
134
  aux [] m |> map rev
135

    
136
let memories insts =
137
  List.(
138
    map
139
      (fun path ->
140
        let _, (_, mems) = hd (rev path) in
141
        map (fun mem -> path, mem) mems)
142
      insts
143
    |> flatten)
144

    
145
let pp_instance ?(indirect = true) pp ptr =
146
  pp_print_list
147
    ~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
148
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
149
    (fun fmt (i, _) -> pp_print_string fmt i)
150

    
151
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
152
  pp_access
153
    ((if indirect then pp_indirect else pp_access)
154
       (pp_instance ~indirect pp_print_string ptr)
155
       pp_print_string)
156
    pp_var_decl
157
    fmt
158
    ((path, "_reg"), mem)
159

    
160
let prefixes l =
161
  let rec pref acc = function
162
    | x :: l ->
163
      pref ([ x ] :: List.map (List.cons x) acc) l
164
    | [] ->
165
      acc
166
  in
167
  pref [] (List.rev l)
168

    
169
let powerset_instances paths =
170
  List.map prefixes paths |> List.flatten |> remove_duplicates
171

    
172
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
173
  fprintf
174
    fmt
175
    "\\separated(@[<v>%a, %a%a%a@])"
176
    pp_self
177
    self
178
    pp_mem
179
    mem
180
    (pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))
181
    paths
182
    (pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
183
    ptrs
184

    
185
let pp_separated' self mem fmt (paths, ptrs) =
186
  pp_separated
187
    pp_print_string
188
    pp_print_string
189
    pp_var_decl
190
    fmt
191
    (self, mem, paths, ptrs)
192

    
193
let pp_separated'' =
194
  pp_comma_list
195
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
196
    ~pp_epilogue:pp_print_cpar
197
    pp_var_decl
198

    
199
let pp_forall pp_l pp_r fmt (l, r) =
200
  fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
201

    
202
let pp_exists pp_l pp_r fmt (l, r) =
203
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
204

    
205
let pp_equal 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) =
246
  fprintf fmt "%s_init(%a)" name pp_mem mem
247

    
248
let pp_initialization' = pp_initialization pp_print_string
249

    
250
let pp_local m =
251
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
252

    
253
let pp_locals m =
254
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
255

    
256
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
257

    
258
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
259
  if Types.is_real_type typ && !Options.mpfr then assert false
260
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
261
  else pp_equal pp_l pp_r fmt (var_name, value)
262

    
263
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
264
    (var_type, var_name, value) =
265
  let depth = expansion_depth value in
266
  let loop_vars = mk_loop_variables m var_type depth in
267
  let reordered_loop_vars = reorder_loop_variables loop_vars in
268
  let aux typ fmt vars =
269
    match vars with
270
    | [] ->
271
      pp_basic_assign_spec
272
        (pp_value_suffix
273
           ~indirect:indirect_l
274
           m
275
           self_l
276
           var_type
277
           loop_vars
278
           pp_var_l)
279
        (pp_value_suffix
280
           ~indirect:indirect_r
281
           m
282
           self_r
283
           var_type
284
           loop_vars
285
           pp_var_r)
286
        fmt
287
        typ
288
        var_name
289
        value
290
    | (_d, LVar _i) :: _q ->
291
      assert false
292
    (* let typ' = Types.array_element_type typ in
293
     * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
294
     *   i i i pp_c_dimension d i
295
     *   (aux typ') q *)
296
    | (_d, LInt _r) :: _q ->
297
      assert false
298
    (* let typ' = Types.array_element_type typ in
299
     * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
300
     * fprintf fmt "@[<v 2>{@,%a@]@,}"
301
     *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
302
    | _ ->
303
      assert false
304
  in
305
  reset_loop_counter ();
306
  aux var_type fmt reordered_loop_vars
307

    
308
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
309
  fprintf
310
    fmt
311
    "%s_pack%a(@[<hov>%a,@ %a@])"
312
    name
313
    (pp_print_option pp_print_int)
314
    i
315
    pp_mem
316
    mem
317
    pp_self
318
    self
319

    
320
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
321
  pp_memory_pack_aux
322
    ?i:mp.mpindex
323
    pp_mem
324
    pp_self
325
    fmt
326
    (mp.mpname.node_id, mem, self)
327

    
328
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
329
    (name, vars, mem_in, mem_out) =
330
  let stateless = fst (get_stateless_status m) in
331
  fprintf
332
    fmt
333
    "%s_transition%a(@[<hov>%t%a%t@])"
334
    name
335
    (pp_print_option pp_print_int)
336
    i
337
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
338
    (pp_comma_list
339
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
340
       pp_var)
341
    vars
342
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
343

    
344
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
345
  pp_transition_aux
346
    ?i:t.tindex
347
    m
348
    pp_mem_in
349
    pp_mem_out
350
    pp_var
351
    fmt
352
    (t.tname.node_id, t.tvars, mem_in, mem_out)
353

    
354
let pp_transition_aux' ?i m =
355
  pp_transition_aux ?i m 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 (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
        m
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
507
    | Fun (_, vl) ->
508
      List.exists has_mem vl
509
    | Access (t, i)
510
    | Power (t, i) ->
511
      has_mem t || has_mem i
512
    | _ ->
513
      false
514

    
515
  let has_memory : type a. machine_t -> (value_t, a) expression_t -> bool = fun m -> function
516
    | Val v -> has_memory_val m v
517
    | _ -> false
518

    
519
  let pp_spec mode m =
520
    let rec pp_spec mode fmt f =
521
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
522
        let self = mk_self m in
523
        let mem = mk_mem m in
524
        let mem_in = mk_mem_in m in
525
        let mem_out = mk_mem_out m in
526
        let mem_reset = mk_mem_reset m in
527
        match mode with
528
        | MemoryPackMode ->
529
          self, self, true, mem, mem, false
530
        | TransitionMode ->
531
          mem_in, mem_in, false, mem_out, mem_out, false
532
        | TransitionFootprintMode ->
533
          mem_in, mem_in, false, mem_out, mem_out, false
534
        | ResetIn ->
535
          mem_reset, mem_reset, false, mem_out, mem_out, false
536
        | ResetOut ->
537
          mem_in, mem_in, false, mem_reset, mem_reset, false
538
        | InstrMode self ->
539
          let mem = "*" ^ mem in
540
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
541
          self, flush_str_formatter (), false, mem, mem, false
542
      in
543
      let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
544
       fun fmt e -> pp_expr m mem_out fmt e
545
      in
546
      let pp_spec' = pp_spec mode in
547
      match f with
548
      | True ->
549
        pp_true fmt ()
550
      | False ->
551
        pp_false fmt ()
552
      | Equal (a, b) ->
553
        let pp_eq fmt () =
554
          pp_assign_spec
555
            m
556
            mem_out
557
            (pp_c_var_read ~test_output:false m)
558
            indirect_l
559
            mem_in
560
            (pp_c_var_read ~test_output:false m)
561
            indirect_r
562
            fmt
563
            (type_of_l_value a, val_of_expr a, val_of_expr b)
564
        in
565
        if has_memory m b then
566
          let inst = find_arrow m in
567
          pp_paren
568
            (pp_implies
569
               (pp_not (pp_initialization pp_access'))
570
               pp_eq)
571
            fmt
572
            ((Arrow.arrow_id, (mem_in, inst)), ())
573
        else
574
          pp_eq fmt ()
575
      | And fs ->
576
        pp_and_l pp_spec' fmt fs
577
      | Or fs ->
578
        pp_or_l pp_spec' fmt fs
579
      | Imply (a, b) ->
580
        pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
581
      | Exists (xs, a) ->
582
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
583
      | Forall (xs, a) ->
584
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
585
      | Ternary (e, a, b) ->
586
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
587
      | Predicate p ->
588
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
589
      | StateVarPack ResetFlag ->
590
        let r = vdecl_to_val reset_flag in
591
        pp_assign_spec
592
          m
593
          mem_out
594
          (pp_c_var_read ~test_output:false m)
595
          indirect_l
596
          mem_in
597
          (pp_c_var_read ~test_output:false m)
598
          indirect_r
599
          fmt
600
          (Type_predef.type_bool, r, r)
601
      | StateVarPack (StateVar v) ->
602
        let v' = vdecl_to_val v in
603
        let inst = find_arrow m in
604
        pp_paren
605
          (pp_implies
606
             (pp_not (pp_initialization pp_access'))
607
             (pp_assign_spec
608
                m
609
                mem_out
610
                (pp_c_var_read ~test_output:false m)
611
                indirect_l
612
                mem_in
613
                (pp_c_var_read ~test_output:false m)
614
                indirect_r))
615
          fmt
616
          ((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
617
      | ExistsMem (f, rc, tr) ->
618
        pp_exists
619
          (pp_machine_decl' ~ghost:true)
620
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
621
          fmt
622
          ((f, mk_mem_reset m), (rc, tr))
623
      | Value v ->
624
        pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
625

    
626
    in
627
    pp_spec mode
628
end
629

    
630
let pp_predicate pp_l pp_r fmt (l, r) =
631
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
632

    
633
let pp_lemma pp_l pp_r fmt (l, r) =
634
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
635

    
636
let pp_axiomatic pp_l pp_r fmt (l, r) =
637
  fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
638

    
639
let pp_axiom pp_l pp_r fmt (l, r) =
640
  fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
641

    
642
let pp_mem_valid_def fmt m =
643
  if not (fst (get_stateless_status m)) then
644
    let name = m.mname.node_id in
645
    let self = mk_self m in
646
    pp_acsl
647
      (pp_predicate
648
         (pp_mem_valid (pp_machine_decl pp_ptr))
649
         (pp_and
650
            (pp_and_l (fun fmt (inst, (td, _)) ->
651
                 if Arrow.td_is_arrow td then
652
                   pp_valid pp_indirect' fmt [ self, inst ]
653
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
654
            (pp_valid pp_print_string)))
655
      fmt
656
      ((name, (name, self)), (m.minstances, [ self ]))
657

    
658
let pp_memory_pack_def m fmt mp =
659
  let name = mp.mpname.node_id in
660
  let self = mk_self m in
661
  let mem = mk_mem m in
662
  pp_acsl
663
    (pp_predicate
664
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
665
       (PrintSpec.pp_spec MemoryPackMode m))
666
    fmt
667
    ((mp, (name, mem), (name, self)), mp.mpformula)
668

    
669
let pp_machine_ghost_struct fmt m =
670
  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
671

    
672
let pp_memory_pack_defs fmt m =
673
  if not (fst (get_stateless_status m)) then
674
    fprintf
675
      fmt
676
      "%a@,%a"
677
      pp_machine_ghost_struct
678
      m
679
      (pp_print_list
680
         ~pp_epilogue:pp_print_cut
681
         ~pp_open_box:pp_open_vbox0
682
         (pp_memory_pack_def m))
683
      m.mspec.mmemory_packs
684

    
685
let pp_transition_def m fmt t =
686
  let name = t.tname.node_id in
687
  let mem_in = mk_mem_in m in
688
  let mem_out = mk_mem_out m in
689
  pp_acsl
690
    (pp_predicate
691
       (pp_transition
692
          m
693
          (pp_machine_decl' ~ghost:true)
694
          (pp_machine_decl' ~ghost:true)
695
          (pp_local m))
696
       (PrintSpec.pp_spec TransitionMode m))
697
    fmt
698
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
699

    
700
let pp_transition_defs fmt m =
701
  pp_print_list
702
    ~pp_epilogue:pp_print_cut
703
    ~pp_open_box:pp_open_vbox0
704
    (pp_transition_def m)
705
    fmt
706
    m.mspec.mtransitions
707

    
708
let pp_transition_footprint fmt t =
709
  fprintf
710
    fmt
711
    "%s_transition%a_footprint"
712
    t.tname.node_id
713
    (pp_print_option pp_print_int)
714
    t.tindex
715

    
716
let pp_transition_footprint_lemma m fmt t =
717
  let name = t.tname.node_id in
718
  let mem_in = mk_mem_in m in
719
  let mem_out = mk_mem_out m in
720
  let mems =
721
    ISet.(
722
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
723
  in
724
  let insts =
725
    IMap.(
726
      diff
727
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
728
        t.tinst_footprint)
729
  in
730
  let memories =
731
    List.map
732
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
733
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
734
  in
735
  let mems_empty = ISet.is_empty mems in
736
  let insts_empty = IMap.is_empty insts in
737
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
738
  let tr ?mems ?insts () =
739
    Spec_common.mk_transition
740
      ?mems
741
      ?insts
742
      ?i:t.tindex
743
      name
744
      (vdecls_to_vals t.tvars)
745
  in
746
  if not (mems_empty && insts_empty) then
747
    pp_acsl
748
      (pp_lemma
749
         pp_transition_footprint
750
         (pp_forall
751
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
752
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
753
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
754
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
755
                else pp_forall (pp_locals m))
756
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
757
      fmt
758
      ( t,
759
        ( (m.mname.node_id, [ mem_in; mem_out ]),
760
          ( instances,
761
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
762
      )
763

    
764
let pp_transition_footprint_lemmas fmt m =
765
  pp_print_list
766
    ~pp_epilogue:pp_print_cut
767
    ~pp_open_box:pp_open_vbox0
768
    (pp_transition_footprint_lemma m)
769
    fmt
770
    (List.filter
771
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
772
       m.mspec.mtransitions)
773

    
774
let pp_initialization_def fmt m =
775
  if not (fst (get_stateless_status m)) then
776
    let name = m.mname.node_id in
777
    let mem_in = mk_mem_in m in
778
    pp_acsl
779
      (pp_predicate
780
         (pp_initialization (pp_machine_decl' ~ghost:true))
781
         (pp_and_l (fun fmt (i, (td, _)) ->
782
              if Arrow.td_is_arrow td then
783
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
784
              else
785
                pp_equal
786
                  (pp_reset_flag ~indirect:false pp_access')
787
                  pp_print_int
788
                  fmt
789
                  ((mem_in, i), 1))))
790
      fmt
791
      ((name, (name, mem_in)), m.minstances)
792

    
793
let pp_reset_cleared_def fmt m =
794
  if not (fst (get_stateless_status m)) then
795
    let name = m.mname.node_id in
796
    let mem_in = mk_mem_in m in
797
    let mem_out = mk_mem_out m in
798
    pp_acsl
799
      (pp_predicate
800
         (pp_reset_cleared
801
            (pp_machine_decl' ~ghost:true)
802
            (pp_machine_decl' ~ghost:true))
803
         (pp_ite
804
            (pp_reset_flag' ~indirect:false)
805
            (pp_and
806
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
807
               pp_initialization')
808
            (pp_equal pp_print_string pp_print_string)))
809
      fmt
810
      ( (name, (name, mem_in), (name, mem_out)),
811
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
812

    
813
let pp_register_chain ?(indirect = true) ptr =
814
  pp_print_list
815
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
816
    ~pp_epilogue:(fun fmt () ->
817
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
818
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
819
    (fun fmt (i, _) -> pp_print_string fmt i)
820

    
821
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
822
  pp_print_list
823
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
824
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
825
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
826
    (fun fmt (i, _) -> pp_print_string fmt i)
827
    fmt
828
    mems
829

    
830
let pp_arrow_reset_ghost mem fmt inst =
831
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
832

    
833
module GhostProto : MODIFIERS_GHOST_PROTO = struct
834
  let pp_ghost_parameters ?(cut = true) fmt vs =
835
    fprintf
836
      fmt
837
      "%a%a"
838
      (if cut then pp_print_cut else pp_print_nothing)
839
      ()
840
      (pp_acsl_line'
841
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
842
      vs
843
end
844

    
845
module HdrMod = struct
846
  module GhostProto = GhostProto
847

    
848
  let pp_machine_decl_prefix _ _ = ()
849

    
850
  let pp_import_arrow fmt () =
851
    fprintf
852
      fmt
853
      "#include \"%s/arrow_spec.h%s\""
854
      (Arrow.arrow_top_decl ()).top_decl_owner
855
      (if !Options.cpp then "pp" else "")
856

    
857
  let pp_predicates fmt machines =
858
    let pp_preds comment pp =
859
      pp_print_list
860
        ~pp_open_box:pp_open_vbox0
861
        ~pp_prologue:(pp_print_endcut comment)
862
        pp
863
        ~pp_epilogue:pp_print_cutcut
864
    in
865
    fprintf
866
      fmt
867
      "%a%a"
868
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
869
      machines
870
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
871
      machines
872

    
873
  let pp_machine_alloc_decl fmt m =
874
    pp_machine_decl_prefix fmt m;
875
    if not (fst (get_stateless_status m)) then
876
      if !Options.static_mem then
877
        (* Static allocation *)
878
        let macro = m, mk_attribute m, mk_instance m in
879
        fprintf
880
          fmt
881
          "%a@,%a@,%a"
882
          (pp_static_declare_macro ~ghost:true)
883
          macro
884
          (pp_static_link_macro ~ghost:true)
885
          macro
886
          (pp_static_alloc_macro ~ghost:true)
887
          macro
888
      else
889
        (* Dynamic allocation *)
890
        (* TODO: handle dynamic alloc *)
891
        assert false
892
  (* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
893
   *   (m.mname.node_id, m.mstatic)
894
   *   pp_dealloc_prototype m.mname.node_id *)
895
end
896

    
897
module SrcMod = struct
898
  module GhostProto = GhostProto
899

    
900
  let pp_predicates fmt machines =
901
    let pp_preds comment pp =
902
      pp_print_list
903
        ~pp_open_box:pp_open_vbox0
904
        ~pp_prologue:(pp_print_endcut comment)
905
        pp
906
        ~pp_epilogue:pp_print_cutcut
907
    in
908
    fprintf
909
      fmt
910
      "%a%a%a%a%a%a"
911
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
912
      machines
913
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
914
      machines
915
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
916
      machines
917
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
918
      machines
919
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
920
      machines
921
      (pp_preds
922
         "/* ACSL transition memory footprints lemmas */"
923
         pp_transition_footprint_lemmas)
924
      machines
925

    
926
  let pp_clear_reset_spec fmt self mem m =
927
    let name = m.mname.node_id in
928
    let arws, narws =
929
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
930
    in
931
    let mk_insts = List.map (fun x -> [ x ]) in
932
    pp_acsl_cut
933
      (fun fmt () ->
934
        fprintf
935
          fmt
936
          "%a@,\
937
           %a@,\
938
           %a@,\
939
           %a@,\
940
           %a@,\
941
           %a@,\
942
           %a@,\
943
           %a@,\
944
           %a@,\
945
           %a@,\
946
           @[<v 2>behavior reset:@;\
947
           %a@,\
948
           %a@]@,\
949
           @[<v 2>behavior no_reset:@;\
950
           %a@,\
951
           %a@]@,\
952
           complete behaviors;@,\
953
           disjoint behaviors;"
954
          (pp_requires pp_mem_valid')
955
          (name, self)
956
          (pp_requires (pp_separated' self mem))
957
          (mk_insts m.minstances, [])
958
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
959
          (name, mem, self)
960
          (pp_ensures
961
             (pp_memory_pack_aux
962
                ~i:(List.length m.mspec.mmemory_packs - 2)
963
                pp_ptr
964
                pp_print_string))
965
          (name, mem, self)
966
          (pp_assigns pp_reset_flag')
967
          [ self ]
968
          (pp_assigns (pp_register_chain self))
969
          (mk_insts arws)
970
          (pp_assigns (pp_reset_flag_chain self))
971
          (mk_insts narws)
972
          (pp_assigns pp_reset_flag')
973
          [ mem ]
974
          (pp_assigns (pp_register_chain ~indirect:false mem))
975
          (mk_insts arws)
976
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
977
          (mk_insts narws)
978
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
979
          (mem, 1)
980
          (pp_ensures (pp_initialization pp_ptr))
981
          (name, mem)
982
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
983
          (mem, 0)
984
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
985
          (mem, mem))
986
      fmt
987
      ()
988

    
989
  let pp_set_reset_spec fmt self mem m =
990
    let name = m.mname.node_id in
991
    pp_acsl_cut
992
      (fun fmt () ->
993
        fprintf
994
          fmt
995
          "%a@,%a@,%a"
996
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
997
          (name, mem, self)
998
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
999
          (mem, 1)
1000
          (pp_assigns pp_reset_flag')
1001
          [ self; mem ])
1002
      fmt
1003
      ()
1004

    
1005
  let spec_from_contract c =
1006
    Spec_common.red (Imply (c.mc_pre, c.mc_post))
1007

    
1008
  let pp_contract m fmt c =
1009
    PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
1010

    
1011
  let contract_of machines m =
1012
    match m.mspec.mnode_spec with
1013
    | Some spec ->
1014
      begin match spec with
1015
        | Contract c ->
1016
          Some c, None
1017
        | NodeSpec f ->
1018
          let m_f = find_machine f machines in
1019
          begin match m_f.mspec.mnode_spec with
1020
            | Some (Contract c) ->
1021
              Some c, Some m_f
1022
            | _ ->
1023
              None, None
1024
          end
1025
      end
1026
    | None ->
1027
      None, None
1028

    
1029
  let pp_init_def fmt m =
1030
    let name = m.mname.node_id in
1031
    let mem = mk_mem m in
1032
    pp_predicate
1033
      (pp_init (pp_machine_decl' ~ghost:true))
1034
      (pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
1035
      fmt
1036
      ((name, (name, mem)), ((name, mem), mem))
1037

    
1038
  let rename n x = sprintf "%s_%d" x n
1039

    
1040
  let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
1041

    
1042
  let rec rename_value n v =
1043
    { v with value_desc =
1044
                match v.value_desc with
1045
                  | Machine_code_types.Var v -> Machine_code_types.Var (rename_var_decl n v)
1046
                  | Fun (f, vs) -> Fun (f, List.map (rename_value n) vs)
1047
                  | Array vs -> Array (List.map (rename_value n) vs)
1048
                  | Access (v1, v2) -> Access (rename_value n v1, rename_value n v2)
1049
                  | Power (v1, v2) -> Power (rename_value n v1, rename_value n v2)
1050
                  | v -> v
1051
    }
1052

    
1053
  let rename_expression: type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t =
1054
    fun n -> function
1055
    | Val v -> Val (rename_value n v)
1056
    | Var v -> Var (rename_var_decl n v)
1057
    | e -> e
1058

    
1059
  let rename_predicate n = function
1060
    | Transition (f, inst, i, es, r, mf, mif) ->
1061
      Transition (f, inst, i, List.map (rename_expression n) es, r, mf, mif)
1062
    | p -> p
1063

    
1064
  let rec rename_formula n = function
1065
    | Equal (e1, e2) -> Equal (rename_expression n e1, rename_expression n e2)
1066
    | And fs -> And (List.map (rename_formula n) fs)
1067
    | Or fs -> Or (List.map (rename_formula n) fs)
1068
    | Imply (f1, f2) -> Imply (rename_formula n f1, rename_formula n f2)
1069
    | Exists (xs, f) -> Exists (List.map (rename_var_decl n) xs, rename_formula n f)
1070
    | Forall (xs, f) -> Forall (List.map (rename_var_decl n) xs, rename_formula n f)
1071
    | Ternary (e, t, f) -> Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
1072
    | Predicate p -> Predicate (rename_predicate n p)
1073
    | ExistsMem (x, f1, f2) -> ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
1074
    | Value v -> Value (rename_value n v)
1075
    | f -> f
1076

    
1077
    
1078
  let rename_contract n c =
1079
    { c with
1080
      mc_pre = rename_formula n c.mc_pre;
1081
      mc_post = rename_formula n c.mc_post; }
1082

    
1083
  let but_last l =
1084
    List.(rev (tl (rev l)))
1085

    
1086
  let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt (n, mem_in, mem_out) =
1087
    let name = m.mname.node_id in
1088
    let inputs = m.mstep.step_inputs in
1089
    let outputs = m.mstep.step_outputs in
1090
    fprintf fmt "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
1091
      name
1092
      case
1093
      n
1094
      pp_mem_in
1095
      mem_in
1096
      pp_vars
1097
      (inputs @ outputs)
1098
      pp_mem_out
1099
      mem_out
1100

    
1101
  let pp_k_induction_base_case m =
1102
    pp_k_induction_case "base" m
1103

    
1104
  let pp_k_induction_inductive_case m =
1105
    pp_k_induction_case "inductive" m
1106

    
1107
  let pp_base_cases m fmt (c, m_c, k) =
1108
    let name = m.mname.node_id in
1109
    let mem = mk_mem m in
1110
    let inputs = m.mstep.step_inputs in
1111
    let outputs = m.mstep.step_outputs in
1112
    let l = List.init (k - 1) (fun n -> n + 1) in
1113
    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
1114
      (fun fmt n ->
1115
         let l = List.init (n + 1) (fun n -> n) in
1116
         let l' = List.init n (fun n -> n) in
1117
         let pp =
1118
           pp_implies
1119
             (pp_and
1120
                (pp_and_l (fun fmt -> function
1121
                     | 0 ->
1122
                       pp_init pp_print_string fmt (name, rename 0 mem)
1123
                     | n ->
1124
                       pp_transition_aux m pp_print_string pp_print_string pp_var_decl
1125
                         fmt
1126
                         (name,
1127
                          List.map (rename_var_decl n) (inputs @ outputs),
1128
                          rename (n - 1) mem,
1129
                          rename n mem)))
1130
                (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1131
             (pp_contract m)
1132
         in
1133
         pp_predicate
1134
           (pp_k_induction_base_case
1135
              m
1136
              (pp_machine_decl' ~ghost:true)
1137
              (pp_machine_decl' ~ghost:true)
1138
              (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
1139
           (pp_forall (pp_locals m)
1140
              (if n > 1 then
1141
                 pp_forall
1142
                   (fun fmt l -> fprintf fmt "%a@,%a"
1143
                       (pp_machine_decl ~ghost:true
1144
                          (pp_comma_list ~pp_eol:pp_print_comma
1145
                             (fun fmt n -> pp_print_string fmt (rename n mem))))
1146
                       (name, but_last l)
1147
                       (pp_locals m)
1148
                       (List.flatten
1149
                          (List.map (fun n ->
1150
                               List.map (rename_var_decl n) (inputs @ outputs))
1151
                              (List.tl l))))
1152
                   pp
1153
               else
1154
                 fun fmt (_, x) -> pp fmt x))
1155
           fmt
1156
           ((n, (name, rename (n - 1) mem), (name, rename n mem)),
1157
            (List.map (rename_var_decl n) m_c.mstep.step_outputs,
1158
             (l', ((l,
1159
                    (m_c.mname.node_id,
1160
                     List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs),
1161
                     "", "")),
1162
                   rename_contract n c)))))
1163
           fmt
1164
           l
1165

    
1166
  let pp_inductive_case m fmt (c, m_c, k) =
1167
    let name = m.mname.node_id in
1168
    let mem = mk_mem m in
1169
    let inputs = m.mstep.step_inputs in
1170
    let outputs = m.mstep.step_outputs in
1171
    let l = List.init k (fun n -> n + 1) in
1172
    let pp =
1173
      pp_implies
1174
        (pp_and_l (fun fmt n ->
1175
             pp_and
1176
               (pp_and
1177
                  (pp_transition_aux m pp_print_string pp_print_string pp_var_decl)
1178
                  (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1179
               (pp_contract m)
1180
               fmt
1181
               (((name,
1182
                  List.map (rename_var_decl n) (inputs @ outputs),
1183
                  rename (n - 1) mem,
1184
                  rename n mem),
1185
                 (m_c.mname.node_id,
1186
                  List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs),
1187
                  "", "")),
1188
                rename_contract n c)))
1189
        (pp_contract m)
1190
    in
1191
    pp_predicate
1192
      (pp_k_induction_inductive_case
1193
         m
1194
         (pp_machine_decl' ~ghost:true)
1195
         (pp_machine_decl' ~ghost:true)
1196
         (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
1197
      (pp_forall (pp_locals m)
1198
         (if k > 1 then
1199
            pp_forall
1200
              (fun fmt l -> fprintf fmt "%a@,%a"
1201
                  (pp_machine_decl ~ghost:true
1202
                     (pp_comma_list ~pp_eol:pp_print_comma
1203
                        (fun fmt n -> pp_print_string fmt (rename (n - 1) mem))))
1204
                  (name, but_last l)
1205
                  (pp_locals m)
1206
                  (List.flatten
1207
                     (List.map (fun n ->
1208
                          List.map (rename_var_decl (n - 1)) (inputs @ outputs))
1209
                         (List.tl l))))
1210
              pp
1211
          else
1212
            fun fmt (_, x) -> pp fmt x))
1213
      fmt
1214
      ((k, (name, rename (k - 1) mem), (name, rename k mem)),
1215
       (List.(flatten (List.map (fun n -> List.map (rename_var_decl n) m_c.mstep.step_outputs) l)),
1216
        (l, (l, rename_contract k c))))
1217

    
1218
  let pp_k_induction_lemmas m fmt k =
1219
    let name = m.mname.node_id in
1220
    let mem_in = mk_mem_in m in
1221
    let mem_out = mk_mem_out m in
1222
    let inputs = m.mstep.step_inputs in
1223
    let outputs = m.mstep.step_outputs in
1224
    let l = List.init k (fun n -> n + 1) in
1225
    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
1226
      (fun fmt n ->
1227
         pp_lemma
1228
           (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
1229
           (pp_forall
1230
              (fun fmt () -> fprintf fmt "%a,@;%a"
1231
                  (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1232
                  (name, [mem_in; mem_out])
1233
                  (pp_locals m)
1234
                  (inputs @ outputs))
1235
              ((if n = k then
1236
                  pp_k_induction_inductive_case
1237
                else
1238
                  pp_k_induction_base_case)
1239
                 m
1240
                 pp_print_string
1241
                 pp_print_string
1242
                 (pp_comma_list pp_var_decl)))
1243
           fmt
1244
           (n, ((), (n, mem_in, mem_out))))
1245
      fmt
1246
      l
1247

    
1248
  let pp_k_induction_axiom m fmt (c, m_c, k) =
1249
    let name = m.mname.node_id in
1250
    let mem_in = mk_mem_in m in
1251
    let mem_out = mk_mem_out m in
1252
    let inputs = m.mstep.step_inputs in
1253
    let outputs = m.mstep.step_outputs in
1254
    let l = List.init k (fun n -> n + 1) in
1255
    pp_axiomatic
1256
      (fun fmt () -> fprintf fmt "%s_k_Induction" name)
1257
      (pp_axiom
1258
         (fun fmt () -> fprintf fmt "%s_k_induction" name)
1259
         (pp_forall
1260
           (pp_locals m)
1261
           (pp_forall
1262
              (fun fmt () -> fprintf fmt "%a,@;%a"
1263
                  (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1264
                  (name, [mem_in; mem_out])
1265
                  (pp_locals m)
1266
                  (inputs @ outputs))
1267
              (pp_implies
1268
                 (pp_and
1269
                    (pp_and_l
1270
                       (fun fmt n ->
1271
                          (if n = k then
1272
                             pp_k_induction_inductive_case
1273
                           else
1274
                             pp_k_induction_base_case)
1275
                            m
1276
                            pp_print_string
1277
                            pp_print_string
1278
                            (pp_comma_list pp_var_decl)
1279
                            fmt
1280
                            (n, mem_in, mem_out)))
1281
                    (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1282
                 (pp_contract m)))))
1283
      fmt
1284
      ((),
1285
       ((),
1286
        (m_c.mstep.step_outputs,
1287
         ((),
1288
          (((l,
1289
             (m_c.mname.node_id,
1290
              m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1291
              "", "")), c))))))
1292

    
1293

    
1294
  let pp_k_induction m fmt (_, _, k as c_m_k) =
1295
    pp_acsl_cut
1296
      (fun fmt () -> fprintf fmt "%a@,@,%a@,@,%a@,@,%a@,@,%a"
1297
          pp_init_def m
1298
          (pp_base_cases m) c_m_k
1299
          (pp_inductive_case m) c_m_k
1300
          (pp_k_induction_lemmas m) k
1301
          (pp_k_induction_axiom m) c_m_k)
1302
      fmt
1303
      ()
1304

    
1305
  let pp_proof_annotation m m_c fmt c =
1306
    let pp m_c fmt = function
1307
      | Kinduction k ->
1308
        pp_k_induction m fmt (c, m_c, k)
1309
    in
1310
    match m_c with
1311
    | Some m_c ->
1312
      pp_print_option (pp m_c) fmt c.mc_proof
1313
    | None -> ()
1314

    
1315
  let pp_step_spec fmt machines self mem m =
1316
    let name = m.mname.node_id in
1317
    let insts = instances machines m in
1318
    let insts' = powerset_instances insts in
1319
    let insts'' =
1320
      List.(
1321
        filter
1322
          (fun l -> l <> [])
1323
          (map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
1324
    in
1325
    let inputs = m.mstep.step_inputs in
1326
    let outputs = m.mstep.step_outputs in
1327
    let pp_if_outputs pp =
1328
      if outputs = [] then pp_print_nothing else pp
1329
    in
1330
    let c, m_c = contract_of machines m in
1331
    (* (\* prevent printing an ensures clause with contract name *\)
1332
     * let spec =
1333
     *   match m.mspec.mnode_spec with
1334
     *   | Some (NodeSpec _) -> None
1335
     *   | s -> s
1336
     * in *)
1337
    let pp_spec = pp_print_option
1338
        (if m.mis_contract then pp_print_nothing else pp_ensures (pp_contract m)) in
1339
    let pp_spec_vars, pp_assigns_spec_vars =
1340
      match m.mspec.mnode_spec with
1341
      | Some (NodeSpec f) ->
1342
        let m_f = find_machine f machines in
1343
        pp_acsl_cut
1344
          (pp_ghost
1345
             (fun fmt () ->
1346
                fprintf
1347
                  fmt
1348
                  "@;<0 2>@[<v>%a@]"
1349
                  (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
1350
                     ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m))
1351
                  m_f.mstep.step_outputs)),
1352
        fun fmt () -> pp_assigns pp_var_decl fmt m_f.mstep.step_outputs
1353
      | _ -> pp_print_nothing, pp_print_nothing
1354
    in
1355
    pp_print_option (pp_proof_annotation m m_c) fmt c;
1356
    pp_spec_vars fmt ();
1357
    pp_acsl_cut
1358
      ~ghost:m.mis_contract
1359
      (fun fmt () ->
1360
        if fst (get_stateless_status m) then
1361
          fprintf
1362
            fmt
1363
            "%a@,%a@,%a@,%a@,%a@,%a"
1364
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1365
            outputs
1366
            (pp_if_outputs (pp_requires pp_separated''))
1367
            outputs
1368
            pp_assigns_spec_vars ()
1369
            (pp_assigns pp_ptr_decl)
1370
            outputs
1371
            (pp_ensures (pp_transition_aux' m))
1372
            (name, inputs @ outputs, "", "")
1373
            pp_spec
1374
            c
1375
        else
1376
          fprintf
1377
            fmt
1378
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
1379
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1380
            outputs
1381
            (pp_requires pp_mem_valid')
1382
            (name, self)
1383
            (pp_requires (pp_separated' self mem))
1384
            (insts', outputs)
1385
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
1386
            (name, mem, self)
1387
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
1388
            (name, mem, self)
1389
            (pp_ensures
1390
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
1391
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
1392
            (name, inputs @ outputs, mem, mem)
1393
            pp_spec
1394
            c
1395
            pp_assigns_spec_vars ()
1396
            (pp_assigns pp_ptr_decl)
1397
            outputs
1398
            (pp_assigns (pp_reg self))
1399
            m.mmemory
1400
            (pp_assigns pp_reset_flag')
1401
            [ self ]
1402
            (pp_assigns (pp_memory self))
1403
            (memories insts')
1404
            (pp_assigns (pp_register_chain self))
1405
            insts
1406
            (pp_assigns (pp_reset_flag_chain self))
1407
            insts''
1408
            (pp_assigns (pp_reg mem))
1409
            m.mmemory
1410
            (pp_assigns pp_reset_flag')
1411
            [ mem ]
1412
            (pp_assigns (pp_memory ~indirect:false mem))
1413
            (memories insts')
1414
            (pp_assigns (pp_register_chain ~indirect:false mem))
1415
            insts
1416
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1417
            insts'')
1418
      fmt
1419
      ()
1420

    
1421
  let pp_ghost_instr_code m self fmt instr =
1422
    match instr.instr_desc with
1423
    | MStateAssign (x, v) ->
1424
      fprintf
1425
        fmt
1426
        "@,%a"
1427
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
1428
        (x, v)
1429
    | MResetAssign b ->
1430
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
1431
    | MSetReset inst ->
1432
      let td, _ = List.assoc inst m.minstances in
1433
      if Arrow.td_is_arrow td then
1434
        fprintf
1435
          fmt
1436
          "@,%a;"
1437
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
1438
          inst
1439
    | _ ->
1440
      ()
1441

    
1442
  let pp_step_instr_spec m self mem fmt instr =
1443
    let ghost = m.mis_contract in
1444
    fprintf
1445
      fmt
1446
      "%a%a"
1447
      (pp_ghost_instr_code m mem)
1448
      instr
1449
      (pp_print_list
1450
         ~pp_open_box:pp_open_vbox0
1451
         ~pp_prologue:pp_print_cut
1452
         (pp_acsl_line' ~ghost (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
1453
      instr.instr_spec
1454

    
1455
  let pp_ghost_parameter mem fmt inst =
1456
    GhostProto.pp_ghost_parameters
1457
      ~cut:false
1458
      fmt
1459
      (match inst with
1460
      | Some inst ->
1461
        [ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
1462
      | None ->
1463
        [ mem, pp_print_string ])
1464

    
1465
  let pp_contract fmt machines _self mem m =
1466
    let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
1467
    match contract_of machines m with
1468
    | Some c, Some m_c ->
1469
      fprintf fmt "%a%a"
1470
        (pp_acsl_line'_cut
1471
           (pp_ghost
1472
              (fun fmt () ->
1473
                 fprintf
1474
                   fmt
1475
                   "%a(%a%a);"
1476
                   pp_machine_step_name
1477
                   m_c.mname.node_id
1478
                   (pp_vars ~pp_eol:pp_print_comma)
1479
                   m_c.mstep.step_inputs
1480
                   (pp_comma_list (pp_c_var_write m))
1481
                   m_c.mstep.step_outputs)))
1482
        ()
1483
        (pp_acsl_cut
1484
           (pp_print_option
1485
              (fun fmt -> function
1486
                 | Kinduction k ->
1487
                   let l = List.init k (fun n -> n + 1) in
1488
                   let pp_mem_in = pp_at_pre pp_ptr in
1489
                   let pp_mem_out = pp_ptr in
1490
                   pp_assert
1491
                     (pp_and
1492
                        (pp_and_l
1493
                           (fun fmt n ->
1494
                              (if n = k then
1495
                                 pp_k_induction_inductive_case
1496
                               else
1497
                                 pp_k_induction_base_case)
1498
                                m
1499
                                pp_mem_in
1500
                                pp_mem_out
1501
                                pp_vars
1502
                                fmt
1503
                                (n, mem, mem)))
1504
                        (pp_transition_aux m_c pp_print_string pp_print_string (pp_c_var_read m)))
1505
                     fmt
1506
                     (l, (m_c.mname.node_id,
1507
                          m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1508
                          "", ""))))) c.mc_proof
1509
        | _, _ -> ()
1510

    
1511
end
1512

    
1513
module MainMod = struct
1514
  let main_mem_ghost = "main_mem_ghost"
1515

    
1516
  let pp_declare_ghost_state fmt name =
1517
    pp_acsl_line'_cut
1518
      (pp_ghost (fun fmt () ->
1519
           fprintf
1520
             fmt
1521
             "%a(,%s);"
1522
             (pp_machine_static_alloc_name ~ghost:true)
1523
             name
1524
             main_mem_ghost))
1525
      fmt
1526
      ()
1527

    
1528
  let pp_ghost_state_parameter fmt () =
1529
    GhostProto.pp_ghost_parameters
1530
      ~cut:false
1531
      fmt
1532
      [ main_mem_ghost, pp_ref pp_print_string ]
1533

    
1534
  let pp_main_loop_invariants main_mem machines fmt m =
1535
    let name = m.mname.node_id in
1536
    let insts = powerset_instances (instances machines m) in
1537
    pp_acsl_cut
1538
      (fun fmt () ->
1539
        fprintf
1540
          fmt
1541
          "%a@,%a@,%a@,%a"
1542
          (pp_loop_invariant pp_mem_valid')
1543
          (name, main_mem)
1544
          (pp_loop_invariant
1545
             (pp_memory_pack_aux pp_print_string pp_print_string))
1546
          (name, main_mem_ghost, main_mem)
1547
          (pp_loop_invariant
1548
             (pp_separated
1549
                (pp_paren pp_print_string)
1550
                pp_ref'
1551
                (pp_ref pp_var_decl)))
1552
          (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
1553
          (pp_loop_invariant
1554
             (pp_or
1555
                (pp_valid_read pp_stdout)
1556
                (pp_equal pp_stdout pp_null)))
1557
          ((), ((), ())))
1558
      fmt
1559
      ()
1560

    
1561
  let pp_main_spec fmt =
1562
    pp_acsl_cut
1563
      (fun fmt () ->
1564
        fprintf
1565
          fmt
1566
          "%a@,%a@,%a@,%a"
1567
          (pp_requires
1568
             (pp_or
1569
                (pp_valid_read pp_stdout)
1570
                (pp_equal pp_stdout pp_null)))
1571
          ((), ((), ()))
1572
          (pp_terminates pp_false)
1573
          ()
1574
          (pp_ensures pp_false)
1575
          ()
1576
          (pp_assigns pp_nothing)
1577
          [ () ])
1578
      fmt
1579
      ()
1580
end
1581

    
1582
(**************************************************************************)
1583
(*                              MAKEFILE                                  *)
1584
(**************************************************************************)
1585

    
1586
module MakefileMod = struct
1587
  let other_targets fmt basename _nodename dependencies =
1588
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1589
    (* EACSL version of library file . c *)
1590
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1591
    fprintf
1592
      fmt
1593
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1594
       e-acsl -print -ocode %s_eacsl.c@."
1595
      basename
1596
      basename;
1597
    fprintf fmt "@.";
1598
    fprintf fmt "@.";
1599

    
1600
    (* EACSL version of library file . c + main .c *)
1601
    fprintf
1602
      fmt
1603
      "%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1604
      basename
1605
      basename
1606
      basename
1607
      basename;
1608
    fprintf
1609
      fmt
1610
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1611
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
1612
      basename
1613
      basename
1614
      basename;
1615
    (* Ugly hack to deal with eacsl bugs *)
1616
    fprintf
1617
      fmt
1618
      "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1619
      basename
1620
      basename;
1621
    fprintf fmt "@.";
1622
    fprintf fmt "@.";
1623

    
1624
    (* EACSL version of binary *)
1625
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1626
    fprintf
1627
      fmt
1628
      "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1629
      basename;
1630
    (* compiling instrumented lib + main *)
1631
    C_backend_makefile.fprintf_dependencies fmt dependencies;
1632
    fprintf
1633
      fmt
1634
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1635
       %s_main_eacsl.o %a@."
1636
      basename
1637
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1638
      (C_backend_makefile.compiled_dependencies dependencies)
1639
      ("${FRAMACEACSL}/e_acsl.c "
1640
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1641
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1642
      basename
1643
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1644
      (C_backend_makefile.lib_dependencies dependencies);
1645
    fprintf fmt "@."
1646
end
1647

    
1648
(* Local Variables: *)
1649
(* compile-command:"make -C ../../.." *)
1650
(* End: *)
(15-15/18)