From ccb6c0341ebb0fd1a66a47d29a644a24679a100a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 3 Oct 2017 19:07:10 +0200
Subject: [PATCH] preparing manual addition of remarks into the report
---
.../markdown-report/Report_markdown.mli | 3 +
src/plugins/markdown-report/markdown.ml | 6 +
src/plugins/markdown-report/markdown.mli | 3 +
src/plugins/markdown-report/md_gen.ml | 507 ++++++++++++------
4 files changed, 351 insertions(+), 168 deletions(-)
diff --git a/src/plugins/markdown-report/Report_markdown.mli b/src/plugins/markdown-report/Report_markdown.mli
index c5b9481ff9d..528de49a885 100644
--- a/src/plugins/markdown-report/Report_markdown.mli
+++ b/src/plugins/markdown-report/Report_markdown.mli
@@ -25,6 +25,7 @@ and block = block_element list
and element =
| Block of block
| Raw of string (** non-markdown element, printed as-is. *)
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *)
| H2 of text * string option
| H3 of text * string option
@@ -43,6 +44,8 @@ type pandoc_markdown =
val plain: string -> text
+val plain_format: ('a, Format.formatter, unit, text) format4 -> 'a
+
(** gives a link whose text is the URL itself. *)
val plain_link: string -> inline
diff --git a/src/plugins/markdown-report/markdown.ml b/src/plugins/markdown-report/markdown.ml
index 19a1f503277..3dc4823cc70 100644
--- a/src/plugins/markdown-report/markdown.ml
+++ b/src/plugins/markdown-report/markdown.ml
@@ -24,6 +24,7 @@ and block = block_element list
and element =
| Block of block
| Raw of string (** non-markdown element, printed as-is. *)
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *)
| H2 of text * string option
| H3 of text * string option
@@ -42,6 +43,8 @@ type pandoc_markdown =
let plain s = [ Plain s]
+let plain_format txt = Format.kasprintf plain txt
+
let plain_link s = Link ([Inline_code s],s)
let rec pp_inline fmt =
@@ -168,6 +171,9 @@ and pp_quote fmt l =
and pp_element fmt = function
| Block b -> Format.fprintf fmt "@[<v>%a@]@\n" pp_block b
| Raw s -> Format.pp_print_string fmt s
+ | Comment s ->
+ Format.fprintf fmt
+ "@[<hv>@[<hv 5><!-- %a@]@ -->@]@\n" Format.pp_print_text s
| H1(t,lab) -> Format.fprintf fmt "@[<h># %a%a@]@\n" pp_text t pp_lab lab
| H2(t,lab) -> Format.fprintf fmt "@[<h>## %a%a@]@\n" pp_text t pp_lab lab
| H3(t,lab) -> Format.fprintf fmt "@[<h>### %a%a@]@\n" pp_text t pp_lab lab
diff --git a/src/plugins/markdown-report/markdown.mli b/src/plugins/markdown-report/markdown.mli
index e8a0a8c797b..1cedad28699 100644
--- a/src/plugins/markdown-report/markdown.mli
+++ b/src/plugins/markdown-report/markdown.mli
@@ -24,6 +24,7 @@ and block = block_element list
and element =
| Block of block
| Raw of string (** non-markdown element, printed as-is. *)
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *)
| H2 of text * string option
| H3 of text * string option
@@ -42,6 +43,8 @@ type pandoc_markdown =
val plain: string -> text
+val plain_format: ('a, Format.formatter, unit, text) format4 -> 'a
+
(** gives a link whose text is the URL itself. *)
val plain_link: string -> inline
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index d2fff1bc627..f8a9ba52de6 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -1,3 +1,5 @@
+open Cil_types
+
module Self =
Plugin.Register(
struct
@@ -20,6 +22,26 @@ struct
let help = "generates an analysis report on the current project"
end)
+module Gen_draft = Self.False(
+ struct
+ let option_name = "-mdr-gen-draft"
+ let help =
+ "instead of a full report, generates an empty draft \
+ in a format suitable for -mdr-add-remarks"
+ end)
+
+module Remarks = Self.Empty_string(
+struct
+ let option_name = "-mdr-remarks"
+ let arg_name = "f"
+ let help =
+ "reads <f> to add additional remarks to various sections of the report. \
+ must be in a format compatible with the file produced by -mdr-gen-draft. \
+ Remarks themselves must be written in pandoc's markdown, although this is \
+ not enforced by the plug-in."
+end
+)
+
module Authors = Self.String_list(
struct
let option_name = "-mdr-authors"
@@ -58,6 +80,8 @@ let all_eva_domains =
(e.g. `a[i]` when `i` is not precisely known by `Cvalue`)"
]
+let insert_marks = [ Comment "BEGIN_REMARK"; Comment "END_REMARK" ]
+
let plural l s =
match l with
| [] | [ _ ] -> s
@@ -74,23 +98,30 @@ let codelines lang pp code =
let lines = String.split_on_char '\n' s in
Code_block (lang, lines)
-let section_domains () =
- let l = get_eva_domains () in
- Block
- (match l with
- | [] ->
- [Text
- (plain
- "Only the base domain (`Cvalue`) has been used for the analysis")]
- | _ ->
- [Text
- (plain
- "In addition to the base domain (`Cvalue`), additional domains \
- have been used by EVA");
- DL l]
- )
-
-let section_stubs () =
+let section_domains is_draft =
+ if is_draft then
+ Comment
+ "You can give more information about the choice of EVA domains"
+ :: insert_marks
+ else begin
+ let l = get_eva_domains () in
+ [ Block
+ (match l with
+ | [] ->
+ [Text
+ (plain
+ "Only the base domain (`Cvalue`) \
+ has been used for the analysis")]
+ | _ ->
+ [Text
+ (plain
+ "In addition to the base domain (`Cvalue`), additional \
+ domains have been used by EVA");
+ DL l]
+ )]
+ end
+
+let section_stubs is_draft =
let stubbed_kf =
List.concat
(List.map
@@ -112,62 +143,105 @@ let section_stubs () =
(fun s -> String.length s <> 0 && s.[0] <> '@' && s.[0] <> '-')
(fun s ->
let kf = Globals.Functions.find_by_name s in
- [ Text [Inline_code s; Plain "with the following specification"];
- codelines "acsl" Printer.pp_funspec (Annotations.funspec kf)])
+ let content =
+ if is_draft then insert_marks
+ else
+ [ Block
+ [ Text
+ [Inline_code s; Plain "has the following specification"];
+ codelines
+ "acsl" Printer.pp_funspec (Annotations.funspec kf)]]
+ in
+ H4 ([Inline_code s], Some s) :: content)
l
in
let describe_func kf =
- [Text
- [ Inline_code (Kernel_function.get_name kf);
- Plain
- (Format.asprintf
- "@[<h>(defined at %a)@]"
- Cil_datatype.Location.pretty
- (Kernel_function.get_location kf))
- ]]
+ let name = Kernel_function.get_name kf in
+ let loc = Kernel_function.get_location kf in
+ let content =
+ if is_draft then insert_marks
+ else
+ [ Block
+ [ Text
+ (Inline_code name ::
+ plain_format
+ "@[<h>is defined at %a@]" Cil_datatype.Location.pretty loc);
+ codelines "c"
+ Printer.pp_global
+ (GFun (Kernel_function.get_definition kf,loc))
+ ]
+ ]
+ in
+ H4 ([Inline_code name], Some name) :: content
in
let content =
if stubbed_kf <> [] then begin
- [ Text
- (plain
- "The following functions have been stubbed with a C definition");
- UL (List.map describe_func stubbed_kf)]
+ List.map describe_func stubbed_kf
end else []
in
- let content =
- if use_spec <> [] then begin
- [ Text
- (plain
- "The following functions have been stubbed with an \
- ACSL specification");
- UL use_spec]
- end else content
- in
+ let content = content @ use_spec in
+ let content = List.concat content in
if content = [] then
- Block [Text (plain "No stubs have been used for this analysis")]
+ if is_draft then
+ Comment "No stubs have been used" :: insert_marks
+ else
+ [ Block [Text (plain "No stubs have been used for this analysis")]]
else
- Block content
-
-let gen_context () = [
- H1 (plain "Context of the analysis", Some "context");
- H2 (plain "Input files", Some "c-input");
- Block [
- Text
- (plain "The C source files (not including the headers `.h` files)" @
- plain "that have been considered during the analysis are the following:"
- );
- UL (List.map (fun x -> [Text [ Inline_code x ]]) (Kernel.Files.get ()));
- ];
- H2 (plain "Configuration", Some "options");
- Block [
- Text
- (plain "The options that have been used for this analysis \
- are the following.")];
- H3 (plain "EVA Domains", Some "domains");
- section_domains();
- H3 (plain "Stubbed Functions", Some "stubs");
- section_stubs()
-]
+ content
+
+let gen_context is_draft =
+ let context =
+ if is_draft then
+ Comment "You can add here some overall introduction to the analysis"
+ :: insert_marks
+ else []
+ in
+ context @ [
+ H1 (plain "Context of the analysis", Some "context");
+ H2 (plain "Input files", Some "c-input")
+ ] @
+ (if is_draft then
+ Comment
+ "You can add here some remarks about the set of files \
+ that is considered by Frama-C"
+ :: insert_marks
+ else [])
+ @ [
+ Block [
+ Text
+ (plain "The C source files (not including the headers `.h` files)" @
+ plain "that have been considered during the analysis \
+ are the following:"
+ );
+ UL (List.map (fun x -> [Text [ Inline_code x ]]) (Kernel.Files.get ()));
+ ];
+ H2 (plain "Configuration", Some "options");
+ Block [
+ Text
+ (plain "The options that have been used for this analysis \
+ are the following.")]
+ ] @
+ (if is_draft then
+ Comment
+ "You can add here some remarks about the options used for the analysis"
+ :: insert_marks
+ else [])
+ @
+ H3 (plain "EVA Domains", Some "domains")
+ :: section_domains is_draft
+ @ H3 (plain "Stubbed Functions", Some "stubs")
+ :: section_stubs is_draft
+
+let string_of_pos pos =
+ Format.asprintf
+ "%s:%d" (Filename.basename pos.Lexing.pos_fname) pos.Lexing.pos_lnum
+
+let string_of_pos_opt =
+ function
+ | None -> "Global"
+ | Some pos -> string_of_pos pos
+
+let string_of_loc (l1, _) = string_of_pos l1
let make_events_table print_kind caption events =
let open Log in
@@ -189,18 +263,12 @@ let make_events_table print_kind caption events =
| Error -> "User error"
| Failure -> "Internal error"
in
- let pos = function
- | None -> "Global"
- | Some pos ->
- Format.asprintf
- "%s:%d" (Filename.basename pos.Lexing.pos_fname) pos.Lexing.pos_lnum
- 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 =
- [ plain (pos evt_source);
+ [ plain (string_of_pos_opt evt_source);
[ Plain evt_message;
Plain "(emitted by";
Inline_code evt_plugin;
@@ -221,7 +289,30 @@ let make_warnings_table warnings =
make_events_table
false (plain (plural warnings "Warning" ^ " reported by Frama-C")) warnings
-let gen_section_warnings () =
+let section_event is_err nb event =
+ 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 =
+ Some
+ (Format.asprintf "@[<h>%s-%d@]" (if is_err then "err" else "warn") nb)
+ in
+ [ H2 (plain title, lab);
+ Block [ Text (plain "message text is"); Text (plain event.evt_message) ]]
+ @ insert_marks
+
+let make_events_list is_err l =
+ List.concat (List.mapi (section_event is_err) l)
+
+let make_errors_list = make_events_list true
+
+let make_warnings_list = make_events_list false
+
+let gen_section_warnings is_draft =
let open Log in
Messages.reset_once_flag ();
let errs = ref [] in
@@ -242,112 +333,166 @@ let gen_section_warnings () =
triggered without stopping everything. Applying the same treatment
to a Failure catched by an evil plugin cannot hurt.
*)
- [ H1 (plain "Errors in the analyzer", Some "errors");
- Block [
- Text [Bold "Important warning:";
- Plain "Frama-C did not complete its execution successfully.";
- Plain "Analysis results may be inaccurate.";
- Plain ((plural errs "The error") ^ " listed below must be");
- Plain "fixed first before examining other warnings and alarms."
- ];
- ];
- make_errors_table errs
- ]
+ let content =
+ if is_draft then
+ Comment "you can comment on each individual error" ::
+ make_errors_list errs
+ else
+ [
+ Block [
+ Text [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."
+ ];
+ ];
+ make_errors_table errs
+ ]
+ in
+ H1 (plain "Errors in the analyzer", Some "errors") :: content
end else []
in
if Messages.nb_warnings () <> 0 then begin
- error_section @
- [ H1 (plain "Warnings", Some "warnings");
- Block [
- Text [
- Plain ("The table below lists the " ^ plural warnings "warning");
- Plain "that have been emitted by the analyzer.";
- Plain "They might put additional assumptions on the relevance";
- Plain "of the analysis results and must be reviewed carefully";
- ];
- Text [
- Plain "Note that this does not take into account emitted alarms:";
- Plain "they are reported in";
- Link (plain "in the next section", "#alarms")
+ let content =
+ if is_draft then
+ Comment "you can comment on each individual error" ::
+ make_warnings_list warnings
+ else
+ [
+ Block [
+ Text [
+ Plain ("The table below lists the " ^ plural warnings "warning");
+ Plain "that have been emitted by the analyzer.";
+ Plain "They might put additional assumptions on the relevance";
+ Plain "of the analysis results and must be reviewed carefully";
+ ];
+ Text [
+ Plain "Note that this does not take into account emitted alarms:";
+ Plain "they are reported in";
+ Link (plain "in the next section", "#alarms")
+ ]
+ ];
+ make_warnings_table warnings
]
- ];
- make_warnings_table warnings
- ]
+ in
+ error_section @
+ H1 (plain "Warnings", Some "warnings") :: content
end else error_section
-let gen_section_alarms () =
- let treat_alarm e kf s ~rank:_ alarm annot l =
+let gen_section_alarms is_draft =
+ let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
let kind = plain (Alarms.get_name alarm) in
+ let label = "Alarm-" ^ string_of_int i in
+ let link = [Link (plain_format "%d" i, "#"^label)] in
let func = plain (Kernel_function.get_name kf) in
- let loc =
- plain
- (Format.asprintf
- "%a" Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc s))
- in
+ let loc = string_of_loc (Cil_datatype.Stmt.loc s) in
+ let loc_text = plain loc in
let emitter = plain (Emitter.get_name e) in
- let descr =
- [ Inline_code(Format.asprintf "%a" Printer.pp_code_annotation annot)]
+ let descr = codelines "acsl" Printer.pp_code_annotation annot in
+ let sec_title = plain_format "Alarm %d at %s" i loc in
+ let sec_content =
+ if is_draft then
+ Block [ descr ] :: insert_marks
+ else
+ [
+ Block
+ [
+ Text
+ (plain
+ "The following ACSL assertion must hold to avoid \
+ and undefined behavior ("
+ @ kind @ plain ")");
+ descr
+ ]
+ ]
in
- [ kind; emitter; func; loc; descr ] :: l
+ (i+1,
+ sec @ H2 (sec_title, Some label) :: sec_content,
+ [ link; kind; emitter; func; loc_text ] :: content)
in
- let content = Alarms.fold treat_alarm [] in
+ let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
match content with
| [] ->
- [ H1 (plain "Results of the analysis", Some "alarms");
- Block [
- Text
- [ Bold "No alarm"; Plain "was found during the analysis";
- Plain "Any execution starting from";
- Inline_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."
+ let text_content =
+ if is_draft then
+ Comment "No alarm!" :: insert_marks
+ else
+ [
+ Block [
+ Text
+ [ Bold "No alarm"; Plain "was found during the analysis";
+ Plain "Any execution starting from";
+ Inline_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."
+ ]
]
- ]
- ]
+ ]
+ in
+ H1 (plain "Results of the analysis", Some "alarms") :: text_content
| _ :: 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 =
- [ plain "Kind", Center;
+ [ plain "No", Center;
+ plain "Kind", Center;
plain "Emitter", Center;
plain "Function", Left;
plain "Location", Left;
- plain "Description", Left;
]
in
- [ H1 (plain "Results of the analysis", Some "alarms");
- Block [
- Text
- [ Plain ("The table below lists the " ^ alarm);
- Plain "that have been emitted during the analysis.";
- Plain "Any execution starting from";
- Inline_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."
- ]
- ];
- Table { content; caption; header }
- ]
+ let text_content =
+ if is_draft then begin
+ sections
+ end else
+ [
+ Block [
+ Text
+ [ Plain ("The table below lists the " ^ alarm);
+ Plain "that have been emitted during the analysis.";
+ Plain "Any execution starting from";
+ Inline_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"
+ ]
+ ];
+ Table { content; caption; header }
+ ]
+ in
+ H1 (plain "Results of the analysis", Some "alarms") :: text_content
-let gen_section_callgraph () =
- [ H1 (plain "Flamegraph", Some "flamegraph");
- Block [
- Text [
- Plain "The image below shows the flamegraph (";
- plain_link "http://www.brendangregg.com/flamegraphs.html";
- Plain ") for the chosen entry point."
+let gen_section_callgraph is_draft =
+ let content =
+ if is_draft then
+ Comment
+ "flamegraph allow to visualize the functions and callstacks \
+ whose analysis is the most costly."
+ :: insert_marks
+ else
+ [
+ Block [
+ Text [
+ Plain "The image below shows the flamegraph (";
+ plain_link "http://www.brendangregg.com/flamegraphs.html";
+ Plain ") for the chosen entry point."
+ ]
+ ];
+ Block
+ [ Text [Image ("flamegraph", "../server.flamegraph.svg")] ]
]
- ];
- Block
- [ Text [Image ("flamegraph", "../server.flamegraph.svg")] ]
- ]
+ in
+ H1 (plain "Flamegraph", Some "flamegraph") :: content
-let gen_alarms () =
- gen_section_warnings () @
- gen_section_alarms () @
- gen_section_callgraph ()
+let gen_alarms is_draft =
+ gen_section_warnings is_draft @
+ gen_section_alarms is_draft @
+ gen_section_callgraph is_draft
let mk_date () =
let tm = Unix.gmtime (Unix.time()) in
@@ -355,26 +500,52 @@ let mk_date () =
(Printf.sprintf "%d-%02d-%02d"
(1900 + tm.Unix.tm_year) (1 + tm.Unix.tm_mon) tm.Unix.tm_mday)
+let mk_remarks () =
+ let f = Remarks.get () in
+ if f <> "" then failwith "writeme"
+ else Datatype.String.Map.empty
+
+let gen_report is_draft =
+ let _remarks = mk_remarks () in
+ let context = gen_context is_draft in
+ let alarms = gen_alarms is_draft in
+ let title =
+ if is_draft then plain "Frama-C Analysis Report" else plain "Draft report"
+ in
+ let authors = List.map (fun x -> plain x) (Authors.get ()) in
+ let date = mk_date () in
+ let elements = context @ alarms in
+ 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. \
+ For any section of the document, you can write markdown content \
+ between the BEGIN and END comments. Please don't alter the structure \
+ of the document as it is used by the plugin to associate content to \
+ the relevant section."
+ :: elements
+ else elements
+ in
+ let doc = { title; authors; date; elements;} in
+ try
+ let out = open_out (Output.get()) in
+ let fmt = Format.formatter_of_out_channel out in
+ Markdown.pp_pandoc fmt doc;
+ close_out out
+ with Sys_error s ->
+ Self.warning
+ "Unable to open %s for writing (%s). No report will be generated"
+ (Output.get()) s
+
let main () =
- if Generate.get () then begin
- let context = gen_context () in
- let alarms = gen_alarms () in
- let doc =
- { title = plain "Frama-C Analysis Report";
- authors = List.map (fun x -> plain x) (Authors.get ());
- date = mk_date ();
- elements = context @ alarms
- }
- in
- try
- let out = open_out (Output.get()) in
- let fmt = Format.formatter_of_out_channel out in
- Markdown.pp_pandoc fmt doc;
- close_out out
- with Sys_error s ->
- Self.warning
- "Unable to open %s for writing (%s). No report will be generated"
- (Output.get()) s
+ if Gen_draft.get () then begin
+ if Generate.get () then
+ Self.warning
+ "-mdr-gen and -mdr-gen-draft can be activated at the \
+ same time. Only draft will be generated";
+ gen_report true
end
+ else if Generate.get () then gen_report false
let () = Db.Main.extend main
--
GitLab