Project

General

Profile

Download (9.55 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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
open Options
12

    
13
let print_version () =
14
  let open Utils.Format in
15
  printf
16
    "@[<v>Lustrec compiler, version %s (%s)@,\
17
     Standard lib: %s@,\
18
     User provided include directory: @[<h>%a@]@]@." version codename
19
    Version.include_path
20
    (pp_print_list ~pp_sep:pp_print_space pp_print_string)
21
    !include_dirs
22

    
23
let add_include_dir dir =
24
  let removed_slash_suffix =
25
    let len = String.length dir in
26
    if dir.[len - 1] = '/' then String.sub dir 0 (len - 1) else dir
27
  in
28
  include_dirs := removed_slash_suffix :: !include_dirs
29

    
30
(** Solving the path of required library: If local: look in the folders
31
    described in !Options.include_dirs If non local: look first as a local, then
32
    in Version.include_path: ie. in Version.include_path::!Options.include_dirs
33
    Note that in options.ml, include folder are added as heads. One need to
34
    perform a fold_right to respect the order *)
35
let search_lib_path (local, full_file_name) =
36
  let paths =
37
    if local then !include_dirs else Version.include_path :: !include_dirs
38
  in
39
  let name =
40
    List.fold_right
41
      (fun dir res ->
42
        match res with
43
        | Some _ ->
44
          res
45
        | None ->
46
          let path_to_lib = dir ^ "/" ^ full_file_name in
47
          if Sys.file_exists path_to_lib then Some dir else None)
48
      paths None
49
  in
50
  match name with
51
  | None ->
52
    Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name
53
      (Utils.fprintf_list ~sep:", " Format.pp_print_string)
54
      paths;
55
    raise Not_found
56
  | Some s ->
57
    s
58

    
59
(* Search for path of core libs (without lusic: arrow and io_frontend *)
60
let core_dependency lib_name = search_lib_path (false, lib_name ^ ".h")
61

    
62
let name_dependency (_, dep) ext =
63
  let dir = search_lib_path (false, dep ^ ext) in
64
  dir ^ "/" ^ dep
65

    
66
let set_mpfr prec =
67
  if prec > 0 then (
68
    mpfr := true;
69
    mpfr_prec := prec;
70
    real_type := "mpfr"
71
    (* salsa_enabled := false; (* We deactivate salsa *) TODO *))
72
  else failwith "mpfr requires a positive integer"
73

    
74
let set_real_type s =
75
  match s with
76
  | "mpfr" ->
77
    mpfr := true;
78
    real_type := "mpfr"
79
  | _ ->
80
    real_type := s
81

    
82
let setup () = Backends.setup ()
83

    
84
let set_backend s = output := s
85

    
86
let common_options =
87
  [
88
    ( "-d",
89
      Arg.Set_string dest_dir,
90
      "uses the specified \x1b[4mdirectory\x1b[0m as root for \
91
       generated/imported object and C files <default: .>" );
92
    "-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m";
93
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
94
    "-print-types", Arg.Set print_types, "prints node types";
95
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
96
    "-print-nodes", Arg.Set print_nodes, "prints node list";
97
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
98
    ( "-algebraic-loop-max",
99
      Arg.Set_int al_nb_max,
100
      "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>" );
101
    "-kind2", Arg.Set kind2_print, "active kind2 output";
102
    ( "-verbose",
103
      Arg.Set_int verbose_level,
104
      "changes verbose \x1b[4mlevel\x1b[0m <default: 1>" );
105
    "-version", Arg.Unit print_version, " displays the version";
106
  ]
107

    
108
let lustrec_options =
109
  common_options
110
  @ [
111
      ( "-init",
112
        Arg.Set delay_calculus,
113
        "performs an initialisation analysis for Lustre nodes <default: no \
114
         analysis>" );
115
      ( "-dynamic",
116
        Arg.Clear static_mem,
117
        "specifies a dynamic allocation scheme for main Lustre node <default: \
118
         static>" );
119
      ( "-check-access",
120
        Arg.Set check,
121
        "checks at runtime that array accesses always lie within bounds \
122
         <default: no check>" );
123
      ( "-mpfr",
124
        Arg.Int set_mpfr,
125
        "replaces FP numbers by the MPFR library multiple precision numbers \
126
         with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP \
127
         numbers>" );
128
      ( "-lusi",
129
        Arg.Set lusi,
130
        "only generates a .lusi interface source file from a Lustre source \
131
         <default: no generation>" );
132
      ( "-no-spec",
133
        Arg.Unit (fun () -> spec := "no"),
134
        "do not generate any specification" );
135
      ( "-acsl-spec",
136
        Arg.Unit (fun () -> spec := "acsl"),
137
        "generates an ACSL encoding of the specification. Only meaningful for \
138
         the C backend <default>" );
139
      ( "-c-spec",
140
        Arg.Unit (fun () -> spec := "c"),
141
        "generates a C encoding of the specification instead of ACSL contracts \
142
         and annotations. Only meaningful for the C backend" );
143
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output
144
         instead of C"; *)
145
      ( "-ada",
146
        Arg.Unit (fun () -> set_backend "Ada"),
147
        "generates Ada encoding output instead of C" );
148
      ( "-horn",
149
        Arg.Unit (fun () -> set_backend "horn"),
150
        "generates Horn clauses encoding output instead of C" );
151
      ( "-horn-traces",
152
        Arg.Unit
153
          (fun () ->
154
            set_backend "horn";
155
            traces := true),
156
        "produce traceability file for Horn backend. Enable the horn backend." );
157
      ( "-horn-cex",
158
        Arg.Unit
159
          (fun () ->
160
            set_backend "horn";
161
            horn_cex := true),
162
        "generate cex enumeration. Enable the horn backend (work in progress)" );
163
      ( "-horn-query",
164
        Arg.Unit
165
          (fun () ->
166
            set_backend "horn";
167
            horn_query := true),
168
        "generate queries in generated Horn file. Enable the horn backend \
169
         (work in progress)" );
170
      ( "-horn-sfunction",
171
        Arg.Set_string sfunction,
172
        "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m" );
173
      "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
174
      ( "-lustre",
175
        Arg.Unit (fun () -> output := "lustre"),
176
        "generates Lustre output, performing all active optimizations" );
177
      ( "-emf",
178
        Arg.Unit (fun () -> set_backend "emf"),
179
        "generates EMF output, to be used by CocoSim" );
180
      ( "-inline",
181
        Arg.Unit
182
          (fun () ->
183
            global_inline := true;
184
            const_unfold := true),
185
        "inlines all node calls (require a main node). Implies constant \
186
         unfolding" );
187
      ( "-witnesses",
188
        Arg.Set witnesses,
189
        "enables production of witnesses during compilation" );
190
      ( "-O",
191
        Arg.Set_int optimization,
192
        "changes optimization \x1b[4mlevel\x1b[0m <default: 2>" );
193
      "-c++", Arg.Set cpp, "c++ backend";
194
      ( "-int",
195
        Arg.Set_string int_type,
196
        "specifies the integer type (default=\"int\")" );
197
      ( "-real",
198
        Arg.String set_real_type,
199
        "specifies the real type (default=\"double\" without mpfr option)" );
200
      ( "-real-print-prec",
201
        Arg.Set_int print_prec_double,
202
        "specifies the number of digits to be printed for real values \
203
         (default=15)" );
204
      ( "-int_div_euclidean",
205
        Arg.Set integer_div_euclidean,
206
        "interprets integer division as Euclidean (default : C division \
207
         semantics)" );
208
      ( "-int_div_C",
209
        Arg.Clear integer_div_euclidean,
210
        "interprets integer division as C division (default)" );
211
      ( "-mauve",
212
        Arg.String
213
          (fun node ->
214
            mauve := node;
215
            cpp := true;
216
            static_mem := false),
217
        "generates the mauve code" );
218
    ]
219

    
220
let lustret_options =
221
  common_options
222
  @ [
223
      ( "-nb-mutants",
224
        Arg.Set_int nb_mutants,
225
        "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>" );
226
      "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
227
      ( "-no-mutation-suffix",
228
        Arg.Set no_mutation_suffix,
229
        "does not rename node with the _mutant suffix" );
230
    ]
231

    
232
let lustrev_options =
233
  common_options
234
  @ [
235
      ( "-inline",
236
        Arg.Unit
237
          (fun () ->
238
            global_inline := true;
239
            const_unfold := true),
240
        "inlines all node calls (require a main node). Implies constant \
241
         unfolding" );
242
      ( "-O",
243
        Arg.Set_int optimization,
244
        "changes optimization \x1b[4mlevel\x1b[0m <default: 2>" );
245
    ]
246

    
247
let plugin_opt (name, activate, usage, options) =
248
  let usage () =
249
    Format.printf "@[<v 2>Plugin %s:@ %t@]@." name usage;
250
    exit 0
251
  in
252
  ("-" ^ name, Arg.Unit activate, "activate plugin " ^ name)
253
  ::
254
  ("-" ^ name ^ "-help", Arg.Unit usage, "plugin " ^ name ^ " help")
255
  :: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
256

    
257
let verifier_opt (name, activate, options) =
258
  ("-" ^ name, Arg.Unit activate, "run verifier " ^ name)
259
  :: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
260

    
261
let get_witness_dir filename =
262
  (* Make sure the directory exists *)
263
  let dir = !dest_dir ^ "/" ^ Filename.basename filename ^ "_witnesses" in
264
  let _ =
265
    try
266
      if not (Sys.is_directory dir) then (
267
        Format.eprintf "File of name %s exists. It should be a directory.@." dir;
268
        exit 1)
269
    with Sys_error _ -> Unix.mkdir dir 0o750
270
  in
271
  dir
(48-48/66)