Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by Lélio Brun 7 months ago

work on spec generation almost done

View differences:

src/backends/C/c_backend_spec.ml
1

  
1 2
(********************************************************************)
2 3
(*                                                                  *)
3 4
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
......
13 14
open Lustre_types
14 15
open Machine_code_types
15 16
open C_backend_common
16
open Machine_code_common
17 17
open Corelang
18
open Spec_types
19
open Spec_common
20
open Machine_code_common
18 21

  
19 22
(**************************************************************************)
20 23
(*     Printing spec for c *)
21 24

  
22 25
(**************************************************************************)
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
26

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

  
142 31
let pp_acsl_basic_type_desc t_desc =
143 32
  if Types.is_bool_type t_desc then
144 33
    (* if !Options.cpp then "bool" else "_Bool" *)
......
151 40
  else
152 41
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
153 42

  
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
43
let pp_acsl pp fmt =
44
  fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
164 45

  
165
let pp_spec_cut pp fmt =
166
  fprintf fmt "%a@," (pp_spec pp)
46
let pp_acsl_cut pp fmt =
47
  fprintf fmt "%a@," (pp_acsl pp)
167 48

  
168
let pp_spec_line pp fmt =
169
  fprintf fmt "//%@ %a@," pp
49
let pp_acsl_line pp fmt =
50
  fprintf fmt "//%@ @[<h>%a@]" pp
170 51

  
171 52
let pp_requires pp_req fmt =
172 53
  fprintf fmt "requires %a;" pp_req
......
174 55
let pp_ensures pp_ens fmt =
175 56
  fprintf fmt "ensures %a;" pp_ens
176 57

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

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

  
184 67
let pp_ghost pp_gho fmt =
......
214 97
let pp_true fmt () =
215 98
  pp_print_string fmt "\\true"
216 99

  
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 *)
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
234 105

  
235 106
let instances machines m =
236 107
  let open List in
237
  let grow paths i mems =
108
  let grow paths i td mems =
238 109
    match paths with
239
    | [] -> [[i, mems]]
240
    | _ -> map (cons (i, mems)) paths
110
    | [] -> [[i, (td, mems)]]
111
    | _ -> map (cons (i, (td, mems))) paths
241 112
  in
242 113
  let rec aux paths m =
243 114
    map (fun (i, (td, _)) ->
244 115
        try
245 116
          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 [])
117
          aux (grow paths i td m.mmemory) m
118
        with Not_found -> grow paths i td [])
248 119
      m.minstances |> flatten
249 120
  in
250 121
  aux [] m |> map rev
251 122

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

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

  
263
let pp_memory fmt (path, mem) =
264
  pp_access (pp_indirect pp_instance pp_print_string) pp_var_decl
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
265 139
    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 140

  
285 141
let prefixes l =
286 142
  let rec pref acc = function
......
292 148
let powerset_instances paths =
293 149
  List.map prefixes paths |> List.flatten
294 150

  
295
let pp_separated self fmt (paths, ptrs) =
296
  fprintf fmt "\\separated(@[<h>%s%a%a@])"
151
let pp_separated self mem fmt (paths, ptrs) =
152
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
297 153
    self
298
    (pp_print_list
299
       ~pp_prologue:pp_print_comma
300
       ~pp_sep:pp_print_comma
301
       pp_instance)
154
    mem
155
    (pp_comma_list
156
       ~pp_prologue:pp_print_comma'
157
       (pp_instance self))
302 158
    paths
303
    (pp_print_list
304
       ~pp_prologue:pp_print_comma
305
       ~pp_sep:pp_print_comma
159
    (pp_comma_list
160
       ~pp_prologue:pp_print_comma'
306 161
       pp_var_decl)
307 162
    ptrs
308 163

  
309 164
let pp_separated' =
310
  pp_print_list
165
  pp_comma_list
311 166
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
312 167
    ~pp_epilogue:pp_print_cpar
313
    ~pp_sep:pp_print_comma
314 168
    pp_var_decl
315 169

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

  
316 173
let pp_forall pp_l pp_r fmt (l, r) =
317 174
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
318 175
    pp_l l
......
350 207
    pp_v
351 208
    fmt
352 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

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

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

  
359 234
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
360 235
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
361 236
    pp_c c
......
365 240
let pp_paren pp fmt v =
366 241
  fprintf fmt "(%a)" pp v
367 242

  
368
let pp_machine_decl fmt (id, mem_type, var) =
369
  fprintf fmt "struct %s_%s %s" id mem_type var
370

  
371
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
372
  fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
373
    name
374
    (pp_print_option pp_print_int) i
375
    pp_mem mem
376
    pp_self self
377

  
378
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
379

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

  
383
let pp_mem_init' = pp_mem_init pp_print_string
246
let pp_initialization' = pp_initialization pp_print_string
384 247

  
385
let pp_locals m fmt vs =
386
  pp_print_list
248
let pp_locals m =
249
  pp_comma_list
387 250
    ~pp_open_box:pp_open_hbox
388
    ~pp_sep:pp_print_comma
389
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs
251
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
390 252

  
391 253
let pp_ptr_decl fmt v =
392
  fprintf fmt "*%s" v.var_id
254
  pp_ptr fmt v.var_id
393 255

  
394 256
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
395 257
  if Types.is_real_type typ && !Options.mpfr
......
399 261
  else
400 262
    pp_equal pp_l pp_r fmt (var_name, value)
401 263

  
402
let pp_assign_spec
403
    m self_l pp_var_l self_r pp_var_r fmt (var_type, var_name, value) =
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) =
404 266
  let depth = expansion_depth value in
405 267
  let loop_vars = mk_loop_variables m var_type depth in
406 268
  let reordered_loop_vars = reorder_loop_variables loop_vars in
......
408 270
    match vars with
409 271
    | [] ->
410 272
      pp_basic_assign_spec
411
        (pp_value_suffix ~indirect:false m self_l var_type loop_vars pp_var_l)
412
        (pp_value_suffix ~indirect:false m self_r var_type loop_vars pp_var_r)
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)
413 275
        fmt typ var_name value
414 276
    | (_d, LVar _i) :: _q ->
415 277
      assert false
......
441 303
  else
442 304
    fprintf fmt "%s" id.var_id
443 305

  
444
let rec assigned s instr =
445
  let open VDSet in
446
  match instr.instr_desc with
447
  | MLocalAssign (x, _) ->
448
    add x s
449
  | MStep (xs, _, _) ->
450
    union s (of_list xs)
451
  | MBranch (_, brs) ->
452
    List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)
453
  | _ -> s
454

  
455
let rec occur_val s v =
456
  let open VDSet in
457
  match v.value_desc with
458
  | Var x ->
459
    add x s
460
  | Fun (_, vs)
461
  | Array vs ->
462
    List.fold_left occur_val s vs
463
  | Access (v1, v2)
464
  | Power (v1, v2) ->
465
    occur_val (occur_val s v1) v2
466
  | _ -> s
467

  
468
let rec occur s instr =
469
  let open VDSet in
470
  match instr.instr_desc with
471
  | MLocalAssign (_, v)
472
  | MStateAssign (_, v) ->
473
    occur_val s v
474
  | MStep (_, _, vs) ->
475
    List.fold_left occur_val s vs
476
  | MBranch (v, brs) ->
477
    List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)
478
            (occur_val s v) brs)
479
  | _ -> s
480

  
481
let live = Hashtbl.create 32
482

  
483
let set_live_of m =
484
  let open VDSet in
485
  let locals = of_list m.mstep.step_locals in
486
  let outputs = of_list m.mstep.step_outputs in
487
  let vars = union locals outputs in
488
  let no_occur_after i =
489
    let occ, _ = List.fold_left (fun (s, j) instr ->
490
        if j <= i then (s, j+1) else (occur s instr, j+1))
491
        (empty, 0) m.mstep.step_instrs in
492
    diff locals occ
493
  in
494
  let l, _, _ = List.fold_left (fun (l, asg, i) instr ->
495
      let asg = inter (assigned asg instr) vars in
496
      Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)
497
      (Live.empty, empty, 0) m.mstep.step_instrs in
498
  Hashtbl.add live m.mname.node_id (Live.add 0 empty l)
306
let pp_nothing fmt () =
307
  pp_print_string fmt "\\nothing"
499 308

  
500
let live_i m i =
501
  Live.find i (Hashtbl.find live m.mname.node_id)
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
502 324

  
503
let pp_mem_trans_aux ?i stateless pp_mem_in pp_mem_out pp_input pp_output fmt
325
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
504 326
    (name, inputs, locals, outputs, mem_in, mem_out) =
505
  fprintf fmt "%s_transition%a(@[<hov>%a%a%a%a%a@])"
327
  let stateless = fst (get_stateless_status m) in
328
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
506 329
    name
507 330
    (pp_print_option pp_print_int) i
508
    (fun fmt () -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in) ()
509
    (pp_print_list
510
       (* ~pp_epilogue:pp_print_comma *)
511
       ~pp_sep:pp_print_comma
512
       pp_input) inputs
513
    (pp_print_option
514
       (fun fmt _ ->
515
          pp_print_list
516
            ~pp_prologue:pp_print_comma
517
            ~pp_sep:pp_print_comma
518
            pp_input fmt locals))
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))
519 335
    i
520
    (fun fmt () -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out) ()
521
    (pp_print_list
522
       ~pp_prologue:pp_print_comma
523
       ~pp_sep:pp_print_comma
524
       pp_output) outputs
525

  
526
let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt
527
    (m, mem_in, mem_out) =
528
  let locals, outputs = match i with
529
    | Some 0 ->
530
      [], []
531
    | Some i when i < List.length m.mstep.step_instrs ->
532
      let li = live_i m i in
533
      VDSet.(inter (of_list m.mstep.step_locals) li |> elements,
534
             inter (of_list m.mstep.step_outputs) li |> elements)
535
    | Some _ ->
536
      [], m.mstep.step_outputs
537
    | _ ->
538
      m.mstep.step_locals, m.mstep.step_outputs
539
  in
540
  pp_mem_trans_aux ?i (fst (get_stateless_status m))
541
    pp_mem_in pp_mem_out pp_input pp_output fmt
542
    (m.mname.node_id,
543
     m.mstep.step_inputs,
544
     locals,
545
     outputs,
546
     mem_in,
547
     mem_out)
548

  
549
let pp_mem_trans' ?i fmt =
550
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt
551
let pp_mem_trans'' ?i fmt =
552
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
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
553 508

  
554
let pp_nothing fmt () =
555
  pp_print_string fmt "\\nothing"
509
end
556 510

  
557 511
let pp_predicate pp_l pp_r fmt (l, r) =
558 512
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
......
563 517
  if not (fst (get_stateless_status m)) then
564 518
    let name = m.mname.node_id in
565 519
    let self = mk_self m in
566
    pp_spec
520
    pp_acsl
567 521
      (pp_predicate
568
         (pp_mem_valid pp_machine_decl)
522
         (pp_mem_valid (pp_machine_decl pp_ptr))
569 523
         (pp_and
570 524
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
571 525
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
572 526
            (pp_valid pp_print_string)))
573 527
      fmt
574
      ((name, (name, "mem", "*" ^ self)),
528
      ((name, (name, self)),
575 529
       (m.minstances, [self]))
576 530

  
577
let print_machine_ghost_simulation_aux ?i m pp fmt v =
578
  let name = m.mname.node_id in
531

  
532
let pp_memory_pack_def m fmt mp =
533
  let name = mp.mpname.node_id in
579 534
  let self = mk_self m in
580 535
  let mem = mk_mem m in
581
  pp_spec
536
  pp_acsl
582 537
    (pp_predicate
583
       (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
584
       pp)
538
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
539
       (PrintSpec.pp_spec MemoryPackMode m))
585 540
    fmt
586
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
587
     v)
588

  
589
let print_ghost_simulation dependencies m fmt (i, instr) =
590
  let name = m.mname.node_id in
591
  let self = mk_self m in
592
  let mem = mk_mem m in
593
  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
594
  let pred pp v = pp_and prev_ghost pp fmt ((), v) in
595
  let rec aux fmt instr =
596
    match instr.instr_desc with
597
    | MStateAssign (m, _) ->
598
      pp_equal
599
        (pp_access pp_print_string (pp_access pp_print_string pp_var_decl))
600
        (pp_indirect pp_print_string (pp_access pp_print_string pp_var_decl))
601
        fmt
602
        ((mem, ("_reg", m)), (self, ("_reg", m)))
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 (_, i, _)
612
    | MReset i ->
613
      begin try
614
          let n, _ = List.assoc i m.minstances in
615
          pp_mem_ghost pp_access' pp_indirect' fmt
616
            (node_name n, (mem, i), (self, i))
617
        with Not_found -> pp_true fmt ()
618
      end
619
    | MBranch (_, brs) ->
620
      (* TODO: handle branches *)
621
      pp_and_l aux fmt List.(flatten (map snd brs))
622
    | _ -> pp_true fmt ()
623
  in
624
  pred aux instr
625

  
626
let print_machine_ghost_simulation dependencies m fmt i instr =
627
  print_machine_ghost_simulation_aux m
628
    (print_ghost_simulation dependencies m)
629
    ~i:(i+1)
630
    fmt (i, instr)
541
    ((mp, (name, mem), (name, self)),
542
     mp.mpformula)
631 543

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

  
635
let print_machine_ghost_simulations dependencies fmt m =
547
let pp_memory_pack_defs fmt m =
636 548
  if not (fst (get_stateless_status m)) then
637
    let name = m.mname.node_id in
638
    let self = mk_self m in
639
    let mem = mk_mem m in
640
    fprintf fmt "%a@,%a@,%a%a"
549
    fprintf fmt "%a@,%a"
641 550
      print_machine_ghost_struct m
642
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
643
      (pp_print_list_i
644
        ~pp_epilogue:pp_print_cut
645
        ~pp_open_box:pp_open_vbox0
646
        (print_machine_ghost_simulation dependencies m))
647
      m.mstep.step_instrs
648
      (print_machine_ghost_simulation_aux m
649
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
650

  
651
let print_machine_trans_simulation_aux ?i m pp fmt v =
652
  let name = m.mname.node_id in
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
653 558
  let mem_in = mk_mem_in m in
654 559
  let mem_out = mk_mem_out m in
655
  pp_spec
560
  pp_acsl
656 561
    (pp_predicate
657
       (pp_mem_trans pp_machine_decl pp_machine_decl
658
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
562
       (pp_transition m
563
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
659 564
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
660
          ?i)
661
       pp)
565
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
566
       (PrintSpec.pp_spec TransitionMode m))
662 567
    fmt
663
    ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
664
     v)
665

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

  
752
let print_machine_trans_annotations dependencies fmt m =
753
  set_live_of m;
754
  let i = List.length m.mstep.step_instrs in
755
  let mem_in = mk_mem_in m in
756
  let mem_out = mk_mem_out m in
757
  let last_trans fmt () =
758
    let locals = VDSet.(inter
759
                          (of_list m.mstep.step_locals)
760
                          (live_i m i)
761
                        |> elements) in
762
    if locals = []
763
    then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
764
    else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
765
        (locals, (m, mem_in, mem_out))
766
  in
767
  fprintf fmt "%a@,%a%a"
768
    (print_machine_trans_simulation_aux m pp_true ~i:0) ()
769
    (pp_print_list_i
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
770 674
       ~pp_epilogue:pp_print_cut
771 675
       ~pp_open_box:pp_open_vbox0
772
       (print_machine_trans_simulation dependencies m))
773
    m.mstep.step_instrs
774
    (print_machine_trans_simulation_aux m last_trans) ()
676
       (pp_transition_def m)) m.mspec.mtransitions
775 677

  
776 678
let print_machine_init_predicate fmt m =
777 679
  if not (fst (get_stateless_status m)) then
778 680
    let name = m.mname.node_id in
779 681
    let mem_in = mk_mem_in m in
780
    pp_spec
682
    pp_acsl
781 683
      (pp_predicate
782
         (pp_mem_init pp_machine_decl)
684
         (pp_initialization (pp_machine_decl' ~ghost:true))
783 685
         (pp_and_l (fun fmt (i, (td, _)) ->
784
              pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))
686
              pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
785 687
      fmt
786
      ((name, (name, "mem_ghost", mem_in)), m.minstances)
688
      ((name, (name, mem_in)), m.minstances)
787 689

  
788 690
let pp_at pp_p fmt (p, l) =
789 691
  fprintf fmt "\\at(%a, %s)" pp_p p l
......
793 695
let pp_at_pre pp_p fmt p =
794 696
  pp_at pp_p fmt (p, label_pre)
795 697

  
796
let pp_register =
698
let pp_register ?(indirect=true) ptr =
797 699
  pp_print_list
798
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
799
    ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
800
    ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
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 "."))
801 704
    (fun fmt (i, _) -> pp_print_string fmt i)
802 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

  
803 722
module HdrMod = struct
804 723

  
724
  module GhostProto = GhostProto
725

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

  
807 728
  let pp_import_standard_spec fmt () =
......
813 734

  
814 735
module SrcMod = struct
815 736

  
816
  let pp_predicates dependencies fmt machines =
737
  module GhostProto = GhostProto
738

  
739
  let pp_predicates (* dependencies *) fmt machines =
817 740
    fprintf fmt
818 741
      "%a%a%a%a"
819 742
      (pp_print_list
......
825 748
         ~pp_open_box:pp_open_vbox0
826 749
         ~pp_sep:pp_print_cutcut
827 750
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
828
         (print_machine_ghost_simulations dependencies)
751
         pp_memory_pack_defs
829 752
         ~pp_epilogue:pp_print_cutcut) machines
830 753
      (pp_print_list
831 754
         ~pp_open_box:pp_open_vbox0
......
837 760
         ~pp_open_box:pp_open_vbox0
838 761
         ~pp_sep:pp_print_cutcut
839 762
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
840
         (print_machine_trans_annotations dependencies)
763
         pp_transition_defs
841 764
         ~pp_epilogue:pp_print_cutcut) machines
842 765

  
843
  let pp_reset_spec fmt machines self m =
766
  let pp_clear_reset_spec fmt machines self mem m =
844 767
    let name = m.mname.node_id in
845
    let mem = mk_mem m in
846
    let insts = instances machines m in
847
    pp_spec_cut (fun fmt () ->
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 () ->
848 772
        fprintf fmt
849
          "%a@,%a@,%a@,%a"
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@]"
850 778
          (pp_requires pp_mem_valid') (name, self)
851
          (pp_requires (pp_separated self)) (powerset_instances insts, [])
852
          (pp_assigns pp_register) insts
853
          (pp_ensures
854
             (pp_forall
855
                pp_machine_decl
856
                (pp_implies
857
                   pp_mem_ghost'
858
                   pp_mem_init')))
859
          ((name, "mem_ghost", mem),
860
           ((name, mem, self), (name, mem))))
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
      )
861 795
      fmt ()
862 796

  
863
  let pp_step_spec fmt machines self m =
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 =
864 808
    let name = m.mname.node_id in
865
    let mem_in = mk_mem_in m in
866
    let mem_out = mk_mem_out m in
867 809
    let insts = instances machines m in
868 810
    let insts' = powerset_instances insts in
869
    pp_spec_cut (fun fmt () ->
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 () ->
870 817
        if fst (get_stateless_status m) then
871 818
          fprintf fmt
872 819
            "%a@,%a@,%a@,%a"
873
            (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
874
            (pp_requires pp_separated') m.mstep.step_outputs
875
            (pp_assigns pp_ptr_decl) m.mstep.step_outputs
876
            (pp_ensures  pp_mem_trans'') (m, mem_in, mem_out)
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, "", "")
877 825
        else
878 826
          fprintf fmt
879
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
880
            (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
827
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
828
            (pp_requires (pp_valid pp_var_decl)) outputs
881 829
            (pp_requires pp_mem_valid') (name, self)
882
            (pp_requires (pp_separated self)) (insts', m.mstep.step_outputs)
883
            (pp_assigns pp_ptr_decl) m.mstep.step_outputs
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
884 834
            (pp_assigns (pp_reg self)) m.mmemory
885
            (pp_assigns pp_memory) (memories insts')
886
            (pp_assigns pp_register) insts
887
            (pp_ensures
888
               (pp_forall
889
                  pp_machine_decl
890
                  (pp_forall
891
                     pp_machine_decl
892
                     (pp_implies
893
                        (pp_at_pre pp_mem_ghost')
894
                        (pp_implies
895
                           pp_mem_ghost'
896
                           pp_mem_trans'')))))
897
            ((name, "mem_ghost", mem_in),
898
             ((name, "mem_ghost", mem_out),
899
              ((name, mem_in, self),
900
               ((name, mem_out, self),
901
                (m, mem_in, mem_out)))))
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)
902 845
      )
903 846
      fmt ()
904 847

  
905
  let pp_step_instr_spec m self fmt (i, _instr) =
906
    let name = m.mname.node_id in
907
    let mem_in = mk_mem_in m in
908
    let mem_out = mk_mem_out m in
909
    if fst (get_stateless_status m) then
910
      fprintf fmt "@,%a"
911
        (pp_spec (pp_assert (pp_mem_trans'' ~i))) (m, mem_in, mem_out)
912
    else
913
      fprintf fmt "@,%a"
914
        (pp_spec
915
           (pp_assert
916
              (pp_forall
917
                 pp_machine_decl
918
                 (pp_forall
919
                    pp_machine_decl
920
                    (pp_implies
921
                       (pp_at_pre pp_mem_ghost')
922
                       (pp_implies
923
                          (pp_mem_ghost' ~i)
924
                          (pp_mem_trans'' ~i)))))))
925
        ((name, "mem_ghost", mem_in),
926
         ((name, "mem_ghost", mem_out),
927
          ((name, mem_in, self),
928
           ((name, mem_out, self),
929
            (m, mem_in, mem_out)))))
930

  
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"))))
931 859
end
932 860

  
933 861
(**************************************************************************)

Also available in: Unified diff