Project

General

Profile

Download (30.2 KB) Statistics
| Branch: | Tag: | Revision:
1

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

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

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

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

    
27
(* TODO ACSL
28
   Return updates machines (eg with local annotations) and acsl preamble *)
29
let preprocess_acsl machines = machines, []
30
                          
31
let pp_acsl_basic_type_desc t_desc =
32
  if Types.is_bool_type t_desc then
33
    (* if !Options.cpp then "bool" else "_Bool" *)
34
    "_Bool"
35
  else if Types.is_int_type t_desc then
36
    (* !Options.int_type *)
37
    "integer"
38
  else if Types.is_real_type t_desc then
39
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
40
  else
41
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
42

    
43
let pp_acsl pp fmt =
44
  fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
45

    
46
let pp_acsl_cut pp fmt =
47
  fprintf fmt "%a@," (pp_acsl pp)
48

    
49
let pp_acsl_line pp fmt =
50
  fprintf fmt "//%@ @[<h>%a@]" pp
51

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

    
55
let pp_ensures pp_ens fmt =
56
  fprintf fmt "ensures %a;" pp_ens
57

    
58
let pp_assumes pp_asm fmt =
59
  fprintf fmt "assumes %a;" pp_asm
60

    
61
let pp_assigns pp =
62
  pp_comma_list
63
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
64
    ~pp_epilogue:pp_print_semicolon'
65
    pp
66

    
67
let pp_ghost pp_gho fmt =
68
  fprintf fmt "ghost %a" pp_gho
69

    
70
let pp_assert pp_ast fmt =
71
  fprintf fmt "assert %a;" pp_ast
72

    
73
let pp_mem_valid pp_var fmt (name, var) =
74
  fprintf fmt "%s_valid(%a)" name pp_var var
75

    
76
let pp_mem_valid' = pp_mem_valid pp_print_string
77

    
78
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
79
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
80

    
81
let pp_indirect' = pp_indirect pp_print_string pp_print_string
82

    
83
let pp_access pp_stru pp_field fmt (stru, field) =
84
  fprintf fmt "%a.%a" pp_stru stru pp_field field
85

    
86
let pp_access' = pp_access pp_print_string pp_print_string
87

    
88
let pp_inst self fmt (name, _) =
89
  pp_indirect' fmt (self, name)
90

    
91
let pp_var_decl fmt v =
92
  pp_print_string fmt v.var_id
93

    
94
let pp_reg self fmt field =
95
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
96

    
97
let pp_true fmt () =
98
  pp_print_string fmt "\\true"
99

    
100
let pp_false fmt () =
101
  pp_print_string fmt "\\false"
102

    
103
let pp_at pp_v fmt (v, l) =
104
  fprintf fmt "\\at(%a, %s)" pp_v v l
105

    
106
let instances machines m =
107
  let open List in
108
  let grow paths i td mems =
109
    match paths with
110
    | [] -> [[i, (td, mems)]]
111
    | _ -> map (cons (i, (td, mems))) paths
112
  in
113
  let rec aux paths m =
114
    map (fun (i, (td, _)) ->
115
        try
116
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
117
          aux (grow paths i td m.mmemory) m
118
        with Not_found -> grow paths i td [])
119
      m.minstances |> flatten
120
  in
121
  aux [] m |> map rev
122

    
123
let memories insts =
124
  List.(map (fun path ->
125
      let _, (_, mems) = hd (rev path) in
126
      map (fun mem -> path, mem) mems) insts |> flatten)
127

    
128
let pp_instance ?(indirect=true) ptr =
129
  pp_print_list
130
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
131
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
132
    (fun fmt (i, _) -> pp_print_string fmt i)
133

    
134
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
135
  pp_access
136
    ((if indirect then pp_indirect else pp_access)
137
       (pp_instance ~indirect ptr) pp_print_string)
138
    pp_var_decl
139
    fmt ((path, "_reg"), mem)
140

    
141
let prefixes l =
142
  let rec pref acc = function
143
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
144
    | [] -> acc
145
  in
146
  pref [] (List.rev l)
147

    
148
let powerset_instances paths =
149
  List.map prefixes paths |> List.flatten
150

    
151
let pp_separated self mem fmt (paths, ptrs) =
152
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
153
    self
154
    mem
155
    (pp_comma_list
156
       ~pp_prologue:pp_print_comma'
157
       (pp_instance self))
158
    paths
159
    (pp_comma_list
160
       ~pp_prologue:pp_print_comma'
161
       pp_var_decl)
162
    ptrs
163

    
164
let pp_separated' =
165
  pp_comma_list
166
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
167
    ~pp_epilogue:pp_print_cpar
168
    pp_var_decl
169

    
170
let pp_par pp fmt =
171
  fprintf fmt "(%a)" pp
172

    
173
let pp_forall pp_l pp_r fmt (l, r) =
174
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
175
    pp_l l
176
    pp_r r
177

    
178
let pp_exists pp_l pp_r fmt (l, r) =
179
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
180
    pp_l l
181
    pp_r r
182

    
183
let pp_equal pp_l pp_r fmt (l, r) =
184
  fprintf fmt "%a == %a"
185
    pp_l l
186
    pp_r r
187

    
188
let pp_different pp_l pp_r fmt (l, r) =
189
  fprintf fmt "%a != %a"
190
    pp_l l
191
    pp_r r
192

    
193
let pp_implies pp_l pp_r fmt (l, r) =
194
  fprintf fmt "@[<v>%a ==>@ %a@]"
195
    pp_l l
196
    pp_r r
197

    
198
let pp_and pp_l pp_r fmt (l, r) =
199
  fprintf fmt "@[<v>%a @ && %a@]"
200
    pp_l l
201
    pp_r r
202

    
203
let pp_and_l pp_v fmt =
204
  pp_print_list
205
    ~pp_open_box:pp_open_vbox0
206
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
207
    pp_v
208
    fmt
209

    
210
let pp_or pp_l pp_r fmt (l, r) =
211
  fprintf fmt "@[<v>%a @ || %a@]"
212
    pp_l l
213
    pp_r r
214

    
215
let pp_or_l pp_v fmt =
216
  pp_print_list
217
    ~pp_open_box:pp_open_vbox0
218
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
219
    pp_v
220
    fmt
221

    
222
let pp_not pp fmt =
223
  fprintf fmt "!%a" pp
224

    
225
let pp_valid pp =
226
  pp_and_l
227
  (* pp_print_list *)
228
    (* ~pp_sep:pp_print_cut *)
229
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
230

    
231
let pp_old pp fmt =
232
  fprintf fmt "\\old(%a)" pp
233

    
234
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
235
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
236
    pp_c c
237
    pp_t t
238
    pp_f f
239

    
240
let pp_paren pp fmt v =
241
  fprintf fmt "(%a)" pp v
242

    
243
let pp_initialization pp_mem fmt (name, mem) =
244
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
245

    
246
let pp_initialization' = pp_initialization pp_print_string
247

    
248
let pp_locals m =
249
  pp_comma_list
250
    ~pp_open_box:pp_open_hbox
251
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
252

    
253
let pp_ptr_decl fmt v =
254
  pp_ptr fmt v.var_id
255

    
256
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
257
  if Types.is_real_type typ && !Options.mpfr
258
  then
259
    assert false
260
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
261
  else
262
    pp_equal pp_l pp_r fmt (var_name, value)
263

    
264
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
265
    (var_type, var_name, value) =
266
  let depth = expansion_depth value in
267
  let loop_vars = mk_loop_variables m var_type depth in
268
  let reordered_loop_vars = reorder_loop_variables loop_vars in
269
  let rec aux typ fmt vars =
270
    match vars with
271
    | [] ->
272
      pp_basic_assign_spec
273
        (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars pp_var_l)
274
        (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars pp_var_r)
275
        fmt typ var_name value
276
    | (_d, LVar _i) :: _q ->
277
      assert false
278
      (* let typ' = Types.array_element_type typ in
279
       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
280
       *   i i i pp_c_dimension d i
281
       *   (aux typ') q *)
282
    | (_d, LInt _r) :: _q ->
283
      assert false
284
      (* let typ' = Types.array_element_type typ in
285
       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
286
       * fprintf fmt "@[<v 2>{@,%a@]@,}"
287
       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
288
    | _ -> assert false
289
  in
290
  begin
291
    reset_loop_counter ();
292
    aux var_type fmt reordered_loop_vars;
293
  end
294

    
295
let pp_c_var_read m fmt id =
296
  (* mpfr_t is a static array, not treated as general arrays *)
297
  if Types.is_address_type id.var_type
298
  then
299
    if is_memory m id
300
    && not (Types.is_real_type id.var_type && !Options.mpfr)
301
    then fprintf fmt "(*%s)" id.var_id
302
    else fprintf fmt "%s" id.var_id
303
  else
304
    fprintf fmt "%s" id.var_id
305

    
306
let pp_nothing fmt () =
307
  pp_print_string fmt "\\nothing"
308

    
309
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
310
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])"
311
    name
312
    (pp_print_option pp_print_int) i
313
    pp_mem mem
314
    pp_self self
315

    
316
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
317
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
318
    (mp.mpname.node_id, mem, self)
319

    
320
let pp_memory_pack_aux' ?i fmt =
321
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
322
let pp_memory_pack' fmt =
323
  pp_memory_pack pp_print_string pp_print_string fmt
324

    
325
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
326
    (name, inputs, locals, outputs, mem_in, mem_out) =
327
  let stateless = fst (get_stateless_status m) in
328
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
329
    name
330
    (pp_print_option pp_print_int) i
331
    (fun fmt -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in)
332
    (pp_comma_list pp_input) inputs
333
    (pp_print_option (fun fmt _ ->
334
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
335
    i
336
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
337
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs
338

    
339
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
340
    (t, mem_in, mem_out) =
341
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
342
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
343

    
344
let pp_transition_aux' ?i m =
345
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
346
let pp_transition_aux'' ?i m =
347
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
348
let pp_transition' m =
349
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
350
let pp_transition'' m =
351
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
352

    
353
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
354
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])"
355
    name
356
    pp_mem_in mem_in
357
    pp_mem_out mem_out
358

    
359
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
360

    
361
module PrintSpec = struct
362

    
363
  let pp_reg pp_mem fmt = function
364
    | ResetFlag ->
365
      fprintf fmt "%t_reset" pp_mem
366
    | StateVar x ->
367
      fprintf fmt "%t%a" pp_mem pp_var_decl x
368

    
369
  let pp_expr:
370
    type a. machine_t -> (formatter -> unit) -> formatter -> (value_t, a) expression_t -> unit =
371
    fun m pp_mem fmt -> function
372
    | Val v -> pp_val m fmt v
373
    | Tag t -> pp_print_string fmt t
374
    | Var v -> pp_var_decl fmt v
375
    | Memory r -> pp_reg pp_mem fmt r
376

    
377
  let pp_predicate m mem_in mem_in' mem_out mem_out' fmt p =
378
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
379
      fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
380
    in
381
    match p with
382
    | Transition (f, inst, i, inputs, locals, outputs) ->
383
      let pp_mem_in, pp_mem_out = match inst with
384
        | None ->
385
          pp_print_string, pp_print_string
386
        | Some inst ->
387
          (fun fmt mem_in -> pp_access' fmt (mem_in, inst)),
388
          (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
389
      in
390
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr pp_expr fmt
391
        (f, inputs, locals, outputs, mem_in', mem_out')
392
    | MemoryPack (f, inst, i) ->
393
      let pp_mem, pp_self = match inst with
394
        | None ->
395
          pp_print_string, pp_print_string
396
        | Some inst ->
397
          (fun fmt mem -> pp_access' fmt (mem, inst)),
398
          (fun fmt self -> pp_indirect' fmt (self, inst))
399
      in
400
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
401
    | ResetCleared f ->
402
      pp_reset_cleared' fmt (f, mem_in, mem_out)
403
      (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
404
    | Initialization -> ()
405

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

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

    
415
  type mode =
416
    | MemoryPackMode
417
    | TransitionMode
418
    | ResetIn
419
    | ResetOut
420
    | InstrMode of ident
421

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

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

    
509
end
510

    
511
let pp_predicate pp_l pp_r fmt (l, r) =
512
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
513
    pp_l l
514
    pp_r r
515

    
516
let print_machine_valid_predicate fmt m =
517
  if not (fst (get_stateless_status m)) then
518
    let name = m.mname.node_id in
519
    let self = mk_self m in
520
    pp_acsl
521
      (pp_predicate
522
         (pp_mem_valid (pp_machine_decl pp_ptr))
523
         (pp_and
524
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
525
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
526
            (pp_valid pp_print_string)))
527
      fmt
528
      ((name, (name, self)),
529
       (m.minstances, [self]))
530

    
531

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

    
544
let print_machine_ghost_struct fmt m =
545
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
546

    
547
let pp_memory_pack_defs fmt m =
548
  if not (fst (get_stateless_status m)) then
549
    fprintf fmt "%a@,%a"
550
      print_machine_ghost_struct m
551
      (pp_print_list
552
         ~pp_epilogue:pp_print_cut
553
         ~pp_open_box:pp_open_vbox0
554
         (pp_memory_pack_def m)) m.mspec.mmemory_packs
555

    
556
let pp_transition_def m fmt t =
557
  let name = t.tname.node_id in
558
  let mem_in = mk_mem_in m in
559
  let mem_out = mk_mem_out m in
560
  pp_acsl
561
    (pp_predicate
562
       (pp_transition m
563
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
564
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
565
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
566
       (PrintSpec.pp_spec TransitionMode m))
567
    fmt
568
    ((t, (name, mem_in), (name, mem_out)),
569
     t.tformula)
570

    
571
(* let print_trans_simulation dependencies m fmt (i, instr) =
572
 *   let mem_in = mk_mem_in m in
573
 *   let mem_out = mk_mem_out m in
574
 *   let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
575
 *                    (live_i m (i+1))) in
576
 *   (\* XXX *\)
577
 *   (\* printf "%d : %a\n%d : %a\nocc: %a\n\n"
578
 *    *   i
579
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
580
 *    *   (i+1)
581
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
582
 *    *   (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *\)
583
 *   let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
584
 *   let pred pp v =
585
 *     let vars = VDSet.(union (of_list m.mstep.step_locals)
586
 *                         (of_list m.mstep.step_outputs)) in
587
 *     let locals = VDSet.(inter vars d |> elements) in
588
 *     if locals = []
589
 *     then pp_and prev_trans pp fmt ((), v)
590
 *     else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
591
 *   in
592
 *   let rec aux fmt instr = match instr.instr_desc with
593
 *     | MLocalAssign (x, v)
594
 *     | MStateAssign (x, v) ->
595
 *       pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
596
 *         (x.var_type, mk_val (Var x) x.var_type, v)
597
 *     | MStep ([i0], i, vl)
598
 *       when Basic_library.is_value_internal_fun
599
 *           (mk_val (Fun (i, vl)) i0.var_type)  ->
600
 *       pp_true fmt ()
601
 *     | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
602
 *       pp_true fmt ()
603
 *     | MStep ([_], i, _) when has_c_prototype i dependencies ->
604
 *       pp_true fmt ()
605
 *     | MStep (xs, i, ys) ->
606
 *       begin try
607
 *           let n, _ = List.assoc i m.minstances in
608
 *           pp_mem_trans_aux
609
 *             (fst (get_stateless_status_top_decl n))
610
 *             pp_access' pp_access'
611
 *             (pp_c_val m mem_in (pp_c_var_read m))
612
 *             pp_var_decl
613
 *             fmt
614
 *             (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
615
 *         with Not_found -> pp_true fmt ()
616
 *       end
617
 *     | MReset i ->
618
 *       begin try
619
 *           let n, _ = List.assoc i m.minstances in
620
 *           pp_mem_init' fmt (node_name n, mem_out)
621
 *         with Not_found -> pp_true fmt ()
622
 *       end
623
 *     | MBranch (v, brs) ->
624
 *       if let t = fst (List.hd brs) in t = tag_true || t = tag_false
625
 *       then (\* boolean case *\)
626
 *         pp_ite (pp_c_val m mem_in (pp_c_var_read m))
627
 *           (fun fmt () ->
628
 *              match List.assoc tag_true brs with
629
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
630
 *              | []
631
 *              | exception Not_found -> pp_true fmt ())
632
 *           (fun fmt () ->
633
 *              match List.assoc tag_false brs with
634
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
635
 *              | []
636
 *              | exception Not_found -> pp_true fmt ())
637
 *           fmt (v, (), ())
638
 *       else (\* enum type case *\)
639
 *       pp_and_l (fun fmt (l, instrs) ->
640
 *             let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
641
 *             pp_paren (pp_implies
642
 *                         (pp_equal pp_val pp_c_tag)
643
 *                         (pp_and_l aux))
644
 *               fmt
645
 *               ((v, l), instrs))
646
 *         fmt brs
647
 *     | _ -> pp_true fmt ()
648
 *   in
649
 *   pred aux instr *)
650

    
651
(* let print_machine_trans_simulation dependencies m fmt i instr =
652
 *   print_machine_trans_simulation_aux m
653
 *     (print_trans_simulation dependencies m)
654
 *     ~i:(i+1)
655
 *     fmt (i, instr) *)
656

    
657
let pp_transition_defs fmt m =
658
  (* set_live_of m; *)
659
  (* let i = List.length m.mstep.step_instrs in *)
660
  (* let mem_in = mk_mem_in m in
661
   * let mem_out = mk_mem_out m in *)
662
  (* let last_trans fmt () =
663
   *   let locals = VDSet.(inter
664
   *                         (of_list m.mstep.step_locals)
665
   *                         (live_i m i)
666
   *                       |> elements) in
667
   *   if locals = []
668
   *   then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
669
   *   else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
670
   *       (locals, (m, mem_in, mem_out))
671
   * in *)
672
  fprintf fmt "%a"
673
    (pp_print_list
674
       ~pp_epilogue:pp_print_cut
675
       ~pp_open_box:pp_open_vbox0
676
       (pp_transition_def m)) m.mspec.mtransitions
677

    
678
let print_machine_init_predicate fmt m =
679
  if not (fst (get_stateless_status m)) then
680
    let name = m.mname.node_id in
681
    let mem_in = mk_mem_in m in
682
    pp_acsl
683
      (pp_predicate
684
         (pp_initialization (pp_machine_decl' ~ghost:true))
685
         (pp_and_l (fun fmt (i, (td, _)) ->
686
              pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
687
      fmt
688
      ((name, (name, mem_in)), m.minstances)
689

    
690
let pp_at pp_p fmt (p, l) =
691
  fprintf fmt "\\at(%a, %s)" pp_p p l
692

    
693
let label_pre = "Pre"
694

    
695
let pp_at_pre pp_p fmt p =
696
  pp_at pp_p fmt (p, label_pre)
697

    
698
let pp_register ?(indirect=true) ptr =
699
  pp_print_list
700
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
701
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
702
                     (if indirect then "->" else "."))
703
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
704
    (fun fmt (i, _) -> pp_print_string fmt i)
705

    
706
let pp_reset_flag ?(indirect=true) ptr fmt mems =
707
  pp_print_list
708
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
709
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reset"
710
                     (if indirect then "->" else "."))
711
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
712
    (fun fmt (i, _) -> pp_print_string fmt i)
713
    fmt mems
714

    
715
module GhostProto: MODIFIERS_GHOST_PROTO = struct
716
  let pp_ghost_parameters fmt vs =
717
    fprintf fmt "@;%a"
718
      (pp_acsl (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
719
      vs
720
end
721

    
722
module HdrMod = struct
723

    
724
  module GhostProto = GhostProto
725

    
726
  let print_machine_decl_prefix = fun _ _ -> ()
727

    
728
  let pp_import_standard_spec fmt () =
729
    fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
730
      (Arrow.arrow_top_decl ()).top_decl_owner
731
      (if !Options.cpp then "pp" else "")
732

    
733
end
734

    
735
module SrcMod = struct
736

    
737
  module GhostProto = GhostProto
738

    
739
  let pp_predicates (* dependencies *) fmt machines =
740
    fprintf fmt
741
      "%a%a%a%a"
742
      (pp_print_list
743
         ~pp_open_box:pp_open_vbox0
744
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
745
         print_machine_valid_predicate
746
         ~pp_epilogue:pp_print_cutcut) machines
747
      (pp_print_list
748
         ~pp_open_box:pp_open_vbox0
749
         ~pp_sep:pp_print_cutcut
750
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
751
         pp_memory_pack_defs
752
         ~pp_epilogue:pp_print_cutcut) machines
753
      (pp_print_list
754
         ~pp_open_box:pp_open_vbox0
755
         ~pp_sep:pp_print_cutcut
756
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
757
         print_machine_init_predicate
758
         ~pp_epilogue:pp_print_cutcut) machines
759
      (pp_print_list
760
         ~pp_open_box:pp_open_vbox0
761
         ~pp_sep:pp_print_cutcut
762
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
763
         pp_transition_defs
764
         ~pp_epilogue:pp_print_cutcut) machines
765

    
766
  let pp_clear_reset_spec fmt machines self mem m =
767
    let name = m.mname.node_id in
768
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
769
        m.minstances in
770
    let mk_insts = List.map (fun x -> [x]) in
771
    pp_acsl_cut (fun fmt () ->
772
        fprintf fmt
773
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
774
          @[<v 2>behavior reset:@;\
775
          %a@,%a@]@,\
776
          @[<v 2>behavior no_reset:@;\
777
          %a@,%a@]"
778
          (pp_requires pp_mem_valid') (name, self)
779
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
780
          (pp_ensures (pp_memory_pack_aux
781
                         ~i:(List.length m.mspec.mmemory_packs - 2)
782
                         pp_ptr pp_print_string))
783
          (name, mem, self)
784
          (pp_assigns pp_indirect') [self, "_reset"]
785
          (pp_assigns (pp_register self)) (mk_insts arws)
786
          (pp_assigns (pp_reset_flag self)) (mk_insts narws)
787
          (pp_assigns pp_indirect') [mem, "_reset"]
788
          (pp_assigns (pp_register ~indirect:false mem)) (mk_insts arws)
789
          (pp_assigns (pp_reset_flag ~indirect:false mem)) (mk_insts narws)
790
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 1)
791
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
792
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 0)
793
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
794
      )
795
      fmt ()
796

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

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

    
848
  let pp_step_instr_spec m self fmt instr =
849
    fprintf fmt "@,%a"
850
      (pp_print_list ~pp_open_box:pp_open_vbox0
851
         (pp_acsl (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
852
      instr.instr_spec
853

    
854
  let pp_ghost_set_reset_spec fmt =
855
    fprintf fmt "@;%a@;"
856
      (pp_acsl_line
857
         (pp_ghost
858
            (fun fmt mem -> fprintf fmt "%a = 1;" pp_indirect' (mem, "_reset"))))
859
end
860

    
861
(**************************************************************************)
862
(*                              MAKEFILE                                  *)
863
(**************************************************************************)
864

    
865
module MakefileMod = struct
866

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

    
877
    (* EACSL version of library file . c + main .c  *)
878
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
879
    fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."
880
      basename basename basename;
881
    (* Ugly hack to deal with eacsl bugs *)
882
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
883
    fprintf fmt "@.";
884
    fprintf fmt "@.";
885

    
886
    (* EACSL version of binary *)
887
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
888
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
889
    C_backend_makefile.fprintf_dependencies fmt dependencies;
890
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
891
      basename
892
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
893
      (C_backend_makefile.compiled_dependencies dependencies)
894
      ("${FRAMACEACSL}/e_acsl.c "
895
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
896
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
897
      basename
898
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
899
      (C_backend_makefile.lib_dependencies dependencies)
900
    ;
901
    fprintf fmt "@."
902

    
903
end
904

    
905
(* Local Variables: *)
906
(* compile-command:"make -C ../../.." *)
907
(* End: *)
(8-8/9)