Project

General

Profile

Download (31.5 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_acsl_line' pp fmt =
53
  fprintf fmt "/*%@ @[<h>%a@] */" pp
54

    
55
let pp_acsl_line_cut pp fmt =
56
  fprintf fmt "%a@," (pp_acsl_line pp)
57

    
58
let pp_requires pp_req fmt =
59
  fprintf fmt "requires %a;" pp_req
60

    
61
let pp_ensures pp_ens fmt =
62
  fprintf fmt "ensures %a;" pp_ens
63

    
64
let pp_assumes pp_asm fmt =
65
  fprintf fmt "assumes %a;" pp_asm
66

    
67
let pp_assigns pp =
68
  pp_comma_list
69
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
70
    ~pp_epilogue:pp_print_semicolon'
71
    pp
72

    
73
let pp_ghost pp_gho fmt =
74
  fprintf fmt "ghost %a" pp_gho
75

    
76
let pp_assert pp_ast fmt =
77
  fprintf fmt "assert %a;" pp_ast
78

    
79
let pp_mem_valid pp_var fmt (name, var) =
80
  fprintf fmt "%s_valid(%a)" name pp_var var
81

    
82
let pp_mem_valid' = pp_mem_valid pp_print_string
83

    
84
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
85
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
86

    
87
let pp_indirect' = pp_indirect pp_print_string pp_print_string
88

    
89
let pp_access pp_stru pp_field fmt (stru, field) =
90
  fprintf fmt "%a.%a" pp_stru stru pp_field field
91

    
92
let pp_access' = pp_access pp_print_string pp_print_string
93

    
94
let pp_inst self fmt (name, _) =
95
  pp_indirect' fmt (self, name)
96

    
97
let pp_var_decl fmt v =
98
  pp_print_string fmt v.var_id
99

    
100
let pp_reg self fmt field =
101
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
102

    
103
let pp_true fmt () =
104
  pp_print_string fmt "\\true"
105

    
106
let pp_false fmt () =
107
  pp_print_string fmt "\\false"
108

    
109
let pp_at pp_v fmt (v, l) =
110
  fprintf fmt "\\at(%a, %s)" pp_v v l
111

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

    
129
let memories insts =
130
  List.(map (fun path ->
131
      let _, (_, mems) = hd (rev path) in
132
      map (fun mem -> path, mem) mems) insts |> flatten)
133

    
134
let pp_instance ?(indirect=true) ptr =
135
  pp_print_list
136
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
137
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
138
    (fun fmt (i, _) -> pp_print_string fmt i)
139

    
140
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
141
  pp_access
142
    ((if indirect then pp_indirect else pp_access)
143
       (pp_instance ~indirect ptr) pp_print_string)
144
    pp_var_decl
145
    fmt ((path, "_reg"), mem)
146

    
147
let prefixes l =
148
  let rec pref acc = function
149
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
150
    | [] -> acc
151
  in
152
  pref [] (List.rev l)
153

    
154
let powerset_instances paths =
155
  List.map prefixes paths |> List.flatten
156

    
157
let pp_separated self mem fmt (paths, ptrs) =
158
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
159
    self
160
    mem
161
    (pp_comma_list
162
       ~pp_prologue:pp_print_comma'
163
       (pp_instance self))
164
    paths
165
    (pp_comma_list
166
       ~pp_prologue:pp_print_comma'
167
       pp_var_decl)
168
    ptrs
169

    
170
let pp_separated' =
171
  pp_comma_list
172
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
173
    ~pp_epilogue:pp_print_cpar
174
    pp_var_decl
175

    
176
let pp_par pp fmt =
177
  fprintf fmt "(%a)" pp
178

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

    
184
let pp_exists pp_l pp_r fmt (l, r) =
185
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
186
    pp_l l
187
    pp_r r
188

    
189
let pp_equal pp_l pp_r fmt (l, r) =
190
  fprintf fmt "%a == %a"
191
    pp_l l
192
    pp_r r
193

    
194
let pp_different pp_l pp_r fmt (l, r) =
195
  fprintf fmt "%a != %a"
196
    pp_l l
197
    pp_r r
198

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

    
204
let pp_and pp_l pp_r fmt (l, r) =
205
  fprintf fmt "@[<v>%a @ && %a@]"
206
    pp_l l
207
    pp_r r
208

    
209
let pp_and_l pp_v fmt =
210
  pp_print_list
211
    ~pp_open_box:pp_open_vbox0
212
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
213
    pp_v
214
    fmt
215

    
216
let pp_or pp_l pp_r fmt (l, r) =
217
  fprintf fmt "@[<v>%a @ || %a@]"
218
    pp_l l
219
    pp_r r
220

    
221
let pp_or_l pp_v fmt =
222
  pp_print_list
223
    ~pp_open_box:pp_open_vbox0
224
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
225
    pp_v
226
    fmt
227

    
228
let pp_not pp fmt =
229
  fprintf fmt "!%a" pp
230

    
231
let pp_valid pp =
232
  pp_and_l
233
  (* pp_print_list *)
234
    (* ~pp_sep:pp_print_cut *)
235
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
236

    
237
let pp_old pp fmt =
238
  fprintf fmt "\\old(%a)" pp
239

    
240
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
241
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
242
    pp_c c
243
    pp_t t
244
    pp_f f
245

    
246
let pp_paren pp fmt v =
247
  fprintf fmt "(%a)" pp v
248

    
249
let pp_initialization pp_mem fmt (name, mem) =
250
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
251

    
252
let pp_initialization' = pp_initialization pp_print_string
253

    
254
let pp_locals m =
255
  pp_comma_list
256
    ~pp_open_box:pp_open_hbox
257
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
258

    
259
let pp_ptr_decl fmt v =
260
  pp_ptr fmt v.var_id
261

    
262
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
263
  if Types.is_real_type typ && !Options.mpfr
264
  then
265
    assert false
266
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
267
  else
268
    pp_equal pp_l pp_r fmt (var_name, value)
269

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

    
301
let pp_c_var_read m fmt id =
302
  (* mpfr_t is a static array, not treated as general arrays *)
303
  if Types.is_address_type id.var_type
304
  then
305
    if is_memory m id
306
    && not (Types.is_real_type id.var_type && !Options.mpfr)
307
    then fprintf fmt "(*%s)" id.var_id
308
    else fprintf fmt "%s" id.var_id
309
  else
310
    fprintf fmt "%s" id.var_id
311

    
312
let pp_nothing fmt () =
313
  pp_print_string fmt "\\nothing"
314

    
315
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
316
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])"
317
    name
318
    (pp_print_option pp_print_int) i
319
    pp_mem mem
320
    pp_self self
321

    
322
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
323
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
324
    (mp.mpname.node_id, mem, self)
325

    
326
let pp_memory_pack_aux' ?i fmt =
327
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
328
let pp_memory_pack' fmt =
329
  pp_memory_pack pp_print_string pp_print_string fmt
330

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

    
345
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
346
    (t, mem_in, mem_out) =
347
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
348
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
349

    
350
let pp_transition_aux' ?i m =
351
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
352
let pp_transition_aux'' ?i m =
353
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
354
let pp_transition' m =
355
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
356
let pp_transition'' m =
357
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
358

    
359
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
360
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])"
361
    name
362
    pp_mem_in mem_in
363
    pp_mem_out mem_out
364

    
365
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
366

    
367
module PrintSpec = struct
368

    
369
  let pp_reg pp_mem fmt = function
370
    | ResetFlag ->
371
      fprintf fmt "%t%s" pp_mem reset_flag_name
372
    | StateVar x ->
373
      fprintf fmt "%t%a" pp_mem pp_var_decl x
374

    
375
  let pp_expr:
376
    type a. machine_t -> (formatter -> unit) -> formatter -> (value_t, a) expression_t -> unit =
377
    fun m pp_mem fmt -> function
378
    | Val v -> pp_val m fmt v
379
    | Tag t -> pp_print_string fmt t
380
    | Var v -> pp_var_decl fmt v
381
    | Memory r -> pp_reg pp_mem fmt r
382

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

    
412
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
413

    
414
  let val_of_expr: type a. (value_t, a) expression_t -> value_t = function
415
    | Val v -> v
416
    | Tag t -> id_to_tag t
417
    | Var v -> vdecl_to_val v
418
    | Memory (StateVar v) -> vdecl_to_val v
419
    | Memory ResetFlag -> vdecl_to_val reset_flag
420

    
421
  type mode =
422
    | MemoryPackMode
423
    | TransitionMode
424
    | ResetIn
425
    | ResetOut
426
    | InstrMode of ident
427

    
428
  let find_arrow m =
429
    try
430
      List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
431
      |> fst
432
    with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
433

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

    
515
end
516

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

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

    
537

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

    
550
let print_machine_ghost_struct fmt m =
551
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
552

    
553
let pp_memory_pack_defs fmt m =
554
  if not (fst (get_stateless_status m)) then
555
    fprintf fmt "%a@,%a"
556
      print_machine_ghost_struct m
557
      (pp_print_list
558
         ~pp_epilogue:pp_print_cut
559
         ~pp_open_box:pp_open_vbox0
560
         (pp_memory_pack_def m)) 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) (pp_machine_decl' ~ghost:true)
570
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
571
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
572
       (PrintSpec.pp_spec TransitionMode m))
573
    fmt
574
    ((t, (name, mem_in), (name, mem_out)),
575
     t.tformula)
576

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

    
657
(* let print_machine_trans_simulation dependencies m fmt i instr =
658
 *   print_machine_trans_simulation_aux m
659
 *     (print_trans_simulation dependencies m)
660
 *     ~i:(i+1)
661
 *     fmt (i, instr) *)
662

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

    
684
let print_machine_init_predicate fmt m =
685
  if not (fst (get_stateless_status m)) then
686
    let name = m.mname.node_id in
687
    let mem_in = mk_mem_in m in
688
    pp_acsl
689
      (pp_predicate
690
         (pp_initialization (pp_machine_decl' ~ghost:true))
691
         (pp_and_l (fun fmt (i, (td, _)) ->
692
              pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
693
      fmt
694
      ((name, (name, mem_in)), m.minstances)
695

    
696
let pp_at pp_p fmt (p, l) =
697
  fprintf fmt "\\at(%a, %s)" pp_p p l
698

    
699
let label_pre = "Pre"
700

    
701
let pp_at_pre pp_p fmt p =
702
  pp_at pp_p fmt (p, label_pre)
703

    
704
let pp_register_chain ?(indirect=true) ptr =
705
  pp_print_list
706
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
707
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
708
                     (if indirect then "->" else "."))
709
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
710
    (fun fmt (i, _) -> pp_print_string fmt i)
711

    
712
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
713
  pp_print_list
714
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
715
    ~pp_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
716
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
717
    (fun fmt (i, _) -> pp_print_string fmt i)
718
    fmt mems
719

    
720
let pp_arrow_reset_ghost mem fmt inst =
721
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
722

    
723
module GhostProto: MODIFIERS_GHOST_PROTO = struct
724
  let pp_ghost_parameters ?(cut=true) fmt vs =
725
    fprintf fmt "%a%a"
726
      (if cut then pp_print_cut else pp_print_nothing) ()
727
      (pp_acsl_line'
728
         (pp_ghost
729
            (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
730
      vs
731
end
732

    
733
module HdrMod = struct
734

    
735
  module GhostProto = GhostProto
736

    
737
  let print_machine_decl_prefix = fun _ _ -> ()
738

    
739
  let pp_import_standard_spec fmt () =
740
    fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
741
      (Arrow.arrow_top_decl ()).top_decl_owner
742
      (if !Options.cpp then "pp" else "")
743

    
744
end
745

    
746
module SrcMod = struct
747

    
748
  module GhostProto = GhostProto
749

    
750
  let pp_predicates (* dependencies *) fmt machines =
751
    fprintf fmt
752
      "%a%a%a%a"
753
      (pp_print_list
754
         ~pp_open_box:pp_open_vbox0
755
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
756
         print_machine_valid_predicate
757
         ~pp_epilogue:pp_print_cutcut) machines
758
      (pp_print_list
759
         ~pp_open_box:pp_open_vbox0
760
         ~pp_sep:pp_print_cutcut
761
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
762
         pp_memory_pack_defs
763
         ~pp_epilogue:pp_print_cutcut) machines
764
      (pp_print_list
765
         ~pp_open_box:pp_open_vbox0
766
         ~pp_sep:pp_print_cutcut
767
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
768
         print_machine_init_predicate
769
         ~pp_epilogue:pp_print_cutcut) machines
770
      (pp_print_list
771
         ~pp_open_box:pp_open_vbox0
772
         ~pp_sep:pp_print_cutcut
773
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
774
         pp_transition_defs
775
         ~pp_epilogue:pp_print_cutcut) machines
776

    
777
  let pp_clear_reset_spec fmt self mem m =
778
    let name = m.mname.node_id in
779
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
780
        m.minstances in
781
    let mk_insts = List.map (fun x -> [x]) in
782
    pp_acsl_cut (fun fmt () ->
783
        fprintf fmt
784
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
785
          @[<v 2>behavior reset:@;\
786
          %a@,%a@]@,\
787
          @[<v 2>behavior no_reset:@;\
788
          %a@,%a@]@,\
789
          complete behaviors;@,\
790
          disjoint behaviors;"
791
          (pp_requires pp_mem_valid') (name, self)
792
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
793
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
794
          (name, mem, self)
795
          (pp_ensures (pp_memory_pack_aux
796
                         ~i:(List.length m.mspec.mmemory_packs - 2)
797
                         pp_ptr pp_print_string))
798
          (name, mem, self)
799
          (pp_assigns pp_reset_flag) [self]
800
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
801
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
802
          (pp_assigns pp_reset_flag) [mem]
803
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
804
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
805
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
806
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
807
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
808
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
809
      )
810
      fmt ()
811

    
812
  let pp_set_reset_spec fmt self mem m =
813
    let name = m.mname.node_id in
814
    pp_acsl_cut (fun fmt () ->
815
        fprintf fmt
816
          "%a@,%a@,%a"
817
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
818
          (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
819
          (pp_assigns pp_reset_flag) [self; mem])
820
      fmt ()
821

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

    
863
  let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
864
    | MStateAssign (x, v) ->
865
      fprintf fmt "@,%a"
866
        (pp_acsl_line
867
           (pp_ghost
868
              (pp_assign m self (pp_c_var_read m))))
869
        (x, v)
870
    | MResetAssign b ->
871
      fprintf fmt "@,%a"
872
        (pp_acsl_line
873
           (pp_ghost
874
              (pp_reset_assign self)))
875
        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
881
              (pp_ghost
882
                 (pp_arrow_reset_ghost self)))
883
           inst
884
    | _ -> ()
885

    
886
  let pp_step_instr_spec m self mem fmt instr =
887
    fprintf fmt "%a%a"
888
      (pp_ghost_instr_code m mem) 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

    
901
end
902

    
903
(**************************************************************************)
904
(*                              MAKEFILE                                  *)
905
(**************************************************************************)
906

    
907
module MakefileMod = struct
908

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

    
919
    (* EACSL version of library file . c + main .c  *)
920
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
921
    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@."
922
      basename basename basename;
923
    (* Ugly hack to deal with eacsl bugs *)
924
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
925
    fprintf fmt "@.";
926
    fprintf fmt "@.";
927

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

    
945
end
946

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