Source file register.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Utils

let add_label_support () =
  let hfile = Format.asprintf "%a" Filepath.pretty_abs
      (Options.Share.get_file "labels.h")
  in
  Kernel.CppExtraArgs.append_before ["-include "^hfile]

let store_label_data out annotations =
  (* TODO do that in its own module, ultimately shared with the other LTest-tools *)
  (* TODO (later) do something better than csv *)
  let formatter = Format.formatter_of_out_channel out in
  Format.fprintf formatter "# id, status, tag, origin_loc, current_loc, emitter, drivers, exec_time@.";
  let print_one (id, tags, cond, origin_loc) =
    let l = String.split_on_char '/' (print_file_path origin_loc) in
    let origin_file = List.nth l ((List.length l)-1) in
    let origin_line = (fst origin_loc).Filepath.pos_lnum in
    (* let us note obviously uncoverable labels as uncoverable
       (should only work when -lannot-simplify is on) *)
    let verdict = if Cil.isZero cond then "uncoverable" else "unknown" in
    Format.fprintf formatter "%d, %s, %s, %s:%d, , LAnnot, , 0.@." id verdict tags origin_file origin_line
  in
  List.iter print_one (List.rev annotations);
  Format.pp_print_flush formatter ()

let compute_outfile opt files =
  if opt = "" then
    if files = [] then
      "a_labels.out"
    else
      let base = Filepath.to_string_rel (List.hd files) in
      (* TODO check if it's not better to take the last filename *)
      let prefix = Filename.chop_extension base in
      let len_prefix = String.length prefix in
      let suffix = String.sub base len_prefix ((String.length base)-len_prefix) in
      prefix ^ "_labels" ^ suffix
  else
    opt


let annotate_on_project ann_names =
  let filename = compute_outfile (Options.Output.get ()) (Kernel.Files.get ()) in
  let basename = Filename.chop_extension filename in
  (* Remove .hyperlabels file if exists *)
  let hl_data_filename = basename ^ ".hyperlabels" in
  if Sys.file_exists hl_data_filename then
    Sys.remove hl_data_filename;

  let annotations = ref [] in
  let collect ann = annotations := ann :: !annotations in
  Annotators.annotate filename ann_names ~collect (Ast.get ());

  let annotations = !annotations in
  (* output modified c file *)
  Options.feedback "write modified C file (to %s)" filename;
  let out = open_out filename in
  let formatter = Format.formatter_of_out_channel out in
  Utils.Printer.pp_file formatter (Ast.get ());
  Format.pp_print_flush formatter ();
  close_out out;
  (* output label data *)
  let data_filename = basename ^ ".labels" in
  Options.feedback "write label data (to %s)" data_filename;
  Options.feedback "%d labels created" (Annotators.getCurrentLabelId ());
  let out = open_out data_filename in
  store_label_data out annotations;
  close_out out;
  Options.feedback "finished"

let annotate ann_names =
  let base_project = Project.current () in
  let prj_name = (Project.get_name base_project) ^ "_labels" in
  let prj = Project.create_by_copy ~last:false prj_name in
  Options.debug "start project %s" prj_name;
  Project.on prj annotate_on_project ann_names

let setupMutatorOptions () =
  let f mutname =
    Options.debug ~level:2 "Enabling %s mutator" mutname;
    if mutname = "AOR" then L_wm.aorOption := true
    else if mutname = "COR" then L_wm.corOption := true
    else if mutname = "ABS" then L_wm.absOption := true
    else if mutname = "ROR" then L_wm.rorOption := true
    else Options.debug ~level:2 "Unknown mutators %s : Ignored" mutname;
  in
  Options.Mutators.iter f

(* ENTRY POINT *)
let main () =
  try
    Annotators.init_builtins ();
    setupMutatorOptions ();
    annotate (Datatype.String.Set.elements (Options.Annotators.get ()))
  with
  | Globals.No_such_entry_point _ ->
    Options.abort "`-main` parameter missing"
  | Dynamic.Unbound_value(s) -> Options.fatal "%s unbound" s
  | Dynamic.Incompatible_type(s) -> Options.fatal "%s incompatible" s
  | Failure s -> Options.fatal "unexpected failure: %s" s

let main_once, _ = State_builder.apply_once "LAnnotate.run" [] main

let help () =
  if Options.ListAnnotators.get () then begin
    Annotators.print_help Format.std_formatter;
    raise Cmdline.Exit
  end else Cmdline.nop

let () = Cmdline.run_after_exiting_stage help

let run () =
  if not (Options.Annotators.is_empty ()) then main_once ()

let setup_run () =
  if not (Options.Annotators.is_empty ()) then begin
    Kernel.LogicalOperators.on (); (* invalidate the Ast if any *)
    add_label_support ()
  end

let setup_once, _ = State_builder.apply_once "LAnnotate.setup_run" [] setup_run

let () = Cmdline.run_after_configuring_stage setup_once

let () = Boot.Main.extend run