Project

General

Profile

Download (58.6 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
open Utils
12
open Format
13
open Lustre_types
14
open Machine_code_types
15
open C_backend_common
16
open Corelang
17
open Spec_types
18
open Machine_code_common
19
module Mpfr = Lustrec_mpfr
20

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

    
24
(**************************************************************************)
25

    
26
let pp_acsl_basic_type_desc t_desc =
27
  if Types.is_bool_type t_desc then
28
    (* if !Options.cpp then "bool" else "_Bool" *)
29
    "_Bool"
30
  else if Types.is_int_type t_desc then
31
    (* !Options.int_type *)
32
    if t_desc.tid = -1 then "int" else "integer"
33
  else if Types.is_real_type t_desc then
34
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
35
  else assert false
36
(* Not a basic C type. Do not handle arrays or pointers *)
37

    
38
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
39

    
40
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
41

    
42
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
43

    
44
let pp_acsl_line' ?(ghost = false) pp fmt x =
45
  let op = if ghost then "" else "*" in
46
  let cl = if ghost then "@" else "*" in
47
  fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
48

    
49
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
50

    
51
let pp_requires pp fmt = fprintf fmt "requires %a;" pp
52

    
53
let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
54

    
55
let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
56

    
57
let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
58

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

    
65
let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
66

    
67
let pp_assert pp fmt = fprintf fmt "assert %a;" pp
68

    
69
let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
70

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

    
74
let pp_mem_valid' = pp_mem_valid pp_print_string
75

    
76
let pp_ref pp fmt = fprintf fmt "&%a" pp
77

    
78
let pp_ref' = pp_ref pp_print_string
79

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

    
83
let pp_indirect' = pp_indirect pp_print_string pp_print_string
84

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

    
88
let pp_access' = pp_access pp_print_string pp_print_string
89

    
90
let pp_var_decl fmt v = pp_print_string fmt v.var_id
91

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

    
95
let pp_true fmt () = pp_print_string fmt "\\true"
96

    
97
let pp_cast pp_ty pp fmt (ty, x) = fprintf fmt "(%a) %a" pp_ty ty pp x
98

    
99
let pp_bool_cast pp fmt x = pp_cast pp_print_string pp fmt ("_Bool", x)
100

    
101
let pp_double_cast pp fmt x = pp_cast pp_print_string pp fmt ("double", x)
102

    
103
let pp_true_c_bool fmt () = pp_bool_cast pp_print_string fmt "1"
104

    
105
let pp_false fmt () = pp_print_string fmt "\\false"
106

    
107
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
108

    
109
let pp_null fmt () = pp_print_string fmt "\\null"
110

    
111
let pp_stdout fmt () = pp_print_string fmt "stdout"
112

    
113
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
114

    
115
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
116

    
117
let find_machine f = List.find (fun m -> m.mname.node_id = f)
118

    
119
let instances machines m =
120
  let open List in
121
  let grow paths i td mems =
122
    match paths with
123
    | [] ->
124
      [ [ i, (td, mems) ] ]
125
    | _ ->
126
      map (cons (i, (td, mems))) paths
127
  in
128
  let rec aux paths m =
129
    map
130
      (fun (i, (td, _)) ->
131
        try
132
          let m = find_machine (node_name td) machines in
133
          aux (grow paths i td m.mmemory) m
134
        with Not_found -> grow paths i td [])
135
      m.minstances
136
    |> flatten
137
  in
138
  aux [] m |> map rev
139

    
140
let memories insts =
141
  List.(
142
    map
143
      (fun path ->
144
        let _, (_, mems) = hd (rev path) in
145
        map (fun mem -> path, mem) mems)
146
      insts
147
    |> flatten)
148

    
149
let pp_instance ?(indirect = true) pp ptr =
150
  pp_print_list
151
    ~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
152
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
153
    (fun fmt (i, _) -> pp_print_string fmt i)
154

    
155
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
156
  pp_access
157
    ((if indirect then pp_indirect else pp_access)
158
       (pp_instance ~indirect pp_print_string ptr)
159
       pp_print_string)
160
    pp_var_decl
161
    fmt
162
    ((path, "_reg"), mem)
163

    
164
let prefixes l =
165
  let rec pref acc = function
166
    | x :: l ->
167
      pref ([ x ] :: List.map (List.cons x) acc) l
168
    | [] ->
169
      acc
170
  in
171
  pref [] (List.rev l)
172

    
173
let powerset_instances paths =
174
  List.map prefixes paths |> List.flatten |> remove_duplicates
175

    
176
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
177
  fprintf
178
    fmt
179
    "\\separated(@[<v>%a, %a%a%a@])"
180
    pp_self
181
    self
182
    pp_mem
183
    mem
184
    (pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))
185
    paths
186
    (pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
187
    ptrs
188

    
189
let pp_separated' self mem fmt (paths, ptrs) =
190
  pp_separated
191
    pp_print_string
192
    pp_print_string
193
    pp_var_decl
194
    fmt
195
    (self, mem, paths, ptrs)
196

    
197
let pp_separated'' =
198
  pp_comma_list
199
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
200
    ~pp_epilogue:pp_print_cpar
201
    pp_var_decl
202

    
203
let pp_forall pp_l pp_r fmt (l, r) =
204
  fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
205

    
206
let pp_exists pp_l pp_r fmt (l, r) =
207
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
208

    
209
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
210

    
211
let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r
212

    
213
let pp_implies pp_l pp_r fmt (l, r) =
214
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
215

    
216
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
217

    
218
let pp_and_l pp_v fmt =
219
  pp_print_list
220
    ~pp_open_box:pp_open_vbox0
221
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
222
    ~pp_nil:pp_true
223
    pp_v
224
    fmt
225

    
226
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
227

    
228
let pp_or_l pp_v fmt =
229
  pp_print_list
230
    ~pp_open_box:pp_open_vbox0
231
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
232
    pp_v
233
    fmt
234

    
235
let pp_not pp fmt = fprintf fmt "!%a" pp
236

    
237
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
238

    
239
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
240

    
241
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
242

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

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

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

    
251
let pp_init pp_mem fmt (name, mem) = fprintf fmt "%s_init(%a)" name pp_mem mem
252

    
253
let pp_initialization' = pp_initialization pp_print_string
254

    
255
let pp_local m =
256
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
257

    
258
let pp_locals m =
259
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
260

    
261
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
262

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

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

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

    
325
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
326
  pp_memory_pack_aux
327
    ?i:mp.mpindex
328
    pp_mem
329
    pp_self
330
    fmt
331
    (mp.mpname.node_id, mem, self)
332

    
333
let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt
334
    (name, vars, mem_in, mem_out) =
335
  fprintf
336
    fmt
337
    "%s_transition%a(@[<hov>%t%a%t@])"
338
    name
339
    (pp_print_option pp_print_int)
340
    i
341
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
342
    (pp_comma_list
343
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
344
       pp_var)
345
    vars
346
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
347

    
348
let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out)
349
    =
350
  pp_transition_aux
351
    ?i:t.tindex
352
    stateless
353
    pp_mem_in
354
    pp_mem_out
355
    pp_var
356
    fmt
357
    (t.tname.node_id, t.tvars, mem_in, mem_out)
358

    
359
let pp_transition_aux' ?i m =
360
  let stateless = fst (get_stateless_status m) in
361
  pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->
362
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
363

    
364
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
365
  fprintf
366
    fmt
367
    "%s_reset_cleared(@[<hov>%a,@ %a@])"
368
    name
369
    pp_mem_in
370
    mem_in
371
    pp_mem_out
372
    mem_out
373

    
374
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
375

    
376
let pp_functional_update mems insts fmt mem =
377
  let rec aux fmt = function
378
    | [] ->
379
      pp_print_string fmt mem
380
    | (x, is_mem) :: fields ->
381
      fprintf
382
        fmt
383
        "{ @[<hov>%a@ \\with .%s%s = %s@] }"
384
        aux
385
        fields
386
        (if is_mem then "_reg." else "")
387
        x
388
        x
389
  in
390
  aux
391
    fmt
392
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
393
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
394

    
395
module PrintSpec = struct
396
  type mode =
397
    | MemoryPackMode
398
    | TransitionMode
399
    | TransitionFootprintMode
400
    | ResetIn
401
    | ResetOut
402
    | InstrMode of ident
403

    
404
  let pp_reg mem fmt = function
405
    | ResetFlag ->
406
      fprintf fmt "%s.%s" mem reset_flag_name
407
    | StateVar x ->
408
      fprintf fmt "%s.%a" mem pp_var_decl x
409

    
410
  let not_var v = match v.value_desc with
411
    | Var _ -> false
412
    | _ -> true
413

    
414
  let pp_expr ?(test_output = false) m mem fmt = function
415
    | Val v ->
416
      let pp = pp_c_val ~indirect:false m mem (pp_c_var_read ~test_output m) in
417
      (if not_var v
418
       then if Types.is_bool_type v.value_type
419
         then pp_bool_cast pp
420
         else if Types.is_real_type v.value_type
421
         then pp_double_cast pp
422
         else pp
423
       else pp) fmt v
424
    | Tag t ->
425
      pp_print_string fmt t
426
    | Var v ->
427
      pp_var_decl fmt v
428
    | Memory r ->
429
      pp_reg mem fmt r
430

    
431
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
432
    let test_output, mem_update =
433
      match mode with
434
      | InstrMode _ ->
435
        true, false
436
      | TransitionFootprintMode ->
437
        false, true
438
      | _ ->
439
        false, false
440
    in
441
    let pp_expr test_output fmt e = pp_expr ~test_output m mem_out fmt e in
442
    match p with
443
    | Transition (stateless, f, inst, i, vars, r, mems, insts) ->
444
      let pp_mem_in, pp_mem_out =
445
        match inst with
446
        | None ->
447
          ( pp_print_string,
448
            if mem_update then pp_functional_update mems insts
449
            else pp_print_string )
450
        | Some inst ->
451
          ( (fun fmt mem_in ->
452
              if r then pp_print_string fmt mem_in
453
              else pp_access' fmt (mem_in, inst)),
454
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
455
      in
456
      pp_transition_aux
457
        ?i
458
        stateless
459
        pp_mem_in
460
        pp_mem_out
461
        (pp_expr test_output)
462
        fmt
463
        (f, vars, mem_in', mem_out')
464
    | Reset (_f, inst, r) ->
465
      pp_ite
466
        (pp_c_val m mem_in (pp_c_var_read m))
467
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
468
        (pp_equal pp_print_string pp_access')
469
        fmt
470
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
471
    | MemoryPack (f, inst, i) ->
472
      let pp_mem, pp_self =
473
        match inst with
474
        | None ->
475
          pp_print_string, pp_print_string
476
        | Some inst ->
477
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
478
            fun fmt self -> pp_indirect' fmt (self, inst) )
479
      in
480
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
481
    | ResetCleared f ->
482
      pp_reset_cleared' fmt (f, mem_in, mem_out)
483
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
484
    | Initialization ->
485
      ()
486

    
487
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
488

    
489
  let val_of_expr = function
490
    | Val v ->
491
      v
492
    | Tag t ->
493
      id_to_tag t
494
    | Var v ->
495
      vdecl_to_val v
496
    | Memory (StateVar v) ->
497
      vdecl_to_val v
498
    | Memory ResetFlag ->
499
      vdecl_to_val reset_flag
500

    
501
  let find_arrow loc m =
502
    match List.find_opt (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances with
503
    | Some (f, _) -> Some f
504
    | None ->
505
      Error.pp_warning loc
506
        (fun fmt -> pp_print_string fmt "Generating stateful spec for uninitialized state variables.");
507
      None
508

    
509
  let rec has_memory_val m v =
510
    let has_mem = has_memory_val m in
511
    match v.value_desc with
512
    | Var v ->
513
      is_memory m v
514
    | Array vl | Fun (_, vl) ->
515
      List.exists has_mem vl
516
    | Access (t, i) | Power (t, i) ->
517
      has_mem t || has_mem i
518
    | _ ->
519
      false
520

    
521
  let has_memory m = function Val v -> has_memory_val m v | _ -> false
522

    
523
  let pp_spec mode m =
524
    let rec pp_spec mode fmt f =
525
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
526
        let self = mk_self m in
527
        let mem = mk_mem m in
528
        let mem_in = mk_mem_in m in
529
        let mem_out = mk_mem_out m in
530
        let mem_reset = mk_mem_reset m in
531
        match mode with
532
        | MemoryPackMode ->
533
          self, self, true, mem, mem, false
534
        | TransitionMode ->
535
          mem_in, mem_in, false, mem_out, mem_out, false
536
        | TransitionFootprintMode ->
537
          mem_in, mem_in, false, mem_out, mem_out, false
538
        | ResetIn ->
539
          mem_reset, mem_reset, false, mem_out, mem_out, false
540
        | ResetOut ->
541
          mem_in, mem_in, false, mem_reset, mem_reset, false
542
        | InstrMode self ->
543
          let mem = "(*" ^ mem ^ ")" in
544
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
545
          self, flush_str_formatter (), false, mem, mem, false
546
      in
547
      let pp_expr fmt e = pp_expr m mem_out fmt e in
548
      let pp_spec' = pp_spec mode in
549
      match f with
550
      | True ->
551
        pp_true fmt ()
552
      | False ->
553
        pp_false fmt ()
554
      | Equal (a, b) ->
555
        let pp_eq fmt () =
556
          pp_assign_spec
557
            m
558
            mem_out
559
            (pp_c_var_read ~test_output:false m)
560
            indirect_l
561
            mem_in
562
            (pp_c_var_read ~test_output:false m)
563
            indirect_r
564
            fmt
565
            (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
566
        in
567
        if has_memory m b then
568
          let inst = find_arrow Location.dummy m in
569
          pp_print_option
570
            ~none:pp_eq
571
            (fun fmt inst ->
572
               pp_paren
573
                 (pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
574
                 fmt
575
                 ((Arrow.arrow_id, (mem_in, inst)), ()))
576
            fmt inst
577
        else pp_eq fmt ()
578
      | GEqual (a, b) ->
579
        pp_assign_spec ~pp_op:pp_gequal
580
          m
581
          mem_out
582
          (pp_c_var_read ~test_output:false m)
583
          indirect_l
584
          mem_in
585
          (pp_c_var_read ~test_output:false m)
586
          indirect_r
587
          fmt
588
          (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
589
      | And fs ->
590
        pp_and_l pp_spec' fmt fs
591
      | Or fs ->
592
        pp_or_l pp_spec' fmt fs
593
      | Imply (a, b) ->
594
        pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
595
      | Exists (xs, a) ->
596
        pp_exists (pp_locals m) pp_spec' fmt (xs, a)
597
      | Forall (xs, a) ->
598
        pp_forall (pp_locals m) pp_spec' fmt (xs, a)
599
      | Ternary (e, a, b) ->
600
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
601
      | Predicate p ->
602
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
603
      | StateVarPack ResetFlag ->
604
        let r = vdecl_to_val reset_flag in
605
        pp_assign_spec
606
          m
607
          mem_out
608
          (pp_c_var_read ~test_output:false m)
609
          indirect_l
610
          mem_in
611
          (pp_c_var_read ~test_output:false m)
612
          indirect_r
613
          fmt
614
          (Type_predef.type_bool, r, r)
615
      | StateVarPack (StateVar v) ->
616
        let v' = vdecl_to_val v in
617
        let pp_eq fmt () =
618
          pp_assign_spec
619
            m
620
            mem_out
621
            (pp_c_var_read ~test_output:false m)
622
            indirect_l
623
            mem_in
624
            (pp_c_var_read ~test_output:false m)
625
            indirect_r
626
            fmt
627
            (v.var_type, v', v')
628
        in
629
        let inst = find_arrow Location.dummy m in
630
        pp_print_option
631
          ~none:pp_eq
632
          (fun fmt inst ->
633
             pp_paren
634
               (pp_implies
635
                  (pp_not (pp_initialization pp_access'))
636
                  pp_eq)
637
               fmt
638
               ((Arrow.arrow_id, (mem_out, inst)), ()))
639
          fmt inst
640
      | ExistsMem (f, rc, tr) ->
641
        pp_exists
642
          (pp_machine_decl' ~ghost:true)
643
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
644
          fmt
645
          ((f, mk_mem_reset m), (rc, tr))
646
      | Value v ->
647
        pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
648
    in
649

    
650
    pp_spec mode
651
end
652

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

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

    
659
let pp_axiomatic pp_l pp_r fmt (l, r) =
660
  fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
661

    
662
let pp_axiom pp_l pp_r fmt (l, r) =
663
  fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
664

    
665
let pp_mem_valid_def fmt m =
666
  if not (fst (get_stateless_status m) || m.mis_contract) then
667
    let name = m.mname.node_id in
668
    let self = mk_self m in
669
    pp_acsl
670
      (pp_predicate
671
         (pp_mem_valid (pp_machine_decl pp_ptr))
672
         (pp_and
673
            (pp_and_l (fun fmt (inst, (td, _)) ->
674
                 if Arrow.td_is_arrow td then
675
                   pp_valid pp_indirect' fmt [ self, inst ]
676
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
677
            (pp_valid pp_print_string)))
678
      fmt
679
      ((name, (name, self)), (m.minstances, [ self ]))
680

    
681
let pp_memory_pack_def m fmt mp =
682
  if not (fst (get_stateless_status m) || m.mis_contract) then
683
    let name = mp.mpname.node_id in
684
    let self = mk_self m in
685
    let mem = mk_mem m in
686
    pp_acsl_cut
687
      (pp_predicate
688
         (pp_memory_pack
689
            (pp_machine_decl' ~ghost:true)
690
            (pp_machine_decl pp_ptr))
691
         (PrintSpec.pp_spec MemoryPackMode m))
692
      fmt
693
      ((mp, (name, mem), (name, self)), mp.mpformula)
694

    
695
let pp_machine_ghost_struct fmt m =
696
  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
697

    
698
let pp_memory_pack_defs fmt m =
699
  if not (fst (get_stateless_status m)) then
700
    fprintf
701
      fmt
702
      "%a@,%a"
703
      pp_machine_ghost_struct
704
      m
705
      (pp_print_list
706
         ~pp_sep:pp_print_nothing
707
         ~pp_epilogue:pp_print_cut
708
         ~pp_open_box:pp_open_vbox0
709
         (pp_memory_pack_def m))
710
      m.mspec.mmemory_packs
711

    
712
let pp_transition_def m fmt t =
713
  let name = t.tname.node_id in
714
  let mem_in = mk_mem_in m in
715
  let mem_out = mk_mem_out m in
716
  let stateless = fst (get_stateless_status m) in
717
  pp_acsl
718
    (pp_predicate
719
       (pp_transition
720
          stateless
721
          (pp_machine_decl' ~ghost:true)
722
          (pp_machine_decl' ~ghost:true)
723
          (pp_local m))
724
       (PrintSpec.pp_spec TransitionMode m))
725
    fmt
726
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
727

    
728
let pp_transition_defs fmt m =
729
  pp_print_list
730
    ~pp_epilogue:pp_print_cut
731
    ~pp_open_box:pp_open_vbox0
732
    (pp_transition_def m)
733
    fmt
734
    m.mspec.mtransitions
735

    
736
let pp_transition_footprint fmt t =
737
  fprintf
738
    fmt
739
    "%s_transition%a_footprint"
740
    t.tname.node_id
741
    (pp_print_option pp_print_int)
742
    t.tindex
743

    
744
let pp_transition_footprint_lemma m fmt t =
745
  let name = t.tname.node_id in
746
  let mem_in = mk_mem_in m in
747
  let mem_out = mk_mem_out m in
748
  let stateless = fst (get_stateless_status m) in
749
  let mems =
750
    ISet.(
751
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
752
  in
753
  let insts =
754
    IMap.(
755
      diff
756
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
757
        t.tinst_footprint)
758
  in
759
  let memories =
760
    List.map
761
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
762
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
763
  in
764
  let mems_empty = ISet.is_empty mems in
765
  let insts_empty = IMap.is_empty insts in
766
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
767
  let tr ?mems ?insts () =
768
    Spec_common.mk_transition
769
      ?mems
770
      ?insts
771
      ?i:t.tindex
772
      stateless
773
      name
774
      (vdecls_to_vals t.tvars)
775
  in
776
  if not ((mems_empty && insts_empty) || m.mis_contract) then
777
    pp_acsl_cut
778
      (pp_lemma
779
         pp_transition_footprint
780
         (pp_forall
781
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
782
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
783
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
784
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
785
                else pp_forall (pp_locals m))
786
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
787
      fmt
788
      ( t,
789
        ( (m.mname.node_id, [ mem_in; mem_out ]),
790
          ( instances,
791
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
792
      )
793

    
794
let pp_transition_footprint_lemmas fmt m =
795
  pp_print_list
796
    ~pp_epilogue:pp_print_cut
797
    ~pp_open_box:pp_open_vbox0
798
    ~pp_sep:pp_print_nothing
799
    (pp_transition_footprint_lemma m)
800
    fmt
801
    (List.filter
802
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
803
       m.mspec.mtransitions)
804

    
805
let pp_initialization_def fmt m =
806
  if not (fst (get_stateless_status m)) then
807
    let name = m.mname.node_id in
808
    let mem_in = mk_mem_in m in
809
    pp_acsl
810
      (pp_predicate
811
         (pp_initialization (pp_machine_decl' ~ghost:true))
812
         (pp_and_l (fun fmt (i, (td, _)) ->
813
              if Arrow.td_is_arrow td then
814
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
815
              else
816
                pp_equal
817
                  (pp_reset_flag ~indirect:false pp_access')
818
                  pp_print_int
819
                  fmt
820
                  ((mem_in, i), 1))))
821
      fmt
822
      ((name, (name, mem_in)), m.minstances)
823

    
824
let pp_reset_cleared_def fmt m =
825
  if not (fst (get_stateless_status m)) then
826
    let name = m.mname.node_id in
827
    let mem_in = mk_mem_in m in
828
    let mem_out = mk_mem_out m in
829
    pp_acsl
830
      (pp_predicate
831
         (pp_reset_cleared
832
            (pp_machine_decl' ~ghost:true)
833
            (pp_machine_decl' ~ghost:true))
834
         (pp_ite
835
            (pp_reset_flag' ~indirect:false)
836
            (pp_and
837
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
838
               pp_initialization')
839
            (pp_equal pp_print_string pp_print_string)))
840
      fmt
841
      ( (name, (name, mem_in), (name, mem_out)),
842
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
843

    
844
let pp_register_chain ?(indirect = true) ptr =
845
  pp_print_list
846
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
847
    ~pp_epilogue:(fun fmt () ->
848
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
849
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
850
    (fun fmt (i, _) -> pp_print_string fmt i)
851

    
852
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
853
  pp_print_list
854
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
855
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
856
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
857
    (fun fmt (i, _) -> pp_print_string fmt i)
858
    fmt
859
    mems
860

    
861
let pp_arrow_reset_ghost mem fmt inst =
862
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
863

    
864
module GhostProto : MODIFIERS_GHOST_PROTO = struct
865
  let pp_ghost_parameters ?(cut = true) fmt vs =
866
    fprintf
867
      fmt
868
      "%a%a"
869
      (if cut then pp_print_cut else pp_print_nothing)
870
      ()
871
      (pp_acsl_line'
872
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
873
      vs
874
end
875

    
876
module HdrMod = struct
877
  module GhostProto = GhostProto
878

    
879
  let pp_machine_decl_prefix _ _ = ()
880

    
881
  let pp_import_arrow fmt () =
882
    fprintf
883
      fmt
884
      "#include \"%s/arrow_spec.h%s\""
885
      (Arrow.arrow_top_decl ()).top_decl_owner
886
      (if !Options.cpp then "pp" else "")
887

    
888
  let pp_predicates fmt machines =
889
    let pp_preds comment pp =
890
      pp_print_list
891
        ~pp_open_box:pp_open_vbox0
892
        ~pp_prologue:(pp_print_endcut comment)
893
        pp
894
        ~pp_epilogue:pp_print_cutcut
895
    in
896
    fprintf
897
      fmt
898
      "%a%a"
899
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
900
      machines
901
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
902
      machines
903

    
904
  let pp_machine_alloc_decl fmt m =
905
    pp_machine_decl_prefix fmt m;
906
    if not (fst (get_stateless_status m)) then
907
      if !Options.static_mem then
908
        (* Static allocation *)
909
        let macro = m, mk_attribute m, mk_instance m in
910
        fprintf
911
          fmt
912
          "%a@,%a@,%a"
913
          (pp_static_declare_macro ~ghost:true)
914
          macro
915
          (pp_static_link_macro ~ghost:true)
916
          macro
917
          (pp_static_alloc_macro ~ghost:true)
918
          macro
919
      else
920
        (* Dynamic allocation *)
921
        (* TODO: handle dynamic alloc *)
922
        assert false
923
  (* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
924
   *   (m.mname.node_id, m.mstatic)
925
   *   pp_dealloc_prototype m.mname.node_id *)
926
end
927

    
928
module SrcMod = struct
929
  module GhostProto = GhostProto
930

    
931
  let pp_predicates fmt machines =
932
    let pp_preds comment pp =
933
      pp_print_list
934
        ~pp_open_box:pp_open_vbox0
935
        ~pp_prologue:(pp_print_endcut comment)
936
        pp
937
        ~pp_epilogue:pp_print_cutcut
938
    in
939
    fprintf
940
      fmt
941
      "%a%a%a%a%a%a"
942
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
943
      machines
944
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
945
      machines
946
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
947
      machines
948
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
949
      machines
950
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
951
      machines
952
      (pp_preds
953
         "/* ACSL transition memory footprints lemmas */"
954
         pp_transition_footprint_lemmas)
955
      machines
956

    
957
  let pp_clear_reset_spec fmt self mem m =
958
    let name = m.mname.node_id in
959
    let arws, narws =
960
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
961
    in
962
    let mk_insts = List.map (fun x -> [ x ]) in
963
    pp_acsl_cut
964
      (fun fmt () ->
965
        fprintf
966
          fmt
967
          "%a@,\
968
           %a@,\
969
           %a@,\
970
           %a@,\
971
           %a@,\
972
           %a@,\
973
           %a@,\
974
           %a@,\
975
           %a@,\
976
           %a@,\
977
           @[<v 2>behavior reset:@;\
978
           %a@,\
979
           %a@]@,\
980
           @[<v 2>behavior no_reset:@;\
981
           %a@,\
982
           %a@]@,\
983
           complete behaviors;@,\
984
           disjoint behaviors;"
985
          (pp_requires pp_mem_valid')
986
          (name, self)
987
          (pp_requires (pp_separated' self mem))
988
          (mk_insts m.minstances, [])
989
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
990
          (name, mem, self)
991
          (pp_ensures
992
             (pp_memory_pack_aux
993
                ~i:(List.length m.mspec.mmemory_packs - 2)
994
                pp_ptr
995
                pp_print_string))
996
          (name, mem, self)
997
          (pp_assigns pp_reset_flag')
998
          [ self ]
999
          (pp_assigns (pp_register_chain self))
1000
          (mk_insts arws)
1001
          (pp_assigns (pp_reset_flag_chain self))
1002
          (mk_insts narws)
1003
          (pp_assigns pp_reset_flag')
1004
          [ mem ]
1005
          (pp_assigns (pp_register_chain ~indirect:false mem))
1006
          (mk_insts arws)
1007
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1008
          (mk_insts narws)
1009
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
1010
          (mem, 1)
1011
          (pp_ensures (pp_initialization pp_ptr))
1012
          (name, mem)
1013
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
1014
          (mem, 0)
1015
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
1016
          (mem, mem))
1017
      fmt
1018
      ()
1019

    
1020
  let pp_set_reset_spec fmt self mem m =
1021
    let name = m.mname.node_id in
1022
    pp_acsl_cut
1023
      (fun fmt () ->
1024
        fprintf
1025
          fmt
1026
          "%a@,%a@,%a"
1027
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
1028
          (name, mem, self)
1029
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
1030
          (mem, 1)
1031
          (pp_assigns pp_reset_flag')
1032
          [ self; mem ])
1033
      fmt
1034
      ()
1035

    
1036
  let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
1037

    
1038
  let pp_contract m fmt c =
1039
    PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
1040

    
1041
  let contract_of machines m =
1042
    match m.mspec.mnode_spec with
1043
    | Some spec -> (
1044
      match spec with
1045
      | Contract c ->
1046
        Some c, None
1047
      | NodeSpec f -> (
1048
        let m_f = find_machine f machines in
1049
        match m_f.mspec.mnode_spec with
1050
        | Some (Contract c) ->
1051
          Some c, Some m_f
1052
        | _ ->
1053
          None, None))
1054
    | None ->
1055
      None, None
1056

    
1057
  let pp_init_def fmt m =
1058
    let name = m.mname.node_id in
1059
    let mem = mk_mem m in
1060
    pp_predicate
1061
      (pp_init (pp_machine_decl' ~ghost:true))
1062
      (pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
1063
      fmt
1064
      ((name, (name, mem)), ((name, mem), mem))
1065

    
1066
  let rename n x = sprintf "%s_%d" x n
1067

    
1068
  let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
1069

    
1070
  let rec rename_value n v =
1071
    {
1072
      v with
1073
      value_desc =
1074
        (match v.value_desc with
1075
        | Machine_code_types.Var v ->
1076
          Machine_code_types.Var (rename_var_decl n v)
1077
        | Fun (f, vs) ->
1078
          Fun (f, List.map (rename_value n) vs)
1079
        | Array vs ->
1080
          Array (List.map (rename_value n) vs)
1081
        | Access (v1, v2) ->
1082
          Access (rename_value n v1, rename_value n v2)
1083
        | Power (v1, v2) ->
1084
          Power (rename_value n v1, rename_value n v2)
1085
        | v ->
1086
          v);
1087
    }
1088

    
1089
  let rename_expression n = function
1090
    | Val v ->
1091
      Val (rename_value n v)
1092
    | Var v ->
1093
      Var (rename_var_decl n v)
1094
    | e ->
1095
      e
1096

    
1097
  let rename_predicate n = function
1098
    | Transition (s, f, inst, i, es, r, mf, mif) ->
1099
      Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif)
1100
    | p ->
1101
      p
1102

    
1103
  let rec rename_formula n = function
1104
    | Equal (e1, e2) ->
1105
      Equal (rename_expression n e1, rename_expression n e2)
1106
    | And fs ->
1107
      And (List.map (rename_formula n) fs)
1108
    | Or fs ->
1109
      Or (List.map (rename_formula n) fs)
1110
    | Imply (f1, f2) ->
1111
      Imply (rename_formula n f1, rename_formula n f2)
1112
    | Exists (xs, f) ->
1113
      Exists (List.map (rename_var_decl n) xs, rename_formula n f)
1114
    | Forall (xs, f) ->
1115
      Forall (List.map (rename_var_decl n) xs, rename_formula n f)
1116
    | Ternary (e, t, f) ->
1117
      Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
1118
    | Predicate p ->
1119
      Predicate (rename_predicate n p)
1120
    | ExistsMem (x, f1, f2) ->
1121
      ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
1122
    | Value v ->
1123
      Value (rename_value n v)
1124
    | f ->
1125
      f
1126

    
1127
  let rename_contract n c =
1128
    {
1129
      c with
1130
      mc_pre = rename_formula n c.mc_pre;
1131
      mc_post = rename_formula n c.mc_post;
1132
    }
1133

    
1134
  let but_last l = List.(rev (tl (rev l)))
1135

    
1136
  let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt
1137
      (n, mem_in, mem_out) =
1138
    let name = m.mname.node_id in
1139
    let inputs = m.mstep.step_inputs in
1140
    let outputs = m.mstep.step_outputs in
1141
    fprintf
1142
      fmt
1143
      "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
1144
      name
1145
      case
1146
      n
1147
      pp_mem_in
1148
      mem_in
1149
      pp_vars
1150
      (inputs @ outputs)
1151
      pp_mem_out
1152
      mem_out
1153

    
1154
  let pp_k_induction_base_case m = pp_k_induction_case "base" m
1155

    
1156
  let pp_k_induction_inductive_case m = pp_k_induction_case "inductive" m
1157

    
1158
  let pp_base_cases m fmt (c, m_c, k) =
1159
    let name = m.mname.node_id in
1160
    let name_c = m_c.mname.node_id in
1161
    let mem = mk_mem m in
1162
    let mem_c = mk_mem_c m in
1163
    let inputs = m.mstep.step_inputs in
1164
    let outputs = m.mstep.step_outputs in
1165
    let stateless = fst (get_stateless_status m) in
1166
    let stateless_c = fst (get_stateless_status m_c) in
1167
    let l = List.init (k - 1) (fun n -> n + 1) in
1168
    pp_print_list
1169
      ~pp_open_box:pp_open_vbox0
1170
      ~pp_sep:pp_print_cutcut
1171
      (fun fmt n ->
1172
        let l = List.init (n + 1) (fun n -> n) in
1173
        let pp fmt =
1174
          let pp =
1175
            pp_implies
1176
              (pp_and_l (fun fmt -> function
1177
                 | 0 ->
1178
                   let pp = pp_init pp_print_string in
1179
                   (if stateless_c then fun fmt (x, _) -> pp fmt x
1180
                   else pp_and pp pp)
1181
                     fmt
1182
                     ((name, rename 0 mem), (name_c, rename 0 mem_c))
1183
                 | n' ->
1184
                   let pp_var_c fmt (out, vd) =
1185
                     if out && n' < n then pp_true_c_bool fmt ()
1186
                     else pp_var_decl fmt vd
1187
                   in
1188
                   let c_inputs =
1189
                     List.map
1190
                       (fun v -> false, rename_var_decl n' v)
1191
                       m_c.mstep.step_inputs
1192
                   in
1193
                   let c_outputs =
1194
                     List.map
1195
                       (fun v -> true, rename_var_decl n' v)
1196
                       m_c.mstep.step_outputs
1197
                   in
1198
                   let pp stateless pp_var =
1199
                     pp_transition_aux
1200
                       stateless
1201
                       pp_print_string
1202
                       pp_print_string
1203
                       pp_var
1204
                   in
1205
                   pp_and
1206
                     (pp stateless pp_var_decl)
1207
                     (pp stateless_c pp_var_c)
1208
                     fmt
1209
                     ( ( name,
1210
                         List.map (rename_var_decl n') (inputs @ outputs),
1211
                         rename (n' - 1) mem,
1212
                         rename n' mem ),
1213
                       ( name_c,
1214
                         c_inputs @ c_outputs,
1215
                         rename (n' - 1) mem_c,
1216
                         rename n' mem_c ) )))
1217
              (pp_contract m)
1218
          in
1219
          if stateless_c then pp fmt
1220
          else fun x ->
1221
            pp_forall
1222
              (pp_machine_decl
1223
                 ~ghost:true
1224
                 (pp_comma_list (fun fmt n ->
1225
                      pp_print_string fmt (rename n mem_c))))
1226
              pp
1227
              fmt
1228
              ((name_c, l), x)
1229
        in
1230
        pp_predicate
1231
          (pp_k_induction_base_case
1232
             m
1233
             (pp_machine_decl' ~ghost:true)
1234
             (pp_machine_decl' ~ghost:true)
1235
             (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
1236
          (pp_forall
1237
             (pp_locals m)
1238
             (if n > 1 then
1239
              pp_forall
1240
                (fun fmt l ->
1241
                  fprintf
1242
                    fmt
1243
                    "%a@,%a"
1244
                    (pp_machine_decl
1245
                       ~ghost:true
1246
                       (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
1247
                            pp_print_string fmt (rename n mem))))
1248
                    (name, but_last l)
1249
                    (pp_locals m)
1250
                    (List.flatten
1251
                       (List.map
1252
                          (fun n ->
1253
                            List.map (rename_var_decl n) (inputs @ outputs))
1254
                          (List.tl l))))
1255
                pp
1256
             else fun fmt (_, x) -> pp fmt x))
1257
          fmt
1258
          ( (n, (name, rename (n - 1) mem), (name, rename n mem)),
1259
            ( List.map (rename_var_decl n) m_c.mstep.step_outputs,
1260
              (but_last l, (l, rename_contract n c)) ) ))
1261
      fmt
1262
      l
1263

    
1264
  let pp_inductive_case m fmt (c, m_c, k) =
1265
    let name = m.mname.node_id in
1266
    let mem = mk_mem m in
1267
    let mem_c = mk_mem_c m_c in
1268
    let inputs = m.mstep.step_inputs in
1269
    let outputs = m.mstep.step_outputs in
1270
    let stateless = fst (get_stateless_status m) in
1271
    let stateless_c = fst (get_stateless_status m_c) in
1272
    let l = List.init k (fun n -> n + 1) in
1273
    let l' = 0 :: l in
1274
    let pp fmt =
1275
      let pp =
1276
        pp_implies
1277
          (pp_and_l (fun fmt n ->
1278
               let pp_var_c fmt (out, vd) =
1279
                 if out && n < k then pp_true_c_bool fmt ()
1280
                 else pp_var_decl fmt vd
1281
               in
1282
               let c_inputs =
1283
                 List.map
1284
                   (fun v -> false, rename_var_decl n v)
1285
                   m_c.mstep.step_inputs
1286
               in
1287
               let c_outputs =
1288
                 List.map
1289
                   (fun v -> true, rename_var_decl n v)
1290
                   m_c.mstep.step_outputs
1291
               in
1292
               pp_and
1293
                 (pp_transition_aux
1294
                    stateless
1295
                    pp_print_string
1296
                    pp_print_string
1297
                    pp_var_decl)
1298
                 (pp_transition_aux
1299
                    stateless_c
1300
                    pp_print_string
1301
                    pp_print_string
1302
                    pp_var_c)
1303
                 fmt
1304
                 ( ( name,
1305
                     List.map (rename_var_decl n) (inputs @ outputs),
1306
                     rename (n - 1) mem,
1307
                     rename n mem ),
1308
                   ( m_c.mname.node_id,
1309
                     c_inputs @ c_outputs,
1310
                     rename (n - 1) mem_c,
1311
                     rename n mem_c ) )))
1312
          (pp_contract m)
1313
      in
1314
      if stateless_c then pp fmt
1315
      else fun x ->
1316
        pp_forall
1317
          (pp_machine_decl
1318
             ~ghost:true
1319
             (pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
1320
          pp
1321
          fmt
1322
          ((m_c.mname.node_id, l'), x)
1323
    in
1324
    pp_predicate
1325
      (pp_k_induction_inductive_case
1326
         m
1327
         (pp_machine_decl' ~ghost:true)
1328
         (pp_machine_decl' ~ghost:true)
1329
         (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
1330
      (pp_forall
1331
         (pp_locals m)
1332
         (if k > 1 then
1333
          pp_forall
1334
            (fun fmt l ->
1335
              fprintf
1336
                fmt
1337
                "%a@,%a"
1338
                (pp_machine_decl
1339
                   ~ghost:true
1340
                   (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
1341
                        pp_print_string fmt (rename (n - 1) mem))))
1342
                (name, but_last l)
1343
                (pp_locals m)
1344
                (List.flatten
1345
                   (List.map
1346
                      (fun n ->
1347
                        List.map (rename_var_decl (n - 1)) (inputs @ outputs))
1348
                      (List.tl l))))
1349
            pp
1350
         else fun fmt (_, x) -> pp fmt x))
1351
      fmt
1352
      ( (k, (name, rename (k - 1) mem), (name, rename k mem)),
1353
        ( List.map (rename_var_decl k) m_c.mstep.step_outputs,
1354
          (l, (l, rename_contract k c)) ) )
1355

    
1356
  let pp_k_induction_lemmas m fmt k =
1357
    let name = m.mname.node_id in
1358
    let mem_in = mk_mem_in m in
1359
    let mem_out = mk_mem_out m in
1360
    let inputs = m.mstep.step_inputs in
1361
    let outputs = m.mstep.step_outputs in
1362
    let l = List.init k (fun n -> n + 1) in
1363
    pp_print_list
1364
      ~pp_open_box:pp_open_vbox0
1365
      ~pp_sep:pp_print_cutcut
1366
      (fun fmt n ->
1367
        pp_lemma
1368
          (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
1369
          (pp_forall
1370
             (fun fmt () ->
1371
               fprintf
1372
                 fmt
1373
                 "%a,@;%a"
1374
                 (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1375
                 (name, [ mem_in; mem_out ])
1376
                 (pp_locals m)
1377
                 (inputs @ outputs))
1378
             ((if n = k then pp_k_induction_inductive_case
1379
              else pp_k_induction_base_case)
1380
                m
1381
                pp_print_string
1382
                pp_print_string
1383
                (pp_comma_list pp_var_decl)))
1384
          fmt
1385
          (n, ((), (n, mem_in, mem_out))))
1386
      fmt
1387
      l
1388

    
1389
  let pp_k_induction_axiom m fmt (c, m_c, k) =
1390
    let name = m.mname.node_id in
1391
    let mem_in = mk_mem_in m in
1392
    let mem_out = mk_mem_out m in
1393
    let mem_in_c = mk_mem_in_c m_c in
1394
    let mem_out_c = mk_mem_out_c m_c in
1395
    let inputs = m.mstep.step_inputs in
1396
    let outputs = m.mstep.step_outputs in
1397
    let stateless = fst (get_stateless_status m) in
1398
    let stateless_c = fst (get_stateless_status m_c) in
1399
    let l = List.init k (fun n -> n + 1) in
1400
    let pp =
1401
      pp_implies
1402
        (pp_and_l (fun fmt n ->
1403
             (if n = k then pp_k_induction_inductive_case
1404
             else pp_k_induction_base_case)
1405
               m
1406
               pp_print_string
1407
               pp_print_string
1408
               (pp_comma_list pp_var_decl)
1409
               fmt
1410
               (n, mem_in, mem_out)))
1411
        (pp_forall
1412
           (pp_locals m)
1413
           (pp_implies
1414
              (pp_and
1415
                 (pp_transition_aux
1416
                    stateless
1417
                    pp_print_string
1418
                    pp_print_string
1419
                    pp_var_decl)
1420
                 (pp_transition_aux
1421
                    stateless_c
1422
                    pp_print_string
1423
                    pp_print_string
1424
                    pp_var_decl))
1425
              (pp_contract m)))
1426
    in
1427
    pp_axiomatic
1428
      (fun fmt () -> fprintf fmt "%s_k_Induction" name)
1429
      (pp_axiom
1430
         (fun fmt () -> fprintf fmt "%s_k_induction" name)
1431
         (pp_forall
1432
            (fun fmt () ->
1433
              fprintf
1434
                fmt
1435
                "%a,@;%a"
1436
                (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1437
                (name, [ mem_in; mem_out ])
1438
                (pp_locals m)
1439
                (inputs @ outputs))
1440
            (if stateless_c then pp
1441
            else fun fmt x ->
1442
              pp_forall
1443
                (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1444
                pp
1445
                fmt
1446
                ((m_c.mname.node_id, [ mem_in_c; mem_out_c ]), x))))
1447
      fmt
1448
      ( (),
1449
        ( (),
1450
          ( (),
1451
            ( l,
1452
              ( m_c.mstep.step_outputs,
1453
                ( ( (name, inputs @ outputs, mem_in, mem_out),
1454
                    ( m_c.mname.node_id,
1455
                      m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1456
                      mem_in_c,
1457
                      mem_out_c ) ),
1458
                  c ) ) ) ) ) )
1459

    
1460
  let pp_k_induction m fmt ((_, m_c, k) as c_m_k) =
1461
    let stateless_c = fst (get_stateless_status m_c) in
1462
    pp_acsl_cut
1463
      (fun fmt () ->
1464
        fprintf
1465
          fmt
1466
          "%a@,@,%a@,@,%a@,@,%a@,@,%a@,@,%a"
1467
          pp_init_def
1468
          m
1469
          (if stateless_c then pp_print_nothing else pp_init_def)
1470
          m_c
1471
          (pp_base_cases m)
1472
          c_m_k
1473
          (pp_inductive_case m)
1474
          c_m_k
1475
          (pp_k_induction_lemmas m)
1476
          k
1477
          (pp_k_induction_axiom m)
1478
          c_m_k)
1479
      fmt
1480
      ()
1481

    
1482
  let pp_proof_annotation m m_c fmt c =
1483
    let pp m_c fmt = function
1484
      | Kinduction k ->
1485
        pp_k_induction m fmt (c, m_c, k)
1486
    in
1487
    match m_c with
1488
    | Some m_c ->
1489
      pp_print_option (pp m_c) fmt c.mc_proof
1490
    | None ->
1491
      ()
1492

    
1493
  let pp_step_spec fmt machines self mem m =
1494
    let name = m.mname.node_id in
1495
    let insts = instances machines m in
1496
    let insts' = powerset_instances insts in
1497
    let insts'' =
1498
      List.(
1499
        filter
1500
          (fun l -> l <> [])
1501
          (map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
1502
    in
1503
    let inputs = m.mstep.step_inputs in
1504
    let outputs = m.mstep.step_outputs in
1505
    let stateless = fst (get_stateless_status m) in
1506
    let pp_if_outputs pp = if outputs = [] then pp_print_nothing else pp in
1507
    let c, m_c = contract_of machines m in
1508
    let pp_spec =
1509
      pp_print_option
1510
        (if m.mis_contract then pp_print_nothing
1511
        else fun fmt c ->
1512
          pp_print_option
1513
            (fun fmt m_c ->
1514
              let mem_in = mk_mem_in_c m_c in
1515
              let mem_out = mk_mem_out_c m_c in
1516
              let stateless_c = fst (get_stateless_status m_c) in
1517
              pp_ensures
1518
                (pp_implies
1519
                   (pp_transition_aux
1520
                      stateless_c
1521
                      pp_print_string
1522
                      pp_print_string
1523
                      (fun fmt v ->
1524
                        (if is_output m v then pp_ptr_decl else pp_var_decl)
1525
                          fmt
1526
                          v))
1527
                   (pp_contract m))
1528
                fmt
1529
                ( ( m_c.mname.node_id,
1530
                    m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1531
                    mem_in,
1532
                    mem_out ),
1533
                  c ))
1534
            fmt
1535
            m_c)
1536
    in
1537
    let pp_spec_vars =
1538
      match m_c with
1539
      | Some m_c ->
1540
        let mem_in = mk_mem_in_c m_c in
1541
        let mem_out = mk_mem_out_c m_c in
1542
        let stateless_c = fst (get_stateless_status m_c) in
1543
        pp_acsl_cut
1544
          (pp_ghost (fun fmt () ->
1545
               fprintf
1546
                 fmt
1547
                 "@;<0 2>@[<v>%a%a@]"
1548
                 (pp_print_list
1549
                    ~pp_open_box:pp_open_vbox0
1550
                    ~pp_sep:pp_print_semicolon
1551
                    ~pp_eol:pp_print_semicolon
1552
                    (pp_c_decl_local_var m))
1553
                 m_c.mstep.step_outputs
1554
                 (if stateless_c then pp_print_nothing
1555
                 else
1556
                   pp_machine_decl
1557
                     ~ghost:true
1558
                     (pp_comma_list ~pp_eol:pp_print_semicolon pp_print_string))
1559
                 (m_c.mname.node_id, [ mem_in; mem_out ])))
1560
      | _ ->
1561
        pp_print_nothing
1562
    in
1563
    pp_print_option (pp_proof_annotation m m_c) fmt c;
1564
    pp_spec_vars fmt ();
1565
    pp_acsl_cut
1566
      (fun fmt () ->
1567
        if stateless then
1568
          fprintf
1569
            fmt
1570
            "%a@,%a@,%a@,%a@,%a"
1571
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1572
            outputs
1573
            (pp_if_outputs (pp_requires pp_separated''))
1574
            outputs
1575
            (pp_assigns pp_ptr_decl)
1576
            outputs
1577
            (pp_ensures (pp_transition_aux' m))
1578
            (name, inputs @ outputs, "", "")
1579
            pp_spec
1580
            c
1581
        else
1582
          fprintf
1583
            fmt
1584
            "%a@,\
1585
             %a@,\
1586
             %a@,\
1587
             %a@,\
1588
             %a@,\
1589
             %a@,\
1590
             %a@,\
1591
             %a@,\
1592
             %a@,\
1593
             %a@,\
1594
             %a@,\
1595
             %a@,\
1596
             %a@,\
1597
             %a@,\
1598
             %a@,\
1599
             %a@,\
1600
             %a@,\
1601
             %a"
1602
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1603
            outputs
1604
            (pp_requires pp_mem_valid')
1605
            (name, self)
1606
            (pp_requires (pp_separated' self mem))
1607
            (insts', outputs)
1608
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
1609
            (name, mem, self)
1610
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
1611
            (name, mem, self)
1612
            (pp_ensures
1613
               (pp_transition_aux stateless (pp_old pp_ptr) pp_ptr (fun fmt v ->
1614
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
1615
            (name, inputs @ outputs, mem, mem)
1616
            pp_spec
1617
            c
1618
            (pp_assigns pp_ptr_decl)
1619
            outputs
1620
            (pp_assigns (pp_reg self))
1621
            m.mmemory
1622
            (pp_assigns pp_reset_flag')
1623
            [ self ]
1624
            (pp_assigns (pp_memory self))
1625
            (memories insts')
1626
            (pp_assigns (pp_register_chain self))
1627
            insts
1628
            (pp_assigns (pp_reset_flag_chain self))
1629
            insts''
1630
            (pp_assigns (pp_reg mem))
1631
            m.mmemory
1632
            (pp_assigns pp_reset_flag')
1633
            [ mem ]
1634
            (pp_assigns (pp_memory ~indirect:false mem))
1635
            (memories insts')
1636
            (pp_assigns (pp_register_chain ~indirect:false mem))
1637
            insts
1638
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1639
            insts'')
1640
      fmt
1641
      ()
1642

    
1643
  let pp_ghost_instr_code m self fmt instr =
1644
    match instr.instr_desc with
1645
    | MStateAssign (x, v) ->
1646
      fprintf
1647
        fmt
1648
        "@,%a"
1649
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
1650
        (x, v)
1651
    | MResetAssign b ->
1652
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
1653
    | MSetReset inst ->
1654
      let td, _ = List.assoc inst m.minstances in
1655
      if Arrow.td_is_arrow td then
1656
        fprintf
1657
          fmt
1658
          "@,%a;"
1659
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
1660
          inst
1661
    | _ ->
1662
      ()
1663

    
1664
  let pp_step_instr_spec m self mem fmt instr =
1665
    let ghost = m.mis_contract in
1666
    fprintf
1667
      fmt
1668
      "%a%a"
1669
      (pp_ghost_instr_code m mem)
1670
      instr
1671
      (pp_print_list
1672
         ~pp_open_box:pp_open_vbox0
1673
         ~pp_prologue:pp_print_cut
1674
         (pp_acsl_line'
1675
            ~ghost
1676
            (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
1677
      instr.instr_spec
1678

    
1679
  let pp_ghost_parameter mem fmt inst =
1680
    GhostProto.pp_ghost_parameters
1681
      ~cut:false
1682
      fmt
1683
      (match inst with
1684
      | Some inst ->
1685
        [ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
1686
      | None ->
1687
        [ mem, pp_print_string ])
1688

    
1689
  let pp_contract fmt machines _self mem m =
1690
    let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
1691
    match contract_of machines m with
1692
    | Some c, Some _ ->
1693
      pp_print_option
1694
        (pp_acsl_cut (fun fmt -> function
1695
           | Kinduction k ->
1696
             let l = List.init k (fun n -> n + 1) in
1697
             let pp_mem_in = pp_at_pre pp_ptr in
1698
             let pp_mem_out = pp_ptr in
1699
             pp_assert
1700
               (pp_and_l (fun fmt n ->
1701
                    (if n = k then pp_k_induction_inductive_case
1702
                    else pp_k_induction_base_case)
1703
                      m
1704
                      pp_mem_in
1705
                      pp_mem_out
1706
                      pp_vars
1707
                      fmt
1708
                      (n, mem, mem)))
1709
               fmt
1710
               l))
1711
        fmt
1712
        c.mc_proof
1713
    | _, _ ->
1714
      ()
1715
end
1716

    
1717
module MainMod = struct
1718
  let main_mem_ghost = "main_mem_ghost"
1719

    
1720
  let pp_declare_ghost_state fmt name =
1721
    pp_acsl_line'_cut
1722
      (pp_ghost (fun fmt () ->
1723
           fprintf
1724
             fmt
1725
             "%a(,%s);"
1726
             (pp_machine_static_alloc_name ~ghost:true)
1727
             name
1728
             main_mem_ghost))
1729
      fmt
1730
      ()
1731

    
1732
  let pp_ghost_state_parameter fmt () =
1733
    GhostProto.pp_ghost_parameters
1734
      ~cut:false
1735
      fmt
1736
      [ main_mem_ghost, pp_ref pp_print_string ]
1737

    
1738
  let pp_main_loop_invariants main_mem machines fmt m =
1739
    let name = m.mname.node_id in
1740
    let insts = powerset_instances (instances machines m) in
1741
    pp_acsl_cut
1742
      (fun fmt () ->
1743
        fprintf
1744
          fmt
1745
          "%a@,%a@,%a@,%a"
1746
          (pp_loop_invariant pp_mem_valid')
1747
          (name, main_mem)
1748
          (pp_loop_invariant
1749
             (pp_memory_pack_aux pp_print_string pp_print_string))
1750
          (name, main_mem_ghost, main_mem)
1751
          (pp_loop_invariant
1752
             (pp_separated
1753
                (pp_paren pp_print_string)
1754
                pp_ref'
1755
                (pp_ref pp_var_decl)))
1756
          (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
1757
          (pp_loop_invariant
1758
             (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
1759
          ((), ((), ())))
1760
      fmt
1761
      ()
1762

    
1763
  let pp_main_spec fmt =
1764
    pp_acsl_cut
1765
      (fun fmt () ->
1766
        fprintf
1767
          fmt
1768
          "%a@,%a@,%a@,%a"
1769
          (pp_requires
1770
             (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
1771
          ((), ((), ()))
1772
          (pp_terminates pp_false)
1773
          ()
1774
          (pp_ensures pp_false)
1775
          ()
1776
          (pp_assigns pp_nothing)
1777
          [ () ])
1778
      fmt
1779
      ()
1780
end
1781

    
1782
(**************************************************************************)
1783
(*                              MAKEFILE                                  *)
1784
(**************************************************************************)
1785

    
1786
module MakefileMod = struct
1787
  let pp_print_dependencies = C_backend_makefile.fprintf_dependencies "_spec"
1788

    
1789
  let pp_arrow_o fmt () = pp_print_string fmt "arrow_spec.o"
1790

    
1791
  let other_targets fmt basename _nodename dependencies =
1792
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1793
    (* EACSL version of library file . c *)
1794
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1795
    fprintf
1796
      fmt
1797
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1798
       e-acsl -print -ocode %s_eacsl.c@."
1799
      basename
1800
      basename;
1801
    fprintf fmt "@.";
1802
    fprintf fmt "@.";
1803

    
1804
    (* EACSL version of library file . c + main .c *)
1805
    fprintf
1806
      fmt
1807
      "%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1808
      basename
1809
      basename
1810
      basename
1811
      basename;
1812
    fprintf
1813
      fmt
1814
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1815
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
1816
      basename
1817
      basename
1818
      basename;
1819
    (* Ugly hack to deal with eacsl bugs *)
1820
    fprintf
1821
      fmt
1822
      "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1823
      basename
1824
      basename;
1825
    fprintf fmt "@.";
1826
    fprintf fmt "@.";
1827

    
1828
    (* EACSL version of binary *)
1829
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1830
    fprintf
1831
      fmt
1832
      "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1833
      basename;
1834
    (* compiling instrumented lib + main *)
1835
    pp_print_dependencies fmt dependencies;
1836
    fprintf
1837
      fmt
1838
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1839
       %s_main_eacsl.o %a@."
1840
      basename
1841
      (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1842
      (C_backend_makefile.compiled_dependencies dependencies)
1843
      ("${FRAMACEACSL}/e_acsl.c "
1844
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1845
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1846
      basename
1847
      (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1848
      (C_backend_makefile.lib_dependencies dependencies);
1849
    fprintf fmt "@."
1850
end
1851

    
1852
(* TODO: complete this list *)
1853
let acsl_keywords = ISet.of_list ["set"]
1854

    
1855
let sanitize x = if ISet.mem x acsl_keywords then "__" ^ x else x
1856

    
1857
let sanitize_var_decl vd = { vd with var_id = sanitize vd.var_id }
1858

    
1859
let sanitize_var_decls = List.map sanitize_var_decl
1860

    
1861
let rec sanitize_value v =
1862
  let value_desc = match v.value_desc with
1863
    | Machine_code_types.Var vd -> Machine_code_types.Var (sanitize_var_decl vd)
1864
    | Fun (f, vs) -> Fun (f, sanitize_values vs)
1865
    | Array vs -> Array (sanitize_values vs)
1866
    | Access (v1, v2) -> Access (sanitize_value v1, sanitize_value v2)
1867
    | Power (v1, v2) -> Power (sanitize_value v1, sanitize_value v2)
1868
    | v -> v
1869
  in
1870
  { v with value_desc }
1871

    
1872
and sanitize_values vs = List.map sanitize_value vs
1873

    
1874
let sanitize_expr = function
1875
  | Val v -> Val (sanitize_value v)
1876
  | Var v -> Var (sanitize_var_decl v)
1877
  | e -> e
1878

    
1879
let sanitize_predicate = function
1880
  | Transition (st, f, inst, i, vs, r, mf, mfinsts) ->
1881
    Transition (st, f, inst, i, List.map sanitize_expr vs, r, mf, mfinsts)
1882
  | p -> p
1883

    
1884
let rec sanitize_formula = function
1885
  | Equal (e1, e2) -> Equal (sanitize_expr e1, sanitize_expr e2)
1886
  | GEqual (e1, e2) -> GEqual (sanitize_expr e1, sanitize_expr e2)
1887
  | And fs -> And (sanitize_formulae fs)
1888
  | Or fs -> Or (sanitize_formulae fs)
1889
  | Imply (f1, f2) -> Imply (sanitize_formula f1, sanitize_formula f2)
1890
  | Exists (vs, f) -> Exists (sanitize_var_decls vs, sanitize_formula f)
1891
  | Forall (vs, f) -> Forall (sanitize_var_decls vs, sanitize_formula f)
1892
  | Ternary (e, t, f) -> Ternary (sanitize_expr e, sanitize_formula t, sanitize_formula f)
1893
  | Predicate p -> Predicate (sanitize_predicate p)
1894
  | ExistsMem (m, f1, f2) -> ExistsMem (m, sanitize_formula f1, sanitize_formula f2)
1895
  | Value v -> Value (sanitize_value v)
1896
  | f -> f
1897

    
1898
and sanitize_formulae fs = List.map sanitize_formula fs
1899

    
1900
let rec sanitize_instr i =
1901
  let sanitize_instr_desc = function
1902
    | MLocalAssign (x, v) ->
1903
      MLocalAssign (sanitize_var_decl x, sanitize_value v)
1904
    | MStateAssign (x, v) ->
1905
      MStateAssign (x, sanitize_value v)
1906
    | MStep (xs, f, vs) ->
1907
      MStep (sanitize_var_decls xs, f, sanitize_values vs)
1908
    | MBranch (v, brs) ->
1909
      MBranch (sanitize_value v, List.map (fun (t, instrs) -> t, sanitize_instrs instrs) brs)
1910
    | i -> i
1911
  in
1912
  { i with
1913
    instr_desc = sanitize_instr_desc i.instr_desc;
1914
    instr_spec = sanitize_formulae i.instr_spec
1915
  }
1916

    
1917
and sanitize_instrs instrs = List.map sanitize_instr instrs
1918

    
1919
let sanitize_step s =
1920
  { s with
1921
    step_inputs = sanitize_var_decls s.step_inputs;
1922
    step_outputs = sanitize_var_decls s.step_outputs;
1923
    step_locals = sanitize_var_decls s.step_locals;
1924
    step_instrs = sanitize_instrs s.step_instrs
1925
  }
1926

    
1927
let sanitize_transition t =
1928
  { t with
1929
    tvars = sanitize_var_decls t.tvars;
1930
    tformula = sanitize_formula t.tformula
1931
  }
1932

    
1933
let sanitize_transitions = List.map sanitize_transition
1934

    
1935
let sanitize_memory_pack mp =
1936
  { mp with
1937
    mpformula = sanitize_formula mp.mpformula
1938
  }
1939

    
1940
let sanitize_memory_packs = List.map sanitize_memory_pack
1941

    
1942
let sanitize_spec s =
1943
  { s with
1944
    mtransitions = sanitize_transitions s.mtransitions;
1945
    mmemory_packs = sanitize_memory_packs s.mmemory_packs
1946
  }
1947
let sanitize_machine m =
1948
  { m with
1949
    mstep = sanitize_step m.mstep;
1950
    mspec = sanitize_spec m.mspec
1951
  }
1952

    
1953
let sanitize_machines = List.map sanitize_machine
1954

    
1955
(* Local Variables: *)
1956
(* compile-command:"make -C ../../.." *)
1957
(* End: *)
(15-15/18)