Skip to content
Snippets Groups Projects
Commit ccb6c034 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

preparing manual addition of remarks into the report

parent e60a67fa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/markdown-report/Report_markdown.mli
+ 3
− 0
View file @ ccb6c034
...@@ -25,6 +25,7 @@ and block = block_element list ...@@ -25,6 +25,7 @@ and block = block_element list
and element = and element =
| Block of block | Block of block
| Raw of string (** non-markdown element, printed as-is. *) | Raw of string (** non-markdown element, printed as-is. *)
| Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *) | H1 of text * string option (** optional label. *)
| H2 of text * string option | H2 of text * string option
| H3 of text * string option | H3 of text * string option
...@@ -43,6 +44,8 @@ type pandoc_markdown = ...@@ -43,6 +44,8 @@ type pandoc_markdown =
val plain: string -> text val plain: string -> text
val plain_format: ('a, Format.formatter, unit, text) format4 -> 'a
(** gives a link whose text is the URL itself. *) (** gives a link whose text is the URL itself. *)
val plain_link: string -> inline val plain_link: string -> inline
......
src/plugins/markdown-report/markdown.ml
+ 6
− 0
View file @ ccb6c034
...@@ -24,6 +24,7 @@ and block = block_element list ...@@ -24,6 +24,7 @@ and block = block_element list
and element = and element =
| Block of block | Block of block
| Raw of string (** non-markdown element, printed as-is. *) | Raw of string (** non-markdown element, printed as-is. *)
| Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *) | H1 of text * string option (** optional label. *)
| H2 of text * string option | H2 of text * string option
| H3 of text * string option | H3 of text * string option
...@@ -42,6 +43,8 @@ type pandoc_markdown = ...@@ -42,6 +43,8 @@ type pandoc_markdown =
let plain s = [ Plain s] let plain s = [ Plain s]
let plain_format txt = Format.kasprintf plain txt
let plain_link s = Link ([Inline_code s],s) let plain_link s = Link ([Inline_code s],s)
let rec pp_inline fmt = let rec pp_inline fmt =
...@@ -168,6 +171,9 @@ and pp_quote fmt l = ...@@ -168,6 +171,9 @@ and pp_quote fmt l =
and pp_element fmt = function and pp_element fmt = function
| Block b -> Format.fprintf fmt "@[<v>%a@]@\n" pp_block b | Block b -> Format.fprintf fmt "@[<v>%a@]@\n" pp_block b
| Raw s -> Format.pp_print_string fmt s | 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 | 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 | 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 | H3(t,lab) -> Format.fprintf fmt "@[<h>### %a%a@]@\n" pp_text t pp_lab lab
......
src/plugins/markdown-report/markdown.mli
+ 3
− 0
View file @ ccb6c034
...@@ -24,6 +24,7 @@ and block = block_element list ...@@ -24,6 +24,7 @@ and block = block_element list
and element = and element =
| Block of block | Block of block
| Raw of string (** non-markdown element, printed as-is. *) | Raw of string (** non-markdown element, printed as-is. *)
| Comment of string (** markdown comment, printed <!-- like this --> *)
| H1 of text * string option (** optional label. *) | H1 of text * string option (** optional label. *)
| H2 of text * string option | H2 of text * string option
| H3 of text * string option | H3 of text * string option
...@@ -42,6 +43,8 @@ type pandoc_markdown = ...@@ -42,6 +43,8 @@ type pandoc_markdown =
val plain: string -> text val plain: string -> text
val plain_format: ('a, Format.formatter, unit, text) format4 -> 'a
(** gives a link whose text is the URL itself. *) (** gives a link whose text is the URL itself. *)
val plain_link: string -> inline val plain_link: string -> inline
......
src/plugins/markdown-report/md_gen.ml
+ 339
− 168
View file @ ccb6c034
open Cil_types
module Self = module Self =
Plugin.Register( Plugin.Register(
struct struct
...@@ -20,6 +22,26 @@ struct ...@@ -20,6 +22,26 @@ struct
let help = "generates an analysis report on the current project" let help = "generates an analysis report on the current project"
end) 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( module Authors = Self.String_list(
struct struct
let option_name = "-mdr-authors" let option_name = "-mdr-authors"
...@@ -58,6 +80,8 @@ let all_eva_domains = ...@@ -58,6 +80,8 @@ let all_eva_domains =
(e.g. `a[i]` when `i` is not precisely known by `Cvalue`)" (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 = let plural l s =
match l with match l with
| [] | [ _ ] -> s | [] | [ _ ] -> s
...@@ -74,23 +98,30 @@ let codelines lang pp code = ...@@ -74,23 +98,30 @@ let codelines lang pp code =
let lines = String.split_on_char '\n' s in let lines = String.split_on_char '\n' s in
Code_block (lang, lines) Code_block (lang, lines)
let section_domains () = let section_domains is_draft =
let l = get_eva_domains () in if is_draft then
Block Comment
(match l with "You can give more information about the choice of EVA domains"
| [] -> :: insert_marks
[Text else begin
(plain let l = get_eva_domains () in
"Only the base domain (`Cvalue`) has been used for the analysis")] [ Block
| _ -> (match l with
[Text | [] ->
(plain [Text
"In addition to the base domain (`Cvalue`), additional domains \ (plain
have been used by EVA"); "Only the base domain (`Cvalue`) \
DL l] has been used for the analysis")]
) | _ ->
[Text
let section_stubs () = (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 = let stubbed_kf =
List.concat List.concat
(List.map (List.map
...@@ -112,62 +143,105 @@ let section_stubs () = ...@@ -112,62 +143,105 @@ let section_stubs () =
(fun s -> String.length s <> 0 && s.[0] <> '@' && s.[0] <> '-') (fun s -> String.length s <> 0 && s.[0] <> '@' && s.[0] <> '-')
(fun s -> (fun s ->
let kf = Globals.Functions.find_by_name s in let kf = Globals.Functions.find_by_name s in
[ Text [Inline_code s; Plain "with the following specification"]; let content =
codelines "acsl" Printer.pp_funspec (Annotations.funspec kf)]) 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 l
in in
let describe_func kf = let describe_func kf =
[Text let name = Kernel_function.get_name kf in
[ Inline_code (Kernel_function.get_name kf); let loc = Kernel_function.get_location kf in
Plain let content =
(Format.asprintf if is_draft then insert_marks
"@[<h>(defined at %a)@]" else
Cil_datatype.Location.pretty [ Block
(Kernel_function.get_location kf)) [ 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 in
let content = let content =
if stubbed_kf <> [] then begin if stubbed_kf <> [] then begin
[ Text List.map describe_func stubbed_kf
(plain
"The following functions have been stubbed with a C definition");
UL (List.map describe_func stubbed_kf)]
end else [] end else []
in in
let content = let content = content @ use_spec in
if use_spec <> [] then begin let content = List.concat content in
[ Text
(plain
"The following functions have been stubbed with an \
ACSL specification");
UL use_spec]
end else content
in
if content = [] then 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 else
Block content content
let gen_context () = [ let gen_context is_draft =
H1 (plain "Context of the analysis", Some "context"); let context =
H2 (plain "Input files", Some "c-input"); if is_draft then
Block [ Comment "You can add here some overall introduction to the analysis"
Text :: insert_marks
(plain "The C source files (not including the headers `.h` files)" @ else []
plain "that have been considered during the analysis are the following:" in
); context @ [
UL (List.map (fun x -> [Text [ Inline_code x ]]) (Kernel.Files.get ())); H1 (plain "Context of the analysis", Some "context");
]; H2 (plain "Input files", Some "c-input")
H2 (plain "Configuration", Some "options"); ] @
Block [ (if is_draft then
Text Comment
(plain "The options that have been used for this analysis \ "You can add here some remarks about the set of files \
are the following.")]; that is considered by Frama-C"
H3 (plain "EVA Domains", Some "domains"); :: insert_marks
section_domains(); else [])
H3 (plain "Stubbed Functions", Some "stubs"); @ [
section_stubs() 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 make_events_table print_kind caption events =
let open Log in let open Log in
...@@ -189,18 +263,12 @@ let make_events_table print_kind caption events = ...@@ -189,18 +263,12 @@ let make_events_table print_kind caption events =
| Error -> "User error" | Error -> "User error"
| Failure -> "Internal error" | Failure -> "Internal error"
in 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 treat_event { evt_kind; evt_plugin; evt_source; evt_message } =
let evt_message = let evt_message =
Str.global_replace (Str.regexp_string "\n") " " evt_message Str.global_replace (Str.regexp_string "\n") " " evt_message
in in
let line = let line =
[ plain (pos evt_source); [ plain (string_of_pos_opt evt_source);
[ Plain evt_message; [ Plain evt_message;
Plain "(emitted by"; Plain "(emitted by";
Inline_code evt_plugin; Inline_code evt_plugin;
...@@ -221,7 +289,30 @@ let make_warnings_table warnings = ...@@ -221,7 +289,30 @@ let make_warnings_table warnings =
make_events_table make_events_table
false (plain (plural warnings "Warning" ^ " reported by Frama-C")) warnings 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 let open Log in
Messages.reset_once_flag (); Messages.reset_once_flag ();
let errs = ref [] in let errs = ref [] in
...@@ -242,112 +333,166 @@ let gen_section_warnings () = ...@@ -242,112 +333,166 @@ let gen_section_warnings () =
triggered without stopping everything. Applying the same treatment triggered without stopping everything. Applying the same treatment
to a Failure catched by an evil plugin cannot hurt. to a Failure catched by an evil plugin cannot hurt.
*) *)
[ H1 (plain "Errors in the analyzer", Some "errors"); let content =
Block [ if is_draft then
Text [Bold "Important warning:"; Comment "you can comment on each individual error" ::
Plain "Frama-C did not complete its execution successfully."; make_errors_list errs
Plain "Analysis results may be inaccurate."; else
Plain ((plural errs "The error") ^ " listed below must be"); [
Plain "fixed first before examining other warnings and alarms." Block [
]; Text [Bold "Important warning:";
]; Plain "Frama-C did not complete its execution ";
make_errors_table errs 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 [] end else []
in in
if Messages.nb_warnings () <> 0 then begin if Messages.nb_warnings () <> 0 then begin
error_section @ let content =
[ H1 (plain "Warnings", Some "warnings"); if is_draft then
Block [ Comment "you can comment on each individual error" ::
Text [ make_warnings_list warnings
Plain ("The table below lists the " ^ plural warnings "warning"); else
Plain "that have been emitted by the analyzer."; [
Plain "They might put additional assumptions on the relevance"; Block [
Plain "of the analysis results and must be reviewed carefully"; Text [
]; Plain ("The table below lists the " ^ plural warnings "warning");
Text [ Plain "that have been emitted by the analyzer.";
Plain "Note that this does not take into account emitted alarms:"; Plain "They might put additional assumptions on the relevance";
Plain "they are reported in"; Plain "of the analysis results and must be reviewed carefully";
Link (plain "in the next section", "#alarms") ];
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
] ]
]; in
make_warnings_table warnings error_section @
] H1 (plain "Warnings", Some "warnings") :: content
end else error_section end else error_section
let gen_section_alarms () = let gen_section_alarms is_draft =
let treat_alarm e kf s ~rank:_ alarm annot l = let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
let kind = plain (Alarms.get_name alarm) in 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 func = plain (Kernel_function.get_name kf) in
let loc = let loc = string_of_loc (Cil_datatype.Stmt.loc s) in
plain let loc_text = plain loc in
(Format.asprintf
"%a" Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc s))
in
let emitter = plain (Emitter.get_name e) in let emitter = plain (Emitter.get_name e) in
let descr = let descr = codelines "acsl" Printer.pp_code_annotation annot in
[ Inline_code(Format.asprintf "%a" Printer.pp_code_annotation annot)] 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 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 in
let content = Alarms.fold treat_alarm [] in let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
match content with match content with
| [] -> | [] ->
[ H1 (plain "Results of the analysis", Some "alarms"); let text_content =
Block [ if is_draft then
Text Comment "No alarm!" :: insert_marks
[ Bold "No alarm"; Plain "was found during the analysis"; else
Plain "Any execution starting from"; [
Inline_code (Kernel.MainFunction.get_function_name ()); Block [
Plain "in a context matching the one used for the analysis"; Text
Plain "will be immune from any undefined behavior." [ 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 -> | _ :: l ->
let alarm = if l = [] then "alarm" else "alarms" in let alarm = if l = [] then "alarm" else "alarms" in
let caption = let caption =
Some (plain (String.capitalize_ascii alarm ^ " emitted by the analysis")) Some (plain (String.capitalize_ascii alarm ^ " emitted by the analysis"))
in in
let header = let header =
[ plain "Kind", Center; [ plain "No", Center;
plain "Kind", Center;
plain "Emitter", Center; plain "Emitter", Center;
plain "Function", Left; plain "Function", Left;
plain "Location", Left; plain "Location", Left;
plain "Description", Left;
] ]
in in
[ H1 (plain "Results of the analysis", Some "alarms"); let text_content =
Block [ if is_draft then begin
Text sections
[ Plain ("The table below lists the " ^ alarm); end else
Plain "that have been emitted during the analysis."; [
Plain "Any execution starting from"; Block [
Inline_code (Kernel.MainFunction.get_function_name()); Text
Plain "in a context matching the one used for the analysis"; [ Plain ("The table below lists the " ^ alarm);
Plain "will be immune from any other undefined behavior." Plain "that have been emitted during the analysis.";
] Plain "Any execution starting from";
]; Inline_code (Kernel.MainFunction.get_function_name());
Table { content; caption; header } 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 () = let gen_section_callgraph is_draft =
[ H1 (plain "Flamegraph", Some "flamegraph"); let content =
Block [ if is_draft then
Text [ Comment
Plain "The image below shows the flamegraph ("; "flamegraph allow to visualize the functions and callstacks \
plain_link "http://www.brendangregg.com/flamegraphs.html"; whose analysis is the most costly."
Plain ") for the chosen entry point." :: 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")] ]
] ]
]; in
Block H1 (plain "Flamegraph", Some "flamegraph") :: content
[ Text [Image ("flamegraph", "../server.flamegraph.svg")] ]
]
let gen_alarms () = let gen_alarms is_draft =
gen_section_warnings () @ gen_section_warnings is_draft @
gen_section_alarms () @ gen_section_alarms is_draft @
gen_section_callgraph () gen_section_callgraph is_draft
let mk_date () = let mk_date () =
let tm = Unix.gmtime (Unix.time()) in let tm = Unix.gmtime (Unix.time()) in
...@@ -355,26 +500,52 @@ let mk_date () = ...@@ -355,26 +500,52 @@ let mk_date () =
(Printf.sprintf "%d-%02d-%02d" (Printf.sprintf "%d-%02d-%02d"
(1900 + tm.Unix.tm_year) (1 + tm.Unix.tm_mon) tm.Unix.tm_mday) (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 () = let main () =
if Generate.get () then begin if Gen_draft.get () then begin
let context = gen_context () in if Generate.get () then
let alarms = gen_alarms () in Self.warning
let doc = "-mdr-gen and -mdr-gen-draft can be activated at the \
{ title = plain "Frama-C Analysis Report"; same time. Only draft will be generated";
authors = List.map (fun x -> plain x) (Authors.get ()); gen_report true
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
end end
else if Generate.get () then gen_report false
let () = Db.Main.extend main let () = Db.Main.extend main
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment