Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / main_lustre_testgen.ml @ 264a4844

History | View | Annotate | Download (5.75 KB)

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 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
  Typing.uneval_prog_generics prog;
63
  Clock_calculus.uneval_prog_generics prog;
64

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

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

    
88
  prog, dependencies
89

    
90
let testgen_source dirname basename extension =
91
  let source_name = dirname ^ "/" ^ basename ^ extension in
92

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

    
95
  (* Parsing source *)
96
  let prog = parse_source source_name in
97

    
98
  let prog, dependencies = stage1 prog dirname basename in
99

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

    
138
let testgen dirname basename extension =
139
  match extension with
140
  | ".lus"   -> testgen_source dirname basename extension
141
  | _        -> assert false
142

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

    
158
let _ =
159
  Global.initialize ();
160
  Corelang.add_internal_funs ();
161
  try
162
    Printexc.record_backtrace true;
163

    
164
    let options = Options_management.lustret_options
165

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

    
177
(* Local Variables: *)
178
(* compile-command:"make -C .." *)
179
(* End: *)