Merge pull request #1752 from goblint/g2html-ocaml

Output g2html directly

Author: sim642

docs/user-guide/inspecting.md

@@ -1,10 +1,21 @@
 # Inspecting results
 
-## g2html
+## HTML
+1. Run Goblint with additional `--html` argument.
+2. Run `python3 -m http.server --directory result 8080`
+   or `npx http-server -c-1 result`.
+3. Inspect results at <http://localhost:8080/index.xml>.
+
+Modern browsers' security settings forbid some file access which is necessary for the HTML output to work, hence the need for serving the results via Python's `http.server` (or similar).
+
+## g2html (legacy)
+If there are problems with the above HTML output, the legacy g2html output (using an external Java component) is still possible.
+The frontend of the above HTML output is reused from g2html, so the two look the same (except for code highlighting).
+
 1. First time run: `make jar`.
-2. Run Goblint with additional `--html` argument.
+2. Run Goblint with additional `--set result g2html` arguments.
 3. Run `python3 -m http.server --directory result 8080`
-   or  `npx http-server -c-1 result`.
+   or `npx http-server -c-1 result`.
 4. Inspect results at <http://localhost:8080/index.xml>.
 
 Modern browsers' security settings forbid some file access which is necessary for g2html to work, hence the need for serving the results via Python's `http.server` (or similar).

dune-project

@@ -83,7 +83,8 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
   )
   (sites
     (share lib)
-    (share conf))
+    (share conf)
+    (share xslt))
 )
 
 ; (map_workspace_root false) ;uncomment to enable breakpoints

make.sh

@@ -74,7 +74,7 @@ rule() {
       }
     ;; setup)
       echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
-      echo "For the --html output you also need: javac, ant, dot (graphviz)"
+      echo "For the --html output you also need: graphviz and python3-pygments (optional)"
       echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup

src/common/framework/cfgTools.ml

@@ -654,12 +654,12 @@ let sprint_fundec_html_dot (module Cfg : CfgBidir) live fd =
   fprint_fundec_html_dot (module Cfg) live fd Format.str_formatter;
   Format.flush_str_formatter ()
 
-let dead_code_cfg (module FileCfg: MyCFG.FileCfg) live =
+let dead_code_cfg ~path (module FileCfg: MyCFG.FileCfg) live =
   iterGlobals FileCfg.file (fun glob ->
       match glob with
       | GFun (fd,loc) ->
         (* ignore (Printf.printf "fun: %s\n" fd.svar.vname); *)
-        let base_dir = GobSys.mkdir_or_exists_absolute (Fpath.v "cfgs") in
+        let base_dir = GobSys.mkdir_or_exists_absolute path in
         let c_file_name = Str.global_substitute (Str.regexp Filename.dir_sep) (fun _ -> "%2F") loc.file in
         let dot_file_name = fd.svar.vname^".dot" in
         let file_dir = GobSys.mkdir_or_exists_absolute Fpath.(base_dir / c_file_name) in

src/config/options.schema.json

@@ -81,7 +81,7 @@
       "description":
         "Result style: none, fast_xml, json, pretty, pretty-deterministic, json-messages, sarif.",
       "type": "string",
-      "enum": ["none", "fast_xml", "json", "pretty", "pretty-deterministic", "json-messages", "sarif"],
+      "enum": ["none", "fast_xml", "g2html", "xslt", "json", "pretty", "pretty-deterministic", "json-messages", "sarif"],
       "default": "none"
     },
     "solver": {
@@ -117,12 +117,6 @@
       "enum": ["auto", "always", "never"],
       "default": "auto"
     },
-    "g2html": {
-      "title": "g2html",
-      "description": "Run g2html.jar on the generated xml.",
-      "type": "boolean",
-      "default": false
-    },
     "save_run": {
       "title": "save_run",
       "description":

src/framework/analysisResult.ml

@@ -1,4 +1,4 @@
-(** Analysis result output. *)
+(** Analysis results. *)
 
 open GoblintCil
 open Pretty
@@ -32,164 +32,22 @@ sig
   val result_name: string
 end
 
-module Result (Range: Printable.S) (C: ResultConf) =
-struct
-  include BatHashtbl.Make (ResultNode)
-  type nonrec t = Range.t t (* specialize polymorphic type for Range values *)
-
-  let pretty () mapping =
-    let f key st dok =
-      dok ++ dprintf "%a ->@?  @[%a@]\n" ResultNode.pretty key Range.pretty st
-    in
-    let content () = fold f mapping nil in
-    let defline () = dprintf "OTHERS -> Not available\n" in
-    dprintf "@[Mapping {\n  @[%t%t@]}@]" content defline
-
-  let pretty_deterministic () mapping =
-    let bindings =
-      to_list mapping
-      |> List.sort [%ord: ResultNode.t * Range.t]
-    in
-    let f dok (key, st) =
-      dok ++ dprintf "%a ->@?  @[%a@]\n" ResultNode.pretty key Range.pretty st
-    in
-    let content () = List.fold_left f nil bindings in
-    let defline () = dprintf "OTHERS -> Not available\n" in
-    dprintf "@[Mapping {\n  @[%t%t@]}@]" content defline
+module type Result =
+sig
+  include ResultConf
+  module Range: Printable.S
+  module H: BatHashtbl.S with type key := ResultNode.t
+  include BatHashtbl.S with type 'a t := 'a H.t and type key := ResultNode.t
+  type t = Range.t H.t
+end
 
+module Result (Range: Printable.S) (C: ResultConf): Result with module Range = Range =
+struct
   include C
-
-  let printXml f xs =
-    let print_one n v =
-      (* Not using Node.location here to have updated locations in incremental analysis.
-         See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
-      let loc = UpdateCil.getLoc n in
-      BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\" endLine=\"%d\" endColumn=\"%d\" synthetic=\"%B\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column loc.endLine loc.endColumn loc.synthetic;
-      BatPrintf.fprintf f "%a</call>\n" Range.printXml v
-    in
-    iter print_one xs
-
-  let printJson f xs =
-    let print_one n v =
-      (* Not using Node.location here to have updated locations in incremental analysis.
-         See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
-      let loc = UpdateCil.getLoc n in
-      BatPrintf.fprintf f "{\n\"id\": \"%s\", \"file\": \"%s\", \"line\": \"%d\", \"byte\": \"%d\", \"column\": \"%d\", \"states\": %s\n},\n" (Node.show_id n) loc.file loc.line loc.byte loc.column (Yojson.Safe.to_string (Range.to_yojson v))
-    in
-    iter print_one xs
-
-  let printXmlWarning f () =
-    let one_text f Messages.Piece.{loc; text = m; _} =
-      match loc with
-      | Some loc ->
-        let l = Messages.Location.to_cil loc in
-        BatPrintf.fprintf f "\n<text file=\"%s\" line=\"%d\" column=\"%d\">%s</text>" l.file l.line l.column (XmlUtil.escape m)
-      | None ->
-        () (* TODO: not outputting warning without location *)
-    in
-    let one_w f (m: Messages.Message.t) = match m.multipiece with
-      | Single piece  -> one_text f piece
-      | Group {group_text = n; pieces = e; group_loc} ->
-        let group_loc_text = match group_loc with
-          | None -> ""
-          | Some group_loc -> GobPretty.sprintf " (%a)" CilType.Location.pretty (Messages.Location.to_cil group_loc)
-        in
-        BatPrintf.fprintf f "<group name=\"%s%s\">%a</group>\n" n group_loc_text (BatList.print ~first:"" ~last:"" ~sep:"" one_text) e
-    in
-    let one_w f x = BatPrintf.fprintf f "\n<warning>%a</warning>" one_w x in
-    List.iter (one_w f) !Messages.Table.messages_list
-
-  let output table gtable gtfxml (file: file) =
-    let out = Messages.get_out result_name !Messages.out in
-    match get_string "result" with
-    | "pretty" -> ignore (fprintf out "%a\n" pretty (Lazy.force table))
-    | "pretty-deterministic" -> ignore (fprintf out "%a\n" pretty_deterministic (Lazy.force table))
-    | "fast_xml" ->
-      let module SH = BatHashtbl.Make (Basetype.RawStrings) in
-      let file2funs = SH.create 100 in
-      let funs2node = SH.create 100 in
-      iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table);
-      iterGlobals file (function
-          | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname
-          | _ -> ()
-        );
-      let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in
-      let p_nodes f xs =
-        List.iter (BatPrintf.fprintf f "<node name=\"%a\"/>\n" p_node) xs
-      in
-      let p_funs f xs =
-        let one_fun n =
-          BatPrintf.fprintf f "<function name=\"%s\">\n%a</function>\n" n p_nodes (SH.find_all funs2node n)
-        in
-        List.iter one_fun xs
-      in
-      let write_file f fn =
-        Messages.xml_file_name := fn;
-        Logs.info "Writing xml to temp. file: %s" fn;
-        BatPrintf.fprintf f "<run>";
-        BatPrintf.fprintf f "<parameters>%s</parameters>" GobSys.command_line;
-        BatPrintf.fprintf f "<statistics>";
-        let timing_ppf = BatFormat.formatter_of_out_channel f in
-        Timing.Default.print timing_ppf;
-        Format.pp_print_flush timing_ppf ();
-        BatPrintf.fprintf f "</statistics>";
-        BatPrintf.fprintf f "<result>\n";
-        BatEnum.iter (fun b -> BatPrintf.fprintf f "<file name=\"%s\" path=\"%s\">\n%a</file>\n" (Filename.basename b) b p_funs (SH.find_all file2funs b)) (BatEnum.uniq @@ SH.keys file2funs); (* nosemgrep: batenum-module *)
-        BatPrintf.fprintf f "%a" printXml (Lazy.force table);
-        gtfxml f gtable;
-        printXmlWarning f ();
-        BatPrintf.fprintf f "</result></run>\n";
-        BatPrintf.fprintf f "%!"
-      in
-      if get_bool "g2html" then
-        BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file
-      else
-        let f = BatIO.output_channel out in
-        write_file f (get_string "outfile")
-    | "json" ->
-      let open BatPrintf in
-      let module SH = BatHashtbl.Make (Basetype.RawStrings) in
-      let file2funs = SH.create 100 in
-      let funs2node = SH.create 100 in
-      iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table);
-      iterGlobals file (function
-          | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname
-          | _ -> ()
-        );
-      let p_enum p f xs = BatEnum.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in (* nosemgrep: batenum-module *)
-      let p_list p f xs = BatList.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in
-      (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*)
-      (*let p_obj f xs = BatList.print ~first:"{\n  " ~last:"\n}" ~sep:",\n  " p_kv xs in*)
-      let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in
-      let p_fun f x = fprintf f "{\n  \"name\": \"%s\",\n  \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in
-      (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*)
-      let p_file f x = fprintf f "{\n  \"name\": \"%s\",\n  \"path\": \"%s\",\n  \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in
-      let write_file f fn =
-        Logs.info "Writing json to temp. file: %s" fn;
-        fprintf f "{\n  \"parameters\": \"%s\",\n  " GobSys.command_line;
-        fprintf f "\"files\": %a,\n  " (p_enum p_file) (SH.keys file2funs);
-        fprintf f "\"results\": [\n  %a\n]\n" printJson (Lazy.force table);
-        (*gtfxml f gtable;*)
-        (*printXmlWarning f ();*)
-        fprintf f "}\n";
-      in
-      if get_bool "g2html" then
-        BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file
-      else
-        let f = BatIO.output_channel out in
-        write_file f (get_string "outfile")
-    | "sarif" ->
-      Logs.result "Writing Sarif to file: %s" (get_string "outfile");
-      Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list));
-    | "json-messages" ->
-      let json = `Assoc [
-          ("files", Preprocessor.dependencies_to_yojson ());
-          ("messages", Messages.Table.to_yojson ());
-        ]
-      in
-      Yojson.Safe.to_channel ~std:true out json
-    | "none" -> ()
-    | s -> failwith @@ "Unsupported value for option `result`: "^s
+  module Range = Range
+  module H = BatHashtbl.Make (ResultNode)
+  include H
+  type t = Range.t H.t
 end
 
 module ResultType2 (S: Analyses.Spec) =

src/framework/analysisResultOutput.ml

@@ -0,0 +1,97 @@
+(** Analysis result output. *)
+
+open GoblintCil
+open Pretty
+open GobConfig
+open AnalysisResult
+
+module Make (Result: Result) =
+struct
+  open Result
+
+  let pretty () mapping =
+    let f key st dok =
+      dok ++ dprintf "%a ->@?  @[%a@]\n" ResultNode.pretty key Range.pretty st
+    in
+    let content () = fold f mapping nil in
+    let defline () = dprintf "OTHERS -> Not available\n" in
+    dprintf "@[Mapping {\n  @[%t%t@]}@]" content defline
+
+  let pretty_deterministic () mapping =
+    let bindings =
+      to_list mapping
+      |> List.sort [%ord: ResultNode.t * Range.t]
+    in
+    let f dok (key, st) =
+      dok ++ dprintf "%a ->@?  @[%a@]\n" ResultNode.pretty key Range.pretty st
+    in
+    let content () = List.fold_left f nil bindings in
+    let defline () = dprintf "OTHERS -> Not available\n" in
+    dprintf "@[Mapping {\n  @[%t%t@]}@]" content defline
+
+
+  let printJson f xs =
+    let print_one n v =
+      (* Not using Node.location here to have updated locations in incremental analysis.
+         See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
+      let loc = UpdateCil.getLoc n in
+      BatPrintf.fprintf f "{\n\"id\": \"%s\", \"file\": \"%s\", \"line\": \"%d\", \"byte\": \"%d\", \"column\": \"%d\", \"states\": %s\n},\n" (Node.show_id n) loc.file loc.line loc.byte loc.column (Yojson.Safe.to_string (Range.to_yojson v))
+    in
+    iter print_one xs
+
+
+  let output table live gtable gtfxml (module FileCfg: MyCFG.FileCfg) =
+    let file = FileCfg.file in
+    let out = Messages.get_out result_name !Messages.out in
+    match get_string "result" with
+    | "pretty" -> ignore (fprintf out "%a\n" pretty (Lazy.force table))
+    | "pretty-deterministic" -> ignore (fprintf out "%a\n" pretty_deterministic (Lazy.force table))
+    | "fast_xml"
+    | "g2html" ->
+      let module Output = XsltResultOutput.Make (Result) in
+      Output.output table live gtable gtfxml (module FileCfg)
+    | "xslt" ->
+      let module Output = XsltResultOutput.Make2 (Result) in
+      Output.output table live gtable gtfxml (module FileCfg)
+    | "json" ->
+      let open BatPrintf in
+      let module SH = BatHashtbl.Make (Basetype.RawStrings) in
+      let file2funs = SH.create 100 in
+      let funs2node = SH.create 100 in
+      iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table);
+      iterGlobals file (function
+          | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname
+          | _ -> ()
+        );
+      let p_enum p f xs = BatEnum.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in (* nosemgrep: batenum-module *)
+      let p_list p f xs = BatList.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in
+      (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*)
+      (*let p_obj f xs = BatList.print ~first:"{\n  " ~last:"\n}" ~sep:",\n  " p_kv xs in*)
+      let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in
+      let p_fun f x = fprintf f "{\n  \"name\": \"%s\",\n  \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in
+      (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*)
+      let p_file f x = fprintf f "{\n  \"name\": \"%s\",\n  \"path\": \"%s\",\n  \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in
+      let write_file f fn =
+        Logs.info "Writing json to temp. file: %s" fn;
+        fprintf f "{\n  \"parameters\": \"%s\",\n  " GobSys.command_line;
+        fprintf f "\"files\": %a,\n  " (p_enum p_file) (SH.keys file2funs);
+        fprintf f "\"results\": [\n  %a\n]\n" printJson (Lazy.force table);
+        (*gtfxml f gtable;*)
+        (*printXmlWarning f ();*)
+        fprintf f "}\n";
+      in
+      let f = BatIO.output_channel out in
+      write_file f (get_string "outfile")
+    | "sarif" ->
+      Logs.result "Writing Sarif to file: %s" (get_string "outfile");
+      Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list));
+    | "json-messages" ->
+      let json = `Assoc [
+          ("files", Preprocessor.dependencies_to_yojson ());
+          ("messages", Messages.Table.to_yojson ());
+        ]
+      in
+      Yojson.Safe.to_channel ~std:true out json
+    | "none" -> ()
+    | s -> failwith @@ "Unsupported value for option `result`: "^s
+end

src/framework/control.ml

@@ -102,6 +102,7 @@ struct
   module LT = SetDomain.HeadlessSet (RT)
   (* Analysis result structure---a hashtable from program points to [LT] *)
   module Result = AnalysisResult.Result (LT) (struct let result_name = "analysis" end)
+  module ResultOutput = AnalysisResultOutput.Make (Result)
 
   module Query = ResultQuery.Query (SpecSys)
 
@@ -760,7 +761,7 @@ struct
     in
 
     if get_bool "exp.cfgdot" then
-      CfgTools.dead_code_cfg (module FileCfg) liveness;
+      CfgTools.dead_code_cfg ~path:(Fpath.v "cfgs") (module FileCfg) liveness;
 
     let warn_global g v =
       (* Logs.debug "warn_global %a %a" EQSys.GVar.pretty_trace g EQSys.G.pretty v; *)
@@ -840,7 +841,7 @@ struct
     if get_string "result" <> "none" then Logs.debug "Generating output: %s" (get_string "result");
 
     Messages.finalize ();
-    Timing.wrap "result output" (Result.output (lazy local_xml) gh make_global_fast_xml) file
+    Timing.wrap "result output" (ResultOutput.output (lazy local_xml) liveness gh make_global_fast_xml) (module FileCfg)
 end
 
 (* This function was originally a part of the [AnalyzeCFG] module, but