md_gen.ml 20.4 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
open Cil_types
24
25
open Markdown

26
27
28
29
30
31
32
33
34
type env =
  { is_draft: bool;
    remarks: Markdown.element list Datatype.String.Map.t; }

let insert_remark_opt env anchor placeholder =
  try Datatype.String.Map.find anchor env.remarks with Not_found -> placeholder

let insert_remark env anchor = insert_remark_opt env anchor []

35
36
37
38
39
40
41
(* apparently, pandoc, or at least its latex output,
   does not like anchors beginning with _ *)
let sanitize_anchor s =
  if s = "" then "a"
  else if s.[0] = '_' then "a" ^ s
  else s

42
43
44
45
let insert_marks env anchor =
  Comment "BEGIN_REMARK"
  :: insert_remark env anchor
  @ [Comment "END_REMARK"]
46

47
48
49
50
51
52
let plural l s =
  match l with
  | [] | [ _ ] -> s
  | _::_::_ -> s ^ "s"

let get_eva_domains () =
53
54
55
56
  let eva_domains = Eva.Value_parameters.enabled_domains () in
  let domains = List.filter (fun (name, _) -> name <> "cvalue") eva_domains in
  let aux (name, descr) = (plain "domain" @ bold name), plain descr in
  List.map aux domains
57

58
59
60
61
62
63
let section_domains env =
  let anchor = "domains" in
  let head = H3 (plain "EVA Domains", Some anchor) in
  if env.is_draft then
    head
    :: Comment "You can give more information about the choice of EVA domains"
64
    :: insert_marks env anchor
65
66
  else begin
    let l = get_eva_domains () in
67
68
    head
    :: Block
Virgile Prevosto's avatar
Virgile Prevosto committed
69
70
71
72
      (match l with
       | [] ->
         [Text
            (plain
73
               "Only the base domain (`cvalue`) \
Virgile Prevosto's avatar
Virgile Prevosto committed
74
75
76
77
                has been used for the analysis")]
       | _ ->
         [Text
            (plain
78
               "In addition to the base domain (`cvalue`), additional \
Virgile Prevosto's avatar
Virgile Prevosto committed
79
80
81
                domains have been used by EVA");
          DL l]
      )
82
    :: insert_remark env anchor
83
84
  end

85
let section_stubs env =
86
87
88
  let stubbed_kf =
    List.concat
      (List.map
89
         (fun f ->
90
91
            let filename = Filepath.Normalized.of_string f in
            Globals.FileIndex.get_functions ~declarations:false filename)
92
         (Mdr_params.Stubs.get ())
93
94
      )
  in
95
  let stubbed_kf = List.filter Kernel_function.is_definition stubbed_kf in
96
  let opt = Dynamic.Parameter.String.get "-eva-use-spec" () in
97
98
99
100
101
102
103
104
105
106
107
  let l = String.split_on_char ',' opt in
  let use_spec =
    Extlib.filter_map
      (* The option can include categories in Frama-C's List/Set/Map sense,
         which begins with a '@'. In particular, @default is included by
         default. Theoretically, there could also be some '-' to suppress
         the inclusion of a function
      *)
      (fun s -> String.length s <> 0 && s.[0] <> '@' && s.[0] <> '-')
      (fun s ->
         let kf = Globals.Functions.find_by_name s in
108
         let anchor = sanitize_anchor s in
109
         let content =
110
           if env.is_draft then insert_marks env anchor
111
112
113
           else
             let intro = Markdown.text @@ Markdown.format
                 "`%s` has the following specification" s in
114
             let funspec = Markdown.codeblock ~lang:"acsl" "%a"
115
116
                 Printer.pp_funspec (Annotations.funspec kf) in
             Block ( intro @ funspec ) :: insert_remark env anchor
117
         in
118
         H4 (code s, Some anchor) :: content)
119
120
121
      l
  in
  let describe_func kf =
122
    let name = Kernel_function.get_name kf in
123
    let anchor = sanitize_anchor name in
124
125
    let loc = Kernel_function.get_location kf in
    let content =
126
      if env.is_draft then insert_marks env anchor
127
      else
128
129
130
        let intro = Markdown.text @@ Markdown.format
            "`%s` @[<h>is defined at %a@]"
            name Cil_datatype.Location.pretty loc in
131
        let fundecl = Markdown.codeblock ~lang:"c" "%a"
132
133
            Printer.pp_global (GFun (Kernel_function.get_definition kf,loc)) in
        Block ( intro @ fundecl ) :: insert_remark env anchor
134
    in
135
    H4 (code name, Some anchor) :: content
136
137
138
  in
  let content =
    if stubbed_kf <> [] then begin
139
      List.map describe_func stubbed_kf
140
141
    end else []
  in
142
143
  let content = content @ use_spec in
  let content = List.concat content in
144
  if content = [] then
145
    if env.is_draft then
146
      [ Comment "No stubs have been used" ]
147
148
    else
      [ Block [Text (plain "No stubs have been used for this analysis")]]
149
  else
150
151
    content

152
153
154
let get_files () =
  let dir_table = Datatype.String.Hashtbl.create 17 in
  let add_entry f =
155
    let f = Filepath.Normalized.to_pretty_string f in
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
    let dir = Filename.dirname f in
    let base = Filename.basename f in
    let suf =
      try
        let i = String.rindex base '.' in
        String.sub base i (String.length base - i)
      with Not_found -> ""
    in
    let entries =
      try Datatype.String.Hashtbl.find dir_table dir
      with Not_found -> Datatype.String.Map.empty
    in
    let subentries =
      try Datatype.String.Map.find suf entries
      with Not_found -> Datatype.String.Set.empty
    in
    Datatype.String.(
      Hashtbl.replace
        dir_table dir (Map.add suf (Set.add base subentries) entries))
  in
  List.iter add_entry (Kernel.Files.get());
  let treat_subentry dir dir_files suf files l =
    let dir_files =
      List.fold_left
        (fun acc s ->
           if Filename.check_suffix s suf then Datatype.String.Set.add s acc
           else acc)
        Datatype.String.Set.empty dir_files
    in
    if Datatype.String.Set.subset dir_files files then
      (dir ^ "/*" ^ suf) :: l
    else
      Datatype.String.Set.elements files @ l
  in
  let treat_entry dir map l =
    try
      let dir_files = Array.to_list (Sys.readdir dir) in
      Datatype.String.Map.fold (treat_subentry dir dir_files) map l
    with Sys_error s ->
      Mdr_params.warning "Unable to find directory %s: %s" dir s;
      Datatype.String.Map.fold
        (fun _ s l -> Datatype.String.Set.elements s @ l) map l
  in
  Datatype.String.Hashtbl.fold treat_entry dir_table []

201
202
203
204
205
206
207
let gen_inputs env =
  let anchor = "c-input" in
  let prelude =
    if env.is_draft then
      Comment
        "You can add here some remarks about the set of files \
         that is considered by Frama-C"
208
      :: insert_marks env anchor
Virgile Prevosto's avatar
Virgile Prevosto committed
209
210
    else
      insert_remark env anchor
211
  in
212
213
  H2 (plain "Input files", Some anchor)
  :: prelude
214
215
216
217
218
219
220
  @ [
    Block [
      Text
        (plain "The C source files (not including the headers `.h` files)" @
         plain "that have been considered during the analysis \
                are the following:"
        );
221
      UL (List.map (fun x -> text @@ code x) (get_files()));
222
223
224
225
226
227
228
229
230
    ]]

let gen_config env =
  let anchor = "options" in
  let header = H2 (plain "Configuration", Some anchor) in
  let content =
    if env.is_draft then
      Comment
        "You can add here some remarks about the options used for the analysis"
231
      :: insert_marks env anchor
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
    else begin
      let placeholder = [
        Block [
          Text
            (plain "The options that have been used for this analysis \
                    are the following.")]]
      in insert_remark_opt env anchor placeholder
    end
  in
  header :: content

let gen_context env =
  let context =
    let anchor = "intro" in
    let header = H1 (plain "Introduction", Some anchor) in
    if env.is_draft then
      header
      :: Comment "You can add here some overall introduction to the analysis"
250
      :: insert_marks env anchor
251
252
253
254
255
256
257
258
259
260
261
    else begin
      match insert_remark env anchor with
      | [] -> []
      | (_::_) as l -> header :: l
    end
  in
  context @
  H1 (plain "Context of the analysis", Some "context")
  :: gen_inputs env
  @ gen_config env
  @ section_domains env
262
  @ H3 (plain "Stubbed Functions", Some "stubs")
263
    :: (
Virgile Prevosto's avatar
Virgile Prevosto committed
264
265
266
267
268
      if env.is_draft then
        Comment
          "You can add here general comments about the stubs that have been used"
        :: insert_marks env "stubs"
      else insert_remark env "stubs")
269
  @ section_stubs env
270

271
272
273
274
275
276
277
278
let gen_coverage env =
  let anchor = "coverage" in
  let header = H1 (plain "Coverage", Some anchor) in
  let content = Eva_coverage.md_gen () in
  let content =
    if env.is_draft then
      content @
      Comment "You can comment on the coverage obtained by EVA"
279
      :: insert_marks env anchor
280
281
282
283
284
    else
      content @ insert_remark env anchor
  in
  header :: content

285
let string_of_pos pos = Format.asprintf "%a" Filepath.pp_pos pos
286
287
288
289
290
291
292

let string_of_pos_opt =
  function
  | None -> "Global"
  | Some pos -> string_of_pos pos

let string_of_loc (l1, _) = string_of_pos l1
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318

let make_events_table print_kind caption events =
  let open Log in
  let caption = Some caption in
  let header =
    [
      plain "Location", Left;
      plain "Description", Left;
    ]
  in
  let header =
    if print_kind then (plain "Kind", Center) :: header else header
  in
  let kind = function
    | Result -> "Result"
    | Feedback -> "Feedback"
    | Debug -> "Debug"
    | Warning -> "Warning"
    | Error -> "User error"
    | Failure -> "Internal error"
  in
  let treat_event { evt_kind; evt_plugin; evt_source; evt_message } =
    let evt_message =
      Str.global_replace (Str.regexp_string "\n") " " evt_message
    in
    let line =
319
      [ plain (string_of_pos_opt evt_source);
320
        format "`%s` (emitted by `%s`)" evt_message evt_plugin ]
321
322
323
324
325
326
327
328
329
330
331
332
333
334
    in
    if print_kind then plain (kind evt_kind) :: line else line
  in
  let content = List.fold_left (fun l evt -> treat_event evt :: l) [] events in
  Table { caption; header; content }

let make_errors_table errs =
  make_events_table true
    (plain (plural errs "Error" ^  " reported by Frama-C")) errs

let make_warnings_table warnings =
  make_events_table
    false (plain (plural warnings "Warning" ^ " reported by Frama-C")) warnings

335
let section_event is_err env nb event =
336
337
338
339
340
341
342
343
  let open Log in
  let title =
    Format.asprintf "@[<h>%s %d (%s)@]"
      (if is_err then "Error" else "Warning")
      nb
      (string_of_pos_opt event.evt_source)
  in
  let lab =
344
345
346
347
    Format.asprintf "@[<h>%s-%d@]" (if is_err then "err" else "warn") nb
  in
  let content =
    if env.is_draft then
348
      insert_marks env lab
349
    else insert_remark env lab
350
  in
351
  H2 (plain title, Some lab)
352
353
  :: Block (
    (text @@ plain "Message:") @
354
    codeblock "[%s] %s" event.evt_plugin event.evt_message
355
  )
356
  :: content
357

358
359
let make_events_list is_err env l =
  List.concat (List.mapi (section_event is_err env) l)
360
361
362
363
364

let make_errors_list = make_events_list true

let make_warnings_list = make_events_list false

365
let gen_section_warnings env =
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
  let open Log in
  Messages.reset_once_flag ();
  let errs = ref [] in
  let warnings = ref [] in
  let add_event evt =
    match evt.evt_kind with
    | Error | Failure -> errs:= evt :: !errs
    | Warning -> warnings := evt :: !warnings
    | _ -> ()
  in
  Messages.iter add_event;
  let errs = !errs in
  let warnings = !warnings in
  let error_section =
    if Messages.nb_errors () <> 0 then begin
      (* Failure are supposed to stop the analyses right away, so that no
         report will be generated. On the other hand, Error messages can be
         triggered without stopping everything. Applying the same treatment
         to a Failure catched by an evil plugin cannot hurt.
      *)
386
387
388
      let prelude =
        if env.is_draft then
          [ Comment "you can comment on each individual error" ]
389
390
        else
          [
391
392
393
394
395
396
397
398
            Block ( text @@ glue [
                bold "Important warning:";
                plain "Frama-C did not complete its execution ";
                plain "successfully. Analysis results may be inaccurate.";
                plain ((plural errs "The error") ^ " listed below must be");
                plain "fixed first before examining other ";
                plain "warnings and alarms."
              ] ) ;
399
400
401
            make_errors_table errs
          ]
      in
402
403
      H1 (plain "Errors in the analyzer", Some "errors")
      :: prelude
Virgile Prevosto's avatar
Virgile Prevosto committed
404
      @ make_errors_list env (List.rev errs)
405
406
407
    end else []
  in
  if Messages.nb_warnings () <> 0 then begin
408
409
410
    let prelude =
      if env.is_draft then
        [Comment "you can comment on each individual error"]
411
      else
412
413
414
415
        [Block (
            (text @@ glue [
                plain ("The table below lists the " ^ plural warnings "warning");
                plain "that have been emitted by the analyzer.";
416
417
                plain "They might put additional assumptions on the relevance";
                plain "of the analysis results and must be reviewed carefully";
418
419
420
421
422
423
424
425
              ]) @
            (text @@ glue [
                plain "Note that this does not take into account emitted alarms:";
                plain "they are reported in";
                link ~text:(plain "the next section") ~name:"alarms" ()
              ])
          );
         make_warnings_table warnings ]
426
427
    in
    error_section @
428
429
    H1 (plain "Warnings", Some "warnings")
    :: prelude
Virgile Prevosto's avatar
Virgile Prevosto committed
430
    @ make_warnings_list env (List.rev warnings)
431
432
  end else error_section

433
let gen_section_alarms env =
434
435
  let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
    let label = "Alarm-" ^ string_of_int i in
436
    let link = link ~text:(format "%d" i) ~name:label () in
437
438
439
    let kind = code @@ Alarms.get_name alarm in
    let func = code @@ Kernel_function.get_name kf in
    let loc = string_of_loc @@ Cil_datatype.Stmt.loc s in
440
    let loc_text = plain loc in
441
    let emitter = code (Emitter.get_name e) in
442
    let descr = codeblock ~lang:"acsl" "%a" Printer.pp_code_annotation annot in
443
    let sec_title = format "Alarm %d at %s" i loc in
444
    let sec_content =
445
      if env.is_draft then
446
        Block descr :: insert_marks env label
447
      else
448
        Block
449
450
451
452
453
          ( (text @@ glue [
                plain "The following ACSL assertion must hold to avoid" ;
                plain (Alarms.get_description alarm |> String.lowercase_ascii) ;
                format "(undefined behavior)."
              ])
454
            @ descr )
455
        :: insert_remark env label
456
    in
457
458
    (i+1,
     sec @ H2 (sec_title, Some label) :: sec_content,
459
     [ link; kind; emitter; func; loc_text ] :: content)
460
  in
461
  let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
462
  let content = List.rev content in
463
464
  match content with
  | [] ->
465
    let anchor = "alarms" in
466
    let text_content =
467
      if env.is_draft then
468
        Comment "No alarm!" :: insert_marks env anchor
469
      else
470
471
472
473
474
475
476
        Block (text @@ glue [
            bold "No alarm"; plain "was found during the analysis";
            plain "Any execution starting from";
            code (Kernel.MainFunction.get_function_name ());
            plain "in a context matching the one used for the analysis";
            plain "will be immune from any undefined behavior."
          ])
477
        :: insert_remark env anchor
478
    in
479
    H1 (plain "Results of the analysis", Some anchor) :: text_content
480
481
482
483
484
485
  | _ :: l ->
    let alarm = if l = [] then "alarm" else "alarms" in
    let caption =
      Some (plain (String.capitalize_ascii alarm ^ " emitted by the analysis"))
    in
    let header =
486
487
      [ plain "No", Center;
        plain "Kind", Center;
488
489
490
491
492
        plain "Emitter", Center;
        plain "Function", Left;
        plain "Location", Left;
      ]
    in
493
    let text_content =
494
      if env.is_draft then begin
495
        sections
496
      end else begin
497
498
499
500
501
502
503
504
505
506
        Block (text @@ glue [
            plain ("The table below lists the " ^ alarm);
            plain "that have been emitted during the analysis.";
            plain "Any execution starting from";
            code (Kernel.MainFunction.get_function_name());
            plain "in a context matching the one used for the analysis";
            plain "will be immune from any other undefined behavior.";
            plain "More information on each individual alarm is";
            plain "given in the remainder of this section"
          ]) ::
507
508
509
        Table { content; caption; header } ::
        sections
      end
510
511
    in
    H1 (plain "Results of the analysis", Some "alarms") :: text_content
512

513
let gen_section_callgraph env =
Florent Kirchner's avatar
Florent Kirchner committed
514
515
516
  let f = Mdr_params.FlameGraph.get () in
  if f = "" then []
  else begin
517
    let anchor = "flamegraph" in
Florent Kirchner's avatar
Florent Kirchner committed
518
    let content =
519
      if env.is_draft then
Florent Kirchner's avatar
Florent Kirchner committed
520
        Comment
521
522
          "A flamegraph provides a visualization of the functions and \
           callstacks whose analysis is the most costly."
523
        :: insert_marks env anchor
Florent Kirchner's avatar
Florent Kirchner committed
524
      else
525
526
527
528
529
530
531
        par (
          plain "The image below shows the flamegraph (" @
          url "http://www.brendangregg.com/flamegraphs.html" @
          plain ") for the chosen entry point."
        )
        @ par (image ~alt:"Flamegraph visualization." ~file:f)
        @ insert_remark env anchor
Florent Kirchner's avatar
Florent Kirchner committed
532
    in
533
    H1 (plain "Flamegraph", Some anchor) :: content
Florent Kirchner's avatar
Florent Kirchner committed
534
  end
535

536
537
538
539
540
541
let gen_section_postlude env =
  let anchor = "conclusion" in
  let header = H1 (plain "Conclusion", Some anchor) in
  if env.is_draft then
    header ::
    Comment "You can put here some concluding remarks"
542
    :: insert_marks env anchor
543
544
545
546
547
  else begin
    match insert_remark env anchor with
    | [] -> []
    | (_::_) as l -> header :: l
  end
548

549
550
551
552
553
let gen_alarms env =
  gen_section_warnings env @
  gen_section_alarms env @
  gen_section_callgraph env @
  gen_section_postlude env
554

555
let mk_remarks is_draft =
556
  let f = Mdr_params.Remarks.get () in
557
  if f <> "" then Parse_remarks.get_remarks f
558
  else if is_draft then begin
559
560
561
562
563
564
565
    let f = Mdr_params.Output.get() in
    if Sys.file_exists f then begin
      Mdr_params.feedback
        "Re-using pre-existing remarks in draft file %s" f;
      Parse_remarks.get_remarks f
    end else Datatype.String.Map.empty
  end else  Datatype.String.Map.empty
566

567
let gen_report ~draft:is_draft () =
568
  let remarks = mk_remarks is_draft in
569
570
  let env = { remarks; is_draft } in
  let context = gen_context env in
571
  let coverage = gen_coverage env in
572
  let alarms = gen_alarms env in
Virgile Prevosto's avatar
Virgile Prevosto committed
573
  let title = Mdr_params.Title.get () in
574
  let title =
Virgile Prevosto's avatar
Virgile Prevosto committed
575
576
577
578
579
580
    if title = "" then begin
      if is_draft then
        plain "Draft report"
      else
        plain "Frama-C Analysis Report"
    end else plain title
581
  in
582
  let authors = List.map (fun x -> plain x) (Mdr_params.Authors.get ()) in
583
584
585
  let date = match Mdr_params.Date.get () with
    | "" -> None
    | s -> Some (plain s) in
586
  let elements = context @ coverage @ alarms in
587
588
589
590
591
  let elements =
    if is_draft then
      Comment
        "This file contains additional remarks that will be added to \
         automatically generated content by Frama-C's Markdown-report plugin. \
592
593
         For any section of the document, you can write pandoc markdown \
         content between the BEGIN and END comments. In addition, the plug-in \
594
595
596
         will consider any \\<!-- INCLUDE file.md --\\> comment (without backslashes) \
         as a directive to include the content of file.md in the corresponding \
         section. \
597
         Please don't alter the structure \
598
599
600
601
602
         of the document as it is used by the plugin to associate content to \
         the relevant section."
      :: elements
    else elements
  in
603
  let elements =
Virgile Prevosto's avatar
Virgile Prevosto committed
604
605
606
    Raw [ "\\let\\underscore\\_" ;
          "\\renewcommand{\\_}{\\discretionary{\\underscore}{}{\\underscore}}"]
    :: elements
607
  in
608
  let doc = Markdown.pandoc ~title ~authors ?date elements in
609
  let file = Mdr_params.Output.get() in
610
  try
611
612
    Command.print_file file (fun fmt -> Markdown.pp_pandoc fmt doc) ;
    Mdr_params.result "Report %s generated" file
613
  with Sys_error s ->
614
    Mdr_params.warning
615
      "Unable to open %s for writing (%s). No report generated" file s