Project

General

Profile

« Previous | Next » 

Revision f20d8ac7

Added by Christophe Garion almost 3 years ago

Ada: skeletons for Ada compiler

View differences:

src/_tags.in
7 7
"checks": include
8 8
"parsers": include
9 9
"backends": include
10
"backends/Ada": include
10 11
"backends/C": include
11 12
"backends/Horn": include
12 13
"backends/EMF": include
src/backends/Ada/.merlin
1
REC
src/backends/Ada/ada_backend.ml
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

  
14
let translate_to_ada basename prog machines dependencies =
15
  let module Ads = Ada_backend_ads.Main in
16
  let module Adb = Ada_backend_adb.Main in
17
  let module Wrapper = Ada_backend_wrapper.Main in
18
  print_endline "Ada code generated!"
19

  
20
(* Local Variables: *)
21
(* compile-command:"make -C ../../.." *)
22
(* End: *)
src/backends/Ada/ada_backend_adb.ml
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
module Main =
13
struct
14
end
src/backends/Ada/ada_backend_ads.ml
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
module Main =
13
struct
14
end
src/backends/Ada/ada_backend_wrapper.ml
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
module Main =
13
struct
14
end
src/compiler_stages.ml
9 9
  match !Options.output, !Options.spec with
10 10
  | "C", "C" -> true
11 11
  | _ -> false
12
     
12

  
13 13

  
14 14
(* check whether a source file has a compiled header, if not, generate the
15 15
   compiled header *)
......
68 68
  let orig, prog =
69 69
    if !Options.global_inline && !Options.main_node <> "" then
70 70
      (if !Options.witnesses then prog else []),
71
      Inliner.global_inline basename prog 
71
      Inliner.global_inline basename prog
72 72
    else (* if !Option.has_local_inline *)
73 73
      [],
74 74
      Inliner.local_inline prog (* type_env clock_env *)
......
88 88

  
89 89
  (* Registering and checking machine types *)
90 90
  if Machine_types.is_active then Machine_types.load prog;
91
  
91

  
92 92

  
93 93
  (* Generating a .lusi header file only *)
94 94
  if !Options.lusi then
......
96 96
       exported as a lusi *)
97 97
    raise (StopPhase1 prog);
98 98

  
99
  (* Optimization of prog: 
100
     - Unfold consts 
99
  (* Optimization of prog:
100
     - Unfold consts
101 101
     - eliminate trivial expressions
102 102
  *)
103 103
  (*
104
    let prog = 
104
    let prog =
105 105
    if !Options.const_unfold || !Options.optimization >= 5 then
106 106
    begin
107 107
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
......
139 139
  Clock_calculus.uneval_prog_generics prog;
140 140

  
141 141

  
142
(* Disabling witness option. Could but reactivated later 
142
(* Disabling witness option. Could but reactivated later
143 143
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
144 144
    begin
145 145
      let orig = Corelang.copy_prog orig in
......
154 154
	!Options.main_node
155 155
	orig prog type_env clock_env
156 156
    end;
157
*)  
157
*)
158 158

  
159 159
  (* Computes and stores generic calls for each node,
160 160
     only useful for ANSI C90 compliant generic node compilation *)
......
201 201
      Access.check_prog prog;
202 202
    end;
203 203

  
204
  
204

  
205 205
  let prog = SortProg.sort_nodes_locals prog in
206
  
206

  
207 207
  prog, dependencies
208 208

  
209 209

  
210 210
    (* from source to machine code, with optimization *)
211
let stage2 prog =    
211
let stage2 prog =
212 212
  (* Computation of node equation scheduling. It also breaks dependency cycles
213 213
     and warns about unused input or memory variables *)
214 214
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
215 215
  let prog, node_schs =
216
    try 
216
    try
217 217
      Scheduling.schedule_prog prog
218 218
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
219 219
				 systemtic way in AlgebraicLoop module *)
......
226 226
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
227 227
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
228 228

  
229
  (* TODO Salsa optimize prog: 
229
  (* TODO Salsa optimize prog:
230 230
     - emits warning for programs with pre inside expressions
231 231
     - make sure each node arguments and memory is bounded by a local annotation
232 232
     - introduce fresh local variables for each real pure subexpression
......
238 238
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
239 239

  
240 240
  (* Optimize machine code *)
241
  Optimize_machine.optimize prog node_schs machine_code   
241
  Optimize_machine.optimize prog node_schs machine_code
242 242

  
243 243

  
244 244
(* printing code *)
245 245
let stage3 prog machine_code dependencies basename =
246 246
  let basename    =  Filename.basename basename in
247 247
  match !Options.output with
248
    "C" -> 
248
    "C" ->
249 249
      begin
250 250
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
251 251
	C_backend.translate_to_c
......
262 262
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
263 263
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
264 264
     end
265
  | "Ada" ->
266
    begin
267
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@,");
268
      Ada_backend.translate_to_ada
269
	basename prog machine_code dependencies
270
    end
265 271
  | "horn" ->
266 272
     begin
267 273
       let destname = !Options.dest_dir ^ "/" ^ basename in
src/options_management.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11
open Options
12
  
12

  
13 13
let print_version () =
14 14
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
15 15
  Format.printf "Standard lib: %s@." Version.include_path;
......
21 21
  let removed_slash_suffix =
22 22
    let len = String.length dir in
23 23
    if dir.[len-1] = '/' then
24
      String.sub dir 0 (len - 1) 
24
      String.sub dir 0 (len - 1)
25 25
    else
26 26
      dir
27 27
  in
28 28
  include_dirs := removed_slash_suffix :: !include_dirs
29 29

  
30
    
30

  
31 31
(** Solving the path of required library:
32 32
    If local: look in the folders described in !Options.include_dirs
33 33
    If non local: look first as a local, then in Version.include_path:
......
41 41
    List.fold_right (fun dir res ->
42 42
      match res with Some _ -> res
43 43
      | None ->
44
	 let path_to_lib = dir ^ "/" ^ full_file_name in 
44
	 let path_to_lib = dir ^ "/" ^ full_file_name in
45 45
	 if Sys.file_exists path_to_lib then
46 46
	   Some dir
47 47
	 else
......
57 57
(* Search for path of core libs (without lusic: arrow and io_frontend *)
58 58
let core_dependency lib_name =
59 59
  search_lib_path (false, lib_name ^ ".h")
60
    
60

  
61 61
let name_dependency (local, dep) =
62 62
  let dir = search_lib_path (false, dep ^ ".lusic") in
63 63
  dir ^ "/" ^ dep
64
  
64

  
65 65
let set_mpfr prec =
66 66
  if prec > 0 then (
67 67
    mpfr := true;
......
79 79
      real_type := "mpfr";
80 80
    )
81 81
  | _ -> real_type := s
82
     
82

  
83 83
let set_backend s =
84 84
  output := s;
85 85
  Backends.setup ()
......
90 90
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
91 91
    "-print-types", Arg.Set print_types, "prints node types";
92 92
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
93
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; 
94
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>"; 
93
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
94
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>";
95 95
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
96 96
    "-version", Arg.Unit print_version, " displays the version";
97 97
  ]
98 98

  
99 99
let lustrec_options =
100 100
  common_options @
101
    [ 
101
    [
102 102
      "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
103 103
      "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
104 104
      "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
......
108 108
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
109 109
      "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
110 110
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
111
      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
111 112
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
112 113
      "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
113 114
      "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
......
119 120
      "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
120 121
      "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
121 122
      "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
122
      
123

  
123 124
      "-c++" , Arg.Set        cpp      , "c++ backend";
124 125
      "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
125 126
      "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
......
140 141
let plugin_opt (name, activate, options) =
141 142
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
142 143
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
143
 
144

  
144 145

  
145 146
let get_witness_dir filename =
146 147
  (* Make sure the directory exists *)

Also available in: Unified diff