Project

General

Profile

Download (31 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
(**************************************************************************)
21
(*     Printing spec for c *)
22

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

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

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

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

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

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

    
45
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line 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_par pp fmt = fprintf fmt "(%a)" pp
156

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

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

    
163
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
164

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

    
167
let pp_implies pp_l pp_r fmt (l, r) =
168
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
169

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

    
172
let pp_and_l pp_v fmt =
173
  pp_print_list ~pp_open_box:pp_open_vbox0
174
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
175
    pp_v fmt
176

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

    
179
let pp_or_l pp_v fmt =
180
  pp_print_list ~pp_open_box:pp_open_vbox0
181
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
182
    pp_v fmt
183

    
184
let pp_not pp fmt = fprintf fmt "!%a" pp
185

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

    
188
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
189

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

    
193
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
194

    
195
let pp_initialization pp_mem fmt (name, mem) =
196
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
197

    
198
let pp_initialization' = pp_initialization pp_print_string
199

    
200
let pp_local m =
201
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
202

    
203
let pp_locals m =
204
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
205

    
206
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
207

    
208
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
209
  if Types.is_real_type typ && !Options.mpfr then assert false
210
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
211
  else pp_equal pp_l pp_r fmt (var_name, value)
212

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

    
245
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
246

    
247
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
248
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
249
    (pp_print_option pp_print_int)
250
    i pp_mem mem pp_self self
251

    
252
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
253
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
254
    (mp.mpname.node_id, mem, self)
255

    
256
let pp_memory_pack_aux' ?i fmt =
257
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
258

    
259
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
260

    
261
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
262
    (name, vars, mem_in, mem_out) =
263
  let stateless = fst (get_stateless_status m) in
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%t@])" name
265
    (pp_print_option pp_print_int)
266
    i
267
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
268
    (pp_comma_list
269
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
270
       pp_var)
271
    vars
272
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
273

    
274
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
275
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_var fmt
276
    (t.tname.node_id, t.tvars, mem_in, mem_out)
277

    
278
let pp_transition_aux' ?i m =
279
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl
280

    
281
let pp_transition_aux'' ?i m =
282
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
283
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
284

    
285
let pp_transition' m =
286
  pp_transition m pp_print_string pp_print_string pp_var_decl
287

    
288
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
289
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
290
    pp_mem_out mem_out
291

    
292
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
293

    
294
let pp_functional_update mems insts fmt mem =
295
  let rec aux fmt = function
296
    | [] ->
297
      pp_print_string fmt mem
298
    | (x, is_mem) :: fields ->
299
      fprintf fmt "{ @[<hov>%a@ \\with .%s%s = %s@] }" aux fields
300
        (if is_mem then "_reg." else "")
301
        x x
302
  in
303
  aux fmt
304
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
305
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
306

    
307
module PrintSpec = struct
308
  type mode =
309
    | MemoryPackMode
310
    | TransitionMode
311
    | TransitionFootprintMode
312
    | ResetIn
313
    | ResetOut
314
    | InstrMode of ident
315

    
316
  let pp_reg mem fmt = function
317
    | ResetFlag ->
318
      fprintf fmt "%s.%s" mem reset_flag_name
319
    | StateVar x ->
320
      fprintf fmt "%s.%a" mem pp_var_decl x
321

    
322
  let pp_expr :
323
      type a.
324
      ?test_output:bool ->
325
      machine_t ->
326
      ident ->
327
      formatter ->
328
      (value_t, a) expression_t ->
329
      unit =
330
   fun ?(test_output = false) m mem fmt -> function
331
    | Val v ->
332
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
333
    | Tag t ->
334
      pp_print_string fmt t
335
    | Var v ->
336
      pp_var_decl fmt v
337
    | Memory r ->
338
      pp_reg mem fmt r
339

    
340
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
341
    let test_output, mem_update =
342
      match mode with
343
      | InstrMode _ ->
344
        true, false
345
      | TransitionFootprintMode ->
346
        false, true
347
      | _ ->
348
        false, false
349
    in
350
    let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
351
        =
352
     fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
353
    in
354
    match p with
355
    | Transition (f, inst, i, vars, r, mems, insts) ->
356
      let pp_mem_in, pp_mem_out =
357
        match inst with
358
        | None ->
359
          ( pp_print_string,
360
            if mem_update then pp_functional_update mems insts
361
            else pp_print_string )
362
        | Some inst ->
363
          ( (fun fmt mem_in ->
364
              if r then pp_print_string fmt mem_in
365
              else pp_access' fmt (mem_in, inst)),
366
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
367
      in
368
      pp_transition_aux ?i m pp_mem_in pp_mem_out (pp_expr test_output) fmt
369
        (f, vars, mem_in', mem_out')
370
    | Reset (_f, inst, r) ->
371
      pp_ite
372
        (pp_c_val m mem_in (pp_c_var_read m))
373
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
374
        (pp_equal pp_print_string pp_access')
375
        fmt
376
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
377
    | MemoryPack (f, inst, i) ->
378
      let pp_mem, pp_self =
379
        match inst with
380
        | None ->
381
          pp_print_string, pp_print_string
382
        | Some inst ->
383
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
384
            fun fmt self -> pp_indirect' fmt (self, inst) )
385
      in
386
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
387
    | ResetCleared f ->
388
      pp_reset_cleared' fmt (f, mem_in, mem_out)
389
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
390
    | Initialization ->
391
      ()
392

    
393
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
394

    
395
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
396
    | Val v ->
397
      v
398
    | Tag t ->
399
      id_to_tag t
400
    | Var v ->
401
      vdecl_to_val v
402
    | Memory (StateVar v) ->
403
      vdecl_to_val v
404
    | Memory ResetFlag ->
405
      vdecl_to_val reset_flag
406

    
407
  let find_arrow m =
408
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
409
    with Not_found ->
410
      eprintf "Internal error: arrow not found";
411
      raise Not_found
412

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

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

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

    
504
let pp_mem_valid_def fmt m =
505
  if not (fst (get_stateless_status m)) then
506
    let name = m.mname.node_id in
507
    let self = mk_self m in
508
    pp_acsl
509
      (pp_predicate
510
         (pp_mem_valid (pp_machine_decl pp_ptr))
511
         (pp_and
512
            (pp_and_l (fun fmt (inst, (td, _)) ->
513
                 if Arrow.td_is_arrow td then
514
                   pp_valid pp_indirect' fmt [ self, inst ]
515
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
516
            (pp_valid pp_print_string)))
517
      fmt
518
      ((name, (name, self)), (m.minstances, [ self ]))
519

    
520
let pp_memory_pack_def m fmt mp =
521
  let name = mp.mpname.node_id in
522
  let self = mk_self m in
523
  let mem = mk_mem m in
524
  pp_acsl
525
    (pp_predicate
526
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
527
       (PrintSpec.pp_spec MemoryPackMode m))
528
    fmt
529
    ((mp, (name, mem), (name, self)), mp.mpformula)
530

    
531
let print_machine_ghost_struct fmt m =
532
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
533

    
534
let pp_memory_pack_defs fmt m =
535
  if not (fst (get_stateless_status m)) then
536
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
537
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
538
         (pp_memory_pack_def m))
539
      m.mspec.mmemory_packs
540

    
541
let pp_transition_def m fmt t =
542
  let name = t.tname.node_id in
543
  let mem_in = mk_mem_in m in
544
  let mem_out = mk_mem_out m in
545
  pp_acsl
546
    (pp_predicate
547
       (pp_transition m
548
          (pp_machine_decl' ~ghost:true)
549
          (pp_machine_decl' ~ghost:true)
550
          (pp_local m))
551
       (PrintSpec.pp_spec TransitionMode m))
552
    fmt
553
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
554

    
555
let pp_transition_defs fmt m =
556
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
557
    (pp_transition_def m) fmt m.mspec.mtransitions
558

    
559
let pp_transition_footprint fmt t =
560
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
561
    (pp_print_option pp_print_int)
562
    t.tindex
563

    
564
let pp_transition_footprint_lemma m fmt t =
565
  let name = t.tname.node_id in
566
  let mem_in = mk_mem_in m in
567
  let mem_out = mk_mem_out m in
568
  let mems =
569
    ISet.(
570
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
571
  in
572
  let insts =
573
    IMap.(
574
      diff
575
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
576
        t.tinst_footprint)
577
  in
578
  let memories =
579
    List.map
580
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
581
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
582
  in
583
  let mems_empty = ISet.is_empty mems in
584
  let insts_empty = IMap.is_empty insts in
585
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
586
  let tr ?mems ?insts () =
587
    Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
588
      (vdecls_to_vals t.tvars)
589
  in
590
  if not (mems_empty && insts_empty) then
591
    pp_acsl
592
      (pp_lemma pp_transition_footprint
593
         (pp_forall
594
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
595
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
596
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
597
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
598
                else pp_forall (pp_locals m))
599
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
600
      fmt
601
      ( t,
602
        ( (m.mname.node_id, [ mem_in; mem_out ]),
603
          ( instances,
604
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
605
      )
606

    
607
let pp_transition_footprint_lemmas fmt m =
608
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
609
    (pp_transition_footprint_lemma m)
610
    fmt
611
    (List.filter
612
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
613
       m.mspec.mtransitions)
614

    
615
let pp_initialization_def fmt m =
616
  if not (fst (get_stateless_status m)) then
617
    let name = m.mname.node_id in
618
    let mem_in = mk_mem_in m in
619
    pp_acsl
620
      (pp_predicate
621
         (pp_initialization (pp_machine_decl' ~ghost:true))
622
         (pp_and_l (fun fmt (i, (td, _)) ->
623
              if Arrow.td_is_arrow td then
624
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
625
              else
626
                pp_equal
627
                  (pp_reset_flag ~indirect:false pp_access')
628
                  pp_print_int fmt
629
                  ((mem_in, i), 1))))
630
      fmt
631
      ((name, (name, mem_in)), m.minstances)
632

    
633
let pp_reset_cleared_def fmt m =
634
  if not (fst (get_stateless_status m)) then
635
    let name = m.mname.node_id in
636
    let mem_in = mk_mem_in m in
637
    let mem_out = mk_mem_out m in
638
    pp_acsl
639
      (pp_predicate
640
         (pp_reset_cleared
641
            (pp_machine_decl' ~ghost:true)
642
            (pp_machine_decl' ~ghost:true))
643
         (pp_ite
644
            (pp_reset_flag' ~indirect:false)
645
            (pp_and
646
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
647
               pp_initialization')
648
            (pp_equal pp_print_string pp_print_string)))
649
      fmt
650
      ( (name, (name, mem_in), (name, mem_out)),
651
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
652

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

    
655
let label_pre = "Pre"
656

    
657
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
658

    
659
let pp_register_chain ?(indirect = true) ptr =
660
  pp_print_list
661
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
662
    ~pp_epilogue:(fun fmt () ->
663
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
664
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
665
    (fun fmt (i, _) -> pp_print_string fmt i)
666

    
667
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
668
  pp_print_list
669
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
670
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
671
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
672
    (fun fmt (i, _) -> pp_print_string fmt i)
673
    fmt mems
674

    
675
let pp_arrow_reset_ghost mem fmt inst =
676
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
677

    
678
module GhostProto : MODIFIERS_GHOST_PROTO = struct
679
  let pp_ghost_parameters ?(cut = true) fmt vs =
680
    fprintf fmt "%a%a"
681
      (if cut then pp_print_cut else pp_print_nothing)
682
      ()
683
      (pp_acsl_line'
684
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
685
      vs
686
end
687

    
688
module HdrMod = struct
689
  module GhostProto = GhostProto
690

    
691
  let print_machine_decl_prefix _ _ = ()
692

    
693
  let pp_import_arrow fmt () =
694
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
695
      (Arrow.arrow_top_decl ()).top_decl_owner
696
      (if !Options.cpp then "pp" else "")
697
end
698

    
699
module SrcMod = struct
700
  module GhostProto = GhostProto
701

    
702
  let pp_predicates (* dependencies *) fmt machines =
703
    let pp_preds comment pp =
704
      pp_print_list ~pp_open_box:pp_open_vbox0
705
        ~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut
706
    in
707
    fprintf fmt "%a%a%a%a%a%a"
708
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
709
      machines
710
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
711
      machines
712
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
713
      machines
714
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
715
      machines
716
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
717
      machines
718
      (pp_preds "/* ACSL transition memory footprints lemmas */"
719
         pp_transition_footprint_lemmas)
720
      machines
721

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

    
782
  let pp_set_reset_spec fmt self mem m =
783
    let name = m.mname.node_id in
784
    pp_acsl_cut
785
      (fun fmt () ->
786
        fprintf fmt "%a@,%a@,%a"
787
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
788
          (name, mem, self)
789
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
790
          (mem, 1)
791
          (pp_assigns pp_reset_flag')
792
          [ self; mem ])
793
      fmt ()
794

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

    
857
  let pp_ghost_instr_code m self fmt instr =
858
    match instr.instr_desc with
859
    | MStateAssign (x, v) ->
860
      fprintf fmt "@,%a"
861
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
862
        (x, v)
863
    | MResetAssign b ->
864
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
865
    | MSetReset inst ->
866
      let td, _ = List.assoc inst m.minstances in
867
      if Arrow.td_is_arrow td then
868
        fprintf fmt "@,%a;"
869
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
870
          inst
871
    | _ ->
872
      ()
873

    
874
  let pp_step_instr_spec m self mem fmt instr =
875
    fprintf fmt "%a%a"
876
      (pp_ghost_instr_code m mem)
877
      instr
878
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
879
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
880
      instr.instr_spec
881

    
882
  let pp_ghost_parameter mem fmt inst =
883
    GhostProto.pp_ghost_parameters ~cut:false fmt
884
      (match inst with
885
      | Some inst ->
886
        [ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ]
887
      | None ->
888
        [ mem, pp_print_string ])
889
end
890

    
891
(**************************************************************************)
892
(*                              MAKEFILE                                  *)
893
(**************************************************************************)
894

    
895
module MakefileMod = struct
896
  let other_targets fmt basename _nodename dependencies =
897
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
898
    (* EACSL version of library file . c *)
899
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
900
    fprintf fmt
901
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
902
       e-acsl -print -ocode %s_eacsl.c@."
903
      basename basename;
904
    fprintf fmt "@.";
905
    fprintf fmt "@.";
906

    
907
    (* EACSL version of library file . c + main .c *)
908
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename
909
      basename basename;
910
    fprintf fmt
911
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
912
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
913
      basename basename basename;
914
    (* Ugly hack to deal with eacsl bugs *)
915
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
916
      basename basename;
917
    fprintf fmt "@.";
918
    fprintf fmt "@.";
919

    
920
    (* EACSL version of binary *)
921
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
922
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
923
      basename;
924
    (* compiling instrumented lib + main *)
925
    C_backend_makefile.fprintf_dependencies fmt dependencies;
926
    fprintf fmt
927
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
928
       %s_main_eacsl.o %a@."
929
      basename
930
      (Utils.fprintf_list ~sep:" " (fun fmt dep ->
931
           Format.fprintf fmt "%s.o" dep.name))
932
      (C_backend_makefile.compiled_dependencies dependencies)
933
      ("${FRAMACEACSL}/e_acsl.c "
934
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
935
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
936
      basename
937
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
938
      (C_backend_makefile.lib_dependencies dependencies);
939
    fprintf fmt "@."
940
end
941

    
942
(* Local Variables: *)
943
(* compile-command:"make -C ../../.." *)
944
(* End: *)
(8-8/9)