Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/backends/Ada/ada_backend_adb.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 |
... | ... | |
20 | 21 |
open Ada_backend_common |
21 | 22 |
|
22 | 23 |
(** Main module for generating packages bodies **) |
23 |
module Main = struct |
|
24 |
(** Printing function for basic assignement [var := value]. |
|
25 | 24 |
|
26 |
@param fmt the formater to print on @param var_name the name of the |
|
27 |
variable @param value the value to be assigned **) |
|
28 |
let pp_assign env fmt var value = |
|
29 |
fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value |
|
25 |
(** Printing function for basic assignement [var := value]. |
|
30 | 26 |
|
31 |
(** Printing function for instruction. See {!type:Machine_code_types.instr_t} |
|
32 |
for more details on machine types. |
|
27 |
@param fmt the formater to print on @param var_name the name of the |
|
28 |
variable @param value the value to be assigned **) |
|
29 |
let pp_assign env fmt var value = |
|
30 |
fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value |
|
33 | 31 |
|
34 |
@param typed_submachines list of all typed machine instances of this |
|
35 |
machine @param machine the current machine @param fmt the formater to |
|
36 |
print on @param instr the instruction to print **) |
|
37 |
let rec pp_machine_instr typed_submachines env instr fmt = |
|
38 |
let pp_instr = pp_machine_instr typed_submachines env in |
|
39 |
(* Print args for a step call *) |
|
40 |
let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in |
|
41 |
(* Print a when branch of a case *) |
|
42 |
let pp_when (cond, instrs) fmt = |
|
43 |
fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs) |
|
44 |
in |
|
45 |
(* Print a case *) |
|
46 |
let pp_case fmt (g, hl) = |
|
47 |
fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block |
|
48 |
(List.map pp_when hl) |
|
49 |
in |
|
50 |
(* Print a if *) |
|
51 |
(* If neg is true the we must test for the negation of the condition. It |
|
52 |
first check that we don't have a negation and a else case, if so it |
|
53 |
inverses the two branch and remove the negation doing a recursive call. *) |
|
54 |
let pp_if fmt (neg, g, instrs1, instrs2) = |
|
55 |
let pp_cond = |
|
56 |
if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x |
|
57 |
else pp_value env |
|
58 |
in |
|
59 |
let pp_else = |
|
60 |
match instrs2 with |
|
61 |
| None -> |
|
62 |
fun fmt -> fprintf fmt "" |
|
63 |
| Some i2 -> |
|
64 |
fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2) |
|
65 |
in |
|
66 |
fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block |
|
67 |
(List.map pp_instr instrs1) |
|
68 |
pp_else |
|
69 |
in |
|
70 |
match get_instr_desc instr with |
|
71 |
(* no reset *) |
|
72 |
| MNoReset _ -> |
|
73 |
() |
|
74 |
(* TODO: handle clear_reset *) |
|
75 |
| MClearReset -> |
|
76 |
() |
|
77 |
(* reset *) |
|
78 |
| MSetReset i when List.mem_assoc i typed_submachines -> |
|
79 |
let substitution, submachine = get_instance i typed_submachines in |
|
80 |
let pp_package = |
|
81 |
pp_package_name_with_polymorphic substitution submachine |
|
82 |
in |
|
83 |
let args = |
|
84 |
if is_machine_statefull submachine then [ [ pp_state i ] ] else [] |
|
85 |
in |
|
86 |
pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args) |
|
87 |
| MLocalAssign (ident, value) -> |
|
88 |
pp_assign env fmt ident value |
|
89 |
| MStateAssign (ident, value) -> |
|
90 |
pp_assign env fmt ident value |
|
91 |
| MStep ([ i0 ], i, vl) when is_builtin_fun i -> |
|
92 |
let value = mk_val (Fun (i, vl)) i0.var_type in |
|
93 |
pp_assign env fmt i0 value |
|
94 |
| MStep (il, i, vl) when List.mem_assoc i typed_submachines -> |
|
95 |
let substitution, submachine = get_instance i typed_submachines in |
|
96 |
let pp_package = |
|
97 |
pp_package_name_with_polymorphic substitution submachine |
|
98 |
in |
|
99 |
let input = List.map (fun x fmt -> pp_value env fmt x) vl in |
|
100 |
let output = List.map pp_var_name il in |
|
101 |
let args = |
|
102 |
(if is_machine_statefull submachine then [ [ pp_state i ] ] else []) |
|
103 |
@ (if input != [] then [ input ] else []) |
|
104 |
@ if output != [] then [ output ] else [] |
|
105 |
in |
|
106 |
pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args) |
|
107 |
| MBranch (_, []) -> |
|
108 |
assert false |
|
109 |
| MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true -> |
|
110 |
pp_if fmt (build_if g c1 i1 tl) |
|
111 |
| MBranch (g, hl) -> |
|
112 |
pp_case fmt (g, hl) |
|
113 |
| MComment s -> |
|
114 |
let lines = String.split_on_char '\n' s in |
|
115 |
fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines |
|
116 |
| _ -> |
|
117 |
assert false |
|
32 |
(** Printing function for instruction. See {!type:Machine_code_types.instr_t} |
|
33 |
for more details on machine types. |
|
118 | 34 |
|
119 |
(** Print the definition of the step procedure from a machine. |
|
120 |
|
|
121 |
@param typed_submachines list of all typed machine instances of this |
|
122 |
machine @param fmt the formater to print on @param machine the machine **) |
|
123 |
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) = |
|
124 |
let transform_local_to_state_assign instr = |
|
125 |
match instr.instr_desc with |
|
126 |
| MLocalAssign (ident, value) -> |
|
127 |
{ instr with instr_desc = MStateAssign (ident, value) } |
|
128 |
| _ -> |
|
129 |
instr |
|
35 |
@param typed_submachines list of all typed machine instances of this |
|
36 |
machine @param machine the current machine @param fmt the formater to |
|
37 |
print on @param instr the instruction to print **) |
|
38 |
let rec pp_machine_instr typed_submachines env instr fmt = |
|
39 |
let pp_instr = pp_machine_instr typed_submachines env in |
|
40 |
(* Print args for a step call *) |
|
41 |
let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in |
|
42 |
(* Print a when branch of a case *) |
|
43 |
let pp_when (cond, instrs) fmt = |
|
44 |
fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs) |
|
45 |
in |
|
46 |
(* Print a case *) |
|
47 |
let pp_case fmt (g, hl) = |
|
48 |
fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block |
|
49 |
(List.map pp_when hl) |
|
50 |
in |
|
51 |
(* Print a if *) |
|
52 |
(* If neg is true the we must test for the negation of the condition. It |
|
53 |
first check that we don't have a negation and a else case, if so it |
|
54 |
inverses the two branch and remove the negation doing a recursive call. *) |
|
55 |
let pp_if fmt (neg, g, instrs1, instrs2) = |
|
56 |
let pp_cond = |
|
57 |
if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x |
|
58 |
else pp_value env |
|
130 | 59 |
in |
131 |
let pp_local_ghost_list, spec_instrs =
|
|
132 |
match m_spec_opt with
|
|
60 |
let pp_else =
|
|
61 |
match instrs2 with
|
|
133 | 62 |
| None -> |
134 |
[], [] |
|
135 |
| Some m_spec -> |
|
136 |
( List.map |
|
137 |
(build_pp_var_decl_local (Some (true, false, [], []))) |
|
138 |
(List.filter |
|
139 |
(fun x -> not (List.mem x.var_id guarantees)) |
|
140 |
m_spec.mstep.step_locals), |
|
141 |
List.map transform_local_to_state_assign m_spec.mstep.step_instrs ) |
|
63 |
fun fmt -> fprintf fmt "" |
|
64 |
| Some i2 -> |
|
65 |
fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2) |
|
66 |
in |
|
67 |
fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block |
|
68 |
(List.map pp_instr instrs1) |
|
69 |
pp_else |
|
70 |
in |
|
71 |
match get_instr_desc instr with |
|
72 |
(* no reset *) |
|
73 |
| MNoReset _ -> |
|
74 |
() |
|
75 |
(* TODO: handle clear_reset *) |
|
76 |
| MClearReset -> |
|
77 |
() |
|
78 |
(* reset *) |
|
79 |
| MSetReset i when List.mem_assoc i typed_submachines -> |
|
80 |
let substitution, submachine = get_instance i typed_submachines in |
|
81 |
let pp_package = |
|
82 |
pp_package_name_with_polymorphic substitution submachine |
|
142 | 83 |
in |
143 |
let pp_local_list =
|
|
144 |
List.map (build_pp_var_decl_local None) m.mstep.step_locals
|
|
84 |
let args =
|
|
85 |
if is_machine_statefull submachine then [ [ pp_state i ] ] else []
|
|
145 | 86 |
in |
146 |
let pp_instr_list = |
|
147 |
List.map |
|
148 |
(pp_machine_instr typed_submachines env) |
|
149 |
(m.mstep.step_instrs @ spec_instrs) |
|
87 |
pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args) |
|
88 |
| MLocalAssign (ident, value) -> |
|
89 |
pp_assign env fmt ident value |
|
90 |
| MStateAssign (ident, value) -> |
|
91 |
pp_assign env fmt ident value |
|
92 |
| MStep ([ i0 ], i, vl) when is_builtin_fun i -> |
|
93 |
let value = mk_val (Fun (i, vl)) i0.var_type in |
|
94 |
pp_assign env fmt i0 value |
|
95 |
| MStep (il, i, vl) when List.mem_assoc i typed_submachines -> |
|
96 |
let substitution, submachine = get_instance i typed_submachines in |
|
97 |
let pp_package = |
|
98 |
pp_package_name_with_polymorphic substitution submachine |
|
150 | 99 |
in |
151 |
let content = |
|
152 |
AdaProcedureContent |
|
153 |
( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ]) |
|
154 |
@ if pp_local_list = [] then [] else [ pp_local_list ]), |
|
155 |
pp_instr_list ) |
|
100 |
let input = List.map (fun x fmt -> pp_value env fmt x) vl in |
|
101 |
let output = List.map pp_var_name il in |
|
102 |
let args = |
|
103 |
(if is_machine_statefull submachine then [ [ pp_state i ] ] else []) |
|
104 |
@ (if input != [] then [ input ] else []) |
|
105 |
@ if output != [] then [ output ] else [] |
|
156 | 106 |
in |
157 |
pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content |
|
107 |
pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args) |
|
108 |
| MBranch (_, []) -> |
|
109 |
assert false |
|
110 |
| MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true -> |
|
111 |
pp_if fmt (build_if g c1 i1 tl) |
|
112 |
| MBranch (g, hl) -> |
|
113 |
pp_case fmt (g, hl) |
|
114 |
| MComment s -> |
|
115 |
let lines = String.split_on_char '\n' s in |
|
116 |
fprintf fmt "%a" (pp_print_list ~pp_sep:pp_print_nothing pp_oneline_comment) lines |
|
117 |
| _ -> |
|
118 |
assert false |
|
158 | 119 |
|
159 |
(** Print the definition of the reset procedure from a machine.
|
|
120 |
(** Print the definition of the step procedure from a machine.
|
|
160 | 121 |
|
161 |
@param typed_submachines list of all typed machine instances of this |
|
162 |
machine @param fmt the formater to print on @param machine the machine **) |
|
163 |
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) = |
|
164 |
let build_assign = function |
|
165 |
| var -> |
|
166 |
mkinstr (MStateAssign (var, mk_default_value var.var_type)) |
|
167 |
in |
|
168 |
let env, memory = |
|
169 |
match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory |
|
170 |
in |
|
171 |
let assigns = List.map build_assign memory in |
|
172 |
let pp_instr_list = |
|
173 |
List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit) |
|
174 |
in |
|
175 |
pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt |
|
176 |
(AdaProcedureContent ([], pp_instr_list)) |
|
122 |
@param typed_submachines list of all typed machine instances of this |
|
123 |
machine @param fmt the formater to print on @param machine the machine **) |
|
124 |
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) = |
|
125 |
let transform_local_to_state_assign instr = |
|
126 |
match instr.instr_desc with |
|
127 |
| MLocalAssign (ident, value) -> |
|
128 |
{ instr with instr_desc = MStateAssign (ident, value) } |
|
129 |
| _ -> |
|
130 |
instr |
|
131 |
in |
|
132 |
let pp_local_ghost_list, spec_instrs = |
|
133 |
match m_spec_opt with |
|
134 |
| None -> |
|
135 |
[], [] |
|
136 |
| Some m_spec -> |
|
137 |
( List.map |
|
138 |
(build_pp_var_decl_local (Some (true, false, [], []))) |
|
139 |
(List.filter |
|
140 |
(fun x -> not (List.mem x.var_id guarantees)) |
|
141 |
m_spec.mstep.step_locals), |
|
142 |
List.map transform_local_to_state_assign m_spec.mstep.step_instrs ) |
|
143 |
in |
|
144 |
let pp_local_list = |
|
145 |
List.map (build_pp_var_decl_local None) m.mstep.step_locals |
|
146 |
in |
|
147 |
let pp_instr_list = |
|
148 |
List.map |
|
149 |
(pp_machine_instr typed_submachines env) |
|
150 |
(m.mstep.step_instrs @ spec_instrs) |
|
151 |
in |
|
152 |
let content = |
|
153 |
AdaProcedureContent |
|
154 |
( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ]) |
|
155 |
@ if pp_local_list = [] then [] else [ pp_local_list ]), |
|
156 |
pp_instr_list ) |
|
157 |
in |
|
158 |
pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content |
|
177 | 159 |
|
178 |
(** Print the package definition(ads) of a machine. It requires the list of |
|
179 |
all typed instance. A typed submachine instance is (ident, type_machine) |
|
180 |
with ident the instance name and typed_machine is (substitution, machine) |
|
181 |
with machine the machine associated to the instance and substitution the |
|
182 |
instanciation of all its polymorphic types. @param fmt the formater to |
|
183 |
print on @param typed_submachines list of all typed machine instances of |
|
184 |
this machine @param m the machine **) |
|
185 |
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) |
|
186 |
= |
|
187 |
let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in |
|
188 |
let pp_reset fmt = |
|
189 |
if is_machine_statefull machine then |
|
190 |
fprintf fmt "%a;@,@," |
|
191 |
(pp_reset_definition env typed_submachines) |
|
192 |
(machine, opt_spec_machine) |
|
193 |
else fprintf fmt "" |
|
194 |
in |
|
195 |
let aux pkgs (id, _) = |
|
196 |
try |
|
197 |
let pkg, _ = List.assoc id ada_supported_funs in |
|
198 |
if List.mem pkg pkgs then pkgs else pkg :: pkgs |
|
199 |
with Not_found -> pkgs |
|
200 |
in |
|
201 |
let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in |
|
202 |
let pp_content fmt = |
|
203 |
fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset |
|
204 |
(*Define the step procedure*) |
|
205 |
(pp_step_definition env typed_submachines) |
|
206 |
(machine, opt_spec_machine, guarantees) |
|
207 |
in |
|
208 |
fprintf fmt "%a%t%a;@." |
|
209 |
(* Include all the required packages*) |
|
210 |
(Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) |
|
211 |
packages |
|
212 |
(Utils.pp_final_char_if_non_empty ";@,@," packages) |
|
213 |
(*Print package*) |
|
214 |
(pp_package (pp_package_name machine) [] true) |
|
215 |
pp_content |
|
216 |
end |
|
160 |
(** Print the definition of the reset procedure from a machine. |
|
161 |
|
|
162 |
@param typed_submachines list of all typed machine instances of this |
|
163 |
machine @param fmt the formater to print on @param machine the machine **) |
|
164 |
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) = |
|
165 |
let build_assign = function |
|
166 |
| var -> |
|
167 |
mkinstr (MStateAssign (var, mk_default_value var.var_type)) |
|
168 |
in |
|
169 |
let env, memory = |
|
170 |
match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory |
|
171 |
in |
|
172 |
let assigns = List.map build_assign memory in |
|
173 |
let pp_instr_list = |
|
174 |
List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit) |
|
175 |
in |
|
176 |
pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt |
|
177 |
(AdaProcedureContent ([], pp_instr_list)) |
|
178 |
|
|
179 |
(** Print the package definition(ads) of a machine. It requires the list of |
|
180 |
all typed instance. A typed submachine instance is (ident, type_machine) |
|
181 |
with ident the instance name and typed_machine is (substitution, machine) |
|
182 |
with machine the machine associated to the instance and substitution the |
|
183 |
instanciation of all its polymorphic types. @param fmt the formater to |
|
184 |
print on @param typed_submachines list of all typed machine instances of |
|
185 |
this machine @param m the machine **) |
|
186 |
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) |
|
187 |
= |
|
188 |
let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in |
|
189 |
let pp_reset fmt = |
|
190 |
if is_machine_statefull machine then |
|
191 |
fprintf fmt "%a;@,@," |
|
192 |
(pp_reset_definition env typed_submachines) |
|
193 |
(machine, opt_spec_machine) |
|
194 |
else fprintf fmt "" |
|
195 |
in |
|
196 |
let aux pkgs (id, _) = |
|
197 |
try |
|
198 |
let pkg, _ = List.assoc id ada_supported_funs in |
|
199 |
if List.mem pkg pkgs then pkgs else pkg :: pkgs |
|
200 |
with Not_found -> pkgs |
|
201 |
in |
|
202 |
let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in |
|
203 |
let pp_content fmt = |
|
204 |
fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset |
|
205 |
(*Define the step procedure*) |
|
206 |
(pp_step_definition env typed_submachines) |
|
207 |
(machine, opt_spec_machine, guarantees) |
|
208 |
in |
|
209 |
fprintf fmt "%a%a;@." |
|
210 |
(* Include all the required packages*) |
|
211 |
(pp_print_list |
|
212 |
~pp_sep:pp_print_semicolon |
|
213 |
~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,") |
|
214 |
(pp_with AdaPrivate)) |
|
215 |
packages |
|
216 |
(*Print package*) |
|
217 |
(pp_package (pp_package_name machine) [] true) |
|
218 |
pp_content |
|
217 | 219 |
|
218 | 220 |
(* Local Variables: *) |
219 | 221 |
(* compile-command: "make -C ../../.." *) |
Also available in: Unified diff
another step towards refactoring