Project

General

Profile

Download (34.1 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 Machine_code_common
17
open Corelang
18

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

    
22
(**************************************************************************)
23
(* OLD STUFF ???
24

    
25

    
26
let pp_acsl_type var fmt t =
27
  let rec aux t pp_suffix =
28
  match (Types.repr t).Types.tdesc with
29
  | Types.Tclock t'       -> aux t' pp_suffix
30
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
31
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
32
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
33
  | Types.Tarray (d, t')  ->
34
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
35
    aux t' pp_suffix'
36
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
37
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
38
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
39
  | _                     -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
40
  in aux t (fun fmt () -> ())
41

    
42
let pp_acsl_var_decl fmt id =
43
  pp_acsl_type id.var_id fmt id.var_type
44

    
45

    
46
let rec pp_eexpr is_output fmt eexpr = 
47
  let pp_eexpr = pp_eexpr is_output in
48
  match eexpr.eexpr_desc with
49
    | EExpr_const c -> Printers.pp_econst fmt c
50
    | EExpr_ident id -> 
51
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
52
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
53
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
54
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
55
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
56
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
57
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
58
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
59
    | EExpr_merge (id, e1, e2) -> 
60
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
61
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
62
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
63
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
64

    
65

    
66
    (* | EExpr_whennot _ *)
67
    (* | EExpr_uclock _ *)
68
    (* | EExpr_dclock _ *)
69
    (* | EExpr_phclock _ -> assert false *)
70
and pp_eapp is_output fmt id e r =
71
  let pp_eexpr = pp_eexpr is_output in
72
  match r with
73
  | None ->
74
    (match id, e.eexpr_desc with
75
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
76
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
77
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
78
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
79
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
80
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
81
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
82
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
83
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
84
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
85
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
86
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
87
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
88
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
89
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
90
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
91
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
92
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
93
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
94
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
95

    
96
let pp_ensures is_output fmt e =
97
  match e with
98
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
99
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
100

    
101
let pp_acsl_spec outputs fmt spec =
102
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
103
  let pp_eexpr = pp_eexpr is_output in
104
  fprintf fmt "@[<v 2>/*@@ ";
105
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
106
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
107
  fprintf fmt "@ ";
108
  (* fprintf fmt "assigns *self%t%a;@ "  *)
109
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
110
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
111
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
112
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
113
      name
114
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
115
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
116
  ) fmt spec.behaviors;
117
  fprintf fmt "@]@ */@.";
118
  ()
119

    
120

    
121

    
122

    
123
let print_machine_decl_prefix fmt m =
124
   (* Print specification if any *)
125
   (match m.mspec with
126
  | None -> ()
127
  | Some spec -> 
128
    pp_acsl_spec m.mstep.step_outputs fmt spec
129
  )
130

    
131
  *)
132

    
133
   (* TODO ACSL
134
   Return updates machines (eg with local annotations) and acsl preamble *)
135
let preprocess_acsl machines = machines, []
136
                          
137
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
138
let pp_acsl_preamble fmt _preamble =
139
  Format.fprintf fmt "";
140
  ()
141

    
142
let pp_acsl_basic_type_desc t_desc =
143
  if Types.is_bool_type t_desc then
144
    (* if !Options.cpp then "bool" else "_Bool" *)
145
    "_Bool"
146
  else if Types.is_int_type t_desc then
147
    (* !Options.int_type *)
148
    "integer"
149
  else if Types.is_real_type t_desc then
150
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
151
  else
152
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
153

    
154
module VarDecl = struct
155
  type t = var_decl
156
  let compare v1 v2 = compare v1.var_id v2.var_id
157
end
158
module VDSet = Set.Make(VarDecl)
159

    
160
module Live = Map.Make(Int)
161

    
162
let pp_spec pp fmt =
163
  fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
164

    
165
let pp_spec_cut pp fmt =
166
  fprintf fmt "%a@," (pp_spec pp)
167

    
168
let pp_spec_line pp fmt =
169
  fprintf fmt "//%@ %a@," pp
170

    
171
let pp_requires pp_req fmt =
172
  fprintf fmt "requires %a;" pp_req
173

    
174
let pp_ensures pp_ens fmt =
175
  fprintf fmt "ensures %a;" pp_ens
176

    
177
let pp_assigns pp =
178
  pp_print_list
179
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
180
    ~pp_epilogue:pp_print_semicolon'
181
    ~pp_sep:pp_print_comma
182
    pp
183

    
184
let pp_ghost pp_gho fmt =
185
  fprintf fmt "ghost %a" pp_gho
186

    
187
let pp_assert pp_ast fmt =
188
  fprintf fmt "assert %a;" pp_ast
189

    
190
let pp_mem_valid pp_var fmt (name, var) =
191
  fprintf fmt "%s_valid(%a)" name pp_var var
192

    
193
let pp_mem_valid' = pp_mem_valid pp_print_string
194

    
195
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
196
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
197

    
198
let pp_indirect' = pp_indirect pp_print_string pp_print_string
199

    
200
let pp_access pp_stru pp_field fmt (stru, field) =
201
  fprintf fmt "%a.%a" pp_stru stru pp_field field
202

    
203
let pp_access' = pp_access pp_print_string pp_print_string
204

    
205
let pp_inst self fmt (name, _) =
206
  pp_indirect' fmt (self, name)
207

    
208
let pp_var_decl fmt v =
209
  pp_print_string fmt v.var_id
210

    
211
let pp_reg self fmt field =
212
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
213

    
214
let pp_true fmt () =
215
  pp_print_string fmt "\\true"
216

    
217
(* let memories machines m =
218
 *   let open List in
219
 *   let grow paths i =
220
 *     match paths with
221
 *     | [] -> [[i]]
222
 *     | _ -> map (cons i) paths
223
 *   in
224
 *   let rec aux paths m =
225
 *     map (fun (i, (td, _)) ->
226
 *         let paths = grow paths i in
227
 *         try
228
 *           let m = find (fun m -> m.mname.node_id = node_name td) machines in
229
 *           aux paths m
230
 *         with Not_found -> paths)
231
 *       m.minstances |> flatten
232
 *   in
233
 *   aux [] m |> map rev *)
234

    
235
let instances machines m =
236
  let open List in
237
  let grow paths i mems =
238
    match paths with
239
    | [] -> [[i, mems]]
240
    | _ -> map (cons (i, mems)) paths
241
  in
242
  let rec aux paths m =
243
    map (fun (i, (td, _)) ->
244
        try
245
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
246
          aux (grow paths i m.mmemory) m
247
        with Not_found -> grow paths i [])
248
      m.minstances |> flatten
249
  in
250
  aux [] m |> map rev
251

    
252
let memories insts =
253
  List.(map (fun path ->
254
      let mems = snd (hd (rev path)) in
255
      map (fun mem -> path, mem) mems) insts |> flatten)
256

    
257
let pp_instance =
258
  pp_print_list
259
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
260
    ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
261
    (fun fmt (i, _) -> pp_print_string fmt i)
262

    
263
let pp_memory fmt (path, mem) =
264
  pp_access (pp_indirect pp_instance pp_print_string) pp_var_decl
265
    fmt ((path, "_reg"), mem)
266
  (* let mems = snd List.(hd (rev path)) in
267
   * pp_print_list
268
   *   ~pp_sep:pp_print_comma
269
   *   (fun fmt mem -> pp_access pp_instance pp_var_decl fmt (path, mem))
270
   *   fmt
271
   *   mems *)
272
  (* let mems = ref [] in
273
   * let pp fmt =
274
   *   pp_print_list
275
   *     ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
276
   *     ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
277
   *     (fun fmt (i, regs) -> mems := regs; pp_print_string fmt i)
278
   *     fmt
279
   * in
280
   * pp_print_list
281
   *   ~pp_sep:pp_print_comma
282
   *   (fun fmt mem -> pp_access pp pp_var_decl fmt (insts, mem))
283
   *   fmt !mems *)
284

    
285
let prefixes l =
286
  let rec pref acc = function
287
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
288
    | [] -> acc
289
  in
290
  pref [] (List.rev l)
291

    
292
let powerset_instances paths =
293
  List.map prefixes paths |> List.flatten
294

    
295
let pp_separated self fmt (paths, ptrs) =
296
  fprintf fmt "\\separated(@[<h>%s%a%a@])"
297
    self
298
    (pp_print_list
299
       ~pp_prologue:pp_print_comma
300
       ~pp_sep:pp_print_comma
301
       pp_instance)
302
    paths
303
    (pp_print_list
304
       ~pp_prologue:pp_print_comma
305
       ~pp_sep:pp_print_comma
306
       pp_var_decl)
307
    ptrs
308

    
309
let pp_forall pp_l pp_r fmt (l, r) =
310
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
311
    pp_l l
312
    pp_r r
313

    
314
let pp_exists pp_l pp_r fmt (l, r) =
315
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
316
    pp_l l
317
    pp_r r
318

    
319
let pp_valid =
320
  pp_print_braced
321
    ~pp_nil:pp_true
322
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid(")
323
    ~pp_epilogue:pp_print_cpar
324

    
325
let pp_equal pp_l pp_r fmt (l, r) =
326
  fprintf fmt "%a == %a"
327
    pp_l l
328
    pp_r r
329

    
330
let pp_different pp_l pp_r fmt (l, r) =
331
  fprintf fmt "%a != %a"
332
    pp_l l
333
    pp_r r
334

    
335
let pp_implies pp_l pp_r fmt (l, r) =
336
  fprintf fmt "@[<v>%a ==>@ %a@]"
337
    pp_l l
338
    pp_r r
339

    
340
let pp_and pp_l pp_r fmt (l, r) =
341
  fprintf fmt "@[<v>%a @ && %a@]"
342
    pp_l l
343
    pp_r r
344

    
345
let pp_and_l pp_v fmt =
346
  pp_print_list
347
    ~pp_open_box:pp_open_vbox0
348
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
349
    pp_v
350
    fmt
351

    
352
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
353
  fprintf fmt "%a @[<hov>? %a@ : %a@]"
354
    pp_c c
355
    pp_t t
356
    pp_f f
357

    
358
let pp_paren pp fmt v =
359
  fprintf fmt "(%a)" pp v
360

    
361
let pp_machine_decl fmt (id, mem_type, var) =
362
  fprintf fmt "struct %s_%s %s" id mem_type var
363

    
364
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
365
  fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
366
    name
367
    (pp_print_option pp_print_int) i
368
    pp_mem mem
369
    pp_self self
370

    
371
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
372

    
373
let pp_mem_init pp_mem fmt (name, mem) =
374
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
375

    
376
let pp_mem_init' = pp_mem_init pp_print_string
377

    
378
let pp_locals m fmt vs =
379
  pp_print_list
380
    ~pp_open_box:pp_open_hbox
381
    ~pp_sep:pp_print_comma
382
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs
383

    
384
let pp_ptr_decl fmt v =
385
  fprintf fmt "*%s" v.var_id
386

    
387
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
388
  if Types.is_real_type typ && !Options.mpfr
389
  then
390
    assert false
391
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
392
  else
393
    pp_equal pp_l pp_r fmt (var_name, value)
394

    
395
let pp_assign_spec
396
    m self_l pp_var_l self_r pp_var_r fmt (var_type, var_name, value) =
397
  let depth = expansion_depth value in
398
  let loop_vars = mk_loop_variables m var_type depth in
399
  let reordered_loop_vars = reorder_loop_variables loop_vars in
400
  let rec aux typ fmt vars =
401
    match vars with
402
    | [] ->
403
      pp_basic_assign_spec
404
        (pp_value_suffix ~indirect:false m self_l var_type loop_vars pp_var_l)
405
        (pp_value_suffix ~indirect:false m self_r var_type loop_vars pp_var_r)
406
        fmt typ var_name value
407
    | (d, LVar i) :: q ->
408
      assert false
409
      (* let typ' = Types.array_element_type typ in
410
       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
411
       *   i i i pp_c_dimension d i
412
       *   (aux typ') q *)
413
    | (d, LInt r) :: q ->
414
      assert false
415
      (* let typ' = Types.array_element_type typ in
416
       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
417
       * fprintf fmt "@[<v 2>{@,%a@]@,}"
418
       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
419
    | _ -> assert false
420
  in
421
  begin
422
    reset_loop_counter ();
423
    aux var_type fmt reordered_loop_vars;
424
  end
425

    
426
let pp_c_var_read m fmt id =
427
  (* mpfr_t is a static array, not treated as general arrays *)
428
  if Types.is_address_type id.var_type
429
  then
430
    if Machine_code_common.is_memory m id
431
    && not (Types.is_real_type id.var_type && !Options.mpfr)
432
    then fprintf fmt "(*%s)" id.var_id
433
    else fprintf fmt "%s" id.var_id
434
  else
435
    fprintf fmt "%s" id.var_id
436

    
437
let rec assigned s instr =
438
  let open VDSet in
439
  match instr.instr_desc with
440
  | MLocalAssign (x, _) ->
441
    add x s
442
  | MStep (xs, _, _) ->
443
    union s (of_list xs)
444
  | MBranch (_, brs) ->
445
    List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)
446
  | _ -> s
447

    
448
let rec occur_val s v =
449
  let open VDSet in
450
  match v.value_desc with
451
  | Var x ->
452
    add x s
453
  | Fun (_, vs)
454
  | Array vs ->
455
    List.fold_left occur_val s vs
456
  | Access (v1, v2)
457
  | Power (v1, v2) ->
458
    occur_val (occur_val s v1) v2
459
  | _ -> s
460

    
461
let rec occur s instr =
462
  let open VDSet in
463
  match instr.instr_desc with
464
  | MLocalAssign (_, v)
465
  | MStateAssign (_, v) ->
466
    occur_val s v
467
  | MStep (_, _, vs) ->
468
    List.fold_left occur_val s vs
469
  | MBranch (v, brs) ->
470
    List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)
471
            (occur_val s v) brs)
472
  | _ -> s
473

    
474
let live = Hashtbl.create 32
475

    
476
let set_live_of m =
477
  let open VDSet in
478
  let locals = of_list m.mstep.step_locals in
479
  let outputs = of_list m.mstep.step_outputs in
480
  let vars = union locals outputs in
481
  let no_occur_after i =
482
    let occ, _ = List.fold_left (fun (s, j) instr ->
483
        if j <= i then (s, j+1) else (occur s instr, j+1))
484
        (empty, 0) m.mstep.step_instrs in
485
    diff locals occ
486
  in
487
  let l, _, _ = List.fold_left (fun (l, asg, i) instr ->
488
      let asg = inter (assigned asg instr) vars in
489
      Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)
490
      (Live.empty, empty, 0) m.mstep.step_instrs in
491
  Hashtbl.add live m.mname.node_id (Live.add 0 empty l)
492

    
493
let live_i m i =
494
  Live.find i (Hashtbl.find live m.mname.node_id)
495

    
496
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
497
    (name, inputs, locals, outputs, mem_in, mem_out) =
498
  fprintf fmt "%s_transition%a(@[<hov>%a,@ %a%a%a%a@])"
499
    name
500
    (pp_print_option pp_print_int) i
501
    pp_mem_in mem_in
502
    (pp_print_list
503
       ~pp_epilogue:pp_print_comma
504
       ~pp_sep:pp_print_comma
505
       pp_input) inputs
506
    (pp_print_option
507
       (fun fmt _ ->
508
          pp_print_list
509
            ~pp_epilogue:pp_print_comma
510
            ~pp_sep:pp_print_comma
511
            pp_input fmt locals))
512
    i
513
    pp_mem_out mem_out
514
    (pp_print_list
515
       ~pp_prologue:pp_print_comma
516
       ~pp_sep:pp_print_comma
517
       pp_output) outputs
518

    
519
let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt
520
    (m, mem_in, mem_out) =
521
  let locals, outputs = match i with
522
    | Some 0 ->
523
      [], []
524
    | Some i when i < List.length m.mstep.step_instrs ->
525
      let li = live_i m i in
526
      VDSet.(inter (of_list m.mstep.step_locals) li |> elements,
527
             inter (of_list m.mstep.step_outputs) li |> elements)
528
    | Some _ ->
529
      [], m.mstep.step_outputs
530
    | _ ->
531
      m.mstep.step_locals, m.mstep.step_outputs
532
  in
533
  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
534
    (m.mname.node_id,
535
     m.mstep.step_inputs,
536
     locals,
537
     outputs,
538
     mem_in,
539
     mem_out)
540

    
541
let pp_mem_trans' ?i fmt =
542
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt
543
let pp_mem_trans'' ?i fmt =
544
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
545

    
546
let pp_nothing fmt () =
547
  pp_print_string fmt "\\nothing"
548

    
549
let pp_predicate pp_l pp_r fmt (l, r) =
550
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
551
    pp_l l
552
    pp_r r
553

    
554
let print_machine_valid_predicate fmt m =
555
  if not (fst (Machine_code_common.get_stateless_status m)) then
556
    let name = m.mname.node_id in
557
    let self = mk_self m in
558
    pp_spec
559
      (pp_predicate
560
         (pp_mem_valid pp_machine_decl)
561
         (pp_and
562
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
563
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
564
            (pp_valid pp_print_string)))
565
      fmt
566
      ((name, (name, "mem", "*" ^ self)),
567
       (m.minstances, [self]))
568

    
569
let print_machine_ghost_simulation_aux ?i m pp fmt v =
570
  let name = m.mname.node_id in
571
  let self = mk_self m in
572
  let mem = mk_mem m in
573
  pp_spec
574
    (pp_predicate
575
       (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
576
       pp)
577
    fmt
578
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
579
     v)
580

    
581
let print_ghost_simulation dependencies m fmt (i, instr) =
582
  let name = m.mname.node_id in
583
  let self = mk_self m in
584
  let mem = mk_mem m in
585
  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
586
  let pred pp v = pp_and prev_ghost pp fmt ((), v) in
587
  let rec aux fmt instr =
588
    match instr.instr_desc with
589
    | MStateAssign (m, _) ->
590
      pp_equal
591
        (pp_access pp_print_string (pp_access pp_print_string pp_var_decl))
592
        (pp_indirect pp_print_string (pp_access pp_print_string pp_var_decl))
593
        fmt
594
        ((mem, ("_reg", m)), (self, ("_reg", m)))
595
    | MStep ([i0], i, vl)
596
      when Basic_library.is_value_internal_fun
597
          (mk_val (Fun (i, vl)) i0.var_type)  ->
598
      pp_true fmt ()
599
    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
600
      pp_true fmt ()
601
    | MStep ([_], i, _) when has_c_prototype i dependencies ->
602
      pp_true fmt ()
603
    | MStep (_, i, _)
604
    | MReset i ->
605
      begin try
606
          let n, _ = List.assoc i m.minstances in
607
          pp_mem_ghost pp_access' pp_indirect' fmt
608
            (node_name n, (mem, i), (self, i))
609
        with Not_found -> pp_true fmt ()
610
      end
611
    | MBranch (_, brs) ->
612
      (* TODO: handle branches *)
613
      pp_and_l aux fmt List.(flatten (map snd brs))
614
    | _ -> pp_true fmt ()
615
  in
616
  pred aux instr
617

    
618
let print_machine_ghost_simulation dependencies m fmt i instr =
619
  print_machine_ghost_simulation_aux m
620
    (print_ghost_simulation dependencies m)
621
    ~i:(i+1)
622
    fmt (i, instr)
623

    
624
let print_machine_ghost_struct fmt m =
625
  pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
626

    
627
let print_machine_ghost_simulations dependencies fmt m =
628
  if not (fst (Machine_code_common.get_stateless_status m)) then
629
    let name = m.mname.node_id in
630
    let self = mk_self m in
631
    let mem = mk_mem m in
632
    fprintf fmt "%a@,%a@,%a%a"
633
      print_machine_ghost_struct m
634
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
635
      (pp_print_list_i
636
        ~pp_epilogue:pp_print_cut
637
        ~pp_open_box:pp_open_vbox0
638
        (print_machine_ghost_simulation dependencies m))
639
      m.mstep.step_instrs
640
      (print_machine_ghost_simulation_aux m
641
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
642

    
643
let print_machine_trans_simulation_aux ?i m pp fmt v =
644
  let name = m.mname.node_id in
645
  let mem_in = mk_mem_in m in
646
  let mem_out = mk_mem_out m in
647
  pp_spec
648
    (pp_predicate
649
       (pp_mem_trans pp_machine_decl pp_machine_decl
650
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
651
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
652
          ?i)
653
       pp)
654
    fmt
655
    ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
656
     v)
657

    
658
let print_trans_simulation machines dependencies m fmt (i, instr) =
659
  let mem_in = mk_mem_in m in
660
  let mem_out = mk_mem_out m in
661
  let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
662
                   (live_i m (i+1))) in
663
  (* XXX *)
664
  printf "%d : %a\n%d : %a\nocc: %a\n\n"
665
    i
666
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
667
    (i+1)
668
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
669
    (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr));
670
  let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
671
  let pred pp v =
672
    let vars = VDSet.(union (of_list m.mstep.step_locals)
673
                        (of_list m.mstep.step_outputs)) in
674
    let locals = VDSet.(inter vars d |> elements) in
675
    if locals = []
676
    then pp_and prev_trans pp fmt ((), v)
677
    else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
678
  in
679
  let rec aux fmt instr = match instr.instr_desc with
680
    | MLocalAssign (x, v)
681
    | MStateAssign (x, v) ->
682
      pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m)fmt
683
        (x.var_type, mk_val (Var x) x.var_type, v)
684
    | MStep ([i0], i, vl)
685
      when Basic_library.is_value_internal_fun
686
          (mk_val (Fun (i, vl)) i0.var_type)  ->
687
      pp_true fmt ()
688
    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
689
      pp_true fmt ()
690
    | MStep ([_], i, _) when has_c_prototype i dependencies ->
691
      pp_true fmt ()
692
    | MStep (xs, f, ys) ->
693
      begin try
694
          let n, _ = List.assoc f m.minstances in
695
            pp_mem_trans_aux
696
              pp_access' pp_access'
697
              (pp_c_val m mem_in (pp_c_var_read m))
698
              pp_var_decl
699
              fmt
700
              (node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
701
        with Not_found -> pp_true fmt ()
702
      end
703
    | MReset f ->
704
      begin try
705
          let n, _ = List.assoc f m.minstances in
706
          pp_mem_init' fmt (node_name n, mem_out)
707
        with Not_found -> pp_true fmt ()
708
      end
709
    | MBranch (v, brs) ->
710
      if let t = fst (List.hd brs) in t = tag_true || t = tag_false
711
      then (* boolean case *)
712
        pp_ite (pp_c_val m mem_in (pp_c_var_read m))
713
          (fun fmt () ->
714
             try
715
               let l = List.assoc tag_true brs in
716
               pp_paren (pp_and_l aux) fmt l
717
             with Not_found -> pp_true fmt ())
718
          (fun fmt () ->
719
             try
720
               let l = List.assoc tag_false brs in
721
               pp_paren (pp_and_l aux) fmt l
722
             with Not_found -> pp_true fmt ())
723
          
724
          (* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux)) *)
725
          fmt (v, (), ())
726
      else (* enum type case *)
727
      pp_and_l (fun fmt (l, instrs) ->
728
          let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
729
          (* if l = tag_false then
730
           *   pp_paren (pp_implies
731
           *               (pp_different pp_val pp_c_tag)
732
           *               (pp_and_l aux))
733
           *     fmt
734
           *     ((v, tag_true), instrs)
735
           * else *)
736
            pp_paren (pp_implies
737
                        (pp_equal pp_val pp_c_tag)
738
                        (pp_and_l aux))
739
              fmt
740
              ((v, l), instrs))
741
        fmt brs
742
    | _ -> pp_true fmt ()
743
  in
744
  pred aux instr
745

    
746
let print_machine_trans_simulation machines dependencies m fmt i instr =
747
  print_machine_trans_simulation_aux m
748
    (print_trans_simulation machines dependencies m)
749
    ~i:(i+1)
750
    fmt (i, instr)
751

    
752
let print_machine_trans_annotations machines dependencies fmt m =
753
  if not (fst (Machine_code_common.get_stateless_status m)) then begin
754
    set_live_of m;
755
    let i = List.length m.mstep.step_instrs in
756
    let mem_in = mk_mem_in m in
757
    let mem_out = mk_mem_out m in
758
    let last_trans fmt () =
759
      let locals = VDSet.(inter
760
                            (of_list m.mstep.step_locals)
761
                            (live_i m i)
762
                          |> elements) in
763
      if locals = []
764
      then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
765
      else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
766
          (locals, (m, mem_in, mem_out))
767
    in
768
    fprintf fmt "%a@,%a%a"
769
      (print_machine_trans_simulation_aux m pp_true ~i:0) ()
770
      (pp_print_list_i
771
        ~pp_epilogue:pp_print_cut
772
        ~pp_open_box:pp_open_vbox0
773
        (print_machine_trans_simulation machines dependencies m))
774
      m.mstep.step_instrs
775
      (print_machine_trans_simulation_aux m last_trans) ()
776
  end
777

    
778
let print_machine_init_predicate fmt m =
779
  if not (fst (Machine_code_common.get_stateless_status m)) then
780
    let name = m.mname.node_id in
781
    let mem_in = mk_mem_in m in
782
    pp_spec
783
      (pp_predicate
784
         (pp_mem_init pp_machine_decl)
785
         (pp_and_l (fun fmt (i, (td, _)) ->
786
              pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))
787
      fmt
788
      ((name, (name, "mem_ghost", mem_in)), m.minstances)
789

    
790
let pp_at pp_p fmt (p, l) =
791
  fprintf fmt "\\at(%a, %s)" pp_p p l
792

    
793
let label_pre = "Pre"
794

    
795
let pp_at_pre pp_p fmt p =
796
  pp_at pp_p fmt (p, label_pre)
797

    
798
let pp_arrow_spec fmt () =
799
  let name = "_arrow" in
800
  let mem_in = "mem_in" in
801
  let mem_out = "mem_out" in
802
  let reg_first = "_reg", "_first" in
803
  let mem_in_first = mem_in, reg_first in
804
  let mem_out_first = mem_out, reg_first in
805
  let mem = "mem" in
806
  let self = "self" in
807
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"
808

    
809
    (pp_spec_line (pp_ghost pp_print_string))
810
    "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
811

    
812
    (pp_spec_cut
813
       (pp_predicate
814
          (pp_mem_valid pp_machine_decl)
815
          (pp_valid pp_print_string)))
816
    ((name, (name, "mem", "*" ^ self)), [self])
817

    
818
    (pp_spec_cut
819
       (pp_predicate
820
          (pp_mem_init pp_machine_decl)
821
          (pp_equal
822
             (pp_access pp_print_string pp_access')
823
             pp_print_int)))
824
    ((name, (name, "mem_ghost", mem_in)),
825
     (mem_in_first, 1))
826

    
827
    (pp_spec_cut
828
       (pp_predicate
829
          (pp_mem_trans_aux
830
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
831
          (pp_ite
832
             (pp_access pp_print_string pp_access')
833
             (pp_paren
834
                (pp_and
835
                   (pp_equal
836
                      (pp_access pp_print_string pp_access')
837
                      pp_print_int)
838
                   (pp_equal pp_print_string pp_print_string)))
839
                (pp_paren
840
                   (pp_and
841
                      (pp_equal
842
                         (pp_access pp_print_string pp_access')
843
                         (pp_access pp_print_string pp_access'))
844
                      (pp_equal pp_print_string pp_print_string))))))
845
    ((name, ["integer x"; "integer y"], [], ["_Bool out"],
846
      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
847
     (* (("out", mem_in_first), *)
848
     (mem_in_first, ((mem_out_first, 0), ("out", "x")),
849
      ((mem_out_first, mem_in_first), ("out", "y"))))
850

    
851
    (pp_spec_cut
852
       (pp_predicate
853
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
854
          (pp_equal
855
             (pp_access pp_print_string pp_access')
856
             (pp_indirect pp_print_string pp_access'))))
857
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
858
    ((mem, reg_first), (self, reg_first)))
859

    
860
module SrcMod = struct
861

    
862
  let pp_predicates dependencies fmt machines =
863
    fprintf fmt
864
      "%a@,%a%a%a%a"
865
      pp_arrow_spec ()
866
      (pp_print_list
867
         ~pp_open_box:pp_open_vbox0
868
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
869
         print_machine_valid_predicate
870
         ~pp_epilogue:pp_print_cutcut) machines
871
      (pp_print_list
872
         ~pp_open_box:pp_open_vbox0
873
         ~pp_sep:pp_print_cutcut
874
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
875
         (print_machine_ghost_simulations dependencies)
876
         ~pp_epilogue:pp_print_cutcut) machines
877
      (pp_print_list
878
         ~pp_open_box:pp_open_vbox0
879
         ~pp_sep:pp_print_cutcut
880
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
881
         print_machine_init_predicate
882
         ~pp_epilogue:pp_print_cutcut) machines
883
      (pp_print_list
884
         ~pp_open_box:pp_open_vbox0
885
         ~pp_sep:pp_print_cutcut
886
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
887
         (print_machine_trans_annotations machines dependencies)
888
         ~pp_epilogue:pp_print_cutcut) machines
889

    
890
  let pp_register =
891
    pp_print_list
892
      ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
893
      ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
894
      ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
895
      (fun fmt (i, _) -> pp_print_string fmt i)
896

    
897
  let pp_reset_spec fmt machines self m =
898
    let name = m.mname.node_id in
899
    let mem = mk_mem m in
900
    let insts = instances machines m in
901
    pp_spec_cut (fun fmt () ->
902
        fprintf fmt
903
          "%a@,%a@,%a@,%a"
904
          (pp_requires pp_mem_valid') (name, self)
905
          (pp_requires (pp_separated self)) (powerset_instances insts, [])
906
          (pp_assigns pp_register) insts
907
          (pp_ensures
908
             (pp_forall
909
                pp_machine_decl
910
                (pp_implies
911
                   pp_mem_ghost'
912
                   pp_mem_init')))
913
          ((name, "mem_ghost", mem),
914
           ((name, mem, self), (name, mem))))
915
      fmt ()
916

    
917
  let pp_step_spec fmt machines self m =
918
    let name = m.mname.node_id in
919
    let mem_in = mk_mem_in m in
920
    let mem_out = mk_mem_out m in
921
    let insts = instances machines m in
922
    let insts' = powerset_instances insts in
923
    pp_spec_cut (fun fmt () ->
924
        fprintf fmt
925
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
926
          (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
927
          (pp_requires pp_mem_valid') (name, self)
928
          (pp_requires (pp_separated self)) (insts', m.mstep.step_outputs)
929
          (pp_assigns pp_ptr_decl) m.mstep.step_outputs
930
          (pp_assigns (pp_reg self)) m.mmemory
931
          (pp_assigns pp_memory) (memories insts')
932
          (pp_assigns pp_register) insts
933
          (pp_ensures
934
             (pp_forall
935
                (fun fmt () ->
936
                   fprintf fmt "%a, %s"
937
                     pp_machine_decl (name, "mem_ghost", mem_in)
938
                     mem_out)
939
                (pp_implies
940
                   (pp_at_pre pp_mem_ghost')
941
                   (pp_implies
942
                      pp_mem_ghost'
943
                      pp_mem_trans''))))
944
          ((),
945
           ((name, mem_in, self),
946
            ((name, mem_out, self),
947
             (m, mem_in, mem_out)))))
948
      fmt ()
949

    
950
  let pp_step_instr_spec m self fmt (i, _instr) =
951
    let name = m.mname.node_id in
952
    let mem_in = mk_mem_in m in
953
    let mem_out = mk_mem_out m in
954
    fprintf fmt "@,%a"
955
      (pp_spec
956
         (pp_assert
957
            (pp_forall
958
               (fun fmt () ->
959
                  fprintf fmt "%a, %s"
960
                    pp_machine_decl (name, "mem_ghost", mem_in)
961
                    mem_out)
962
               (pp_implies
963
                  (pp_at_pre pp_mem_ghost')
964
                  (pp_implies
965
                     (pp_mem_ghost' ~i)
966
                     (pp_mem_trans'' ~i))))))
967
      ((),
968
       ((name, mem_in, self),
969
        ((name, mem_out, self),
970
         (m, mem_in, mem_out))))
971

    
972
end
973

    
974
(**************************************************************************)
975
(*                              MAKEFILE                                  *)
976
(**************************************************************************)
977

    
978
module MakefileMod = struct
979

    
980
  let other_targets fmt basename _nodename dependencies =
981
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
982
    (* EACSL version of library file . c *)
983
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
984
    fprintf fmt
985
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
986
      basename basename;
987
    fprintf fmt "@.";
988
    fprintf fmt "@.";
989

    
990
    (* EACSL version of library file . c + main .c  *)
991
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
992
    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@."
993
      basename basename basename;
994
    (* Ugly hack to deal with eacsl bugs *)
995
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
996
    fprintf fmt "@.";
997
    fprintf fmt "@.";
998

    
999
    (* EACSL version of binary *)
1000
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1001
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
1002
    C_backend_makefile.fprintf_dependencies fmt dependencies;
1003
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
1004
      basename
1005
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
1006
      (C_backend_makefile.compiled_dependencies dependencies)
1007
      ("${FRAMACEACSL}/e_acsl.c "
1008
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1009
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1010
      basename
1011
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
1012
      (C_backend_makefile.lib_dependencies dependencies)
1013
    ;
1014
    fprintf fmt "@."
1015

    
1016
end
1017

    
1018
(* Local Variables: *)
1019
(* compile-command:"make -C ../../.." *)
1020
(* End: *)
(9-9/10)