Revision ca7ff3f7
Added by Lélio Brun 8 months 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