Add SARIF output format support with comprehensive tests

Examples/SarifTest.boogie.st

@@ -0,0 +1,13 @@
+program Boogie;
+
+// Simple test program for SARIF output
+procedure AddPositive(x : int, y : int) returns (z : int)
+spec {
+  requires [x_positive]: (x > 0);
+  requires [y_positive]: (y > 0);
+  ensures [result_positive]: (z > 0);
+  ensures [result_sum]: (z == x + y);
+}
+{
+  z := x + y;
+};

Strata.lean

@@ -15,8 +15,12 @@ import Strata.DL.SMT.SMT
 import Strata.DL.Lambda.Lambda
 import Strata.DL.Imperative.Imperative
 
+/- Utilities -/
+import Strata.Util.Sarif
+
 /- Boogie -/
 import Strata.Languages.Boogie.StatementSemantics
+import Strata.Languages.Boogie.SarifOutput
 
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect

Strata/Languages/Boogie/Options.lean

@@ -13,6 +13,8 @@ structure Options where
   removeIrrelevantAxioms : Bool
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
+  /-- Output results in SARIF format -/
+  outputSarif : Bool
 
 def Options.default : Options := {
   verbose := true,
@@ -21,7 +23,8 @@ def Options.default : Options := {
   checkOnly := false,
   stopOnFirstError := false,
   removeIrrelevantAxioms := false,
-  solverTimeout := 10
+  solverTimeout := 10,
+  outputSarif := false
 }
 
 instance : Inhabited Options where

Strata/Languages/Boogie/SarifOutput.lean

@@ -0,0 +1,85 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Boogie.Verifier
+import Strata.Util.Sarif
+
+/-!
+# Boogie SARIF Output
+
+This module provides Boogie-specific conversion functions for SARIF output.
+-/
+
+namespace Boogie.Sarif
+
+open Strata.Sarif Strata.SMT
+
+/-! ## Boogie-Specific Conversion Functions -/
+
+/-- Convert Boogie Outcome to SARIF Level -/
+def outcomeToLevel : Outcome → Level
+  | .pass => .none
+  | .fail => .error
+  | .unknown => .warning
+  | .implementationError _ => .error
+
+/-- Convert Boogie Outcome to a descriptive message -/
+def outcomeToMessage (outcome : Outcome) (smtResult : SMT.Result) : String :=
+  match outcome with
+  | .pass => "Verification succeeded"
+  | .fail =>
+    match smtResult with
+    | .sat m =>
+      if m.isEmpty then
+        "Verification failed"
+      else
+        s!"Verification failed with counterexample: {Std.format m}"
+    | _ => "Verification failed"
+  | .unknown => "Verification result unknown (solver timeout or incomplete)"
+  | .implementationError msg => s!"Verification error: {msg}"
+
+/-- Extract location information from metadata -/
+def extractLocation (md : Imperative.MetaData Expression) : Option Location := do
+  let fileRangeElem ← md.findElem Imperative.MetaData.fileRange
+  match fileRangeElem.value with
+  | .fileRange fr =>
+    let uri := match fr.file with
+               | .file path => path
+    pure { uri, startLine := fr.start.line, startColumn := fr.start.column }
+  | _ => none
+
+/-- Convert a VCResult to a SARIF Result -/
+def vcResultToSarifResult (vcr : VCResult) : Strata.Sarif.Result :=
+  let ruleId := vcr.obligation.label
+  let level := outcomeToLevel vcr.result
+  let messageText := outcomeToMessage vcr.result vcr.smtResult
+  let message : Strata.Sarif.Message := { text := messageText }
+
+  let locations := match extractLocation vcr.obligation.metadata with
+    | some loc => #[locationToSarif loc]
+    | none => #[]
+
+  { ruleId, level, message, locations }
+
+/-- Convert VCResults to a SARIF document -/
+def vcResultsToSarif (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
+  let tool : Strata.Sarif.Tool := {
+    driver := {
+      name := "Strata",
+      version := "0.1.0",
+      informationUri := "https://github.com/strata-org/Strata"
+    }
+  }
+
+  let results := vcResults.map vcResultToSarifResult
+
+  let run : Strata.Sarif.Run := { tool, results }
+
+  { version := "2.1.0",
+    schema := "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json",
+    runs := #[run] }
+
+end Boogie.Sarif

Strata/Util/Sarif.lean

@@ -0,0 +1,142 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Lean.Data.Json
+
+/-!
+# SARIF Output
+
+This module provides support for outputting results in SARIF
+(Static Analysis Results Interchange Format) version 2.1.0.
+
+SARIF specification: https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html
+-/
+
+namespace Strata.Sarif
+
+open Lean (Json ToJson FromJson)
+
+/-! ## SARIF Data Structures -/
+
+/-- SARIF location representing a position in source code -/
+structure Location where
+  uri : String
+  startLine : Nat
+  startColumn : Nat
+  deriving Repr, ToJson, FromJson, BEq
+
+/-- SARIF artifact location representing a file URI -/
+structure ArtifactLocation where
+  uri : String
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF region representing a source code region with line and column information -/
+structure Region where
+  startLine : Nat
+  startColumn : Nat
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF physical location with region information -/
+structure PhysicalLocation where
+  artifactLocation : ArtifactLocation
+  region : Region
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF location wrapper -/
+structure SarifLocation where
+  physicalLocation : PhysicalLocation
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF message -/
+structure Message where
+  text : String
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF result level -/
+inductive Level where
+  | none     -- Verification passed
+  | note     -- Informational
+  | warning  -- Unknown result or potential issue
+  | error    -- Verification failed
+  deriving Repr, DecidableEq
+
+instance : ToString Level where
+  toString
+  | .none => "none"
+  | .note => "note"
+  | .warning => "warning"
+  | .error => "error"
+
+instance : ToJson Level where
+  toJson level := Json.str (toString level)
+
+instance : FromJson Level where
+  fromJson? j := do
+    let s ← j.getStr?
+    match s with
+    | "none" => pure .none
+    | "note" => pure .note
+    | "warning" => pure .warning
+    | "error" => pure .error
+    | _ => throw s!"Invalid SARIF level: {s}"
+
+/-- SARIF result representing a single verification result -/
+structure Result where
+  ruleId : String
+  level : Level
+  message : Message
+  locations : Array SarifLocation := #[]
+  deriving Repr, ToJson, FromJson
+
+instance : Inhabited Result where
+  default := { ruleId := "", level := .none, message := { text := "" } }
+
+/-- SARIF tool driver information -/
+structure Driver where
+  name : String
+  version : String := "0.1.0"
+  informationUri : String := "https://github.com/strata-org/Strata"
+  deriving Repr, ToJson, FromJson, Inhabited
+
+/-- SARIF tool information -/
+structure Tool where
+  driver : Driver
+  deriving Repr, ToJson, FromJson, Inhabited
+
+/-- SARIF run representing a single analysis run -/
+structure Run where
+  tool : Tool
+  results : Array Result
+  deriving Repr, ToJson, FromJson
+
+instance : Inhabited Run where
+  default := { tool := default, results := #[] }
+
+/-- Top-level SARIF document -/
+structure SarifDocument where
+  version : String := "2.1.0"
+  /-- Schema URI as specified by SARIF 2.1.0 -/
+  schema : String := "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json"
+  runs : Array Run
+  deriving Repr, ToJson, FromJson
+
+/-! ## Utility Functions -/
+
+/-- Convert a location to SARIF format -/
+def locationToSarif (loc : Location) : SarifLocation :=
+  let artifactLocation : ArtifactLocation := { uri := loc.uri }
+  let region : Region := { startLine := loc.startLine, startColumn := loc.startColumn }
+  { physicalLocation := { artifactLocation, region } }
+
+/-- Convert SARIF document to JSON string -/
+def toJsonString (sarif : SarifDocument) : String :=
+  Json.compress (ToJson.toJson sarif)
+
+/-- Convert SARIF document to pretty-printed JSON string -/
+def toPrettyJsonString (sarif : SarifDocument) : String :=
+  Json.pretty (ToJson.toJson sarif)
+
+end Strata.Sarif