Project

General

Profile

Download (7.3 KB) Statistics
| Branch: | Tag: | Revision:
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
open Utils
17
open Compiler_common
18

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

    
21
let extensions = [ ".lus" ]
22

    
23
let pp_trace trace_filename mutation_list =
24
  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
    (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
    mutation_list;
32
  Format.fprintf trace_fmt "@.@?"
33

    
34
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
  let prog = parse source_name extension in
41
  let params = Backends.get_normalization_params () in
42
  let prog, _ =
43
    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
  in
50

    
51
  (* Two cases - generation of coverage conditions - generation of mutants: a
52
     number of mutated lustre files *)
53
  if !Options.gen_mcdc then (
54
    let prog_mcdc = PathConditions.mcdc prog in
55
    (* We re-type the fresh equations *)
56
    (*let _ = Modules.load ~is_header:false prog_mcdc in*)
57
    let _ = type_decls !Global.type_env prog_mcdc in
58

    
59
    let destname = !Options.dest_dir ^ "/" ^ basename in
60
    let source_file = destname ^ ".mcdc" in
61

    
62
    (* Could be changed *)
63

    
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
    let fmt = formatter_of_out_channel source_out in
68
    Printers.pp_prog fmt prog_mcdc;
69
    Format.fprintf fmt "@.@?";
70

    
71
    (* Prog is (1) cleaned from initial equations TODO (2) produced as EMF *)
72
    Options.output := "emf";
73
    let params = Backends.get_normalization_params () in
74
    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
75
    let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in
76
    let source_emf = source_file ^ ".emf" in
77
    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
    exit 0);
82

    
83
  (* generate mutants *)
84
  let mutants = Mutation.mutate !Options.nb_mutants prog in
85

    
86
  (* Print generated mutants in target directory. *)
87
  let cpt = ref 0 in
88
  let mutation_list =
89
    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
      mutants
124
  in
125
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
126

    
127
  (* Printing traceability *)
128
  let trace_filename =
129
    match !Options.dest_dir with
130
    | "" ->
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
  in
137
  pp_trace trace_filename mutation_list;
138

    
139
  (* Printing the CMakeLists.txt file *)
140
  let cmakelists =
141
    (if !Options.dest_dir = "" then "" else !Options.dest_dir ^ "/")
142
    ^ "CMakeLists.txt"
143
  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
  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
  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
  Format.fprintf cmake_fmt "Lustre_Compile(@[<v 0>@ ";
155
  if !Options.main_node <> "" then
156
    Format.fprintf cmake_fmt "NODE \"%s_mutant\"@ " !Options.main_node;
157
  Format.fprintf cmake_fmt "LIBNAME \"${L}_%s_mutant\"@ " !Options.main_node;
158
  Format.fprintf cmake_fmt "LUS_FILES \"${lus_file}\")@]@]@.";
159
  Format.fprintf cmake_fmt "ENDFOREACH()@.@?";
160

    
161
  (* We stop the process here *)
162
  exit 0
163

    
164
let testgen dirname basename extension =
165
  match extension with
166
  | ".lus" ->
167
    testgen_source dirname basename extension
168
  | _ ->
169
    assert false
170

    
171
let anonymous filename =
172
  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
  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
  else raise (Arg.Bad "Can only compile *.lus files")
184

    
185
let _ =
186
  Global.initialize ();
187
  Corelang.add_internal_funs ();
188
  try
189
    Printexc.record_backtrace true;
190

    
191
    let options = Options_management.lustret_options in
192

    
193
    Arg.parse options anonymous usage
194
  with
195
  | Parse.Error _
196
  | 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

    
208
(* Local Variables: *)
209
(* compile-command:"make -C .." *)
210
(* End: *)
(37-37/66)