Project

General

Profile

Download (31.2 KB) Statistics
| Branch: | Tag: | Revision:
1

    
2
(********************************************************************)
3
(*                                                                  *)
4
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
5
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
6
(*                                                                  *)
7
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
8
(*  under the terms of the GNU Lesser General Public License        *)
9
(*  version 2.1.                                                    *)
10
(*                                                                  *)
11
(********************************************************************)
12

    
13
open Utils.Format
14
open Lustre_types
15
open Machine_code_types
16
open C_backend_common
17
open Corelang
18
open Spec_types
19
open Machine_code_common
20

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

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

    
26
(* TODO ACSL
27
   Return updates machines (eg with local annotations) and acsl preamble *)
28
let preprocess_acsl machines = machines, []
29
                          
30
let pp_acsl_basic_type_desc t_desc =
31
  if Types.is_bool_type t_desc then
32
    (* if !Options.cpp then "bool" else "_Bool" *)
33
    "_Bool"
34
  else if Types.is_int_type t_desc then
35
    (* !Options.int_type *)
36
    if t_desc.tid = -1 then "int" else "integer"
37
  else if Types.is_real_type t_desc then
38
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
39
  else
40
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
41

    
42
let pp_acsl pp fmt =
43
  fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
44

    
45
let pp_acsl_cut pp fmt =
46
  fprintf fmt "%a@," (pp_acsl pp)
47

    
48
let pp_acsl_line pp fmt =
49
  fprintf fmt "//%@ @[<h>%a@]" pp
50

    
51
let pp_acsl_line' pp fmt =
52
  fprintf fmt "/*%@ @[<h>%a@] */" pp
53

    
54
let pp_acsl_line_cut pp fmt =
55
  fprintf fmt "%a@," (pp_acsl_line pp)
56

    
57
let pp_requires pp_req fmt =
58
  fprintf fmt "requires %a;" pp_req
59

    
60
let pp_ensures pp_ens fmt =
61
  fprintf fmt "ensures %a;" pp_ens
62

    
63
let pp_assumes pp_asm fmt =
64
  fprintf fmt "assumes %a;" pp_asm
65

    
66
let pp_assigns pp =
67
  pp_comma_list
68
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
69
    ~pp_epilogue:pp_print_semicolon'
70
    pp
71

    
72
let pp_ghost pp_gho fmt =
73
  fprintf fmt "ghost %a" pp_gho
74

    
75
let pp_assert pp_ast fmt =
76
  fprintf fmt "assert %a;" pp_ast
77

    
78
let pp_mem_valid pp_var fmt (name, var) =
79
  fprintf fmt "%s_valid(%a)" name pp_var var
80

    
81
let pp_mem_valid' = pp_mem_valid 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 =
94
  pp_print_string fmt v.var_id
95

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

    
99
let pp_true fmt () =
100
  pp_print_string fmt "\\true"
101

    
102
let pp_false fmt () =
103
  pp_print_string fmt "\\false"
104

    
105
let pp_at pp_v fmt (v, l) =
106
  fprintf fmt "\\at(%a, %s)" pp_v v l
107

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

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

    
130
let pp_instance ?(indirect=true) ptr =
131
  pp_print_list
132
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
133
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
134
    (fun fmt (i, _) -> pp_print_string fmt i)
135

    
136
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
137
  pp_access
138
    ((if indirect then pp_indirect else pp_access)
139
       (pp_instance ~indirect ptr) pp_print_string)
140
    pp_var_decl
141
    fmt ((path, "_reg"), mem)
142

    
143
let prefixes l =
144
  let rec pref acc = function
145
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
146
    | [] -> acc
147
  in
148
  pref [] (List.rev l)
149

    
150
let powerset_instances paths =
151
  List.map prefixes paths |> List.flatten
152

    
153
let pp_separated self mem fmt (paths, ptrs) =
154
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
155
    self
156
    mem
157
    (pp_comma_list
158
       ~pp_prologue:pp_print_comma'
159
       (pp_instance self))
160
    paths
161
    (pp_comma_list
162
       ~pp_prologue:pp_print_comma'
163
       pp_var_decl)
164
    ptrs
165

    
166
let pp_separated' =
167
  pp_comma_list
168
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
169
    ~pp_epilogue:pp_print_cpar
170
    pp_var_decl
171

    
172
let pp_par pp fmt =
173
  fprintf fmt "(%a)" pp
174

    
175
let pp_forall pp_l pp_r fmt (l, r) =
176
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
177
    pp_l l
178
    pp_r r
179

    
180
let pp_exists pp_l pp_r fmt (l, r) =
181
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
182
    pp_l l
183
    pp_r r
184

    
185
let pp_equal pp_l pp_r fmt (l, r) =
186
  fprintf fmt "%a == %a"
187
    pp_l l
188
    pp_r r
189

    
190
let pp_different pp_l pp_r fmt (l, r) =
191
  fprintf fmt "%a != %a"
192
    pp_l l
193
    pp_r r
194

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

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

    
205
let pp_and_l pp_v fmt =
206
  pp_print_list
207
    ~pp_open_box:pp_open_vbox0
208
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
209
    pp_v
210
    fmt
211

    
212
let pp_or pp_l pp_r fmt (l, r) =
213
  fprintf fmt "@[<v>%a @ || %a@]"
214
    pp_l l
215
    pp_r r
216

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

    
224
let pp_not pp fmt =
225
  fprintf fmt "!%a" pp
226

    
227
let pp_valid pp =
228
  pp_and_l
229
  (* pp_print_list *)
230
    (* ~pp_sep:pp_print_cut *)
231
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
232

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

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

    
242
let pp_paren pp fmt v =
243
  fprintf fmt "(%a)" pp v
244

    
245
let pp_initialization pp_mem fmt (name, mem) =
246
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
247

    
248
let pp_initialization' = pp_initialization pp_print_string
249

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

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

    
258
let pp_ptr_decl fmt v =
259
  pp_ptr fmt v.var_id
260

    
261
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
262
  if Types.is_real_type typ && !Options.mpfr
263
  then
264
    assert false
265
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
266
  else
267
    pp_equal pp_l pp_r fmt (var_name, value)
268

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

    
300
let pp_nothing fmt () =
301
  pp_print_string fmt "\\nothing"
302

    
303
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
304
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])"
305
    name
306
    (pp_print_option pp_print_int) i
307
    pp_mem mem
308
    pp_self self
309

    
310
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
311
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
312
    (mp.mpname.node_id, mem, self)
313

    
314
let pp_memory_pack_aux' ?i fmt =
315
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
316
let pp_memory_pack' fmt =
317
  pp_memory_pack pp_print_string pp_print_string fmt
318

    
319
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
320
    (name, inputs, locals, outputs, mem_in, mem_out) =
321
  let stateless = fst (get_stateless_status m) in
322
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
323
    name
324
    (pp_print_option pp_print_int) i
325
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
326
    (pp_comma_list
327
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
328
       pp_input) inputs
329
    (pp_print_option (fun fmt _ ->
330
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
331
    i
332
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
333
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs
334

    
335
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
336
    (t, mem_in, mem_out) =
337
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
338
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
339

    
340
let pp_transition_aux' ?i m =
341
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
342
let pp_transition_aux'' ?i m =
343
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
344
let pp_transition' m =
345
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
346
let pp_transition'' m =
347
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
348

    
349
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
350
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])"
351
    name
352
    pp_mem_in mem_in
353
    pp_mem_out mem_out
354

    
355
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
356

    
357
let pp_functional_update mems fmt mem =
358
  let rec aux fmt mems =
359
    match mems with
360
    | [] -> pp_print_string fmt mem
361
    | x :: mems ->
362
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
363
  in
364
  aux fmt
365
  (* if Utils.ISet.is_empty mems then
366
   *   pp_print_string fmt mem
367
   *     else
368
   *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
369
   *     mem
370
   *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
371
   *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
372
      (Utils.ISet.elements mems)
373

    
374
module PrintSpec = struct
375

    
376
  type mode =
377
    | MemoryPackMode
378
    | TransitionMode
379
    | TransitionFootprintMode
380
    | ResetIn
381
    | ResetOut
382
    | InstrMode of ident
383

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

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

    
399
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
400
    let output, mem_update = match mode with
401
      | InstrMode _ -> true, false
402
      | TransitionFootprintMode -> false, true
403
      | _ -> false, false
404
    in
405
    let pp_expr:
406
      type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
407
      fun ?output fmt e -> pp_expr ?output m mem_out fmt e
408
    in
409
    match p with
410
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
411
      let pp_mem_in, pp_mem_out = match inst with
412
        | None ->
413
          pp_print_string,
414
          if mem_update then pp_functional_update mems else pp_print_string
415
        | Some inst ->
416
          (fun fmt mem_in ->
417
             if r then pp_print_string fmt mem_in
418
             else pp_access' fmt (mem_in, inst)),
419
          (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
420
      in
421
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output)
422
        fmt
423
        (f, inputs, locals, outputs, mem_in', mem_out')
424
    | Reset (_f, inst, r) ->
425
      pp_ite
426
        (pp_c_val m mem_in (pp_c_var_read m))
427
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
428
        (pp_equal pp_print_string pp_access')
429
        fmt
430
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
431
    | MemoryPack (f, inst, i) ->
432
      let pp_mem, pp_self = match inst with
433
        | None ->
434
          pp_print_string, pp_print_string
435
        | Some inst ->
436
          (fun fmt mem -> pp_access' fmt (mem, inst)),
437
          (fun fmt self -> pp_indirect' fmt (self, inst))
438
      in
439
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
440
    | ResetCleared f ->
441
      pp_reset_cleared' fmt (f, mem_in, mem_out)
442
      (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
443
    | Initialization -> ()
444

    
445
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
446

    
447
  let val_of_expr: type a. (value_t, a) expression_t -> value_t = function
448
    | Val v -> v
449
    | Tag t -> id_to_tag t
450
    | Var v -> vdecl_to_val v
451
    | Memory (StateVar v) -> vdecl_to_val v
452
    | Memory ResetFlag -> vdecl_to_val reset_flag
453

    
454
  let find_arrow m =
455
    try
456
      List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
457
      |> fst
458
    with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
459

    
460
  let pp_spec mode m fmt f =
461
    let rec pp_spec mode fmt f =
462
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
463
        let self = mk_self m in
464
        let mem = mk_mem m in
465
        let mem_in = mk_mem_in m in
466
        let mem_out = mk_mem_out m in
467
        let mem_reset = mk_mem_reset m in
468
        match mode with
469
        | MemoryPackMode ->
470
          self, self, true, mem, mem, false
471
        | TransitionMode ->
472
          mem_in, mem_in, false, mem_out, mem_out, false
473
        | TransitionFootprintMode ->
474
          mem_in, mem_in, false, mem_out, mem_out, false
475
        | ResetIn ->
476
          mem_reset, mem_reset, false, mem_out, mem_out, false
477
        | ResetOut ->
478
          mem_in, mem_in, false, mem_reset, mem_reset, false
479
        | InstrMode self ->
480
          let mem = "*" ^ mem in
481
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
482
          self, flush_str_formatter (), false,
483
          mem, mem, false
484
      in
485
      let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
486
        fun fmt e -> pp_expr m mem_out fmt e
487
      in
488
      let pp_spec' = pp_spec mode in
489
      match f with
490
      | True ->
491
        pp_true fmt ()
492
      | False ->
493
        pp_false fmt ()
494
      | Equal (a, b) ->
495
        pp_assign_spec m
496
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
497
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
498
          fmt
499
          (type_of_l_value a, val_of_expr a, val_of_expr b)
500
      | And fs ->
501
        pp_and_l pp_spec' fmt fs
502
      | Or fs ->
503
        pp_or_l pp_spec' fmt fs
504
      | Imply (a, b) ->
505
        pp_par (pp_implies pp_spec' pp_spec') fmt (a, b)
506
      | Exists (xs, a) ->
507
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
508
      | Forall (xs, a) ->
509
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
510
      | Ternary (e, a, b) ->
511
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
512
      | Predicate p ->
513
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
514
      | StateVarPack ResetFlag ->
515
        let r = vdecl_to_val reset_flag in
516
        pp_assign_spec m
517
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
518
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
519
          fmt
520
          (Type_predef.type_bool, r, r)
521
      | StateVarPack (StateVar v) ->
522
        let v' = vdecl_to_val v in
523
        let inst = find_arrow m in
524
        pp_par (pp_implies
525
                  (pp_not (pp_initialization pp_access'))
526
                  (pp_assign_spec m
527
                     mem_out (pp_c_var_read ~test_output:false m) indirect_l
528
                     mem_in (pp_c_var_read ~test_output:false m) indirect_r))
529
          fmt
530
          ((Arrow.arrow_id, (mem_out, inst)),
531
           (v.var_type, v', v'))
532
      | ExistsMem (f, rc, tr) ->
533
        pp_exists
534
          (pp_machine_decl' ~ghost:true)
535
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
536
          fmt
537
          ((f, mk_mem_reset m),
538
           (rc, tr))
539
    in
540
    match mode with
541
    | TransitionFootprintMode ->
542
      let mem_in = mk_mem_in m in
543
      let mem_out = mk_mem_out m in
544
      pp_forall
545
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
546
        (pp_spec mode)
547
        fmt ((m.mname.node_id, [mem_in; mem_out]), f)
548
    | _ ->
549
      pp_spec mode fmt f
550

    
551
end
552

    
553
let pp_predicate pp_l pp_r fmt (l, r) =
554
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
555
    pp_l l
556
    pp_r r
557

    
558
let pp_lemma pp_l pp_r fmt (l, r) =
559
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]"
560
    pp_l l
561
    pp_r r
562

    
563
let pp_mem_valid_def fmt m =
564
  if not (fst (get_stateless_status m)) then
565
    let name = m.mname.node_id in
566
    let self = mk_self m in
567
    pp_acsl
568
      (pp_predicate
569
         (pp_mem_valid (pp_machine_decl pp_ptr))
570
         (pp_and
571
            (pp_and_l (fun fmt (inst, (td, _)) ->
572
                 if Arrow.td_is_arrow td then
573
                   pp_valid pp_indirect' fmt [self, inst]
574
                 else
575
                   pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
576
            (pp_valid pp_print_string)))
577
      fmt
578
      ((name, (name, self)),
579
       (m.minstances, [self]))
580

    
581
let pp_memory_pack_def m fmt mp =
582
  let name = mp.mpname.node_id in
583
  let self = mk_self m in
584
  let mem = mk_mem m in
585
  pp_acsl
586
    (pp_predicate
587
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
588
       (PrintSpec.pp_spec MemoryPackMode m))
589
    fmt
590
    ((mp, (name, mem), (name, self)),
591
     mp.mpformula)
592

    
593
let print_machine_ghost_struct fmt m =
594
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
595

    
596
let pp_memory_pack_defs fmt m =
597
  if not (fst (get_stateless_status m)) then
598
    fprintf fmt "%a@,%a"
599
      print_machine_ghost_struct m
600
      (pp_print_list
601
         ~pp_epilogue:pp_print_cut
602
         ~pp_open_box:pp_open_vbox0
603
         (pp_memory_pack_def m)) m.mspec.mmemory_packs
604

    
605
let pp_transition_def m fmt t =
606
  let name = t.tname.node_id in
607
  let mem_in = mk_mem_in m in
608
  let mem_out = mk_mem_out m in
609
  pp_acsl
610
    (pp_predicate
611
       (pp_transition m
612
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
613
          (pp_local m)
614
          (pp_local m))
615
       (PrintSpec.pp_spec TransitionMode m))
616
    fmt
617
    ((t, (name, mem_in), (name, mem_out)),
618
     t.tformula)
619

    
620
let pp_transition_defs fmt m =
621
  pp_print_list
622
    ~pp_epilogue:pp_print_cut
623
    ~pp_open_box:pp_open_vbox0
624
    (pp_transition_def m) fmt m.mspec.mtransitions
625

    
626
let pp_transition_footprint fmt t =
627
  fprintf fmt "%s_transition%a_footprint"
628
    t.tname.node_id
629
    (pp_print_option pp_print_int) t.tindex
630

    
631
let pp_transition_footprint_lemma m fmt t =
632
  let open Utils.ISet in
633
  let name = t.tname.node_id in
634
  let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in
635
  let memories = List.map (fun v ->
636
      { v with var_type = { v.var_type with tid = -1 }})
637
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
638
  in
639
  if not (is_empty mems) then
640
    pp_acsl
641
      (pp_lemma
642
         pp_transition_footprint
643
         (PrintSpec.pp_spec TransitionFootprintMode m))
644
      fmt
645
      (t,
646
       Forall (
647
         memories @ t.tinputs @ t.tlocals @ t.toutputs,
648
         Imply (Spec_common.mk_transition ?i:t.tindex name
649
                  (vdecls_to_vals t.tinputs)
650
                  (vdecls_to_vals t.tlocals)
651
                  (vdecls_to_vals t.toutputs),
652
                Spec_common.mk_transition ~mems ?i:t.tindex name
653
                  (vdecls_to_vals t.tinputs)
654
                  (vdecls_to_vals t.tlocals)
655
                  (vdecls_to_vals t.toutputs))))
656

    
657
let pp_transition_footprint_lemmas fmt m =
658
  pp_print_list
659
    ~pp_epilogue:pp_print_cut
660
    ~pp_open_box:pp_open_vbox0
661
    (pp_transition_footprint_lemma m) fmt
662
    (List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
663
         m.mspec.mtransitions)
664

    
665
let pp_initialization_def fmt m =
666
  if not (fst (get_stateless_status m)) then
667
    let name = m.mname.node_id in
668
    let mem_in = mk_mem_in m in
669
    pp_acsl
670
      (pp_predicate
671
         (pp_initialization (pp_machine_decl' ~ghost:true))
672
         (pp_and_l (fun fmt (i, (td, _)) ->
673
              if Arrow.td_is_arrow td then
674
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
675
              else
676
                pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int
677
                  fmt
678
                  ((mem_in, i), 1))))
679
      fmt
680
      ((name, (name, mem_in)), m.minstances)
681

    
682
let pp_reset_cleared_def fmt m =
683
  if not (fst (get_stateless_status m)) then
684
    let name = m.mname.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_reset_cleared
690
            (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true))
691
         (pp_ite
692
            (pp_reset_flag' ~indirect:false)
693
            (pp_and
694
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
695
               pp_initialization')
696
            (pp_equal pp_print_string pp_print_string)))
697
      fmt
698
      ((name, (name, mem_in), (name, mem_out)),
699
       (mem_in,
700
        ((mem_out, 0), (name, mem_out)),
701
        (mem_out, mem_in)))
702

    
703
let pp_at pp_p fmt (p, l) =
704
  fprintf fmt "\\at(%a, %s)" pp_p p l
705

    
706
let label_pre = "Pre"
707

    
708
let pp_at_pre pp_p fmt p =
709
  pp_at pp_p fmt (p, label_pre)
710

    
711
let pp_register_chain ?(indirect=true) ptr =
712
  pp_print_list
713
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
714
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
715
                     (if indirect then "->" else "."))
716
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
717
    (fun fmt (i, _) -> pp_print_string fmt i)
718

    
719
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
720
  pp_print_list
721
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
722
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
723
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
724
    (fun fmt (i, _) -> pp_print_string fmt i)
725
    fmt mems
726

    
727
let pp_arrow_reset_ghost mem fmt inst =
728
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
729

    
730
module GhostProto: MODIFIERS_GHOST_PROTO = struct
731
  let pp_ghost_parameters ?(cut=true) fmt vs =
732
    fprintf fmt "%a%a"
733
      (if cut then pp_print_cut else pp_print_nothing) ()
734
      (pp_acsl_line'
735
         (pp_ghost
736
            (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
737
      vs
738
end
739

    
740
module HdrMod = struct
741

    
742
  module GhostProto = GhostProto
743

    
744
  let print_machine_decl_prefix = fun _ _ -> ()
745

    
746
  let pp_import_arrow fmt () =
747
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
748
      (Arrow.arrow_top_decl ()).top_decl_owner
749
      (if !Options.cpp then "pp" else "")
750

    
751
end
752

    
753
module SrcMod = struct
754

    
755
  module GhostProto = GhostProto
756

    
757
  let pp_predicates (* dependencies *) fmt machines =
758
    let pp_preds comment pp =
759
      pp_print_list
760
        ~pp_open_box:pp_open_vbox0
761
        ~pp_prologue:(pp_print_endcut comment)
762
        pp
763
        ~pp_epilogue:pp_print_cutcut in
764
    fprintf fmt
765
      "%a%a%a%a%a%a"
766
      (pp_preds "/* ACSL `valid` predicates */"
767
         pp_mem_valid_def) machines
768
      (pp_preds "/* ACSL `memory pack` simulations */"
769
         pp_memory_pack_defs) machines
770
      (pp_preds "/* ACSL initialization annotations */"
771
         pp_initialization_def) machines
772
      (pp_preds "/* ACSL reset cleared annotations */"
773
         pp_reset_cleared_def) machines
774
      (pp_preds "/* ACSL transition annotations */"
775
         pp_transition_defs) machines
776
      (pp_preds "/* ACSL transition memory footprints lemmas */"
777
         pp_transition_footprint_lemmas) machines
778

    
779
  let pp_clear_reset_spec fmt self mem m =
780
    let name = m.mname.node_id in
781
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
782
        m.minstances in
783
    let mk_insts = List.map (fun x -> [x]) in
784
    pp_acsl_cut (fun fmt () ->
785
        fprintf fmt
786
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
787
          @[<v 2>behavior reset:@;\
788
          %a@,%a@]@,\
789
          @[<v 2>behavior no_reset:@;\
790
          %a@,%a@]@,\
791
          complete behaviors;@,\
792
          disjoint behaviors;"
793
          (pp_requires pp_mem_valid') (name, self)
794
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
795
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
796
          (name, mem, self)
797
          (pp_ensures (pp_memory_pack_aux
798
                         ~i:(List.length m.mspec.mmemory_packs - 2)
799
                         pp_ptr pp_print_string))
800
          (name, mem, self)
801
          (pp_assigns pp_reset_flag') [self]
802
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
803
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
804
          (pp_assigns pp_reset_flag') [mem]
805
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
806
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
807
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
808
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
809
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0)
810
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
811
      )
812
      fmt ()
813

    
814
  let pp_set_reset_spec fmt self mem m =
815
    let name = m.mname.node_id in
816
    pp_acsl_cut (fun fmt () ->
817
        fprintf fmt
818
          "%a@,%a@,%a"
819
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
820
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
821
          (pp_assigns pp_reset_flag') [self; mem])
822
      fmt ()
823

    
824
  let pp_step_spec fmt machines self mem m =
825
    let name = m.mname.node_id in
826
    let insts = instances machines m in
827
    let insts' = powerset_instances insts in
828
    let insts'' = List.(filter (fun l -> l <> [])
829
                          (map (filter (fun (_, (td, _)) ->
830
                               not (Arrow.td_is_arrow td))) insts)) in
831
    let inputs = m.mstep.step_inputs in
832
    let outputs = m.mstep.step_outputs in
833
    pp_acsl_cut (fun fmt () ->
834
        if fst (get_stateless_status m) then
835
          fprintf fmt
836
            "%a@,%a@,%a@,%a"
837
            (pp_requires (pp_valid pp_var_decl)) outputs
838
            (pp_requires pp_separated') outputs
839
            (pp_assigns pp_ptr_decl) outputs
840
            (pp_ensures (pp_transition_aux'' m))
841
            (name, inputs, [], outputs, "", "")
842
        else
843
          fprintf fmt
844
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
845
            (pp_requires (pp_valid pp_var_decl)) outputs
846
            (pp_requires pp_mem_valid') (name, self)
847
            (pp_requires (pp_separated self mem)) (insts', outputs)
848
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
849
            (name, mem, self)
850
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
851
            (name, mem, self)
852
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
853
                           pp_ptr pp_var_decl pp_ptr_decl))
854
            (name, inputs, [], outputs, mem, mem)
855
            (pp_assigns pp_ptr_decl) outputs
856
            (pp_assigns (pp_reg self)) m.mmemory
857
            (pp_assigns pp_reset_flag') [self]
858
            (pp_assigns (pp_memory self)) (memories insts')
859
            (pp_assigns (pp_register_chain self)) insts
860
            (pp_assigns (pp_reset_flag_chain self)) insts''
861
            (pp_assigns (pp_reg mem)) m.mmemory
862
            (pp_assigns pp_reset_flag') [mem]
863
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
864
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
865
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
866
      )
867
      fmt ()
868

    
869
  let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
870
    | MStateAssign (x, v) ->
871
      fprintf fmt "@,%a"
872
        (pp_acsl_line
873
           (pp_ghost
874
              (pp_assign m self (pp_c_var_read m))))
875
        (x, v)
876
    | MResetAssign b ->
877
      fprintf fmt "@,%a"
878
        (pp_acsl_line
879
           (pp_ghost
880
              (pp_reset_assign self)))
881
        b
882
    | MSetReset inst ->
883
      let td, _ = List.assoc inst m.minstances in
884
      if Arrow.td_is_arrow td then
885
         fprintf fmt "@,%a;"
886
           (pp_acsl_line
887
              (pp_ghost
888
                 (pp_arrow_reset_ghost self)))
889
           inst
890
    | _ -> ()
891

    
892
  let pp_step_instr_spec m self mem fmt instr =
893
    fprintf fmt "%a%a"
894
      (pp_ghost_instr_code m mem) instr
895
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
896
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
897
      instr.instr_spec
898

    
899
  let pp_ghost_parameter mem fmt inst =
900
    GhostProto.pp_ghost_parameters ~cut:false fmt
901
      (match inst with
902
       | Some inst ->
903
         [inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)]
904
       | None ->
905
         [mem, pp_print_string])
906

    
907
end
908

    
909
(**************************************************************************)
910
(*                              MAKEFILE                                  *)
911
(**************************************************************************)
912

    
913
module MakefileMod = struct
914

    
915
  let other_targets fmt basename _nodename dependencies =
916
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
917
    (* EACSL version of library file . c *)
918
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
919
    fprintf fmt
920
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
921
      basename basename;
922
    fprintf fmt "@.";
923
    fprintf fmt "@.";
924

    
925
    (* EACSL version of library file . c + main .c  *)
926
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
927
    fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."
928
      basename basename basename;
929
    (* Ugly hack to deal with eacsl bugs *)
930
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
931
    fprintf fmt "@.";
932
    fprintf fmt "@.";
933

    
934
    (* EACSL version of binary *)
935
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
936
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
937
    C_backend_makefile.fprintf_dependencies fmt dependencies;
938
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
939
      basename
940
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
941
      (C_backend_makefile.compiled_dependencies dependencies)
942
      ("${FRAMACEACSL}/e_acsl.c "
943
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
944
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
945
      basename
946
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
947
      (C_backend_makefile.lib_dependencies dependencies)
948
    ;
949
    fprintf fmt "@."
950

    
951
end
952

    
953
(* Local Variables: *)
954
(* compile-command:"make -C ../../.." *)
955
(* End: *)
(8-8/9)