From 40d33d552d2a819290e78ee6b058f75bf9797929 Mon Sep 17 00:00:00 2001
From: "xavier.thirioux" <xavier.thirioux@enseeiht.fr>
Date: Wed, 5 Apr 2017 16:53:42 +0200
Subject: [PATCH] first version (doesn't even compile) of mutation and test
generation standalone command: lustret mostly a recovery of an ancient svn
repo: mutations
---
Makefile.in | 12 +-
lustrec.odocl | 4 +
src/Makefile.in | 10 +-
src/main_lustre_compiler.ml | 2 +-
src/main_lustre_testgen.ml | 184 +++++++++++
src/mmap.ml | 337 +++++++++++++++++++
src/mutation.ml | 642 ++++++++++++++++++++++++++++++++++++
src/options.ml | 51 ++-
src/pathConditions.ml | 162 +++++++++
9 files changed, 1384 insertions(+), 20 deletions(-)
create mode 100644 src/main_lustre_testgen.ml
create mode 100644 src/mmap.ml
create mode 100644 src/mutation.ml
create mode 100644 src/pathConditions.ml
diff --git a/Makefile.in b/Makefile.in
index d22ebb2e..5eb51426 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -11,12 +11,20 @@ LUSI_MPFR_LIB=include/mpfr_lustre.lusi
LOCAL_BINDIR=bin
LOCAL_DOCDIR=doc/manual
+all: $(LOCAL_BINDIR)/lustrec $(LOCAL_BINDIR)/lustret
+
$(LOCAL_BINDIR)/lustrec: configure Makefile
@echo Compiling binary lustrec
- @$(OCAMLBUILD) -cflags -I,@OCAMLGRAPH_PATH@ -lflag @OCAMLGRAPH_PATH@/graph.cmxa -lflag nums.cmxa -I src -I src/backends/C -I src/plugins/scopes src/main_lustre_compiler.native
+ @$(OCAMLBUILD) -cflags -I,@OCAMLGRAPH_PATH@ -lflag @OCAMLGRAPH_PATH@/graph.cmxa -lflag -I src -I src/backends/C -I src/plugins/scopes src/main_lustre_compiler.native
@mkdir -p $(LOCAL_BINDIR)
@mv _build/src/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
+$(LOCAL_BINDIR)/lustret: configure Makefile
+ @echo Compiling binary lustret
+ @$(OCAMLBUILD) -cflags -I,@OCAMLGRAPH_PATH@ -lflag @OCAMLGRAPH_PATH@/graph.cmxa -lflag nums.cmxa -I src -I src/backends/C -I src/plugins/scopes src/main_lustre_testgen.native
+ @mkdir -p $(LOCAL_BINDIR)
+ @mv _build/src/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
+
configure: configure.ac
@echo configure.ac has changed relaunching autoconf
@autoconf
@@ -74,5 +82,5 @@ install: clean-lusic compile-lusi compile-mpfr-lusi
mkdir -p ${datadir}
install -m 0655 share/FindLustre.cmake ${datadir}
-.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
+.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean
diff --git a/lustrec.odocl b/lustrec.odocl
index 6e869690..f6d36e4a 100644
--- a/lustrec.odocl
+++ b/lustrec.odocl
@@ -33,13 +33,17 @@ Log
Lusic
LustreSpec
Machine_code
+Mmap
+Mutation
Main_lustre_compiler
+Main_lustre_testgen
Modules
Mpfr
Normalization
Optimize_machine
Optimize_prog
Options
+PathConditions
Parse
Parser_lustre
Plugins
diff --git a/src/Makefile.in b/src/Makefile.in
index 126a31f7..8b5b5580 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -10,12 +10,20 @@ LUSI_LIBS=include/math.lusi include/conv.lusi
LOCAL_BINDIR=../bin
LOCAL_DOCDIR=../doc/manual
+all: lustrec lustret
+
lustrec:
@echo Compiling binary lustrec
@$(OCAMLBUILD) main_lustre_compiler.native
@mkdir -p $(LOCAL_BINDIR)
@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
+lustret:
+ @echo Compiling binary lustret
+ @$(OCAMLBUILD) main_lustre_testgen.native
+ @mkdir -p $(LOCAL_BINDIR)
+ @mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
+
doc:
@echo Generating doc
@$(OCAMLBUILD) lustrec.docdir/index.html
@@ -37,5 +45,5 @@ dist-clean: clean
install:
make -C .. install
-.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
+.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 8c8f549c..2e94e7f5 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -457,7 +457,7 @@ let _ =
try
Printexc.record_backtrace true;
- let options = Options.options @
+ let options = Options.lustrec_options @
List.flatten (
List.map Options.plugin_opt [
Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
new file mode 100644
index 00000000..e0e752bd
--- /dev/null
+++ b/src/main_lustre_testgen.ml
@@ -0,0 +1,184 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+(* This module is used for the lustre test generator *)
+
+open Format
+open Log
+
+open Utils
+open LustreSpec
+open Compiler_common
+
+let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
+
+let extensions = [".lus"]
+
+(* From prog to prog *)
+let stage1 prog dirname basename =
+ (* Removing automata *)
+ let prog = expand_automata prog in
+
+ Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
+ (* Importing source *)
+ let _ = Modules.load_program ISet.empty prog in
+
+ (* Extracting dependencies *)
+ let dependencies, type_env, clock_env = import_dependencies prog in
+
+ (* Sorting nodes *)
+ let prog = SortProg.sort prog in
+
+ (* Perform inlining before any analysis *)
+ let orig, prog =
+ if !Options.global_inline && !Options.main_node <> "" then
+ (if !Options.witnesses then prog else []),
+ Inliner.global_inline basename prog type_env clock_env
+ else (* if !Option.has_local_inline *)
+ [],
+ Inliner.local_inline basename prog type_env clock_env
+ in
+
+ check_stateless_decls prog;
+
+ (* Typing *)
+ let computed_types_env = type_decls type_env prog in
+
+ (* Clock calculus *)
+ let computed_clocks_env = clock_decls clock_env prog in
+
+ (* Creating destination directory if needed *)
+ create_dest_dir ();
+
+ (* Compatibility with Lusi *)
+ (* Checking the existence of a lusi (Lustre Interface file) *)
+ let extension = ".lusi" in
+ compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
+
+ Typing.uneval_prog_generics prog;
+ Clock_calculus.uneval_prog_generics prog;
+
+ if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
+ begin
+ let orig = Corelang.copy_prog orig in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
+ check_stateless_decls orig;
+ let _ = Typing.type_prog type_env orig in
+ let _ = Clock_calculus.clock_prog clock_env orig in
+ Typing.uneval_prog_generics orig;
+ Clock_calculus.uneval_prog_generics orig;
+ Inliner.witness
+ basename
+ !Options.main_node
+ orig prog type_env clock_env
+ end;
+
+ (* Normalization phase *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
+ (* Special treatment of arrows in lustre backend. We want to keep them *)
+ if !Options.output = "lustre" then
+ Normalization.unfold_arrow_active := false;
+ let prog = Normalization.normalize_prog prog in
+ Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
+ prog, dependencies
+
+let testgen_source dirname basename extension =
+ let source_name = dirname ^ "/" ^ basename ^ extension in
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
+
+ (* Parsing source *)
+ let prog = parse_source source_name in
+
+ let prog, dependencies = stage1 prog dirname basename in
+
+ if !Options.gen_mcdc then (
+ PathConditions.mcdc prog;
+ exit 0
+ ) ;
+ (* generate mutants *)
+ let mutants, mutation_printer = Mutation.mutate !Options.nb_mutants prog in
+
+ (* Print generated mutants in target directory. *)
+ let cpt = ref 0 in
+ List.iter (fun (mutation, mutant) ->
+ (* Debugging code *)
+ (* if List.mem !cpt [238;371;601;799;875;998] then *)
+ (* Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e *)
+ (* ; *)
+ incr cpt;
+ let mutant_filename =
+ match !Options.dest_dir with
+ | "" -> (* Mutants are generated in source directory *)
+ basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension
+ | dir -> (* Mutants are generated in target directory *)
+ dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension
+ in
+ let mutant_out = (
+ try
+ open_out mutant_filename
+ with
+ Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
+ )
+ in
+ let mutant_fmt = formatter_of_out_channel mutant_out in
+ report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename mutation_printer mutation);
+ Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant
+ )
+ mutants;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
+ (* We stop the process here *)
+ exit 0
+
+let testgen dirname basename extension =
+ match extension with
+ | ".lus" -> testgen_source dirname basename extension
+ | _ -> assert false
+
+let anonymous filename =
+ let ok_ext, ext = List.fold_left
+ (fun (ok, ext) ext' ->
+ if not ok && Filename.check_suffix filename ext' then
+ true, ext'
+ else
+ ok, ext)
+ (false, "") extensions in
+ if ok_ext then
+ let dirname = Filename.dirname filename in
+ let basename = Filename.chop_suffix (Filename.basename filename) ext in
+ testgen dirname basename ext
+ else
+ raise (Arg.Bad ("Can only compile *.lus files"))
+
+let _ =
+ Global.initialize ();
+ Corelang.add_internal_funs ();
+ try
+ Printexc.record_backtrace true;
+
+ let options = Options.lustret_options
+
+ in
+
+ Arg.parse options anonymous usage
+ with
+ | Parse.Error _
+ | Types.Error (_,_) | Clocks.Error (_,_)
+ | Corelang.Error _ (*| Task_set.Error _*)
+ | Causality.Error _ -> exit 1
+ | Sys_error msg -> (eprintf "Failure: %s@." msg)
+ | exc -> (Utils.track_exception (); raise exc)
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/mmap.ml b/src/mmap.ml
new file mode 100644
index 00000000..7d65bc6b
--- /dev/null
+++ b/src/mmap.ml
@@ -0,0 +1,337 @@
+(***********************************************************************)
+(* *)
+(* OCaml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking described in file ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+module type OrderedType =
+ sig
+ type t
+ val compare: t -> t -> int
+ end
+
+module type S =
+ sig
+ type key
+ type +'a t
+ val empty: 'a t
+ val is_empty: 'a t -> bool
+ val mem: key -> 'a t -> bool
+ val add: key -> 'a -> 'a t -> 'a t
+ val singleton: key -> 'a -> 'a t
+ val remove: key -> 'a t -> 'a t
+ val merge:
+ (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+ val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val iter: (key -> 'a -> unit) -> 'a t -> unit
+ val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+ val for_all: (key -> 'a -> bool) -> 'a t -> bool
+ val exists: (key -> 'a -> bool) -> 'a t -> bool
+ val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+ val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
+ val cardinal: 'a t -> int
+ val bindings: 'a t -> (key * 'a) list
+ val min_binding: 'a t -> (key * 'a)
+ val max_binding: 'a t -> (key * 'a)
+ val choose: 'a t -> (key * 'a)
+ val split: key -> 'a t -> 'a t * 'a option * 'a t
+ val find: key -> 'a t -> 'a
+ val map: ('a -> 'b) -> 'a t -> 'b t
+ val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
+ end
+
+module Make(Ord: OrderedType) = struct
+
+ type key = Ord.t
+
+ type 'a t =
+ Empty
+ | Node of 'a t * key * 'a * 'a t * int
+
+ let height = function
+ Empty -> 0
+ | Node(_,_,_,_,h) -> h
+
+ let create l x d r =
+ let hl = height l and hr = height r in
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let singleton x d = Node(Empty, x, d, Empty, 1)
+
+ let bal l x d r =
+ let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
+ let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
+ if hl > hr + 2 then begin
+ match l with
+ Empty -> invalid_arg "Map.bal"
+ | Node(ll, lv, ld, lr, _) ->
+ if height ll >= height lr then
+ create ll lv ld (create lr x d r)
+ else begin
+ match lr with
+ Empty -> invalid_arg "Map.bal"
+ | Node(lrl, lrv, lrd, lrr, _)->
+ create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+ end
+ end else if hr > hl + 2 then begin
+ match r with
+ Empty -> invalid_arg "Map.bal"
+ | Node(rl, rv, rd, rr, _) ->
+ if height rr >= height rl then
+ create (create l x d rl) rv rd rr
+ else begin
+ match rl with
+ Empty -> invalid_arg "Map.bal"
+ | Node(rll, rlv, rld, rlr, _) ->
+ create (create l x d rll) rlv rld (create rlr rv rd rr)
+ end
+ end else
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let empty = Empty
+
+ let is_empty = function Empty -> true | _ -> false
+
+ let rec add x data = function
+ Empty ->
+ Node(Empty, x, data, Empty, 1)
+ | Node(l, v, d, r, h) ->
+ let c = Ord.compare x v in
+ if c = 0 then
+ Node(l, x, data, r, h)
+ else if c < 0 then
+ bal (add x data l) v d r
+ else
+ bal l v d (add x data r)
+
+ let rec find x = function
+ Empty ->
+ raise Not_found
+ | Node(l, v, d, r, _) ->
+ let c = Ord.compare x v in
+ if c = 0 then d
+ else find x (if c < 0 then l else r)
+
+ let rec mem x = function
+ Empty ->
+ false
+ | Node(l, v, d, r, _) ->
+ let c = Ord.compare x v in
+ c = 0 || mem x (if c < 0 then l else r)
+
+ let rec min_binding = function
+ Empty -> raise Not_found
+ | Node(Empty, x, d, r, _) -> (x, d)
+ | Node(l, x, d, r, _) -> min_binding l
+
+ let rec max_binding = function
+ Empty -> raise Not_found
+ | Node(l, x, d, Empty, _) -> (x, d)
+ | Node(l, x, d, r, _) -> max_binding r
+
+ let rec remove_min_binding = function
+ Empty -> invalid_arg "Map.remove_min_elt"
+ | Node(Empty, x, d, r, _) -> r
+ | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+ let merge t1 t2 =
+ match (t1, t2) with
+ (Empty, t) -> t
+ | (t, Empty) -> t
+ | (_, _) ->
+ let (x, d) = min_binding t2 in
+ bal t1 x d (remove_min_binding t2)
+
+ let rec remove x = function
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let c = Ord.compare x v in
+ if c = 0 then
+ merge l r
+ else if c < 0 then
+ bal (remove x l) v d r
+ else
+ bal l v d (remove x r)
+
+ let rec iter f = function
+ Empty -> ()
+ | Node(l, v, d, r, _) ->
+ iter f l; f v d; iter f r
+
+ let rec map f = function
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let l' = map f l in
+ let d' = f d in
+ let r' = map f r in
+ Node(l', v, d', r', h)
+
+ let rec mapi f = function
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let l' = mapi f l in
+ let d' = f v d in
+ let r' = mapi f r in
+ Node(l', v, d', r', h)
+
+ let rec fold f m accu =
+ match m with
+ Empty -> accu
+ | Node(l, v, d, r, _) ->
+ fold f r (f v d (fold f l accu))
+
+ let rec for_all p = function
+ Empty -> true
+ | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r
+
+ let rec exists p = function
+ Empty -> false
+ | Node(l, v, d, r, _) -> p v d || exists p l || exists p r
+
+ (* Beware: those two functions assume that the added k is *strictly*
+ smaller (or bigger) than all the present keys in the tree; it
+ does not test for equality with the current min (or max) key.
+
+ Indeed, they are only used during the "join" operation which
+ respects this precondition.
+ *)
+
+ let rec add_min_binding k v = function
+ | Empty -> singleton k v
+ | Node (l, x, d, r, h) ->
+ bal (add_min_binding k v l) x d r
+
+ let rec add_max_binding k v = function
+ | Empty -> singleton k v
+ | Node (l, x, d, r, h) ->
+ bal l x d (add_max_binding k v r)
+
+ (* Same as create and bal, but no assumptions are made on the
+ relative heights of l and r. *)
+
+ let rec join l v d r =
+ match (l, r) with
+ (Empty, _) -> add_min_binding v d r
+ | (_, Empty) -> add_max_binding v d l
+ | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
+ if lh > rh + 2 then bal ll lv ld (join lr v d r) else
+ if rh > lh + 2 then bal (join l v d rl) rv rd rr else
+ create l v d r
+
+ (* Merge two trees l and r into one.
+ All elements of l must precede the elements of r.
+ No assumption on the heights of l and r. *)
+
+ let concat t1 t2 =
+ match (t1, t2) with
+ (Empty, t) -> t
+ | (t, Empty) -> t
+ | (_, _) ->
+ let (x, d) = min_binding t2 in
+ join t1 x d (remove_min_binding t2)
+
+ let concat_or_join t1 v d t2 =
+ match d with
+ | Some d -> join t1 v d t2
+ | None -> concat t1 t2
+
+ let rec split x = function
+ Empty ->
+ (Empty, None, Empty)
+ | Node(l, v, d, r, _) ->
+ let c = Ord.compare x v in
+ if c = 0 then (l, Some d, r)
+ else if c < 0 then
+ let (ll, pres, rl) = split x l in (ll, pres, join rl v d r)
+ else
+ let (lr, pres, rr) = split x r in (join l v d lr, pres, rr)
+
+ let rec merge f s1 s2 =
+ match (s1, s2) with
+ (Empty, Empty) -> Empty
+ | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 ->
+ let (l2, d2, r2) = split v1 s2 in
+ concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2)
+ | (_, Node (l2, v2, d2, r2, h2)) ->
+ let (l1, d1, r1) = split v2 s1 in
+ concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2)
+ | _ ->
+ assert false
+
+ let rec filter p = function
+ Empty -> Empty
+ | Node(l, v, d, r, _) ->
+ (* call [p] in the expected left-to-right order *)
+ let l' = filter p l in
+ let pvd = p v d in
+ let r' = filter p r in
+ if pvd then join l' v d r' else concat l' r'
+
+ let rec partition p = function
+ Empty -> (Empty, Empty)
+ | Node(l, v, d, r, _) ->
+ (* call [p] in the expected left-to-right order *)
+ let (lt, lf) = partition p l in
+ let pvd = p v d in
+ let (rt, rf) = partition p r in
+ if pvd
+ then (join lt v d rt, concat lf rf)
+ else (concat lt rt, join lf v d rf)
+
+ type 'a enumeration = End | More of key * 'a * 'a t * 'a enumeration
+
+ let rec cons_enum m e =
+ match m with
+ Empty -> e
+ | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e))
+
+ let compare cmp m1 m2 =
+ let rec compare_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) -> 0
+ | (End, _) -> -1
+ | (_, End) -> 1
+ | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+ let c = Ord.compare v1 v2 in
+ if c <> 0 then c else
+ let c = cmp d1 d2 in
+ if c <> 0 then c else
+ compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in compare_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ let equal cmp m1 m2 =
+ let rec equal_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) -> true
+ | (End, _) -> false
+ | (_, End) -> false
+ | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+ Ord.compare v1 v2 = 0 && cmp d1 d2 &&
+ equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in equal_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ let rec cardinal = function
+ Empty -> 0
+ | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r
+
+ let rec bindings_aux accu = function
+ Empty -> accu
+ | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l
+
+ let bindings s =
+ bindings_aux [] s
+
+ let choose = min_binding
+
+end
diff --git a/src/mutation.ml b/src/mutation.ml
new file mode 100644
index 00000000..f2e40022
--- /dev/null
+++ b/src/mutation.ml
@@ -0,0 +1,642 @@
+open Corelang
+open Log
+open Format
+
+let random_seed = ref 0
+let threshold_delay = 95
+let threshold_inc_int = 97
+let threshold_dec_int = 97
+let threshold_random_int = 96
+let threshold_switch_int = 100 (* not implemented yet *)
+let threshold_random_float = 100 (* not used yet *)
+let threshold_negate_bool_var = 95
+let threshold_arith_op = 95
+let threshold_rel_op = 95
+let threshold_bool_op = 95
+
+let int_consts = ref []
+
+let rename_app id =
+ if !Options.no_mutation_suffix then
+ id
+ else
+ id ^ "_mutant"
+
+(************************************************************************************)
+(* Gathering constants in the code *)
+(************************************************************************************)
+
+module IntSet = Set.Make (struct type t = int let compare = compare end)
+module OpCount = Mmap.Make (struct type t = string let compare = compare end)
+
+type records = {
+ consts: IntSet.t;
+ nb_boolexpr: int;
+ nb_pre: int;
+ nb_op: int OpCount.t;
+}
+
+let arith_op = ["+" ; "-" ; "*" ; "/"]
+let bool_op = ["&&"; "||"; "xor"; "impl"]
+let rel_op = ["<" ; "<=" ; ">" ; ">=" ; "!=" ; "=" ]
+let ops = arith_op @ bool_op @ rel_op
+let all_ops = "not" :: ops
+
+let empty_records =
+ {consts=IntSet.empty; nb_boolexpr=0; nb_pre=0; nb_op=OpCount.empty}
+
+let records = ref empty_records
+
+let merge_records records_list =
+ let merge_record r1 r2 =
+ {
+ consts = IntSet.union r1.consts r2.consts;
+
+ nb_boolexpr = r1.nb_boolexpr + r2.nb_boolexpr;
+ nb_pre = r1.nb_pre + r2.nb_pre;
+
+ nb_op = OpCount.merge (fun op r1opt r2opt ->
+ match r1opt, r2opt with
+ | None, _ -> r2opt
+ | _, None -> r1opt
+ | Some x, Some y -> Some (x+y)
+ ) r1.nb_op r2.nb_op
+ }
+ in
+ List.fold_left merge_record empty_records records_list
+
+let compute_records_const_value c =
+ match c with
+ | Const_int i -> {empty_records with consts = IntSet.singleton i}
+ | _ -> empty_records
+
+let rec compute_records_expr expr =
+ let boolexpr =
+ if (Types.repr expr.expr_type).Types.tdesc = Types.Tbool then
+ {empty_records with nb_boolexpr = 1}
+ else
+ empty_records
+ in
+ let subrec =
+ match expr.expr_desc with
+ | Expr_const c -> compute_records_const_value c
+ | Expr_tuple l -> merge_records (List.map compute_records_expr l)
+ | Expr_ite (i,t,e) ->
+ merge_records (List.map compute_records_expr [i;t;e])
+ | Expr_arrow (e1, e2) ->
+ merge_records (List.map compute_records_expr [e1;e2])
+ | Expr_pre e ->
+ merge_records (
+ ({empty_records with nb_pre = 1})
+ ::[compute_records_expr e])
+ | Expr_appl (op_id, args, r) ->
+ if List.mem op_id ops then
+ merge_records (
+ ({empty_records with nb_op = OpCount.singleton op_id 1})
+ ::[compute_records_expr args])
+ else
+ compute_records_expr args
+ | _ -> empty_records
+ in
+ merge_records [boolexpr;subrec]
+
+let compute_records_eq eq = compute_records_expr eq.eq_rhs
+
+let compute_records_node nd =
+ merge_records (List.map compute_records_eq nd.node_eqs)
+
+let compute_records_top_decl td =
+ match td.top_decl_desc with
+ | Node nd -> compute_records_node nd
+ | Consts constsl -> merge_records (List.map (fun c -> compute_records_const_value c.const_value) constsl)
+ | _ -> empty_records
+
+let compute_records prog =
+ merge_records (List.map compute_records_top_decl prog)
+
+(*****************************************************************)
+(* Random mutation *)
+(*****************************************************************)
+
+let check_mut e1 e2 =
+ let rec eq e1 e2 =
+ match e1.expr_desc, e2.expr_desc with
+ | Expr_const c1, Expr_const c2 -> c1 = c2
+ | Expr_ident id1, Expr_ident id2 -> id1 = id2
+ | Expr_tuple el1, Expr_tuple el2 -> List.length el1 = List.length el2 && List.for_all2 eq el1 el2
+ | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> eq i1 i2 && eq t1 t2 && eq e1 e2
+ | Expr_arrow (x1, y1), Expr_arrow (x2, y2) -> eq x1 x2 && eq y1 y2
+ | Expr_pre e1, Expr_pre e2 -> eq e1 e2
+ | Expr_appl (id1, e1, _), Expr_appl (id2, e2, _) -> id1 = id2 && eq e1 e2
+ | _ -> false
+ in
+ if not (eq e1 e2) then
+ Some (e1, e2)
+ else
+ None
+
+let mk_cst_expr c = mkexpr Location.dummy_loc (Expr_const c)
+
+let rdm_mutate_int i =
+ if Random.int 100 > threshold_inc_int then
+ i+1
+ else if Random.int 100 > threshold_dec_int then
+ i-1
+ else if Random.int 100 > threshold_random_int then
+ Random.int 10
+ else if Random.int 100 > threshold_switch_int then
+ let idx = Random.int (List.length !int_consts) in
+ List.nth !int_consts idx
+ else
+ i
+
+let rdm_mutate_float f =
+ if Random.int 100 > threshold_random_float then
+ Random.float 10.
+ else
+ f
+
+let rdm_mutate_op op =
+match op with
+| "+" | "-" | "*" | "/" when Random.int 100 > threshold_arith_op ->
+ let filtered = List.filter (fun x -> x <> op) ["+"; "-"; "*"; "/"] in
+ List.nth filtered (Random.int 3)
+| "&&" | "||" | "xor" | "impl" when Random.int 100 > threshold_bool_op ->
+ let filtered = List.filter (fun x -> x <> op) ["&&"; "||"; "xor"; "impl"] in
+ List.nth filtered (Random.int 3)
+| "<" | "<=" | ">" | ">=" | "!=" | "=" when Random.int 100 > threshold_rel_op ->
+ let filtered = List.filter (fun x -> x <> op) ["<"; "<="; ">"; ">="; "!="; "="] in
+ List.nth filtered (Random.int 5)
+| _ -> op
+
+
+let rdm_mutate_var expr =
+ match (Types.repr expr.expr_type).Types.tdesc with
+ | Types.Tbool ->
+ (* if Random.int 100 > threshold_negate_bool_var then *)
+ let new_e = mkpredef_unary_call Location.dummy_loc "not" expr in
+ Some (expr, new_e), new_e
+ (* else *)
+ (* expr *)
+ | _ -> None, expr
+
+let rdm_mutate_pre orig_expr =
+ let new_e = Expr_pre orig_expr in
+ Some (orig_expr, {orig_expr with expr_desc = new_e}), new_e
+
+
+let rdm_mutate_const_value c =
+ match c with
+ | Const_int i -> Const_int (rdm_mutate_int i)
+ | Const_real s -> Const_real s (* those are string, let's leave them *)
+ | Const_float f -> Const_float (rdm_mutate_float f)
+ | Const_array _
+ | Const_tag _ -> c
+
+let rdm_mutate_const c =
+ let new_const = rdm_mutate_const_value c.const_value in
+ let mut = check_mut (mk_cst_expr c.const_value) (mk_cst_expr new_const) in
+ mut, { c with const_value = new_const }
+
+
+let select_in_list list rdm_mutate_elem =
+ let selected = Random.int (List.length list) in
+ let mutation_opt, new_list, _ =
+ List.fold_right
+ (fun elem (mutation_opt, res, cpt) -> if cpt = selected then
+ let mutation, new_elem = rdm_mutate_elem elem in
+ Some mutation, new_elem::res, cpt+1 else mutation_opt, elem::res, cpt+1)
+ list
+ (None, [], 0)
+ in
+ match mutation_opt with
+ | Some mut -> mut, new_list
+ | _ -> assert false
+
+
+let rec rdm_mutate_expr expr =
+ let mk_e d = { expr with expr_desc = d } in
+ match expr.expr_desc with
+ | Expr_ident id -> rdm_mutate_var expr
+ | Expr_const c ->
+ let new_const = rdm_mutate_const_value c in
+ let mut = check_mut (mk_cst_expr c) (mk_cst_expr new_const) in
+ mut, mk_e (Expr_const new_const)
+ | Expr_tuple l ->
+ let mut, l' = select_in_list l rdm_mutate_expr in
+ mut, mk_e (Expr_tuple l')
+ | Expr_ite (i,t,e) ->
+ let mut, [i'; t'; e'] = select_in_list [i; t; e] rdm_mutate_expr in
+ mut, mk_e (Expr_ite (i', t', e'))
+ | Expr_arrow (e1, e2) ->
+ let mut, [e1'; e2'] = select_in_list [e1; e2] rdm_mutate_expr in
+ mut, mk_e (Expr_arrow (e1', e2'))
+ | Expr_pre e ->
+ let select_pre = Random.bool () in
+ if select_pre then
+ let mut, new_expr = rdm_mutate_pre expr in
+ mut, mk_e new_expr
+ else
+ let mut, e' = rdm_mutate_expr e in
+ mut, mk_e (Expr_pre e')
+ | Expr_appl (op_id, args, r) ->
+ let select_op = Random.bool () in
+ if select_op then
+ let new_op_id = rdm_mutate_op op_id in
+ let new_e = mk_e (Expr_appl (new_op_id, args, r)) in
+ let mut = check_mut expr new_e in
+ mut, new_e
+ else
+ let mut, new_args = rdm_mutate_expr args in
+ mut, mk_e (Expr_appl (op_id, new_args, r))
+
+ (* Other constructs are kept.
+ | Expr_fby of expr * expr
+ | Expr_array of expr list
+ | Expr_access of expr * Dimension.dim_expr
+ | Expr_power of expr * Dimension.dim_expr
+ | Expr_when of expr * ident * label
+ | Expr_merge of ident * (label * expr) list
+ | Expr_uclock of expr * int
+ | Expr_dclock of expr * int
+ | Expr_phclock of expr * rat *)
+ (* | _ -> expr.expr_desc *)
+
+
+let rdm_mutate_eq eq =
+ let mutation, new_rhs = rdm_mutate_expr eq.eq_rhs in
+ mutation, { eq with eq_rhs = new_rhs }
+
+let rdm_mutate_node nd =
+ let mutation, new_node_eqs =
+ select_in_list
+ nd.node_eqs
+ (fun eq -> let mut, new_eq = rdm_mutate_eq eq in
+ report ~level:1
+ (fun fmt -> fprintf fmt "mutation: %a becomes %a@."
+ Printers.pp_node_eq eq
+ Printers.pp_node_eq new_eq);
+ mut, new_eq )
+ in
+ mutation, { nd with node_eqs = new_node_eqs }
+
+let rdm_mutate_top_decl td =
+ match td.top_decl_desc with
+ | Node nd ->
+ let mutation, new_node = rdm_mutate_node nd in
+ mutation, { td with top_decl_desc = Node new_node}
+ | Consts constsl ->
+ let mut, new_constsl = select_in_list constsl rdm_mutate_const in
+ mut, { td with top_decl_desc = Consts new_constsl }
+ | _ -> None, td
+
+(* Create a single mutant with the provided random seed *)
+let rdm_mutate_prog prog =
+ select_in_list prog rdm_mutate_top_decl
+
+let rdm_mutate nb prog =
+ let rec iterate nb res =
+ incr random_seed;
+ if nb <= 0 then
+ res
+ else (
+ Random.init !random_seed;
+ let mutation, new_mutant = rdm_mutate_prog prog in
+ match mutation with
+ None -> iterate nb res
+ | Some mutation -> (
+ if List.mem_assoc mutation res then (
+ iterate nb res
+ )
+ else (
+ report ~level:1 (fun fmt -> fprintf fmt "%i mutants remaining@." nb);
+ iterate (nb-1) ((mutation, new_mutant)::res)
+ )
+ )
+ )
+ in
+ iterate nb []
+
+
+(*****************************************************************)
+(* Random mutation *)
+(*****************************************************************)
+
+type mutant_t = Boolexpr of int | Pre of int | Op of string * int * string | IncrIntCst of int | DecrIntCst of int | SwitchIntCst of int * int
+
+let target : mutant_t option ref = ref None
+
+let print_directive fmt d =
+ match d with
+ | Pre n -> Format.fprintf fmt "pre %i" n
+ | Boolexpr n -> Format.fprintf fmt "boolexpr %i" n
+ | Op (o, i, d) -> Format.fprintf fmt "%s %i -> %s" o i d
+ | IncrIntCst n -> Format.fprintf fmt "incr int cst %i" n
+ | DecrIntCst n -> Format.fprintf fmt "decr int cst %i" n
+ | SwitchIntCst (n, m) -> Format.fprintf fmt "switch int cst %i -> %i" n m
+
+let fold_mutate_int i =
+ if Random.int 100 > threshold_inc_int then
+ i+1
+ else if Random.int 100 > threshold_dec_int then
+ i-1
+ else if Random.int 100 > threshold_random_int then
+ Random.int 10
+ else if Random.int 100 > threshold_switch_int then
+ try
+ let idx = Random.int (List.length !int_consts) in
+ List.nth !int_consts idx
+ with _ -> i
+ else
+ i
+
+let fold_mutate_float f =
+ if Random.int 100 > threshold_random_float then
+ Random.float 10.
+ else
+ f
+
+let fold_mutate_op op =
+(* match op with *)
+(* | "+" | "-" | "*" | "/" when Random.int 100 > threshold_arith_op -> *)
+(* let filtered = List.filter (fun x -> x <> op) ["+"; "-"; "*"; "/"] in *)
+(* List.nth filtered (Random.int 3) *)
+(* | "&&" | "||" | "xor" | "impl" when Random.int 100 > threshold_bool_op -> *)
+(* let filtered = List.filter (fun x -> x <> op) ["&&"; "||"; "xor"; "impl"] in *)
+(* List.nth filtered (Random.int 3) *)
+(* | "<" | "<=" | ">" | ">=" | "!=" | "=" when Random.int 100 > threshold_rel_op -> *)
+(* let filtered = List.filter (fun x -> x <> op) ["<"; "<="; ">"; ">="; "!="; "="] in *)
+(* List.nth filtered (Random.int 5) *)
+(* | _ -> op *)
+ match !target with
+ | Some (Op(op_orig, 0, op_new)) when op_orig = op -> (
+ target := None;
+ op_new
+ )
+ | Some (Op(op_orig, n, op_new)) when op_orig = op -> (
+ target := Some (Op(op_orig, n-1, op_new));
+ op
+ )
+ | _ -> if List.mem op Basic_library.internal_funs then op else rename_app op
+
+
+let fold_mutate_var expr =
+ (* match (Types.repr expr.expr_type).Types.tdesc with *)
+ (* | Types.Tbool -> *)
+ (* (\* if Random.int 100 > threshold_negate_bool_var then *\) *)
+ (* mkpredef_unary_call Location.dummy_loc "not" expr *)
+ (* (\* else *\) *)
+ (* (\* expr *\) *)
+ (* | _ ->
+ *)expr
+
+let fold_mutate_boolexpr expr =
+ match !target with
+ | Some (Boolexpr 0) -> (
+ target := None;
+ mkpredef_unary_call Location.dummy_loc "not" expr
+ )
+ | Some (Boolexpr n) ->
+ (target := Some (Boolexpr (n-1)); expr)
+ | _ -> expr
+
+let fold_mutate_pre orig_expr e =
+ match !target with
+ Some (Pre 0) -> (
+ target := None;
+ Expr_pre ({orig_expr with expr_desc = Expr_pre e})
+ )
+ | Some (Pre n) -> (
+ target := Some (Pre (n-1));
+ Expr_pre e
+ )
+ | _ -> Expr_pre e
+
+let fold_mutate_const_value c =
+match c with
+| Const_int i -> (
+ match !target with
+ | Some (IncrIntCst 0) -> (target := None; Const_int (i+1))
+ | Some (DecrIntCst 0) -> (target := None; Const_int (i-1))
+ | Some (SwitchIntCst (0, id)) -> (target := None; Const_int (List.nth (IntSet.elements (IntSet.remove i !records.consts)) id))
+ | Some (IncrIntCst n) -> (target := Some (IncrIntCst (n-1)); c)
+ | Some (DecrIntCst n) -> (target := Some (DecrIntCst (n-1)); c)
+ | Some (SwitchIntCst (n, id)) -> (target := Some (SwitchIntCst (n-1, id)); c)
+ | _ -> c)
+| _ -> c
+
+(*
+ match c with
+ | Const_int i -> Const_int (fold_mutate_int i)
+ | Const_real s -> Const_real s (* those are string, let's leave them *)
+ | Const_float f -> Const_float (fold_mutate_float f)
+ | Const_array _
+ | Const_tag _ -> c
+TODO
+
+ *)
+let fold_mutate_const c =
+ { c with const_value = fold_mutate_const_value c.const_value }
+
+let rec fold_mutate_expr expr =
+ let new_expr =
+ match expr.expr_desc with
+ | Expr_ident id -> fold_mutate_var expr
+ | _ -> (
+ let new_desc = match expr.expr_desc with
+ | Expr_const c -> Expr_const (fold_mutate_const_value c)
+ | Expr_tuple l -> Expr_tuple (List.fold_right (fun e res -> (fold_mutate_expr e)::res) l [])
+ | Expr_ite (i,t,e) -> Expr_ite (fold_mutate_expr i, fold_mutate_expr t, fold_mutate_expr e)
+ | Expr_arrow (e1, e2) -> Expr_arrow (fold_mutate_expr e1, fold_mutate_expr e2)
+ | Expr_pre e -> fold_mutate_pre expr (fold_mutate_expr e)
+ | Expr_appl (op_id, args, r) -> Expr_appl (fold_mutate_op op_id, fold_mutate_expr args, r)
+ (* Other constructs are kept.
+ | Expr_fby of expr * expr
+ | Expr_array of expr list
+ | Expr_access of expr * Dimension.dim_expr
+ | Expr_power of expr * Dimension.dim_expr
+ | Expr_when of expr * ident * label
+ | Expr_merge of ident * (label * expr) list
+ | Expr_uclock of expr * int
+ | Expr_dclock of expr * int
+ | Expr_phclock of expr * rat *)
+ | _ -> expr.expr_desc
+
+ in
+ { expr with expr_desc = new_desc }
+ )
+ in
+ if (Types.repr expr.expr_type).Types.tdesc = Types.Tbool then
+ fold_mutate_boolexpr new_expr
+ else
+ new_expr
+
+let fold_mutate_eq eq =
+ { eq with eq_rhs = fold_mutate_expr eq.eq_rhs }
+
+let fold_mutate_node nd =
+ { nd with
+ node_eqs =
+ List.fold_right (fun e res -> (fold_mutate_eq e)::res) nd.node_eqs [];
+ node_id = rename_app nd.node_id
+ }
+
+let fold_mutate_top_decl td =
+ match td.top_decl_desc with
+ | Node nd -> { td with top_decl_desc = Node (fold_mutate_node nd)}
+ | Consts constsl -> { td with top_decl_desc = Consts (List.fold_right (fun e res -> (fold_mutate_const e)::res) constsl [])}
+ | _ -> td
+
+(* Create a single mutant with the provided random seed *)
+let fold_mutate_prog prog =
+ List.fold_right (fun e res -> (fold_mutate_top_decl e)::res) prog []
+
+let create_mutant prog directive =
+ target := Some directive;
+ let prog' = fold_mutate_prog prog in
+ target := None;
+ prog'
+
+
+let op_mutation op =
+ let res =
+ let rem_op l = List.filter (fun e -> e <> op) l in
+ if List.mem op arith_op then rem_op arith_op else
+ if List.mem op bool_op then rem_op bool_op else
+ if List.mem op rel_op then rem_op rel_op else
+ (Format.eprintf "Failing with op %s@." op;
+ assert false
+ )
+ in
+ (* Format.eprintf "Mutation op %s to [%a]@." op (Utils.fprintf_list ~sep:"," Format.pp_print_string) res; *)
+ res
+
+let rec remains select list =
+ match list with
+ [] -> []
+ | hd::tl -> if select hd then tl else remains select tl
+
+let next_change m =
+ let res =
+ let rec first_op () =
+ try
+ let min_binding = OpCount.min_binding !records.nb_op in
+ Op (fst min_binding, 0, List.hd (op_mutation (fst min_binding)))
+ with Not_found -> first_boolexpr ()
+ and first_boolexpr () =
+ if !records.nb_boolexpr > 0 then
+ Boolexpr 0
+ else first_pre ()
+ and first_pre () =
+ if !records.nb_pre > 0 then
+ Pre 0
+ else
+ first_op ()
+ and first_intcst () =
+ if IntSet.cardinal !records.consts > 0 then
+ IncrIntCst 0
+ else
+ first_boolexpr ()
+ in
+ match m with
+ | Boolexpr n ->
+ if n+1 >= !records.nb_boolexpr then
+ first_pre ()
+ else
+ Boolexpr (n+1)
+ | Pre n ->
+ if n+1 >= !records.nb_pre then
+ first_op ()
+ else Pre (n+1)
+ | Op (orig, id, mut_op) -> (
+ match remains (fun x -> x = mut_op) (op_mutation orig) with
+ | next_op::_ -> Op (orig, id, next_op)
+ | [] -> if id+1 >= OpCount.find orig !records.nb_op then (
+ match remains (fun (k1, _) -> k1 = orig) (OpCount.bindings !records.nb_op) with
+ | [] -> first_intcst ()
+ | hd::_ -> Op (fst hd, 0, List.hd (op_mutation (fst hd)))
+ ) else
+ Op(orig, id+1, List.hd (op_mutation orig))
+ )
+ | IncrIntCst n ->
+ if n+1 >= IntSet.cardinal !records.consts then
+ DecrIntCst 0
+ else IncrIntCst (n+1)
+ | DecrIntCst n ->
+ if n+1 >= IntSet.cardinal !records.consts then
+ SwitchIntCst (0, 0)
+ else DecrIntCst (n+1)
+ | SwitchIntCst (n, m) ->
+ if m+1 > -1 + IntSet.cardinal !records.consts then
+ SwitchIntCst (n, m+1)
+ else if n+1 >= IntSet.cardinal !records.consts then
+ SwitchIntCst (n+1, 0)
+ else first_boolexpr ()
+
+ in
+ (* Format.eprintf "from: %a to: %a@." print_directive m print_directive res; *)
+ res
+
+let fold_mutate nb prog =
+ incr random_seed;
+ Random.init !random_seed;
+ let find_next_new mutants mutant =
+ let rec find_next_new init current =
+ if init = current then raise Not_found else
+ if List.mem current mutants then
+ find_next_new init (next_change current)
+ else
+ current
+ in
+ find_next_new mutant (next_change mutant)
+ in
+ (* Creating list of nb elements of mutants *)
+ let rec create_mutants_directives rnb mutants =
+ if rnb <= 0 then mutants
+ else
+ let random_mutation =
+ match Random.int 6 with
+ | 5 -> IncrIntCst (try Random.int (IntSet.cardinal !records.consts) with _ -> 0)
+ | 4 -> DecrIntCst (try Random.int (IntSet.cardinal !records.consts) with _ -> 0)
+ | 3 -> SwitchIntCst ((try Random.int (IntSet.cardinal !records.consts) with _ -> 0), (try Random.int (-1 + IntSet.cardinal !records.consts) with _ -> 0))
+ | 2 -> Pre (try Random.int !records.nb_pre with _ -> 0)
+ | 1 -> Boolexpr (try Random.int !records.nb_boolexpr with _ -> 0)
+ | 0 -> let bindings = OpCount.bindings !records.nb_op in
+ let op, nb_op = List.nth bindings (try Random.int (List.length bindings) with _ -> 0) in
+ let new_op = List.nth (op_mutation op) (try Random.int (List.length (op_mutation op)) with _ -> 0) in
+ Op (op, (try Random.int nb_op with _ -> 0), new_op)
+ | _ -> assert false
+ in
+ if List.mem random_mutation mutants then
+ try
+ let new_mutant = (find_next_new mutants random_mutation) in
+ report ~level:2 (fun fmt -> fprintf fmt " %i mutants generated out of %i expected@." (nb-rnb) nb);
+ create_mutants_directives (rnb-1) (new_mutant::mutants)
+ with Not_found -> (
+ report ~level:1 (fun fmt -> fprintf fmt "Only %i mutants generated out of %i expected@." (nb-rnb) nb);
+ mutants
+ )
+ else
+ create_mutants_directives (rnb-1) (random_mutation::mutants)
+ in
+ let mutants_directives = create_mutants_directives nb [] in
+ List.map (fun d -> d, create_mutant prog d) mutants_directives
+
+
+let mutate nb prog =
+ records := compute_records prog;
+ (* Format.printf "Records: %i pre, %i boolexpr" (\* , %a ops *\) *)
+ (* !records.nb_pre *)
+(* !records.nb_boolexpr *)
+(* (\* !records.op *\) *)
+(* ; *)
+ fold_mutate nb prog, print_directive
+
+
+
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
+
+
diff --git a/src/options.ml b/src/options.ml
index 42d00716..0e1fd67a 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -22,7 +22,7 @@ else Version.include_path
let print_version () =
Format.printf "Lustrec compiler, version %s (%s)@." version codename;
Format.printf "Include directory: %s@." include_path;
- Format.printf "User selected Include directory: %s@." !include_dir
+ Format.printf "User selected include directory: %s@." !include_dir
let main_node = ref ""
let static_mem = ref true
@@ -53,6 +53,12 @@ let salsa_enabled = ref true
let sfunction = ref ""
+(* test generation options *)
+let nb_mutants = ref 1000
+let gen_mcdc = ref false
+let no_mutation_suffix = ref false
+
+
let set_mpfr prec =
if prec > 0 then (
mpfr := true;
@@ -61,12 +67,20 @@ let set_mpfr prec =
)
else
failwith "mpfr requires a positive integer"
-
-let options =
-[ "-d", Arg.Set_string dest_dir,
-"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
-"-I", Arg.Set_string include_dir, "Include directory";
+
+let common_options =
+ [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
+ "-I", Arg.Set_string include_dir, "sets include \x1b[4mdirectory\x1b[0m";
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
+ "-print-types", Arg.Set print_types, "prints node types";
+ "-print-clocks", Arg.Set print_clocks, "prints node clocks";
+ "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
+ "-version", Arg.Unit print_version, " displays the version";
+ ]
+
+let lustrec_options =
+ common_options @
+ [
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
@@ -77,20 +91,25 @@ let options =
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
- "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
- "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
- "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
- "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
- "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
+ "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produces traceability file for Horn backend. Enable the horn backend.";
+ "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generates cex enumeration. Enable the horn backend (work in progress)";
+ "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generates queries in generated Horn file. Enable the horn backend (work in progress)";
+ "-horn-sfunction", Arg.Set_string sfunction, "gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
+ "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
- "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
- "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
- "-print_types", Arg.Set print_types, "prints node types";
- "-print_clocks", Arg.Set print_clocks, "prints node clocks";
+ "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
+ "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
- "-version", Arg.Unit print_version, " displays the version";]
+ "-version", Arg.Unit print_version, " displays the version";
+ ]
+let lustret_options =
+ common_options @
+ [ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>";
+ "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
+ "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
+ ]
let plugin_opt (name, activate, options) =
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
new file mode 100644
index 00000000..13330125
--- /dev/null
+++ b/src/pathConditions.ml
@@ -0,0 +1,162 @@
+open LustreSpec
+open Corelang
+open Log
+open Format
+
+module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
+
+let inout_vars = ref []
+
+let print_tautology_var fmt v =
+ match (Types.repr v.var_type).Types.tdesc with
+ | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id
+ | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
+ | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
+ | _ -> Format.fprintf fmt "(true)"
+
+let print_path arg = match !inout_vars with
+ | [] -> Format.printf "%t@." arg
+ | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l
+
+let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
+
+let rec print_pre fmt nb_pre =
+ if nb_pre <= 0 then ()
+ else (
+ Format.fprintf fmt "pre ";
+ print_pre fmt (nb_pre-1)
+ )
+(*
+let combine2 f sub1 sub2 =
+ let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
+ let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
+ let common = IdSet.inter elem_e1 elem_e2 in
+ let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
+ let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
+ (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
+ (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
+ (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) )
+*)
+
+let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
+match active, modified, orig with
+| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)
+| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)
+| [], [], [] -> []
+| _ -> assert false
+
+let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list =
+ let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in
+ let all = List.fold_right IdSet.union elems IdSet.empty in
+ List.map (fun v ->
+ let active_subs = List.map (IdSet.mem v) elems in
+ v, f (select v active_subs subs orig)
+ ) (IdSet.elements all)
+
+let rec compute_neg_expr cpt_pre expr =
+ match expr.expr_desc with
+ | Expr_tuple l ->
+ let neg = List.map (compute_neg_expr cpt_pre) l in
+ combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
+
+ | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool ->
+ let list = [i; t; e] in
+ let neg = List.map (compute_neg_expr cpt_pre) list in
+ combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
+ | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
+ gen_mcdc_cond_guard i;
+ let list = [i; t; e] in
+ let neg = List.map (compute_neg_expr cpt_pre) list in
+ combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
+ )
+ | Expr_arrow (e1, e2) ->
+ let e1' = compute_neg_expr cpt_pre e1 in
+ let e2' = compute_neg_expr cpt_pre e2 in
+ combine (fun [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }) [e1'; e2'] [e1; e2]
+ | Expr_pre e ->
+ List.map
+ (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
+ (compute_neg_expr (cpt_pre+1) e)
+
+ | Expr_appl (op_name, args, r) when List.mem op_name rel_op ->
+ [(expr, cpt_pre), mkpredef_unary_call Location.dummy_loc "not" expr]
+
+ | Expr_appl (op_name, args, r) ->
+ List.map
+ (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
+ (compute_neg_expr cpt_pre args)
+
+ | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
+ [(expr, cpt_pre), mkpredef_unary_call Location.dummy_loc "not" expr]
+ | _ -> []
+
+and
+ gen_mcdc_cond_var v expr =
+ report ~level:1 (fun fmt -> Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr);
+ let leafs_n_neg_expr = compute_neg_expr 0 expr in
+ if List.length leafs_n_neg_expr > 1 then (
+ List.iter (fun ((vi, nb_pre), expr_neg_vi) ->
+ print_path (fun fmt -> Format.fprintf fmt "%a%a and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi);
+ print_path (fun fmt -> Format.fprintf fmt "(not %a%a) and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi)
+ ) leafs_n_neg_expr
+ )
+
+and gen_mcdc_cond_guard expr =
+ report ~level:1 (fun fmt -> Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr);
+ let leafs_n_neg_expr = compute_neg_expr 0 expr in
+ if List.length leafs_n_neg_expr > 1 then (
+ List.iter (fun ((vi, nb_pre), expr_neg_vi) ->
+ print_path (fun fmt -> Format.fprintf fmt "%a%a and (%a != %a)" print_pre nb_pre Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi);
+ print_path (fun fmt -> Format.fprintf fmt "(not %a%a) and (%a != %a)" print_pre nb_pre Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi)
+
+ ) leafs_n_neg_expr
+ )
+
+
+let rec mcdc_expr cpt_pre expr =
+ match expr.expr_desc with
+ | Expr_tuple l -> List.iter (mcdc_expr cpt_pre) l
+ | Expr_ite (i,t,e) -> (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e])
+ | Expr_arrow (e1, e2) -> List.iter (mcdc_expr cpt_pre) [e1; e2]
+ | Expr_pre e -> mcdc_expr (cpt_pre+1) e
+ | Expr_appl (_, args, _) -> mcdc_expr cpt_pre args
+ | _ -> ()
+
+let mcdc_var_def v expr =
+ match (Types.repr expr.expr_type).Types.tdesc with
+ | Types.Tbool -> gen_mcdc_cond_var v expr
+ | _ -> mcdc_expr 0 expr
+
+let mcdc_node_eq eq =
+ match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
+ | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
+ | _::_, Types.Ttuple tl, Expr_tuple rhs -> List.iter2 mcdc_var_def eq.eq_lhs rhs
+ | _ -> mcdc_expr 0 eq.eq_rhs
+
+let mcdc_top_decl td =
+ match td.top_decl_desc with
+ | Node nd -> List.iter mcdc_node_eq nd.node_eqs
+ | _ -> ()
+
+
+let mcdc prog =
+ (* If main node is provided add silly constraints to show in/out variables in the path condition *)
+ if !Options.main_node <> "" then (
+ inout_vars :=
+ let top = List.find
+ (fun td ->
+ match td.top_decl_desc with
+ | Node nd when nd.node_id = !Options.main_node -> true
+ | _ -> false)
+ prog
+ in
+ match top.top_decl_desc with
+ | Node nd -> nd.node_inputs @ nd.node_outputs
+ | _ -> assert false);
+ List.iter mcdc_top_decl prog
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
+
+
--
GitLab