sarif_gen.ml 4.08 KB
Newer Older
1
2
3
4
5
6
7
8
open Sarif

let frama_c_sarif =
  let name = "frama-c" in
  let version = Config.version_and_codename in
  let semanticVersion = Config.version in
  let fullName = name ^ "-" ^ version in
  let downloadUri = "https://frama-c.com/download.html" in
9
  let sarifLoggerVersion = Mdr_version.version in
10
11
12
13
  Tool.create
    ~name ~version ~semanticVersion
    ~fullName ~downloadUri ~sarifLoggerVersion ()

14

15
16
17
18
19
let get_remarks () =
  let f = Mdr_params.Remarks.get () in
  if f <> "" then Parse_remarks.get_remarks f
  else Datatype.String.Map.empty

20
21
22
23
24
let get_remark remarks label =
  match Datatype.String.Map.find_opt label remarks with
  | None -> []
  | Some l -> l

25
26
27
28
29
let gen_invocation () =
  let commandLine = Array.fold_right (fun s acc -> s ^ " " ^ acc) Sys.argv "" in
  let arguments = List.tl (Array.to_list Sys.argv) in
  Invocation.create ~commandLine ~arguments ()

30
31
32
33
34
35
36
37
38
39
40
41
let gen_remark alarm =
  let open Markdown in
  [ Block
      [ Text
          (plain
             (Printf.sprintf "This alarms represents a potential %s."
                (Alarms.get_description alarm)
             )
          )
      ]
  ]

42
43
let make_message alarm annot remark =
  let open Markdown in
44
45
46
  let name = Alarms.get_name alarm in
  let text = name ^ "." in
  let kind = plain (name ^ ":") in
47
48
  let descr = codelines "acsl" Printer.pp_code_annotation annot in
  let summary = Block [Text kind; descr] in
49
50
51
52
53
  let markdown =
    match remark with
      | [] -> summary :: gen_remark alarm
      | _ -> summary :: remark
  in
54
55
56
  let richText =
    String.trim (Format.asprintf "@[%a@]" Markdown.pp_elements markdown)
  in
57
  Message.create ~text ~richText ()
58
59
60
61

let gen_results remarks =
  let treat_alarm _e _kf s ~rank:_ alarm annot (i, content) =
    let label = "Alarm-" ^ string_of_int i in
62
    let level = Result_level.warning in
63
64
65
66
67
68
69
70
71
72
73
    let remark = get_remark remarks label in
    let message = make_message alarm annot remark in
    let locations = [ Location.of_loc (Cil_datatype.Stmt.loc s) ] in
    let res =
      Sarif_result.create ~level ~message ~locations ()
    in
    (i+1, res :: content)
  in
  let _, content = Alarms.fold treat_alarm (0, []) in
  List.rev content

74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
let is_alarm = function
  | Property.IPCodeAnnot (_,_,ca) -> Extlib.has_some (Alarms.find ca)
  | _ -> false

let level_of_status =
  let open Property_status.Feedback in
  let open Sarif.Result_level in
  function
  | Never_tried -> notApplicable
  | Considered_valid | Valid | Valid_under_hyp | Valid_but_dead -> pass
  | Unknown | Unknown_but_dead -> warning
  | Invalid | Invalid_under_hyp | Invalid_but_dead -> error
  | Inconsistent -> note

let make_ip_message ip =
89
  let text = Format.asprintf "@[%a.@]" Property.short_pretty ip in
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
  Message.plain_text ~text ()

let gen_status ip =
  let status = Property_status.Feedback.get ip in
  let level = level_of_status status in
  let locations = [ Location.of_loc (Property.location ip) ] in
  let message = make_ip_message ip in
  Sarif_result.create ~level ~locations ~message ()

let gen_statuses () =
  let f ip content =
    if is_alarm ip then content else (gen_status ip) :: content
  in
  List.rev (Property_status.fold f [])

105
106
107
108
109
110
111
112
113
114
let gen_files () =
  let add_src_file f =
    let key = Filename.chop_extension (Filename.basename f) in
    let fileLocation = FileLocation.create ~uri:(Filepath.normalize f) () in
    let roles = [ Role.analysisTarget ] in
    let mimeType = "text/x-csrc" in
    key, File.create ~fileLocation ~roles ~mimeType ()
  in
  List.map add_src_file (Kernel.Files.get ())

115
let gen_run remarks =
116
  let tool = frama_c_sarif in
117
  let invocations = [gen_invocation ()] in
118
  let results = gen_results remarks in
119
  let results = results @ (gen_statuses ()) in
120
121
  let files = gen_files () in
  Run.create ~tool ~invocations ~results ~files ()
122
123

let generate () =
124
125
  let remarks = get_remarks () in
  let runs = [ gen_run remarks ] in
126
127
128
129
130
131
132
133
134
135
136
  let json = Schema.create ~runs () in
  let out = Mdr_params.Output.get () in
  let chan =
    if out = "" then stdout
    else begin
      try open_out out
      with Sys_error s ->
        Mdr_params.abort "Unable to open output file %s: %s" out s
    end
  in
  Yojson.Safe.to_channel chan (Schema.to_yojson json)