Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/backends/Ada/ada_backend.ml | ||
|---|---|---|
| 11 | 11 |
|
| 12 | 12 |
open Format |
| 13 | 13 |
open Machine_code_types |
| 14 |
|
|
| 15 | 14 |
open Misc_lustre_function |
| 16 | 15 |
open Ada_backend_common |
| 17 | 16 |
|
| 18 | 17 |
let indent_size = 2 |
| 19 | 18 |
|
| 20 |
(** Log at level 2 a string message with some indentation. |
|
| 21 |
@param indent the indentation level |
|
| 22 |
@param info the message |
|
| 23 |
**) |
|
| 19 |
(** Log at level 2 a string message with some indentation. @param indent the |
|
| 20 |
indentation level @param info the message **) |
|
| 24 | 21 |
let log_str_level_two indent info = |
| 25 |
let str_indent = String.make (indent*indent_size) ' ' in
|
|
| 22 |
let str_indent = String.make (indent * indent_size) ' ' in
|
|
| 26 | 23 |
let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in |
| 27 | 24 |
Log.report ~level:2 pp_message; |
| 28 | 25 |
Format.pp_print_flush Format.err_formatter () |
| 29 | 26 |
|
| 30 |
(** Write a new file with formatter |
|
| 31 |
@param destname folder where the file shoudl be created |
|
| 32 |
@param pp_filename function printing the filename |
|
| 33 |
@param pp_file function wich pretty print the file |
|
| 34 |
@param arg will be given to pp_filename and pp_file |
|
| 35 |
**) |
|
| 27 |
(** Write a new file with formatter @param destname folder where the file shoudl |
|
| 28 |
be created @param pp_filename function printing the filename @param pp_file |
|
| 29 |
function wich pretty print the file @param arg will be given to pp_filename |
|
| 30 |
and pp_file **) |
|
| 36 | 31 |
let write_file destname pp_filename pp_file arg = |
| 37 | 32 |
let path = asprintf "%s%a" destname pp_filename arg in |
| 38 | 33 |
let out = open_out path in |
| 39 | 34 |
let fmt = formatter_of_out_channel out in |
| 40 |
log_str_level_two 2 ("generating "^path);
|
|
| 35 |
log_str_level_two 2 ("generating " ^ path);
|
|
| 41 | 36 |
pp_file fmt arg; |
| 42 | 37 |
pp_print_flush fmt (); |
| 43 | 38 |
close_out out |
| 44 | 39 |
|
| 45 |
|
|
| 46 |
(** Exception raised when a machine contains a feature not supported by the |
|
| 47 |
Ada backend*) |
|
| 48 | 40 |
exception CheckFailed of string |
| 41 |
(** Exception raised when a machine contains a feature not supported by the Ada |
|
| 42 |
backend*) |
|
| 49 | 43 |
|
| 50 |
|
|
| 51 |
(** Check that a machine match the requirement for an Ada compilation : |
|
| 52 |
- No constants. |
|
| 53 |
@param machine the machine to test |
|
| 54 |
**) |
|
| 44 |
(** Check that a machine match the requirement for an Ada compilation : - No |
|
| 45 |
constants. @param machine the machine to test **) |
|
| 55 | 46 |
let check machine = |
| 56 | 47 |
match machine.mconst with |
| 57 |
| [] -> () |
|
| 58 |
| _ -> raise (CheckFailed "machine.mconst should be void") |
|
| 59 |
|
|
| 48 |
| [] -> |
|
| 49 |
() |
|
| 50 |
| _ -> |
|
| 51 |
raise (CheckFailed "machine.mconst should be void") |
|
| 60 | 52 |
|
| 61 | 53 |
let get_typed_submachines machines m = |
| 62 |
let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in |
|
| 54 |
let instances = |
|
| 55 |
List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls |
|
| 56 |
in |
|
| 63 | 57 |
let submachines = List.map (get_machine machines) instances in |
| 64 | 58 |
List.map2 |
| 65 | 59 |
(fun instance submachine -> |
| 66 |
let ident = (fst instance) in
|
|
| 60 |
let ident = fst instance in
|
|
| 67 | 61 |
ident, (get_substitution m ident submachine, submachine)) |
| 68 | 62 |
instances submachines |
| 69 | 63 |
|
| 70 | 64 |
let extract_contract machines m = |
| 71 | 65 |
let rec find_submachine_from_ident ident = function |
| 72 |
| [] -> raise Not_found |
|
| 73 |
| h::_ when h.mname.node_id = ident -> h |
|
| 74 |
| _::t -> find_submachine_from_ident ident t |
|
| 66 |
| [] -> |
|
| 67 |
raise Not_found |
|
| 68 |
| h :: _ when h.mname.node_id = ident -> |
|
| 69 |
h |
|
| 70 |
| _ :: t -> |
|
| 71 |
find_submachine_from_ident ident t |
|
| 75 | 72 |
in |
| 76 | 73 |
let extract_ident eexpr = |
| 77 | 74 |
match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with |
| 78 |
| Expr_ident ident -> ident |
|
| 79 |
| _ -> assert false |
|
| 80 |
(* |
|
| 81 |
| Expr_const cst -> assert false |
|
| 82 |
| Expr_tuple exprs -> assert false |
|
| 83 |
| Expr_ite (expr1, expr2, expr3) -> assert false |
|
| 84 |
| Expr_arrow (expr1, expr2) -> assert false |
|
| 85 |
| Expr_fby (expr1, expr2) -> assert false |
|
| 86 |
| Expr_array exprs -> assert false |
|
| 87 |
| Expr_access (expr1, dim) -> assert false |
|
| 88 |
| Expr_power (expr1, dim) -> assert false |
|
| 89 |
| Expr_pre expr -> assert false |
|
| 90 |
| Expr_when (expr,ident,label) -> assert false |
|
| 91 |
| Expr_merge (ident, l) -> assert false |
|
| 92 |
| Expr_appl call -> assert false |
|
| 93 |
*) |
|
| 75 |
| Expr_ident ident -> |
|
| 76 |
ident |
|
| 77 |
| _ -> |
|
| 78 |
assert false |
|
| 79 |
(* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false | |
|
| 80 |
Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1, |
|
| 81 |
expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false | |
|
| 82 |
Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert |
|
| 83 |
false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert |
|
| 84 |
false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident, |
|
| 85 |
l) -> assert false | Expr_appl call -> assert false *) |
|
| 94 | 86 |
in |
| 95 | 87 |
match m.mspec.mnode_spec with |
| 96 |
| Some (NodeSpec ident) -> |
|
| 97 |
begin |
|
| 98 |
let machine_spec = find_submachine_from_ident ident machines in |
|
| 99 |
let guarantees = |
|
| 100 |
match machine_spec.mspec.mnode_spec with |
|
| 101 |
| Some (Contract contract) -> |
|
| 102 |
assert (contract.consts=[]); |
|
| 103 |
assert (contract.locals=[]); |
|
| 104 |
assert (contract.stmts=[]); |
|
| 105 |
assert (contract.assume=[]); |
|
| 106 |
List.map extract_ident contract.guarantees |
|
| 107 |
| _ -> assert false |
|
| 108 |
in |
|
| 109 |
let opt_machine_spec = |
|
| 110 |
match machine_spec.mstep.step_instrs with |
|
| 111 |
| [] -> None |
|
| 112 |
| _ -> Some machine_spec |
|
| 113 |
in |
|
| 114 |
(opt_machine_spec, guarantees) |
|
| 115 |
end |
|
| 116 |
| _ -> None, [] |
|
| 88 |
| Some (NodeSpec ident) -> |
|
| 89 |
let machine_spec = find_submachine_from_ident ident machines in |
|
| 90 |
let guarantees = |
|
| 91 |
match machine_spec.mspec.mnode_spec with |
|
| 92 |
| Some (Contract contract) -> |
|
| 93 |
assert (contract.consts = []); |
|
| 94 |
assert (contract.locals = []); |
|
| 95 |
assert (contract.stmts = []); |
|
| 96 |
assert (contract.assume = []); |
|
| 97 |
List.map extract_ident contract.guarantees |
|
| 98 |
| _ -> |
|
| 99 |
assert false |
|
| 100 |
in |
|
| 101 |
let opt_machine_spec = |
|
| 102 |
match machine_spec.mstep.step_instrs with |
|
| 103 |
| [] -> |
|
| 104 |
None |
|
| 105 |
| _ -> |
|
| 106 |
Some machine_spec |
|
| 107 |
in |
|
| 108 |
opt_machine_spec, guarantees |
|
| 109 |
| _ -> |
|
| 110 |
None, [] |
|
| 117 | 111 |
|
| 118 | 112 |
(** Main function of the Ada backend. It calls all the subfunction creating all |
| 119 |
the file and fill them with Ada code representing the machines list given. |
|
| 120 |
@param basename name of the lustre file |
|
| 121 |
@param prog list of machines to translate |
|
| 122 |
**) |
|
| 113 |
the file and fill them with Ada code representing the machines list given. |
|
| 114 |
@param basename name of the lustre file @param prog list of machines to |
|
| 115 |
translate **) |
|
| 123 | 116 |
let translate_to_ada basename machines = |
| 124 | 117 |
let module Ads = Ada_backend_ads.Main in |
| 125 | 118 |
let module Adb = Ada_backend_adb.Main in |
| 126 | 119 |
let module Wrapper = Ada_backend_wrapper.Main in |
| 127 |
|
|
| 128 | 120 |
let is_real_machine m = |
| 129 |
match m.mspec.mnode_spec with |
|
| 130 |
| Some (Contract _) -> false |
|
| 131 |
| _ -> true |
|
| 121 |
match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true |
|
| 132 | 122 |
in |
| 133 | 123 |
|
| 134 | 124 |
let filtered_machines = List.filter is_real_machine machines in |
| 135 | 125 |
|
| 136 | 126 |
let typed_submachines = |
| 137 |
List.map (get_typed_submachines machines) filtered_machines in |
|
| 138 |
|
|
| 127 |
List.map (get_typed_submachines machines) filtered_machines |
|
| 128 |
in |
|
| 129 |
|
|
| 139 | 130 |
let contracts = List.map (extract_contract machines) filtered_machines in |
| 140 | 131 |
|
| 141 | 132 |
let _machines = List.combine contracts filtered_machines in |
| ... | ... | |
| 143 | 134 |
let _machines = List.combine typed_submachines _machines in |
| 144 | 135 |
|
| 145 | 136 |
let _pp_filename ext fmt (_, (_, machine)) = |
| 146 |
pp_machine_filename ext fmt machine in |
|
| 137 |
pp_machine_filename ext fmt machine |
|
| 138 |
in |
|
| 147 | 139 |
|
| 148 | 140 |
(* Extract the main machine if there is one *) |
| 149 |
let main_machine = (match !Options.main_node with |
|
| 150 |
| "" -> None |
|
| 151 |
| main_node -> ( |
|
| 152 |
match Machine_code_common.get_machine_opt filtered_machines main_node with |
|
| 153 |
| None -> begin |
|
| 154 |
Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found; |
|
| 155 |
raise (Error.Error (Location.dummy_loc, Error.Main_not_found)) |
|
| 156 |
end |
|
| 157 |
| Some m -> Some m |
|
| 158 |
)) in |
|
| 141 |
let main_machine = |
|
| 142 |
match !Options.main_node with |
|
| 143 |
| "" -> |
|
| 144 |
None |
|
| 145 |
| main_node -> ( |
|
| 146 |
match Machine_code_common.get_machine_opt filtered_machines main_node with |
|
| 147 |
| None -> |
|
| 148 |
Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg |
|
| 149 |
Error.Main_not_found; |
|
| 150 |
raise (Error.Error (Location.dummy_loc, Error.Main_not_found)) |
|
| 151 |
| Some m -> |
|
| 152 |
Some m) |
|
| 153 |
in |
|
| 159 | 154 |
|
| 160 | 155 |
let destname = !Options.dest_dir ^ "/" in |
| 161 | 156 |
|
| ... | ... | |
| 171 | 166 |
(* If a main node is given we generate a main adb file and a project file *) |
| 172 | 167 |
log_str_level_two 1 "Generating wrapper files"; |
| 173 | 168 |
(match main_machine with |
| 174 |
| None -> () |
|
| 175 |
| Some machine -> |
|
| 176 |
write_file destname |
|
| 177 |
pp_main_filename |
|
| 178 |
(Wrapper.pp_main_adb (*get_typed_submachines filtered_machines machine*)) |
|
| 179 |
machine; |
|
| 180 |
write_file destname |
|
| 181 |
(fun fmt _ -> Wrapper.pp_project_name (basename^"_exe") fmt) |
|
| 182 |
(Wrapper.pp_project_file filtered_machines basename) |
|
| 183 |
main_machine); |
|
| 184 |
write_file destname |
|
| 185 |
Wrapper.pp_project_configuration_name |
|
| 169 |
| None -> |
|
| 170 |
() |
|
| 171 |
| Some machine -> |
|
| 172 |
write_file destname pp_main_filename Wrapper.pp_main_adb |
|
| 173 |
(*get_typed_submachines filtered_machines machine*) |
|
| 174 |
machine; |
|
| 175 |
write_file destname |
|
| 176 |
(fun fmt _ -> Wrapper.pp_project_name (basename ^ "_exe") fmt) |
|
| 177 |
(Wrapper.pp_project_file filtered_machines basename) |
|
| 178 |
main_machine); |
|
| 179 |
write_file destname Wrapper.pp_project_configuration_name |
|
| 186 | 180 |
(fun fmt _ -> Wrapper.pp_project_configuration_file fmt) |
| 187 | 181 |
basename; |
| 188 | 182 |
write_file destname |
| 189 |
(fun fmt _ -> Wrapper.pp_project_name (basename^"_lib") fmt)
|
|
| 183 |
(fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
|
|
| 190 | 184 |
(Wrapper.pp_project_file filtered_machines basename) |
| 191 |
None; |
|
| 192 |
|
|
| 185 |
None |
|
| 193 | 186 |
|
| 194 | 187 |
(* Local Variables: *) |
| 195 | 188 |
(* compile-command:"make -C ../../.." *) |
Also available in: Unified diff
reformatting