Project

General

Profile

Revision 1bff14ac

View differences:

Makefile.in
89 89
	cd test; ctest -M Experimental -T Submit -R COMPIL_LUSTRE
90 90

  
91 91
test: test-config
92
	cd test; ctest -D Experimental -R COMPIL_LUSTRE
92
	cd test; ctest -D Experimental -R COMPIL_LUSTRE\|MAKE\|BIN\|DIFF
93 93

  
94 94
test-full-no-submit: test-config
95 95
	cd test; ctest -M Experimental -T Start -T Update -T Configure -T Build -T Test 
src/backends/C/c_backend_main.ml
175 175

  
176 176
let print_main_header fmt =
177 177
  fprintf fmt (if !Options.cpp then "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.hpp\"@." else "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@.")
178
    (Options.core_dependency "io_frontend")
178
    (Options_management.core_dependency "io_frontend")
179 179

  
180 180
let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) =
181 181
  print_main_header main_fmt;
src/backends/EMF/EMF_backend.ml
174 174
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_val vars)) vl 
175 175

  
176 176
     
177

  
178
     
179
let rec pp_instr m vars fmt i =
177
(* detect whether the instruction i represents a STEP, ie an arrow with true -> false *)
178
let is_step_fun m i =
180 179
  match Corelang.get_instr_desc i with
181
  | MLocalAssign (var,v) 
182
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
183 180
  | MStep ([var], i, vl)  -> (
184 181
    let name = (Machine_code.get_node_def i m).node_id in
185 182
    match name, vl with
186
      "_arrow", [v1; v2] -> (
183
    | "_arrow", [v1; v2] -> (
187 184
	match v1.value_desc, v2.value_desc with
188
	| Cst c1, Cst c2 -> if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then fprintf fmt "STEP" else assert false (* only handle true -> false *)
185
	| Cst c1, Cst c2 ->
186
	   if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
187
	     true
188
	   else
189
	     assert false (* only handle true -> false *)
189 190
	| _ -> assert false
190
      )
191
    | _ -> raise (Unhandled ("call to node " ^ name))
191
    )
192
    | _ -> false
192 193
  )
194
  | _ -> false
195

  
196
     
197
let rec pp_instr m vars fmt i =
198
  match Corelang.get_instr_desc i with
199
  | MLocalAssign (var,v) 
200
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
201
  | MStep _ when is_step_fun m i  -> fprintf fmt "STEP" 
193 202
  | MBranch (g,[(tag1,case1);(tag2,case2)])     ->
194 203
     let then_case, else_case =
195 204
       if tag1 = Corelang.tag_true then
......
201 210
       (pp_val vars) g
202 211
       (pp_instrs m vars) then_case
203 212
       (pp_instrs m vars) else_case
204
  | MStep _ (* only single output for function call *)
213
  | MStep _ (* no function calls handled yet *)
205 214
  | MBranch _ (* EMF backend only accept true/false ite *)
206 215
  | MReset _           
207 216
  | MNoReset _
......
258 267
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
259 268
    Utils.ISet.empty
260 269
    il
270

  
271

  
272
let pp_original_lustre_expression m fmt i =
273
  match Corelang.get_instr_desc i with
274
  | MLocalAssign _ | MStateAssign _ 
275
  | MBranch _
276
    -> ( match i.lustre_eq with None -> () | Some e -> Printers.pp_node_eq fmt e) 
277
  | MStep _ when is_step_fun m i -> () (* we print nothing, this is a STEP *)
278
  | MStep _ -> (match i.lustre_eq with None -> () | Some eq -> Printers.pp_node_eq fmt eq)
279
  | _ -> ()
261 280
    
262 281
let pp_instr_main m fmt i =
263 282
  (* first, we extract the expression and associated variables *)
264 283
  let var = get_instr_var i in
265 284
  let vars = Utils.ISet.elements (get_instr_vars i) in	
266
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%t]@]}"
285
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}"
267 286
    var.var_id
268 287
    (pp_instr m vars) i
269 288
    (fprintf_list ~sep:", " pp_var_string) vars
270
    (fun fmt -> ()
271
      (*xxxx
272
      if is expr than print associated lustre eq else empty string
273
	xxx todo
274
      *)
275
    ) 
289
    (pp_original_lustre_expression m) i
290

  
291
    
276 292
     
277 293
let pp_machine fmt m =
278 294
  try
src/backends/Horn/horn_backend.ml
85 85
  List.iter
86 86
    (fun dep ->
87 87
      let (local, s) = Corelang.dependency_of_top dep in
88
      let basename = (Options.name_dependency (local, s)) ^ ".smt2" in
88
      let basename = (Options_management.name_dependency (local, s)) ^ ".smt2" in
89 89
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
90 90
      let horn = load_file basename in
91 91
      fprintf fmt "@.%s@." horn;
src/backends/backends.ml
3 3

  
4 4
let setup s =
5 5
  match s with
6
  | "emf" -> join_guards := false
6
  | "emf" ->
7
     join_guards := false; (* guards should not be joined, in order to have only
8
			      if c then x = e1 else x = e2 to ease
9
			      reconstruction of flows. *)
10
    Options.optimization := 0; (* Optimization=0 prevents expression
11
				  elimination. This simplifies largely the
12
				  association of lustre expression to
13
				  instructions *)
7 14
  | _ -> ()
15

  
16
(* Local Variables: *)
17
(* compile-command: "make -k -C .." *)
18
(* End: *)
src/compiler_common.ml
239 239
  List.fold_left
240 240
    (fun (compilation_dep, type_env, clock_env) dep ->
241 241
      let (local, s) = Corelang.dependency_of_top dep in
242
      let basename = Options.name_dependency (local, s) in
242
      let basename = Options_management.name_dependency (local, s) in
243 243
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "  Library %s@ " basename);
244 244
      let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in
245 245
      (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "");*)
src/corelang.ml
181 181
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
182 182

  
183 183

  
184
let mkinstr (* TODO ?(lustre_expr=None) ?(lustre_eq=None) *) i =
184
let mkinstr ?(lustre_expr=None) ?(lustre_eq=None) i =
185 185
  {
186 186
    instr_desc = i;
187

  
187
    (* lustre_expr = lustre_expr; *)
188
    lustre_eq = lustre_eq;
188 189
  }
189 190

  
190 191
let get_instr_desc i = i.instr_desc
src/corelang.mli
32 32
val mktop: top_decl_desc -> top_decl
33 33

  
34 34
(* constructor for machine types *)
35
val mkinstr: (* TODO ?lustre_expr:expr -> ?lustre_eq: eq option -> *) instr_t_desc -> instr_t
35
val mkinstr: ?lustre_expr:expr option -> ?lustre_eq: eq option -> instr_t_desc -> instr_t
36 36
val get_instr_desc: instr_t -> instr_t_desc
37 37
val update_instr_desc: instr_t -> instr_t_desc -> instr_t
38 38
  
src/inliner.ml
418 418
  let _ = Clock_calculus.clock_prog clock_env new_prog in
419 419
*)
420 420
   
421
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
421
  let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
422 422
  let witness_out = open_out witness_file in
423 423
  let witness_fmt = Format.formatter_of_out_channel witness_out in
424 424
  begin
src/lustreSpec.ml
237 237

  
238 238
type instr_t =
239 239
  {
240
    instr_desc: instr_t_desc;
240
    instr_desc: instr_t_desc; (* main data: the content *)
241
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
242
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
241 243
  }
242 244
and instr_t_desc =
243 245
  | MLocalAssign of var_decl * value_t
src/machine_code.ml
43 43
    | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
44 44

  
45 45
let rec pp_instr fmt i =
46
  match i.instr_desc with
46
  let _ =
47
    match i.instr_desc with
47 48
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
48 49
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
49 50
    | MReset i           -> Format.fprintf fmt "reset %s" i
50 51
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
51 52
    | MStep (il, i, vl)  ->
52
      Format.fprintf fmt "%a = %s (%a)"
53
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
54
	i
55
	(Utils.fprintf_list ~sep:", " pp_val) vl
53
       Format.fprintf fmt "%a = %s (%a)"
54
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
55
	 i
56
	 (Utils.fprintf_list ~sep:", " pp_val) vl
56 57
    | MBranch (g,hl)     ->
57
      Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
58
	pp_val g
59
	(Utils.fprintf_list ~sep:"@," pp_branch) hl
58
       Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
59
	 pp_val g
60
	 (Utils.fprintf_list ~sep:"@," pp_branch) hl
60 61
    | MComment s -> Format.pp_print_string fmt s
61

  
62
       
63
  in
64
  (* Annotation *)
65
  (* let _ = *)
66
  (*   match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
67
  (* in *)
68
  let _ = 
69
    match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
70
  in
71
  ()
72
    
62 73
and pp_branch fmt (t, h) =
63 74
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
64 75

  
......
149 160
let is_memory m id =
150 161
  List.exists (fun o -> o.var_id = id.var_id) m.mmemory
151 162

  
152
let conditional (* TODO ?(lustre_expr:expr option=None) *) c t e =
153
  mkinstr (* TODO ?lustre_expr *) (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
163
let conditional ?lustre_eq c t e =
164
  mkinstr ?lustre_eq:lustre_eq  (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
154 165

  
155 166
let dummy_var_decl name typ =
156 167
  {
......
189 200
let arrow_top_decl =
190 201
  {
191 202
    top_decl_desc = Node arrow_desc;
192
    top_decl_owner = (Options.core_dependency "arrow");
203
    top_decl_owner = (Options_management.core_dependency "arrow");
193 204
    top_decl_itf = false;
194 205
    top_decl_loc = Location.dummy_loc
195 206
  }
......
409 420
  | _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
410 421

  
411 422
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
423
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
412 424
  match expr.expr_desc with
413 425
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
414
			    conditional (* TODO ?lustre_expr:(Some expr) *) g
426
			    conditional ?lustre_eq:(Some (Some eq)) g
415 427
                              [translate_act node args (y, t)]
416 428
                              [translate_act node args (y, e)]
417
  | Expr_merge (x, hl)   -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MBranch (translate_ident node args x,
429
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some (Some eq)) (MBranch (translate_ident node args x,
418 430
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl))
419
  | _                    -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MLocalAssign (y, translate_expr node args expr))
431
  | _                    -> mkinstr ?lustre_eq:(Some (Some eq))  (MLocalAssign (y, translate_expr node args expr))
420 432

  
421 433
let reset_instance node args i r c =
422 434
  match r with
......
436 448
      mkinstr (MReset o) :: si,
437 449
      Utils.IMap.add o (arrow_top_decl, []) j,
438 450
      d,
439
      (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:eq *) (MStep ([var_x], o, [c1;c2])))) :: s)
451
      (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some (Some eq)) (MStep ([var_x], o, [c1;c2])))) :: s)
440 452
  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->
441 453
     let var_x = get_node_var x node in
442 454
     (ISet.add var_x m,
443 455
      si,
444 456
      j,
445 457
      d,
446
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1))) :: s)
458
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some (Some eq)) (MStateAssign (var_x, translate_expr node args e1))) :: s)
447 459
  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
448 460
     let var_x = get_node_var x node in
449 461
     (ISet.add var_x m,
450
      mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1)) :: si,
462
      mkinstr ?lustre_eq:(Some (Some eq)) (MStateAssign (var_x, translate_expr node args e1)) :: si,
451 463
      j,
452 464
      d,
453
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e2))) :: s)
465
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some (Some eq)) (MStateAssign (var_x, translate_expr node args e2))) :: s)
454 466

  
455 467
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
456 468
     let var_p = List.map (fun v -> get_node_var v node) p in
......
473 485
      (if Stateless.check_node node_f
474 486
       then []
475 487
       else reset_instance node args o r call_ck) @
476
	(control_on_clock node args call_ck (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStep (var_p, o, vl)))) :: s)
488
	(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some (Some eq)) (MStep (var_p, o, vl)))) :: s)
477 489
  (*
478 490
    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
479 491
    are preserved. While they are replaced as if g then x = t else x = e in  C or Java
src/main_lustre_compiler.ml
486 486
  try
487 487
    Printexc.record_backtrace true;
488 488

  
489
    let options = Options.lustrec_options @ (Plugins.options ()) in
489
    let options = Options_management.lustrec_options @ (Plugins.options ()) in
490 490
    
491 491
    Arg.parse options anonymous usage
492 492
  with
src/main_lustre_testgen.ml
161 161
  try
162 162
    Printexc.record_backtrace true;
163 163

  
164
    let options = Options.lustret_options
164
    let options = Options_management.lustret_options
165 165

  
166 166
    in
167 167
    
src/modules.ml
114 114
  with Not_found -> Hashtbl.add consts_table name value
115 115

  
116 116
let import_dependency_aux loc (local, dep) =
117
  let basename = Options.name_dependency (local, dep) in
117
  let basename = Options_management.name_dependency (local, dep) in
118 118
  let extension = ".lusic" in 
119 119
  try
120 120
    let lusic = Lusic.read_lusic basename extension in
......
158 158
    | Const c -> (add_const true c.const_id decl; imported)
159 159
    | TypeDef tdef -> (add_type true tdef.tydef_id decl; imported)
160 160
    | Open (local, dep) ->
161
       let basename = Options.name_dependency (local, dep) in
161
       let basename = Options_management.name_dependency (local, dep) in
162 162
       if ISet.mem basename imported then imported else
163 163
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
164 164
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
......
183 183
    | Const c -> (add_const false c.const_id decl; imported)
184 184
    | TypeDef tdef -> (add_type false tdef.tydef_id decl; imported)
185 185
    | Open (local, dep) ->
186
       let basename = Options.name_dependency (local, dep) in
186
       let basename = Options_management.name_dependency (local, dep) in
187 187
       if ISet.mem basename imported then imported else
188 188
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
189 189
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
src/options.ml
12 12
let version = Version.number
13 13
let codename = Version.codename
14 14
let include_dirs = ref ["."]
15
(* let include_path = *)
16
(* if (!include_dir <> ".") then Version.prefix ^ !include_dir *)
17
(* else Version.include_path *)
18

  
19

  
20

  
21

  
22
let print_version () =
23
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
24
  Format.printf "Standard lib: %s@." Version.include_path;
25
  Format.printf "User provided include directory: @[<h>%a@]@."
26
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) !include_dirs
27 15

  
28 16
let main_node = ref ""
29 17
let static_mem = ref true
......
64 52
let gen_mcdc = ref false
65 53
let no_mutation_suffix = ref false
66 54

  
67
let add_include_dir dir =
68
  let removed_slash_suffix =
69
    let len = String.length dir in
70
    if dir.[len-1] = '/' then
71
      String.sub dir 0 (len - 1) 
72
    else
73
      dir
74
  in
75
  include_dirs := removed_slash_suffix :: !include_dirs
76

  
77
    
78
(** Solving the path of required library:
79
    If local: look in the folders described in !Options.include_dirs
80
    If non local: look first as a local, then in Version.include_path:
81
    ie. in Version.include_path::!Options.include_dirs
82
    Note that in options.ml, include folder are added as heads. One need to
83
    perform a fold_right to respect the order
84
*)
85
let search_lib_path (local, full_file_name) =
86
  let paths = (if local then !include_dirs else Version.include_path::!include_dirs) in
87
  let name =
88
    List.fold_right (fun dir res ->
89
      match res with Some _ -> res
90
      | None ->
91
	 let path_to_lib = dir ^ "/" ^ full_file_name in 
92
	 if Sys.file_exists path_to_lib then
93
	   Some dir
94
	 else
95
	   None
96
    )
97
      paths
98
      None
99
  in
100
  match name with
101
  | None -> Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;raise Not_found
102
  | Some s -> s
103

  
104
(* Search for path of core libs (without lusic: arrow and io_frontend *)
105
let core_dependency lib_name =
106
  search_lib_path (false, lib_name ^ ".h")
107
    
108
let name_dependency (local, dep) =
109
  let dir = search_lib_path (false, dep ^ ".lusic") in
110
  dir ^ "/" ^ dep
111
  
112
let set_mpfr prec =
113
  if prec > 0 then (
114
    mpfr := true;
115
    mpfr_prec := prec;
116
    (* salsa_enabled := false; (* We deactivate salsa *) TODO *)
117
  )
118
  else
119
    failwith "mpfr requires a positive integer"
120

  
121
let set_backend s =
122
  output := s;
123
  Backends.setup s
124

  
125
let common_options =
126
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
127
    "-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m";
128
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
129
    "-print-types", Arg.Set print_types, "prints node types";
130
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
131
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
132
    "-version", Arg.Unit print_version, " displays the version";
133
  ]
134

  
135
let lustrec_options =
136
   common_options @
137
  [ 
138
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
139
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
140
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
141
    "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
142
    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
143
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
144
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
145
    "-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";
146
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
147
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
148
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
149
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
150
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
151
    "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
152
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
153
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
154
   "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
155
   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
156
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
157
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
158
    
159
    "-c++" , Arg.Set        cpp      , "c++ backend";
160
    "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
161
    "-real", Arg.Set_string real_type, "specifies the real type (default=\"double\" without mpfr option)";
162
    "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
163

  
164
    "-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";
165
]
166

  
167
let lustret_options =
168
  common_options @
169
  [ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>";
170
    "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
171
    "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
172
  ]
173

  
174
let plugin_opt (name, activate, options) =
175
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
176
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
177
 
178 55

  
179
let get_witness_dir filename =
180
  (* Make sure the directory exists *)
181
  let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
182
  let _ = try
183
	    if not (Sys.is_directory dir) then (
184
	      Format.eprintf "File of name %s exists. It should be a directory.@." dir;
185
	      exit 1
186
	    )
187
    with Sys_error _ -> Unix.mkdir dir 0o750
188
  in
189
  dir
190 56

  
191 57
(* Local Variables: *)
192 58
(* compile-command:"make -C .." *)
src/options_management.ml
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
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
15
  Format.printf "Standard lib: %s@." Version.include_path;
16
  Format.printf "User provided include directory: @[<h>%a@]@."
17
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) !include_dirs
18

  
19

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

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

  
57
(* Search for path of core libs (without lusic: arrow and io_frontend *)
58
let core_dependency lib_name =
59
  search_lib_path (false, lib_name ^ ".h")
60
    
61
let name_dependency (local, dep) =
62
  let dir = search_lib_path (false, dep ^ ".lusic") in
63
  dir ^ "/" ^ dep
64
  
65
let set_mpfr prec =
66
  if prec > 0 then (
67
    mpfr := true;
68
    mpfr_prec := prec;
69
    (* salsa_enabled := false; (* We deactivate salsa *) TODO *)
70
  )
71
  else
72
    failwith "mpfr requires a positive integer"
73

  
74
let set_backend s =
75
  output := s;
76
  Backends.setup s
77

  
78
let common_options =
79
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
80
    "-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m";
81
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
82
    "-print-types", Arg.Set print_types, "prints node types";
83
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
84
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
85
    "-version", Arg.Unit print_version, " displays the version";
86
  ]
87

  
88
let lustrec_options =
89
   common_options @
90
  [ 
91
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
92
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
93
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
94
    "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
95
    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
96
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
97
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
98
    "-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";
99
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
100
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
101
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
102
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
103
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
104
    "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
105
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
106
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
107
   "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
108
   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
109
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
110
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
111
    
112
    "-c++" , Arg.Set        cpp      , "c++ backend";
113
    "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
114
    "-real", Arg.Set_string real_type, "specifies the real type (default=\"double\" without mpfr option)";
115
    "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
116

  
117
    "-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";
118
]
119

  
120
let lustret_options =
121
  common_options @
122
  [ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>";
123
    "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
124
    "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
125
  ]
126

  
127
let plugin_opt (name, activate, options) =
128
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
129
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
130
 
131

  
132
let get_witness_dir filename =
133
  (* Make sure the directory exists *)
134
  let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
135
  let _ = try
136
	    if not (Sys.is_directory dir) then (
137
	      Format.eprintf "File of name %s exists. It should be a directory.@." dir;
138
	      exit 1
139
	    )
140
    with Sys_error _ -> Unix.mkdir dir 0o750
141
  in
142
  dir
src/plugins.ml
5 5

  
6 6
let options () = 
7 7
  List.flatten (
8
    List.map Options.plugin_opt (
8
    List.map Options_management.plugin_opt (
9 9
      List.map (fun m ->
10 10
	let module M = (val m : PluginType.PluginType) in
11 11
	(M.name, M.activate, M.options)

Also available in: Unified diff