Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

src/backends/Ada/ada_backend_ads.ml
25 25
module Main =
26 26
struct
27 27

  
28
  (** Print a new statement instantiating a generic package.
29
     @param fmt the formater to print on
30
     @param substitutions the instanciation substitution
31
     @param machine the machine to instanciate
32
  **)
33
  let pp_new_package fmt (substitutions, machine) =
34
    let pp_name = pp_package_name machine in
35
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
36
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
37
    pp_package_instanciation pp_new_name pp_name fmt instanciations
38 28

  
39
  (** Print a precondition in aspect
40
     @param fmt the formater to print on
41
     @param expr the expession to print as pre
42
  **)
43
  let pp_pre fmt expr =
44
    fprintf fmt "Pre => %a"
45
      pp_clean_ada_identifier expr
29
  let suffixOld = "_old"
30
  let suffixNew = "_new"
31
  let pp_transition_name fmt = fprintf fmt "transition"
32
  let pp_state_name_transition suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
46 33

  
47
  (** Print a postcondition in aspect
48
     @param fmt the formater to print on
49
     @param expr the expession to print as pre
50
  **)
51
  let pp_post fmt ident =
52
    fprintf fmt "Post => %a"
53
      pp_clean_ada_identifier ident
54 34

  
55
  (** Print the declaration of a procedure with a contract
56
     @param pp_prototype the prototype printer
57
     @param fmt the formater to print on
58
     @param contract the contract for the function to declare
59
  **)
60
  let pp_contract guarantees fmt =
61
    fprintf fmt "@,  @[<v>Global => null%t%a@]"
62
      (Utils.pp_final_char_if_non_empty ",@," guarantees)
63
      (Utils.fprintf_list ~sep:",@," pp_post) guarantees
64 35

  
65
(*
66
  let pp_transition_name fmt = fprintf fmt "transition"
67
  let pp_state_name_transition suffix fmt = fprintf fmt "%t_%s" pp_state_name suffix
68 36

  
69
  (** Printing function for basic assignement [var_name := value].
37
  (** Printing function for basic assignement [var := value].
70 38

  
71 39
      @param fmt the formater to print on
72 40
      @param var_name the name of the variable
73 41
      @param value the value to be assigned
74 42
   **)
75
  let pp_basic_assign m fmt var_name value =
76
    fprintf fmt "%a = %a"
77
      (pp_access_var m) var_name
78
      (pp_value m) value
43
  let pp_local_eq env fmt var value =
44
    fprintf fmt "%t = %a"
45
      (pp_var_name var)
46
      (pp_value env) value
79 47

  
48
  (** Printing function for basic assignement [var := value].
49

  
50
      @param fmt the formater to print on
51
      @param var_name the name of the variable
52
      @param value the value to be assigned
53
   **)
54
  let pp_state_eq env fmt var value =
55
    fprintf fmt "%t = %a"
56
      (pp_access (pp_state_name_transition suffixNew) (pp_var_name var))
57
      (pp_value env) value
80 58

  
81 59
  (** Printing function for instruction. See
82 60
      {!type:Machine_code_types.instr_t} for more details on
......
87 65
      @param fmt the formater to print on
88 66
      @param instr the instruction to print
89 67
   **)
90
  let rec pp_machine_instr typed_submachines machine instr fmt =
91
    let pp_instr = pp_machine_instr typed_submachines machine in
92
    (* Print args for a step call *)
93
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
94
    let pp_args vl il fmt =
95
      fprintf fmt "@[%a@]%t@[%a@]"
96
        (Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
97
        (Utils.pp_final_char_if_non_empty ",@," il)
98
        (Utils.fprintf_list ~sep:",@ " pp_var_name) il
99
    in
100
    (* Print a when branch of a case *)
101
    let pp_when (cond, instrs) fmt =
102
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
103
    in
104
    (* Print a case *)
105
    let pp_case fmt (g, hl) =
106
      fprintf fmt "case %a is@,%aend case"
107
        (pp_value machine) g
108
        pp_block (List.map pp_when hl)
109
    in
110
    (* Print a if *)
111
    (* If neg is true the we must test for the negation of the condition. It
112
       first check that we don't have a negation and a else case, if so it
113
       inverses the two branch and remove the negation doing a recursive
114
       call. *)
115
    let rec pp_if neg fmt (g, instrs1, instrs2) =
116
      match neg, instrs2 with
117
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
118
        | _ ->
119
          let pp_cond =
120
            if neg then
121
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
122
            else
123
              pp_value machine
124
          in
125
          let pp_else = match instrs2 with
126
            | None -> fun fmt -> fprintf fmt ""
127
            | Some i2 -> fun fmt ->
128
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
129
          in
130
          fprintf fmt "if %a then@,%a%tend if"
131
            pp_cond g
132
            pp_block (List.map pp_instr instrs1)
133
            pp_else
134
    in
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
135 71
    match get_instr_desc instr with
136 72
      (* no reset *)
137 73
      | MNoReset _ -> ()
......
139 75
      | MReset i when List.mem_assoc i typed_submachines ->
140 76
          let (substitution, submachine) = get_instance i typed_submachines in
141 77
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
142
          pp_call fmt (pp_package_access (pp_package, pp_name), [pp_state i])
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)
143 80
      | MLocalAssign (ident, value) ->
144
          pp_basic_assign machine fmt ident value
81
          pp_local_eq env fmt ident value
145 82
      | MStateAssign (ident, value) ->
146
          pp_basic_assign machine fmt ident value
83
          pp_state_eq env fmt ident value
147 84
      | MStep ([i0], i, vl) when is_builtin_fun i ->
148 85
          let value = mk_val (Fun (i, vl)) i0.var_type in
149
          pp_basic_assign machine fmt i0 value
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
          
150 91
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
151 92
          let (substitution, submachine) = get_instance i typed_submachines in
152
          pp_package_call
153
            pp_step_procedure_name
154
            fmt
155
            (substitution, submachine, pp_state i, Some (pp_args vl il))
156
      | MBranch (_, []) -> assert false
157
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
158
          let neg = c1=tag_false in
159
          let other = match tl with
160
            | []         -> None
161
            | [(c2, i2)] -> Some i2
162
            | _          -> assert false
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 [])
163 100
          in
164
          pp_if neg fmt (g, i1, other)
165
      | MBranch (g, hl) -> pp_case fmt (g, hl)
166
      | MComment s  ->
167
          let lines = String.split_on_char '\n' s in
168
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
101
          fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)
102
      | MComment s -> ()
169 103
      | _ -> assert false
170 104

  
105

  
106

  
107

  
108

  
109

  
110

  
111

  
112

  
113

  
114

  
115

  
116

  
117

  
118

  
119

  
120

  
121

  
171 122
  (** Print the expression function representing the transition predicate.
172 123
     @param fmt the formater to print on
173 124
     @param machine the machine
174 125
  **)
175
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
176
    let spec_instrs = match opt_spec_machine with
177
      | None -> []
178
      | Some m -> m.mstep.step_instrs
179
    in
180
    fprintf fmt "function %t (%a; %a) return Boolean is (@,  @[<v>%a@,@]) with Ghost"
181
      pp_transition_name
182
      pp_var_decl_mode (In, pp_state_name_transition "old", pp_state_type)
183
      pp_var_decl_mode (In, pp_state_name_transition "new", pp_state_type)
184
      (Utils.fprintf_list ~sep:" and@," (pp_machine_instr typed_submachines m)) (m.mstep.step_instrs@spec_instrs)*)
126
  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
130
    let inputs = build_pp_var_decl_step_input AdaIn None m in
131
    let outputs = build_pp_var_decl_step_output AdaIn None m in
132
    let instrs = push_if_in_expr m.mstep.step_instrs in
133
    let content = List.map (pp_machine_instr typed_submachines env) instrs in
134
    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))
185 136
    
137

  
138

  
139

  
140

  
141

  
142

  
143

  
144

  
145

  
146

  
147

  
148

  
149
  (** Print a new statement instantiating a generic package.
150
     @param fmt the formater to print on
151
     @param substitutions the instanciation substitution
152
     @param machine the machine to instanciate
153
  **)
154
  let pp_new_package fmt (substitutions, machine) =
155
    let pp_name = pp_package_name machine in
156
    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
158
    pp_package_instanciation pp_new_name pp_name fmt instanciations
159

  
186 160
  (** Remove duplicates from a list according to a given predicate.
187 161
     @param eq the predicate defining equality
188 162
     @param l the list to parse
......
210 184
     @param typed_submachines list of all typed submachines of this machine
211 185
     @param m the machine
212 186
  **)
213
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), m)) =
187
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
214 188
    let typed_machines = snd (List.split typed_submachines) in
215 189
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
216 190
    
......
225 199

  
226 200
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
227 201
      (*Declare the state type*)
228
      (pp_type_decl pp_state_type AdaLimitedPrivate)
202
      (pp_type_decl pp_state_type AdaPrivate)
229 203
      (*Declare the reset procedure*)
230 204
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
231 205
    in
232

  
233
    let vars = List.map (build_pp_var_decl AdaNoMode) m.mmemory in
234
    let states = List.map build_pp_state_decl_from_subinstance typed_instances in
235
    let var_lists = (if vars = [] then [] else [vars])@(if states = [] then [] else [states]) in
236

  
237
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a"
238
      (*Instantiate the polymorphic type that need to be instantiated*)
239
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
240
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
241
      (*Define the state type*)
242
      (pp_record pp_state_type) var_lists
206
    
207
    let vars_spec = match m_spec_opt with
208
      | None -> []
209
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode None) m_spec.mstep.step_locals
243 210
    in
211
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
212
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
213
    let var_lists =
214
      (if states = [] then [] else [states]) @
215
      (if vars = [] then [] else [vars])@
216
      (if vars_spec = [] then [] else [vars_spec]) in
244 217
    
245 218
    let pp_ifstatefull fmt pp =
246 219
      if is_machine_statefull m then
......
249 222
        fprintf fmt ""
250 223
    in
251 224

  
225
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,@,%a"
226
      (*Instantiate the polymorphic type that need to be instantiated*)
227
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
228
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
229
      (*Define the state type*)
230
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
231
        
232
      (*Declare the transition predicate*)
233
      (pp_transition_predicate false typed_submachines) (m_spec_opt, m)
234
    in
235

  
252 236
    let pp_content fmt =
253
      let pp_contract_opt = match guarantees with
254
                              | [] -> None
255
                              | _ ->  Some (pp_contract guarantees) in
256
      fprintf fmt "%a%a%a%a" (* %a;@, *)
237
      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
        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
            pp_clean_ada_identifier fmt x
247
        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 [])
254
        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))
259
      in
260
      fprintf fmt "%a%a%a@,@,%a;%t" (* %a;@, *)
257 261
        pp_ifstatefull pp_state_decl_and_reset
258 262
        
259
        (*Declare the transition predicate*)
260
        (* pp_transition_predicate typed_submachines) (opt_spec_machine, m) *)
261
        
262 263
        (*Declare the step procedure*)
263 264
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
264 265
        
265 266
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
266 267
        
268
        (*Declare the transition predicate*)
269
        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)
270
        
267 271
        (*Print the private section*)
268
        pp_ifstatefull pp_private_section
272
        pp_private_section
269 273
    in
270 274
    
271 275
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in

Also available in: Unified diff