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 |
| src/mutation.ml | ||
|---|---|---|
| 344 | 344 |
|
| 345 | 345 |
type mutant_t = Boolexpr of int | Pre of int | Op of string * int * string | IncrIntCst of int | DecrIntCst of int | SwitchIntCst of int * int |
| 346 | 346 |
|
| 347 |
(* Denotes the parent node, the equation lhs and the location of the mutation *) |
|
| 348 |
type mutation_loc = ident * ident list * Location.t |
|
| 347 | 349 |
let target : mutant_t option ref = ref None |
| 348 | 350 |
|
| 351 |
let mutation_info : mutation_loc option ref = ref None |
|
| 352 |
let current_node: ident option ref = ref None |
|
| 353 |
let current_eq_lhs : ident list option ref = ref None |
|
| 354 |
let current_loc : Location.t option ref = ref None |
|
| 355 |
|
|
| 356 |
let set_mutation_loc () = |
|
| 357 |
target := None; |
|
| 358 |
match !current_node, !current_eq_lhs, !current_loc with |
|
| 359 |
| Some n, Some elhs, Some l -> mutation_info := Some (n, elhs, l) |
|
| 360 |
| _ -> assert false (* Those global vars should be defined during the |
|
| 361 |
visitor pattern execution *) |
|
| 362 |
|
|
| 349 | 363 |
let print_directive fmt d = |
| 350 | 364 |
match d with |
| 351 | 365 |
| Pre n -> Format.fprintf fmt "pre %i" n |
| ... | ... | |
| 355 | 369 |
| DecrIntCst n -> Format.fprintf fmt "decr int cst %i" n |
| 356 | 370 |
| SwitchIntCst (n, m) -> Format.fprintf fmt "switch int cst %i -> %i" n m |
| 357 | 371 |
|
| 372 |
let print_directive_json fmt d = |
|
| 373 |
match d with |
|
| 374 |
| Pre _ -> Format.fprintf fmt "\"mutation\": \"pre\"" |
|
| 375 |
| Boolexpr _ -> Format.fprintf fmt "\"mutation\": \"not\"" |
|
| 376 |
| Op (o, _, d) -> Format.fprintf fmt "\"mutation\": \"op_conv\", \"from\": \"%s\", \"to\": \"%s\"" o d |
|
| 377 |
| IncrIntCst n -> Format.fprintf fmt "\"mutation\": \"cst_incr\"" |
|
| 378 |
| DecrIntCst n -> Format.fprintf fmt "\"mutation\": \"cst_decr\"" |
|
| 379 |
| SwitchIntCst (n, m) -> Format.fprintf fmt "\"mutation\": \"cst_switch\", \"to_cst\": \"%i\"" m |
|
| 380 |
|
|
| 381 |
let print_loc_json fmt (n,eqlhs, l) = |
|
| 382 |
Format.fprintf fmt "\"node_id\": \"%s\", \"eq_lhs\": [%a], \"loc_line\": \"%i\"" |
|
| 383 |
n |
|
| 384 |
(Utils.fprintf_list ~sep:", " (fun fmt s -> Format.fprintf fmt "\"%s\"" s)) eqlhs |
|
| 385 |
(Location.loc_line l) |
|
| 386 |
|
|
| 358 | 387 |
let fold_mutate_int i = |
| 359 | 388 |
if Random.int 100 > threshold_inc_int then |
| 360 | 389 |
i+1 |
| ... | ... | |
| 390 | 419 |
(* | _ -> op *) |
| 391 | 420 |
match !target with |
| 392 | 421 |
| Some (Op(op_orig, 0, op_new)) when op_orig = op -> ( |
| 393 |
target := None;
|
|
| 422 |
set_mutation_loc ();
|
|
| 394 | 423 |
op_new |
| 395 | 424 |
) |
| 396 | 425 |
| Some (Op(op_orig, n, op_new)) when op_orig = op -> ( |
| ... | ... | |
| 413 | 442 |
let fold_mutate_boolexpr expr = |
| 414 | 443 |
match !target with |
| 415 | 444 |
| Some (Boolexpr 0) -> ( |
| 416 |
target := None; |
|
| 445 |
set_mutation_loc (); |
|
| 446 |
|
|
| 417 | 447 |
mkpredef_call expr.expr_loc "not" [expr] |
| 418 | 448 |
) |
| 419 | 449 |
| Some (Boolexpr n) -> |
| ... | ... | |
| 423 | 453 |
let fold_mutate_pre orig_expr e = |
| 424 | 454 |
match !target with |
| 425 | 455 |
Some (Pre 0) -> ( |
| 426 |
target := None;
|
|
| 456 |
set_mutation_loc ();
|
|
| 427 | 457 |
Expr_pre ({orig_expr with expr_desc = Expr_pre e})
|
| 428 | 458 |
) |
| 429 | 459 |
| Some (Pre n) -> ( |
| ... | ... | |
| 436 | 466 |
match c with |
| 437 | 467 |
| Const_int i -> ( |
| 438 | 468 |
match !target with |
| 439 |
| Some (IncrIntCst 0) -> (target := None; Const_int (i+1))
|
|
| 440 |
| Some (DecrIntCst 0) -> (target := None; Const_int (i-1))
|
|
| 441 |
| Some (SwitchIntCst (0, id)) -> (target := None; Const_int (List.nth (IntSet.elements (IntSet.remove i !records.consts)) id))
|
|
| 469 |
| Some (IncrIntCst 0) -> (set_mutation_loc (); Const_int (i+1))
|
|
| 470 |
| Some (DecrIntCst 0) -> (set_mutation_loc (); Const_int (i-1))
|
|
| 471 |
| Some (SwitchIntCst (0, id)) -> (set_mutation_loc (); Const_int (List.nth (IntSet.elements (IntSet.remove i !records.consts)) id))
|
|
| 442 | 472 |
| Some (IncrIntCst n) -> (target := Some (IncrIntCst (n-1)); c) |
| 443 | 473 |
| Some (DecrIntCst n) -> (target := Some (DecrIntCst (n-1)); c) |
| 444 | 474 |
| Some (SwitchIntCst (n, id)) -> (target := Some (SwitchIntCst (n-1, id)); c) |
| ... | ... | |
| 459 | 489 |
{ c with const_value = fold_mutate_const_value c.const_value }
|
| 460 | 490 |
|
| 461 | 491 |
let rec fold_mutate_expr expr = |
| 492 |
current_loc := Some expr.expr_loc; |
|
| 462 | 493 |
let new_expr = |
| 463 | 494 |
match expr.expr_desc with |
| 464 | 495 |
| Expr_ident id -> fold_mutate_var expr |
| ... | ... | |
| 492 | 523 |
new_expr |
| 493 | 524 |
|
| 494 | 525 |
let fold_mutate_eq eq = |
| 526 |
current_eq_lhs := Some eq.eq_lhs; |
|
| 495 | 527 |
{ eq with eq_rhs = fold_mutate_expr eq.eq_rhs }
|
| 496 | 528 |
|
| 497 | 529 |
let fold_mutate_stmt stmt = |
| ... | ... | |
| 499 | 531 |
| Eq eq -> Eq (fold_mutate_eq eq) |
| 500 | 532 |
| Aut aut -> assert false |
| 501 | 533 |
|
| 502 |
let fold_mutate_node nd = |
|
| 534 |
let fold_mutate_node nd = |
|
| 535 |
current_node := Some nd.node_id; |
|
| 503 | 536 |
{ nd with
|
| 504 | 537 |
node_stmts = |
| 505 | 538 |
List.fold_right (fun stmt res -> (fold_mutate_stmt stmt)::res) nd.node_stmts []; |
| ... | ... | |
| 519 | 552 |
let create_mutant prog directive = |
| 520 | 553 |
target := Some directive; |
| 521 | 554 |
let prog' = fold_mutate_prog prog in |
| 522 |
target := None; |
|
| 523 |
prog' |
|
| 555 |
let mutation_info = match !target , !mutation_info with |
|
| 556 |
| None, Some mi -> mi |
|
| 557 |
| _ -> assert false (* The mutation has not been performed. *) |
|
| 558 |
|
|
| 559 |
in |
|
| 560 |
(* target := None; (* should happen only if no mutation occured during the |
|
| 561 |
visit *)*) |
|
| 562 |
prog', mutation_info |
|
| 524 | 563 |
|
| 525 | 564 |
|
| 526 | 565 |
let op_mutation op = |
| ... | ... | |
| 645 | 684 |
create_mutants_directives (rnb-1) (random_mutation::mutants) |
| 646 | 685 |
in |
| 647 | 686 |
let mutants_directives = create_mutants_directives nb [] in |
| 648 |
List.map (fun d -> d, create_mutant prog d) mutants_directives |
|
| 687 |
List.map (fun d -> |
|
| 688 |
let mutant, loc = create_mutant prog d in |
|
| 689 |
d, loc, mutant ) mutants_directives |
|
| 649 | 690 |
|
| 650 | 691 |
|
| 651 | 692 |
let mutate nb prog = |
| ... | ... | |
| 655 | 696 |
(* !records.nb_boolexpr *) |
| 656 | 697 |
(* (\* !records.op *\) *) |
| 657 | 698 |
(* ; *) |
| 658 |
fold_mutate nb prog, print_directive
|
|
| 699 |
fold_mutate nb prog
|
|
| 659 | 700 |
|
| 660 | 701 |
|
| 661 | 702 |
|
Also available in: Unified diff
[lustret] Improved mutation with json traceability