Project

General

Profile

Download (34.9 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
open Utils
12
open Format
13
open Lustre_types
14
open Machine_code_types
15
open C_backend_common
16
open Corelang
17
open Spec_types
18
open Machine_code_common
19
module Mpfr = Lustrec_mpfr
20

    
21
(**************************************************************************)
22
(*     Printing spec for c *)
23

    
24
(**************************************************************************)
25

    
26
let pp_acsl_basic_type_desc t_desc =
27
  if Types.is_bool_type t_desc then
28
    (* if !Options.cpp then "bool" else "_Bool" *)
29
    "_Bool"
30
  else if Types.is_int_type t_desc then
31
    (* !Options.int_type *)
32
    if t_desc.tid = -1 then "int" else "integer"
33
  else if Types.is_real_type t_desc then
34
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
35
  else assert false
36
(* Not a basic C type. Do not handle arrays or pointers *)
37

    
38
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
39

    
40
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
41

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

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

    
46
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
47

    
48
let pp_requires pp fmt = fprintf fmt "requires %a;" pp
49

    
50
let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
51

    
52
let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
53

    
54
let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
55

    
56
let pp_assigns pp =
57
  pp_comma_list
58
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
59
    ~pp_epilogue:pp_print_semicolon'
60
    pp
61

    
62
let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
63

    
64
let pp_assert pp fmt = fprintf fmt "assert %a;" pp
65

    
66
let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
67

    
68
let pp_mem_valid pp_var fmt (name, var) =
69
  fprintf fmt "%s_valid(%a)" name pp_var var
70

    
71
let pp_mem_valid' = pp_mem_valid pp_print_string
72

    
73
let pp_ref pp fmt = fprintf fmt "&%a" pp
74

    
75
let pp_ref' = pp_ref pp_print_string
76

    
77
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
78
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
79

    
80
let pp_indirect' = pp_indirect pp_print_string pp_print_string
81

    
82
let pp_access pp_stru pp_field fmt (stru, field) =
83
  fprintf fmt "%a.%a" pp_stru stru pp_field field
84

    
85
let pp_access' = pp_access pp_print_string pp_print_string
86

    
87
let pp_var_decl fmt v = pp_print_string fmt v.var_id
88

    
89
let pp_reg self fmt field =
90
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
91

    
92
let pp_true fmt () = pp_print_string fmt "\\true"
93

    
94
let pp_false fmt () = pp_print_string fmt "\\false"
95

    
96
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
97

    
98
let pp_null fmt () = pp_print_string fmt "\\null"
99

    
100
let pp_stdout fmt () = pp_print_string fmt "stdout"
101

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

    
104
let instances machines m =
105
  let open List in
106
  let grow paths i td mems =
107
    match paths with
108
    | [] ->
109
      [ [ i, (td, mems) ] ]
110
    | _ ->
111
      map (cons (i, (td, mems))) paths
112
  in
113
  let rec aux paths m =
114
    map
115
      (fun (i, (td, _)) ->
116
        try
117
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
118
          aux (grow paths i td m.mmemory) m
119
        with Not_found -> grow paths i td [])
120
      m.minstances
121
    |> flatten
122
  in
123
  aux [] m |> map rev
124

    
125
let memories insts =
126
  List.(
127
    map
128
      (fun path ->
129
        let _, (_, mems) = hd (rev path) in
130
        map (fun mem -> path, mem) mems)
131
      insts
132
    |> flatten)
133

    
134
let pp_instance ?(indirect = true) pp ptr =
135
  pp_print_list
136
    ~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
137
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
138
    (fun fmt (i, _) -> pp_print_string fmt i)
139

    
140
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
141
  pp_access
142
    ((if indirect then pp_indirect else pp_access)
143
       (pp_instance ~indirect pp_print_string ptr)
144
       pp_print_string)
145
    pp_var_decl
146
    fmt
147
    ((path, "_reg"), mem)
148

    
149
let prefixes l =
150
  let rec pref acc = function
151
    | x :: l ->
152
      pref ([ x ] :: List.map (List.cons x) acc) l
153
    | [] ->
154
      acc
155
  in
156
  pref [] (List.rev l)
157

    
158
let powerset_instances paths =
159
  List.map prefixes paths |> List.flatten |> remove_duplicates
160

    
161
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
162
  fprintf
163
    fmt
164
    "\\separated(@[<v>%a, %a@;%a@;%a@])"
165
    pp_self
166
    self
167
    pp_mem
168
    mem
169
    (pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance pp_self self))
170
    paths
171
    (pp_comma_list ~pp_prologue:pp_print_comma' pp_ptr)
172
    ptrs
173

    
174
let pp_separated' self mem fmt (paths, ptrs) =
175
  pp_separated
176
    pp_print_string
177
    pp_print_string
178
    pp_var_decl
179
    fmt
180
    (self, mem, paths, ptrs)
181

    
182
let pp_separated'' =
183
  pp_comma_list
184
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
185
    ~pp_epilogue:pp_print_cpar
186
    pp_var_decl
187

    
188
let pp_forall pp_l pp_r fmt (l, r) =
189
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
190

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

    
194
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
195

    
196
let pp_implies pp_l pp_r fmt (l, r) =
197
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
198

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

    
201
let pp_and_l pp_v fmt =
202
  pp_print_list
203
    ~pp_open_box:pp_open_vbox0
204
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
205
    pp_v
206
    fmt
207

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

    
210
let pp_or_l pp_v fmt =
211
  pp_print_list
212
    ~pp_open_box:pp_open_vbox0
213
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
214
    pp_v
215
    fmt
216

    
217
let pp_not pp fmt = fprintf fmt "!%a" pp
218

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

    
221
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
222

    
223
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
224

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

    
228
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
229

    
230
let pp_initialization pp_mem fmt (name, mem) =
231
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
232

    
233
let pp_initialization' = pp_initialization pp_print_string
234

    
235
let pp_local m =
236
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
237

    
238
let pp_locals m =
239
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
240

    
241
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
242

    
243
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
244
  if Types.is_real_type typ && !Options.mpfr then assert false
245
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
246
  else pp_equal pp_l pp_r fmt (var_name, value)
247

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

    
293
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
294
  fprintf
295
    fmt
296
    "%s_pack%a(@[<hov>%a,@ %a@])"
297
    name
298
    (pp_print_option pp_print_int)
299
    i
300
    pp_mem
301
    mem
302
    pp_self
303
    self
304

    
305
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
306
  pp_memory_pack_aux
307
    ?i:mp.mpindex
308
    pp_mem
309
    pp_self
310
    fmt
311
    (mp.mpname.node_id, mem, self)
312

    
313
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
314
    (name, vars, mem_in, mem_out) =
315
  let stateless = fst (get_stateless_status m) in
316
  fprintf
317
    fmt
318
    "%s_transition%a(@[<hov>%t%a%t@])"
319
    name
320
    (pp_print_option pp_print_int)
321
    i
322
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
323
    (pp_comma_list
324
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
325
       pp_var)
326
    vars
327
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
328

    
329
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
330
  pp_transition_aux
331
    ?i:t.tindex
332
    m
333
    pp_mem_in
334
    pp_mem_out
335
    pp_var
336
    fmt
337
    (t.tname.node_id, t.tvars, mem_in, mem_out)
338

    
339
let pp_transition_aux' ?i m =
340
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
341
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
342

    
343
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
344
  fprintf
345
    fmt
346
    "%s_reset_cleared(@[<hov>%a,@ %a@])"
347
    name
348
    pp_mem_in
349
    mem_in
350
    pp_mem_out
351
    mem_out
352

    
353
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
354

    
355
let pp_functional_update mems insts fmt mem =
356
  let rec aux fmt = function
357
    | [] ->
358
      pp_print_string fmt mem
359
    | (x, is_mem) :: fields ->
360
      fprintf
361
        fmt
362
        "{ @[<hov>%a@ \\with .%s%s = %s@] }"
363
        aux
364
        fields
365
        (if is_mem then "_reg." else "")
366
        x
367
        x
368
  in
369
  aux
370
    fmt
371
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
372
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
373

    
374
module PrintSpec = struct
375
  type mode =
376
    | MemoryPackMode
377
    | TransitionMode
378
    | TransitionFootprintMode
379
    | ResetIn
380
    | ResetOut
381
    | InstrMode of ident
382

    
383
  let pp_reg mem fmt = function
384
    | ResetFlag ->
385
      fprintf fmt "%s.%s" mem reset_flag_name
386
    | StateVar x ->
387
      fprintf fmt "%s.%a" mem pp_var_decl x
388

    
389
  let pp_expr :
390
      type a.
391
      ?test_output:bool ->
392
      machine_t ->
393
      ident ->
394
      formatter ->
395
      (value_t, a) expression_t ->
396
      unit =
397
   fun ?(test_output = false) m mem fmt -> function
398
    | Val v ->
399
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
400
    | Tag t ->
401
      pp_print_string fmt t
402
    | Var v ->
403
      pp_var_decl fmt v
404
    | Memory r ->
405
      pp_reg mem fmt r
406

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

    
466
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
467

    
468
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
469
    | Val v ->
470
      v
471
    | Tag t ->
472
      id_to_tag t
473
    | Var v ->
474
      vdecl_to_val v
475
    | Memory (StateVar v) ->
476
      vdecl_to_val v
477
    | Memory ResetFlag ->
478
      vdecl_to_val reset_flag
479

    
480
  let find_arrow m =
481
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
482
    with Not_found ->
483
      eprintf "Internal error: arrow not found";
484
      raise Not_found
485

    
486
  let pp_spec mode m =
487
    let rec pp_spec mode fmt f =
488
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
489
        let self = mk_self m in
490
        let mem = mk_mem m in
491
        let mem_in = mk_mem_in m in
492
        let mem_out = mk_mem_out m in
493
        let mem_reset = mk_mem_reset m in
494
        match mode with
495
        | MemoryPackMode ->
496
          self, self, true, mem, mem, false
497
        | TransitionMode ->
498
          mem_in, mem_in, false, mem_out, mem_out, false
499
        | TransitionFootprintMode ->
500
          mem_in, mem_in, false, mem_out, mem_out, false
501
        | ResetIn ->
502
          mem_reset, mem_reset, false, mem_out, mem_out, false
503
        | ResetOut ->
504
          mem_in, mem_in, false, mem_reset, mem_reset, false
505
        | InstrMode self ->
506
          let mem = "*" ^ mem in
507
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
508
          self, flush_str_formatter (), false, mem, mem, false
509
      in
510
      let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
511
       fun fmt e -> pp_expr m mem_out fmt e
512
      in
513
      let pp_spec' = pp_spec mode in
514
      match f with
515
      | True ->
516
        pp_true fmt ()
517
      | False ->
518
        pp_false fmt ()
519
      | Equal (a, b) ->
520
        pp_assign_spec
521
          m
522
          mem_out
523
          (pp_c_var_read ~test_output:false m)
524
          indirect_l
525
          mem_in
526
          (pp_c_var_read ~test_output:false m)
527
          indirect_r
528
          fmt
529
          (type_of_l_value a, val_of_expr a, val_of_expr b)
530
      | And fs ->
531
        pp_and_l pp_spec' fmt fs
532
      | Or fs ->
533
        pp_or_l pp_spec' fmt fs
534
      | Imply (a, b) ->
535
        pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
536
      | Exists (xs, a) ->
537
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
538
      | Forall (xs, a) ->
539
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
540
      | Ternary (e, a, b) ->
541
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
542
      | Predicate p ->
543
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
544
      | StateVarPack ResetFlag ->
545
        let r = vdecl_to_val reset_flag in
546
        pp_assign_spec
547
          m
548
          mem_out
549
          (pp_c_var_read ~test_output:false m)
550
          indirect_l
551
          mem_in
552
          (pp_c_var_read ~test_output:false m)
553
          indirect_r
554
          fmt
555
          (Type_predef.type_bool, r, r)
556
      | StateVarPack (StateVar v) ->
557
        let v' = vdecl_to_val v in
558
        let inst = find_arrow m in
559
        pp_paren
560
          (pp_implies
561
             (pp_not (pp_initialization pp_access'))
562
             (pp_assign_spec
563
                m
564
                mem_out
565
                (pp_c_var_read ~test_output:false m)
566
                indirect_l
567
                mem_in
568
                (pp_c_var_read ~test_output:false m)
569
                indirect_r))
570
          fmt
571
          ((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
572
      | ExistsMem (f, rc, tr) ->
573
        pp_exists
574
          (pp_machine_decl' ~ghost:true)
575
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
576
          fmt
577
          ((f, mk_mem_reset m), (rc, tr))
578
    in
579
    pp_spec mode
580
end
581

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

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

    
588
let pp_mem_valid_def fmt m =
589
  if not (fst (get_stateless_status m)) then
590
    let name = m.mname.node_id in
591
    let self = mk_self m in
592
    pp_acsl
593
      (pp_predicate
594
         (pp_mem_valid (pp_machine_decl pp_ptr))
595
         (pp_and
596
            (pp_and_l (fun fmt (inst, (td, _)) ->
597
                 if Arrow.td_is_arrow td then
598
                   pp_valid pp_indirect' fmt [ self, inst ]
599
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
600
            (pp_valid pp_print_string)))
601
      fmt
602
      ((name, (name, self)), (m.minstances, [ self ]))
603

    
604
let pp_memory_pack_def m fmt mp =
605
  let name = mp.mpname.node_id in
606
  let self = mk_self m in
607
  let mem = mk_mem m in
608
  pp_acsl
609
    (pp_predicate
610
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
611
       (PrintSpec.pp_spec MemoryPackMode m))
612
    fmt
613
    ((mp, (name, mem), (name, self)), mp.mpformula)
614

    
615
let pp_machine_ghost_struct fmt m =
616
  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
617

    
618
let pp_memory_pack_defs fmt m =
619
  if not (fst (get_stateless_status m)) then
620
    fprintf
621
      fmt
622
      "%a@,%a"
623
      pp_machine_ghost_struct
624
      m
625
      (pp_print_list
626
         ~pp_epilogue:pp_print_cut
627
         ~pp_open_box:pp_open_vbox0
628
         (pp_memory_pack_def m))
629
      m.mspec.mmemory_packs
630

    
631
let pp_transition_def m fmt t =
632
  let name = t.tname.node_id in
633
  let mem_in = mk_mem_in m in
634
  let mem_out = mk_mem_out m in
635
  pp_acsl
636
    (pp_predicate
637
       (pp_transition
638
          m
639
          (pp_machine_decl' ~ghost:true)
640
          (pp_machine_decl' ~ghost:true)
641
          (pp_local m))
642
       (PrintSpec.pp_spec TransitionMode m))
643
    fmt
644
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
645

    
646
let pp_transition_defs fmt m =
647
  pp_print_list
648
    ~pp_epilogue:pp_print_cut
649
    ~pp_open_box:pp_open_vbox0
650
    (pp_transition_def m)
651
    fmt
652
    m.mspec.mtransitions
653

    
654
let pp_transition_footprint fmt t =
655
  fprintf
656
    fmt
657
    "%s_transition%a_footprint"
658
    t.tname.node_id
659
    (pp_print_option pp_print_int)
660
    t.tindex
661

    
662
let pp_transition_footprint_lemma m fmt t =
663
  let name = t.tname.node_id in
664
  let mem_in = mk_mem_in m in
665
  let mem_out = mk_mem_out m in
666
  let mems =
667
    ISet.(
668
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
669
  in
670
  let insts =
671
    IMap.(
672
      diff
673
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
674
        t.tinst_footprint)
675
  in
676
  let memories =
677
    List.map
678
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
679
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
680
  in
681
  let mems_empty = ISet.is_empty mems in
682
  let insts_empty = IMap.is_empty insts in
683
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
684
  let tr ?mems ?insts () =
685
    Spec_common.mk_transition
686
      ?mems
687
      ?insts
688
      ?i:t.tindex
689
      name
690
      (vdecls_to_vals t.tvars)
691
  in
692
  if not (mems_empty && insts_empty) then
693
    pp_acsl
694
      (pp_lemma
695
         pp_transition_footprint
696
         (pp_forall
697
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
698
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
699
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
700
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
701
                else pp_forall (pp_locals m))
702
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
703
      fmt
704
      ( t,
705
        ( (m.mname.node_id, [ mem_in; mem_out ]),
706
          ( instances,
707
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
708
      )
709

    
710
let pp_transition_footprint_lemmas fmt m =
711
  pp_print_list
712
    ~pp_epilogue:pp_print_cut
713
    ~pp_open_box:pp_open_vbox0
714
    (pp_transition_footprint_lemma m)
715
    fmt
716
    (List.filter
717
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
718
       m.mspec.mtransitions)
719

    
720
let pp_initialization_def fmt m =
721
  if not (fst (get_stateless_status m)) then
722
    let name = m.mname.node_id in
723
    let mem_in = mk_mem_in m in
724
    pp_acsl
725
      (pp_predicate
726
         (pp_initialization (pp_machine_decl' ~ghost:true))
727
         (pp_and_l (fun fmt (i, (td, _)) ->
728
              if Arrow.td_is_arrow td then
729
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
730
              else
731
                pp_equal
732
                  (pp_reset_flag ~indirect:false pp_access')
733
                  pp_print_int
734
                  fmt
735
                  ((mem_in, i), 1))))
736
      fmt
737
      ((name, (name, mem_in)), m.minstances)
738

    
739
let pp_reset_cleared_def fmt m =
740
  if not (fst (get_stateless_status m)) then
741
    let name = m.mname.node_id in
742
    let mem_in = mk_mem_in m in
743
    let mem_out = mk_mem_out m in
744
    pp_acsl
745
      (pp_predicate
746
         (pp_reset_cleared
747
            (pp_machine_decl' ~ghost:true)
748
            (pp_machine_decl' ~ghost:true))
749
         (pp_ite
750
            (pp_reset_flag' ~indirect:false)
751
            (pp_and
752
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
753
               pp_initialization')
754
            (pp_equal pp_print_string pp_print_string)))
755
      fmt
756
      ( (name, (name, mem_in), (name, mem_out)),
757
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
758

    
759
let pp_register_chain ?(indirect = true) ptr =
760
  pp_print_list
761
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
762
    ~pp_epilogue:(fun fmt () ->
763
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
764
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
765
    (fun fmt (i, _) -> pp_print_string fmt i)
766

    
767
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
768
  pp_print_list
769
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
770
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
771
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
772
    (fun fmt (i, _) -> pp_print_string fmt i)
773
    fmt
774
    mems
775

    
776
let pp_arrow_reset_ghost mem fmt inst =
777
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
778

    
779
module GhostProto : MODIFIERS_GHOST_PROTO = struct
780
  let pp_ghost_parameters ?(cut = true) fmt vs =
781
    fprintf
782
      fmt
783
      "%a%a"
784
      (if cut then pp_print_cut else pp_print_nothing)
785
      ()
786
      (pp_acsl_line'
787
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
788
      vs
789
end
790

    
791
module HdrMod = struct
792
  module GhostProto = GhostProto
793

    
794
  let pp_machine_decl_prefix _ _ = ()
795

    
796
  let pp_import_arrow fmt () =
797
    fprintf
798
      fmt
799
      "#include \"%s/arrow_spec.h%s\""
800
      (Arrow.arrow_top_decl ()).top_decl_owner
801
      (if !Options.cpp then "pp" else "")
802

    
803
  let pp_predicates fmt machines =
804
    let pp_preds comment pp =
805
      pp_print_list
806
        ~pp_open_box:pp_open_vbox0
807
        ~pp_prologue:(pp_print_endcut comment)
808
        pp
809
        ~pp_epilogue:pp_print_cutcut
810
    in
811
    fprintf
812
      fmt
813
      "%a%a"
814
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
815
      machines
816
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
817
      machines
818

    
819
  let pp_machine_alloc_decl fmt m =
820
    pp_machine_decl_prefix fmt m;
821
    if not (fst (get_stateless_status m)) then
822
      if !Options.static_mem then
823
        (* Static allocation *)
824
        let macro = m, mk_attribute m, mk_instance m in
825
        fprintf
826
          fmt
827
          "%a@,%a@,%a"
828
          (pp_static_declare_macro ~ghost:true)
829
          macro
830
          (pp_static_link_macro ~ghost:true)
831
          macro
832
          (pp_static_alloc_macro ~ghost:true)
833
          macro
834
      else
835
        (* Dynamic allocation *)
836
        (* TODO: handle dynamic alloc *)
837
        assert false
838
  (* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
839
   *   (m.mname.node_id, m.mstatic)
840
   *   pp_dealloc_prototype m.mname.node_id *)
841
end
842

    
843
module SrcMod = struct
844
  module GhostProto = GhostProto
845

    
846
  let pp_predicates fmt machines =
847
    let pp_preds comment pp =
848
      pp_print_list
849
        ~pp_open_box:pp_open_vbox0
850
        ~pp_prologue:(pp_print_endcut comment)
851
        pp
852
        ~pp_epilogue:pp_print_cutcut
853
    in
854
    fprintf
855
      fmt
856
      "%a%a%a%a%a%a"
857
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
858
      machines
859
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
860
      machines
861
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
862
      machines
863
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
864
      machines
865
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
866
      machines
867
      (pp_preds
868
         "/* ACSL transition memory footprints lemmas */"
869
         pp_transition_footprint_lemmas)
870
      machines
871

    
872
  let pp_clear_reset_spec fmt self mem m =
873
    let name = m.mname.node_id in
874
    let arws, narws =
875
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
876
    in
877
    let mk_insts = List.map (fun x -> [ x ]) in
878
    pp_acsl_cut
879
      (fun fmt () ->
880
        fprintf
881
          fmt
882
          "%a@,\
883
           %a@,\
884
           %a@,\
885
           %a@,\
886
           %a@,\
887
           %a@,\
888
           %a@,\
889
           %a@,\
890
           %a@,\
891
           %a@,\
892
           @[<v 2>behavior reset:@;\
893
           %a@,\
894
           %a@]@,\
895
           @[<v 2>behavior no_reset:@;\
896
           %a@,\
897
           %a@]@,\
898
           complete behaviors;@,\
899
           disjoint behaviors;"
900
          (pp_requires pp_mem_valid')
901
          (name, self)
902
          (pp_requires (pp_separated' self mem))
903
          (mk_insts m.minstances, [])
904
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
905
          (name, mem, self)
906
          (pp_ensures
907
             (pp_memory_pack_aux
908
                ~i:(List.length m.mspec.mmemory_packs - 2)
909
                pp_ptr
910
                pp_print_string))
911
          (name, mem, self)
912
          (pp_assigns pp_reset_flag')
913
          [ self ]
914
          (pp_assigns (pp_register_chain self))
915
          (mk_insts arws)
916
          (pp_assigns (pp_reset_flag_chain self))
917
          (mk_insts narws)
918
          (pp_assigns pp_reset_flag')
919
          [ mem ]
920
          (pp_assigns (pp_register_chain ~indirect:false mem))
921
          (mk_insts arws)
922
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
923
          (mk_insts narws)
924
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
925
          (mem, 1)
926
          (pp_ensures (pp_initialization pp_ptr))
927
          (name, mem)
928
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
929
          (mem, 0)
930
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
931
          (mem, mem))
932
      fmt
933
      ()
934

    
935
  let pp_set_reset_spec fmt self mem m =
936
    let name = m.mname.node_id in
937
    pp_acsl_cut
938
      (fun fmt () ->
939
        fprintf
940
          fmt
941
          "%a@,%a@,%a"
942
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
943
          (name, mem, self)
944
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
945
          (mem, 1)
946
          (pp_assigns pp_reset_flag')
947
          [ self; mem ])
948
      fmt
949
      ()
950

    
951
  let pp_step_spec fmt machines self mem m =
952
    let name = m.mname.node_id in
953
    let insts = instances machines m in
954
    let insts' = powerset_instances insts in
955
    let insts'' =
956
      List.(
957
        filter
958
          (fun l -> l <> [])
959
          (map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
960
    in
961
    let inputs = m.mstep.step_inputs in
962
    let outputs = m.mstep.step_outputs in
963
    pp_acsl_cut
964
      (fun fmt () ->
965
        if fst (get_stateless_status m) then
966
          fprintf
967
            fmt
968
            "%a@,%a@,%a@,%a"
969
            (pp_requires (pp_valid pp_var_decl))
970
            outputs
971
            (pp_requires pp_separated'')
972
            outputs
973
            (pp_assigns pp_ptr_decl)
974
            outputs
975
            (pp_ensures (pp_transition_aux' m))
976
            (name, inputs @ outputs, "", "")
977
        else
978
          fprintf
979
            fmt
980
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
981
            (pp_requires (pp_valid pp_var_decl))
982
            outputs
983
            (pp_requires pp_mem_valid')
984
            (name, self)
985
            (pp_requires (pp_separated' self mem))
986
            (insts', outputs)
987
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
988
            (name, mem, self)
989
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
990
            (name, mem, self)
991
            (pp_ensures
992
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
993
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
994
            (name, inputs @ outputs, mem, mem)
995
            (pp_assigns pp_ptr_decl)
996
            outputs
997
            (pp_assigns (pp_reg self))
998
            m.mmemory
999
            (pp_assigns pp_reset_flag')
1000
            [ self ]
1001
            (pp_assigns (pp_memory self))
1002
            (memories insts')
1003
            (pp_assigns (pp_register_chain self))
1004
            insts
1005
            (pp_assigns (pp_reset_flag_chain self))
1006
            insts''
1007
            (pp_assigns (pp_reg mem))
1008
            m.mmemory
1009
            (pp_assigns pp_reset_flag')
1010
            [ mem ]
1011
            (pp_assigns (pp_memory ~indirect:false mem))
1012
            (memories insts')
1013
            (pp_assigns (pp_register_chain ~indirect:false mem))
1014
            insts
1015
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1016
            insts'')
1017
      fmt
1018
      ()
1019

    
1020
  let pp_ghost_instr_code m self fmt instr =
1021
    match instr.instr_desc with
1022
    | MStateAssign (x, v) ->
1023
      fprintf
1024
        fmt
1025
        "@,%a"
1026
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
1027
        (x, v)
1028
    | MResetAssign b ->
1029
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
1030
    | MSetReset inst ->
1031
      let td, _ = List.assoc inst m.minstances in
1032
      if Arrow.td_is_arrow td then
1033
        fprintf
1034
          fmt
1035
          "@,%a;"
1036
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
1037
          inst
1038
    | _ ->
1039
      ()
1040

    
1041
  let pp_step_instr_spec m self mem fmt instr =
1042
    fprintf
1043
      fmt
1044
      "%a%a"
1045
      (pp_ghost_instr_code m mem)
1046
      instr
1047
      (pp_print_list
1048
         ~pp_open_box:pp_open_vbox0
1049
         ~pp_prologue:pp_print_cut
1050
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
1051
      instr.instr_spec
1052

    
1053
  let pp_ghost_parameter mem fmt inst =
1054
    GhostProto.pp_ghost_parameters
1055
      ~cut:false
1056
      fmt
1057
      (match inst with
1058
      | Some inst ->
1059
        [ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
1060
      | None ->
1061
        [ mem, pp_print_string ])
1062
end
1063

    
1064
module MainMod = struct
1065
  let main_mem_ghost = "main_mem_ghost"
1066

    
1067
  let pp_declare_ghost_state fmt name =
1068
    pp_acsl_line'_cut
1069
      (pp_ghost (fun fmt () ->
1070
           fprintf
1071
             fmt
1072
             "%a(,%s);"
1073
             (pp_machine_static_alloc_name ~ghost:true)
1074
             name
1075
             main_mem_ghost))
1076
      fmt
1077
      ()
1078

    
1079
  let pp_ghost_state_parameter fmt () =
1080
    GhostProto.pp_ghost_parameters
1081
      ~cut:false
1082
      fmt
1083
      [ main_mem_ghost, pp_ref pp_print_string ]
1084

    
1085
  let pp_main_loop_invariants main_mem machines fmt m =
1086
    let name = m.mname.node_id in
1087
    let insts = powerset_instances (instances machines m) in
1088
    pp_acsl_cut
1089
      (fun fmt () ->
1090
        fprintf
1091
          fmt
1092
          "%a@,%a@,%a@,%a"
1093
          (pp_loop_invariant pp_mem_valid')
1094
          (name, main_mem)
1095
          (pp_loop_invariant
1096
             (pp_memory_pack_aux pp_print_string pp_print_string))
1097
          (name, main_mem_ghost, main_mem)
1098
          (pp_loop_invariant
1099
             (pp_separated
1100
                (pp_paren pp_print_string)
1101
                pp_ref'
1102
                (pp_ref pp_var_decl)))
1103
          (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
1104
          (pp_loop_invariant
1105
             (pp_or
1106
                (pp_valid_read pp_stdout)
1107
                (pp_equal pp_stdout pp_null)))
1108
          ((), ((), ())))
1109
      fmt
1110
      ()
1111

    
1112
  let pp_main_spec fmt =
1113
    pp_acsl_cut
1114
      (fun fmt () ->
1115
        fprintf
1116
          fmt
1117
          "%a@,%a@,%a@,%a"
1118
          (pp_requires
1119
             (pp_or
1120
                (pp_valid_read pp_stdout)
1121
                (pp_equal pp_stdout pp_null)))
1122
          ((), ((), ()))
1123
          (pp_terminates pp_false)
1124
          ()
1125
          (pp_ensures pp_false)
1126
          ()
1127
          (pp_assigns pp_nothing)
1128
          [ () ])
1129
      fmt
1130
      ()
1131
end
1132

    
1133
(**************************************************************************)
1134
(*                              MAKEFILE                                  *)
1135
(**************************************************************************)
1136

    
1137
module MakefileMod = struct
1138
  let other_targets fmt basename _nodename dependencies =
1139
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1140
    (* EACSL version of library file . c *)
1141
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1142
    fprintf
1143
      fmt
1144
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1145
       e-acsl -print -ocode %s_eacsl.c@."
1146
      basename
1147
      basename;
1148
    fprintf fmt "@.";
1149
    fprintf fmt "@.";
1150

    
1151
    (* EACSL version of library file . c + main .c *)
1152
    fprintf
1153
      fmt
1154
      "%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1155
      basename
1156
      basename
1157
      basename
1158
      basename;
1159
    fprintf
1160
      fmt
1161
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1162
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
1163
      basename
1164
      basename
1165
      basename;
1166
    (* Ugly hack to deal with eacsl bugs *)
1167
    fprintf
1168
      fmt
1169
      "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1170
      basename
1171
      basename;
1172
    fprintf fmt "@.";
1173
    fprintf fmt "@.";
1174

    
1175
    (* EACSL version of binary *)
1176
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1177
    fprintf
1178
      fmt
1179
      "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1180
      basename;
1181
    (* compiling instrumented lib + main *)
1182
    C_backend_makefile.fprintf_dependencies fmt dependencies;
1183
    fprintf
1184
      fmt
1185
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1186
       %s_main_eacsl.o %a@."
1187
      basename
1188
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1189
      (C_backend_makefile.compiled_dependencies dependencies)
1190
      ("${FRAMACEACSL}/e_acsl.c "
1191
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1192
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1193
      basename
1194
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1195
      (C_backend_makefile.lib_dependencies dependencies);
1196
    fprintf fmt "@."
1197
end
1198

    
1199
(* Local Variables: *)
1200
(* compile-command:"make -C ../../.." *)
1201
(* End: *)
(15-15/18)