Project

General

Profile

Download (6.62 KB) Statistics
| Branch: | Tag: | Revision:
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
open Misc_lustre_function
15
open Ada_backend_common
16

    
17
let indent_size = 2
18

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

    
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 **)
31
let write_file destname pp_filename pp_file arg =
32
  let path = asprintf "%s%a" destname pp_filename arg in
33
  let out = open_out path in
34
  let fmt = formatter_of_out_channel out in
35
  log_str_level_two 2 ("generating " ^ path);
36
  pp_file fmt arg;
37
  pp_print_flush fmt ();
38
  close_out out
39

    
40
exception CheckFailed of string
41
(** Exception raised when a machine contains a feature not supported by the Ada
42
    backend*)
43

    
44
(** Check that a machine match the requirement for an Ada compilation : - No
45
    constants. @param machine the machine to test **)
46
let check machine =
47
  match machine.mconst with
48
  | [] ->
49
    ()
50
  | _ ->
51
    raise (CheckFailed "machine.mconst should be void")
52

    
53
let get_typed_submachines machines m =
54
  let instances =
55
    List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
56
  in
57
  let submachines = List.map (get_machine machines) instances in
58
  List.map2
59
    (fun instance submachine ->
60
      let ident = fst instance in
61
      ident, (get_substitution m ident submachine, submachine))
62
    instances submachines
63

    
64
let extract_contract machines m =
65
  let rec find_submachine_from_ident ident = function
66
    | [] ->
67
      raise Not_found
68
    | h :: _ when h.mname.node_id = ident ->
69
      h
70
    | _ :: t ->
71
      find_submachine_from_ident ident t
72
  in
73
  let extract_ident eexpr =
74
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
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 *)
86
  in
87
  match m.mspec.mnode_spec with
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, []
111

    
112
(** Main function of the Ada backend. It calls all the subfunction creating all
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 **)
116
let translate_to_ada basename machines =
117
  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
  let is_real_machine m =
121
    match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
122
  in
123

    
124
  let filtered_machines = List.filter is_real_machine machines in
125

    
126
  let typed_submachines =
127
    List.map (get_typed_submachines machines) filtered_machines
128
  in
129

    
130
  let contracts = List.map (extract_contract machines) filtered_machines in
131

    
132
  let _machines = List.combine contracts filtered_machines in
133

    
134
  let _machines = List.combine typed_submachines _machines in
135

    
136
  let _pp_filename ext fmt (_, (_, machine)) =
137
    pp_machine_filename ext fmt machine
138
  in
139

    
140
  (* Extract the main machine if there is one *)
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
154

    
155
  let destname = !Options.dest_dir ^ "/" in
156

    
157
  log_str_level_two 1 "Checking machines";
158
  List.iter check machines;
159

    
160
  log_str_level_two 1 "Generating ads";
161
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
162

    
163
  log_str_level_two 1 "Generating adb";
164
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
165

    
166
  (* 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
  (match main_machine with
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
180
    (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
181
    basename;
182
  write_file destname
183
    (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
184
    (Wrapper.pp_project_file filtered_machines basename)
185
    None
186

    
187
(* Local Variables: *)
188
(* compile-command:"make -C ../../.." *)
189
(* End: *)
(2-2/11)