Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

src/backends/Ada/ada_backend_ads.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open Utils
12 13
open Format
13 14
open Machine_code_types
14 15
open Lustre_types
......
17 18
open Ada_backend_common
18 19

  
19 20
(** Functions printing the .ads file **)
20
module Main = struct
21
  let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
22
  (*should be replaced by the init of list from ocaml std lib*)
23 21

  
24
  let suffixOld = "_old"
22
let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
23
(*should be replaced by the init of list from ocaml std lib*)
25 24

  
26
  let suffixNew = "_new"
25
let suffixOld = "_old"
27 26

  
28
  let pp_invariant_name fmt = fprintf fmt "inv"
27
let suffixNew = "_new"
29 28

  
30
  let pp_transition_name fmt = fprintf fmt "transition"
29
let pp_invariant_name fmt = fprintf fmt "inv"
31 30

  
32
  let pp_init_name fmt = fprintf fmt "init"
31
let pp_transition_name fmt = fprintf fmt "transition"
33 32

  
34
  let pp_state_name_predicate suffix fmt =
35
    fprintf fmt "%t%s" pp_state_name suffix
33
let pp_init_name fmt = fprintf fmt "init"
36 34

  
37
  let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
35
let pp_state_name_predicate suffix fmt =
36
  fprintf fmt "%t%s" pp_state_name suffix
38 37

  
39
  (** Print the expression function representing the transition predicate.
40
      @param fmt the formater to print on **)
41
  let pp_init_predicate fmt () =
42
    let new_state =
43
      AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
44
    in
45
    pp_predicate pp_init_name [ [ new_state ] ] true fmt None
38
let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
46 39

  
47
  (** Print the expression function representing the transition predicate.
48
      @param fmt the formater to print on @param machine the machine **)
49
  let pp_transition_predicate fmt (_, m) =
50
    let old_state =
51
      AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
52
    in
53
    let new_state =
54
      AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
55
    in
56
    let inputs = build_pp_var_decl_step_input AdaIn None m in
57
    let outputs = build_pp_var_decl_step_output AdaIn None m in
58
    pp_predicate pp_transition_name
59
      ([ [ old_state; new_state ] ] @ inputs @ outputs)
60
      true fmt None
40
(** Print the expression function representing the transition predicate.
41
    @param fmt the formater to print on **)
42
let pp_init_predicate fmt () =
43
  let new_state =
44
    AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
45
  in
46
  pp_predicate pp_init_name [ [ new_state ] ] true fmt None
61 47

  
62
  let pp_invariant_predicate fmt () =
63
    pp_predicate pp_invariant_name
64
      [ [ build_pp_state_decl AdaIn None ] ]
65
      true fmt None
48
(** Print the expression function representing the transition predicate.
49
    @param fmt the formater to print on @param machine the machine **)
50
let pp_transition_predicate fmt (_, m) =
51
  let old_state =
52
    AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
53
  in
54
  let new_state =
55
    AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
56
  in
57
  let inputs = build_pp_var_decl_step_input AdaIn None m in
58
  let outputs = build_pp_var_decl_step_output AdaIn None m in
59
  pp_predicate pp_transition_name
60
    ([ [ old_state; new_state ] ] @ inputs @ outputs)
61
    true fmt None
66 62

  
67
  (** Print a new statement instantiating a generic package. @param fmt the
68
      formater to print on @param substitutions the instanciation substitution
69
      @param machine the machine to instanciate **)
70
  let pp_new_package fmt (substitutions, machine) =
71
    let pp_name = pp_package_name machine in
72
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
73
    let instanciations =
74
      List.map
75
        (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
76
        substitutions
77
    in
78
    pp_package_instanciation pp_new_name pp_name fmt instanciations
63
let pp_invariant_predicate fmt () =
64
  pp_predicate pp_invariant_name
65
    [ [ build_pp_state_decl AdaIn None ] ]
66
    true fmt None
79 67

  
80
  (** Remove duplicates from a list according to a given predicate. @param eq
81
      the predicate defining equality @param l the list to parse **)
82
  let remove_duplicates eq l =
83
    let aux l x = if List.exists (eq x) l then l else x :: l in
84
    List.fold_left aux [] l
68
(** Print a new statement instantiating a generic package. @param fmt the
69
    formater to print on @param substitutions the instanciation substitution
70
    @param machine the machine to instanciate **)
71
let pp_new_package fmt (substitutions, machine) =
72
  let pp_name = pp_package_name machine in
73
  let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
74
  let instanciations =
75
    List.map
76
      (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
77
      substitutions
78
  in
79
  pp_package_instanciation pp_new_name pp_name fmt instanciations
85 80

  
86
  (** Compare two typed machines. **)
87
  let eq_typed_machine (subst1, machine1) (subst2, machine2) =
88
    String.equal machine1.mname.node_id machine2.mname.node_id
89
    && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
81
(** Remove duplicates from a list according to a given predicate. @param eq
82
    the predicate defining equality @param l the list to parse **)
83
let remove_duplicates eq l =
84
  let aux l x = if List.exists (eq x) l then l else x :: l in
85
  List.fold_left aux [] l
90 86

  
91
  (** Print the package declaration(ads) of a machine. It requires the list of
92
      all typed instance. A typed submachine is a (ident, typed_machine) with -
93
      ident: the name - typed_machine: a (substitution, machine) with - machine:
94
      the submachine struct - substitution the instanciation of all its
95
      polymorphic types. @param fmt the formater to print on @param
96
      typed_submachines list of all typed submachines of this machine @param m
97
      the machine **)
98
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
99
    let typed_machines = snd (List.split typed_submachines) in
100
    let typed_machines_set =
101
      remove_duplicates eq_typed_machine typed_machines
102
    in
87
(** Compare two typed machines. **)
88
let eq_typed_machine (subst1, machine1) (subst2, machine2) =
89
  String.equal machine1.mname.node_id machine2.mname.node_id
90
  && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
103 91

  
104
    let machines_to_import =
105
      List.map pp_package_name (snd (List.split typed_machines_set))
106
    in
92
(** Print the package declaration(ads) of a machine. It requires the list of
93
    all typed instance. A typed submachine is a (ident, typed_machine) with -
94
    ident: the name - typed_machine: a (substitution, machine) with - machine:
95
    the submachine struct - substitution the instanciation of all its
96
    polymorphic types. @param fmt the formater to print on @param
97
    typed_submachines list of all typed submachines of this machine @param m
98
    the machine **)
99
let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
100
  let typed_machines = snd (List.split typed_submachines) in
101
  let typed_machines_set =
102
    remove_duplicates eq_typed_machine typed_machines
103
  in
107 104

  
108
    let polymorphic_types = find_all_polymorphic_type m in
105
  let machines_to_import =
106
    List.map pp_package_name (snd (List.split typed_machines_set))
107
  in
109 108

  
110
    let typed_machines_to_instanciate =
111
      List.filter (fun (l, _) -> l != []) typed_machines_set
112
    in
109
  let polymorphic_types = find_all_polymorphic_type m in
113 110

  
114
    let typed_instances =
115
      List.filter is_submachine_statefull typed_submachines
116
    in
111
  let typed_machines_to_instanciate =
112
    List.filter (fun (l, _) -> l != []) typed_machines_set
113
  in
117 114

  
118
    let memories =
119
      match m_spec_opt with
120
      | None ->
121
        []
122
      | Some m ->
123
        List.map
124
          (fun x ->
125
            pp_var_decl
126
              (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
127
          m.mmemory
128
    in
129
    let ghost_private = memories in
130
    (* Commented since not used. Could be reinjected in the code let vars_spec =
131
       match m_spec_opt with | None -> [] | Some m_spec -> List.map
132
       (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
133
       (m_spec.mmemory) in *)
134
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
135
    let states =
115
  let typed_instances =
116
    List.filter is_submachine_statefull typed_submachines
117
  in
118

  
119
  let memories =
120
    match m_spec_opt with
121
    | None ->
122
      []
123
    | Some m ->
136 124
      List.map
137
        (build_pp_state_decl_from_subinstance AdaNoMode None)
138
        typed_instances
139
    in
140
    let var_lists =
141
      (if states = [] then [] else [ states ])
142
      @ if vars = [] then [] else [ vars ]
143
    in
125
        (fun x ->
126
           pp_var_decl
127
             (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
128
        m.mmemory
129
  in
130
  let ghost_private = memories in
131
  (* Commented since not used. Could be reinjected in the code let vars_spec =
132
     match m_spec_opt with | None -> [] | Some m_spec -> List.map
133
     (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
134
     (m_spec.mmemory) in *)
135
  let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
136
  let states =
137
    List.map
138
      (build_pp_state_decl_from_subinstance AdaNoMode None)
139
      typed_instances
140
  in
141
  let var_lists =
142
    (if states = [] then [] else [ states ])
143
    @ if vars = [] then [] else [ vars ]
144
  in
144 145

  
145
    let pp_ifstatefull fmt pp =
146
      if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
147
    in
146
  let pp_ifstatefull fmt pp =
147
    if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
148
  in
148 149

  
149
    let pp_state_decl_and_reset fmt =
150
      let init fmt =
151
        pp_call fmt
152
          ( pp_access pp_axiomatize_package_name pp_init_name,
153
            [ [ pp_state_name ] ] )
154
      in
155
      let contract = Some (false, false, [], [ init ]) in
156
      fprintf fmt "%t;@,@,%a;@,@,"
157
        (*Declare the state type*)
158
        (pp_type_decl pp_state_type AdaPrivate)
159
        (*Declare the reset procedure*)
160
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
161
        AdaNoContent
150
  let pp_state_decl_and_reset fmt =
151
    let init fmt =
152
      pp_call fmt
153
        ( pp_access pp_axiomatize_package_name pp_init_name,
154
          [ [ pp_state_name ] ] )
162 155
    in
156
    let contract = Some (false, false, [], [ init ]) in
157
    fprintf fmt "%t;@,@,%a;@,@,"
158
      (*Declare the state type*)
159
      (pp_type_decl pp_state_type AdaPrivate)
160
      (*Declare the reset procedure*)
161
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
162
      AdaNoContent
163
  in
163 164

  
164
    let pp_private_section fmt =
165
      fprintf fmt "@,private@,@,%a%t%a%t%a"
166
        (*Instantiate the polymorphic type that need to be instantiated*)
167
        (Utils.fprintf_list ~sep:";@," pp_new_package)
168
        typed_machines_to_instanciate
169
        (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
170
        (*Define the state type*)
171
        pp_ifstatefull
172
        (fun fmt -> pp_record pp_state_type fmt var_lists)
173
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
174
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
175
        ghost_private
176
    in
165
  let pp_private_section fmt =
166
    fprintf fmt "@,private@,@,%a%a%a"
167
      (*Instantiate the polymorphic type that need to be instantiated*)
168
      (pp_print_list
169
         ~pp_sep:pp_print_semicolon
170
         ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
171
         pp_new_package)
172
      typed_machines_to_instanciate
173
      (*Define the state type*)
174
      pp_ifstatefull
175
      (fun fmt -> pp_record pp_state_type fmt var_lists)
176
      (pp_print_list
177
         ~pp_sep:pp_print_semicolon
178
         ~pp_prologue:(fun fmt () -> fprintf fmt ";@,@,")
179
         (fun fmt pp -> pp fmt))
180
      ghost_private
181
  in
177 182

  
178
    let pp_content fmt =
179
      let pp_contract_opt =
180
        let pp_var x fmt = pp_clean_ada_identifier fmt x in
181
        let guarantee_post_conditions = List.map pp_var guarantees in
182
        let state_pre_conditions, state_post_conditions =
183
          if is_machine_statefull m then
184
            let input = List.map pp_var_name m.mstep.step_inputs in
185
            let output = List.map pp_var_name m.mstep.step_outputs in
186
            let args =
187
              [ [ pp_old pp_state_name; pp_state_name ] ]
188
              @ (if input != [] then [ input ] else [])
189
              @ if output != [] then [ output ] else []
190
            in
191
            let transition fmt =
192
              pp_call fmt
193
                (pp_access pp_axiomatize_package_name pp_transition_name, args)
194
            in
195
            let invariant fmt =
196
              pp_call fmt
197
                ( pp_access pp_axiomatize_package_name pp_invariant_name,
198
                  [ [ pp_state_name ] ] )
199
            in
200
            [ invariant ], [ transition; invariant ]
201
          else [], []
202
        in
203
        let post_conditions =
204
          state_post_conditions @ guarantee_post_conditions
205
        in
206
        let pre_conditions = state_pre_conditions in
207
        if post_conditions = [] && pre_conditions = [] then None
208
        else Some (false, false, pre_conditions, post_conditions)
183
  let pp_content fmt =
184
    let pp_contract_opt =
185
      let pp_var x fmt = pp_clean_ada_identifier fmt x in
186
      let guarantee_post_conditions = List.map pp_var guarantees in
187
      let state_pre_conditions, state_post_conditions =
188
        if is_machine_statefull m then
189
          let input = List.map pp_var_name m.mstep.step_inputs in
190
          let output = List.map pp_var_name m.mstep.step_outputs in
191
          let args =
192
            [ [ pp_old pp_state_name; pp_state_name ] ]
193
            @ (if input != [] then [ input ] else [])
194
            @ if output != [] then [ output ] else []
195
          in
196
          let transition fmt =
197
            pp_call fmt
198
              (pp_access pp_axiomatize_package_name pp_transition_name, args)
199
          in
200
          let invariant fmt =
201
            pp_call fmt
202
              ( pp_access pp_axiomatize_package_name pp_invariant_name,
203
                [ [ pp_state_name ] ] )
204
          in
205
          [ invariant ], [ transition; invariant ]
206
        else [], []
209 207
      in
210
      let pp_guarantee name =
211
        pp_var_decl
212
          ( AdaNoMode,
213
            (fun fmt -> pp_clean_ada_identifier fmt name),
214
            pp_boolean_type,
215
            Some (true, false, [], []) )
208
      let post_conditions =
209
        state_post_conditions @ guarantee_post_conditions
216 210
      in
217
      let ghost_public = List.map pp_guarantee guarantees in
218
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
219
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
220
        ghost_public
221
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
222
        pp_ifstatefull pp_state_decl_and_reset
223
        (*Declare the step procedure*)
224
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m)
225
           pp_contract_opt)
226
        AdaNoContent pp_ifstatefull
227
        (fun fmt -> fprintf fmt ";@,")
228
        (pp_package pp_axiomatize_package_name [] false)
229
        (fun fmt ->
230
          fprintf fmt
231
            "pragma Annotate (GNATProve, External_Axiomatization);@,\
232
             @,\
233
             %a;@,\
234
             %a;@,\
235
             %a"
236
            (*Declare the init predicate*)
237
            pp_init_predicate ()
238
            (*Declare the transition predicate*)
239
            pp_transition_predicate (m_spec_opt, m)
240
            (*Declare the invariant predicate*)
241
            pp_invariant_predicate ())
242
        (*Print the private section*)
243
        pp_private_section
211
      let pre_conditions = state_pre_conditions in
212
      if post_conditions = [] && pre_conditions = [] then None
213
      else Some (false, false, pre_conditions, post_conditions)
214
    in
215
    let pp_guarantee name =
216
      pp_var_decl
217
        ( AdaNoMode,
218
          (fun fmt -> pp_clean_ada_identifier fmt name),
219
          pp_boolean_type,
220
          Some (true, false, [], []) )
244 221
    in
222
    let ghost_public = List.map pp_guarantee guarantees in
223
    fprintf fmt "@,%a%a%a%a@,@,%a;@,@,%t"
224
      (pp_print_list
225
         ~pp_sep:pp_print_semicolon
226
         ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
227
         (fun fmt pp -> pp fmt))
228
      ghost_public
229
      pp_ifstatefull pp_state_decl_and_reset
230
      (*Declare the step procedure*)
231
      (pp_procedure pp_step_procedure_name (build_pp_arg_step m)
232
         pp_contract_opt)
233
      AdaNoContent pp_ifstatefull
234
      (fun fmt -> fprintf fmt ";@,")
235
      (pp_package pp_axiomatize_package_name [] false)
236
      (fun fmt ->
237
         fprintf fmt
238
           "pragma Annotate (GNATProve, External_Axiomatization);@,\
239
            @,\
240
            %a;@,\
241
            %a;@,\
242
            %a"
243
           (*Declare the init predicate*)
244
           pp_init_predicate ()
245
           (*Declare the transition predicate*)
246
           pp_transition_predicate (m_spec_opt, m)
247
           (*Declare the invariant predicate*)
248
           pp_invariant_predicate ())
249
      (*Print the private section*)
250
      pp_private_section
251
  in
245 252

  
246
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
247
    let pp_generics = List.map pp_poly_type polymorphic_types in
253
  let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
254
  let pp_generics = List.map pp_poly_type polymorphic_types in
248 255

  
249
    fprintf fmt "@[<v>%a%t%a;@]@."
250
      (* Include all the subinstance package*)
251
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility))
252
      machines_to_import
253
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
254
      (*Begin the package*)
255
      (pp_package (pp_package_name m) pp_generics false)
256
      pp_content
257
end
256
  fprintf fmt "@[<v>%a%a;@]@."
257
    (* Include all the subinstance package*)
258
    (pp_print_list
259
       ~pp_sep:pp_print_semicolon
260
       ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
261
       (pp_with AdaNoVisibility))
262
    machines_to_import
263
    (*Begin the package*)
264
    (pp_package (pp_package_name m) pp_generics false)
265
    pp_content

Also available in: Unified diff