Project

General

Profile

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