sarif_gen.ml 7.45 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

23
24
25
26
open Sarif

let frama_c_sarif =
  let name = "frama-c" in
27
28
  let version = Fc_config.version_and_codename in
  let semanticVersion = Fc_config.version in
29
30
31
  let fullName = name ^ "-" ^ version in
  let downloadUri = "https://frama-c.com/download.html" in
  Tool.create
Andre Maroneze's avatar
Andre Maroneze committed
32
    (Driver.create ~name ~version ~semanticVersion ~fullName ~downloadUri ())
33

34

35
36
37
38
39
let get_remarks () =
  let f = Mdr_params.Remarks.get () in
  if f <> "" then Parse_remarks.get_remarks f
  else Datatype.String.Map.empty

40
41
42
43
44
let get_remark remarks label =
  match Datatype.String.Map.find_opt label remarks with
  | None -> []
  | Some l -> l

45
46
47
48
49
50
51
52
53
54
let command_line () = Array.to_list Sys.argv

module Analysis_cmdline =
  State_builder.Ref(Datatype.List(Datatype.String))
    (struct
      let name = "Sarif_gen.Analysis_cmdline"
      let dependencies = []
      let default = command_line
    end)

55
let gen_invocation () =
56
57
58
  let cl = Analysis_cmdline.get () in
  let commandLine = String.concat " " cl in
  let arguments = List.tl cl in
59
60
  Invocation.create ~commandLine ~arguments ()

61
62
63
64
65
let gen_remark alarm =
  let open Markdown in
  [ Block
      [ Text
          (plain
66
             (Printf.sprintf "This alarm represents a potential %s."
67
68
69
70
71
72
                (Alarms.get_description alarm)
             )
          )
      ]
  ]

Andre Maroneze's avatar
Andre Maroneze committed
73
let kind_of_status =
74
  let open Property_status.Feedback in
Andre Maroneze's avatar
Andre Maroneze committed
75
  let open Sarif.Result_kind in
76
77
78
  function
  | Never_tried -> notApplicable
  | Considered_valid | Valid | Valid_under_hyp | Valid_but_dead -> pass
Andre Maroneze's avatar
Andre Maroneze committed
79
80
81
82
83
84
85
86
87
88
89
  | Unknown | Unknown_but_dead -> open_
  | Invalid | Invalid_under_hyp | Invalid_but_dead -> fail
  | Inconsistent -> review

let level_of_status =
  let open Property_status.Feedback in
  let open Sarif.Result_level in
  function
  | Never_tried -> none
  | Considered_valid | Valid | Valid_under_hyp | Valid_but_dead -> none
  | Unknown | Unknown_but_dead -> none
90
  | Invalid | Invalid_under_hyp | Invalid_but_dead -> error
Andre Maroneze's avatar
Andre Maroneze committed
91
  | Inconsistent -> none
92

93
94
let make_message alarm annot remark =
  let open Markdown in
95
96
97
  let name = Alarms.get_name alarm in
  let text = name ^ "." in
  let kind = plain (name ^ ":") in
98
  let descr = codeblock ~lang:"acsl" "%a" Printer.pp_code_annotation annot in
99
  let summary = Block (Text kind :: descr) in
100
101
  let markdown =
    match remark with
Virgile Prevosto's avatar
Virgile Prevosto committed
102
103
    | [] -> summary :: gen_remark alarm
    | _ -> summary :: remark
104
  in
105
  let richText =
106
107
    String.trim
      (Format.asprintf "@[%a@]" (Markdown.pp_elements ~page:"") markdown)
108
  in
109
  Message.create ~text ~richText ()
110

111
112
113
114
let opt_physical_location_of_loc loc =
  if loc = Cil_datatype.Location.unknown then []
  else [ Location.of_loc loc ]

115
let gen_results remarks =
116
  let treat_alarm _e kf s ~rank:_ alarm annot (i, rules, content) =
117
    let prop = Property.ip_of_code_annot_single kf s annot in
118
119
120
121
    let ruleId = Alarms.get_name alarm in
    let rules =
      Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
    in
122
    let label = "Alarm-" ^ string_of_int i in
Andre Maroneze's avatar
Andre Maroneze committed
123
    let kind = kind_of_status (Property_status.Feedback.get prop) in
124
    let level = level_of_status (Property_status.Feedback.get prop) in
125
126
    let remark = get_remark remarks label in
    let message = make_message alarm annot remark in
127
    let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
128
    let res =
Andre Maroneze's avatar
Andre Maroneze committed
129
      Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
130
    in
131
132
133
134
    (i+1, rules, res :: content)
  in
  let _, rules, content =
    Alarms.fold treat_alarm (0, Datatype.String.Map.empty,[])
135
  in
136
  rules, List.rev content
137

138
let is_alarm = function
139
  | Property.(IPCodeAnnot { ica_ca }) -> Extlib.has_some (Alarms.find ica_ca)
140
141
142
  | _ -> false

let make_ip_message ip =
143
  let text = Format.asprintf "@[%a.@]" Property.short_pretty ip in
144
145
146
147
148
  Message.plain_text ~text ()

let gen_status ip =
  let status = Property_status.Feedback.get ip in
  let level = level_of_status status in
149
  let locations = opt_physical_location_of_loc (Property.location ip) in
150
151
152
153
154
155
156
157
158
  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 [])

159
160
let gen_files () =
  let add_src_file f =
161
162
163
164
    let key =
      let fname = Filepath.Normalized.to_pretty_string f in
      Filename.chop_extension (Filename.basename fname)
    in
Andre Maroneze's avatar
Andre Maroneze committed
165
    let artifactLocation = ArtifactLocation.create ~uri:(f :> string) () in
166
167
    let roles = [ Role.analysisTarget ] in
    let mimeType = "text/x-csrc" in
Andre Maroneze's avatar
Andre Maroneze committed
168
    key, File.create ~artifactLocation ~roles ~mimeType ()
169
170
171
  in
  List.map add_src_file (Kernel.Files.get ())

172
173
174
175
176
177
178
179
let add_rule id desc l =
  let text = desc ^ "." in
  let shortDescription = Message.plain_text ~text () in
  let rule = Rule.create ~id ~shortDescription () in
  (id, rule) :: l

let make_rule_dictionary rules = Datatype.String.Map.fold add_rule rules []

180
let gen_run remarks =
181
  let tool = frama_c_sarif in
182
  let invocations = [gen_invocation ()] in
Virgile Prevosto's avatar
Virgile Prevosto committed
183
184
185
186
  let rules, results = gen_results remarks in
  let user_annot_results = gen_statuses () in
  let rules =
    match user_annot_results with
Virgile Prevosto's avatar
Virgile Prevosto committed
187
188
189
    | [] -> rules
    | _ ->
      Datatype.String.Map.add
190
        "user-spec" "User-written ACSL specification" rules
Virgile Prevosto's avatar
Virgile Prevosto committed
191
192
  in
  let rules = make_rule_dictionary rules in
193
  let resources = Resources.create ~rules () in
Virgile Prevosto's avatar
Virgile Prevosto committed
194
  let results = results @ user_annot_results in
195
  let files = gen_files () in
196
  Run.create ~tool ~invocations ~results ~resources ~files ()
197
198

let generate () =
199
200
  let remarks = get_remarks () in
  let runs = [ gen_run remarks ] in
201
202
203
204
205
206
207
208
209
210
211
  let json = Schema.create ~runs () |> Schema.to_yojson in
  let file = Mdr_params.Output.get () in
  if file = "" then
    Log.print_on_output (fun fmt -> Yojson.Safe.pretty_print fmt json)
  else
    try
      Command.write_file file
        (fun out -> Yojson.Safe.pretty_to_channel ~std:true out json) ;
      Mdr_params.result "Report %s generated" file
    with Sys_error s ->
      Mdr_params.abort "Unable to generate %s (%s)" file s