Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by Lélio Brun 7 months ago

work on spec generation almost done

View differences:

include/arrow.c
12 12
void _arrow_dealloc (struct _arrow_mem * _alloc) {
13 13
  free (_alloc);
14 14
}
15

  
16
_Bool _arrow_step(struct _arrow_mem *self) {
17
  if (self->_reg._first) {
18
    self->_reg._first = 0;
19
    return 1;
20
  }
21
  return 0;
22
}
include/arrow.h
1

  
2 1
#ifndef _ARROW
3 2
#define _ARROW
4 3

  
5
struct _arrow_mem {struct _arrow_reg {_Bool _first; } _reg; };
4
struct _arrow_mem {
5
  struct _arrow_reg {_Bool _first; } _reg;
6
};
6 7

  
7 8
extern struct _arrow_mem *_arrow_alloc ();
8 9

  
......
23 24

  
24 25
#define _arrow_clear(self) {}
25 26

  
26
/* #define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) */
27

  
28 27
#define _arrow_reset(self) {(self)->_reg._first = 1;}
29 28

  
30
/* Step macro for specialized arrows of the form: (true -> false) */
31

  
32
#define _once_step(output,self) { *output = (self)->_reg._first; if ((self)->_reg._first) { (self)->_reg._first=0; }; }
29
_Bool _arrow_step(struct _arrow_mem *self);
33 30

  
34 31
#endif
include/arrow_spec.c
1
#include <stdlib.h>
2
#include <assert.h>
3
#include "arrow_spec.h"
4

  
5
struct _arrow_mem * _arrow_alloc () {
6
  struct _arrow_mem *_alloc;
7
  _alloc = (struct _arrow_mem *) malloc(sizeof(struct _arrow_mem *));
8
  assert (_alloc);
9
  return _alloc;
10
}
11

  
12
void _arrow_dealloc (struct _arrow_mem * _alloc) {
13
  free (_alloc);
14
}
15

  
16
_Bool _arrow_step(struct _arrow_mem *self)
17
       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */
18
{
19
  if (self->_reg._first) {
20
    self->_reg._first = 0;
21
    //@ ghost _arrow_step_ghost(*mem);
22
    return 1;
23
  }
24
  return 0;
25
}
include/arrow_spec.h
1 1
#ifndef ARROW_SPEC_H_
2 2
#define ARROW_SPEC_H_
3 3

  
4
struct _arrow_mem {
5
  struct _arrow_reg {_Bool _first; } _reg;
6
};
7

  
8
extern struct _arrow_mem *_arrow_alloc ();
9

  
10
extern void _arrow_dealloc (struct _arrow_mem *);
11

  
12
#define _arrow_DECLARE(attr, inst)\
13
  attr struct _arrow_mem inst;
14

  
15
#define _arrow_LINK(inst) do {\
16
  ;\
17
} while (0)
18

  
19
#define _arrow_ALLOC(attr, inst)\
20
  _arrow_DECLARE(attr, inst);\
21
  _arrow_LINK(inst)
22

  
23
#define _arrow_init(self) {}
24

  
25
#define _arrow_clear(self) {}
26

  
27
#define _arrow_reset(self) {(self)->_reg._first = 1;}
28

  
4 29
/* ACSL arrow spec */
5 30
//@ ghost struct _arrow_mem_ghost {struct _arrow_reg _reg;};
6
/*@
7
   predicate _arrow_valid(struct _arrow_mem *self) =
8
     \valid(self);
9
*/
10
/*@
11
   predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
12
     mem_in._reg._first == 1;
31

  
32
#define _arrow_reset_ghost(mem) (mem)._reg._first = 1
33
#define _arrow_step_ghost(mem) (mem)._reg._first = 0
34

  
35
/*@ predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
36
      mem_in._reg._first == 1;
37
 */
38

  
39
/*@ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
40
                                struct _arrow_mem_ghost mem_out,
41
                                _Bool out) =
42
      out == mem_in._reg._first
43
      && (mem_in._reg._first ? (mem_out._reg._first == 0)
44
                             : (mem_out._reg._first == mem_in._reg._first));
13 45
*/
14
/*@
15
   predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
16
                               integer x, integer y,
17
                               struct _arrow_mem_ghost mem_out, _Bool out) =
18
     (mem_in._reg._first ? (mem_out._reg._first == 0
19
                            && out == x)
20
                         : (mem_out._reg._first == mem_in._reg._first
21
                            && out == y));
46

  
47
/*@ predicate _arrow_ghost(struct _arrow_mem_ghost mem,
48
                           struct _arrow_mem *self) =
49
      mem._reg._first == self->_reg._first;
22 50
*/
51

  
23 52
/*@
24
   predicate _arrow_ghost(struct _arrow_mem_ghost mem,
25
                          struct _arrow_mem *self) =
26
     mem._reg._first == self->_reg._first;
53
  requires \separated(mem, self);
54
  requires _arrow_ghost(*mem, self);
55
  ensures  _arrow_ghost(*mem, self);
56
  ensures \result == \old(self->_reg._first);
57
  ensures self->_reg._first == 0;
58
  ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);
59
  assigns mem->_reg._first, self->_reg._first;
27 60
*/
61
_Bool _arrow_step(struct _arrow_mem *self)
62
       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
28 63

  
29 64
#endif // ARROW_SPEC_H_
src/arrow.ml
30 30
    top_decl_itf = false;
31 31
    top_decl_loc = Location.dummy_loc
32 32
  }
33

  
34
let td_is_arrow td =
35
  Corelang.node_name td = arrow_id
src/arrow.mli
1 1
val arrow_id: string
2 2
val arrow_top_decl: unit -> Lustre_types.top_decl
3 3
val arrow_desc: Lustre_types.node_desc
4
val td_is_arrow: Lustre_types.top_decl -> bool
src/backends/Ada/ada_backend_adb.ml
85 85
    match get_instr_desc instr with
86 86
      (* no reset *)
87 87
      | MNoReset _ -> ()
88
      (* TODO: handle clear_reset *)
89
      | MClearReset -> ()
88 90
      (* reset  *)
89
      | MReset i when List.mem_assoc i typed_submachines ->
91
      | MSetReset i when List.mem_assoc i typed_submachines ->
90 92
          let (substitution, submachine) = get_instance i typed_submachines in
91 93
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
92 94
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
......
149 151
  **)
150 152
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
151 153
    let build_assign = function var ->
152
      mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
154
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
153 155
    in
154 156
    let env, memory = match m_spec_opt with
155 157
      | None -> env, m.mmemory
src/backends/Ada/misc_lustre_function.ml
268 268
              let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
269 269
              { instr_desc = assign;
270 270
                lustre_eq  = None;
271
                instr_spec = Spec_types.True
271
                instr_spec = []
272 272
              }
273 273
            in
274 274
            let mkval_var id = {
src/backends/C/c_backend_common.ml
37 37
  let baseNAME = protect_filename baseNAME in
38 38
  baseNAME
39 39

  
40
let pp_ptr fmt =
41
  fprintf fmt "*%s"
42

  
43
let reset_label = "Reset"
44

  
45
let pp_label fmt =
46
  fprintf fmt "%s:"
47

  
40 48
let var_is name v =
41 49
  v.var_id = name
42 50

  
......
55 63
let mk_mem = mk_local "mem"
56 64
let mk_mem_in = mk_local "mem_in"
57 65
let mk_mem_out = mk_local "mem_out"
66
let mk_mem_reset = mk_local "mem_reset"
58 67

  
59 68
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
60 69
let mk_instance m =
......
118 127
let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
119 128
let pp_machine_memtype_name ?(ghost=false) fmt id =
120 129
  fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")
130
let pp_machine_decl ?(ghost=false) pp_var fmt (id, var) =
131
  fprintf fmt "%a %a" (pp_machine_memtype_name ~ghost) id pp_var var
132
let pp_machine_decl' ?(ghost=false) fmt =
133
  pp_machine_decl ~ghost pp_print_string fmt
121 134
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
122 135
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
123 136
let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id
124 137
let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id
125 138
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id
126 139
let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id
127
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
140
let pp_machine_set_reset_name fmt id = fprintf fmt "%s_set_reset" id
141
let pp_machine_clear_reset_name fmt id = fprintf fmt "%s_clear_reset" id
128 142
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
129 143
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
130 144
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
......
583 597
      then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
584 598
      else fprintf fmt "%s%s_reg.%a%a"
585 599
          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
600
    else if is_reset_flag v then
601
      fprintf fmt "%s%s%a%a"
602
          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
586 603
    else
587 604
      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
588 605
  | _, Cst cst ->
......
610 627
let print_machine_struct ?(ghost=false) fmt m =
611 628
  if not (fst (Machine_code_common.get_stateless_status m)) then
612 629
    (* Define struct *)
613
    fprintf fmt "@[<v 2>%a {%a%a@]@,};"
630
    fprintf fmt "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"
614 631
      (pp_machine_memtype_name ~ghost) m.mname.node_id
615 632
      (if ghost then
616 633
         (fun fmt -> function
......
658 675
    pp_machine_dealloc_name name
659 676
    (pp_machine_memtype_name ~ghost:false) name
660 677

  
661
let print_reset_prototype self fmt (name, static) =
662
  fprintf fmt "void %a (%a%a *%s)"
663
    pp_machine_reset_name name
664
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
665
       pp_c_decl_input_var) static
666
    (pp_machine_memtype_name ~ghost:false) name
667
    self
668

  
669
let print_init_prototype self fmt (name, static) =
670
  fprintf fmt "void %a (%a%a *%s)"
671
    pp_machine_init_name name
672
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
673
       pp_c_decl_input_var) static
674
    (pp_machine_memtype_name ~ghost:false) name
675
    self
676

  
677
let print_clear_prototype self fmt (name, static) =
678
  fprintf fmt "void %a (%a%a *%s)"
679
    pp_machine_clear_name name
680
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
681
       pp_c_decl_input_var) static
682
    (pp_machine_memtype_name ~ghost:false) name
683
    self
684

  
685
let print_stateless_prototype fmt (name, inputs, outputs) =
686
  fprintf fmt "void %a (@[<v>%a%a@])"
687
    pp_machine_step_name name
688
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
689
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
690
    (pp_print_list ~pp_sep:pp_print_comma pp_c_decl_output_var) outputs
691

  
692
let print_step_prototype self fmt (name, inputs, outputs) =
693
  fprintf fmt "void %a (@[<v>%a%a%a *%s@])"
694
    pp_machine_step_name name
695
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
696
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
697
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
698
       ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
699
    (pp_machine_memtype_name ~ghost:false) name
700
    self
678
module type MODIFIERS_GHOST_PROTO = sig
679
  val pp_ghost_parameters: formatter -> (string * (formatter -> string -> unit)) list -> unit
680
end
681

  
682
module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct
683
  let pp_ghost_parameters _ _ = ()
684
end
685

  
686
module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
687

  
688
  let pp_mem_ghost name fmt mem =
689
    pp_machine_decl ~ghost:true
690
      (fun fmt mem -> fprintf fmt "\ghost %a" pp_ptr mem) fmt
691
      (name, mem)
692

  
693
  let print_clear_reset_prototype self mem fmt (name, static) =
694
    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
695
      pp_machine_clear_reset_name name
696
      (pp_comma_list ~pp_eol:pp_print_comma
697
         pp_c_decl_input_var) static
698
      (pp_machine_memtype_name ~ghost:false) name
699
      self
700
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
701

  
702
  let print_set_reset_prototype self mem fmt (name, static) =
703
    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
704
      pp_machine_set_reset_name name
705
      (pp_comma_list ~pp_eol:pp_print_comma
706
         pp_c_decl_input_var) static
707
      (pp_machine_memtype_name ~ghost:false) name
708
      self
709
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
710

  
711
  let print_step_prototype self mem fmt (name, inputs, outputs) =
712
    fprintf fmt "@[<v>void %a (@[<v>%a%a%a *%s@])%a@]"
713
      pp_machine_step_name name
714
      (pp_comma_list ~pp_eol:pp_print_comma
715
         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
716
      (pp_comma_list ~pp_eol:pp_print_comma
717
         ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
718
      (pp_machine_memtype_name ~ghost:false) name
719
      self
720
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
721

  
722
  let print_init_prototype self fmt (name, static) =
723
    fprintf fmt "void %a (%a%a *%s)"
724
      pp_machine_init_name name
725
      (pp_comma_list ~pp_eol:pp_print_comma
726
         pp_c_decl_input_var) static
727
      (pp_machine_memtype_name ~ghost:false) name
728
      self
729

  
730
  let print_clear_prototype self fmt (name, static) =
731
    fprintf fmt "void %a (%a%a *%s)"
732
      pp_machine_clear_name name
733
      (pp_comma_list ~pp_eol:pp_print_comma
734
         pp_c_decl_input_var) static
735
      (pp_machine_memtype_name ~ghost:false) name
736
      self
737

  
738
  let print_stateless_prototype fmt (name, inputs, outputs) =
739
    fprintf fmt "void %a (@[<v>%a%a@])"
740
      pp_machine_step_name name
741
      (pp_comma_list ~pp_eol:pp_print_comma
742
         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
743
      (pp_comma_list pp_c_decl_output_var) outputs
744

  
745
end
701 746

  
702 747
let print_import_prototype fmt dep =
703 748
  fprintf fmt "#include \"%s.h\"" dep.name
src/backends/C/c_backend_header.ml
22 22

  
23 23

  
24 24
module type MODIFIERS_HDR = sig
25
  module GhostProto: MODIFIERS_GHOST_PROTO
25 26
  val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
26 27
  val pp_import_standard_spec: formatter -> unit -> unit
27 28
end
28 29

  
29 30
module EmptyMod = struct
31
  module GhostProto = EmptyGhostProto
30 32
  let print_machine_decl_prefix = fun _ _ -> ()
31 33
  let pp_import_standard_spec _ _ = ()
32 34
end
33 35

  
34 36
module Main = functor (Mod: MODIFIERS_HDR) -> struct
35 37

  
38
  module Protos = Protos(Mod.GhostProto)
39

  
36 40
  let print_import_standard fmt () =
37 41
    (* if Machine_types.has_machine_type () then *)
38 42
    fprintf fmt
......
231 235
        assert false
232 236
      end
233 237
    else if inode.nodei_stateless then
234
      fprintf fmt "extern %a;" print_stateless_prototype prototype
238
      fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype
235 239
    else
236 240
      let static_inputs = List.filter (fun v -> v.var_dec_const)
237 241
          inode.nodei_inputs in
......
239 243
        List.exists (fun v -> v.var_id = name)
240 244
          (inode.nodei_inputs @ inode.nodei_outputs) in
241 245
      let self = mk_new_name used "self" in
246
      let mem = mk_new_name used "mem" in
242 247
      let static_prototype = (inode.nodei_id, static_inputs) in
243 248
      fprintf fmt
244 249
        "extern %a;@,\
250
         extern %a;@,\
245 251
         extern %a;@,\
246 252
         extern %a;@,\
247 253
         extern %a;"
248
        (print_reset_prototype self) static_prototype
249
        (print_init_prototype self) static_prototype
250
        (print_clear_prototype self) static_prototype
251
        (print_step_prototype self) prototype
254
        (Protos.print_set_reset_prototype self mem) static_prototype
255
        (Protos.print_clear_reset_prototype self mem) static_prototype
256
        (Protos.print_init_prototype self) static_prototype
257
        (Protos.print_clear_prototype self) static_prototype
258
        (Protos.print_step_prototype self mem) prototype
252 259

  
253 260
  let print_const_top_decl fmt tdecl =
254 261
    let cdecl = const_of_top tdecl in
src/backends/C/c_backend_main.ml
87 87
             fprintf fmt "%a *main_mem = %a();"
88 88
               (pp_machine_memtype_name ~ghost:false) mname
89 89
               pp_machine_alloc_name mname) ()
90
        pp_machine_reset_name mname
90
        pp_machine_set_reset_name mname
91 91
        main_mem
92 92

  
93 93
  let print_global_initialize fmt basename =
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 ()
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff