Project

General

Profile

Download (6.62 KB) Statistics
| Branch: | Tag: | Revision:
1 f20d8ac7 Christophe Garion
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12
open Format
13 48a6309c Guillaume DAVY
open Machine_code_types
14 230b168e Guillaume DAVY
open Misc_lustre_function
15 fd834769 Guillaume DAVY
open Ada_backend_common
16
17
let indent_size = 2
18
19 ca7ff3f7 Lélio Brun
(** Log at level 2 a string message with some indentation. @param indent the
20
    indentation level @param info the message **)
21 fd834769 Guillaume DAVY
let log_str_level_two indent info =
22 ca7ff3f7 Lélio Brun
  let str_indent = String.make (indent * indent_size) ' ' in
23 fd834769 Guillaume DAVY
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
24 e6492c59 Guillaume DAVY
  Log.report ~level:2 pp_message;
25
  Format.pp_print_flush Format.err_formatter ()
26 fd834769 Guillaume DAVY
27 ca7ff3f7 Lélio Brun
(** 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 **)
31 fd834769 Guillaume DAVY
let write_file destname pp_filename pp_file arg =
32
  let path = asprintf "%s%a" destname pp_filename arg in
33 48a6309c Guillaume DAVY
  let out = open_out path in
34
  let fmt = formatter_of_out_channel out in
35 ca7ff3f7 Lélio Brun
  log_str_level_two 2 ("generating " ^ path);
36 fd834769 Guillaume DAVY
  pp_file fmt arg;
37
  pp_print_flush fmt ();
38 e6492c59 Guillaume DAVY
  close_out out
39 fd834769 Guillaume DAVY
40 c419ca44 Guillaume DAVY
exception CheckFailed of string
41 ca7ff3f7 Lélio Brun
(** Exception raised when a machine contains a feature not supported by the Ada
42
    backend*)
43 c419ca44 Guillaume DAVY
44 ca7ff3f7 Lélio Brun
(** Check that a machine match the requirement for an Ada compilation : - No
45
    constants. @param machine the machine to test **)
46 c419ca44 Guillaume DAVY
let check machine =
47
  match machine.mconst with
48 ca7ff3f7 Lélio Brun
  | [] ->
49
    ()
50
  | _ ->
51
    raise (CheckFailed "machine.mconst should be void")
52 3de9f6e4 Guillaume DAVY
53 09d7b39f Guillaume DAVY
let get_typed_submachines machines m =
54 ca7ff3f7 Lélio Brun
  let instances =
55
    List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
56
  in
57 09d7b39f Guillaume DAVY
  let submachines = List.map (get_machine machines) instances in
58 3de9f6e4 Guillaume DAVY
  List.map2
59
    (fun instance submachine ->
60 ca7ff3f7 Lélio Brun
      let ident = fst instance in
61 3de9f6e4 Guillaume DAVY
      ident, (get_substitution m ident submachine, submachine))
62 09d7b39f Guillaume DAVY
    instances submachines
63 3de9f6e4 Guillaume DAVY
64 230b168e Guillaume DAVY
let extract_contract machines m =
65
  let rec find_submachine_from_ident ident = function
66 ca7ff3f7 Lélio Brun
    | [] ->
67
      raise Not_found
68
    | h :: _ when h.mname.node_id = ident ->
69
      h
70
    | _ :: t ->
71
      find_submachine_from_ident ident t
72 230b168e Guillaume DAVY
  in
73
  let extract_ident eexpr =
74
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
75 ca7ff3f7 Lélio Brun
    | 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 *)
86 230b168e Guillaume DAVY
  in
87 7ee5f69e Lélio Brun
  match m.mspec.mnode_spec with
88 ca7ff3f7 Lélio Brun
  | 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, []
111 230b168e Guillaume DAVY
112 fd834769 Guillaume DAVY
(** Main function of the Ada backend. It calls all the subfunction creating all
113 ca7ff3f7 Lélio Brun
    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 **)
116 ca7e8027 Lélio Brun
let translate_to_ada basename machines =
117 f20d8ac7 Christophe Garion
  let module Ads = Ada_backend_ads.Main in
118
  let module Adb = Ada_backend_adb.Main in
119
  let module Wrapper = Ada_backend_wrapper.Main in
120 230b168e Guillaume DAVY
  let is_real_machine m =
121 ca7ff3f7 Lélio Brun
    match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
122 230b168e Guillaume DAVY
  in
123
124
  let filtered_machines = List.filter is_real_machine machines in
125
126 09d7b39f Guillaume DAVY
  let typed_submachines =
127 ca7ff3f7 Lélio Brun
    List.map (get_typed_submachines machines) filtered_machines
128
  in
129
130 230b168e Guillaume DAVY
  let contracts = List.map (extract_contract machines) filtered_machines in
131
132
  let _machines = List.combine contracts filtered_machines in
133 3de9f6e4 Guillaume DAVY
134 230b168e Guillaume DAVY
  let _machines = List.combine typed_submachines _machines in
135 3de9f6e4 Guillaume DAVY
136 230b168e Guillaume DAVY
  let _pp_filename ext fmt (_, (_, machine)) =
137 ca7ff3f7 Lélio Brun
    pp_machine_filename ext fmt machine
138
  in
139 3de9f6e4 Guillaume DAVY
140 fd834769 Guillaume DAVY
  (* Extract the main machine if there is one *)
141 ca7ff3f7 Lélio Brun
  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
154 c419ca44 Guillaume DAVY
155 fd834769 Guillaume DAVY
  let destname = !Options.dest_dir ^ "/" in
156 c419ca44 Guillaume DAVY
157 fd834769 Guillaume DAVY
  log_str_level_two 1 "Checking machines";
158 c419ca44 Guillaume DAVY
  List.iter check machines;
159 48a6309c Guillaume DAVY
160 fd834769 Guillaume DAVY
  log_str_level_two 1 "Generating ads";
161 3de9f6e4 Guillaume DAVY
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
162 48a6309c Guillaume DAVY
163 fd834769 Guillaume DAVY
  log_str_level_two 1 "Generating adb";
164 3de9f6e4 Guillaume DAVY
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
165 48a6309c Guillaume DAVY
166 fd834769 Guillaume DAVY
  (* If a main node is given we generate a main adb file and a project file *)
167
  log_str_level_two 1 "Generating wrapper files";
168 61e0c3c4 Guillaume DAVY
  (match main_machine with
169 ca7ff3f7 Lélio Brun
  | 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
180 ca7e8027 Lélio Brun
    (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
181
    basename;
182
  write_file destname
183 ca7ff3f7 Lélio Brun
    (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
184 ca7e8027 Lélio Brun
    (Wrapper.pp_project_file filtered_machines basename)
185 ca7ff3f7 Lélio Brun
    None
186 f20d8ac7 Christophe Garion
187
(* Local Variables: *)
188
(* compile-command:"make -C ../../.." *)
189
(* End: *)