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
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_input pp_output fmt
262
    (name, inputs, locals, outputs, mem_in, mem_out) =
263
  let stateless = fst (get_stateless_status m) in
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" 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_input)
271
    inputs
272
    (pp_print_option (fun fmt _ ->
273
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
274
    i
275
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
276
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
277
    outputs
278

    
279
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
280
    (t, mem_in, mem_out) =
281
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
282
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
283

    
284
let pp_transition_aux' ?i m =
285
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
286

    
287
let pp_transition_aux'' ?i m =
288
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
289

    
290
let pp_transition' m =
291
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
292

    
293
let pp_transition'' m =
294
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
295

    
296
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
297
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
298
    pp_mem_out mem_out
299

    
300
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
301

    
302
let pp_functional_update mems insts fmt mem =
303
  let rec aux fmt = function
304
    | [] ->
305
      pp_print_string fmt mem
306
    | (x, is_mem) :: fields ->
307
      fprintf fmt "{ @[<hov>%a@ \\with .%s%s = %s@] }" aux fields
308
        (if is_mem then "_reg." else "")
309
        x x
310
  in
311
  aux fmt
312
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
313
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
314

    
315
module PrintSpec = struct
316
  type mode =
317
    | MemoryPackMode
318
    | TransitionMode
319
    | TransitionFootprintMode
320
    | ResetIn
321
    | ResetOut
322
    | InstrMode of ident
323

    
324
  let pp_reg mem fmt = function
325
    | ResetFlag ->
326
      fprintf fmt "%s.%s" mem reset_flag_name
327
    | StateVar x ->
328
      fprintf fmt "%s.%a" mem pp_var_decl x
329

    
330
  let pp_expr :
331
      type a.
332
      ?output:bool ->
333
      machine_t ->
334
      ident ->
335
      formatter ->
336
      (value_t, a) expression_t ->
337
      unit =
338
   fun ?(output = false) m mem fmt -> function
339
    | Val v ->
340
      pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
341
    | Tag t ->
342
      pp_print_string fmt t
343
    | Var v ->
344
      pp_var_decl fmt v
345
    | Memory r ->
346
      pp_reg mem fmt r
347

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

    
401
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
402

    
403
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
404
    | Val v ->
405
      v
406
    | Tag t ->
407
      id_to_tag t
408
    | Var v ->
409
      vdecl_to_val v
410
    | Memory (StateVar v) ->
411
      vdecl_to_val v
412
    | Memory ResetFlag ->
413
      vdecl_to_val reset_flag
414

    
415
  let find_arrow m =
416
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
417
    with Not_found ->
418
      eprintf "Internal error: arrow not found";
419
      raise Not_found
420

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

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

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

    
512
let pp_mem_valid_def fmt m =
513
  if not (fst (get_stateless_status m)) then
514
    let name = m.mname.node_id in
515
    let self = mk_self m in
516
    pp_acsl
517
      (pp_predicate
518
         (pp_mem_valid (pp_machine_decl pp_ptr))
519
         (pp_and
520
            (pp_and_l (fun fmt (inst, (td, _)) ->
521
                 if Arrow.td_is_arrow td then
522
                   pp_valid pp_indirect' fmt [ self, inst ]
523
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
524
            (pp_valid pp_print_string)))
525
      fmt
526
      ((name, (name, self)), (m.minstances, [ self ]))
527

    
528
let pp_memory_pack_def m fmt mp =
529
  let name = mp.mpname.node_id in
530
  let self = mk_self m in
531
  let mem = mk_mem m in
532
  pp_acsl
533
    (pp_predicate
534
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
535
       (PrintSpec.pp_spec MemoryPackMode m))
536
    fmt
537
    ((mp, (name, mem), (name, self)), mp.mpformula)
538

    
539
let print_machine_ghost_struct fmt m =
540
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
541

    
542
let pp_memory_pack_defs fmt m =
543
  if not (fst (get_stateless_status m)) then
544
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
545
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
546
         (pp_memory_pack_def m))
547
      m.mspec.mmemory_packs
548

    
549
let pp_transition_def m fmt t =
550
  let name = t.tname.node_id in
551
  let mem_in = mk_mem_in m in
552
  let mem_out = mk_mem_out m in
553
  pp_acsl
554
    (pp_predicate
555
       (pp_transition m
556
          (pp_machine_decl' ~ghost:true)
557
          (pp_machine_decl' ~ghost:true)
558
          (pp_local m) (pp_local m))
559
       (PrintSpec.pp_spec TransitionMode m))
560
    fmt
561
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
562

    
563
let pp_transition_defs fmt m =
564
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
565
    (pp_transition_def m) fmt m.mspec.mtransitions
566

    
567
let pp_transition_footprint fmt t =
568
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
569
    (pp_print_option pp_print_int)
570
    t.tindex
571

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

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

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

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

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

    
666
let label_pre = "Pre"
667

    
668
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
669

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

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

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

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

    
699
module HdrMod = struct
700
  module GhostProto = GhostProto
701

    
702
  let print_machine_decl_prefix _ _ = ()
703

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

    
710
module SrcMod = struct
711
  module GhostProto = GhostProto
712

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

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

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

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

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

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

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

    
902
(**************************************************************************)
903
(*                              MAKEFILE                                  *)
904
(**************************************************************************)
905

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

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

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

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