Merge branch 'feature/andre/mdr-sarif-pretty' into 'master'

Feature/andre/mdr sarif pretty

See merge request frama-c/frama-c!2846

src/libraries/utils/filepath.ml

@@ -277,13 +277,19 @@ module Normalized = struct
     with _ -> false
 
   let to_base_uri name =
-    if is_relative name then None, skip_dot name
-    else begin
-      let p = insert cwd name in
-      let buf = Buffer.create 80 in
-      let res = add_uri_path buf p in
-      res, Buffer.contents buf
-    end
+    let p = insert cwd name in
+    let buf = Buffer.create 80 in
+    let res = add_uri_path buf p in
+    let uri =
+      Buffer.contents buf in
+    let uri =
+      try
+        if String.get uri 0 = '/' then
+          String.sub uri 1 (String.length uri - 1)
+        else uri
+      with Invalid_argument _ -> uri
+    in
+    res, uri
 end
 
 type position =

src/plugins/markdown-report/Makefile.in

@@ -39,7 +39,7 @@ PLUGIN_CMO:=\
 PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure share/acsl.xml
-PLUGIN_TESTS_DIRS:= eva
+PLUGIN_TESTS_DIRS:= eva sarif
 
 include $(FRAMAC_SHARE)/Makefile.dynamic
 

src/plugins/markdown-report/mdr_params.ml

@@ -112,3 +112,17 @@ module Stubs = String_list(
     let arg_name = "f1,...,fn"
     let help = "list of C files containing stub functions"
   end)
+
+module PrintLibc = True(
+  struct
+    let option_name = "-mdr-print-libc"
+    let help =
+      "when set (default), reports include information about libc elements."
+  end)
+
+module SarifDeterministic = False(
+  struct
+    let option_name = "-mdr-sarif-deterministic"
+    let help = "omits non-deterministic data from SARIF reports, such as \
+                absolute file URIs and timestamps."
+  end)

src/plugins/markdown-report/mdr_params.mli

@@ -45,3 +45,9 @@ module Date: Parameter_sig.String
 
 (** Value of [-mdr-stubs]. *)
 module Stubs: Parameter_sig.String_list
+
+(** Value of [-mdr-print-libc]. *)
+module PrintLibc: Parameter_sig.Bool
+
+(** Value of [-mdr-sarif-deterministic]. *)
+module SarifDeterministic: Parameter_sig.Bool

src/plugins/markdown-report/sarif.ml

@@ -98,10 +98,8 @@ module ArtifactLocation = struct
   let default = create ~uri:"" ()
 
   let of_loc loc =
-    let open Filepath in
-    (* by construction, we have an absolute path here, no need for uriBase *)
-    let uri = ((fst loc).pos_path :> string) in
-    create ~uri ()
+    let uriBaseId, uri = Filepath.(Normalized.to_base_uri (fst loc).pos_path) in
+    create ~uri ?uriBaseId ()
 end
 
 module ArtifactLocationDictionary = Json_dictionary(ArtifactLocation)
@@ -462,6 +460,7 @@ module Driver = struct
     semanticVersion: (string [@default ""]);
     fileVersion: (string [@default ""]);
     downloadUri: (string [@default ""]);
+    informationUri: (string [@default ""]);
     sarifLoggerVersion: (string [@default ""]);
     language: (string [@default "en-US"]);
     properties: (Properties.t [@default Properties.default]);
@@ -474,13 +473,14 @@ module Driver = struct
       ?(semanticVersion="")
       ?(fileVersion="")
       ?(downloadUri="")
+      ?(informationUri="")
       ?(sarifLoggerVersion="")
       ?(language="en-US")
       ?(properties=Properties.default)
       ()
     =
     { name; fullName; version; semanticVersion; fileVersion;
-      downloadUri; sarifLoggerVersion; language; properties }
+      downloadUri; informationUri; sarifLoggerVersion; language; properties }
 
   let default = create ~name:"" ()
 end

src/plugins/markdown-report/sarif_gen.ml

@@ -22,14 +22,20 @@
 
 open Sarif
 
-let frama_c_sarif =
+let frama_c_sarif () =
   let name = "frama-c" in
-  let version = Fc_config.version_and_codename in
-  let semanticVersion = Fc_config.version in
+  let version, semanticVersion =
+    if Mdr_params.SarifDeterministic.get () then
+      "0+omitted-for-deterministic-output", ""
+    else
+      Fc_config.version_and_codename, Fc_config.version
+  in
   let fullName = name ^ "-" ^ version in
   let downloadUri = "https://frama-c.com/download.html" in
+  let informationUri = "https://frama-c.com" in
   Tool.create
-    (Driver.create ~name ~version ~semanticVersion ~fullName ~downloadUri ())
+    (Driver.create ~name ~version ~semanticVersion ~fullName ~downloadUri
+       ~informationUri ())
 
 let get_remarks () =
   let f = Mdr_params.Remarks.get () in
@@ -53,6 +59,9 @@ module Analysis_cmdline =
 
 let gen_invocation () =
   let cl = Analysis_cmdline.get () in
+  (* The first argument is _always_ the binary name, but to avoid printing it
+     as an absolute path to binlevel.opt, we replace it with 'frama-c' *)
+  let cl = "frama-c" :: List.tl cl in
   let commandLine = String.concat " " cl in
   let arguments = List.tl cl in
   Invocation.create ~commandLine ~arguments ()
@@ -107,27 +116,51 @@ let make_message alarm annot remark =
   in
   Message.create ~text ~markdown ()
 
+let kf_is_in_libc kf =
+  let g = Kernel_function.get_global kf in
+  Cil.hasAttribute "fc_stdlib" (Cil_datatype.Global.attr g)
+
+let ip_is_in_libc ip =
+  match Property.get_kf ip with
+  | None ->
+    (* possibly an identified lemma; check its attributes *)
+    begin
+      match ip with
+      | IPAxiomatic {iax_attrs=attrs}
+      | IPLemma {il_attrs=attrs}
+      | IPAxiom {il_attrs=attrs} ->
+        Cil.hasAttribute "fc_stdlib" attrs
+      | _ ->
+        false
+    end
+  | Some kf ->
+    kf_is_in_libc kf
+
 let opt_physical_location_of_loc loc =
   if loc = Cil_datatype.Location.unknown then []
   else [ Location.of_loc loc ]
-
+(* Cil_types *)
 let gen_results remarks =
   let treat_alarm _e kf s ~rank:_ alarm annot (i, rules, content) =
-    let prop = Property.ip_of_code_annot_single kf s annot in
-    let ruleId = Alarms.get_name alarm in
-    let rules =
-      Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
-    in
-    let label = "Alarm-" ^ string_of_int i in
-    let kind = kind_of_status (Property_status.Feedback.get prop) in
-    let level = level_of_status (Property_status.Feedback.get prop) in
-    let remark = get_remark remarks label in
-    let message = make_message alarm annot remark in
-    let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
-    let res =
-      Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
-    in
-    (i+1, rules, res :: content)
+    if not (Mdr_params.PrintLibc.get ()) && kf_is_in_libc kf then
+      (* skip alarm in libc *)
+      (i, rules, content)
+    else
+      let prop = Property.ip_of_code_annot_single kf s annot in
+      let ruleId = Alarms.get_name alarm in
+      let rules =
+        Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
+      in
+      let label = "Alarm-" ^ string_of_int i in
+      let kind = kind_of_status (Property_status.Feedback.get prop) in
+      let level = level_of_status (Property_status.Feedback.get prop) in
+      let remark = get_remark remarks label in
+      let message = make_message alarm annot remark in
+      let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
+      let res =
+        Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
+      in
+      (i+1, rules, res :: content)
   in
   let _, rules, content =
     Alarms.fold treat_alarm (0, Datatype.String.Map.empty,[])
@@ -153,14 +186,18 @@ let gen_status ip =
 
 let gen_statuses () =
   let f ip content =
-    if is_alarm ip then content else (gen_status ip) :: content
+    let exclude =
+      is_alarm ip ||
+      (not (Mdr_params.PrintLibc.get ()) && ip_is_in_libc ip)
+    in
+    if exclude then content else (gen_status ip) :: content
   in
   List.rev (Property_status.fold f [])
 
 let gen_artifacts () =
   let add_src_file f =
-    let uri = (f:Filepath.Normalized.t :> string) in
-    let location = ArtifactLocation.create ~uri () in
+    let uriBaseId, uri = Filepath.Normalized.to_base_uri f in
+    let location = ArtifactLocation.create ~uri ?uriBaseId () in
     let roles = [ Role.analysisTarget ] in
     let mimeType = "text/x-csrc" in
     Artifact.create ~location ~roles ~mimeType ()
@@ -176,7 +213,7 @@ let add_rule id desc l =
 let make_taxonomies rules = Datatype.String.Map.fold add_rule rules []
 
 let gen_run remarks =
-  let tool = frama_c_sarif in
+  let tool = frama_c_sarif () in
   let name = "frama-c" in
   let invocations = [gen_invocation ()] in
   let rules, results = gen_results remarks in
@@ -192,7 +229,24 @@ let gen_run remarks =
   let taxonomies = [ToolComponent.create ~name ~rules ()] in
   let results = results @ user_annot_results in
   let artifacts = gen_artifacts () in
-  Run.create ~tool ~invocations ~results ~taxonomies ~artifacts ()
+  let uriBases = ("PWD", Sys.getcwd ()) :: Filepath.all_symbolic_dirs () in
+  let uriBasesJson =
+    List.fold_left (fun acc (name, dir) ->
+        let baseUri =
+          if Mdr_params.SarifDeterministic.get () then
+            "file:///omitted-for-deterministic-output/"
+          else  "file://" ^ dir ^ "/"
+        in
+        (name, `Assoc [("uri", `String baseUri)]) :: acc
+      ) [] uriBases
+  in
+  let originalUriBaseIds =
+    match ArtifactLocationDictionary.of_yojson (`Assoc uriBasesJson) with
+    | Ok x -> x
+    | Error s -> failwith s
+  in
+  Run.create ~tool ~invocations ~results ~taxonomies ~artifacts
+    ~originalUriBaseIds ()
 
 let generate () =
   let remarks = get_remarks () in

src/plugins/markdown-report/tests/sarif/libc.c

+/* run.config
+   CMD: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
+   LOG: with-libc.sarif
+   OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
+   LOG: without-libc.sarif
+   OPT: -mdr-no-print-libc -mdr-out @PTEST_DIR@/result/without-libc.sarif
+*/
+
+#include <string.h>
+
+int main() {
+  char *s = "hello world";
+  int n = strlen(s);
+  return n;
+}

src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle

+[kernel] Parsing tests/sarif/libc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 4 statements reached (out of 4): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     1 valid     0 unknown     0 invalid      1 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
+[mdr] Report tests/sarif/result/with-libc.sarif generated

src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle

+[kernel] Parsing tests/sarif/libc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 4 statements reached (out of 4): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     1 valid     0 unknown     0 invalid      1 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
+[mdr] Report tests/sarif/result/without-libc.sarif generated

src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif

+{
+  "$schema":
+    "https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.1.0-CSD.1/sarif-schema-2.1.0.json",
+  "version": "2.1.0",
+  "runs": [
+    {
+      "tool": {
+        "driver": {
+          "name": "frama-c",
+          "fullName": "frama-c-0+omitted-for-deterministic-output",
+          "version": "0+omitted-for-deterministic-output",
+          "downloadUri": "https://frama-c.com/download.html",
+          "informationUri": "https://frama-c.com"
+        }
+      },
+      "invocations": [
+        {
+          "commandLine":
+            "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
+          "arguments": [
+            "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
+            "-load-module", "eva,from,scope,markdown_report", "-eva",
+            "-eva-no-results", "-mdr-gen", "sarif",
+            "-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
+            "tests/sarif/result/without-libc.sarif"
+          ],
+          "exitCode": 0,
+          "executionSuccessful": true
+        }
+      ],
+      "originalUriBaseIds": {
+        "FRAMAC_SHARE": {
+          "uri": "file:///omitted-for-deterministic-output/"
+        },
+        "FRAMAC_LIB": { "uri": "file:///omitted-for-deterministic-output/" },
+        "FRAMAC_PLUGIN": {
+          "uri": "file:///omitted-for-deterministic-output/"
+        },
+        "PWD": { "uri": "file:///omitted-for-deterministic-output/" }
+      },
+      "artifacts": [
+        {
+          "location": { "uri": "tests/sarif/libc.c", "uriBaseId": "PWD" },
+          "roles": [ "analysisTarget" ],
+          "mimeType": "text/x-csrc"
+        }
+      ],
+      "results": [
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "specialization of valid_string_s at stmt 2."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "tests/sarif/libc.c",
+                  "uriBaseId": "PWD"
+                },
+                "region": {
+                  "startLine": 13,
+                  "startColumn": 10,
+                  "endLine": 13,
+                  "endColumn": 19,
+                  "byteLength": 9
+                }
+              }
+            }
+          ]
+        }
+      ],
+      "defaultSourceLanguage": "C",
+      "taxonomies": [
+        {
+          "name": "frama-c",
+          "rules": [
+            {
+              "id": "user-spec",
+              "shortDescription": {
+                "text": "User-written ACSL specification."
+              }
+            }
+          ],
+          "contents": [ "nonLocalizedData" ]
+        }
+      ]
+    }
+  ]
+}
\ No newline at end of file