Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / main_lustre_testgen.ml @ 40d33d55

History | View | Annotate | Download (5.96 KB)

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

    
12
(* This module is used for the lustre test generator *)
13

    
14
open Format
15
open Log
16

    
17
open Utils
18
open LustreSpec
19
open Compiler_common
20

    
21
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
22

    
23
let extensions = [".lus"]
24

    
25
(* From prog to prog *)
26
let stage1 prog dirname basename =
27
  (* Removing automata *) 
28
  let prog = expand_automata prog in
29

    
30
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
31

    
32
  (* Importing source *)
33
  let _ = Modules.load_program ISet.empty prog in
34

    
35
  (* Extracting dependencies *)
36
  let dependencies, type_env, clock_env = import_dependencies prog in
37

    
38
  (* Sorting nodes *)
39
  let prog = SortProg.sort prog in
40

    
41
  (* Perform inlining before any analysis *)
42
  let orig, prog =
43
    if !Options.global_inline && !Options.main_node <> "" then
44
      (if !Options.witnesses then prog else []),
45
      Inliner.global_inline basename prog type_env clock_env
46
    else (* if !Option.has_local_inline *)
47
      [],
48
      Inliner.local_inline basename prog type_env clock_env
49
  in
50

    
51
  check_stateless_decls prog;
52
  
53
  (* Typing *)
54
  let computed_types_env = type_decls type_env prog in
55

    
56
  (* Clock calculus *)
57
  let computed_clocks_env = clock_decls clock_env prog in
58

    
59
  (* Creating destination directory if needed *)
60
  create_dest_dir ();
61

    
62
  (* Compatibility with Lusi *)
63
  (* Checking the existence of a lusi (Lustre Interface file) *)
64
  let extension = ".lusi" in
65
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
66

    
67
  Typing.uneval_prog_generics prog;
68
  Clock_calculus.uneval_prog_generics prog;
69

    
70
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
71
    begin
72
      let orig = Corelang.copy_prog orig in
73
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
74
      check_stateless_decls orig;
75
      let _ = Typing.type_prog type_env orig in
76
      let _ = Clock_calculus.clock_prog clock_env orig in
77
      Typing.uneval_prog_generics orig;
78
      Clock_calculus.uneval_prog_generics orig;
79
      Inliner.witness
80
	basename
81
	!Options.main_node
82
	orig prog type_env clock_env
83
    end;
84

    
85
  (* Normalization phase *)
86
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
87
  (* Special treatment of arrows in lustre backend. We want to keep them *)
88
  if !Options.output = "lustre" then
89
    Normalization.unfold_arrow_active := false;
90
  let prog = Normalization.normalize_prog prog in
91
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
92

    
93
  prog, dependencies
94

    
95
let testgen_source dirname basename extension =
96
  let source_name = dirname ^ "/" ^ basename ^ extension in
97

    
98
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
99

    
100
  (* Parsing source *)
101
  let prog = parse_source source_name in
102

    
103
  let prog, dependencies = stage1 prog dirname basename in
104

    
105
  if !Options.gen_mcdc then (
106
    PathConditions.mcdc prog;
107
    exit 0
108
  ) ;
109
  (* generate mutants *)
110
  let mutants, mutation_printer = Mutation.mutate !Options.nb_mutants prog in
111
  
112
  (* Print generated mutants in target directory. *)
113
  let cpt = ref 0 in
114
  List.iter (fun (mutation, mutant) ->
115
    (* Debugging code *)
116
    (* if List.mem !cpt [238;371;601;799;875;998] then *)
117
    (*   Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e  *)
118
    (* ; *)
119
    incr cpt;
120
    let mutant_filename = 
121
      match !Options.dest_dir with
122
      | "" -> (* Mutants are generated in source directory *)
123
	basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
124
      | dir ->  (* Mutants are generated in target directory *)
125
	dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
126
    in
127
    let mutant_out = (
128
      try 
129
	open_out mutant_filename 
130
      with
131
	Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
132
    )
133
    in
134
    let mutant_fmt = formatter_of_out_channel mutant_out in
135
    report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename mutation_printer mutation);
136
    Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant    
137
  )
138
    mutants;
139
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
140
    (* We stop the process here *)
141
  exit 0
142

    
143
let testgen dirname basename extension =
144
  match extension with
145
  | ".lus"   -> testgen_source dirname basename extension
146
  | _        -> assert false
147

    
148
let anonymous filename =
149
  let ok_ext, ext = List.fold_left
150
    (fun (ok, ext) ext' ->
151
      if not ok && Filename.check_suffix filename ext' then
152
	true, ext'
153
      else
154
	ok, ext)
155
    (false, "") extensions in
156
  if ok_ext then
157
    let dirname = Filename.dirname filename in
158
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
159
    testgen dirname basename ext
160
  else
161
    raise (Arg.Bad ("Can only compile *.lus files"))
162

    
163
let _ =
164
  Global.initialize ();
165
  Corelang.add_internal_funs ();
166
  try
167
    Printexc.record_backtrace true;
168

    
169
    let options = Options.lustret_options
170

    
171
    in
172
    
173
    Arg.parse options anonymous usage
174
  with
175
  | Parse.Error _
176
  | Types.Error (_,_) | Clocks.Error (_,_)
177
  | Corelang.Error _ (*| Task_set.Error _*)
178
  | Causality.Error _ -> exit 1
179
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
180
  | exc -> (Utils.track_exception (); raise exc)
181

    
182
(* Local Variables: *)
183
(* compile-command:"make -C .." *)
184
(* End: *)