Project

General

Profile

Download (49.2 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 find_machine f =
111
  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_implies pp_l pp_r fmt (l, r) =
206
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
207

    
208
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
209

    
210
let pp_and_l pp_v fmt =
211
  pp_print_list
212
    ~pp_open_box:pp_open_vbox0
213
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
214
    ~pp_nil:pp_true
215
    pp_v
216
    fmt
217

    
218
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
219

    
220
let pp_or_l pp_v fmt =
221
  pp_print_list
222
    ~pp_open_box:pp_open_vbox0
223
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
224
    pp_v
225
    fmt
226

    
227
let pp_not pp fmt = fprintf fmt "!%a" pp
228

    
229
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
230

    
231
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
232

    
233
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
234

    
235
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
236
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
237

    
238
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
239

    
240
let pp_initialization pp_mem fmt (name, mem) =
241
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
242

    
243
let pp_init pp_mem fmt (name, mem) =
244
  fprintf fmt "%s_init(%a)" name pp_mem mem
245

    
246
let pp_initialization' = pp_initialization pp_print_string
247

    
248
let pp_local m =
249
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
250

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

    
254
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
255

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

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

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

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

    
326
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
327
    (name, vars, mem_in, mem_out) =
328
  let stateless = fst (get_stateless_status m) in
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 m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
343
  pp_transition_aux
344
    ?i:t.tindex
345
    m
346
    pp_mem_in
347
    pp_mem_out
348
    pp_var
349
    fmt
350
    (t.tname.node_id, t.tvars, mem_in, mem_out)
351

    
352
let pp_transition_aux' ?i m =
353
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
354
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
355

    
356
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
357
  fprintf
358
    fmt
359
    "%s_reset_cleared(@[<hov>%a,@ %a@])"
360
    name
361
    pp_mem_in
362
    mem_in
363
    pp_mem_out
364
    mem_out
365

    
366
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
367

    
368
let pp_functional_update mems insts fmt mem =
369
  let rec aux fmt = function
370
    | [] ->
371
      pp_print_string fmt mem
372
    | (x, is_mem) :: fields ->
373
      fprintf
374
        fmt
375
        "{ @[<hov>%a@ \\with .%s%s = %s@] }"
376
        aux
377
        fields
378
        (if is_mem then "_reg." else "")
379
        x
380
        x
381
  in
382
  aux
383
    fmt
384
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
385
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
386

    
387
module PrintSpec = struct
388
  type mode =
389
    | MemoryPackMode
390
    | TransitionMode
391
    | TransitionFootprintMode
392
    | ResetIn
393
    | ResetOut
394
    | InstrMode of ident
395

    
396
  let pp_reg mem fmt = function
397
    | ResetFlag ->
398
      fprintf fmt "%s.%s" mem reset_flag_name
399
    | StateVar x ->
400
      fprintf fmt "%s.%a" mem pp_var_decl x
401

    
402
  let pp_expr :
403
      type a.
404
      ?test_output:bool ->
405
      machine_t ->
406
      ident ->
407
      formatter ->
408
      (value_t, a) expression_t ->
409
      unit =
410
   fun ?(test_output = false) m mem fmt -> function
411
    | Val v ->
412
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
413
    | Tag t ->
414
      pp_print_string fmt t
415
    | Var v ->
416
      pp_var_decl fmt v
417
    | Memory r ->
418
      pp_reg mem fmt r
419

    
420
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
421
    let test_output, mem_update =
422
      match mode with
423
      | InstrMode _ ->
424
        true, false
425
      | TransitionFootprintMode ->
426
        false, true
427
      | _ ->
428
        false, false
429
    in
430
    let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
431
        =
432
     fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
433
    in
434
    match p with
435
    | Transition (f, inst, i, vars, r, mems, insts) ->
436
      let pp_mem_in, pp_mem_out =
437
        match inst with
438
        | None ->
439
          ( pp_print_string,
440
            if mem_update then pp_functional_update mems insts
441
            else pp_print_string )
442
        | Some inst ->
443
          ( (fun fmt mem_in ->
444
              if r then pp_print_string fmt mem_in
445
              else pp_access' fmt (mem_in, inst)),
446
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
447
      in
448
      pp_transition_aux
449
        ?i
450
        m
451
        pp_mem_in
452
        pp_mem_out
453
        (pp_expr test_output)
454
        fmt
455
        (f, vars, mem_in', mem_out')
456
    | Reset (_f, inst, r) ->
457
      pp_ite
458
        (pp_c_val m mem_in (pp_c_var_read m))
459
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
460
        (pp_equal pp_print_string pp_access')
461
        fmt
462
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
463
    | MemoryPack (f, inst, i) ->
464
      let pp_mem, pp_self =
465
        match inst with
466
        | None ->
467
          pp_print_string, pp_print_string
468
        | Some inst ->
469
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
470
            fun fmt self -> pp_indirect' fmt (self, inst) )
471
      in
472
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
473
    | ResetCleared f ->
474
      pp_reset_cleared' fmt (f, mem_in, mem_out)
475
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
476
    | Initialization ->
477
      ()
478

    
479
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
480

    
481
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
482
    | Val v ->
483
      v
484
    | Tag t ->
485
      id_to_tag t
486
    | Var v ->
487
      vdecl_to_val v
488
    | Memory (StateVar v) ->
489
      vdecl_to_val v
490
    | Memory ResetFlag ->
491
      vdecl_to_val reset_flag
492

    
493
  let find_arrow m =
494
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
495
    with Not_found ->
496
      eprintf "Internal error: arrow not found";
497
      raise Not_found
498

    
499
  let rec has_memory_val m v =
500
    let has_mem = has_memory_val m in
501
    match v.value_desc with
502
    | Var v ->
503
      is_memory m v
504
    | Array vl
505
    | Fun (_, vl) ->
506
      List.exists has_mem vl
507
    | Access (t, i)
508
    | 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 = fun m -> function
514
    | Val v -> has_memory_val m v
515
    | _ -> false
516

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

    
624
    in
625
    pp_spec mode
626
end
627

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

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

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

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

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

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

    
667
let pp_machine_ghost_struct fmt m =
668
  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
669

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

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

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

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

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

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

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

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

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

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

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

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

    
843
module HdrMod = struct
844
  module GhostProto = GhostProto
845

    
846
  let pp_machine_decl_prefix _ _ = ()
847

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

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

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

    
895
module SrcMod = struct
896
  module GhostProto = GhostProto
897

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

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

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

    
1003
  let spec_from_contract c =
1004
    Spec_common.red (Imply (c.mc_pre, c.mc_post))
1005

    
1006
  let pp_contract m fmt c =
1007
    PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
1008

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

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

    
1036
  let rename n x = sprintf "%s_%d" x n
1037

    
1038
  let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
1039

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

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

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

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

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

    
1081
  let but_last l =
1082
    List.(rev (tl (rev l)))
1083

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

    
1099
  let pp_k_induction_base_case m =
1100
    pp_k_induction_case "base" m
1101

    
1102
  let pp_k_induction_inductive_case m =
1103
    pp_k_induction_case "inductive" m
1104

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

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

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

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

    
1291

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

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

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

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

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

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

    
1463
  let pp_contract fmt machines _self m =
1464
    match m.mspec.mnode_spec with
1465
    | Some (NodeSpec f) ->
1466
      let m_f = find_machine f machines in
1467
      pp_acsl_line'_cut
1468
        (pp_ghost
1469
           (fun fmt () ->
1470
              fprintf
1471
                fmt
1472
                "%a(%a%a);"
1473
                pp_machine_step_name
1474
                m_f.mname.node_id
1475
                (pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m))
1476
                m_f.mstep.step_inputs
1477
                (pp_comma_list (pp_c_var_write m))
1478
                m_f.mstep.step_outputs))
1479
        fmt ()
1480
    | _ -> ()
1481

    
1482
end
1483

    
1484
module MainMod = struct
1485
  let main_mem_ghost = "main_mem_ghost"
1486

    
1487
  let pp_declare_ghost_state fmt name =
1488
    pp_acsl_line'_cut
1489
      (pp_ghost (fun fmt () ->
1490
           fprintf
1491
             fmt
1492
             "%a(,%s);"
1493
             (pp_machine_static_alloc_name ~ghost:true)
1494
             name
1495
             main_mem_ghost))
1496
      fmt
1497
      ()
1498

    
1499
  let pp_ghost_state_parameter fmt () =
1500
    GhostProto.pp_ghost_parameters
1501
      ~cut:false
1502
      fmt
1503
      [ main_mem_ghost, pp_ref pp_print_string ]
1504

    
1505
  let pp_main_loop_invariants main_mem machines fmt m =
1506
    let name = m.mname.node_id in
1507
    let insts = powerset_instances (instances machines m) in
1508
    pp_acsl_cut
1509
      (fun fmt () ->
1510
        fprintf
1511
          fmt
1512
          "%a@,%a@,%a@,%a"
1513
          (pp_loop_invariant pp_mem_valid')
1514
          (name, main_mem)
1515
          (pp_loop_invariant
1516
             (pp_memory_pack_aux pp_print_string pp_print_string))
1517
          (name, main_mem_ghost, main_mem)
1518
          (pp_loop_invariant
1519
             (pp_separated
1520
                (pp_paren pp_print_string)
1521
                pp_ref'
1522
                (pp_ref pp_var_decl)))
1523
          (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
1524
          (pp_loop_invariant
1525
             (pp_or
1526
                (pp_valid_read pp_stdout)
1527
                (pp_equal pp_stdout pp_null)))
1528
          ((), ((), ())))
1529
      fmt
1530
      ()
1531

    
1532
  let pp_main_spec fmt =
1533
    pp_acsl_cut
1534
      (fun fmt () ->
1535
        fprintf
1536
          fmt
1537
          "%a@,%a@,%a@,%a"
1538
          (pp_requires
1539
             (pp_or
1540
                (pp_valid_read pp_stdout)
1541
                (pp_equal pp_stdout pp_null)))
1542
          ((), ((), ()))
1543
          (pp_terminates pp_false)
1544
          ()
1545
          (pp_ensures pp_false)
1546
          ()
1547
          (pp_assigns pp_nothing)
1548
          [ () ])
1549
      fmt
1550
      ()
1551
end
1552

    
1553
(**************************************************************************)
1554
(*                              MAKEFILE                                  *)
1555
(**************************************************************************)
1556

    
1557
module MakefileMod = struct
1558
  let other_targets fmt basename _nodename dependencies =
1559
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1560
    (* EACSL version of library file . c *)
1561
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1562
    fprintf
1563
      fmt
1564
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1565
       e-acsl -print -ocode %s_eacsl.c@."
1566
      basename
1567
      basename;
1568
    fprintf fmt "@.";
1569
    fprintf fmt "@.";
1570

    
1571
    (* EACSL version of library file . c + main .c *)
1572
    fprintf
1573
      fmt
1574
      "%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1575
      basename
1576
      basename
1577
      basename
1578
      basename;
1579
    fprintf
1580
      fmt
1581
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1582
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
1583
      basename
1584
      basename
1585
      basename;
1586
    (* Ugly hack to deal with eacsl bugs *)
1587
    fprintf
1588
      fmt
1589
      "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1590
      basename
1591
      basename;
1592
    fprintf fmt "@.";
1593
    fprintf fmt "@.";
1594

    
1595
    (* EACSL version of binary *)
1596
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1597
    fprintf
1598
      fmt
1599
      "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1600
      basename;
1601
    (* compiling instrumented lib + main *)
1602
    C_backend_makefile.fprintf_dependencies fmt dependencies;
1603
    fprintf
1604
      fmt
1605
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1606
       %s_main_eacsl.o %a@."
1607
      basename
1608
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1609
      (C_backend_makefile.compiled_dependencies dependencies)
1610
      ("${FRAMACEACSL}/e_acsl.c "
1611
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1612
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1613
      basename
1614
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1615
      (C_backend_makefile.lib_dependencies dependencies);
1616
    fprintf fmt "@."
1617
end
1618

    
1619
(* Local Variables: *)
1620
(* compile-command:"make -C ../../.." *)
1621
(* End: *)
(15-15/18)