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

SARIF Data Structures

structure Strata.Sarif.Location : Type

SARIF location representing a position in source code

• uri : String
• startLine : Nat
• startColumn : Nat

instance Strata.Sarif.instReprLocation : Repr Location

Equations

• Strata.Sarif.instReprLocation = { reprPrec := Strata.Sarif.instReprLocation.repr }

def Strata.Sarif.instReprLocation.repr : Location → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instToJsonLocation.toJson : Location → Lean.Json

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instToJsonLocation : Lean.ToJson Location

Equations

• Strata.Sarif.instToJsonLocation = { toJson := Strata.Sarif.instToJsonLocation.toJson }

def Strata.Sarif.instFromJsonLocation.fromJson : Lean.Json → Except String Location

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instFromJsonLocation : Lean.FromJson Location

Equations

• Strata.Sarif.instFromJsonLocation = { fromJson? := Strata.Sarif.instFromJsonLocation.fromJson }

def Strata.Sarif.instBEqLocation.beq : Location → Location → Bool

Equations

• Strata.Sarif.instBEqLocation.beq { uri := a, startLine := a_1, startColumn := a_2 } { uri := b, startLine := b_1, startColumn := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Strata.Sarif.instBEqLocation.beq x✝¹ x✝ = false

instance Strata.Sarif.instBEqLocation : BEq Location

Equations

• Strata.Sarif.instBEqLocation = { beq := Strata.Sarif.instBEqLocation.beq }

structure Strata.Sarif.ArtifactLocation : Type

SARIF artifact location representing a file URI

• uri : String

def Strata.Sarif.instReprArtifactLocation.repr : ArtifactLocation → Nat → Std.Format

Equations

• Strata.Sarif.instReprArtifactLocation.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "uri" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.uri)).group) " }"

instance Strata.Sarif.instReprArtifactLocation : Repr ArtifactLocation

Equations

• Strata.Sarif.instReprArtifactLocation = { reprPrec := Strata.Sarif.instReprArtifactLocation.repr }

def Strata.Sarif.instToJsonArtifactLocation.toJson : ArtifactLocation → Lean.Json

Equations

• Strata.Sarif.instToJsonArtifactLocation.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)]].flatten

instance Strata.Sarif.instToJsonArtifactLocation : Lean.ToJson ArtifactLocation

Equations

• Strata.Sarif.instToJsonArtifactLocation = { toJson := Strata.Sarif.instToJsonArtifactLocation.toJson }

instance Strata.Sarif.instFromJsonArtifactLocation : Lean.FromJson ArtifactLocation

Equations

• Strata.Sarif.instFromJsonArtifactLocation = { fromJson? := Strata.Sarif.instFromJsonArtifactLocation.fromJson }

def Strata.Sarif.instFromJsonArtifactLocation.fromJson : Lean.Json → Except String ArtifactLocation

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instDecidableEqArtifactLocation.decEq (x✝ x✝¹ : ArtifactLocation) : Decidable (x✝ = x✝¹)

Equations

• Strata.Sarif.instDecidableEqArtifactLocation.decEq { uri := a } { uri := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Strata.Sarif.instDecidableEqArtifactLocation : DecidableEq ArtifactLocation

Equations

• Strata.Sarif.instDecidableEqArtifactLocation = Strata.Sarif.instDecidableEqArtifactLocation.decEq

structure Strata.Sarif.Region : Type

SARIF region representing a source code region with line and column information

• startLine : Nat
• startColumn : Nat

def Strata.Sarif.instReprRegion.repr : Region → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprRegion : Repr Region

Equations

• Strata.Sarif.instReprRegion = { reprPrec := Strata.Sarif.instReprRegion.repr }

instance Strata.Sarif.instToJsonRegion : Lean.ToJson Region

Equations

• Strata.Sarif.instToJsonRegion = { toJson := Strata.Sarif.instToJsonRegion.toJson }

def Strata.Sarif.instToJsonRegion.toJson : Region → Lean.Json

Equations

• Strata.Sarif.instToJsonRegion.toJson x✝ = Lean.Json.mkObj [[("startLine", Lean.toJson x✝.startLine)], [("startColumn", Lean.toJson x✝.startColumn)]].flatten

def Strata.Sarif.instFromJsonRegion.fromJson : Lean.Json → Except String Region

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instFromJsonRegion : Lean.FromJson Region

Equations

• Strata.Sarif.instFromJsonRegion = { fromJson? := Strata.Sarif.instFromJsonRegion.fromJson }

instance Strata.Sarif.instDecidableEqRegion : DecidableEq Region

Equations

• Strata.Sarif.instDecidableEqRegion = Strata.Sarif.instDecidableEqRegion.decEq

def Strata.Sarif.instDecidableEqRegion.decEq (x✝ x✝¹ : Region) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

structure Strata.Sarif.PhysicalLocation : Type

SARIF physical location with region information

• artifactLocation : ArtifactLocation
• region : Region

def Strata.Sarif.instReprPhysicalLocation.repr : PhysicalLocation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprPhysicalLocation : Repr PhysicalLocation

Equations

• Strata.Sarif.instReprPhysicalLocation = { reprPrec := Strata.Sarif.instReprPhysicalLocation.repr }

def Strata.Sarif.instToJsonPhysicalLocation.toJson : PhysicalLocation → Lean.Json

Equations

• Strata.Sarif.instToJsonPhysicalLocation.toJson x✝ = Lean.Json.mkObj [[("artifactLocation", Lean.toJson x✝.artifactLocation)], [("region", Lean.toJson x✝.region)]].flatten

instance Strata.Sarif.instToJsonPhysicalLocation : Lean.ToJson PhysicalLocation

Equations

• Strata.Sarif.instToJsonPhysicalLocation = { toJson := Strata.Sarif.instToJsonPhysicalLocation.toJson }

def Strata.Sarif.instFromJsonPhysicalLocation.fromJson : Lean.Json → Except String PhysicalLocation

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instFromJsonPhysicalLocation : Lean.FromJson PhysicalLocation

Equations

• Strata.Sarif.instFromJsonPhysicalLocation = { fromJson? := Strata.Sarif.instFromJsonPhysicalLocation.fromJson }

instance Strata.Sarif.instDecidableEqPhysicalLocation : DecidableEq PhysicalLocation

Equations

• Strata.Sarif.instDecidableEqPhysicalLocation = Strata.Sarif.instDecidableEqPhysicalLocation.decEq

def Strata.Sarif.instDecidableEqPhysicalLocation.decEq (x✝ x✝¹ : PhysicalLocation) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

structure Strata.Sarif.SarifLocation : Type

SARIF location wrapper

• physicalLocation : PhysicalLocation

def Strata.Sarif.instReprSarifLocation.repr : SarifLocation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprSarifLocation : Repr SarifLocation

Equations

• Strata.Sarif.instReprSarifLocation = { reprPrec := Strata.Sarif.instReprSarifLocation.repr }

def Strata.Sarif.instToJsonSarifLocation.toJson : SarifLocation → Lean.Json

Equations

• Strata.Sarif.instToJsonSarifLocation.toJson x✝ = Lean.Json.mkObj [[("physicalLocation", Lean.toJson x✝.physicalLocation)]].flatten

instance Strata.Sarif.instToJsonSarifLocation : Lean.ToJson SarifLocation

Equations

• Strata.Sarif.instToJsonSarifLocation = { toJson := Strata.Sarif.instToJsonSarifLocation.toJson }

instance Strata.Sarif.instFromJsonSarifLocation : Lean.FromJson SarifLocation

Equations

• Strata.Sarif.instFromJsonSarifLocation = { fromJson? := Strata.Sarif.instFromJsonSarifLocation.fromJson }

def Strata.Sarif.instFromJsonSarifLocation.fromJson : Lean.Json → Except String SarifLocation

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instDecidableEqSarifLocation : DecidableEq SarifLocation

Equations

• Strata.Sarif.instDecidableEqSarifLocation = Strata.Sarif.instDecidableEqSarifLocation.decEq

def Strata.Sarif.instDecidableEqSarifLocation.decEq (x✝ x✝¹ : SarifLocation) : Decidable (x✝ = x✝¹)

Equations

• Strata.Sarif.instDecidableEqSarifLocation.decEq { physicalLocation := a } { physicalLocation := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

structure Strata.Sarif.Message : Type

SARIF message

• text : String

instance Strata.Sarif.instReprMessage : Repr Message

Equations

• Strata.Sarif.instReprMessage = { reprPrec := Strata.Sarif.instReprMessage.repr }

def Strata.Sarif.instReprMessage.repr : Message → Nat → Std.Format

Equations

• Strata.Sarif.instReprMessage.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "text" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.text)).group) " }"

instance Strata.Sarif.instToJsonMessage : Lean.ToJson Message

Equations

• Strata.Sarif.instToJsonMessage = { toJson := Strata.Sarif.instToJsonMessage.toJson }

def Strata.Sarif.instToJsonMessage.toJson : Message → Lean.Json

Equations

• Strata.Sarif.instToJsonMessage.toJson x✝ = Lean.Json.mkObj [[("text", Lean.toJson x✝.text)]].flatten

instance Strata.Sarif.instFromJsonMessage : Lean.FromJson Message

Equations

• Strata.Sarif.instFromJsonMessage = { fromJson? := Strata.Sarif.instFromJsonMessage.fromJson }

def Strata.Sarif.instFromJsonMessage.fromJson : Lean.Json → Except String Message

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instDecidableEqMessage : DecidableEq Message

Equations

• Strata.Sarif.instDecidableEqMessage = Strata.Sarif.instDecidableEqMessage.decEq

def Strata.Sarif.instDecidableEqMessage.decEq (x✝ x✝¹ : Message) : Decidable (x✝ = x✝¹)

Equations

• Strata.Sarif.instDecidableEqMessage.decEq { text := a } { text := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Strata.Sarif.Level : Type

SARIF result level

• none : Level
• note : Level
• warning : Level
• error : Level

instance Strata.Sarif.instReprLevel : Repr Level

Equations

• Strata.Sarif.instReprLevel = { reprPrec := Strata.Sarif.instReprLevel.repr }

def Strata.Sarif.instReprLevel.repr : Level → Nat → Std.Format

Equations

• Strata.Sarif.instReprLevel.repr Strata.Sarif.Level.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.Sarif.Level.none")).group prec✝
• Strata.Sarif.instReprLevel.repr Strata.Sarif.Level.note prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.Sarif.Level.note")).group prec✝
• Strata.Sarif.instReprLevel.repr Strata.Sarif.Level.warning prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.Sarif.Level.warning")).group prec✝
• Strata.Sarif.instReprLevel.repr Strata.Sarif.Level.error prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.Sarif.Level.error")).group prec✝

instance Strata.Sarif.instDecidableEqLevel : DecidableEq Level

Equations

• Strata.Sarif.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Strata.Sarif.instToStringLevel : ToString Level

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instToJsonLevel : Lean.ToJson Level

Equations

• Strata.Sarif.instToJsonLevel = { toJson := fun (level : Strata.Sarif.Level) => Lean.Json.str (toString level) }

instance Strata.Sarif.instFromJsonLevel : Lean.FromJson Level

Equations

• One or more equations did not get rendered due to their size.

structure Strata.Sarif.Result : Type

SARIF result representing a single verification result

• ruleId : String

  Stable identifier of the rule that was evaluated to produce the result -

• level : Level
• message : Message
• locations : Array SarifLocation

def Strata.Sarif.instReprResult.repr : Result → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprResult : Repr Result

Equations

• Strata.Sarif.instReprResult = { reprPrec := Strata.Sarif.instReprResult.repr }

instance Strata.Sarif.instToJsonResult : Lean.ToJson Result

Equations

• Strata.Sarif.instToJsonResult = { toJson := Strata.Sarif.instToJsonResult.toJson }

def Strata.Sarif.instToJsonResult.toJson : Result → Lean.Json

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instFromJsonResult : Lean.FromJson Result

Equations

• Strata.Sarif.instFromJsonResult = { fromJson? := Strata.Sarif.instFromJsonResult.fromJson }

def Strata.Sarif.instFromJsonResult.fromJson : Lean.Json → Except String Result

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instDecidableEqResult : DecidableEq Result

Equations

• Strata.Sarif.instDecidableEqResult = Strata.Sarif.instDecidableEqResult.decEq

def Strata.Sarif.instDecidableEqResult.decEq (x✝ x✝¹ : Result) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instInhabitedResult : Inhabited Result

Equations

• Strata.Sarif.instInhabitedResult = { default := { ruleId := "", level := Strata.Sarif.Level.none, message := { text := "" } } }

structure Strata.Sarif.Driver : Type

SARIF tool driver information

• name : String

  The exact command-line tool in Strata -

• version : String
• informationUri : String

instance Strata.Sarif.instReprDriver : Repr Driver

Equations

• Strata.Sarif.instReprDriver = { reprPrec := Strata.Sarif.instReprDriver.repr }

def Strata.Sarif.instReprDriver.repr : Driver → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instToJsonDriver.toJson : Driver → Lean.Json

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instToJsonDriver : Lean.ToJson Driver

Equations

• Strata.Sarif.instToJsonDriver = { toJson := Strata.Sarif.instToJsonDriver.toJson }

instance Strata.Sarif.instFromJsonDriver : Lean.FromJson Driver

Equations

• Strata.Sarif.instFromJsonDriver = { fromJson? := Strata.Sarif.instFromJsonDriver.fromJson }

def Strata.Sarif.instFromJsonDriver.fromJson : Lean.Json → Except String Driver

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instInhabitedDriver.default : Driver

Equations

• Strata.Sarif.instInhabitedDriver.default = { name := default, version := default, informationUri := default }

instance Strata.Sarif.instInhabitedDriver : Inhabited Driver

Equations

• Strata.Sarif.instInhabitedDriver = { default := Strata.Sarif.instInhabitedDriver.default }

structure Strata.Sarif.Tool : Type

SARIF tool information

• driver : Driver

instance Strata.Sarif.instReprTool : Repr Tool

Equations

• Strata.Sarif.instReprTool = { reprPrec := Strata.Sarif.instReprTool.repr }

def Strata.Sarif.instReprTool.repr : Tool → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instToJsonTool.toJson : Tool → Lean.Json

Equations

• Strata.Sarif.instToJsonTool.toJson x✝ = Lean.Json.mkObj [[("driver", Lean.toJson x✝.driver)]].flatten

instance Strata.Sarif.instToJsonTool : Lean.ToJson Tool

Equations

• Strata.Sarif.instToJsonTool = { toJson := Strata.Sarif.instToJsonTool.toJson }

instance Strata.Sarif.instFromJsonTool : Lean.FromJson Tool

Equations

• Strata.Sarif.instFromJsonTool = { fromJson? := Strata.Sarif.instFromJsonTool.fromJson }

def Strata.Sarif.instFromJsonTool.fromJson : Lean.Json → Except String Tool

Equations

• One or more equations did not get rendered due to their size.

def Strata.Sarif.instInhabitedTool.default : Tool

Equations

• Strata.Sarif.instInhabitedTool.default = { driver := default }

instance Strata.Sarif.instInhabitedTool : Inhabited Tool

Equations

• Strata.Sarif.instInhabitedTool = { default := Strata.Sarif.instInhabitedTool.default }

structure Strata.Sarif.Run : Type

SARIF run representing a single analysis run

• tool : Tool
• results : Array Result

def Strata.Sarif.instReprRun.repr : Run → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprRun : Repr Run

Equations

• Strata.Sarif.instReprRun = { reprPrec := Strata.Sarif.instReprRun.repr }

instance Strata.Sarif.instToJsonRun : Lean.ToJson Run

Equations

• Strata.Sarif.instToJsonRun = { toJson := Strata.Sarif.instToJsonRun.toJson }

def Strata.Sarif.instToJsonRun.toJson : Run → Lean.Json

Equations

• Strata.Sarif.instToJsonRun.toJson x✝ = Lean.Json.mkObj [[("tool", Lean.toJson x✝.tool)], [("results", Lean.toJson x✝.results)]].flatten

def Strata.Sarif.instFromJsonRun.fromJson : Lean.Json → Except String Run

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instFromJsonRun : Lean.FromJson Run

Equations

• Strata.Sarif.instFromJsonRun = { fromJson? := Strata.Sarif.instFromJsonRun.fromJson }

instance Strata.Sarif.instInhabitedRun : Inhabited Run

Equations

• Strata.Sarif.instInhabitedRun = { default := { tool := default, results := #[] } }

structure Strata.Sarif.SarifDocument : Type

Top-level SARIF document

• version : String
• schema : String

  Schema URI as specified by SARIF 2.1.0

• runs : Array Run

def Strata.Sarif.instReprSarifDocument.repr : SarifDocument → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.Sarif.instReprSarifDocument : Repr SarifDocument

Equations

• Strata.Sarif.instReprSarifDocument = { reprPrec := Strata.Sarif.instReprSarifDocument.repr }

def Strata.Sarif.instToJsonSarifDocument.toJson : SarifDocument → Lean.Json

Equations

• Strata.Sarif.instToJsonSarifDocument.toJson x✝ = Lean.Json.mkObj [[("version", Lean.toJson x✝.version)], [("schema", Lean.toJson x✝.schema)], [("runs", Lean.toJson x✝.runs)]].flatten

instance Strata.Sarif.instToJsonSarifDocument : Lean.ToJson SarifDocument

Equations

• Strata.Sarif.instToJsonSarifDocument = { toJson := Strata.Sarif.instToJsonSarifDocument.toJson }

instance Strata.Sarif.instFromJsonSarifDocument : Lean.FromJson SarifDocument

Equations

• Strata.Sarif.instFromJsonSarifDocument = { fromJson? := Strata.Sarif.instFromJsonSarifDocument.fromJson }

def Strata.Sarif.instFromJsonSarifDocument.fromJson : Lean.Json → Except String SarifDocument

Equations

• One or more equations did not get rendered due to their size.

Utility Functions

def Strata.Sarif.locationToSarif (loc : Location) : SarifLocation

Convert a location to SARIF format

Equations

• Strata.Sarif.locationToSarif loc = { physicalLocation := { artifactLocation := { uri := loc.uri }, region := { startLine := loc.startLine, startColumn := loc.startColumn } } }

def Strata.Sarif.toJsonString (sarif : SarifDocument) : String

Convert SARIF document to JSON string

Equations

• Strata.Sarif.toJsonString sarif = (Lean.toJson sarif).compress

def Strata.Sarif.toPrettyJsonString (sarif : SarifDocument) : String

Convert SARIF document to pretty-printed JSON string

Equations

• Strata.Sarif.toPrettyJsonString sarif = (Lean.toJson sarif).pretty