Revision 55a8633c
Added by Pierre-Loïc Garoche almost 7 years ago
| src/main_lustre_testgen.ml | ||
|---|---|---|
| 22 | 22 |
|
| 23 | 23 |
let extensions = [".lus"] |
| 24 | 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 prog (* type_env clock_env *) |
|
| 49 |
in |
|
| 50 |
|
|
| 51 |
check_stateless_decls prog; |
|
| 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 |
|
|
| 52 | 40 |
|
| 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 |
Typing.uneval_prog_generics prog; |
|
| 63 |
Clock_calculus.uneval_prog_generics prog; |
|
| 64 |
|
|
| 65 |
if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then |
|
| 66 |
begin |
|
| 67 |
let orig = Corelang.copy_prog orig in |
|
| 68 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,"); |
|
| 69 |
check_stateless_decls orig; |
|
| 70 |
let _ = Typing.type_prog type_env orig in |
|
| 71 |
let _ = Clock_calculus.clock_prog clock_env orig in |
|
| 72 |
Typing.uneval_prog_generics orig; |
|
| 73 |
Clock_calculus.uneval_prog_generics orig; |
|
| 74 |
Inliner.witness |
|
| 75 |
basename |
|
| 76 |
!Options.main_node |
|
| 77 |
orig prog type_env clock_env |
|
| 78 |
end; |
|
| 79 |
|
|
| 80 |
(* Normalization phase *) |
|
| 81 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,"); |
|
| 82 |
(* Special treatment of arrows in lustre backend. We want to keep them *) |
|
| 83 |
if !Options.output = "lustre" then |
|
| 84 |
Normalization.unfold_arrow_active := false; |
|
| 85 |
let prog = Normalization.normalize_prog prog in |
|
| 86 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
|
| 87 |
|
|
| 88 |
prog, dependencies |
|
| 89 |
|
|
| 90 | 41 |
let testgen_source dirname basename extension = |
| 91 | 42 |
let source_name = dirname ^ "/" ^ basename ^ extension in |
| 92 | 43 |
|
| ... | ... | |
| 95 | 46 |
(* Parsing source *) |
| 96 | 47 |
let prog = parse_source source_name in |
| 97 | 48 |
|
| 98 |
let prog, dependencies = stage1 prog dirname basename in |
|
| 49 |
let prog, dependencies = Compiler_stages.stage1 prog dirname basename in
|
|
| 99 | 50 |
|
| 51 |
(* Two cases |
|
| 52 |
- generation of coverage conditions |
|
| 53 |
- generation of mutants: a number of mutated lustre files |
|
| 54 |
*) |
|
| 55 |
|
|
| 100 | 56 |
if !Options.gen_mcdc then ( |
| 101 | 57 |
PathConditions.mcdc prog; |
| 102 | 58 |
exit 0 |
| 103 | 59 |
) ; |
| 60 |
|
|
| 61 |
|
|
| 104 | 62 |
(* generate mutants *) |
| 105 |
let mutants, mutation_printer = Mutation.mutate !Options.nb_mutants prog in
|
|
| 63 |
let mutants = Mutation.mutate !Options.nb_mutants prog in |
|
| 106 | 64 |
|
| 107 | 65 |
(* Print generated mutants in target directory. *) |
| 108 | 66 |
let cpt = ref 0 in |
| 109 |
List.iter (fun (mutation, mutant) -> |
|
| 67 |
let mutation_list = |
|
| 68 |
List.map (fun (mutation, mutation_loc, mutant) -> |
|
| 110 | 69 |
(* Debugging code *) |
| 111 | 70 |
(* if List.mem !cpt [238;371;601;799;875;998] then *) |
| 112 | 71 |
(* Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e *) |
| ... | ... | |
| 115 | 74 |
let mutant_filename = |
| 116 | 75 |
match !Options.dest_dir with |
| 117 | 76 |
| "" -> (* Mutants are generated in source directory *) |
| 118 |
basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension |
|
| 77 |
basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension
|
|
| 119 | 78 |
| dir -> (* Mutants are generated in target directory *) |
| 120 |
dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension |
|
| 79 |
dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension
|
|
| 121 | 80 |
in |
| 122 | 81 |
let mutant_out = ( |
| 123 | 82 |
try |
| ... | ... | |
| 127 | 86 |
) |
| 128 | 87 |
in |
| 129 | 88 |
let mutant_fmt = formatter_of_out_channel mutant_out in |
| 130 |
report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename mutation_printer mutation); |
|
| 131 |
Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant |
|
| 132 |
) |
|
| 133 |
mutants; |
|
| 89 |
report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" |
|
| 90 |
mutant_filename |
|
| 91 |
Mutation.print_directive mutation |
|
| 92 |
); |
|
| 93 |
Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant; |
|
| 94 |
mutation, mutation_loc, mutant_filename |
|
| 95 |
) |
|
| 96 |
mutants |
|
| 97 |
in |
|
| 134 | 98 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@."); |
| 135 |
(* We stop the process here *) |
|
| 99 |
|
|
| 100 |
(* Printing traceability *) |
|
| 101 |
let trace_filename = |
|
| 102 |
match !Options.dest_dir with |
|
| 103 |
| "" -> (* Mutant report is generated in source directory *) |
|
| 104 |
basename^ ".mutation.json" |
|
| 105 |
| dir -> (* Mutants are generated in target directory *) |
|
| 106 |
dir ^ "/" ^ (Filename.basename basename)^ ".mutation.json" |
|
| 107 |
in |
|
| 108 |
pp_trace trace_filename mutation_list; |
|
| 109 |
(* We stop the process here *) |
|
| 136 | 110 |
exit 0 |
| 137 |
|
|
| 111 |
|
|
| 138 | 112 |
let testgen dirname basename extension = |
| 139 | 113 |
match extension with |
| 140 | 114 |
| ".lus" -> testgen_source dirname basename extension |
Also available in: Unified diff
[lustret] Improved mutation with json traceability