Add FileMap to SARIF for metadata conversion (#356)

This fixes a build failure after PRs #343 and #290 crossed in the air.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

Author: tautschnig

Strata/Languages/Core/SarifOutput.lean

@@ -42,30 +42,32 @@ def outcomeToMessage (outcome : Outcome) (smtResult : SMT.Result) : String :=
   | .implementationError msg => s!"Verification error: {msg}"
 
 /-- Extract location information from metadata -/
-def extractLocation (md : Imperative.MetaData Expression) : Option Location := do
+def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaData Expression) : Option Location := do
   let fileRangeElem ← md.findElem Imperative.MetaData.fileRange
   match fileRangeElem.value with
-  | .file2dRange fr =>
+  | .fileRange fr =>
+    let fileMap ← files.find? fr.file
+    let startPos := fileMap.toPosition fr.range.start
     let uri := match fr.file with
                | .file path => path
-    pure { uri, startLine := fr.start.line, startColumn := fr.start.column }
+    pure { uri, startLine := startPos.line, startColumn := startPos.column }
   | _ => none
 
 /-- Convert a VCResult to a SARIF Result -/
-def vcResultToSarifResult (vcr : VCResult) : Strata.Sarif.Result :=
+def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (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
+  let locations := match extractLocation files 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 :=
+def vcResultsToSarif (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
   let tool : Strata.Sarif.Tool := {
     driver := {
       name := "Strata",
@@ -74,7 +76,7 @@ def vcResultsToSarif (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
     }
   }
 
-  let results := vcResults.map vcResultToSarifResult
+  let results := vcResults.map (vcResultToSarifResult files)
 
   let run : Strata.Sarif.Run := { tool, results }
 

StrataTest/Languages/Core/SarifOutputTests.lean

@@ -30,9 +30,20 @@ open Core.SMT (SMTModel Result)
 /-- Create a simple metadata with file and location information -/
 def makeMetadata (file : String) (line col : Nat) : MetaData Expression :=
   let uri := Strata.Uri.file file
-  let pos : Lean.Position := { line := line, column := col }
-  let fr : Strata.File2dRange := { file := uri, start := pos, ending := pos }
-  #[{ fld := Imperative.MetaData.fileRange, value := .file2dRange fr }]
+  -- Create a 1D range (byte offsets). For testing, we use simple offsets.
+  let range : Strata.SourceRange := { start := ⟨0⟩, stop := ⟨10⟩ }
+  let fr : Strata.FileRange := { file := uri, range := range }
+  #[{ fld := Imperative.MetaData.fileRange, value := .fileRange fr }]
+
+/-- Create a simple FileMap for testing -/
+def makeFileMap : Lean.FileMap :=
+  -- Create a simple file map with some dummy content
+  Lean.FileMap.ofString "test content\nline 2\nline 3"
+
+/-- Create a files map for testing -/
+def makeFilesMap (file : String) : Map Strata.Uri Lean.FileMap :=
+  let uri := Strata.Uri.file file
+  Map.empty.insert uri makeFileMap
 
 /-- Create a simple proof obligation for testing -/
 def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression :=
@@ -82,75 +93,84 @@ def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .un
 -- Test location extraction from complete metadata
 #guard
   let md := makeMetadata "/test/file.st" 10 5
-  let loc? := extractLocation md
+  let files := makeFilesMap "/test/file.st"
+  let loc? := extractLocation files md
   match loc? with
-  | some loc => loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 5
+  | some loc => loc.uri = "/test/file.st"
   | none => false
 
 -- Test location extraction from empty metadata
-#guard (extractLocation #[] == none)
+#guard
+  let files := makeFilesMap "/test/file.st"
+  (extractLocation files #[] == none)
 
 -- Test location extraction from metadata with wrong value type
 #guard
   let md : MetaData Expression := #[
     { fld := Imperative.MetaData.fileRange, value := .msg "not a fileRange" }
   ]
-  (extractLocation md == none)
+  let files := makeFilesMap "/test/file.st"
+  (extractLocation files md == none)
 
 /-! ## VCResult to SARIF Conversion Tests -/
 
 -- Test converting a successful VCResult
 #guard
   let md := makeMetadata "/test/file.st" 10 5
+  let files := makeFilesMap "/test/file.st"
   let vcr := makeVCResult "test_obligation" .pass .unsat md
-  let sarifResult := vcResultToSarifResult vcr
+  let sarifResult := vcResultToSarifResult files vcr
   sarifResult.ruleId = "test_obligation" &&
   sarifResult.level = Level.none &&
   sarifResult.locations.size = 1 &&
   match sarifResult.locations[0]? with
   | some loc =>
     loc.physicalLocation.artifactLocation.uri = "/test/file.st" &&
-    loc.physicalLocation.region.startLine = 10 &&
-    loc.physicalLocation.region.startColumn = 5
+    loc.physicalLocation.region.startLine = 1 &&
+    loc.physicalLocation.region.startColumn = 0
   | none => false
 
 -- Test converting a failed VCResult
 #guard
   let md := makeMetadata "/test/file.st" 20 10
+  let files := makeFilesMap "/test/file.st"
   let vcr := makeVCResult "failed_obligation" .fail (.sat []) md
-  let sarifResult := vcResultToSarifResult vcr
+  let sarifResult := vcResultToSarifResult files vcr
   sarifResult.ruleId = "failed_obligation" &&
   sarifResult.level = Level.error &&
   sarifResult.message.text = "Verification failed" &&
   sarifResult.locations.size = 1 &&
   match sarifResult.locations[0]? with
   | some loc =>
     loc.physicalLocation.artifactLocation.uri = "/test/file.st" &&
-    loc.physicalLocation.region.startLine = 20 &&
-    loc.physicalLocation.region.startColumn = 10
+    loc.physicalLocation.region.startLine = 1 &&
+    loc.physicalLocation.region.startColumn = 0
   | none => false
 
 -- Test converting an unknown VCResult
 #guard
+  let files := makeFilesMap "/test/file.st"
   let vcr := makeVCResult "unknown_obligation" .unknown
-  let sarifResult := vcResultToSarifResult vcr
+  let sarifResult := vcResultToSarifResult files vcr
   sarifResult.ruleId = "unknown_obligation" &&
   sarifResult.level = Level.warning &&
   sarifResult.locations.size = 0
 
 -- Test converting an error VCResult
 #guard
+  let files := makeFilesMap "/test/file.st"
   let vcr := makeVCResult "error_obligation" (.implementationError "SMT solver error")
-  let sarifResult := vcResultToSarifResult vcr
+  let sarifResult := vcResultToSarifResult files vcr
   sarifResult.ruleId = "error_obligation" &&
   sarifResult.level = Level.error &&
   sarifResult.message.text.startsWith "Verification error:"
 
 /-! ## SARIF Document Structure Tests -/
 
 #guard
+  let files := makeFilesMap "/test/file.st"
   let vcResults : VCResults := #[]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   sarif.version = "2.1.0" &&
   sarif.runs.size = 1 &&
   match sarif.runs[0]? with
@@ -161,12 +181,15 @@ def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .un
 #guard
   let md1 := makeMetadata "/test/file1.st" 10 5
   let md2 := makeMetadata "/test/file2.st" 20 10
+  let files1 := makeFilesMap "/test/file1.st"
+  let files2 := makeFilesMap "/test/file2.st"
+  let files := files1.union files2
   let vcResults : VCResults := #[
     makeVCResult "obligation1" .pass .unsat md1,
     makeVCResult "obligation2" .fail (.sat []) md2,
     makeVCResult "obligation3" .unknown
   ]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   sarif.version = "2.1.0" &&
   sarif.runs.size = 1 &&
   match sarif.runs[0]? with
@@ -193,21 +216,23 @@ def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .un
 -- Test full SARIF document JSON generation
 #guard
   let md := makeMetadata "/test/example.st" 15 7
+  let files := makeFilesMap "/test/example.st"
   let vcResults : VCResults := #[
     makeVCResult "test_assertion" .pass .unsat md
   ]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   let jsonStr := Strata.Sarif.toJsonString sarif
   (jsonStr.splitOn "\"version\":\"2.1.0\"").length > 1 &&
   (jsonStr.splitOn "\"Strata\"").length > 1 &&
   (jsonStr.splitOn "test_assertion").length > 1
 
 -- Test pretty JSON generation
 #guard
+  let files := makeFilesMap "/test/file.st"
   let vcResults : VCResults := #[
     makeVCResult "simple_test" .pass
   ]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   let prettyJson := Strata.Sarif.toPrettyJsonString sarif
   prettyJson.contains '\n'
 
@@ -217,68 +242,75 @@ def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .un
 #guard
   let cex : SMTModel := [(({ name := "x", metadata := Visibility.unres }, some .int), "42")]
   let md := makeMetadata "/test/cex.st" 25 3
+  let files := makeFilesMap "/test/cex.st"
   let vcr := makeVCResult "cex_obligation" .fail (.sat cex) md
-  let sarifResult := vcResultToSarifResult vcr
+  let sarifResult := vcResultToSarifResult files vcr
   sarifResult.level = Level.error &&
   (sarifResult.message.text.splitOn "counterexample").length > 1 &&
   sarifResult.locations.size = 1 &&
   match sarifResult.locations[0]? with
   | some loc =>
     loc.physicalLocation.artifactLocation.uri = "/test/cex.st" &&
-    loc.physicalLocation.region.startLine = 25 &&
-    loc.physicalLocation.region.startColumn = 3
+    loc.physicalLocation.region.startLine = 1 &&
+    loc.physicalLocation.region.startColumn = 0
   | none => false
 
 /-! ## JSON Output Tests -/
 
 /-- info: "{\"runs\":[{\"results\":[],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
+  let files := makeFilesMap "/test/file.st"
   let vcResults : VCResults := #[]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":5,\"startLine\":10}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/pass.st" 10 5
+  let files := makeFilesMap "/test/pass.st"
   let vcResults : VCResults := #[makeVCResult "test_pass" .pass .unsat md]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":15,\"startLine\":20}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/fail.st" 20 15
+  let files := makeFilesMap "/test/fail.st"
   let vcResults : VCResults := #[makeVCResult "test_fail" .fail (.sat []) md]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
 /-- info: "{\"runs\":[{\"results\":[{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
+  let files := makeFilesMap "/test/file.st"
   let vcResults : VCResults := #[makeVCResult "test_unknown" .unknown]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
 /-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
+  let files := makeFilesMap "/test/file.st"
   let vcResults : VCResults := #[makeVCResult "test_error" (.implementationError "timeout")]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":1,\"startLine\":5}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":1,\"startLine\":10}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md1 := makeMetadata "/test/multi.st" 5 1
   let md2 := makeMetadata "/test/multi.st" 10 1
+  let files := makeFilesMap "/test/multi.st"
   let vcResults : VCResults := #[
     makeVCResult "obligation1" .pass .unsat md1,
     makeVCResult "obligation2" .fail (.sat []) md2,
     makeVCResult "obligation3" .unknown
   ]
-  let sarif := vcResultsToSarif vcResults
+  let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
 end Core.Sarif.Tests

StrataVerify.lean

@@ -117,7 +117,10 @@ def main (args : List String) : IO UInt32 := do
           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 Core."
           else
-            let sarifDoc := Core.Sarif.vcResultsToSarif vcResults
+            -- Create a files map with the single input file
+            let uri := Strata.Uri.file file
+            let files := Map.empty.insert uri inputCtx.fileMap
+            let sarifDoc := Core.Sarif.vcResultsToSarif files vcResults
             let sarifJson := Strata.Sarif.toPrettyJsonString sarifDoc
             let sarifFile := file ++ ".sarif"
             try