Add SARIF output format support with comprehensive tests #290

tautschnig · 2025-12-22T19:25:13Z

Description of changes:

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.

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

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.

joehendrix

Style seems reasonable to me. I had a few changes; the most important is related to #guard_msgs.

Strata/Languages/Boogie/SarifOutput.lean

joehendrix · 2025-12-22T19:41:45Z

StrataTest/Languages/Boogie/SarifOutputTests.lean

+/-! ## VCResult to SARIF Conversion Tests -/
+
+-- Test converting a successful VCResult
+#eval


You can use #guard_msgs in to test the output is expected. I'd add that to all the #eval statements to squelch output.

I believe to have addressed this, if I understood correctly?

Actually, I'm looking over these tests and others, and it's odd they are in IO. I think generally Lean should be functional unless there's a good reason to use IO.

Agreed. Ideally I'd like to see the tests print out SARIF JSON on the success path and #guard_msgs based on that.

That seems does seem like a good use of #guard_msgs. The test would looks something like:

/-- info: (json...) -/ #guard_msgs in #eval (code that generates JSON)

Copilot

Pull request overview

This PR adds support for outputting verification results in SARIF (Static Analysis Results Interchange Format) v2.1.0 JSON format, enabling integration with tools that consume SARIF output. The implementation includes comprehensive data structures, conversion functions, and test coverage.

Key Changes:

New SARIF output module with complete data structures for SARIF v2.1.0 format
Command-line options --sarif and --output-format=sarif to enable SARIF output generation
Comprehensive test suite validating SARIF conversion and JSON serialization

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
StrataVerify.lean	Adds command-line parsing for SARIF options and integrates SARIF output generation into the main verification workflow, with special handling for C_Simp files
Strata/Languages/Boogie/SarifOutput.lean	Implements complete SARIF v2.1.0 data structures and conversion functions to transform VCResults to SARIF format
StrataTest/Languages/Boogie/SarifOutputTests.lean	Provides comprehensive test coverage including level conversion, message generation, location extraction, and JSON serialization
Strata.lean	Adds import for the new SarifOutput module
Examples/SarifTest.boogie.st	Adds example Boogie program for testing SARIF output functionality

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

StrataTest/Languages/Boogie/SarifOutputTests.lean

Copilot · 2025-12-22T21:01:46Z

Strata/Languages/Boogie/SarifOutput.lean

+  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


The extractLocation function provides fallback default values when line or column information is missing (defaulting to line 1, column 1). While this allows SARIF output to be generated, it may be misleading to report a location with incorrect line/column numbers. Consider either returning None when essential location information is missing, or documenting this fallback behavior clearly in the function's docstring.

StrataVerify.lean

Copilot · 2025-12-22T21:01:46Z

StrataTest/Languages/Boogie/SarifOutputTests.lean

+    { fld := .label "file", value := .msg "/test/file.st" },
+    { fld := .label "startLine", value := .msg "10" }
+  ]
+  (extractLocation md == none)


This test expects extractLocation to return none when column information is missing, but the actual implementation (lines 167-169 in SarifOutput.lean) provides fallback default values and returns Some with startColumn := 1. This test will fail. Either update the test to match the implementation's behavior, or change the implementation to match the test's expectations.

Suggested change

(extractLocation md == none)

match extractLocation md with

| some loc =>

loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 1

| none => false

Strata/Languages/Boogie/SarifOutput.lean

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

atomb

It's really cool to have this! I requested a couple of stylistic changes, but they should be easy.

Strata/Languages/Boogie/SarifOutput.lean

StrataVerify.lean

atomb · 2026-01-07T16:29:45Z

It looks like the most recent refactoring led to some missing references. Maybe a missing import?

tautschnig · 2026-01-07T21:55:50Z

It looks like the most recent refactoring led to some missing references. Maybe a missing import?

Err, sorry, I had blindly merged from main, being unaware that #256 had brought about Metadata changes.

joehendrix · 2026-01-15T18:41:23Z

Strata/Util/Sarif.lean

+
+/-- SARIF tool driver information -/
+structure Driver where
+  name : String


What's a "Driver"? Is that a command line a tool name or something else?

I have a similar question about ruleId. I think a short comment with an example would help or maybe just link to a URL for the Sarif reference at the top of model so it is easy for someone not familiar with Sarif to understand what some of the strings are for.

joehendrix · 2026-01-15T18:51:53Z

StrataTest/Languages/Boogie/SarifOutputTests.lean

+#guard_msgs in
+#eval
+  let md := makeMetadata "/test/file.st" 20 10
+  let vcr := makeVCResult "failed_obligation" .fail (.sat []) md
+  let sarifResult := vcResultToSarifResult vcr
+  if sarifResult.ruleId = "failed_obligation" &&
+     sarifResult.level = Level.error &&
+     sarifResult.message.text = "Verification failed" then
+    pure ()
+  else
+    IO.println s!"Failed VCResult conversion test failed: {repr sarifResult}"


I think this would be more idiomatic as the following:

Suggested change

#guard_msgs in

#eval

let md := makeMetadata "/test/file.st" 20 10

let vcr := makeVCResult "failed_obligation" .fail (.sat []) md

let sarifResult := vcResultToSarifResult vcr

if sarifResult.ruleId = "failed_obligation" &&

sarifResult.level = Level.error &&

sarifResult.message.text = "Verification failed" then

pure ()

else

IO.println s!"Failed VCResult conversion test failed: {repr sarifResult}"

#guard

let md := makeMetadata "/test/file.st" 20 10

let vcr := makeVCResult "failed_obligation" .fail (.sat []) md

let sarifResult := vcResultToSarifResult vcr

let expected := {

ruleId := "failed_obligation"

level := Level.error

message := { text = "Verification failed" }

}

sarifResult = expected

This will require deriving DecidableEq be added to the Sarif result type. If you were intentionally only testing three fields, then I'd change it to do the same, but still use #guard in place of #guard_msgs and IO.

joehendrix · 2026-01-15T18:53:18Z

StrataTest/Languages/Boogie/SarifOutputTests.lean

+  if sarif.schema = "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json" then
+    pure ()
+  else
+    IO.println s!"Schema URI test failed: {sarif.schema}"


This test seems pretty artificial.

atomb · 2026-01-15T19:50:29Z

Strata/Util/Sarif.lean

+  uri : String
+  startLine : Nat
+  startColumn : Nat
+  deriving Repr, ToJson, FromJson, BEq


Do these instances just magically give us JSON that's in the right form for SARIF? Pretty cool, if so!

shigoel requested a review from joehendrix December 22, 2025 19:33

joehendrix requested changes Dec 22, 2025

View reviewed changes

Address feedback

09ba853

tautschnig marked this pull request as ready for review December 22, 2025 20:57

Copilot AI review requested due to automatic review settings December 22, 2025 20:57

tautschnig requested review from a team, MikaelMayer, atomb and shigoel as code owners December 22, 2025 20:57

Copilot started reviewing on behalf of tautschnig December 22, 2025 20:57 View session

Copilot AI reviewed Dec 22, 2025

View reviewed changes

tautschnig and others added 3 commits December 22, 2025 22:06

Update StrataTest/Languages/Boogie/SarifOutputTests.lean

6515425

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update Strata/Languages/Boogie/SarifOutput.lean

5e6f19e

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update StrataVerify.lean

763c240

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

atomb requested changes Jan 6, 2026

View reviewed changes

Strata/Languages/Boogie/SarifOutput.lean Show resolved Hide resolved

StrataVerify.lean Outdated Show resolved Hide resolved

tautschnig added 2 commits January 7, 2026 12:09

Refactor to address Aaron's comments

c5cfe82

Merge remote-tracking branch 'origin/main' into tautschnig/SARIF-output

feac468

tautschnig assigned atomb and joehendrix Jan 7, 2026

tautschnig added 2 commits January 7, 2026 22:53

Fixup merge after #296 got merged in

636225f

Merge remote-tracking branch 'origin/main' into tautschnig/SARIF-output

db83267

tautschnig and others added 3 commits January 15, 2026 12:11

Merge remote-tracking branch 'origin/main' into tautschnig/SARIF-output

4c10bb1

Update to latest main

248beb7

Merge branch 'main' into tautschnig/SARIF-output

bf37a14

joehendrix reviewed Jan 15, 2026

View reviewed changes

atomb reviewed Jan 15, 2026

View reviewed changes

-  (extractLocation md == none)
+  match extractLocation md with
+  | some loc =>
+      loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 1
+  | none => false

Add SARIF output format support with comprehensive tests #290

Are you sure you want to change the base?

Add SARIF output format support with comprehensive tests #290

Uh oh!

Conversation

tautschnig commented Dec 22, 2025

Uh oh!

joehendrix left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

atomb left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

atomb commented Jan 7, 2026

Uh oh!

tautschnig commented Jan 7, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joehendrix Jan 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

joehendrix left a comment •

edited

Loading

joehendrix Jan 15, 2026 •

edited

Loading