SARIF output format

.gitignore

@@ -73,4 +73,6 @@ incremental_data/
 *.log
 
 # make relocatable
-relocatable/
+relocatable/
+
+*.sarif

src/framework/analyses.ml

@@ -268,6 +268,10 @@ struct
        iter insert (Lazy.force table);
        let t1 = Unix.gettimeofday () -. t in
        Printf.printf "Done in %fs!\n" t1 *)
+    | "sarif" ->
+      let open BatPrintf in
+      printf "Writing Sarif to file: %s\n%!" (get_string "outfile");
+      Yojson.Safe.pretty_to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list));
     | "json-messages" ->
       Yojson.Safe.pretty_to_channel ~std:true out (Messages.Table.to_yojson ())
     | "none" -> ()

src/maingoblint.ml

@@ -80,6 +80,12 @@ let option_spec_list =
     set_bool "g2html" true;
     set_string "result" "fast_xml"
   in
+  let configure_sarif () =
+    if (get_string "outfile" = "") then
+      set_string "outfile" "goblint.sarif";
+    set_bool "dbg.print_dead_code" true;
+    set_string "result" "sarif"
+  in
   let tmp_arg = ref "" in
   [ "-o"                   , Arg.String (set_string "outfile"), ""
   ; "-v"                   , Arg.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
@@ -99,6 +105,7 @@ let option_spec_list =
   ; "--tracelocs"          , add_int Tracing.tracelocs, ""
   ; "--help"               , Arg.Unit (fun _ -> print_help stdout),""
   ; "--html"               , Arg.Unit (fun _ -> configure_html ()),""
+  ; "--sarif"               , Arg.Unit (fun _ -> configure_sarif ()),""
   ; "--compare_runs"       , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto "compare_runs" (sprintf "['%s','%s']" !tmp_arg x))], ""
   ; "--oil"                , Arg.String oil, ""
   (*     ; "--tramp"              , Arg.String (set_string "ana.osek.tramp"), ""  *)

src/util/defaults.ml

@@ -301,7 +301,7 @@ let default_schema = {schema|
   , "justcil"         : {}
   , "justcfg"         : {}
   , "printstats"      : {}
-  , "verify"        : {}
+  , "verify"          : {}
   , "mainfun"         : {}
   , "exitfun"         : {}
   , "otherfun"        : {}

src/util/messageCategory.ml

@@ -179,6 +179,31 @@ let path_show e =
 
 let show x = String.concat " > " (path_show x)
 
+let behaviorName = function 
+  |Machine -> "Machine";
+  |Implementation -> "Implementation"
+  |Undefined u -> match u with 
+    |NullPointerDereference -> "NullPointerDereference"
+    |UseAfterFree -> "UseAfterFree"
+    | ArrayOutOfBounds aob -> match aob with 
+      | PastEnd -> "PastEnd"
+      | BeforeStart -> "BeforeStart" 
+      | Unknown -> "Unknown Aob"
+let categoryName = function 
+  | Assert -> "Assert" 
+
+  | Race -> "Race"
+  | Cast x -> "Cast" 
+  | Deadcode -> "Deadcode"
+  | Unknown -> "Unknown"
+  | Analyzer -> "Analyzer"
+
+  | Behavior x -> behaviorName x 
+  | Integer x -> match x with 
+    | Overflow -> "Overflow";
+    | DivByZero -> "DivByZero"
+
+
 let from_string_list (s: string list) =
   match s with
   | [] -> Unknown

src/util/sarif.ml

@@ -0,0 +1,157 @@
+(** The Sarif format is a standardised output format for static analysis tools. https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html *)
+open Prelude
+
+open SarifType
+open SarifRules
+
+module Region = SarifType.Region (* TODO: why is this needed if SarifType is opened? *)
+
+
+(*matches the Goblint severity to the Sarif property level.*)
+let severityToLevel (severity:Messages.Severity.t)= match severity with
+  | Error -> "error"
+  | Warning -> "warning"
+  | Info -> "note"
+  | Debug -> "none"
+  | Success -> "none"
+
+
+let createMessageObject (text:String.t) =
+  {
+    Message.text=text;
+  }
+(*A reportingDescriptor offers a lot of information about a Goblint rule *)
+let createReportingDescriptor categoryInformation =
+  {
+    ReportingDescriptor.ruleId=categoryInformation.ruleId;
+    ReportingDescriptor.ruleName=categoryInformation.name;
+    ReportingDescriptor.helpUri=categoryInformation.helpUri;
+    ReportingDescriptor.help=(createMessageObject categoryInformation.helpText);
+    ReportingDescriptor.shortDescription=(createMessageObject categoryInformation.shortDescription);
+    ReportingDescriptor.fullDescription=(createMessageObject categoryInformation.longDescription);
+  }
+
+let transformToReportingDescriptor (id:String.t)=
+  createReportingDescriptor  (getRuleInformation id)
+
+let (driverObject:ToolComponent.t) =
+  {
+    ToolComponent.name="Goblint";
+    ToolComponent.fullName= "Goblint static analyser";
+    ToolComponent.informationUri="https://goblint.in.tum.de/home";
+    ToolComponent.organization="TUM - i2 and UTartu - SWS";
+    ToolComponent.version=Version.goblint;
+    ToolComponent.rules=List.map transformToReportingDescriptor (List.map (fun rule -> rule.name) rules)
+  }
+let (toolObject:Tool.t) =
+  {
+    Tool.driver=driverObject;
+  }
+
+
+(*returns the Rule corresponding to a message entry *)
+let getCategoryInformationID (tags:Messages.Tags.t) =
+  let getCWE (tag:Messages.Tag.t) = match tag with
+    | CWE cwe-> Some cwe;
+    | Category cat -> None;
+  in
+  (* if a CWE is present only the CWE is used, since using multiple ones for the same result doesn' make sense.
+     If only Categorys are present, all of them are displayed.*)
+  match List.find_map_opt getCWE tags with
+  | Some cwe ->  string_of_int cwe;
+  | None -> match tags with
+    | [] -> ""
+    | x::xs -> match x with
+      |Category cat-> MessageCategory.categoryName cat
+      | CWE c-> "" (*this case should not be reachable *)
+
+
+let createArtifact (uri:string) =
+  {
+    Artifact.location={
+      ArtifactLocation.uri=uri;
+    }
+  }
+let createArtifactObject (uri:string) =
+  {
+    ArtifactLocation.uri=uri;
+  }
+let hasLocation (piece:Messages.Piece.t) = match  piece.loc with
+  |Some loc -> true
+  |None -> false
+(*should only be called after hasLocation*)
+let deOptionalizeLocation (piece:Messages.Piece.t)= match piece.loc with
+  | Some loc ->loc
+  | None -> assert false
+
+let createPhysicalLocationObject (piece:Messages.Piece.t) =
+  let createRegionObject (line,column)=
+    {
+      Region.startLine=line;
+      Region.startColumn=column;
+      Region.endLine=line+4;
+      Region.endColumn=column+4;
+    }
+  in
+  {
+    Location.physicalLocation={
+      PhysicalLocation.artifactLocation=  createArtifactObject  (deOptionalizeLocation piece).file;
+      PhysicalLocation.region=createRegionObject ((deOptionalizeLocation piece).line,(deOptionalizeLocation piece).column);
+    }
+  }
+
+
+let createLocationsObject (multiPiece:Messages.MultiPiece.t) = match multiPiece with
+  | Single piece ->List.map createPhysicalLocationObject (List.filter hasLocation  [piece]);
+  | Group {group_text = n; pieces = e} ->List.map createPhysicalLocationObject  (List.take 10 (List.filter hasLocation e))
+
+
+
+let createResult (message:Messages.Message.t) =
+  let getMessage (multiPiece:Messages.MultiPiece.t)=  match multiPiece with
+    | Single piece ->piece.text;
+    | Group {group_text = n; pieces = e} ->n
+  in
+  {
+    Result.ruleId=(getRuleInformation (getCategoryInformationID message.tags)).ruleId;
+    Result.level=severityToLevel message.severity;
+    Result.message=createMessageObject (getMessage message.multipiece);
+    Result.locations=createLocationsObject message.multipiece;
+  }
+
+let getFileLocation (multipiece:Messages.MultiPiece.t)=
+  let getFile (loc:Cil.location) =
+    loc.file
+  in
+  let toLocation = match multipiece with
+
+    | Single piece ->[deOptionalizeLocation piece];
+    | Group {group_text = n; pieces = e} ->
+      List.map deOptionalizeLocation  (List.filter hasLocation e);
+  in
+  List.map getFile toLocation
+
+let collectAllFileLocations (msgList:Messages.Message.t list)=
+  let getUris=
+    List.flatten (List.map (fun (msg:Messages.Message.t)-> getFileLocation msg.multipiece) msgList)
+  in
+  let uniques x xs = if List.mem x xs then xs else x::xs;
+  in
+  List.fold_right uniques getUris []
+let runObject msgList=
+  {
+    Run.invocations=[{
+        Invocation.commandLine=String.concat  ", " (BatArray.to_list BatSys.argv)  ;
+        Invocation.executionSuccessful=true;
+      }];
+    Run.artifacts= List.map createArtifact (collectAllFileLocations   msgList);
+    Run.tool=toolObject;
+    Run.defaultSourceLanguage="C";
+    Run.results=List.map createResult (List.take 5000 msgList);
+  }
+
+let sarifObject msgList={SarifLog.version="2.1.0";
+                         SarifLog.schema="https://schemastore.azurewebsites.net/schemas/json/sarif-2.1.0-rtm.5.json";
+                         SarifLog.runs=[runObject msgList] }
+
+let to_yojson  msgList=   [%to_yojson: SarifLog.t]  (sarifObject msgList)