Project

General

Profile

Revision 40d33d55

View differences:

Makefile.in
11 11
LOCAL_BINDIR=bin
12 12
LOCAL_DOCDIR=doc/manual
13 13

  
14
all: $(LOCAL_BINDIR)/lustrec $(LOCAL_BINDIR)/lustret
15

  
14 16
$(LOCAL_BINDIR)/lustrec: configure Makefile
15 17
	@echo Compiling binary lustrec
16
	@$(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
18
	@$(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
17 19
	@mkdir -p $(LOCAL_BINDIR)
18 20
	@mv _build/src/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
19 21

  
22
$(LOCAL_BINDIR)/lustret: configure Makefile
23
	@echo Compiling binary lustret
24
	@$(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
25
	@mkdir -p $(LOCAL_BINDIR)
26
	@mv _build/src/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
27

  
20 28
configure: configure.ac
21 29
	@echo configure.ac has changed relaunching autoconf
22 30
	@autoconf
......
74 82
	mkdir -p ${datadir}
75 83
	install -m 0655 share/FindLustre.cmake ${datadir}
76 84

  
77
.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
85
.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean
78 86

  
lustrec.odocl
33 33
Lusic
34 34
LustreSpec
35 35
Machine_code
36
Mmap
37
Mutation
36 38
Main_lustre_compiler
39
Main_lustre_testgen
37 40
Modules
38 41
Mpfr
39 42
Normalization
40 43
Optimize_machine
41 44
Optimize_prog
42 45
Options
46
PathConditions
43 47
Parse
44 48
Parser_lustre
45 49
Plugins
src/Makefile.in
10 10
LOCAL_BINDIR=../bin
11 11
LOCAL_DOCDIR=../doc/manual
12 12

  
13
all: lustrec lustret
14

  
13 15
lustrec:
14 16
	@echo Compiling binary lustrec
15 17
	@$(OCAMLBUILD) main_lustre_compiler.native
16 18
	@mkdir -p $(LOCAL_BINDIR)
17 19
	@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
18 20

  
21
lustret:
22
	@echo Compiling binary lustret
23
	@$(OCAMLBUILD) main_lustre_testgen.native
24
	@mkdir -p $(LOCAL_BINDIR)
25
	@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
26

  
19 27
doc:
20 28
	@echo Generating doc
21 29
	@$(OCAMLBUILD) lustrec.docdir/index.html
......
37 45
install:
38 46
	make -C .. install
39 47

  
40
.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
48
.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean
41 49

  
src/main_lustre_compiler.ml
457 457
  try
458 458
    Printexc.record_backtrace true;
459 459

  
460
    let options = Options.options @ 
460
    let options = Options.lustrec_options @ 
461 461
      List.flatten (
462 462
	List.map Options.plugin_opt [
463 463
	  Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
src/main_lustre_testgen.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
(* This module is used for the lustre test generator *)
13

  
14
open Format
15
open Log
16

  
17
open Utils
18
open LustreSpec
19
open Compiler_common
20

  
21
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
22

  
23
let extensions = [".lus"]
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 basename prog type_env clock_env
49
  in
50

  
51
  check_stateless_decls prog;
52
  
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
  (* Compatibility with Lusi *)
63
  (* Checking the existence of a lusi (Lustre Interface file) *)
64
  let extension = ".lusi" in
65
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
66

  
67
  Typing.uneval_prog_generics prog;
68
  Clock_calculus.uneval_prog_generics prog;
69

  
70
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
71
    begin
72
      let orig = Corelang.copy_prog orig in
73
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
74
      check_stateless_decls orig;
75
      let _ = Typing.type_prog type_env orig in
76
      let _ = Clock_calculus.clock_prog clock_env orig in
77
      Typing.uneval_prog_generics orig;
78
      Clock_calculus.uneval_prog_generics orig;
79
      Inliner.witness
80
	basename
81
	!Options.main_node
82
	orig prog type_env clock_env
83
    end;
84

  
85
  (* Normalization phase *)
86
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
87
  (* Special treatment of arrows in lustre backend. We want to keep them *)
88
  if !Options.output = "lustre" then
89
    Normalization.unfold_arrow_active := false;
90
  let prog = Normalization.normalize_prog prog in
91
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
92

  
93
  prog, dependencies
94

  
95
let testgen_source dirname basename extension =
96
  let source_name = dirname ^ "/" ^ basename ^ extension in
97

  
98
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
99

  
100
  (* Parsing source *)
101
  let prog = parse_source source_name in
102

  
103
  let prog, dependencies = stage1 prog dirname basename in
104

  
105
  if !Options.gen_mcdc then (
106
    PathConditions.mcdc prog;
107
    exit 0
108
  ) ;
109
  (* generate mutants *)
110
  let mutants, mutation_printer = Mutation.mutate !Options.nb_mutants prog in
111
  
112
  (* Print generated mutants in target directory. *)
113
  let cpt = ref 0 in
114
  List.iter (fun (mutation, mutant) ->
115
    (* Debugging code *)
116
    (* if List.mem !cpt [238;371;601;799;875;998] then *)
117
    (*   Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e  *)
118
    (* ; *)
119
    incr cpt;
120
    let mutant_filename = 
121
      match !Options.dest_dir with
122
      | "" -> (* Mutants are generated in source directory *)
123
	basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
124
      | dir ->  (* Mutants are generated in target directory *)
125
	dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
126
    in
127
    let mutant_out = (
128
      try 
129
	open_out mutant_filename 
130
      with
131
	Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
132
    )
133
    in
134
    let mutant_fmt = formatter_of_out_channel mutant_out in
135
    report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename mutation_printer mutation);
136
    Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant    
137
  )
138
    mutants;
139
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
140
    (* We stop the process here *)
141
  exit 0
142

  
143
let testgen dirname basename extension =
144
  match extension with
145
  | ".lus"   -> testgen_source dirname basename extension
146
  | _        -> assert false
147

  
148
let anonymous filename =
149
  let ok_ext, ext = List.fold_left
150
    (fun (ok, ext) ext' ->
151
      if not ok && Filename.check_suffix filename ext' then
152
	true, ext'
153
      else
154
	ok, ext)
155
    (false, "") extensions in
156
  if ok_ext then
157
    let dirname = Filename.dirname filename in
158
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
159
    testgen dirname basename ext
160
  else
161
    raise (Arg.Bad ("Can only compile *.lus files"))
162

  
163
let _ =
164
  Global.initialize ();
165
  Corelang.add_internal_funs ();
166
  try
167
    Printexc.record_backtrace true;
168

  
169
    let options = Options.lustret_options
170

  
171
    in
172
    
173
    Arg.parse options anonymous usage
174
  with
175
  | Parse.Error _
176
  | Types.Error (_,_) | Clocks.Error (_,_)
177
  | Corelang.Error _ (*| Task_set.Error _*)
178
  | Causality.Error _ -> exit 1
179
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
180
  | exc -> (Utils.track_exception (); raise exc)
181

  
182
(* Local Variables: *)
183
(* compile-command:"make -C .." *)
184
(* End: *)
src/mmap.ml
1
(***********************************************************************)
2
(*                                                                     *)
3
(*                                OCaml                                *)
4
(*                                                                     *)
5
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
6
(*                                                                     *)
7
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
8
(*  en Automatique.  All rights reserved.  This file is distributed    *)
9
(*  under the terms of the GNU Library General Public License, with    *)
10
(*  the special exception on linking described in file ../LICENSE.     *)
11
(*                                                                     *)
12
(***********************************************************************)
13

  
14
module type OrderedType =
15
  sig
16
    type t
17
    val compare: t -> t -> int
18
  end
19

  
20
module type S =
21
  sig
22
    type key
23
    type +'a t
24
    val empty: 'a t
25
    val is_empty: 'a t -> bool
26
    val mem:  key -> 'a t -> bool
27
    val add: key -> 'a -> 'a t -> 'a t
28
    val singleton: key -> 'a -> 'a t
29
    val remove: key -> 'a t -> 'a t
30
    val merge:
31
          (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
32
    val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
33
    val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
34
    val iter: (key -> 'a -> unit) -> 'a t -> unit
35
    val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
36
    val for_all: (key -> 'a -> bool) -> 'a t -> bool
37
    val exists: (key -> 'a -> bool) -> 'a t -> bool
38
    val filter: (key -> 'a -> bool) -> 'a t -> 'a t
39
    val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
40
    val cardinal: 'a t -> int
41
    val bindings: 'a t -> (key * 'a) list
42
    val min_binding: 'a t -> (key * 'a)
43
    val max_binding: 'a t -> (key * 'a)
44
    val choose: 'a t -> (key * 'a)
45
    val split: key -> 'a t -> 'a t * 'a option * 'a t
46
    val find: key -> 'a t -> 'a
47
    val map: ('a -> 'b) -> 'a t -> 'b t
48
    val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
49
  end
50

  
51
module Make(Ord: OrderedType) = struct
52

  
53
    type key = Ord.t
54

  
55
    type 'a t =
56
        Empty
57
      | Node of 'a t * key * 'a * 'a t * int
58

  
59
    let height = function
60
        Empty -> 0
61
      | Node(_,_,_,_,h) -> h
62

  
63
    let create l x d r =
64
      let hl = height l and hr = height r in
65
      Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
66

  
67
    let singleton x d = Node(Empty, x, d, Empty, 1)
68

  
69
    let bal l x d r =
70
      let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
71
      let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
72
      if hl > hr + 2 then begin
73
        match l with
74
          Empty -> invalid_arg "Map.bal"
75
        | Node(ll, lv, ld, lr, _) ->
76
            if height ll >= height lr then
77
              create ll lv ld (create lr x d r)
78
            else begin
79
              match lr with
80
                Empty -> invalid_arg "Map.bal"
81
              | Node(lrl, lrv, lrd, lrr, _)->
82
                  create (create ll lv ld lrl) lrv lrd (create lrr x d r)
83
            end
84
      end else if hr > hl + 2 then begin
85
        match r with
86
          Empty -> invalid_arg "Map.bal"
87
        | Node(rl, rv, rd, rr, _) ->
88
            if height rr >= height rl then
89
              create (create l x d rl) rv rd rr
90
            else begin
91
              match rl with
92
                Empty -> invalid_arg "Map.bal"
93
              | Node(rll, rlv, rld, rlr, _) ->
94
                  create (create l x d rll) rlv rld (create rlr rv rd rr)
95
            end
96
      end else
97
        Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
98

  
99
    let empty = Empty
100

  
101
    let is_empty = function Empty -> true | _ -> false
102

  
103
    let rec add x data = function
104
        Empty ->
105
          Node(Empty, x, data, Empty, 1)
106
      | Node(l, v, d, r, h) ->
107
          let c = Ord.compare x v in
108
          if c = 0 then
109
            Node(l, x, data, r, h)
110
          else if c < 0 then
111
            bal (add x data l) v d r
112
          else
113
            bal l v d (add x data r)
114

  
115
    let rec find x = function
116
        Empty ->
117
          raise Not_found
118
      | Node(l, v, d, r, _) ->
119
          let c = Ord.compare x v in
120
          if c = 0 then d
121
          else find x (if c < 0 then l else r)
122

  
123
    let rec mem x = function
124
        Empty ->
125
          false
126
      | Node(l, v, d, r, _) ->
127
          let c = Ord.compare x v in
128
          c = 0 || mem x (if c < 0 then l else r)
129

  
130
    let rec min_binding = function
131
        Empty -> raise Not_found
132
      | Node(Empty, x, d, r, _) -> (x, d)
133
      | Node(l, x, d, r, _) -> min_binding l
134

  
135
    let rec max_binding = function
136
        Empty -> raise Not_found
137
      | Node(l, x, d, Empty, _) -> (x, d)
138
      | Node(l, x, d, r, _) -> max_binding r
139

  
140
    let rec remove_min_binding = function
141
        Empty -> invalid_arg "Map.remove_min_elt"
142
      | Node(Empty, x, d, r, _) -> r
143
      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
144

  
145
    let merge t1 t2 =
146
      match (t1, t2) with
147
        (Empty, t) -> t
148
      | (t, Empty) -> t
149
      | (_, _) ->
150
          let (x, d) = min_binding t2 in
151
          bal t1 x d (remove_min_binding t2)
152

  
153
    let rec remove x = function
154
        Empty ->
155
          Empty
156
      | Node(l, v, d, r, h) ->
157
          let c = Ord.compare x v in
158
          if c = 0 then
159
            merge l r
160
          else if c < 0 then
161
            bal (remove x l) v d r
162
          else
163
            bal l v d (remove x r)
164

  
165
    let rec iter f = function
166
        Empty -> ()
167
      | Node(l, v, d, r, _) ->
168
          iter f l; f v d; iter f r
169

  
170
    let rec map f = function
171
        Empty ->
172
          Empty
173
      | Node(l, v, d, r, h) ->
174
          let l' = map f l in
175
          let d' = f d in
176
          let r' = map f r in
177
          Node(l', v, d', r', h)
178

  
179
    let rec mapi f = function
180
        Empty ->
181
          Empty
182
      | Node(l, v, d, r, h) ->
183
          let l' = mapi f l in
184
          let d' = f v d in
185
          let r' = mapi f r in
186
          Node(l', v, d', r', h)
187

  
188
    let rec fold f m accu =
189
      match m with
190
        Empty -> accu
191
      | Node(l, v, d, r, _) ->
192
          fold f r (f v d (fold f l accu))
193

  
194
    let rec for_all p = function
195
        Empty -> true
196
      | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r
197

  
198
    let rec exists p = function
199
        Empty -> false
200
      | Node(l, v, d, r, _) -> p v d || exists p l || exists p r
201

  
202
    (* Beware: those two functions assume that the added k is *strictly*
203
       smaller (or bigger) than all the present keys in the tree; it
204
       does not test for equality with the current min (or max) key.
205

  
206
       Indeed, they are only used during the "join" operation which
207
       respects this precondition.
208
    *)
209

  
210
    let rec add_min_binding k v = function
211
      | Empty -> singleton k v
212
      | Node (l, x, d, r, h) ->
213
        bal (add_min_binding k v l) x d r
214

  
215
    let rec add_max_binding k v = function
216
      | Empty -> singleton k v
217
      | Node (l, x, d, r, h) ->
218
        bal l x d (add_max_binding k v r)
219

  
220
    (* Same as create and bal, but no assumptions are made on the
221
       relative heights of l and r. *)
222

  
223
    let rec join l v d r =
224
      match (l, r) with
225
        (Empty, _) -> add_min_binding v d r
226
      | (_, Empty) -> add_max_binding v d l
227
      | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
228
          if lh > rh + 2 then bal ll lv ld (join lr v d r) else
229
          if rh > lh + 2 then bal (join l v d rl) rv rd rr else
230
          create l v d r
231

  
232
    (* Merge two trees l and r into one.
233
       All elements of l must precede the elements of r.
234
       No assumption on the heights of l and r. *)
235

  
236
    let concat t1 t2 =
237
      match (t1, t2) with
238
        (Empty, t) -> t
239
      | (t, Empty) -> t
240
      | (_, _) ->
241
          let (x, d) = min_binding t2 in
242
          join t1 x d (remove_min_binding t2)
243

  
244
    let concat_or_join t1 v d t2 =
245
      match d with
246
      | Some d -> join t1 v d t2
247
      | None -> concat t1 t2
248

  
249
    let rec split x = function
250
        Empty ->
251
          (Empty, None, Empty)
252
      | Node(l, v, d, r, _) ->
253
          let c = Ord.compare x v in
254
          if c = 0 then (l, Some d, r)
255
          else if c < 0 then
256
            let (ll, pres, rl) = split x l in (ll, pres, join rl v d r)
257
          else
258
            let (lr, pres, rr) = split x r in (join l v d lr, pres, rr)
259

  
260
    let rec merge f s1 s2 =
261
      match (s1, s2) with
262
        (Empty, Empty) -> Empty
263
      | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 ->
264
          let (l2, d2, r2) = split v1 s2 in
265
          concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2)
266
      | (_, Node (l2, v2, d2, r2, h2)) ->
267
          let (l1, d1, r1) = split v2 s1 in
268
          concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2)
269
      | _ ->
270
          assert false
271

  
272
    let rec filter p = function
273
        Empty -> Empty
274
      | Node(l, v, d, r, _) ->
275
          (* call [p] in the expected left-to-right order *)
276
          let l' = filter p l in
277
          let pvd = p v d in
278
          let r' = filter p r in
279
          if pvd then join l' v d r' else concat l' r'
280

  
281
    let rec partition p = function
282
        Empty -> (Empty, Empty)
283
      | Node(l, v, d, r, _) ->
284
          (* call [p] in the expected left-to-right order *)
285
          let (lt, lf) = partition p l in
286
          let pvd = p v d in
287
          let (rt, rf) = partition p r in
288
          if pvd
289
          then (join lt v d rt, concat lf rf)
290
          else (concat lt rt, join lf v d rf)
291

  
292
    type 'a enumeration = End | More of key * 'a * 'a t * 'a enumeration
293

  
294
    let rec cons_enum m e =
295
      match m with
296
        Empty -> e
297
      | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e))
298

  
299
    let compare cmp m1 m2 =
300
      let rec compare_aux e1 e2 =
301
          match (e1, e2) with
302
          (End, End) -> 0
303
        | (End, _)  -> -1
304
        | (_, End) -> 1
305
        | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
306
            let c = Ord.compare v1 v2 in
307
            if c <> 0 then c else
308
            let c = cmp d1 d2 in
309
            if c <> 0 then c else
310
            compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
311
      in compare_aux (cons_enum m1 End) (cons_enum m2 End)
312

  
313
    let equal cmp m1 m2 =
314
      let rec equal_aux e1 e2 =
315
          match (e1, e2) with
316
          (End, End) -> true
317
        | (End, _)  -> false
318
        | (_, End) -> false
319
        | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
320
            Ord.compare v1 v2 = 0 && cmp d1 d2 &&
321
            equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
322
      in equal_aux (cons_enum m1 End) (cons_enum m2 End)
323

  
324
    let rec cardinal = function
325
        Empty -> 0
326
      | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r
327

  
328
    let rec bindings_aux accu = function
329
        Empty -> accu
330
      | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l
331

  
332
    let bindings s =
333
      bindings_aux [] s
334

  
335
    let choose = min_binding
336

  
337
end
src/mutation.ml
1
open Corelang
2
open Log
3
open Format
4

  
5
let random_seed = ref 0
6
let threshold_delay = 95
7
let threshold_inc_int = 97
8
let threshold_dec_int = 97
9
let threshold_random_int = 96
10
let threshold_switch_int = 100 (* not implemented yet *)
11
let threshold_random_float = 100 (* not used yet *)
12
let threshold_negate_bool_var = 95
13
let threshold_arith_op = 95
14
let threshold_rel_op = 95
15
let threshold_bool_op = 95
16

  
17
let int_consts = ref []
18

  
19
let rename_app id = 
20
  if !Options.no_mutation_suffix then
21
    id
22
  else
23
    id ^ "_mutant"
24

  
25
(************************************************************************************)
26
(*                    Gathering constants in the code                               *)
27
(************************************************************************************)
28

  
29
module IntSet = Set.Make (struct type t = int let compare = compare end)
30
module OpCount = Mmap.Make (struct type t = string let compare = compare end)
31

  
32
type records = {
33
  consts: IntSet.t;
34
  nb_boolexpr: int;
35
  nb_pre: int;
36
  nb_op: int OpCount.t;
37
}
38

  
39
let arith_op = ["+" ; "-" ; "*" ; "/"] 
40
let bool_op = ["&&"; "||"; "xor";  "impl"] 
41
let rel_op = ["<" ; "<=" ; ">" ; ">=" ; "!=" ; "=" ] 
42
let ops = arith_op @ bool_op @ rel_op
43
let all_ops = "not" :: ops
44

  
45
let empty_records = 
46
  {consts=IntSet.empty; nb_boolexpr=0; nb_pre=0; nb_op=OpCount.empty}
47

  
48
let records = ref empty_records
49

  
50
let merge_records records_list = 
51
  let merge_record r1 r2 =
52
    {
53
      consts = IntSet.union r1.consts r2.consts;
54

  
55
      nb_boolexpr = r1.nb_boolexpr + r2.nb_boolexpr;
56
      nb_pre = r1.nb_pre + r2.nb_pre;
57

  
58
      nb_op = OpCount.merge (fun op r1opt r2opt ->
59
	match r1opt, r2opt with
60
	| None, _ -> r2opt
61
	| _, None -> r1opt
62
	| Some x, Some y -> Some (x+y)
63
      ) r1.nb_op r2.nb_op 
64
    }
65
  in
66
  List.fold_left merge_record empty_records records_list
67
  
68
let compute_records_const_value c =
69
  match c with
70
  | Const_int i -> {empty_records with consts = IntSet.singleton i}
71
  | _ -> empty_records
72

  
73
let rec compute_records_expr expr =
74
  let boolexpr = 
75
    if (Types.repr expr.expr_type).Types.tdesc = Types.Tbool then
76
      {empty_records with nb_boolexpr = 1}
77
    else
78
      empty_records
79
  in
80
  let subrec = 
81
    match expr.expr_desc with
82
    | Expr_const c -> compute_records_const_value c
83
    | Expr_tuple l -> merge_records (List.map compute_records_expr l)
84
    | Expr_ite (i,t,e) -> 
85
      merge_records (List.map compute_records_expr [i;t;e])
86
    | Expr_arrow (e1, e2) ->       
87
      merge_records (List.map compute_records_expr [e1;e2])
88
    | Expr_pre e -> 
89
      merge_records (
90
	({empty_records with nb_pre = 1})
91
	::[compute_records_expr e])
92
    | Expr_appl (op_id, args, r) -> 
93
      if List.mem op_id ops then
94
	merge_records (
95
	  ({empty_records with nb_op = OpCount.singleton op_id 1})
96
	  ::[compute_records_expr args])
97
      else
98
	compute_records_expr args
99
    | _ -> empty_records
100
  in
101
  merge_records [boolexpr;subrec]
102

  
103
let compute_records_eq eq = compute_records_expr eq.eq_rhs
104

  
105
let compute_records_node nd = 
106
  merge_records (List.map compute_records_eq nd.node_eqs)
107

  
108
let compute_records_top_decl td =
109
  match td.top_decl_desc with
110
  | Node nd -> compute_records_node nd
111
  | Consts constsl -> merge_records (List.map (fun c -> compute_records_const_value c.const_value) constsl)
112
  | _ -> empty_records
113

  
114
let compute_records prog = 
115
  merge_records (List.map compute_records_top_decl prog)
116

  
117
(*****************************************************************)
118
(*                  Random mutation                              *)
119
(*****************************************************************)
120

  
121
let check_mut e1 e2 =
122
  let rec eq e1 e2 =
123
    match e1.expr_desc, e2.expr_desc with
124
    | Expr_const c1, Expr_const c2 -> c1 = c2
125
    | Expr_ident id1, Expr_ident id2 -> id1 = id2
126
    | Expr_tuple el1, Expr_tuple el2 -> List.length el1 = List.length el2 && List.for_all2 eq el1 el2
127
    | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> eq i1 i2 && eq t1 t2 && eq e1 e2
128
    | Expr_arrow (x1, y1), Expr_arrow (x2, y2) -> eq x1 x2 && eq y1 y2
129
    | Expr_pre e1, Expr_pre e2 -> eq e1 e2
130
    | Expr_appl (id1, e1, _), Expr_appl (id2, e2, _) -> id1 = id2 && eq e1 e2
131
  | _ -> false
132
  in
133
  if not (eq e1 e2) then
134
    Some (e1, e2)
135
  else
136
    None
137

  
138
let mk_cst_expr c = mkexpr Location.dummy_loc (Expr_const c)
139

  
140
let rdm_mutate_int i = 
141
  if Random.int 100 > threshold_inc_int then
142
    i+1
143
  else if Random.int 100 > threshold_dec_int then
144
    i-1
145
  else if Random.int 100 > threshold_random_int then
146
    Random.int 10
147
  else if Random.int 100 > threshold_switch_int then
148
    let idx = Random.int (List.length !int_consts) in
149
    List.nth !int_consts idx
150
  else
151
    i
152
  
153
let rdm_mutate_float f =
154
  if Random.int 100 > threshold_random_float then
155
    Random.float 10.
156
  else 
157
    f
158

  
159
let rdm_mutate_op op = 
160
match op with
161
| "+" | "-" | "*" | "/" when Random.int 100 > threshold_arith_op ->
162
  let filtered = List.filter (fun x -> x <> op) ["+"; "-"; "*"; "/"] in
163
  List.nth filtered (Random.int 3)
164
| "&&" | "||" | "xor" | "impl" when Random.int 100 > threshold_bool_op ->
165
  let filtered = List.filter (fun x -> x <> op) ["&&"; "||"; "xor"; "impl"] in
166
  List.nth filtered (Random.int 3)
167
| "<" | "<=" | ">" | ">=" | "!=" | "=" when Random.int 100 > threshold_rel_op ->
168
  let filtered = List.filter (fun x -> x <> op) ["<"; "<="; ">"; ">="; "!="; "="] in
169
  List.nth filtered (Random.int 5)
170
| _ -> op
171

  
172

  
173
let rdm_mutate_var expr = 
174
  match (Types.repr expr.expr_type).Types.tdesc with 
175
  | Types.Tbool ->
176
    (* if Random.int 100 > threshold_negate_bool_var then *)
177
    let new_e = mkpredef_unary_call Location.dummy_loc "not" expr in
178
    Some (expr, new_e), new_e
179
    (* else  *)
180
    (*   expr *)
181
  | _ -> None, expr
182
    
183
let rdm_mutate_pre orig_expr = 
184
  let new_e = Expr_pre orig_expr in
185
  Some (orig_expr, {orig_expr with expr_desc = new_e}), new_e
186

  
187

  
188
let rdm_mutate_const_value c =
189
  match c with
190
  | Const_int i -> Const_int (rdm_mutate_int i)
191
  | Const_real s ->  Const_real s (* those are string, let's leave them *)
192
  | Const_float f -> Const_float (rdm_mutate_float f)
193
  | Const_array _
194
  | Const_tag _ -> c
195

  
196
let rdm_mutate_const c =
197
  let new_const = rdm_mutate_const_value c.const_value in
198
  let mut = check_mut (mk_cst_expr c.const_value) (mk_cst_expr new_const) in
199
  mut, { c with const_value = new_const }
200

  
201

  
202
let select_in_list list rdm_mutate_elem = 
203
  let selected = Random.int (List.length list) in
204
  let mutation_opt, new_list, _ = 
205
    List.fold_right
206
      (fun elem (mutation_opt, res, cpt) -> if cpt = selected then 
207
	  let mutation, new_elem = rdm_mutate_elem elem in
208
	  Some mutation, new_elem::res, cpt+1  else mutation_opt, elem::res, cpt+1)
209
      list 
210
      (None, [], 0)
211
  in
212
  match mutation_opt with
213
  | Some mut -> mut, new_list
214
  | _ -> assert false
215

  
216

  
217
let rec rdm_mutate_expr expr =
218
  let mk_e d = { expr with expr_desc = d } in
219
  match expr.expr_desc with
220
  | Expr_ident id -> rdm_mutate_var expr
221
  | Expr_const c -> 
222
    let new_const = rdm_mutate_const_value c in 
223
    let mut = check_mut (mk_cst_expr c) (mk_cst_expr new_const) in
224
    mut, mk_e (Expr_const new_const)
225
  | Expr_tuple l -> 
226
    let mut, l' = select_in_list l rdm_mutate_expr in
227
    mut, mk_e (Expr_tuple l')
228
  | Expr_ite (i,t,e) -> 
229
    let mut, [i'; t'; e'] = select_in_list [i; t; e] rdm_mutate_expr in
230
    mut, mk_e (Expr_ite (i', t', e'))
231
  | Expr_arrow (e1, e2) -> 
232
    let mut, [e1'; e2'] = select_in_list [e1; e2] rdm_mutate_expr in
233
    mut, mk_e (Expr_arrow (e1', e2'))
234
  | Expr_pre e -> 
235
    let select_pre = Random.bool () in
236
    if select_pre then
237
      let mut, new_expr = rdm_mutate_pre expr in
238
      mut, mk_e new_expr
239
    else
240
      let mut, e' = rdm_mutate_expr e in
241
      mut, mk_e (Expr_pre e')
242
  | Expr_appl (op_id, args, r) -> 
243
    let select_op = Random.bool () in
244
    if select_op then
245
      let new_op_id = rdm_mutate_op op_id in
246
      let new_e = mk_e (Expr_appl (new_op_id, args, r)) in
247
      let mut = check_mut expr new_e in
248
      mut, new_e
249
    else
250
      let mut, new_args = rdm_mutate_expr args in
251
      mut, mk_e (Expr_appl (op_id, new_args, r))
252
	
253
  (* Other constructs are kept.
254
  | Expr_fby of expr * expr
255
  | Expr_array of expr list
256
  | Expr_access of expr * Dimension.dim_expr
257
  | Expr_power of expr * Dimension.dim_expr
258
  | Expr_when of expr * ident * label
259
  | Expr_merge of ident * (label * expr) list
260
  | Expr_uclock of expr * int
261
  | Expr_dclock of expr * int
262
  | Expr_phclock of expr * rat *)
263
  (* | _ -> expr.expr_desc *)
264
  
265

  
266
let rdm_mutate_eq eq =
267
  let mutation, new_rhs = rdm_mutate_expr eq.eq_rhs in
268
  mutation, { eq with eq_rhs = new_rhs }
269

  
270
let rdm_mutate_node nd = 
271
  let mutation, new_node_eqs =       
272
    select_in_list 
273
      nd.node_eqs 
274
      (fun eq -> let mut, new_eq = rdm_mutate_eq eq in
275
		 report ~level:1 
276
		   (fun fmt -> fprintf fmt "mutation: %a becomes %a@." 
277
		     Printers.pp_node_eq eq
278
		     Printers.pp_node_eq new_eq);
279
		 mut, new_eq )
280
  in
281
  mutation, { nd with node_eqs = new_node_eqs }
282

  
283
let rdm_mutate_top_decl td =
284
  match td.top_decl_desc with
285
  | Node nd -> 
286
    let mutation, new_node = rdm_mutate_node nd in 
287
    mutation, { td with top_decl_desc = Node new_node}
288
  | Consts constsl -> 
289
    let mut, new_constsl = select_in_list constsl rdm_mutate_const in
290
    mut, { td with top_decl_desc = Consts new_constsl }
291
  | _ -> None, td
292
    
293
(* Create a single mutant with the provided random seed *)
294
let rdm_mutate_prog prog = 
295
  select_in_list prog rdm_mutate_top_decl
296

  
297
let rdm_mutate nb prog = 
298
  let rec iterate nb res =
299
    incr random_seed;
300
    if nb <= 0 then
301
      res
302
    else (
303
      Random.init !random_seed;
304
      let mutation, new_mutant = rdm_mutate_prog prog in
305
      match mutation with
306
	None -> iterate nb res 
307
      | Some mutation -> ( 
308
	if List.mem_assoc mutation res then (
309
	  iterate nb res
310
	)
311
	else (
312
	  report ~level:1 (fun fmt -> fprintf fmt "%i mutants remaining@." nb); 
313
	  iterate (nb-1) ((mutation, new_mutant)::res)
314
	)
315
      )
316
    )
317
  in
318
  iterate nb []
319

  
320

  
321
(*****************************************************************)
322
(*                  Random mutation                              *)
323
(*****************************************************************)
324

  
325
type mutant_t = Boolexpr of int | Pre of int | Op of string * int * string | IncrIntCst of int | DecrIntCst of int | SwitchIntCst of int * int 
326

  
327
let target : mutant_t option ref = ref None
328

  
329
let print_directive fmt d =
330
  match d with
331
  | Pre n -> Format.fprintf fmt "pre %i" n
332
  | Boolexpr n -> Format.fprintf fmt "boolexpr %i" n
333
  | Op (o, i, d) -> Format.fprintf fmt "%s %i -> %s" o i d
334
  | IncrIntCst n ->  Format.fprintf fmt "incr int cst %i" n
335
  | DecrIntCst n ->  Format.fprintf fmt "decr int cst %i" n
336
  | SwitchIntCst (n, m) ->  Format.fprintf fmt "switch int cst %i -> %i" n m
337

  
338
let fold_mutate_int i = 
339
  if Random.int 100 > threshold_inc_int then
340
    i+1
341
  else if Random.int 100 > threshold_dec_int then
342
    i-1
343
  else if Random.int 100 > threshold_random_int then
344
    Random.int 10
345
  else if Random.int 100 > threshold_switch_int then
346
    try
347
	let idx = Random.int (List.length !int_consts) in
348
        List.nth !int_consts idx
349
    with _ -> i
350
  else
351
    i
352
  
353
let fold_mutate_float f =
354
  if Random.int 100 > threshold_random_float then
355
    Random.float 10.
356
  else 
357
    f
358

  
359
let fold_mutate_op op = 
360
(* match op with *)
361
(* | "+" | "-" | "*" | "/" when Random.int 100 > threshold_arith_op -> *)
362
(*   let filtered = List.filter (fun x -> x <> op) ["+"; "-"; "*"; "/"] in *)
363
(*   List.nth filtered (Random.int 3) *)
364
(* | "&&" | "||" | "xor" | "impl" when Random.int 100 > threshold_bool_op -> *)
365
(*   let filtered = List.filter (fun x -> x <> op) ["&&"; "||"; "xor"; "impl"] in *)
366
(*   List.nth filtered (Random.int 3) *)
367
(* | "<" | "<=" | ">" | ">=" | "!=" | "=" when Random.int 100 > threshold_rel_op -> *)
368
(*   let filtered = List.filter (fun x -> x <> op) ["<"; "<="; ">"; ">="; "!="; "="] in *)
369
(*   List.nth filtered (Random.int 5) *)
370
(* | _ -> op *)
371
  match !target with
372
  | Some (Op(op_orig, 0, op_new)) when op_orig = op -> (
373
    target := None;
374
    op_new
375
  )
376
  | Some (Op(op_orig, n, op_new)) when op_orig = op -> (
377
    target := Some (Op(op_orig, n-1, op_new));
378
    op
379
  )
380
  | _ -> if List.mem op Basic_library.internal_funs then op else rename_app op
381

  
382

  
383
let fold_mutate_var expr = 
384
  (* match (Types.repr expr.expr_type).Types.tdesc with  *)
385
  (* | Types.Tbool -> *)
386
  (*     (\* if Random.int 100 > threshold_negate_bool_var then *\) *)
387
  (*     mkpredef_unary_call Location.dummy_loc "not" expr *)
388
  (*   (\* else  *\) *)
389
  (*   (\*   expr *\) *)
390
  (* | _ -> 
391
 *)expr
392

  
393
let fold_mutate_boolexpr expr =
394
  match !target with
395
  | Some (Boolexpr 0) -> (
396
    target := None;
397
    mkpredef_unary_call Location.dummy_loc "not" expr
398
  )
399
  | Some (Boolexpr n) ->
400
      (target := Some (Boolexpr (n-1)); expr)
401
  | _ -> expr
402
    
403
let fold_mutate_pre orig_expr e = 
404
  match !target with
405
    Some (Pre 0) -> (
406
      target := None;
407
      Expr_pre ({orig_expr with expr_desc = Expr_pre e}) 
408
    )
409
  | Some (Pre n) -> (
410
    target := Some (Pre (n-1));
411
    Expr_pre e
412
  )
413
  | _ -> Expr_pre e
414
    
415
let fold_mutate_const_value c = 
416
match c with
417
| Const_int i -> (
418
  match !target with
419
  | Some (IncrIntCst 0) -> (target := None; Const_int (i+1))
420
  | Some (DecrIntCst 0) -> (target := None; Const_int (i-1))
421
  | Some (SwitchIntCst (0, id)) -> (target := None; Const_int (List.nth (IntSet.elements (IntSet.remove i !records.consts)) id)) 
422
  | Some (IncrIntCst n) -> (target := Some (IncrIntCst (n-1)); c)
423
  | Some (DecrIntCst n) -> (target := Some (DecrIntCst (n-1)); c)
424
  | Some (SwitchIntCst (n, id)) -> (target := Some (SwitchIntCst (n-1, id)); c)
425
  | _ -> c)
426
| _ -> c
427

  
428
(*
429
  match c with
430
  | Const_int i -> Const_int (fold_mutate_int i)
431
  | Const_real s -> Const_real s (* those are string, let's leave them *)
432
  | Const_float f -> Const_float (fold_mutate_float f)
433
  | Const_array _
434
  | Const_tag _ -> c
435
TODO
436

  
437
				  *)
438
let fold_mutate_const c =
439
  { c with const_value = fold_mutate_const_value c.const_value }
440

  
441
let rec fold_mutate_expr expr =
442
  let new_expr = 
443
    match expr.expr_desc with
444
    | Expr_ident id -> fold_mutate_var expr
445
    | _ -> (
446
      let new_desc = match expr.expr_desc with
447
	| Expr_const c -> Expr_const (fold_mutate_const_value c)
448
	| Expr_tuple l -> Expr_tuple (List.fold_right (fun e res -> (fold_mutate_expr e)::res) l [])
449
	| Expr_ite (i,t,e) -> Expr_ite (fold_mutate_expr i, fold_mutate_expr t, fold_mutate_expr e)
450
	| Expr_arrow (e1, e2) -> Expr_arrow (fold_mutate_expr e1, fold_mutate_expr e2)
451
	| Expr_pre e -> fold_mutate_pre expr (fold_mutate_expr e)
452
	| Expr_appl (op_id, args, r) -> Expr_appl (fold_mutate_op op_id, fold_mutate_expr args, r)
453
  (* Other constructs are kept.
454
  | Expr_fby of expr * expr
455
  | Expr_array of expr list
456
  | Expr_access of expr * Dimension.dim_expr
457
  | Expr_power of expr * Dimension.dim_expr
458
  | Expr_when of expr * ident * label
459
  | Expr_merge of ident * (label * expr) list
460
  | Expr_uclock of expr * int
461
  | Expr_dclock of expr * int
462
  | Expr_phclock of expr * rat *)
463
  | _ -> expr.expr_desc
464
    
465
      in
466
      { expr with expr_desc = new_desc }
467
    )
468
  in
469
  if (Types.repr expr.expr_type).Types.tdesc = Types.Tbool then
470
    fold_mutate_boolexpr new_expr  
471
  else
472
    new_expr
473

  
474
let fold_mutate_eq eq =
475
  { eq with eq_rhs = fold_mutate_expr eq.eq_rhs }
476

  
477
let fold_mutate_node nd = 
478
  { nd with 
479
    node_eqs = 
480
      List.fold_right (fun e res -> (fold_mutate_eq e)::res) nd.node_eqs [];
481
    node_id = rename_app nd.node_id
482
  }
483

  
484
let fold_mutate_top_decl td =
485
  match td.top_decl_desc with
486
  | Node nd -> { td with top_decl_desc = Node (fold_mutate_node nd)}
487
  | Consts constsl -> { td with top_decl_desc = Consts (List.fold_right (fun e res -> (fold_mutate_const e)::res) constsl [])}
488
  | _ -> td
489
    
490
(* Create a single mutant with the provided random seed *)
491
let fold_mutate_prog prog = 
492
  List.fold_right (fun e res -> (fold_mutate_top_decl e)::res) prog []
493

  
494
let create_mutant prog directive =  
495
  target := Some directive; 
496
  let prog' = fold_mutate_prog prog in
497
  target := None;
498
  prog'
499
  
500

  
501
let op_mutation op = 
502
  let res =
503
    let rem_op l = List.filter (fun e -> e <> op) l in
504
  if List.mem op arith_op then rem_op arith_op else 
505
    if List.mem op bool_op then rem_op bool_op else 
506
      if List.mem op rel_op then rem_op rel_op else 
507
	(Format.eprintf "Failing with op %s@." op;
508
	  assert false
509
	)
510
  in
511
  (* Format.eprintf "Mutation op %s to [%a]@." op (Utils.fprintf_list ~sep:"," Format.pp_print_string) res; *)
512
  res
513

  
514
let rec remains select list =
515
  match list with 
516
    [] -> []
517
  | hd::tl -> if select hd then tl else remains select tl
518
      
519
let next_change m =
520
  let res = 
521
  let rec first_op () = 
522
    try
523
      let min_binding = OpCount.min_binding !records.nb_op in
524
      Op (fst min_binding, 0, List.hd (op_mutation (fst min_binding)))
525
    with Not_found -> first_boolexpr () 
526
  and first_boolexpr () =
527
    if !records.nb_boolexpr > 0 then 
528
      Boolexpr 0 
529
    else first_pre ()
530
  and first_pre () = 
531
    if !records.nb_pre > 0 then 
532
      Pre 0 
533
    else
534
      first_op ()
535
  and first_intcst () =
536
    if IntSet.cardinal !records.consts > 0 then
537
      IncrIntCst 0
538
    else
539
      first_boolexpr ()
540
  in
541
  match m with
542
  | Boolexpr n -> 
543
    if n+1 >= !records.nb_boolexpr then 
544
      first_pre ()
545
    else
546
      Boolexpr (n+1)
547
  | Pre n -> 
548
    if n+1 >= !records.nb_pre then 
549
      first_op ()
550
    else Pre (n+1)
551
  | Op (orig, id, mut_op) -> (
552
    match remains (fun x -> x = mut_op) (op_mutation orig) with
553
    | next_op::_ -> Op (orig, id, next_op)
554
    | [] -> if id+1 >= OpCount.find orig !records.nb_op then (
555
      match remains (fun (k1, _) -> k1 = orig) (OpCount.bindings !records.nb_op) with
556
      | [] -> first_intcst ()
557
      | hd::_ -> Op (fst hd, 0, List.hd (op_mutation (fst hd)))
558
    ) else
559
	Op(orig, id+1, List.hd (op_mutation orig))
560
  )
561
  | IncrIntCst n ->
562
    if n+1 >= IntSet.cardinal !records.consts then
563
      DecrIntCst 0
564
    else IncrIntCst (n+1)
565
  | DecrIntCst n ->
566
    if n+1 >= IntSet.cardinal !records.consts then
567
      SwitchIntCst (0, 0)
568
    else DecrIntCst (n+1)
569
  | SwitchIntCst (n, m) ->
570
    if m+1 > -1 + IntSet.cardinal !records.consts then
571
      SwitchIntCst (n, m+1)
572
    else if n+1 >= IntSet.cardinal !records.consts then
573
      SwitchIntCst (n+1, 0)
574
    else first_boolexpr ()
575

  
576
  in
577
  (* Format.eprintf "from: %a to: %a@." print_directive m print_directive res; *)
578
  res
579

  
580
let fold_mutate nb prog = 
581
  incr random_seed;
582
  Random.init !random_seed;
583
  let find_next_new mutants mutant =
584
    let rec find_next_new init current =
585
      if init = current then raise Not_found else
586
	if List.mem current mutants then
587
	  find_next_new init (next_change current)
588
	else
589
	  current
590
    in
591
    find_next_new mutant (next_change mutant) 
592
  in
593
  (* Creating list of nb elements of mutants *)
594
  let rec create_mutants_directives rnb mutants = 
595
    if rnb <= 0 then mutants 
596
    else 
597
      let random_mutation = 
598
	match Random.int 6 with
599
	| 5 -> IncrIntCst (try Random.int (IntSet.cardinal !records.consts) with _ -> 0)
600
	| 4 -> DecrIntCst (try Random.int (IntSet.cardinal !records.consts) with _ -> 0)
601
	| 3 -> SwitchIntCst ((try Random.int (IntSet.cardinal !records.consts) with _ -> 0), (try Random.int (-1 + IntSet.cardinal !records.consts) with _ -> 0))
602
	| 2 -> Pre (try Random.int !records.nb_pre with _ -> 0)
603
	| 1 -> Boolexpr (try Random.int !records.nb_boolexpr with _ -> 0)
604
	| 0 -> let bindings = OpCount.bindings !records.nb_op in
605
	       let op, nb_op = List.nth bindings (try Random.int (List.length bindings) with _ -> 0) in
606
	       let new_op = List.nth (op_mutation op) (try Random.int (List.length (op_mutation op)) with _ -> 0) in
607
	       Op (op, (try Random.int nb_op with _ -> 0), new_op)
608
	| _ -> assert false
609
      in
610
      if List.mem random_mutation mutants then
611
	try
612
	  let new_mutant = (find_next_new mutants random_mutation) in
613
	  report ~level:2 (fun fmt -> fprintf fmt " %i mutants generated out of %i expected@." (nb-rnb) nb);
614
	 create_mutants_directives (rnb-1) (new_mutant::mutants) 
615
	with Not_found -> (
616
	  report ~level:1 (fun fmt -> fprintf fmt "Only %i mutants generated out of %i expected@." (nb-rnb) nb); 
617
	  mutants
618
	)
619
      else
620
	create_mutants_directives (rnb-1) (random_mutation::mutants)
621
  in
622
  let mutants_directives = create_mutants_directives nb [] in
623
  List.map (fun d -> d, create_mutant prog d) mutants_directives 
624
  
625

  
626
let mutate nb prog =
627
  records := compute_records prog;
628
  (* Format.printf "Records: %i pre, %i boolexpr" (\* , %a ops *\) *)
629
  (*   !records.nb_pre *)
630
(*     !records.nb_boolexpr *)
631
(*     (\* !records.op *\) *)
632
(* ;  *)   
633
  fold_mutate nb prog, print_directive
634

  
635

  
636

  
637

  
638
(* Local Variables: *)
639
(* compile-command:"make -C .." *)
640
(* End: *)
641

  
642
    
src/options.ml
22 22
let print_version () =
23 23
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
24 24
  Format.printf "Include directory: %s@." include_path;
25
  Format.printf "User selected Include directory: %s@." !include_dir
25
  Format.printf "User selected include directory: %s@." !include_dir
26 26

  
27 27
let main_node = ref ""
28 28
let static_mem = ref true
......
53 53

  
54 54
let sfunction = ref ""
55 55

  
56
(* test generation options *)
57
let nb_mutants = ref 1000
58
let gen_mcdc = ref false
59
let no_mutation_suffix = ref false
60

  
61

  
56 62
let set_mpfr prec =
57 63
  if prec > 0 then (
58 64
    mpfr := true;
......
61 67
  )
62 68
  else
63 69
    failwith "mpfr requires a positive integer"
64
			
65
let options =
66
[ "-d", Arg.Set_string dest_dir,
67
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
68
"-I", Arg.Set_string include_dir, "Include directory";
70

  
71
let common_options =
72
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
73
    "-I", Arg.Set_string include_dir, "sets include \x1b[4mdirectory\x1b[0m";
69 74
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
75
    "-print-types", Arg.Set print_types, "prints node types";
76
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
77
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
78
    "-version", Arg.Unit print_version, " displays the version";
79
  ]
80

  
81
let lustrec_options =
82
   common_options @
83
  [ 
70 84
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
71 85
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
72 86
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
......
77 91
    "-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";
78 92
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
79 93
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
80
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
81
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
82
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
83
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
84
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
94
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produces traceability file for Horn backend. Enable the horn backend.";
95
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generates cex enumeration. Enable the horn backend (work in progress)";
96
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generates queries in generated Horn file. Enable the horn backend (work in progress)";
97
    "-horn-sfunction", Arg.Set_string sfunction, "gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
98
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
85 99
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
86
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
87
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
88
    "-print_types", Arg.Set print_types, "prints node types";
89
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
100
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
101
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
90 102
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
91 103
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
92
    "-version", Arg.Unit print_version, " displays the version";]
104
    "-version", Arg.Unit print_version, " displays the version";
105
  ]
93 106

  
107
let lustret_options =
108
  common_options @
109
  [ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>";
110
    "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
111
    "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
112
  ]
94 113

  
95 114
let plugin_opt (name, activate, options) =
96 115
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
src/pathConditions.ml
1
open LustreSpec 
2
open Corelang
3
open Log
4
open Format
5

  
6
module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
7

  
8
let inout_vars = ref [] 
9

  
10
let print_tautology_var fmt v =
11
  match (Types.repr v.var_type).Types.tdesc with
12
  | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id
13
  | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
14
  | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
15
  | _ -> Format.fprintf fmt "(true)"
16

  
17
let print_path arg = match !inout_vars with
18
  | [] -> Format.printf "%t@." arg  
19
  | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l
20

  
21
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
22

  
23
let rec print_pre fmt nb_pre =
24
  if nb_pre <= 0 then () 
25
  else (
26
    Format.fprintf fmt "pre ";
27
    print_pre fmt (nb_pre-1)
28
  )
29
(*
30
let combine2 f sub1 sub2 = 
31
    let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
32
    let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
33
    let common = IdSet.inter elem_e1 elem_e2 in
34
    let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
35
    let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
36
    (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
37
      (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
38
      (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common))      )
39
*)
40

  
41
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
42
match active, modified, orig with
43
| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)
44
| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)
45
| [], [], [] -> []
46
| _ -> assert false
47
  
48
let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list  = 
49
  let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in
50
  let all = List.fold_right IdSet.union elems IdSet.empty in
51
  List.map (fun v ->
52
    let active_subs = List.map (IdSet.mem v) elems in
53
    v, f (select v active_subs subs orig)
54
  ) (IdSet.elements all)
55

  
56
let rec compute_neg_expr cpt_pre expr = 
57
  match expr.expr_desc with
58
  | Expr_tuple l -> 
59
    let neg = List.map (compute_neg_expr cpt_pre) l in
60
    combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
61

  
62
  | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> 
63
    let list = [i; t; e] in
64
    let neg = List.map (compute_neg_expr cpt_pre) list in
65
    combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
66
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
67
    gen_mcdc_cond_guard i;
68
    let list = [i; t; e] in
69
    let neg = List.map (compute_neg_expr cpt_pre) list in
70
    combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
71
  )
72
  | Expr_arrow (e1, e2) -> 
73
    let e1' = compute_neg_expr cpt_pre e1 in
74
    let e2' = compute_neg_expr cpt_pre e2 in
75
    combine (fun [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }) [e1'; e2'] [e1; e2]
76
  | Expr_pre e -> 
77
    List.map 
78
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
79
      (compute_neg_expr (cpt_pre+1) e)
80

  
81
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
82
    [(expr, cpt_pre), mkpredef_unary_call Location.dummy_loc "not" expr]
83

  
84
  | Expr_appl (op_name, args, r) -> 
85
    List.map 
86
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
87
	(compute_neg_expr cpt_pre args)
88

  
89
  | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
90
    [(expr, cpt_pre), mkpredef_unary_call Location.dummy_loc "not" expr]
91
  | _ -> []
92

  
93
and  
94
 gen_mcdc_cond_var v expr =
95
  report ~level:1 (fun fmt -> Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr);
96
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
97
  if List.length leafs_n_neg_expr > 1 then (
98
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
99
      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);
100
      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)
101
    ) leafs_n_neg_expr
102
  )
103

  
104
and gen_mcdc_cond_guard expr =
105
  report ~level:1 (fun fmt -> Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr);
106
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
107
  if List.length leafs_n_neg_expr > 1 then (
108
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
109
      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);
110
      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)
111
   
112
 ) leafs_n_neg_expr
113
  )
114
  
115

  
116
let rec mcdc_expr cpt_pre expr = 
117
  match expr.expr_desc with
118
  | Expr_tuple l -> List.iter (mcdc_expr cpt_pre) l
119
  | Expr_ite (i,t,e) -> (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e])
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff