Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / main_lustre_testgen.ml @ 684d39e7

History | View | Annotate | Download (6.97 KB)

1 40d33d55 xavier.thirioux
(********************************************************************)
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 8446bf03 ploc
open Lustre_types
19 40d33d55 xavier.thirioux
open Compiler_common
20
21
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
22
23
let extensions = [".lus"]
24
25 55a8633c ploc
let pp_trace trace_filename mutation_list = 
26
  let trace_file = open_out trace_filename in
27
  let trace_fmt = formatter_of_out_channel trace_file in
28
  Format.fprintf trace_fmt "@[<v 2>{@ %a@ }@]"
29
    (fprintf_list
30
       ~sep:",@ "
31
       (fun fmt (mutation, mutation_loc, mutant_name) ->
32
	 Format.fprintf fmt "\"%s\": { @[<v 0>%a,@ %a@ }@]" 
33
	   mutant_name
34
	   Mutation.print_directive_json mutation
35
	   Mutation.print_loc_json mutation_loc
36
       ))
37
    mutation_list;
38
  Format.fprintf trace_fmt "@.@?" 
39
  
40 40d33d55 xavier.thirioux
  
41
let testgen_source dirname basename extension =
42
  let source_name = dirname ^ "/" ^ basename ^ extension in
43
44
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
45
46
  (* Parsing source *)
47 217837e2 ploc
  let prog = parse source_name extension in
48 ad4774b0 ploc
  let params = Backends.get_normalization_params () in
49 217837e2 ploc
  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in
50 40d33d55 xavier.thirioux
51 55a8633c ploc
  (* Two cases
52
     - generation of coverage conditions
53
     - generation of mutants: a number of mutated lustre files 
54
  *)
55
  
56 40d33d55 xavier.thirioux
  if !Options.gen_mcdc then (
57 3e1d20e0 ploc
    let prog_mcdc = PathConditions.mcdc prog in
58 cda2fcc8 ploc
    (* We re-type the fresh equations *)
59 5fccce23 ploc
    let _ = Modules.load ~is_header:false prog_mcdc in
60 2d27eedd ploc
    let _ = type_decls !Global.type_env prog_mcdc in
61 3e1d20e0 ploc
62
    let destname = !Options.dest_dir ^ "/" ^ basename in
63 cda2fcc8 ploc
    let source_file = destname ^ ".mcdc" in (* Could be changed *)
64
65
    (* Modified Lustre is produced in fresh .lus file *)
66
    let source_lus = source_file ^ ".lus" in
67
    let source_out = open_out source_lus in
68 3e1d20e0 ploc
    let fmt = formatter_of_out_channel source_out in
69
    Printers.pp_prog fmt prog_mcdc;
70
    Format.fprintf fmt "@.@?";
71 cda2fcc8 ploc
72
    (* Prog is 
73
       (1) cleaned from initial equations TODO
74
       (2) produced as EMF
75
    *)
76
    Options.output := "emf";
77 ad4774b0 ploc
    let params = Backends.get_normalization_params () in
78
    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
79 cda2fcc8 ploc
    let machine_code = Compiler_stages.stage2 prog_mcdc in
80
    let source_emf = source_file ^ ".emf" in 
81
    let source_out = open_out source_emf in
82
    let fmt = formatter_of_out_channel source_out in
83
    EMF_backend.translate fmt basename prog_mcdc machine_code;
84
85 40d33d55 xavier.thirioux
    exit 0
86
  ) ;
87 55a8633c ploc
88
  
89 40d33d55 xavier.thirioux
  (* generate mutants *)
90 55a8633c ploc
  let mutants = Mutation.mutate !Options.nb_mutants prog in
91 40d33d55 xavier.thirioux
  
92
  (* Print generated mutants in target directory. *)
93
  let cpt = ref 0 in
94 55a8633c ploc
  let mutation_list =
95
    List.map (fun (mutation, mutation_loc, mutant) ->
96 40d33d55 xavier.thirioux
    (* Debugging code *)
97
    (* if List.mem !cpt [238;371;601;799;875;998] then *)
98
    (*   Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e  *)
99
    (* ; *)
100 ef8ef3ed ploc
      incr cpt;
101
      let mutant_basename = (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension  in
102
      let mutant_filename = 
103
	match !Options.dest_dir with
104
	| "" -> (* Mutants are generated in source directory *)
105
	   basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
106 40d33d55 xavier.thirioux
      | dir ->  (* Mutants are generated in target directory *)
107 ef8ef3ed ploc
	 dir ^ "/" ^ mutant_basename 
108 40d33d55 xavier.thirioux
    in
109
    let mutant_out = (
110
      try 
111
	open_out mutant_filename 
112
      with
113
	Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
114
    )
115
    in
116
    let mutant_fmt = formatter_of_out_channel mutant_out in
117 55a8633c ploc
    report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?"
118
      mutant_filename
119
      Mutation.print_directive mutation
120
    );
121
    Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant;
122 ef8ef3ed ploc
    mutation, mutation_loc, mutant_basename
123 55a8633c ploc
    )
124
      mutants
125
  in
126 40d33d55 xavier.thirioux
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
127 55a8633c ploc
  
128
  (* Printing traceability *)
129
  let trace_filename = 
130 ef8ef3ed ploc
    match !Options.dest_dir with
131
    | "" -> (* Mutant report is generated in source directory *)
132
       basename^ ".mutation.json" 
133
    | dir ->  (* Mutants are generated in target directory *)
134
       dir ^ "/" ^ (Filename.basename basename)^ ".mutation.json"
135 55a8633c ploc
  in
136
  pp_trace trace_filename mutation_list;
137 5487dd79 ploc
138
  (* Printing the CMakeLists.txt file *)
139
  let cmakelists = 
140
    (if !Options.dest_dir = "" then "" else !Options.dest_dir ^ "/") ^ "CMakeLists.txt"
141
  in
142
  let cmake_file = open_out cmakelists in
143
  let cmake_fmt = formatter_of_out_channel cmake_file in
144
  Format.fprintf cmake_fmt "cmake_minimum_required(VERSION 3.5)@.";
145 5c3b45a0 ploc
  Format.fprintf cmake_fmt "include(\"%s/share/helpful_functions.cmake\")@." Version.prefix;
146
  Format.fprintf cmake_fmt "include(\"%s/share/FindLustre.cmake\")@." Version.prefix;
147 5487dd79 ploc
  Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@.";
148
  Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ ";
149
  Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ ";
150 5d5139a5 ploc
  Format.fprintf cmake_fmt "Lustre_Compile(@[<v 0>@ ";
151
  if !Options.main_node <> "" then Format.fprintf cmake_fmt "NODE \"%s_mutant\"@ " !Options.main_node;
152
  Format.fprintf cmake_fmt "LIBNAME \"${L}_%s_mutant\"@ " !Options.main_node;
153 5487dd79 ploc
  Format.fprintf cmake_fmt "LUS_FILES \"${lus_file}\")@]@]@.";
154
  Format.fprintf cmake_fmt "ENDFOREACH()@.@?";
155
  
156
  
157 55a8633c ploc
  (* We stop the process here *)
158 40d33d55 xavier.thirioux
  exit 0
159 55a8633c ploc
    
160 40d33d55 xavier.thirioux
let testgen dirname basename extension =
161
  match extension with
162
  | ".lus"   -> testgen_source dirname basename extension
163
  | _        -> assert false
164
165
let anonymous filename =
166
  let ok_ext, ext = List.fold_left
167
    (fun (ok, ext) ext' ->
168
      if not ok && Filename.check_suffix filename ext' then
169
	true, ext'
170
      else
171
	ok, ext)
172
    (false, "") extensions in
173
  if ok_ext then
174
    let dirname = Filename.dirname filename in
175
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
176
    testgen dirname basename ext
177
  else
178
    raise (Arg.Bad ("Can only compile *.lus files"))
179
180
let _ =
181
  Global.initialize ();
182
  Corelang.add_internal_funs ();
183
  try
184
    Printexc.record_backtrace true;
185
186 1bff14ac ploc
    let options = Options_management.lustret_options
187 40d33d55 xavier.thirioux
188
    in
189
    
190
    Arg.parse options anonymous usage
191
  with
192
  | Parse.Error _
193
  | Types.Error (_,_) | Clocks.Error (_,_)
194
  | Corelang.Error _ (*| Task_set.Error _*)
195
  | Causality.Error _ -> exit 1
196
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
197 990210f3 ploc
  | exc -> (track_exception (); raise exc)
198 40d33d55 xavier.thirioux
199
(* Local Variables: *)
200
(* compile-command:"make -C .." *)
201
(* End: *)