Project

General

Profile

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

    
20
module Mpfr = Lustrec_mpfr
21

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

    
25
(**************************************************************************)
26

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

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

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

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

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

    
47
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req
48

    
49
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens
50

    
51
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm
52

    
53
let pp_assigns pp =
54
  pp_comma_list
55
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
56
    ~pp_epilogue:pp_print_semicolon' pp
57

    
58
let pp_ghost pp_gho fmt = fprintf fmt "ghost %a" pp_gho
59

    
60
let pp_assert pp_ast fmt = fprintf fmt "assert %a;" pp_ast
61

    
62
let pp_mem_valid pp_var fmt (name, var) =
63
  fprintf fmt "%s_valid(%a)" name pp_var var
64

    
65
let pp_mem_valid' = pp_mem_valid pp_print_string
66

    
67
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
68
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
69

    
70
let pp_indirect' = pp_indirect pp_print_string pp_print_string
71

    
72
let pp_access pp_stru pp_field fmt (stru, field) =
73
  fprintf fmt "%a.%a" pp_stru stru pp_field field
74

    
75
let pp_access' = pp_access pp_print_string pp_print_string
76

    
77
let pp_var_decl fmt v = pp_print_string fmt v.var_id
78

    
79
let pp_reg self fmt field =
80
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
81

    
82
let pp_true fmt () = pp_print_string fmt "\\true"
83

    
84
let pp_false fmt () = pp_print_string fmt "\\false"
85

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

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

    
109
let memories insts =
110
  List.(
111
    map
112
      (fun path ->
113
        let _, (_, mems) = hd (rev path) in
114
        map (fun mem -> path, mem) mems)
115
      insts
116
    |> flatten)
117

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

    
124
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
125
  pp_access
126
    ((if indirect then pp_indirect else pp_access)
127
       (pp_instance ~indirect ptr)
128
       pp_print_string)
129
    pp_var_decl fmt
130
    ((path, "_reg"), mem)
131

    
132
let prefixes l =
133
  let rec pref acc = function
134
    | x :: l ->
135
      pref ([ x ] :: List.map (List.cons x) acc) l
136
    | [] ->
137
      acc
138
  in
139
  pref [] (List.rev l)
140

    
141
let powerset_instances paths = List.map prefixes paths |> List.flatten
142

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

    
150
let pp_separated' =
151
  pp_comma_list
152
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
153
    ~pp_epilogue:pp_print_cpar pp_var_decl
154

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

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

    
161
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
162

    
163
let pp_implies pp_l pp_r fmt (l, r) =
164
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
165

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

    
168
let pp_and_l pp_v fmt =
169
  pp_print_list ~pp_open_box:pp_open_vbox0
170
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
171
    pp_v fmt
172

    
173
let pp_or_l pp_v fmt =
174
  pp_print_list ~pp_open_box:pp_open_vbox0
175
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
176
    pp_v fmt
177

    
178
let pp_not pp fmt = fprintf fmt "!%a" pp
179

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

    
182
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
183

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

    
187
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
188

    
189
let pp_initialization pp_mem fmt (name, mem) =
190
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
191

    
192
let pp_initialization' = pp_initialization pp_print_string
193

    
194
let pp_local m =
195
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
196

    
197
let pp_locals m =
198
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
199

    
200
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
201

    
202
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
203
  if Types.is_real_type typ && !Options.mpfr then assert false
204
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
205
  else pp_equal pp_l pp_r fmt (var_name, value)
206

    
207
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
208
    (var_type, var_name, value) =
209
  let depth = expansion_depth value in
210
  let loop_vars = mk_loop_variables m var_type depth in
211
  let reordered_loop_vars = reorder_loop_variables loop_vars in
212
  let aux typ fmt vars =
213
    match vars with
214
    | [] ->
215
      pp_basic_assign_spec
216
        (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars
217
           pp_var_l)
218
        (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars
219
           pp_var_r)
220
        fmt typ var_name value
221
    | (_d, LVar _i) :: _q ->
222
      assert false
223
    (* let typ' = Types.array_element_type typ in
224
     * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
225
     *   i i i pp_c_dimension d i
226
     *   (aux typ') q *)
227
    | (_d, LInt _r) :: _q ->
228
      assert false
229
    (* let typ' = Types.array_element_type typ in
230
     * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
231
     * fprintf fmt "@[<v 2>{@,%a@]@,}"
232
     *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
233
    | _ ->
234
      assert false
235
  in
236
  reset_loop_counter ();
237
  aux var_type fmt reordered_loop_vars
238

    
239
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
240
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
241
    (pp_print_option pp_print_int)
242
    i pp_mem mem pp_self self
243

    
244
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
245
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
246
    (mp.mpname.node_id, mem, self)
247

    
248
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
249
    (name, vars, mem_in, mem_out) =
250
  let stateless = fst (get_stateless_status m) in
251
  fprintf fmt "%s_transition%a(@[<hov>%t%a%t@])" name
252
    (pp_print_option pp_print_int)
253
    i
254
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
255
    (pp_comma_list
256
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
257
       pp_var)
258
    vars
259
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
260

    
261
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
262
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_var fmt
263
    (t.tname.node_id, t.tvars, mem_in, mem_out)
264

    
265
let pp_transition_aux' ?i m =
266
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
267
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
268

    
269
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
270
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
271
    pp_mem_out mem_out
272

    
273
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
274

    
275
let pp_functional_update mems insts fmt mem =
276
  let rec aux fmt = function
277
    | [] ->
278
      pp_print_string fmt mem
279
    | (x, is_mem) :: fields ->
280
      fprintf fmt "{ @[<hov>%a@ \\with .%s%s = %s@] }" aux fields
281
        (if is_mem then "_reg." else "")
282
        x x
283
  in
284
  aux fmt
285
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
286
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
287

    
288
module PrintSpec = struct
289
  type mode =
290
    | MemoryPackMode
291
    | TransitionMode
292
    | TransitionFootprintMode
293
    | ResetIn
294
    | ResetOut
295
    | InstrMode of ident
296

    
297
  let pp_reg mem fmt = function
298
    | ResetFlag ->
299
      fprintf fmt "%s.%s" mem reset_flag_name
300
    | StateVar x ->
301
      fprintf fmt "%s.%a" mem pp_var_decl x
302

    
303
  let pp_expr :
304
      type a.
305
      ?test_output:bool ->
306
      machine_t ->
307
      ident ->
308
      formatter ->
309
      (value_t, a) expression_t ->
310
      unit =
311
   fun ?(test_output = false) m mem fmt -> function
312
    | Val v ->
313
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
314
    | Tag t ->
315
      pp_print_string fmt t
316
    | Var v ->
317
      pp_var_decl fmt v
318
    | Memory r ->
319
      pp_reg mem fmt r
320

    
321
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
322
    let test_output, mem_update =
323
      match mode with
324
      | InstrMode _ ->
325
        true, false
326
      | TransitionFootprintMode ->
327
        false, true
328
      | _ ->
329
        false, false
330
    in
331
    let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
332
        =
333
     fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
334
    in
335
    match p with
336
    | Transition (f, inst, i, vars, r, mems, insts) ->
337
      let pp_mem_in, pp_mem_out =
338
        match inst with
339
        | None ->
340
          ( pp_print_string,
341
            if mem_update then pp_functional_update mems insts
342
            else pp_print_string )
343
        | Some inst ->
344
          ( (fun fmt mem_in ->
345
              if r then pp_print_string fmt mem_in
346
              else pp_access' fmt (mem_in, inst)),
347
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
348
      in
349
      pp_transition_aux ?i m pp_mem_in pp_mem_out (pp_expr test_output) fmt
350
        (f, vars, mem_in', mem_out')
351
    | Reset (_f, inst, r) ->
352
      pp_ite
353
        (pp_c_val m mem_in (pp_c_var_read m))
354
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
355
        (pp_equal pp_print_string pp_access')
356
        fmt
357
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
358
    | MemoryPack (f, inst, i) ->
359
      let pp_mem, pp_self =
360
        match inst with
361
        | None ->
362
          pp_print_string, pp_print_string
363
        | Some inst ->
364
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
365
            fun fmt self -> pp_indirect' fmt (self, inst) )
366
      in
367
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
368
    | ResetCleared f ->
369
      pp_reset_cleared' fmt (f, mem_in, mem_out)
370
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
371
    | Initialization ->
372
      ()
373

    
374
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
375

    
376
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
377
    | Val v ->
378
      v
379
    | Tag t ->
380
      id_to_tag t
381
    | Var v ->
382
      vdecl_to_val v
383
    | Memory (StateVar v) ->
384
      vdecl_to_val v
385
    | Memory ResetFlag ->
386
      vdecl_to_val reset_flag
387

    
388
  let find_arrow m =
389
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
390
    with Not_found ->
391
      eprintf "Internal error: arrow not found";
392
      raise Not_found
393

    
394
  let pp_spec mode m =
395
    let rec pp_spec mode fmt f =
396
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
397
        let self = mk_self m in
398
        let mem = mk_mem m in
399
        let mem_in = mk_mem_in m in
400
        let mem_out = mk_mem_out m in
401
        let mem_reset = mk_mem_reset m in
402
        match mode with
403
        | MemoryPackMode ->
404
          self, self, true, mem, mem, false
405
        | TransitionMode ->
406
          mem_in, mem_in, false, mem_out, mem_out, false
407
        | TransitionFootprintMode ->
408
          mem_in, mem_in, false, mem_out, mem_out, false
409
        | ResetIn ->
410
          mem_reset, mem_reset, false, mem_out, mem_out, false
411
        | ResetOut ->
412
          mem_in, mem_in, false, mem_reset, mem_reset, false
413
        | InstrMode self ->
414
          let mem = "*" ^ mem in
415
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
416
          self, flush_str_formatter (), false, mem, mem, false
417
      in
418
      let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
419
       fun fmt e -> pp_expr m mem_out fmt e
420
      in
421
      let pp_spec' = pp_spec mode in
422
      match f with
423
      | True ->
424
        pp_true fmt ()
425
      | False ->
426
        pp_false fmt ()
427
      | Equal (a, b) ->
428
        pp_assign_spec m mem_out
429
          (pp_c_var_read ~test_output:false m)
430
          indirect_l mem_in
431
          (pp_c_var_read ~test_output:false m)
432
          indirect_r fmt
433
          (type_of_l_value a, val_of_expr a, val_of_expr b)
434
      | And fs ->
435
        pp_and_l pp_spec' fmt fs
436
      | Or fs ->
437
        pp_or_l pp_spec' fmt fs
438
      | Imply (a, b) ->
439
        pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
440
      | Exists (xs, a) ->
441
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
442
      | Forall (xs, a) ->
443
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
444
      | Ternary (e, a, b) ->
445
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
446
      | Predicate p ->
447
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
448
      | StateVarPack ResetFlag ->
449
        let r = vdecl_to_val reset_flag in
450
        pp_assign_spec m mem_out
451
          (pp_c_var_read ~test_output:false m)
452
          indirect_l mem_in
453
          (pp_c_var_read ~test_output:false m)
454
          indirect_r fmt
455
          (Type_predef.type_bool, r, r)
456
      | StateVarPack (StateVar v) ->
457
        let v' = vdecl_to_val v in
458
        let inst = find_arrow m in
459
        pp_paren
460
          (pp_implies
461
             (pp_not (pp_initialization pp_access'))
462
             (pp_assign_spec m mem_out
463
                (pp_c_var_read ~test_output:false m)
464
                indirect_l mem_in
465
                (pp_c_var_read ~test_output:false m)
466
                indirect_r))
467
          fmt
468
          ((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
469
      | ExistsMem (f, rc, tr) ->
470
        pp_exists
471
          (pp_machine_decl' ~ghost:true)
472
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
473
          fmt
474
          ((f, mk_mem_reset m), (rc, tr))
475
    in
476
    pp_spec mode
477
end
478

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

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

    
485
let pp_mem_valid_def fmt m =
486
  if not (fst (get_stateless_status m)) then
487
    let name = m.mname.node_id in
488
    let self = mk_self m in
489
    pp_acsl
490
      (pp_predicate
491
         (pp_mem_valid (pp_machine_decl pp_ptr))
492
         (pp_and
493
            (pp_and_l (fun fmt (inst, (td, _)) ->
494
                 if Arrow.td_is_arrow td then
495
                   pp_valid pp_indirect' fmt [ self, inst ]
496
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
497
            (pp_valid pp_print_string)))
498
      fmt
499
      ((name, (name, self)), (m.minstances, [ self ]))
500

    
501
let pp_memory_pack_def m fmt mp =
502
  let name = mp.mpname.node_id in
503
  let self = mk_self m in
504
  let mem = mk_mem m in
505
  pp_acsl
506
    (pp_predicate
507
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
508
       (PrintSpec.pp_spec MemoryPackMode m))
509
    fmt
510
    ((mp, (name, mem), (name, self)), mp.mpformula)
511

    
512
let print_machine_ghost_struct fmt m =
513
  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
514

    
515
let pp_memory_pack_defs fmt m =
516
  if not (fst (get_stateless_status m)) then
517
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
518
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
519
         (pp_memory_pack_def m))
520
      m.mspec.mmemory_packs
521

    
522
let pp_transition_def m fmt t =
523
  let name = t.tname.node_id in
524
  let mem_in = mk_mem_in m in
525
  let mem_out = mk_mem_out m in
526
  pp_acsl
527
    (pp_predicate
528
       (pp_transition m
529
          (pp_machine_decl' ~ghost:true)
530
          (pp_machine_decl' ~ghost:true)
531
          (pp_local m))
532
       (PrintSpec.pp_spec TransitionMode m))
533
    fmt
534
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
535

    
536
let pp_transition_defs fmt m =
537
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
538
    (pp_transition_def m) fmt m.mspec.mtransitions
539

    
540
let pp_transition_footprint fmt t =
541
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
542
    (pp_print_option pp_print_int)
543
    t.tindex
544

    
545
let pp_transition_footprint_lemma m fmt t =
546
  let name = t.tname.node_id in
547
  let mem_in = mk_mem_in m in
548
  let mem_out = mk_mem_out m in
549
  let mems =
550
    ISet.(
551
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
552
  in
553
  let insts =
554
    IMap.(
555
      diff
556
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
557
        t.tinst_footprint)
558
  in
559
  let memories =
560
    List.map
561
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
562
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
563
  in
564
  let mems_empty = ISet.is_empty mems in
565
  let insts_empty = IMap.is_empty insts in
566
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
567
  let tr ?mems ?insts () =
568
    Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
569
      (vdecls_to_vals t.tvars)
570
  in
571
  if not (mems_empty && insts_empty) then
572
    pp_acsl
573
      (pp_lemma pp_transition_footprint
574
         (pp_forall
575
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
576
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
577
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
578
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
579
                else pp_forall (pp_locals m))
580
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
581
      fmt
582
      ( t,
583
        ( (m.mname.node_id, [ mem_in; mem_out ]),
584
          ( instances,
585
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
586
      )
587

    
588
let pp_transition_footprint_lemmas fmt m =
589
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
590
    (pp_transition_footprint_lemma m)
591
    fmt
592
    (List.filter
593
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
594
       m.mspec.mtransitions)
595

    
596
let pp_initialization_def fmt m =
597
  if not (fst (get_stateless_status m)) then
598
    let name = m.mname.node_id in
599
    let mem_in = mk_mem_in m in
600
    pp_acsl
601
      (pp_predicate
602
         (pp_initialization (pp_machine_decl' ~ghost:true))
603
         (pp_and_l (fun fmt (i, (td, _)) ->
604
              if Arrow.td_is_arrow td then
605
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
606
              else
607
                pp_equal
608
                  (pp_reset_flag ~indirect:false pp_access')
609
                  pp_print_int fmt
610
                  ((mem_in, i), 1))))
611
      fmt
612
      ((name, (name, mem_in)), m.minstances)
613

    
614
let pp_reset_cleared_def fmt m =
615
  if not (fst (get_stateless_status m)) then
616
    let name = m.mname.node_id in
617
    let mem_in = mk_mem_in m in
618
    let mem_out = mk_mem_out m in
619
    pp_acsl
620
      (pp_predicate
621
         (pp_reset_cleared
622
            (pp_machine_decl' ~ghost:true)
623
            (pp_machine_decl' ~ghost:true))
624
         (pp_ite
625
            (pp_reset_flag' ~indirect:false)
626
            (pp_and
627
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
628
               pp_initialization')
629
            (pp_equal pp_print_string pp_print_string)))
630
      fmt
631
      ( (name, (name, mem_in), (name, mem_out)),
632
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
633

    
634
let pp_register_chain ?(indirect = true) ptr =
635
  pp_print_list
636
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
637
    ~pp_epilogue:(fun fmt () ->
638
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
639
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
640
    (fun fmt (i, _) -> pp_print_string fmt i)
641

    
642
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
643
  pp_print_list
644
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
645
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
646
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
647
    (fun fmt (i, _) -> pp_print_string fmt i)
648
    fmt mems
649

    
650
let pp_arrow_reset_ghost mem fmt inst =
651
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
652

    
653
module GhostProto : MODIFIERS_GHOST_PROTO = struct
654
  let pp_ghost_parameters ?(cut = true) fmt vs =
655
    fprintf fmt "%a%a"
656
      (if cut then pp_print_cut else pp_print_nothing)
657
      ()
658
      (pp_acsl_line'
659
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
660
      vs
661
end
662

    
663
module HdrMod = struct
664
  module GhostProto = GhostProto
665

    
666
  let print_machine_decl_prefix _ _ = ()
667

    
668
  let pp_import_arrow fmt () =
669
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
670
      (Arrow.arrow_top_decl ()).top_decl_owner
671
      (if !Options.cpp then "pp" else "")
672
end
673

    
674
module SrcMod = struct
675
  module GhostProto = GhostProto
676

    
677
  let pp_predicates (* dependencies *) fmt machines =
678
    let pp_preds comment pp =
679
      pp_print_list ~pp_open_box:pp_open_vbox0
680
        ~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut
681
    in
682
    fprintf fmt "%a%a%a%a%a%a"
683
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
684
      machines
685
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
686
      machines
687
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
688
      machines
689
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
690
      machines
691
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
692
      machines
693
      (pp_preds "/* ACSL transition memory footprints lemmas */"
694
         pp_transition_footprint_lemmas)
695
      machines
696

    
697
  let pp_clear_reset_spec fmt self mem m =
698
    let name = m.mname.node_id in
699
    let arws, narws =
700
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
701
    in
702
    let mk_insts = List.map (fun x -> [ x ]) in
703
    pp_acsl_cut
704
      (fun fmt () ->
705
        fprintf fmt
706
          "%a@,\
707
           %a@,\
708
           %a@,\
709
           %a@,\
710
           %a@,\
711
           %a@,\
712
           %a@,\
713
           %a@,\
714
           %a@,\
715
           %a@,\
716
           @[<v 2>behavior reset:@;\
717
           %a@,\
718
           %a@]@,\
719
           @[<v 2>behavior no_reset:@;\
720
           %a@,\
721
           %a@]@,\
722
           complete behaviors;@,\
723
           disjoint behaviors;"
724
          (pp_requires pp_mem_valid')
725
          (name, self)
726
          (pp_requires (pp_separated self mem))
727
          (mk_insts m.minstances, [])
728
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
729
          (name, mem, self)
730
          (pp_ensures
731
             (pp_memory_pack_aux
732
                ~i:(List.length m.mspec.mmemory_packs - 2)
733
                pp_ptr pp_print_string))
734
          (name, mem, self)
735
          (pp_assigns pp_reset_flag')
736
          [ self ]
737
          (pp_assigns (pp_register_chain self))
738
          (mk_insts arws)
739
          (pp_assigns (pp_reset_flag_chain self))
740
          (mk_insts narws)
741
          (pp_assigns pp_reset_flag')
742
          [ mem ]
743
          (pp_assigns (pp_register_chain ~indirect:false mem))
744
          (mk_insts arws)
745
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
746
          (mk_insts narws)
747
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
748
          (mem, 1)
749
          (pp_ensures (pp_initialization pp_ptr))
750
          (name, mem)
751
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
752
          (mem, 0)
753
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
754
          (mem, mem))
755
      fmt ()
756

    
757
  let pp_set_reset_spec fmt self mem m =
758
    let name = m.mname.node_id in
759
    pp_acsl_cut
760
      (fun fmt () ->
761
        fprintf fmt "%a@,%a@,%a"
762
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
763
          (name, mem, self)
764
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
765
          (mem, 1)
766
          (pp_assigns pp_reset_flag')
767
          [ self; mem ])
768
      fmt ()
769

    
770
  let pp_step_spec fmt machines self mem m =
771
    let name = m.mname.node_id in
772
    let insts = instances machines m in
773
    let insts' = powerset_instances insts in
774
    let insts'' =
775
      List.(
776
        filter
777
          (fun l -> l <> [])
778
          (map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
779
    in
780
    let inputs = m.mstep.step_inputs in
781
    let outputs = m.mstep.step_outputs in
782
    pp_acsl_cut
783
      (fun fmt () ->
784
        if fst (get_stateless_status m) then
785
          fprintf fmt "%a@,%a@,%a@,%a"
786
            (pp_requires (pp_valid pp_var_decl))
787
            outputs
788
            (pp_requires pp_separated')
789
            outputs (pp_assigns pp_ptr_decl) outputs
790
            (pp_ensures (pp_transition_aux' m))
791
            (name, inputs @ outputs, "", "")
792
        else
793
          fprintf fmt
794
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
795
            (pp_requires (pp_valid pp_var_decl))
796
            outputs
797
            (pp_requires pp_mem_valid')
798
            (name, self)
799
            (pp_requires (pp_separated self mem))
800
            (insts', outputs)
801
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
802
            (name, mem, self)
803
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
804
            (name, mem, self)
805
            (pp_ensures
806
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
807
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
808
            (name, inputs @ outputs, mem, mem)
809
            (pp_assigns pp_ptr_decl) outputs
810
            (pp_assigns (pp_reg self))
811
            m.mmemory
812
            (pp_assigns pp_reset_flag')
813
            [ self ]
814
            (pp_assigns (pp_memory self))
815
            (memories insts')
816
            (pp_assigns (pp_register_chain self))
817
            insts
818
            (pp_assigns (pp_reset_flag_chain self))
819
            insts''
820
            (pp_assigns (pp_reg mem))
821
            m.mmemory
822
            (pp_assigns pp_reset_flag')
823
            [ mem ]
824
            (pp_assigns (pp_memory ~indirect:false mem))
825
            (memories insts')
826
            (pp_assigns (pp_register_chain ~indirect:false mem))
827
            insts
828
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
829
            insts'')
830
      fmt ()
831

    
832
  let pp_ghost_instr_code m self fmt instr =
833
    match instr.instr_desc with
834
    | MStateAssign (x, v) ->
835
      fprintf fmt "@,%a"
836
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
837
        (x, v)
838
    | MResetAssign b ->
839
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
840
    | MSetReset inst ->
841
      let td, _ = List.assoc inst m.minstances in
842
      if Arrow.td_is_arrow td then
843
        fprintf fmt "@,%a;"
844
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
845
          inst
846
    | _ ->
847
      ()
848

    
849
  let pp_step_instr_spec m self mem fmt instr =
850
    fprintf fmt "%a%a"
851
      (pp_ghost_instr_code m mem)
852
      instr
853
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
854
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
855
      instr.instr_spec
856

    
857
  let pp_ghost_parameter mem fmt inst =
858
    GhostProto.pp_ghost_parameters ~cut:false fmt
859
      (match inst with
860
      | Some inst ->
861
        [ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ]
862
      | None ->
863
        [ mem, pp_print_string ])
864
end
865

    
866
(**************************************************************************)
867
(*                              MAKEFILE                                  *)
868
(**************************************************************************)
869

    
870
module MakefileMod = struct
871
  let other_targets fmt basename _nodename dependencies =
872
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
873
    (* EACSL version of library file . c *)
874
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
875
    fprintf fmt
876
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
877
       e-acsl -print -ocode %s_eacsl.c@."
878
      basename basename;
879
    fprintf fmt "@.";
880
    fprintf fmt "@.";
881

    
882
    (* EACSL version of library file . c + main .c *)
883
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename
884
      basename basename;
885
    fprintf fmt
886
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
887
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
888
      basename basename basename;
889
    (* Ugly hack to deal with eacsl bugs *)
890
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
891
      basename basename;
892
    fprintf fmt "@.";
893
    fprintf fmt "@.";
894

    
895
    (* EACSL version of binary *)
896
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
897
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
898
      basename;
899
    (* compiling instrumented lib + main *)
900
    C_backend_makefile.fprintf_dependencies fmt dependencies;
901
    fprintf fmt
902
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
903
       %s_main_eacsl.o %a@."
904
      basename
905
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
906
      (C_backend_makefile.compiled_dependencies dependencies)
907
      ("${FRAMACEACSL}/e_acsl.c "
908
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
909
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
910
      basename
911
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
912
      (C_backend_makefile.lib_dependencies dependencies);
913
    fprintf fmt "@."
914
end
915

    
916
(* Local Variables: *)
917
(* compile-command:"make -C ../../.." *)
918
(* End: *)
(15-15/18)