Project

General

Profile

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

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

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

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

    
25
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 fmt mem =
303
  let rec aux fmt mems =
304
    match mems with
305
    | [] ->
306
      pp_print_string fmt mem
307
    | x :: mems ->
308
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
309
  in
310
  aux fmt
311
    (* if Utils.ISet.is_empty mems then
312
     *   pp_print_string fmt mem
313
     *     else
314
     *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
315
     *     mem
316
     *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
317
     *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
318
    (Utils.ISet.elements mems)
319

    
320
module PrintSpec = struct
321
  type mode =
322
    | MemoryPackMode
323
    | TransitionMode
324
    | TransitionFootprintMode
325
    | ResetIn
326
    | ResetOut
327
    | InstrMode of ident
328

    
329
  let pp_reg mem fmt = function
330
    | ResetFlag ->
331
      fprintf fmt "%s.%s" mem reset_flag_name
332
    | StateVar x ->
333
      fprintf fmt "%s.%a" mem pp_var_decl x
334

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

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

    
405
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
406

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

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

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

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

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

    
525
let pp_mem_valid_def fmt m =
526
  if not (fst (get_stateless_status m)) then
527
    let name = m.mname.node_id in
528
    let self = mk_self m in
529
    pp_acsl
530
      (pp_predicate
531
         (pp_mem_valid (pp_machine_decl pp_ptr))
532
         (pp_and
533
            (pp_and_l (fun fmt (inst, (td, _)) ->
534
                 if Arrow.td_is_arrow td then
535
                   pp_valid pp_indirect' fmt [ self, inst ]
536
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
537
            (pp_valid pp_print_string)))
538
      fmt
539
      ((name, (name, self)), (m.minstances, [ self ]))
540

    
541
let pp_memory_pack_def m fmt mp =
542
  let name = mp.mpname.node_id in
543
  let self = mk_self m in
544
  let mem = mk_mem m in
545
  pp_acsl
546
    (pp_predicate
547
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
548
       (PrintSpec.pp_spec MemoryPackMode m))
549
    fmt
550
    ((mp, (name, mem), (name, self)), mp.mpformula)
551

    
552
let print_machine_ghost_struct fmt m =
553
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
554

    
555
let pp_memory_pack_defs fmt m =
556
  if not (fst (get_stateless_status m)) then
557
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
558
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
559
         (pp_memory_pack_def m))
560
      m.mspec.mmemory_packs
561

    
562
let pp_transition_def m fmt t =
563
  let name = t.tname.node_id in
564
  let mem_in = mk_mem_in m in
565
  let mem_out = mk_mem_out m in
566
  pp_acsl
567
    (pp_predicate
568
       (pp_transition m
569
          (pp_machine_decl' ~ghost:true)
570
          (pp_machine_decl' ~ghost:true)
571
          (pp_local m) (pp_local m))
572
       (PrintSpec.pp_spec TransitionMode m))
573
    fmt
574
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
575

    
576
let pp_transition_defs fmt m =
577
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
578
    (pp_transition_def m) fmt m.mspec.mtransitions
579

    
580
let pp_transition_footprint fmt t =
581
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
582
    (pp_print_option pp_print_int)
583
    t.tindex
584

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

    
612
let pp_transition_footprint_lemmas fmt m =
613
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
614
    (pp_transition_footprint_lemma m)
615
    fmt
616
    (List.filter
617
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
618
       m.mspec.mtransitions)
619

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

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

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

    
660
let label_pre = "Pre"
661

    
662
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
663

    
664
let pp_register_chain ?(indirect = true) ptr =
665
  pp_print_list
666
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
667
    ~pp_epilogue:(fun fmt () ->
668
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
669
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
670
    (fun fmt (i, _) -> pp_print_string fmt i)
671

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

    
680
let pp_arrow_reset_ghost mem fmt inst =
681
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
682

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

    
693
module HdrMod = struct
694
  module GhostProto = GhostProto
695

    
696
  let print_machine_decl_prefix _ _ = ()
697

    
698
  let pp_import_arrow fmt () =
699
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
700
      (Arrow.arrow_top_decl ()).top_decl_owner
701
      (if !Options.cpp then "pp" else "")
702
end
703

    
704
module SrcMod = struct
705
  module GhostProto = GhostProto
706

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

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

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

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

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

    
879
  let pp_step_instr_spec m self mem fmt instr =
880
    fprintf fmt "%a%a"
881
      (pp_ghost_instr_code m mem)
882
      instr
883
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
884
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
885
      instr.instr_spec
886

    
887
  let pp_ghost_parameter mem fmt inst =
888
    GhostProto.pp_ghost_parameters ~cut:false fmt
889
      (match inst with
890
      | Some inst ->
891
        [ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ]
892
      | None ->
893
        [ mem, pp_print_string ])
894
end
895

    
896
(**************************************************************************)
897
(*                              MAKEFILE                                  *)
898
(**************************************************************************)
899

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

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

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

    
947
(* Local Variables: *)
948
(* compile-command:"make -C ../../.." *)
949
(* End: *)
(8-8/9)