From 5c431843dc9960826cc3103987b86af6ab8ae8c0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 13:13:41 +0100 Subject: [PATCH 1/8] Add SARIF output format support with comprehensive tests Adds support for outputting verification results in the SARIF (Static Analysis Results Interchange Format) v2.1.0 JSON format via a new output module with complete data structures and conversion functions for transforming VCResults to SARIF format. Command-line options (`--sarif` and `--output-format=sarif`) enable SARIF output generation. --- Examples/SarifTest.boogie.st | 13 + Strata.lean | 1 + Strata/Languages/Boogie/SarifOutput.lean | 223 +++++++++++++++ .../Languages/Boogie/SarifOutputTests.lean | 255 ++++++++++++++++++ StrataVerify.lean | 52 ++-- 5 files changed, 529 insertions(+), 15 deletions(-) create mode 100644 Examples/SarifTest.boogie.st create mode 100644 Strata/Languages/Boogie/SarifOutput.lean create mode 100644 StrataTest/Languages/Boogie/SarifOutputTests.lean diff --git a/Examples/SarifTest.boogie.st b/Examples/SarifTest.boogie.st new file mode 100644 index 000000000..f7270b1da --- /dev/null +++ b/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; +}; diff --git a/Strata.lean b/Strata.lean index 5c5225eef..20bd5d204 100644 --- a/Strata.lean +++ b/Strata.lean @@ -17,6 +17,7 @@ import Strata.DL.Imperative.Imperative /- Boogie -/ import Strata.Languages.Boogie.StatementSemantics +import Strata.Languages.Boogie.SarifOutput /- Code Transforms -/ import Strata.Transform.CallElimCorrect diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean new file mode 100644 index 000000000..ec8e3d377 --- /dev/null +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -0,0 +1,223 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Boogie.Verifier +import Lean.Data.Json + +/-! +# SARIF Output + +This module provides support for outputting verification 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 Boogie.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/tautschnig/strata-private" + deriving Repr, ToJson, FromJson + +instance : Inhabited Driver where + default := { name := "" } + +/-- SARIF tool information -/ +structure Tool where + driver : Driver + deriving Repr, ToJson, FromJson + +instance : Inhabited Tool where + default := { driver := default } + +/-- 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 + +/-! ## Conversion Functions -/ + +/-- Convert Boogie Result to SARIF Level -/ +def resultToLevel : Boogie.Result → Level + | .unsat => .none -- Verification passed + | .sat _ => .error -- Verification failed (counterexample found) + | .unknown => .warning -- Solver could not determine + | .err _ => .error -- Error during verification + +/-- Convert Boogie Result to a descriptive message -/ +def resultToMessage : Boogie.Result → String + | .unsat => "Verification succeeded" + | .sat cex => + if cex.isEmpty then + "Verification failed" + else + s!"Verification failed with counterexample: {Std.format cex}" + | .unknown => "Verification result unknown (solver timeout or incomplete)" + | .err msg => s!"Verification error: {msg}" + +/-- Extract location information from metadata -/ +def extractLocation (md : Imperative.MetaData Expression) : Option Location := do + let file ← md.findElem Imperative.MetaData.fileLabel + let line ← md.findElem Imperative.MetaData.startLineLabel + let col ← md.findElem Imperative.MetaData.startColumnLabel + + let uri? := match file.value with + | .msg m => some m + | _ => none + + let startLine? := match line.value with + | .msg s => s.toNat? + | _ => none + + let startColumn? := match col.value with + | .msg s => s.toNat? + | _ => none + + match uri?, startLine?, startColumn? with + | some uri, some startLine, some startColumn => pure { uri, startLine, startColumn } + | some uri, some startLine, none => pure { uri, startLine, startColumn := 1 } + | some uri, none, some startColumn => pure { uri, startLine := 1, startColumn } + | some uri, none, none => pure { uri, startLine := 1, startColumn := 1 } + | none, _, _ => none + +/-- 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 a VCResult to a SARIF Result -/ +def vcResultToSarifResult (vcr : VCResult) : Result := + let ruleId := vcr.obligation.label + let level := resultToLevel vcr.result + let messageText := resultToMessage vcr.result + let message : 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) : SarifDocument := + let tool : Tool := { + driver := { + name := "Strata", + version := "0.1.0", + informationUri := "https://github.com/tautschnig/strata-private" + } + } + + let results := vcResults.map vcResultToSarifResult + + let run : 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] } + +/-- 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 Boogie.Sarif diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean new file mode 100644 index 000000000..62740eff8 --- /dev/null +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -0,0 +1,255 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Boogie.SarifOutput +import Strata.Languages.Boogie.Verifier +import Lean.Data.Json + +/-! +# SARIF Output Tests + +This file contains tests for the SARIF output functionality, including: +- SARIF JSON structure validation +- VCResult to SARIF conversion +- Various verification result types (success, failure, error, unknown) +- Source location mapping +-/ + +namespace Boogie.Sarif.Tests + +open Lean (Json) +open Imperative + +/-! ## Test Helpers -/ + +/-- Create a simple metadata with file and location information -/ +def makeMetadata (file : String) (line col : Nat) : MetaData Expression := + #[ + { fld := .label "file", value := .msg file }, + { fld := .label "startLine", value := .msg (toString line) }, + { fld := .label "startColumn", value := .msg (toString col) } + ] + +/-- Create a simple proof obligation for testing -/ +def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression := + { label := label + assumptions := [] + obligation := Lambda.LExpr.boolConst () true + metadata := md } + +/-- Create a VCResult for testing -/ +def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expression := #[]) : VCResult := + { obligation := makeObligation label md + result := result + verbose := true } + +/-! ## Level Conversion Tests -/ + +-- Test that unsat (verified) maps to "none" level +#guard resultToLevel .unsat = Level.none + +-- Test that sat (failed) maps to "error" level +#guard resultToLevel (.sat []) = Level.error + +-- Test that unknown maps to "warning" level +#guard resultToLevel .unknown = Level.warning + +-- Test that error maps to "error" level +#guard resultToLevel (.err "test error") = Level.error + +/-! ## Message Generation Tests -/ + +-- Test unsat message +#guard resultToMessage .unsat = "Verification succeeded" + +-- Test sat message without counterexample +#guard resultToMessage (.sat []) = "Verification failed" + +-- Test unknown message +#guard (resultToMessage .unknown).startsWith "Verification result unknown" + +-- Test error message +#guard (resultToMessage (.err "test error")).startsWith "Verification error:" + +/-! ## Location Extraction Tests -/ + +-- Test location extraction from complete metadata +#eval + let md := makeMetadata "/test/file.st" 10 5 + let loc? := extractLocation md + match loc? with + | some loc => + if loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 5 then + IO.println "Location extraction test passed" + else + IO.println s!"Location extraction test failed: uri={loc.uri} line={loc.startLine} col={loc.startColumn}" + | none => IO.println "Location extraction test failed: no location" + +-- Test location extraction from empty metadata +#guard (extractLocation #[] == none) + +-- Test location extraction from incomplete metadata (missing column) +#guard + let md : MetaData Expression := #[ + { fld := .label "file", value := .msg "/test/file.st" }, + { fld := .label "startLine", value := .msg "10" } + ] + (extractLocation md == none) + +/-! ## VCResult to SARIF Conversion Tests -/ + +-- Test converting a successful VCResult +#eval + let md := makeMetadata "/test/file.st" 10 5 + let vcr := makeVCResult "test_obligation" .unsat md + let sarifResult := vcResultToSarifResult vcr + if sarifResult.ruleId = "test_obligation" && + sarifResult.level = Level.none && + sarifResult.locations.size = 1 then + IO.println "Successful VCResult conversion test passed" + else + IO.println s!"Successful VCResult conversion test failed: {repr sarifResult}" + +-- Test converting a failed VCResult +#eval + let md := makeMetadata "/test/file.st" 20 10 + let vcr := makeVCResult "failed_obligation" (.sat []) md + let sarifResult := vcResultToSarifResult vcr + if sarifResult.ruleId = "failed_obligation" && + sarifResult.level = Level.error && + sarifResult.message.text = "Verification failed" then + IO.println "Failed VCResult conversion test passed" + else + IO.println s!"Failed VCResult conversion test failed: {repr sarifResult}" + +-- Test converting an unknown VCResult +#eval + let vcr := makeVCResult "unknown_obligation" .unknown + let sarifResult := vcResultToSarifResult vcr + if sarifResult.ruleId = "unknown_obligation" && + sarifResult.level = Level.warning && + sarifResult.locations.size = 0 then + IO.println "Unknown VCResult conversion test passed" + else + IO.println s!"Unknown VCResult conversion test failed: {repr sarifResult}" + +-- Test converting an error VCResult +#eval + let vcr := makeVCResult "error_obligation" (.err "SMT solver error") + let sarifResult := vcResultToSarifResult vcr + if sarifResult.ruleId = "error_obligation" && + sarifResult.level = Level.error && + (sarifResult.message.text.startsWith "Verification error:") then + IO.println "Error VCResult conversion test passed" + else + IO.println s!"Error VCResult conversion test failed: {repr sarifResult}" + +/-! ## SARIF Document Structure Tests -/ + +#eval + let vcResults : VCResults := #[] + let sarif := vcResultsToSarif vcResults + if sarif.version = "2.1.0" && + sarif.runs.size = 1 && + sarif.runs[0]!.results.size = 0 && + sarif.runs[0]!.tool.driver.name = "Strata" then + IO.println "Empty SARIF document test passed" + else + IO.println s!"Empty SARIF document test failed" + +-- Test creating a SARIF document with multiple VCResults +#eval + let md1 := makeMetadata "/test/file1.st" 10 5 + let md2 := makeMetadata "/test/file2.st" 20 10 + let vcResults : VCResults := #[ + makeVCResult "obligation1" .unsat md1, + makeVCResult "obligation2" (.sat []) md2, + makeVCResult "obligation3" .unknown + ] + let sarif := vcResultsToSarif vcResults + if sarif.version = "2.1.0" && + sarif.runs.size = 1 && + sarif.runs[0]!.results.size = 3 && + sarif.runs[0]!.results[0]!.level = Level.none && + sarif.runs[0]!.results[1]!.level = Level.error && + sarif.runs[0]!.results[2]!.level = Level.warning then + IO.println "Multiple VCResults SARIF document test passed" + else + IO.println s!"Multiple VCResults SARIF document test failed" + +/-! ## JSON Serialization Tests -/ + +/-! ## JSON Serialization Tests -/ + +#eval + let json := Lean.ToJson.toJson Level.none + match json with + | Json.str "none" => IO.println "Level serialization test passed" + | _ => IO.println s!"Level serialization test failed: {json}" + +#eval + let msg : Message := { text := "Test message" } + let json := Lean.ToJson.toJson msg + -- Just check that it serializes without error + IO.println "Message serialization test passed" + +-- Test full SARIF document JSON generation +#eval + let md := makeMetadata "/test/example.st" 15 7 + let vcResults : VCResults := #[ + makeVCResult "test_assertion" .unsat md + ] + let sarif := vcResultsToSarif vcResults + let jsonStr := toJsonString sarif + + -- Check that the JSON contains expected fields + if (jsonStr.splitOn "\"version\":\"2.1.0\"").length > 1 && + (jsonStr.splitOn "\"Strata\"").length > 1 && + (jsonStr.splitOn "test_assertion").length > 1 then + IO.println "SARIF document JSON generation test passed" + else + IO.println s!"SARIF document JSON generation test failed" + +-- Test pretty JSON generation +#eval + let vcResults : VCResults := #[ + makeVCResult "simple_test" .unsat + ] + let sarif := vcResultsToSarif vcResults + let prettyJson := toPrettyJsonString sarif + + -- Pretty JSON should contain newlines for formatting + if prettyJson.contains '\n' then + IO.println "Pretty JSON generation test passed" + else + IO.println s!"Pretty JSON generation test failed" + +/-! ## Integration Test with Counter-Examples -/ + +-- Test SARIF output with counter-example +#eval + let cex : CounterEx := [((BoogieIdent.unres "x", some .int), "42")] + let md := makeMetadata "/test/cex.st" 25 3 + let vcr := makeVCResult "cex_obligation" (.sat cex) md + let sarifResult := vcResultToSarifResult vcr + + if sarifResult.level = Level.error && + (sarifResult.message.text.splitOn "counterexample").length > 1 && + sarifResult.locations.size = 1 then + IO.println "Counter-example SARIF test passed" + else + IO.println s!"Counter-example SARIF test failed: {repr sarifResult}" + +/-! ## Schema URI Test -/ + +#eval + let sarif := vcResultsToSarif #[] + if sarif.schema = "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json" then + IO.println "Schema URI test passed" + else + IO.println s!"Schema URI test failed: {sarif.schema}" + +end Boogie.Sarif.Tests diff --git a/StrataVerify.lean b/StrataVerify.lean index 65f71a6a0..1c354d5c3 100644 --- a/StrataVerify.lean +++ b/StrataVerify.lean @@ -6,6 +6,7 @@ -- Executable for verifying a Strata program from a file. import Strata.Languages.Boogie.Verifier +import Strata.Languages.Boogie.SarifOutput import Strata.Languages.C_Simp.Verify import Strata.Util.IO import Std.Internal.Parsec @@ -22,23 +23,25 @@ def isSuccessVCResult (vcResult : Boogie.VCResult) := def isFailureVCResult (vcResult : Boogie.VCResult) := !isSuccessResult vcResult.result -def parseOptions (args : List String) : Except Std.Format (Options × String) := - go Options.quiet args +def parseOptions (args : List String) : Except Std.Format (Options × String × Bool) := + go Options.quiet args false where - go : Options → List String → Except Std.Format (Options × String) - | opts, "--verbose" :: rest => go {opts with verbose := true} rest - | opts, "--check" :: rest => go {opts with checkOnly := true} rest - | opts, "--type-check" :: rest => go {opts with typeCheckOnly := true} rest - | opts, "--parse-only" :: rest => go {opts with parseOnly := true} rest - | opts, "--stop-on-first-error" :: rest => go {opts with stopOnFirstError := true} rest - | opts, "--solver-timeout" :: secondsStr :: rest => + go : Options → List String → Bool → Except Std.Format (Options × String × Bool) + | opts, "--verbose" :: rest, sarif => go {opts with verbose := true} rest sarif + | opts, "--check" :: rest, sarif => go {opts with checkOnly := true} rest sarif + | opts, "--type-check" :: rest, sarif => go {opts with typeCheckOnly := true} rest sarif + | opts, "--parse-only" :: rest, sarif => go {opts with parseOnly := true} rest sarif + | opts, "--stop-on-first-error" :: rest, sarif => go {opts with stopOnFirstError := true} rest sarif + | opts, "--sarif" :: rest, _ => go opts rest true + | opts, "--output-format=sarif" :: rest, _ => go opts rest true + | opts, "--solver-timeout" :: secondsStr :: rest, sarif => let n? := String.toNat? secondsStr match n? with | .none => .error f!"Invalid number of seconds: {secondsStr}" - | .some n => go {opts with solverTimeout := n} rest - | opts, [file] => pure (opts, file) - | _, [] => .error "StrataVerify requires a file as input" - | _, args => .error f!"Unknown options: {args}" + | .some n => go {opts with solverTimeout := n} rest sarif + | opts, [file], sarif => pure (opts, file, sarif) + | _, [], _ => .error "StrataVerify requires a file as input" + | _, args, _ => .error f!"Unknown options: {args}" def usageMessage : Std.Format := f!"Usage: StrataVerify [OPTIONS] {Std.Format.line}\ @@ -50,12 +53,14 @@ def usageMessage : Std.Format := --type-check Exit after semantic dialect's type inference/checking.{Std.Format.line} \ --parse-only Exit after DDM parsing and type checking.{Std.Format.line} \ --stop-on-first-error Exit after the first verification error.{Std.Format.line} \ - --solver-timeout Set the solver time limit per proof goal." + --solver-timeout Set the solver time limit per proof goal.{Std.Format.line} \ + --sarif Output results in SARIF format to .sarif{Std.Format.line} \ + --output-format=sarif Output results in SARIF format to .sarif" def main (args : List String) : IO UInt32 := do let parseResult := parseOptions args match parseResult with - | .ok (opts, file) => do + | .ok (opts, file, outputSarif) => do let text ← Strata.Util.readInputSource file let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) let dctx := Elab.LoadedDialects.builtin @@ -86,6 +91,23 @@ def main (args : List String) : IO UInt32 := do C_Simp.verify "z3" pgm opts else verify "z3" pgm inputCtx opts + + -- Output in SARIF format if requested + if outputSarif then + -- Skip SARIF generation for C_Simp files because the translation from C_Simp to + -- Boogie discards metadata (file, line, column information), making SARIF output + -- less useful. The vcResultsToSarif function would work type-wise (both produce + -- Boogie.VCResults), but the resulting SARIF would lack location information. + if file.endsWith ".csimp.st" then + println! "SARIF output is not supported for C_Simp files (.csimp.st) because location metadata is not preserved during translation to Boogie." + else + let sarifDoc := Boogie.Sarif.vcResultsToSarif vcResults + let sarifJson := Boogie.Sarif.toPrettyJsonString sarifDoc + let sarifFile := file ++ ".sarif" + IO.FS.writeFile sarifFile sarifJson + println! f!"SARIF output written to {sarifFile}" + + -- Also output standard format for vcResult in vcResults do let posStr := match Boogie.formatPositionMetaData vcResult.obligation.metadata with | .none => "" From 09ba8535a26d6a1e71ef7b0ae8c0346c482390c9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 21:55:10 +0100 Subject: [PATCH 2/8] Address feedback --- Strata/Languages/Boogie/SarifOutput.lean | 12 ++---- .../Languages/Boogie/SarifOutputTests.lean | 41 ++++++++++++------- 2 files changed, 30 insertions(+), 23 deletions(-) diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean index ec8e3d377..93609cbd4 100644 --- a/Strata/Languages/Boogie/SarifOutput.lean +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -99,19 +99,13 @@ instance : Inhabited Result where structure Driver where name : String version : String := "0.1.0" - informationUri : String := "https://github.com/tautschnig/strata-private" - deriving Repr, ToJson, FromJson - -instance : Inhabited Driver where - default := { name := "" } + 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 - -instance : Inhabited Tool where - default := { driver := default } + deriving Repr, ToJson, FromJson, Inhabited /-- SARIF run representing a single analysis run -/ structure Run where diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean index 62740eff8..b4fee0541 100644 --- a/StrataTest/Languages/Boogie/SarifOutputTests.lean +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -77,13 +77,14 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres /-! ## Location Extraction Tests -/ -- Test location extraction from complete metadata +#guard_msgs in #eval let md := makeMetadata "/test/file.st" 10 5 let loc? := extractLocation md match loc? with | some loc => if loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 5 then - IO.println "Location extraction test passed" + pure () else IO.println s!"Location extraction test failed: uri={loc.uri} line={loc.startLine} col={loc.startColumn}" | none => IO.println "Location extraction test failed: no location" @@ -102,6 +103,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres /-! ## VCResult to SARIF Conversion Tests -/ -- Test converting a successful VCResult +#guard_msgs in #eval let md := makeMetadata "/test/file.st" 10 5 let vcr := makeVCResult "test_obligation" .unsat md @@ -109,11 +111,12 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres if sarifResult.ruleId = "test_obligation" && sarifResult.level = Level.none && sarifResult.locations.size = 1 then - IO.println "Successful VCResult conversion test passed" + pure () else IO.println s!"Successful VCResult conversion test failed: {repr sarifResult}" -- Test converting a failed VCResult +#guard_msgs in #eval let md := makeMetadata "/test/file.st" 20 10 let vcr := makeVCResult "failed_obligation" (.sat []) md @@ -121,34 +124,37 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres if sarifResult.ruleId = "failed_obligation" && sarifResult.level = Level.error && sarifResult.message.text = "Verification failed" then - IO.println "Failed VCResult conversion test passed" + pure () else IO.println s!"Failed VCResult conversion test failed: {repr sarifResult}" -- Test converting an unknown VCResult +#guard_msgs in #eval let vcr := makeVCResult "unknown_obligation" .unknown let sarifResult := vcResultToSarifResult vcr if sarifResult.ruleId = "unknown_obligation" && sarifResult.level = Level.warning && sarifResult.locations.size = 0 then - IO.println "Unknown VCResult conversion test passed" + pure () else IO.println s!"Unknown VCResult conversion test failed: {repr sarifResult}" -- Test converting an error VCResult +#guard_msgs in #eval let vcr := makeVCResult "error_obligation" (.err "SMT solver error") let sarifResult := vcResultToSarifResult vcr if sarifResult.ruleId = "error_obligation" && sarifResult.level = Level.error && (sarifResult.message.text.startsWith "Verification error:") then - IO.println "Error VCResult conversion test passed" + pure () else IO.println s!"Error VCResult conversion test failed: {repr sarifResult}" /-! ## SARIF Document Structure Tests -/ +#guard_msgs in #eval let vcResults : VCResults := #[] let sarif := vcResultsToSarif vcResults @@ -156,11 +162,12 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres sarif.runs.size = 1 && sarif.runs[0]!.results.size = 0 && sarif.runs[0]!.tool.driver.name = "Strata" then - IO.println "Empty SARIF document test passed" + pure () else IO.println s!"Empty SARIF document test failed" -- Test creating a SARIF document with multiple VCResults +#guard_msgs in #eval let md1 := makeMetadata "/test/file1.st" 10 5 let md2 := makeMetadata "/test/file2.st" 20 10 @@ -176,7 +183,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres sarif.runs[0]!.results[0]!.level = Level.none && sarif.runs[0]!.results[1]!.level = Level.error && sarif.runs[0]!.results[2]!.level = Level.warning then - IO.println "Multiple VCResults SARIF document test passed" + pure () else IO.println s!"Multiple VCResults SARIF document test failed" @@ -184,19 +191,22 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres /-! ## JSON Serialization Tests -/ +#guard_msgs in #eval let json := Lean.ToJson.toJson Level.none match json with - | Json.str "none" => IO.println "Level serialization test passed" + | Json.str "none" => pure () | _ => IO.println s!"Level serialization test failed: {json}" +#guard_msgs in #eval let msg : Message := { text := "Test message" } - let json := Lean.ToJson.toJson msg + let _ := Lean.ToJson.toJson msg -- Just check that it serializes without error - IO.println "Message serialization test passed" + pure () -- Test full SARIF document JSON generation +#guard_msgs in #eval let md := makeMetadata "/test/example.st" 15 7 let vcResults : VCResults := #[ @@ -209,11 +219,12 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres if (jsonStr.splitOn "\"version\":\"2.1.0\"").length > 1 && (jsonStr.splitOn "\"Strata\"").length > 1 && (jsonStr.splitOn "test_assertion").length > 1 then - IO.println "SARIF document JSON generation test passed" + pure () else IO.println s!"SARIF document JSON generation test failed" -- Test pretty JSON generation +#guard_msgs in #eval let vcResults : VCResults := #[ makeVCResult "simple_test" .unsat @@ -223,13 +234,14 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres -- Pretty JSON should contain newlines for formatting if prettyJson.contains '\n' then - IO.println "Pretty JSON generation test passed" + pure () else IO.println s!"Pretty JSON generation test failed" /-! ## Integration Test with Counter-Examples -/ -- Test SARIF output with counter-example +#guard_msgs in #eval let cex : CounterEx := [((BoogieIdent.unres "x", some .int), "42")] let md := makeMetadata "/test/cex.st" 25 3 @@ -239,16 +251,17 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres if sarifResult.level = Level.error && (sarifResult.message.text.splitOn "counterexample").length > 1 && sarifResult.locations.size = 1 then - IO.println "Counter-example SARIF test passed" + pure () else IO.println s!"Counter-example SARIF test failed: {repr sarifResult}" /-! ## Schema URI Test -/ +#guard_msgs in #eval let sarif := vcResultsToSarif #[] if sarif.schema = "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json" then - IO.println "Schema URI test passed" + pure () else IO.println s!"Schema URI test failed: {sarif.schema}" From 65154259d0a8f37edd84fa7f4957b208c1db9ce9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 22:06:00 +0100 Subject: [PATCH 3/8] Update StrataTest/Languages/Boogie/SarifOutputTests.lean Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- StrataTest/Languages/Boogie/SarifOutputTests.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean index b4fee0541..1bc750234 100644 --- a/StrataTest/Languages/Boogie/SarifOutputTests.lean +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -189,8 +189,6 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres /-! ## JSON Serialization Tests -/ -/-! ## JSON Serialization Tests -/ - #guard_msgs in #eval let json := Lean.ToJson.toJson Level.none From 5e6f19ee806517e54c451fd343835f38f1624259 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 22:06:12 +0100 Subject: [PATCH 4/8] Update Strata/Languages/Boogie/SarifOutput.lean Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- Strata/Languages/Boogie/SarifOutput.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean index 93609cbd4..edd759b0c 100644 --- a/Strata/Languages/Boogie/SarifOutput.lean +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -194,7 +194,7 @@ def vcResultsToSarif (vcResults : VCResults) : SarifDocument := driver := { name := "Strata", version := "0.1.0", - informationUri := "https://github.com/tautschnig/strata-private" + informationUri := "https://github.com/strata-org/Strata" } } From 763c24091418c07a87343954a1ff343b958a5a71 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 22:07:16 +0100 Subject: [PATCH 5/8] Update StrataVerify.lean Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- StrataVerify.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/StrataVerify.lean b/StrataVerify.lean index 1c354d5c3..1d43c05d5 100644 --- a/StrataVerify.lean +++ b/StrataVerify.lean @@ -104,8 +104,11 @@ def main (args : List String) : IO UInt32 := do let sarifDoc := Boogie.Sarif.vcResultsToSarif vcResults let sarifJson := Boogie.Sarif.toPrettyJsonString sarifDoc let sarifFile := file ++ ".sarif" - IO.FS.writeFile sarifFile sarifJson - println! f!"SARIF output written to {sarifFile}" + try + IO.FS.writeFile sarifFile sarifJson + println! f!"SARIF output written to {sarifFile}" + catch e => + println! f!"Error writing SARIF output to {sarifFile}: {e.toString}" -- Also output standard format for vcResult in vcResults do From c5cfe827d3fb4d48b14299cf26286370fdb9b603 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Jan 2026 12:08:22 +0100 Subject: [PATCH 6/8] Refactor to address Aaron's comments --- Strata.lean | 3 + Strata/Languages/Boogie/Options.lean | 5 +- Strata/Languages/Boogie/SarifOutput.lean | 143 ++---------------- Strata/Util/Sarif.lean | 142 +++++++++++++++++ .../Languages/Boogie/SarifOutputTests.lean | 5 +- StrataVerify.lean | 36 ++--- 6 files changed, 181 insertions(+), 153 deletions(-) create mode 100644 Strata/Util/Sarif.lean diff --git a/Strata.lean b/Strata.lean index 20bd5d204..798e6b8b1 100644 --- a/Strata.lean +++ b/Strata.lean @@ -15,6 +15,9 @@ 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 diff --git a/Strata/Languages/Boogie/Options.lean b/Strata/Languages/Boogie/Options.lean index 042feea1d..4f22665b1 100644 --- a/Strata/Languages/Boogie/Options.lean +++ b/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 diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean index edd759b0c..405394c9e 100644 --- a/Strata/Languages/Boogie/SarifOutput.lean +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -5,126 +5,19 @@ -/ import Strata.Languages.Boogie.Verifier -import Lean.Data.Json +import Strata.Util.Sarif /-! -# SARIF Output +# Boogie SARIF Output -This module provides support for outputting verification 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 +This module provides Boogie-specific conversion functions for SARIF output. -/ namespace Boogie.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 - -/-! ## Conversion Functions -/ +open Strata.Sarif + +/-! ## Boogie-Specific Conversion Functions -/ /-- Convert Boogie Result to SARIF Level -/ def resultToLevel : Boogie.Result → Level @@ -169,18 +62,12 @@ def extractLocation (md : Imperative.MetaData Expression) : Option Location := d | some uri, none, none => pure { uri, startLine := 1, startColumn := 1 } | none, _, _ => none -/-- 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 a VCResult to a SARIF Result -/ -def vcResultToSarifResult (vcr : VCResult) : Result := +def vcResultToSarifResult (vcr : VCResult) : Strata.Sarif.Result := let ruleId := vcr.obligation.label let level := resultToLevel vcr.result let messageText := resultToMessage vcr.result - let message : Message := { text := messageText } + let message : Strata.Sarif.Message := { text := messageText } let locations := match extractLocation vcr.obligation.metadata with | some loc => #[locationToSarif loc] @@ -189,8 +76,8 @@ def vcResultToSarifResult (vcr : VCResult) : Result := { ruleId, level, message, locations } /-- Convert VCResults to a SARIF document -/ -def vcResultsToSarif (vcResults : VCResults) : SarifDocument := - let tool : Tool := { +def vcResultsToSarif (vcResults : VCResults) : Strata.Sarif.SarifDocument := + let tool : Strata.Sarif.Tool := { driver := { name := "Strata", version := "0.1.0", @@ -200,18 +87,10 @@ def vcResultsToSarif (vcResults : VCResults) : SarifDocument := let results := vcResults.map vcResultToSarifResult - let run : Run := { tool, results } + 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] } -/-- 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 Boogie.Sarif diff --git a/Strata/Util/Sarif.lean b/Strata/Util/Sarif.lean new file mode 100644 index 000000000..ff4bb51df --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean index 1bc750234..46f57c388 100644 --- a/StrataTest/Languages/Boogie/SarifOutputTests.lean +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -22,6 +22,7 @@ namespace Boogie.Sarif.Tests open Lean (Json) open Imperative +open Strata.Sarif (Level Message) /-! ## Test Helpers -/ @@ -211,7 +212,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres makeVCResult "test_assertion" .unsat md ] let sarif := vcResultsToSarif vcResults - let jsonStr := toJsonString sarif + let jsonStr := Strata.Sarif.toJsonString sarif -- Check that the JSON contains expected fields if (jsonStr.splitOn "\"version\":\"2.1.0\"").length > 1 && @@ -228,7 +229,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres makeVCResult "simple_test" .unsat ] let sarif := vcResultsToSarif vcResults - let prettyJson := toPrettyJsonString sarif + let prettyJson := Strata.Sarif.toPrettyJsonString sarif -- Pretty JSON should contain newlines for formatting if prettyJson.contains '\n' then diff --git a/StrataVerify.lean b/StrataVerify.lean index 1d43c05d5..b769ea3c5 100644 --- a/StrataVerify.lean +++ b/StrataVerify.lean @@ -23,25 +23,25 @@ def isSuccessVCResult (vcResult : Boogie.VCResult) := def isFailureVCResult (vcResult : Boogie.VCResult) := !isSuccessResult vcResult.result -def parseOptions (args : List String) : Except Std.Format (Options × String × Bool) := - go Options.quiet args false +def parseOptions (args : List String) : Except Std.Format (Options × String) := + go Options.quiet args where - go : Options → List String → Bool → Except Std.Format (Options × String × Bool) - | opts, "--verbose" :: rest, sarif => go {opts with verbose := true} rest sarif - | opts, "--check" :: rest, sarif => go {opts with checkOnly := true} rest sarif - | opts, "--type-check" :: rest, sarif => go {opts with typeCheckOnly := true} rest sarif - | opts, "--parse-only" :: rest, sarif => go {opts with parseOnly := true} rest sarif - | opts, "--stop-on-first-error" :: rest, sarif => go {opts with stopOnFirstError := true} rest sarif - | opts, "--sarif" :: rest, _ => go opts rest true - | opts, "--output-format=sarif" :: rest, _ => go opts rest true - | opts, "--solver-timeout" :: secondsStr :: rest, sarif => + go : Options → List String → Except Std.Format (Options × String) + | opts, "--verbose" :: rest => go {opts with verbose := true} rest + | opts, "--check" :: rest => go {opts with checkOnly := true} rest + | opts, "--type-check" :: rest => go {opts with typeCheckOnly := true} rest + | opts, "--parse-only" :: rest => go {opts with parseOnly := true} rest + | opts, "--stop-on-first-error" :: rest => go {opts with stopOnFirstError := true} rest + | opts, "--sarif" :: rest => go {opts with outputSarif := true} rest + | opts, "--output-format=sarif" :: rest => go {opts with outputSarif := true} rest + | opts, "--solver-timeout" :: secondsStr :: rest => let n? := String.toNat? secondsStr match n? with | .none => .error f!"Invalid number of seconds: {secondsStr}" - | .some n => go {opts with solverTimeout := n} rest sarif - | opts, [file], sarif => pure (opts, file, sarif) - | _, [], _ => .error "StrataVerify requires a file as input" - | _, args, _ => .error f!"Unknown options: {args}" + | .some n => go {opts with solverTimeout := n} rest + | opts, [file] => pure (opts, file) + | _, [] => .error "StrataVerify requires a file as input" + | _, args => .error f!"Unknown options: {args}" def usageMessage : Std.Format := f!"Usage: StrataVerify [OPTIONS] {Std.Format.line}\ @@ -60,7 +60,7 @@ def usageMessage : Std.Format := def main (args : List String) : IO UInt32 := do let parseResult := parseOptions args match parseResult with - | .ok (opts, file, outputSarif) => do + | .ok (opts, file) => do let text ← Strata.Util.readInputSource file let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) let dctx := Elab.LoadedDialects.builtin @@ -93,7 +93,7 @@ def main (args : List String) : IO UInt32 := do verify "z3" pgm inputCtx opts -- Output in SARIF format if requested - if outputSarif then + if opts.outputSarif then -- Skip SARIF generation for C_Simp files because the translation from C_Simp to -- Boogie discards metadata (file, line, column information), making SARIF output -- less useful. The vcResultsToSarif function would work type-wise (both produce @@ -102,7 +102,7 @@ def main (args : List String) : IO UInt32 := do println! "SARIF output is not supported for C_Simp files (.csimp.st) because location metadata is not preserved during translation to Boogie." else let sarifDoc := Boogie.Sarif.vcResultsToSarif vcResults - let sarifJson := Boogie.Sarif.toPrettyJsonString sarifDoc + let sarifJson := Strata.Sarif.toPrettyJsonString sarifDoc let sarifFile := file ++ ".sarif" try IO.FS.writeFile sarifFile sarifJson From 636225fb72ec934a47290dee4f63d3f11e4ce694 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Jan 2026 22:53:32 +0100 Subject: [PATCH 7/8] Fixup merge after #296 got merged in --- Strata/Languages/Boogie/SarifOutput.lean | 29 +++++-------------- .../Languages/Boogie/SarifOutputTests.lean | 14 ++++----- 2 files changed, 13 insertions(+), 30 deletions(-) diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean index 405394c9e..09501690c 100644 --- a/Strata/Languages/Boogie/SarifOutput.lean +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -39,28 +39,13 @@ def resultToMessage : Boogie.Result → String /-- Extract location information from metadata -/ def extractLocation (md : Imperative.MetaData Expression) : Option Location := do - let file ← md.findElem Imperative.MetaData.fileLabel - let line ← md.findElem Imperative.MetaData.startLineLabel - let col ← md.findElem Imperative.MetaData.startColumnLabel - - let uri? := match file.value with - | .msg m => some m - | _ => none - - let startLine? := match line.value with - | .msg s => s.toNat? - | _ => none - - let startColumn? := match col.value with - | .msg s => s.toNat? - | _ => none - - match uri?, startLine?, startColumn? with - | some uri, some startLine, some startColumn => pure { uri, startLine, startColumn } - | some uri, some startLine, none => pure { uri, startLine, startColumn := 1 } - | some uri, none, some startColumn => pure { uri, startLine := 1, startColumn } - | some uri, none, none => pure { uri, startLine := 1, startColumn := 1 } - | none, _, _ => none + 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 := diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean index 46f57c388..a6957256e 100644 --- a/StrataTest/Languages/Boogie/SarifOutputTests.lean +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -28,11 +28,10 @@ open Strata.Sarif (Level Message) /-- Create a simple metadata with file and location information -/ def makeMetadata (file : String) (line col : Nat) : MetaData Expression := - #[ - { fld := .label "file", value := .msg file }, - { fld := .label "startLine", value := .msg (toString line) }, - { fld := .label "startColumn", value := .msg (toString col) } - ] + let uri := Imperative.Uri.file file + let pos : Lean.Position := { line := line, column := col } + let fr : Imperative.FileRange := { file := uri, start := pos, ending := pos } + #[{ fld := Imperative.MetaData.fileRange, value := .fileRange fr }] /-- Create a simple proof obligation for testing -/ def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression := @@ -93,11 +92,10 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres -- Test location extraction from empty metadata #guard (extractLocation #[] == none) --- Test location extraction from incomplete metadata (missing column) +-- Test location extraction from metadata with wrong value type #guard let md : MetaData Expression := #[ - { fld := .label "file", value := .msg "/test/file.st" }, - { fld := .label "startLine", value := .msg "10" } + { fld := Imperative.MetaData.fileRange, value := .msg "not a fileRange" } ] (extractLocation md == none) From 248beb7a3937399db7ffc7f7b2e523b059026299 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Jan 2026 12:43:09 +0100 Subject: [PATCH 8/8] Update to latest main --- Strata/Languages/Boogie/SarifOutput.lean | 42 ++++++++------- .../Languages/Boogie/SarifOutputTests.lean | 51 ++++++++++--------- 2 files changed, 50 insertions(+), 43 deletions(-) diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean index 09501690c..fa4f6156e 100644 --- a/Strata/Languages/Boogie/SarifOutput.lean +++ b/Strata/Languages/Boogie/SarifOutput.lean @@ -15,27 +15,31 @@ This module provides Boogie-specific conversion functions for SARIF output. namespace Boogie.Sarif -open Strata.Sarif +open Strata.Sarif Strata.SMT /-! ## Boogie-Specific Conversion Functions -/ -/-- Convert Boogie Result to SARIF Level -/ -def resultToLevel : Boogie.Result → Level - | .unsat => .none -- Verification passed - | .sat _ => .error -- Verification failed (counterexample found) - | .unknown => .warning -- Solver could not determine - | .err _ => .error -- Error during verification - -/-- Convert Boogie Result to a descriptive message -/ -def resultToMessage : Boogie.Result → String - | .unsat => "Verification succeeded" - | .sat cex => - if cex.isEmpty then - "Verification failed" - else - s!"Verification failed with counterexample: {Std.format cex}" +/-- 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)" - | .err msg => s!"Verification error: {msg}" + | .implementationError msg => s!"Verification error: {msg}" /-- Extract location information from metadata -/ def extractLocation (md : Imperative.MetaData Expression) : Option Location := do @@ -50,8 +54,8 @@ def extractLocation (md : Imperative.MetaData Expression) : Option Location := d /-- Convert a VCResult to a SARIF Result -/ def vcResultToSarifResult (vcr : VCResult) : Strata.Sarif.Result := let ruleId := vcr.obligation.label - let level := resultToLevel vcr.result - let messageText := resultToMessage vcr.result + 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 diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean index a6957256e..6c6800593 100644 --- a/StrataTest/Languages/Boogie/SarifOutputTests.lean +++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean @@ -23,6 +23,7 @@ namespace Boogie.Sarif.Tests open Lean (Json) open Imperative open Strata.Sarif (Level Message) +open Boogie.SMT (SMTModel Result) /-! ## Test Helpers -/ @@ -36,43 +37,45 @@ def makeMetadata (file : String) (line col : Nat) : MetaData Expression := /-- Create a simple proof obligation for testing -/ def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression := { label := label + property := .assert assumptions := [] obligation := Lambda.LExpr.boolConst () true metadata := md } /-- Create a VCResult for testing -/ -def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expression := #[]) : VCResult := +def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .unknown) (md : MetaData Expression := #[]) : VCResult := { obligation := makeObligation label md - result := result + smtResult := smtResult + result := outcome verbose := true } /-! ## Level Conversion Tests -/ --- Test that unsat (verified) maps to "none" level -#guard resultToLevel .unsat = Level.none +-- Test that pass (verified) maps to "none" level +#guard outcomeToLevel .pass = Level.none --- Test that sat (failed) maps to "error" level -#guard resultToLevel (.sat []) = Level.error +-- Test that fail maps to "error" level +#guard outcomeToLevel .fail = Level.error -- Test that unknown maps to "warning" level -#guard resultToLevel .unknown = Level.warning +#guard outcomeToLevel .unknown = Level.warning --- Test that error maps to "error" level -#guard resultToLevel (.err "test error") = Level.error +-- Test that implementationError maps to "error" level +#guard outcomeToLevel (.implementationError "test error") = Level.error /-! ## Message Generation Tests -/ --- Test unsat message -#guard resultToMessage .unsat = "Verification succeeded" +-- Test pass message +#guard outcomeToMessage .pass .unknown = "Verification succeeded" --- Test sat message without counterexample -#guard resultToMessage (.sat []) = "Verification failed" +-- Test fail message without counterexample +#guard outcomeToMessage .fail .unknown = "Verification failed" -- Test unknown message -#guard (resultToMessage .unknown).startsWith "Verification result unknown" +#guard (outcomeToMessage .unknown .unknown).startsWith "Verification result unknown" -- Test error message -#guard (resultToMessage (.err "test error")).startsWith "Verification error:" +#guard (outcomeToMessage (.implementationError "test error") .unknown).startsWith "Verification error:" /-! ## Location Extraction Tests -/ @@ -105,7 +108,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres #guard_msgs in #eval let md := makeMetadata "/test/file.st" 10 5 - let vcr := makeVCResult "test_obligation" .unsat md + let vcr := makeVCResult "test_obligation" .pass .unsat md let sarifResult := vcResultToSarifResult vcr if sarifResult.ruleId = "test_obligation" && sarifResult.level = Level.none && @@ -118,7 +121,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres #guard_msgs in #eval let md := makeMetadata "/test/file.st" 20 10 - let vcr := makeVCResult "failed_obligation" (.sat []) md + let vcr := makeVCResult "failed_obligation" .fail (.sat []) md let sarifResult := vcResultToSarifResult vcr if sarifResult.ruleId = "failed_obligation" && sarifResult.level = Level.error && @@ -142,7 +145,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres -- Test converting an error VCResult #guard_msgs in #eval - let vcr := makeVCResult "error_obligation" (.err "SMT solver error") + let vcr := makeVCResult "error_obligation" (.implementationError "SMT solver error") let sarifResult := vcResultToSarifResult vcr if sarifResult.ruleId = "error_obligation" && sarifResult.level = Level.error && @@ -171,8 +174,8 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres let md1 := makeMetadata "/test/file1.st" 10 5 let md2 := makeMetadata "/test/file2.st" 20 10 let vcResults : VCResults := #[ - makeVCResult "obligation1" .unsat md1, - makeVCResult "obligation2" (.sat []) md2, + makeVCResult "obligation1" .pass .unsat md1, + makeVCResult "obligation2" .fail (.sat []) md2, makeVCResult "obligation3" .unknown ] let sarif := vcResultsToSarif vcResults @@ -207,7 +210,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres #eval let md := makeMetadata "/test/example.st" 15 7 let vcResults : VCResults := #[ - makeVCResult "test_assertion" .unsat md + makeVCResult "test_assertion" .pass .unsat md ] let sarif := vcResultsToSarif vcResults let jsonStr := Strata.Sarif.toJsonString sarif @@ -224,7 +227,7 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres #guard_msgs in #eval let vcResults : VCResults := #[ - makeVCResult "simple_test" .unsat + makeVCResult "simple_test" .pass ] let sarif := vcResultsToSarif vcResults let prettyJson := Strata.Sarif.toPrettyJsonString sarif @@ -240,9 +243,9 @@ def makeVCResult (label : String) (result : Boogie.Result) (md : MetaData Expres -- Test SARIF output with counter-example #guard_msgs in #eval - let cex : CounterEx := [((BoogieIdent.unres "x", some .int), "42")] + let cex : SMTModel := [((BoogieIdent.unres "x", some .int), "42")] let md := makeMetadata "/test/cex.st" 25 3 - let vcr := makeVCResult "cex_obligation" (.sat cex) md + let vcr := makeVCResult "cex_obligation" .fail (.sat cex) md let sarifResult := vcResultToSarifResult vcr if sarifResult.level = Level.error &&