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