Project

General

Profile

Download (31.5 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

    
12
open Utils.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

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

    
23
(**************************************************************************)
24

    
25
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
26
   preamble *)
27
let preprocess_acsl machines = machines, []
28

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

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

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

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

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

    
49
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp)
50

    
51
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req
52

    
53
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens
54

    
55
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm
56

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

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

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

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

    
69
let pp_mem_valid' = pp_mem_valid pp_print_string
70

    
71
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
72
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
73

    
74
let pp_indirect' = pp_indirect pp_print_string pp_print_string
75

    
76
let pp_access pp_stru pp_field fmt (stru, field) =
77
  fprintf fmt "%a.%a" pp_stru stru pp_field field
78

    
79
let pp_access' = pp_access pp_print_string pp_print_string
80

    
81
let pp_var_decl fmt v = pp_print_string fmt v.var_id
82

    
83
let pp_reg self fmt field =
84
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
85

    
86
let pp_true fmt () = pp_print_string fmt "\\true"
87

    
88
let pp_false fmt () = pp_print_string fmt "\\false"
89

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

    
92
let instances machines m =
93
  let open List in
94
  let grow paths i td mems =
95
    match paths with
96
    | [] ->
97
      [ [ i, (td, mems) ] ]
98
    | _ ->
99
      map (cons (i, (td, mems))) paths
100
  in
101
  let rec aux paths m =
102
    map
103
      (fun (i, (td, _)) ->
104
        try
105
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
106
          aux (grow paths i td m.mmemory) m
107
        with Not_found -> grow paths i td [])
108
      m.minstances
109
    |> flatten
110
  in
111
  aux [] m |> map rev
112

    
113
let memories insts =
114
  List.(
115
    map
116
      (fun path ->
117
        let _, (_, mems) = hd (rev path) in
118
        map (fun mem -> path, mem) mems)
119
      insts
120
    |> flatten)
121

    
122
let pp_instance ?(indirect = true) ptr =
123
  pp_print_list
124
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
125
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
126
    (fun fmt (i, _) -> pp_print_string fmt i)
127

    
128
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
129
  pp_access
130
    ((if indirect then pp_indirect else pp_access)
131
       (pp_instance ~indirect ptr)
132
       pp_print_string)
133
    pp_var_decl fmt
134
    ((path, "_reg"), mem)
135

    
136
let prefixes l =
137
  let rec pref acc = function
138
    | x :: l ->
139
      pref ([ x ] :: List.map (List.cons x) acc) l
140
    | [] ->
141
      acc
142
  in
143
  pref [] (List.rev l)
144

    
145
let powerset_instances paths = List.map prefixes paths |> List.flatten
146

    
147
let pp_separated self mem fmt (paths, ptrs) =
148
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" self mem
149
    (pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance self))
150
    paths
151
    (pp_comma_list ~pp_prologue:pp_print_comma' pp_var_decl)
152
    ptrs
153

    
154
let pp_separated' =
155
  pp_comma_list
156
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
157
    ~pp_epilogue:pp_print_cpar pp_var_decl
158

    
159
let pp_par pp fmt = fprintf fmt "(%a)" pp
160

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

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

    
167
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
168

    
169
let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r
170

    
171
let pp_implies pp_l pp_r fmt (l, r) =
172
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
173

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

    
176
let pp_and_l pp_v fmt =
177
  pp_print_list ~pp_open_box:pp_open_vbox0
178
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
179
    pp_v fmt
180

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

    
183
let pp_or_l pp_v fmt =
184
  pp_print_list ~pp_open_box:pp_open_vbox0
185
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
186
    pp_v fmt
187

    
188
let pp_not pp fmt = fprintf fmt "!%a" pp
189

    
190
let pp_valid pp =
191
  pp_and_l
192
    (* pp_print_list *)
193
    (* ~pp_sep:pp_print_cut *)
194
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
195

    
196
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
197

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

    
201
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
202

    
203
let pp_initialization pp_mem fmt (name, mem) =
204
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
205

    
206
let pp_initialization' = pp_initialization pp_print_string
207

    
208
let pp_local m =
209
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
210

    
211
let pp_locals m =
212
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
213

    
214
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
215

    
216
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
217
  if Types.is_real_type typ && !Options.mpfr then assert false
218
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
219
  else pp_equal pp_l pp_r fmt (var_name, value)
220

    
221
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
222
    (var_type, var_name, value) =
223
  let depth = expansion_depth value in
224
  let loop_vars = mk_loop_variables m var_type depth in
225
  let reordered_loop_vars = reorder_loop_variables loop_vars in
226
  let aux typ fmt vars =
227
    match vars with
228
    | [] ->
229
      pp_basic_assign_spec
230
        (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars
231
           pp_var_l)
232
        (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars
233
           pp_var_r)
234
        fmt typ var_name value
235
    | (_d, LVar _i) :: _q ->
236
      assert false
237
    (* let typ' = Types.array_element_type typ in
238
     * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
239
     *   i i i pp_c_dimension d i
240
     *   (aux typ') q *)
241
    | (_d, LInt _r) :: _q ->
242
      assert false
243
    (* let typ' = Types.array_element_type typ in
244
     * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
245
     * fprintf fmt "@[<v 2>{@,%a@]@,}"
246
     *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
247
    | _ ->
248
      assert false
249
  in
250
  reset_loop_counter ();
251
  aux var_type fmt reordered_loop_vars
252

    
253
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
254

    
255
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
256
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
257
    (pp_print_option pp_print_int)
258
    i pp_mem mem pp_self self
259

    
260
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
261
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
262
    (mp.mpname.node_id, mem, self)
263

    
264
let pp_memory_pack_aux' ?i fmt =
265
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
266

    
267
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
268

    
269
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
270
    (name, inputs, locals, outputs, mem_in, mem_out) =
271
  let stateless = fst (get_stateless_status m) in
272
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
273
    (pp_print_option pp_print_int)
274
    i
275
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
276
    (pp_comma_list
277
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
278
       pp_input)
279
    inputs
280
    (pp_print_option (fun fmt _ ->
281
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
282
    i
283
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
284
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
285
    outputs
286

    
287
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
288
    (t, mem_in, mem_out) =
289
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
290
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
291

    
292
let pp_transition_aux' ?i m =
293
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
294

    
295
let pp_transition_aux'' ?i m =
296
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
297

    
298
let pp_transition' m =
299
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
300

    
301
let pp_transition'' m =
302
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
303

    
304
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
305
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
306
    pp_mem_out mem_out
307

    
308
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
309

    
310
let pp_functional_update mems fmt mem =
311
  let rec aux fmt mems =
312
    match mems with
313
    | [] ->
314
      pp_print_string fmt mem
315
    | x :: mems ->
316
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
317
  in
318
  aux fmt
319
    (* if Utils.ISet.is_empty mems then
320
     *   pp_print_string fmt mem
321
     *     else
322
     *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
323
     *     mem
324
     *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
325
     *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
326
    (Utils.ISet.elements mems)
327

    
328
module PrintSpec = struct
329
  type mode =
330
    | MemoryPackMode
331
    | TransitionMode
332
    | TransitionFootprintMode
333
    | ResetIn
334
    | ResetOut
335
    | InstrMode of ident
336

    
337
  let pp_reg mem fmt = function
338
    | ResetFlag ->
339
      fprintf fmt "%s.%s" mem reset_flag_name
340
    | StateVar x ->
341
      fprintf fmt "%s.%a" mem pp_var_decl x
342

    
343
  let pp_expr :
344
      type a.
345
      ?output:bool ->
346
      machine_t ->
347
      ident ->
348
      formatter ->
349
      (value_t, a) expression_t ->
350
      unit =
351
   fun ?(output = false) m mem fmt -> function
352
    | Val v ->
353
      pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
354
    | Tag t ->
355
      pp_print_string fmt t
356
    | Var v ->
357
      pp_var_decl fmt v
358
    | Memory r ->
359
      pp_reg mem fmt r
360

    
361
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
362
    let output, mem_update =
363
      match mode with
364
      | InstrMode _ ->
365
        true, false
366
      | TransitionFootprintMode ->
367
        false, true
368
      | _ ->
369
        false, false
370
    in
371
    let pp_expr :
372
        type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
373
     fun ?output fmt e -> pp_expr ?output m mem_out fmt e
374
    in
375
    match p with
376
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
377
      let pp_mem_in, pp_mem_out =
378
        match inst with
379
        | None ->
380
          ( pp_print_string,
381
            if mem_update then pp_functional_update mems else pp_print_string )
382
        | Some inst ->
383
          ( (fun fmt mem_in ->
384
              if r then pp_print_string fmt mem_in
385
              else pp_access' fmt (mem_in, inst)),
386
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
387
      in
388
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
389
        (f, inputs, locals, outputs, mem_in', mem_out')
390
    | Reset (_f, inst, r) ->
391
      pp_ite
392
        (pp_c_val m mem_in (pp_c_var_read m))
393
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
394
        (pp_equal pp_print_string pp_access')
395
        fmt
396
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
397
    | MemoryPack (f, inst, i) ->
398
      let pp_mem, pp_self =
399
        match inst with
400
        | None ->
401
          pp_print_string, pp_print_string
402
        | Some inst ->
403
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
404
            fun fmt self -> pp_indirect' fmt (self, inst) )
405
      in
406
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
407
    | ResetCleared f ->
408
      pp_reset_cleared' fmt (f, mem_in, mem_out)
409
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
410
    | Initialization ->
411
      ()
412

    
413
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
414

    
415
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
416
    | Val v ->
417
      v
418
    | Tag t ->
419
      id_to_tag t
420
    | Var v ->
421
      vdecl_to_val v
422
    | Memory (StateVar v) ->
423
      vdecl_to_val v
424
    | Memory ResetFlag ->
425
      vdecl_to_val reset_flag
426

    
427
  let find_arrow m =
428
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
429
    with Not_found ->
430
      eprintf "Internal error: arrow not found";
431
      raise Not_found
432

    
433
  let pp_spec mode m fmt f =
434
    let rec pp_spec mode fmt f =
435
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
436
        let self = mk_self m in
437
        let mem = mk_mem m in
438
        let mem_in = mk_mem_in m in
439
        let mem_out = mk_mem_out m in
440
        let mem_reset = mk_mem_reset m in
441
        match mode with
442
        | MemoryPackMode ->
443
          self, self, true, mem, mem, false
444
        | TransitionMode ->
445
          mem_in, mem_in, false, mem_out, mem_out, false
446
        | TransitionFootprintMode ->
447
          mem_in, mem_in, false, mem_out, mem_out, false
448
        | ResetIn ->
449
          mem_reset, mem_reset, false, mem_out, mem_out, false
450
        | ResetOut ->
451
          mem_in, mem_in, false, mem_reset, mem_reset, false
452
        | InstrMode self ->
453
          let mem = "*" ^ mem in
454
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
455
          self, flush_str_formatter (), false, mem, mem, false
456
      in
457
      let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
458
       fun fmt e -> pp_expr m mem_out fmt e
459
      in
460
      let pp_spec' = pp_spec mode in
461
      match f with
462
      | True ->
463
        pp_true fmt ()
464
      | False ->
465
        pp_false fmt ()
466
      | Equal (a, b) ->
467
        pp_assign_spec m mem_out
468
          (pp_c_var_read ~test_output:false m)
469
          indirect_l mem_in
470
          (pp_c_var_read ~test_output:false m)
471
          indirect_r fmt
472
          (type_of_l_value a, val_of_expr a, val_of_expr b)
473
      | And fs ->
474
        pp_and_l pp_spec' fmt fs
475
      | Or fs ->
476
        pp_or_l pp_spec' fmt fs
477
      | Imply (a, b) ->
478
        pp_par (pp_implies pp_spec' pp_spec') fmt (a, b)
479
      | Exists (xs, a) ->
480
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
481
      | Forall (xs, a) ->
482
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
483
      | Ternary (e, a, b) ->
484
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
485
      | Predicate p ->
486
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
487
      | StateVarPack ResetFlag ->
488
        let r = vdecl_to_val reset_flag in
489
        pp_assign_spec m mem_out
490
          (pp_c_var_read ~test_output:false m)
491
          indirect_l mem_in
492
          (pp_c_var_read ~test_output:false m)
493
          indirect_r fmt
494
          (Type_predef.type_bool, r, r)
495
      | StateVarPack (StateVar v) ->
496
        let v' = vdecl_to_val v in
497
        let inst = find_arrow m in
498
        pp_par
499
          (pp_implies
500
             (pp_not (pp_initialization pp_access'))
501
             (pp_assign_spec m mem_out
502
                (pp_c_var_read ~test_output:false m)
503
                indirect_l mem_in
504
                (pp_c_var_read ~test_output:false m)
505
                indirect_r))
506
          fmt
507
          ((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
508
      | ExistsMem (f, rc, tr) ->
509
        pp_exists
510
          (pp_machine_decl' ~ghost:true)
511
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
512
          fmt
513
          ((f, mk_mem_reset m), (rc, tr))
514
    in
515
    match mode with
516
    | TransitionFootprintMode ->
517
      let mem_in = mk_mem_in m in
518
      let mem_out = mk_mem_out m in
519
      pp_forall
520
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
521
        (pp_spec mode) fmt
522
        ((m.mname.node_id, [ mem_in; mem_out ]), f)
523
    | _ ->
524
      pp_spec mode fmt f
525
end
526

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

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

    
533
let pp_mem_valid_def fmt m =
534
  if not (fst (get_stateless_status m)) then
535
    let name = m.mname.node_id in
536
    let self = mk_self m in
537
    pp_acsl
538
      (pp_predicate
539
         (pp_mem_valid (pp_machine_decl pp_ptr))
540
         (pp_and
541
            (pp_and_l (fun fmt (inst, (td, _)) ->
542
                 if Arrow.td_is_arrow td then
543
                   pp_valid pp_indirect' fmt [ self, inst ]
544
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
545
            (pp_valid pp_print_string)))
546
      fmt
547
      ((name, (name, self)), (m.minstances, [ self ]))
548

    
549
let pp_memory_pack_def m fmt mp =
550
  let name = mp.mpname.node_id in
551
  let self = mk_self m in
552
  let mem = mk_mem m in
553
  pp_acsl
554
    (pp_predicate
555
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
556
       (PrintSpec.pp_spec MemoryPackMode m))
557
    fmt
558
    ((mp, (name, mem), (name, self)), mp.mpformula)
559

    
560
let print_machine_ghost_struct fmt m =
561
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
562

    
563
let pp_memory_pack_defs fmt m =
564
  if not (fst (get_stateless_status m)) then
565
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
566
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
567
         (pp_memory_pack_def m))
568
      m.mspec.mmemory_packs
569

    
570
let pp_transition_def m fmt t =
571
  let name = t.tname.node_id in
572
  let mem_in = mk_mem_in m in
573
  let mem_out = mk_mem_out m in
574
  pp_acsl
575
    (pp_predicate
576
       (pp_transition m
577
          (pp_machine_decl' ~ghost:true)
578
          (pp_machine_decl' ~ghost:true)
579
          (pp_local m) (pp_local m))
580
       (PrintSpec.pp_spec TransitionMode m))
581
    fmt
582
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
583

    
584
let pp_transition_defs fmt m =
585
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
586
    (pp_transition_def m) fmt m.mspec.mtransitions
587

    
588
let pp_transition_footprint fmt t =
589
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
590
    (pp_print_option pp_print_int)
591
    t.tindex
592

    
593
let pp_transition_footprint_lemma m fmt t =
594
  let open Utils.ISet in
595
  let name = t.tname.node_id in
596
  let mems =
597
    diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint
598
  in
599
  let memories =
600
    List.map
601
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
602
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
603
  in
604
  if not (is_empty mems) then
605
    pp_acsl
606
      (pp_lemma pp_transition_footprint
607
         (PrintSpec.pp_spec TransitionFootprintMode m))
608
      fmt
609
      ( t,
610
        Forall
611
          ( memories @ t.tinputs @ t.tlocals @ t.toutputs,
612
            Imply
613
              ( Spec_common.mk_transition ?i:t.tindex name
614
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
615
                  (vdecls_to_vals t.toutputs),
616
                Spec_common.mk_transition ~mems ?i:t.tindex name
617
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
618
                  (vdecls_to_vals t.toutputs) ) ) )
619

    
620
let pp_transition_footprint_lemmas fmt m =
621
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
622
    (pp_transition_footprint_lemma m)
623
    fmt
624
    (List.filter
625
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
626
       m.mspec.mtransitions)
627

    
628
let pp_initialization_def fmt m =
629
  if not (fst (get_stateless_status m)) then
630
    let name = m.mname.node_id in
631
    let mem_in = mk_mem_in m in
632
    pp_acsl
633
      (pp_predicate
634
         (pp_initialization (pp_machine_decl' ~ghost:true))
635
         (pp_and_l (fun fmt (i, (td, _)) ->
636
              if Arrow.td_is_arrow td then
637
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
638
              else
639
                pp_equal
640
                  (pp_reset_flag ~indirect:false pp_access')
641
                  pp_print_int fmt
642
                  ((mem_in, i), 1))))
643
      fmt
644
      ((name, (name, mem_in)), m.minstances)
645

    
646
let pp_reset_cleared_def fmt m =
647
  if not (fst (get_stateless_status m)) then
648
    let name = m.mname.node_id in
649
    let mem_in = mk_mem_in m in
650
    let mem_out = mk_mem_out m in
651
    pp_acsl
652
      (pp_predicate
653
         (pp_reset_cleared
654
            (pp_machine_decl' ~ghost:true)
655
            (pp_machine_decl' ~ghost:true))
656
         (pp_ite
657
            (pp_reset_flag' ~indirect:false)
658
            (pp_and
659
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
660
               pp_initialization')
661
            (pp_equal pp_print_string pp_print_string)))
662
      fmt
663
      ( (name, (name, mem_in), (name, mem_out)),
664
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
665

    
666
let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l
667

    
668
let label_pre = "Pre"
669

    
670
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
671

    
672
let pp_register_chain ?(indirect = true) ptr =
673
  pp_print_list
674
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
675
    ~pp_epilogue:(fun fmt () ->
676
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
677
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
678
    (fun fmt (i, _) -> pp_print_string fmt i)
679

    
680
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
681
  pp_print_list
682
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
683
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
684
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
685
    (fun fmt (i, _) -> pp_print_string fmt i)
686
    fmt mems
687

    
688
let pp_arrow_reset_ghost mem fmt inst =
689
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
690

    
691
module GhostProto : MODIFIERS_GHOST_PROTO = struct
692
  let pp_ghost_parameters ?(cut = true) fmt vs =
693
    fprintf fmt "%a%a"
694
      (if cut then pp_print_cut else pp_print_nothing)
695
      ()
696
      (pp_acsl_line'
697
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
698
      vs
699
end
700

    
701
module HdrMod = struct
702
  module GhostProto = GhostProto
703

    
704
  let print_machine_decl_prefix _ _ = ()
705

    
706
  let pp_import_arrow fmt () =
707
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
708
      (Arrow.arrow_top_decl ()).top_decl_owner
709
      (if !Options.cpp then "pp" else "")
710
end
711

    
712
module SrcMod = struct
713
  module GhostProto = GhostProto
714

    
715
  let pp_predicates (* dependencies *) fmt machines =
716
    let pp_preds comment pp =
717
      pp_print_list ~pp_open_box:pp_open_vbox0
718
        ~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut
719
    in
720
    fprintf fmt "%a%a%a%a%a%a"
721
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
722
      machines
723
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
724
      machines
725
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
726
      machines
727
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
728
      machines
729
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
730
      machines
731
      (pp_preds "/* ACSL transition memory footprints lemmas */"
732
         pp_transition_footprint_lemmas)
733
      machines
734

    
735
  let pp_clear_reset_spec fmt self mem m =
736
    let name = m.mname.node_id in
737
    let arws, narws =
738
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
739
    in
740
    let mk_insts = List.map (fun x -> [ x ]) in
741
    pp_acsl_cut
742
      (fun fmt () ->
743
        fprintf fmt
744
          "%a@,\
745
           %a@,\
746
           %a@,\
747
           %a@,\
748
           %a@,\
749
           %a@,\
750
           %a@,\
751
           %a@,\
752
           %a@,\
753
           %a@,\
754
           @[<v 2>behavior reset:@;\
755
           %a@,\
756
           %a@]@,\
757
           @[<v 2>behavior no_reset:@;\
758
           %a@,\
759
           %a@]@,\
760
           complete behaviors;@,\
761
           disjoint behaviors;"
762
          (pp_requires pp_mem_valid')
763
          (name, self)
764
          (pp_requires (pp_separated self mem))
765
          (mk_insts m.minstances, [])
766
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
767
          (name, mem, self)
768
          (pp_ensures
769
             (pp_memory_pack_aux
770
                ~i:(List.length m.mspec.mmemory_packs - 2)
771
                pp_ptr pp_print_string))
772
          (name, mem, self)
773
          (pp_assigns pp_reset_flag')
774
          [ self ]
775
          (pp_assigns (pp_register_chain self))
776
          (mk_insts arws)
777
          (pp_assigns (pp_reset_flag_chain self))
778
          (mk_insts narws)
779
          (pp_assigns pp_reset_flag')
780
          [ mem ]
781
          (pp_assigns (pp_register_chain ~indirect:false mem))
782
          (mk_insts arws)
783
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
784
          (mk_insts narws)
785
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
786
          (mem, 1)
787
          (pp_ensures (pp_initialization pp_ptr))
788
          (name, mem)
789
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
790
          (mem, 0)
791
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
792
          (mem, mem))
793
      fmt ()
794

    
795
  let pp_set_reset_spec fmt self mem m =
796
    let name = m.mname.node_id in
797
    pp_acsl_cut
798
      (fun fmt () ->
799
        fprintf fmt "%a@,%a@,%a"
800
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
801
          (name, mem, self)
802
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
803
          (mem, 1)
804
          (pp_assigns pp_reset_flag')
805
          [ self; mem ])
806
      fmt ()
807

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

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

    
887
  let pp_step_instr_spec m self mem fmt instr =
888
    fprintf fmt "%a%a"
889
      (pp_ghost_instr_code m mem)
890
      instr
891
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
892
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
893
      instr.instr_spec
894

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

    
904
(**************************************************************************)
905
(*                              MAKEFILE                                  *)
906
(**************************************************************************)
907

    
908
module MakefileMod = struct
909
  let other_targets fmt basename _nodename dependencies =
910
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
911
    (* EACSL version of library file . c *)
912
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
913
    fprintf fmt
914
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
915
       e-acsl -print -ocode %s_eacsl.c@."
916
      basename basename;
917
    fprintf fmt "@.";
918
    fprintf fmt "@.";
919

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

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

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