Revision 05f85b44
Added by Guillaume DAVY almost 6 years ago
src/backends/Ada/ada_backend_ads.ml | ||
---|---|---|
31 | 31 |
|
32 | 32 |
let suffixOld = "_old" |
33 | 33 |
let suffixNew = "_new" |
34 |
let pp_invariant_name fmt = fprintf fmt "invariant"
|
|
34 |
let pp_invariant_name fmt = fprintf fmt "inv" |
|
35 | 35 |
let pp_transition_name fmt = fprintf fmt "transition" |
36 | 36 |
let pp_init_name fmt = fprintf fmt "init" |
37 | 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" |
|
40 |
|
|
41 |
|
|
42 |
|
|
43 |
(** Printing function for basic assignement [var := value]. |
|
44 |
|
|
45 |
@param fmt the formater to print on |
|
46 |
@param var_name the name of the variable |
|
47 |
@param value the value to be assigned |
|
48 |
**) |
|
49 |
let pp_local_eq env fmt var value = |
|
50 |
fprintf fmt "%t = %a" |
|
51 |
(pp_var_name var) |
|
52 |
(pp_value env) value |
|
53 |
|
|
54 |
(** Printing function for basic assignement [var := value]. |
|
55 |
|
|
56 |
@param fmt the formater to print on |
|
57 |
@param var_name the name of the variable |
|
58 |
@param value the value to be assigned |
|
59 |
**) |
|
60 |
let pp_state_eq env fmt var value = |
|
61 |
fprintf fmt "%t = %a" |
|
62 |
(pp_access (pp_state_name_predicate suffixNew) (pp_var_name var)) |
|
63 |
(pp_value env) value |
|
64 |
|
|
65 |
(** Printing function for instruction. See |
|
66 |
{!type:Machine_code_types.instr_t} for more details on |
|
67 |
machine types. |
|
68 |
|
|
69 |
@param typed_submachines list of all typed machine instances of this machine |
|
70 |
@param machine the current machine |
|
71 |
@param fmt the formater to print on |
|
72 |
@param instr the instruction to print |
|
73 |
**) |
|
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 |
|
|
122 |
|
|
123 |
|
|
124 |
|
|
125 |
|
|
126 |
|
|
127 |
|
|
128 |
|
|
129 |
|
|
130 |
|
|
131 |
|
|
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 |
|
144 |
|
|
145 |
|
|
146 |
|
|
147 |
|
|
38 |
let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize" |
|
148 | 39 |
|
149 | 40 |
(** Print the expression function representing the transition predicate. |
150 | 41 |
@param fmt the formater to print on |
151 | 42 |
@param machine the machine |
152 | 43 |
**) |
153 |
let pp_init_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
|
|
44 |
let pp_init_predicate typed_submachines fmt (opt_spec_machine, m) = |
|
154 | 45 |
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 |
|
|
162 |
|
|
46 |
pp_predicate pp_init_name [[new_state]] true fmt None |
|
163 | 47 |
|
164 | 48 |
(** Print the expression function representing the transition predicate. |
165 | 49 |
@param fmt the formater to print on |
166 | 50 |
@param machine the machine |
167 | 51 |
**) |
168 |
let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
|
|
52 |
let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) = |
|
169 | 53 |
let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in |
170 | 54 |
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 |
|
172 | 55 |
let inputs = build_pp_var_decl_step_input AdaIn None m in |
173 | 56 |
let outputs = build_pp_var_decl_step_output AdaIn None m in |
174 |
let instrs = push_if_in_expr m.mstep.step_instrs in |
|
175 |
let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in |
|
176 |
let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in |
|
177 |
pp_predicate_special pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content)) |
|
178 |
|
|
179 |
let build_pp_past mode with_st i = (mode, pp_past_name (i+1), pp_state_type , with_st) |
|
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 |
|
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 |
|
220 |
|
|
221 |
|
|
57 |
pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None |
|
222 | 58 |
|
59 |
let pp_invariant_predicate typed_submachines fmt (opt_spec_machine, m) = |
|
60 |
pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None |
|
223 | 61 |
|
224 | 62 |
(** Print a new statement instantiating a generic package. |
225 | 63 |
@param fmt the formater to print on |
... | ... | |
229 | 67 |
let pp_new_package fmt (substitutions, machine) = |
230 | 68 |
let pp_name = pp_package_name machine in |
231 | 69 |
let pp_new_name = pp_package_name_with_polymorphic substitutions machine 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
|
|
70 |
let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
|
|
233 | 71 |
pp_package_instanciation pp_new_name pp_name fmt instanciations |
234 | 72 |
|
235 | 73 |
(** Remove duplicates from a list according to a given predicate. |
... | ... | |
259 | 97 |
@param typed_submachines list of all typed submachines of this machine |
260 | 98 |
@param m the machine |
261 | 99 |
**) |
262 |
let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees, past_size), m)) =
|
|
100 |
let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) = |
|
263 | 101 |
let typed_machines = snd (List.split typed_submachines) in |
264 | 102 |
let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in |
265 | 103 |
|
... | ... | |
268 | 106 |
let polymorphic_types = find_all_polymorphic_type m in |
269 | 107 |
|
270 | 108 |
let typed_machines_to_instanciate = |
271 |
(*List.filter (fun (l, _) -> l != [])*) typed_machines_set in
|
|
109 |
List.filter (fun (l, _) -> l != []) typed_machines_set in
|
|
272 | 110 |
|
273 | 111 |
let typed_instances = List.filter is_submachine_statefull typed_submachines in |
274 | 112 |
|
275 | 113 |
let memories = match m_spec_opt with |
276 | 114 |
| None -> [] |
277 |
| Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, [], [])) x)) m.mmemory |
|
115 |
| Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
|
|
278 | 116 |
in |
279 | 117 |
let ghost_private = memories in |
280 | 118 |
|
281 | 119 |
let vars_spec = match m_spec_opt with |
282 | 120 |
| None -> [] |
283 |
| Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, [], []))) (m_spec.mmemory) |
|
121 |
| Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
|
|
284 | 122 |
in |
285 | 123 |
let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in |
286 | 124 |
let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in |
... | ... | |
296 | 134 |
in |
297 | 135 |
|
298 | 136 |
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 |
|
137 |
let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
|
|
138 |
let contract = Some (false, false, [], [init]) in
|
|
301 | 139 |
fprintf fmt "%t;@,@,%a;@,@," |
302 | 140 |
(*Declare the state type*) |
303 | 141 |
(pp_type_decl pp_state_type AdaPrivate) |
... | ... | |
307 | 145 |
in |
308 | 146 |
|
309 | 147 |
let pp_private_section fmt = |
310 |
fprintf fmt "@,private@,@,%a%t%a;@,@,%a;@,@,%a%a%t%a"
|
|
148 |
fprintf fmt "@,private@,@,%a%t%a%t%a" |
|
311 | 149 |
(*Instantiate the polymorphic type that need to be instantiated*) |
312 | 150 |
(Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate |
313 | 151 |
(Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate) |
... | ... | |
315 | 153 |
(*Define the state type*) |
316 | 154 |
pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists) |
317 | 155 |
|
318 |
(*Declare the init predicate*) |
|
319 |
(pp_init_predicate false typed_submachines) (m_spec_opt, m) |
|
320 |
|
|
321 |
(*Declare the transition predicate*) |
|
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 | 156 |
(Utils.pp_final_char_if_non_empty ";@,@," ghost_private) |
328 | 157 |
(Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private |
329 | 158 |
in |
... | ... | |
344 | 173 |
@(if input!=[] then [input] else []) |
345 | 174 |
@(if output!=[] then [output] else []) |
346 | 175 |
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] |
|
176 |
let transition fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_transition_name, args) in |
|
177 |
let invariant fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_invariant_name, [[pp_state_name]]) in |
|
178 |
[invariant], [transition;invariant] |
|
353 | 179 |
end |
354 | 180 |
else |
355 | 181 |
[], [] |
... | ... | |
359 | 185 |
if post_conditions = [] && pre_conditions = [] then |
360 | 186 |
None |
361 | 187 |
else |
362 |
Some (false, pre_conditions, post_conditions) |
|
188 |
Some (false, false, pre_conditions, post_conditions)
|
|
363 | 189 |
in |
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" |
|
190 |
let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, false, [], []))) in |
|
191 |
let ghost_public = List.map pp_guarantee guarantees in |
|
192 |
fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t" |
|
368 | 193 |
|
369 | 194 |
(Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public |
370 | 195 |
(Utils.pp_final_char_if_non_empty ";@,@," ghost_public) |
... | ... | |
376 | 201 |
|
377 | 202 |
pp_ifstatefull (fun fmt -> fprintf fmt ";@,") |
378 | 203 |
|
379 |
(*Declare the init predicate*) |
|
380 |
(pp_init_predicate true typed_submachines) (m_spec_opt, m) |
|
381 |
|
|
382 |
(*Declare the transition predicate*) |
|
383 |
(pp_transition_predicate true typed_submachines) (m_spec_opt, m) |
|
384 |
|
|
385 |
(*Declare the transition predicate*) |
|
386 |
(pp_invariant_predicate true typed_submachines) (past_size, m_spec_opt, m) |
|
204 |
(pp_package (pp_axiomatize_package_name) [] false) |
|
205 |
(fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a" |
|
206 |
(*Declare the init predicate*) |
|
207 |
(pp_init_predicate typed_submachines) (m_spec_opt, m) |
|
208 |
(*Declare the transition predicate*) |
|
209 |
(pp_transition_predicate typed_submachines) (m_spec_opt, m) |
|
210 |
(*Declare the invariant predicate*) |
|
211 |
(pp_invariant_predicate typed_submachines) (m_spec_opt, m) |
|
212 |
) |
|
387 | 213 |
|
388 | 214 |
(*Print the private section*) |
389 | 215 |
pp_private_section |
390 | 216 |
in |
391 | 217 |
|
392 | 218 |
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
|
|
219 |
let pp_generics = List.map pp_poly_type polymorphic_types in
|
|
394 | 220 |
|
395 | 221 |
fprintf fmt "@[<v>%a%t%a;@]@." |
396 | 222 |
|
Also available in: Unified diff
Ada: Start cleaning Ada to prepare for why beckend