lustrec / src / main_lustre_testgen.ml @ a0c92fa8
History | View | Annotate | Download (7.2 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 Lustre_types |
19 |
open Compiler_common |
20 |
|
21 |
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m" |
22 |
|
23 |
let extensions = [".lus"] |
24 |
|
25 |
let pp_trace trace_filename mutation_list = |
26 |
let trace_file = open_out trace_filename in |
27 |
let trace_fmt = formatter_of_out_channel trace_file in |
28 |
Format.fprintf trace_fmt "@[<v 2>{@ %a@ }@]" |
29 |
(fprintf_list |
30 |
~sep:",@ " |
31 |
(fun fmt (mutation, mutation_loc, mutant_name) -> |
32 |
Format.fprintf fmt "\"%s\": { @[<v 0>%a,@ %a@ }@]" |
33 |
mutant_name |
34 |
Mutation.print_directive_json mutation |
35 |
Mutation.print_loc_json mutation_loc |
36 |
)) |
37 |
mutation_list; |
38 |
Format.fprintf trace_fmt "@.@?" |
39 |
|
40 |
|
41 |
let testgen_source dirname basename extension = |
42 |
let source_name = dirname ^ "/" ^ basename ^ extension in |
43 |
|
44 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
45 |
|
46 |
(* Parsing source *) |
47 |
let prog = parse source_name extension in |
48 |
let params = Backends.get_normalization_params () in |
49 |
let prog, dependencies = |
50 |
try |
51 |
Compiler_stages.stage1 params prog dirname basename extension |
52 |
with Compiler_stages.StopPhase1 prog -> ( |
53 |
if !Options.print_nodes then ( |
54 |
Format.printf "%a@.@?" Printers.pp_node_list prog; |
55 |
exit 0 |
56 |
) |
57 |
else |
58 |
assert false |
59 |
) |
60 |
in |
61 |
|
62 |
(* Two cases |
63 |
- generation of coverage conditions |
64 |
- generation of mutants: a number of mutated lustre files |
65 |
*) |
66 |
|
67 |
if !Options.gen_mcdc then ( |
68 |
let prog_mcdc = PathConditions.mcdc prog in |
69 |
(* We re-type the fresh equations *) |
70 |
(*let _ = Modules.load ~is_header:false prog_mcdc in*) |
71 |
let _ = type_decls !Global.type_env prog_mcdc in |
72 |
|
73 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
74 |
let source_file = destname ^ ".mcdc" in (* Could be changed *) |
75 |
|
76 |
(* Modified Lustre is produced in fresh .lus file *) |
77 |
let source_lus = source_file ^ ".lus" in |
78 |
let source_out = open_out source_lus in |
79 |
let fmt = formatter_of_out_channel source_out in |
80 |
Printers.pp_prog fmt prog_mcdc; |
81 |
Format.fprintf fmt "@.@?"; |
82 |
|
83 |
(* Prog is |
84 |
(1) cleaned from initial equations TODO |
85 |
(2) produced as EMF |
86 |
*) |
87 |
Options.output := "emf"; |
88 |
let params = Backends.get_normalization_params () in |
89 |
let prog_mcdc = Normalization.normalize_prog params prog_mcdc in |
90 |
let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in |
91 |
let source_emf = source_file ^ ".emf" in |
92 |
let source_out = open_out source_emf in |
93 |
let fmt = formatter_of_out_channel source_out in |
94 |
EMF_backend.translate fmt basename prog_mcdc machine_code; |
95 |
|
96 |
exit 0 |
97 |
) ; |
98 |
|
99 |
|
100 |
(* generate mutants *) |
101 |
let mutants = Mutation.mutate !Options.nb_mutants prog in |
102 |
|
103 |
(* Print generated mutants in target directory. *) |
104 |
let cpt = ref 0 in |
105 |
let mutation_list = |
106 |
List.map (fun (mutation, mutation_loc, mutant) -> |
107 |
(* Debugging code *) |
108 |
(* if List.mem !cpt [238;371;601;799;875;998] then *) |
109 |
(* Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e *) |
110 |
(* ; *) |
111 |
incr cpt; |
112 |
let mutant_basename = (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension in |
113 |
let mutant_filename = |
114 |
match !Options.dest_dir with |
115 |
| "" -> (* Mutants are generated in source directory *) |
116 |
basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension |
117 |
| dir -> (* Mutants are generated in target directory *) |
118 |
dir ^ "/" ^ mutant_basename |
119 |
in |
120 |
let mutant_out = ( |
121 |
try |
122 |
open_out mutant_filename |
123 |
with |
124 |
Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1 |
125 |
) |
126 |
in |
127 |
let mutant_fmt = formatter_of_out_channel mutant_out in |
128 |
report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" |
129 |
mutant_filename |
130 |
Mutation.print_directive mutation |
131 |
); |
132 |
Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant; |
133 |
mutation, mutation_loc, mutant_basename |
134 |
) |
135 |
mutants |
136 |
in |
137 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@."); |
138 |
|
139 |
(* Printing traceability *) |
140 |
let trace_filename = |
141 |
match !Options.dest_dir with |
142 |
| "" -> (* Mutant report is generated in source directory *) |
143 |
basename^ ".mutation.json" |
144 |
| dir -> (* Mutants are generated in target directory *) |
145 |
dir ^ "/" ^ (Filename.basename basename)^ ".mutation.json" |
146 |
in |
147 |
pp_trace trace_filename mutation_list; |
148 |
|
149 |
(* Printing the CMakeLists.txt file *) |
150 |
let cmakelists = |
151 |
(if !Options.dest_dir = "" then "" else !Options.dest_dir ^ "/") ^ "CMakeLists.txt" |
152 |
in |
153 |
let cmake_file = open_out cmakelists in |
154 |
let cmake_fmt = formatter_of_out_channel cmake_file in |
155 |
Format.fprintf cmake_fmt "cmake_minimum_required(VERSION 3.5)@."; |
156 |
Format.fprintf cmake_fmt "include(\"%s/share/helpful_functions.cmake\")@." Version.prefix; |
157 |
Format.fprintf cmake_fmt "include(\"%s/share/FindLustre.cmake\")@." Version.prefix; |
158 |
Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@."; |
159 |
Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ "; |
160 |
Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ "; |
161 |
Format.fprintf cmake_fmt "Lustre_Compile(@[<v 0>@ "; |
162 |
if !Options.main_node <> "" then Format.fprintf cmake_fmt "NODE \"%s_mutant\"@ " !Options.main_node; |
163 |
Format.fprintf cmake_fmt "LIBNAME \"${L}_%s_mutant\"@ " !Options.main_node; |
164 |
Format.fprintf cmake_fmt "LUS_FILES \"${lus_file}\")@]@]@."; |
165 |
Format.fprintf cmake_fmt "ENDFOREACH()@.@?"; |
166 |
|
167 |
|
168 |
(* We stop the process here *) |
169 |
exit 0 |
170 |
|
171 |
let testgen dirname basename extension = |
172 |
match extension with |
173 |
| ".lus" -> testgen_source dirname basename extension |
174 |
| _ -> assert false |
175 |
|
176 |
let anonymous filename = |
177 |
let ok_ext, ext = List.fold_left |
178 |
(fun (ok, ext) ext' -> |
179 |
if not ok && Filename.check_suffix filename ext' then |
180 |
true, ext' |
181 |
else |
182 |
ok, ext) |
183 |
(false, "") extensions in |
184 |
if ok_ext then |
185 |
let dirname = Filename.dirname filename in |
186 |
let basename = Filename.chop_suffix (Filename.basename filename) ext in |
187 |
testgen dirname basename ext |
188 |
else |
189 |
raise (Arg.Bad ("Can only compile *.lus files")) |
190 |
|
191 |
let _ = |
192 |
Global.initialize (); |
193 |
Corelang.add_internal_funs (); |
194 |
try |
195 |
Printexc.record_backtrace true; |
196 |
|
197 |
let options = Options_management.lustret_options |
198 |
|
199 |
in |
200 |
|
201 |
Arg.parse options anonymous usage |
202 |
with |
203 |
| Parse.Error _ |
204 |
| Types.Error (_,_) | Clocks.Error (_,_) |
205 |
| Error.Error _ (*| Task_set.Error _*) |
206 |
| Causality.Error _ -> exit 1 |
207 |
| Sys_error msg -> (eprintf "Failure: %s@." msg) |
208 |
| exc -> (track_exception (); raise exc) |
209 |
|
210 |
(* Local Variables: *) |
211 |
(* compile-command:"make -C .." *) |
212 |
(* End: *) |