Project

General

Profile

« Previous | Next » 

Revision 173a2a8f

Added by Guillaume DAVY almost 3 years ago

Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second
problem is that the approache requires existential quantification for inputs and
locals. It works for integers and boolean but not for floats. Some complex
solution could be found like writing an iterator for floats, expanding all
local variable and store all the required inputs in ghost variable.

View differences:

src/backends/Ada/ada_backend_ads.ml
21 21
open Ada_printer
22 22
open Ada_backend_common
23 23

  
24

  
25

  
24 26
(** Functions printing the .ads file **)
25 27
module Main =
26 28
struct
27 29

  
30
  let rec init f = function i when i < 0 -> [] | i -> (f i)::(init f (i-1)) (*should be replaced by the init of list from ocaml std lib*)
28 31

  
29 32
  let suffixOld = "_old"
30 33
  let suffixNew = "_new"
34
  let pp_invariant_name fmt = fprintf fmt "invariant"
31 35
  let pp_transition_name fmt = fprintf fmt "transition"
32
  let pp_state_name_transition suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
33

  
36
  let pp_init_name fmt = fprintf fmt "init"
37
  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
38
  let pp_name_generic fmt = fprintf fmt "name"
39
  let pp_type_generic fmt = fprintf fmt "string"
34 40

  
35 41

  
36 42

  
......
53 59
   **)
54 60
  let pp_state_eq env fmt var value =
55 61
    fprintf fmt "%t = %a"
56
      (pp_access (pp_state_name_transition suffixNew) (pp_var_name var))
62
      (pp_access (pp_state_name_predicate suffixNew) (pp_var_name var))
57 63
      (pp_value env) value
58 64

  
59 65
  (** Printing function for instruction. See
......
65 71
      @param fmt the formater to print on
66 72
      @param instr the instruction to print
67 73
   **)
68
  let rec pp_machine_instr typed_submachines env instr fmt =
69
    let pp_instr = pp_machine_instr typed_submachines env in
70
    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_transition suffix) i in
71
    match get_instr_desc instr with
72
      (* no reset *)
73
      | MNoReset _ -> ()
74
      (* reset  *)
75
      | MReset i when List.mem_assoc i typed_submachines ->
76
          let (substitution, submachine) = get_instance i typed_submachines in
77
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
78
          let args = if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [] in
79
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
80
      | MLocalAssign (ident, value) ->
81
          pp_local_eq env fmt ident value
82
      | MStateAssign (ident, value) ->
83
          pp_state_eq env fmt ident value
84
      | MStep ([i0], i, vl) when is_builtin_fun i ->
85
          let value = mk_val (Fun (i, vl)) i0.var_type in
86
          if List.mem_assoc i0.var_id env then
87
            pp_state_eq env fmt i0 value
88
          else
89
            pp_local_eq env fmt i0 value
90
          
91
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
92
          let (substitution, submachine) = get_instance i typed_submachines in
93
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
94
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
95
          let output = List.map pp_var_name il in
96
          let args =
97
            (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])
98
              @(if input!=[] then [input] else [])
99
              @(if output!=[] then [output] else [])
100
          in
101
          fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)
102
      | MComment s -> ()
103
      | _ -> assert false
74
  let pp_machine_instr typed_submachines env (pps, assigned) instr =
75
    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_predicate suffix) i in
76
    let fresh x l = not (List.exists (fun y -> String.equal x.var_id y.var_id) l) in
77
    let pp, newvals =
78
      match get_instr_desc instr with
79
        (* no reset *)
80
        | MNoReset _ -> ((fun fmt -> ()), [])
81
        (* reset  *)
82
        | MReset i when List.mem_assoc i typed_submachines ->
83
            let (substitution, submachine) = get_instance i typed_submachines in
84
            let pp_package = pp_package_name_with_polymorphic substitution submachine in
85
            let args = if is_machine_statefull submachine then [[pp_state suffixNew i]] else [] in
86
            ((fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_init_name), args)),
87
            [])
88
        | MLocalAssign (ident, value) ->
89
            assert(fresh ident assigned);
90
            ((fun fmt -> pp_local_eq env fmt ident value),
91
            [ident])
92
        | MStateAssign (ident, value) ->
93
            assert(fresh ident assigned);
94
            ((fun fmt -> pp_state_eq env fmt ident value),
95
            [ident])
96
        | MStep ([i0], i, vl) when is_builtin_fun i ->
97
            assert(fresh i0 assigned);
98
            let value = mk_val (Fun (i, vl)) i0.var_type in
99
            ((fun fmt -> (if List.mem_assoc i0.var_id env then
100
              pp_state_eq env fmt i0 value
101
            else
102
              pp_local_eq env fmt i0 value)),
103
            [i0])
104
        | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
105
            assert(List.for_all (fun x -> fresh x assigned) il);
106
            let (substitution, submachine) = get_instance i typed_submachines in
107
            let pp_package = pp_package_name_with_polymorphic substitution submachine in
108
            let input = List.map (fun x fmt -> pp_value env fmt x) vl in
109
            let output = List.map pp_var_name il in
110
            let args =
111
              (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])
112
                @(if input!=[] then [input] else [])
113
                @(if output!=[] then [output] else [])
114
            in
115
            ((fun fmt -> fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)),
116
            il)
117
        | MComment s -> ((fun fmt -> ()), [])
118
        | _ -> assert false
119
      in
120
      (pp::pps, newvals@assigned)
121

  
104 122

  
105 123

  
106 124

  
......
112 130

  
113 131

  
114 132

  
133
let pp_predicate_special pp_name args fmt content_opt =
134
  let rec quantify pp_content = function
135
    | [] -> pp_content
136
    | (pp_var, pp_type)::q -> fun fmt ->
137
      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)
138
  in
139
  let content = match content_opt with
140
    | Some (locals, booleans) -> Some (quantify (fun fmt -> Utils.fprintf_list ~sep:"@,and " (fun fmt pp->pp fmt) fmt booleans) locals)
141
    | None -> None
142
  in
143
  pp_predicate pp_name args fmt content
115 144

  
116 145

  
117 146

  
118 147

  
119 148

  
149
  (** Print the expression function representing the transition predicate.
150
     @param fmt the formater to print on
151
     @param machine the machine
152
  **)
153
  let pp_init_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
154
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
155
    let env = [] in
156
    let instrs = push_if_in_expr m.minit in
157
    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in
158
    pp_predicate_special pp_init_name ([[new_state]]) fmt (if prototype then None else Some ([], content))
159
    
160

  
161

  
120 162

  
121 163

  
122 164
  (** Print the expression function representing the transition predicate.
......
124 166
     @param machine the machine
125 167
  **)
126 168
  let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
127
    let old_state = (AdaIn, pp_state_name_transition suffixOld, pp_state_type, None) in
128
    let new_state = (AdaIn, pp_state_name_transition suffixNew, pp_state_type, None) in
129
    let env = List.map (fun x -> x.var_id, pp_state_name_transition suffixOld) m.mmemory in
169
    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
170
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
171
    let env = List.map (fun x -> x.var_id, pp_state_name_predicate suffixOld) m.mmemory in
130 172
    let inputs = build_pp_var_decl_step_input AdaIn None m in
131 173
    let outputs = build_pp_var_decl_step_output AdaIn None m in
132 174
    let instrs = push_if_in_expr m.mstep.step_instrs in
133
    let content = List.map (pp_machine_instr typed_submachines env) instrs in
175
    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in
134 176
    let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in
135
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
136
    
137

  
138

  
139

  
140

  
141

  
177
    pp_predicate_special pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
142 178

  
179
  let build_pp_past mode with_st i = (mode, pp_past_name (i+1), pp_state_type , with_st)
143 180

  
181
  let pp_invariant_predicate prototype typed_submachines fmt (past_size, opt_spec_machine, m) =
182
    let pp_state nbr = if nbr = 0 then pp_state_name else pp_past_name nbr in
183
    if past_size < 1 then fprintf fmt "" else
184
    begin
185
      let pp_var x fmt =
186
          pp_clean_ada_identifier fmt x
187
      in
188
      let input = List.map pp_var_name m.mstep.step_inputs in
189
      let output = List.map pp_var_name m.mstep.step_outputs in
190
      let args =
191
        [[pp_old pp_state_name;pp_state_name]]
192
          @(if input!=[] then [input] else [])
193
          @(if output!=[] then [output] else [])
194
      in
195
      let transition fmt = pp_call fmt (pp_transition_name, args) in
144 196

  
197
      let pp_append_nbr pp nbr fmt = fprintf fmt "%t_%i" pp nbr in
198
      let pp_transition nbr fmt =
199
        assert(is_machine_statefull m);
200
        let args =
201
          [[pp_past_name (nbr+1);pp_state nbr]]
202
            @(if input!=[] then [input] else [])
203
            @(if output!=[] then [output] else [])
204
        in
205
        pp_call fmt (pp_transition_name, args)
206
      in
207
      let build_chain nbr =
208
        assert (nbr > 0);
209
        pp_and (init pp_transition nbr)
210
      in
211
      let pp_init nbr fmt = pp_call fmt (pp_init_name, [[pp_state nbr]]) in
212
      let rec build_initial nbr = pp_and (match nbr with
213
        | 0 -> [pp_init 0]
214
        | i when i > 0 -> [pp_init i;build_chain i]
215
        | _ -> assert false)
216
      in
217
      let content = pp_or ((build_chain (past_size-1))::(init build_initial (past_size-1))) in
218
      fprintf fmt ";@,@,%a" (pp_predicate pp_invariant_name [init (build_pp_past AdaIn None) (past_size-1);[build_pp_state_decl AdaIn None]]) (if prototype then None else Some content)
219
    end
145 220

  
146 221

  
147 222

  
......
154 229
  let pp_new_package fmt (substitutions, machine) =
155 230
    let pp_name = pp_package_name machine in
156 231
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
157
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
232
    let instanciations = ((pp_name_generic, pp_adastring pp_name))::(List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions) in
158 233
    pp_package_instanciation pp_new_name pp_name fmt instanciations
159 234

  
160 235
  (** Remove duplicates from a list according to a given predicate.
......
184 259
     @param typed_submachines list of all typed submachines of this machine
185 260
     @param m the machine
186 261
  **)
187
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
262
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees, past_size), m)) =
188 263
    let typed_machines = snd (List.split typed_submachines) in
189 264
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
190 265
    
......
193 268
    let polymorphic_types = find_all_polymorphic_type m in
194 269
    
195 270
    let typed_machines_to_instanciate =
196
      List.filter (fun (l, _) -> l != []) typed_machines_set in
271
      (*List.filter (fun (l, _) -> l != [])*) typed_machines_set in
197 272

  
198 273
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
199 274

  
200
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
201
      (*Declare the state type*)
202
      (pp_type_decl pp_state_type AdaPrivate)
203
      (*Declare the reset procedure*)
204
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
275
    let memories = match m_spec_opt with
276
      | None -> []
277
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, [], [])) x)) m.mmemory
205 278
    in
279
    let ghost_private = memories in
206 280
    
207 281
    let vars_spec = match m_spec_opt with
208 282
      | None -> []
209
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode None) m_spec.mstep.step_locals
283
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, [], []))) (m_spec.mmemory)
210 284
    in
211 285
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
212 286
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
213 287
    let var_lists =
214 288
      (if states = [] then [] else [states]) @
215
      (if vars = [] then [] else [vars])@
216
      (if vars_spec = [] then [] else [vars_spec]) in
289
      (if vars = [] then [] else [vars]) in
217 290
    
218 291
    let pp_ifstatefull fmt pp =
219 292
      if is_machine_statefull m then
......
222 295
        fprintf fmt ""
223 296
    in
224 297

  
225
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,@,%a"
298
    let pp_state_decl_and_reset fmt =
299
      let init fmt = pp_call fmt (pp_init_name, [[pp_state_name]]) in
300
      let contract = Some (false, [], [init]) in
301
      fprintf fmt "%t;@,@,%a;@,@,"
302
        (*Declare the state type*)
303
        (pp_type_decl pp_state_type AdaPrivate)
304
        
305
        (*Declare the reset procedure*)
306
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
307
    in
308

  
309
    let pp_private_section fmt =
310
      fprintf fmt "@,private@,@,%a%t%a;@,@,%a;@,@,%a%a%t%a"
226 311
      (*Instantiate the polymorphic type that need to be instantiated*)
227 312
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
228 313
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
314
      
229 315
      (*Define the state type*)
230 316
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
231 317
        
318
      (*Declare the init predicate*)
319
      (pp_init_predicate false typed_submachines) (m_spec_opt, m)
320
        
232 321
      (*Declare the transition predicate*)
233 322
      (pp_transition_predicate false typed_submachines) (m_spec_opt, m)
323
        
324
      (*Declare the transition predicate*)
325
      (pp_invariant_predicate false typed_submachines) (past_size, m_spec_opt, m)
326
        
327
      (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
328
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
234 329
    in
235 330

  
236 331
    let pp_content fmt =
237 332
      let pp_contract_opt =
238
        let ghost_memory = match m_spec_opt with
239
          | None -> []
240
          | Some m_spec -> m_spec.mstep.step_locals
241
        in
242 333
        let pp_var x fmt =
243
          if List.exists (fun var -> var.var_id == x) ghost_memory then
244
            pp_access pp_state_name (fun fmt -> pp_clean_ada_identifier fmt x) fmt
245
          else
246 334
            pp_clean_ada_identifier fmt x
247 335
        in
248
        let input = List.map pp_var_name m.mstep.step_inputs in
249
        let output = List.map pp_var_name m.mstep.step_outputs in
250
        let args =
251
          (if is_machine_statefull m then [[pp_old pp_state_name;pp_state_name]] else [])
252
            @(if input!=[] then [input] else [])
253
            @(if output!=[] then [output] else [])
336
        let guarantee_post_conditions = List.map pp_var guarantees in
337
        let state_pre_conditions, state_post_conditions =
338
          if is_machine_statefull m then
339
          begin
340
            let input = List.map pp_var_name m.mstep.step_inputs in
341
            let output = List.map pp_var_name m.mstep.step_outputs in
342
            let args =
343
              [[pp_old pp_state_name;pp_state_name]]
344
                @(if input!=[] then [input] else [])
345
                @(if output!=[] then [output] else [])
346
            in
347
            let transition fmt = pp_call fmt (pp_transition_name, args) in
348
            let invariant fmt = pp_call fmt (pp_invariant_name, [init (fun i->pp_past_name (i+1)) (past_size-1);[pp_state_name]]) in
349
            if past_size > 0 then
350
              [invariant], [transition;invariant]
351
            else
352
              [], [transition]
353
          end
354
          else
355
            [], []
254 356
        in
255
        let transition fmt = pp_call fmt (pp_transition_name, args) in
256
        match guarantees with
257
          | [] -> Some (false, [], [transition])
258
          | _ ->  Some (false, [], transition::(List.map pp_var guarantees))
357
        let post_conditions = state_post_conditions@guarantee_post_conditions in
358
        let pre_conditions = state_pre_conditions in
359
        if post_conditions = [] && pre_conditions = [] then
360
          None
361
        else
362
          Some (false, pre_conditions, post_conditions)
259 363
      in
260
      fprintf fmt "%a%a%a@,@,%a;%t" (* %a;@, *)
364
      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, [], []))) in
365
      let pasts = List.map pp_var_decl (init (build_pp_past AdaNoMode (Some (true, [], []))) (past_size-1)) in
366
      let ghost_public = pasts@(List.map pp_guarantee guarantees) in
367
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%a%a;%t"
368
        
369
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
370
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
371
        
261 372
        pp_ifstatefull pp_state_decl_and_reset
262 373
        
263 374
        (*Declare the step procedure*)
......
265 376
        
266 377
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
267 378
        
379
        (*Declare the init predicate*)
380
        (pp_init_predicate true typed_submachines) (m_spec_opt, m)
381
        
268 382
        (*Declare the transition predicate*)
269 383
        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)
270 384
        
385
        (*Declare the transition predicate*)
386
        (pp_invariant_predicate true typed_submachines) (past_size, m_spec_opt, m)
387
        
271 388
        (*Print the private section*)
272 389
        pp_private_section
273 390
    in
274 391
    
275
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
276
    let pp_generics = List.map pp_poly_types polymorphic_types in
392
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
393
    let pp_generics = (pp_var_decl (AdaNoMode, pp_name_generic, pp_type_generic , None))::(List.map pp_poly_type polymorphic_types) in
277 394
    
278 395
    fprintf fmt "@[<v>%a%t%a;@]@."
279 396
      
280 397
      (* Include all the subinstance package*)
281
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) machines_to_import
398
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
282 399
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
283 400
      
284 401
      (*Begin the package*)

Also available in: Unified diff