Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / main_lustre_mutator.ml @ 7ecfca04

History | View | Annotate | Download (4.64 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
open Format
13
open Log
14

    
15
open Utils
16
open LustreSpec
17
open Compiler_common
18
 
19
exception StopPhase1 of program
20

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

    
23
let extensions = [".ec"; ".lus"; ".lusi"]
24

    
25

    
26

    
27
(* From prog to prog *)
28
let stage1 prog dirname basename =
29
  (* Removing automata *) 
30
  let prog = expand_automata prog in
31

    
32
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
33

    
34
  (* Importing source *)
35
  let _ = Modules.load_program ISet.empty prog in
36

    
37
  (* Extracting dependencies *)
38
  let dependencies, type_env, clock_env = import_dependencies prog in
39

    
40
  (* Sorting nodes *)
41
  let prog = SortProg.sort prog in
42

    
43
  (* Perform inlining before any analysis *)
44
  let orig, prog =
45
    if !Options.global_inline && !Options.main_node <> "" then
46
      (if !Options.witnesses then prog else []),
47
      Inliner.global_inline basename prog type_env clock_env
48
    else (* if !Option.has_local_inline *)
49
      [],
50
      Inliner.local_inline basename prog type_env clock_env
51
  in
52

    
53
  (* Checking stateless/stateful status *)
54
  if Scopes.Plugin.is_active () then
55
    force_stateful_decls prog
56
  else
57
    check_stateless_decls prog;
58

    
59
  (* Typing *)
60
  let computed_types_env = type_decls type_env prog in
61

    
62
  (* Clock calculus *)
63
  let computed_clocks_env = clock_decls clock_env prog in
64

    
65
  if !Options.gen_mcdc then (
66
    PathConditions.mcdc prog;
67
    exit 0
68
  ) ;
69
  (* generate mutants *)
70
  let mutants, mutation_printer = Mutation.mutate !Options.nb_mutants prog in
71
  
72
  (* Print generated mutants in target directory. *)
73
  let cpt = ref 0 in
74
  List.iter (fun (mutation, mutant) ->
75
    (* Debugging code *)
76
    (* if List.mem !cpt [238;371;601;799;875;998] then *)
77
    (*   Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e  *)
78
    (* ; *)
79
    incr cpt;
80
    let mutant_filename = 
81
      match !Options.dest_dir with
82
      | "" -> (* Mutants are generated in source directory *)
83
	basename^ ".mutant.n" ^ (string_of_int !cpt) ^ ".lus" 
84
      | dir ->  (* Mutants are generated in targer directory *)
85
	dir ^ "/" ^ (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ ".lus"
86
    in
87
    let mutant_out = (
88
      try 
89
	open_out mutant_filename 
90
      with
91
	Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
92
    )
93
    in
94
    let mutant_fmt = formatter_of_out_channel mutant_out in
95
    report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename mutation_printer mutation);
96
    Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant    
97
  )
98
    mutants;
99
  exit 0
100
  
101
let mutate dirname basename extension =
102
  (* Loading the input file *)
103
  let source_name = dirname ^ "/" ^ basename ^ extension in
104

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

    
107
   (* Parsing source *)
108
  let prog = parse_source source_name in
109
  stage1 prog dirname basename
110

    
111
  
112
let anonymous filename =
113
  let ok_ext, ext = List.fold_left
114
    (fun (ok, ext) ext' ->
115
      if not ok && Filename.check_suffix filename ext' then
116
	true, ext'
117
      else
118
	ok, ext)
119
    (false, "") extensions in
120
  if ok_ext then
121
    let dirname = Filename.dirname filename in
122
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
123
    mutate dirname basename ext
124
  else
125
    raise (Arg.Bad ("Can only compile *.lus or *.ec files"))
126

    
127
let _ =
128
  Global.initialize ();
129
  Corelang.add_internal_funs ();
130
  try
131
    Printexc.record_backtrace true;
132

    
133
    let options = Options.options @ 
134
      List.flatten (
135
	List.map Options.plugin_opt [
136
	  Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
137
	]
138
      )
139
    in
140
    
141
    Arg.parse options anonymous usage
142
  with
143
  | Parse.Error _
144
  | Types.Error (_,_) | Clocks.Error (_,_)
145
  | Corelang.Error _ (*| Task_set.Error _*)
146
  | Causality.Error _ -> exit 1
147
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
148
  | exc -> (Utils.track_exception (); raise exc)
149

    
150
(* Local Variables: *)
151
(* compile-command:"make -C .." *)
152
(* End: *)