Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend.ml @ 04a188ec

History | View | Annotate | Download (6.65 KB)

1
(********************************************************************)
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
open Machine_code_types
14

    
15
open Misc_lustre_function
16
open Ada_printer
17
open Ada_backend_common
18

    
19
let indent_size = 2
20

    
21
(** Log at level 2 a string message with some indentation.
22
   @param indent the indentation level
23
   @param info the message
24
**)
25
let log_str_level_two indent info =
26
  let str_indent = String.make (indent*indent_size) ' ' in
27
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
28
  Log.report ~level:2 pp_message;
29
  Format.pp_print_flush Format.err_formatter ()
30

    
31
(** Write a new file with formatter
32
   @param destname folder where the file shoudl be created
33
   @param pp_filename function printing the filename
34
   @param pp_file function wich pretty print the file
35
   @param arg will be given to pp_filename and pp_file
36
**)
37
let write_file destname pp_filename pp_file arg =
38
  let path = asprintf "%s%a" destname pp_filename arg in
39
  let out = open_out path in
40
  let fmt = formatter_of_out_channel out in
41
  log_str_level_two 2 ("generating "^path);
42
  pp_file fmt arg;
43
  pp_print_flush fmt ();
44
  close_out out
45

    
46

    
47
(** Exception raised when a machine contains a feature not supported by the
48
  Ada backend*)
49
exception CheckFailed of string
50

    
51

    
52
(** Check that a machine match the requirement for an Ada compilation :
53
      - No constants.
54
   @param machine the machine to test
55
**)
56
let check machine =
57
  match machine.mconst with
58
    | [] -> ()
59
    | _ -> raise (CheckFailed "machine.mconst should be void")
60

    
61

    
62
let get_typed_submachines machines m =
63
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
64
  let submachines = List.map (get_machine machines) instances in
65
  List.map2
66
    (fun instance submachine ->
67
      let ident = (fst instance) in
68
      ident, (get_substitution m ident submachine, submachine))
69
    instances submachines
70

    
71
let extract_contract machines m =
72
  let rec find_submachine_from_ident ident = function
73
    | [] -> raise Not_found
74
    | h::t when h.mname.node_id = ident -> h
75
    | _::t -> find_submachine_from_ident ident t
76
  in
77
  let extract_ident eexpr =
78
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
79
      | Expr_ident ident -> ident
80
      | _ -> assert false
81
      (*
82
      | Expr_const cst -> assert false
83
      | Expr_tuple exprs -> assert false
84
      | Expr_ite (expr1, expr2, expr3) -> assert false
85
      | Expr_arrow (expr1, expr2)  -> assert false
86
      | Expr_fby (expr1, expr2) -> assert false
87
      | Expr_array exprs -> assert false
88
      | Expr_access (expr1, dim) -> assert false
89
      | Expr_power (expr1, dim) -> assert false
90
      | Expr_pre expr -> assert false
91
      | Expr_when (expr,ident,label) -> assert false
92
      | Expr_merge (ident, l) -> assert false
93
      | Expr_appl call -> assert false
94
      *)
95
  in
96
  match m.mspec with
97
    | Some (NodeSpec ident) ->
98
      begin
99
        let machine_spec = find_submachine_from_ident ident machines in
100
        let guarantees =
101
          match machine_spec.mspec with
102
            | Some (Contract contract) ->
103
                assert (contract.consts=[]);
104
                assert (contract.locals=[]);
105
                assert (contract.stmts=[]);
106
                assert (contract.assume=[]);
107
                List.map extract_ident contract.guarantees
108
            | _ -> assert false
109
        in
110
        let opt_machine_spec =
111
          match machine_spec.mstep.step_instrs with
112
            | [] -> None
113
            | _ -> Some machine_spec
114
        in
115
        (opt_machine_spec, guarantees)
116
      end
117
    | _ -> None, []
118

    
119
(** Main function of the Ada backend. It calls all the subfunction creating all
120
the file and fill them with Ada code representing the machines list given.
121
   @param basename name of the lustre file
122
   @param prog useless
123
   @param prog list of machines to translate
124
   @param dependencies useless
125
**)
126
let translate_to_ada basename prog machines dependencies =
127
  let module Ads = Ada_backend_ads.Main in
128
  let module Adb = Ada_backend_adb.Main in
129
  let module Wrapper = Ada_backend_wrapper.Main in
130

    
131
  let is_real_machine m =
132
    match m.mspec with
133
      | Some (Contract x) -> false
134
      | _ -> true
135
  in
136

    
137
  let filtered_machines = List.filter is_real_machine machines in
138

    
139
  let typed_submachines =
140
    List.map (get_typed_submachines machines) filtered_machines in
141
  
142
  let contracts = List.map (extract_contract machines) filtered_machines in
143

    
144
  let _machines = List.combine contracts filtered_machines in
145

    
146
  let _machines = List.combine typed_submachines _machines in
147

    
148
  let _pp_filename ext fmt (_, (_, machine)) =
149
    pp_machine_filename ext fmt machine in
150

    
151
  (* Extract the main machine if there is one *)
152
  let main_machine = (match !Options.main_node with
153
  | "" -> None
154
  | main_node -> (
155
    match Machine_code_common.get_machine_opt filtered_machines main_node with
156
    | None -> begin
157
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
158
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
159
    end
160
    | Some m -> Some m
161
  )) in
162

    
163
  let destname = !Options.dest_dir ^ "/" in
164

    
165
  log_str_level_two 1 "Checking machines";
166
  List.iter check machines;
167

    
168
  log_str_level_two 1 "Generating ads";
169
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
170

    
171
  log_str_level_two 1 "Generating adb";
172
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
173

    
174
  (* If a main node is given we generate a main adb file and a project file *)
175
  log_str_level_two 1 "Generating wrapper files";
176
  (match main_machine with
177
    | None -> ()
178
    | Some machine ->
179
        write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines filtered_machines machine)) machine;
180
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file filtered_machines basename) main_machine);
181
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
182
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
183

    
184

    
185
(* Local Variables: *)
186
(* compile-command:"make -C ../../.." *)
187
(* End: *)