diff --git a/Strata.lean b/Strata.lean index b64f7abbd0..ad1019e907 100644 --- a/Strata.lean +++ b/Strata.lean @@ -17,6 +17,7 @@ import Strata.DL.Lambda.Lambda import Strata.DL.Imperative.Imperative /- Utilities -/ +import Strata.Util.DiagnosticClassifier import Strata.Util.NameProofs import Strata.Util.Sarif diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index 21129ebe39..1fe1ec8dfe 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -390,20 +390,16 @@ public def translateCombinedLaurel (combined : Laurel.Program) let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined (profile := profile) return (coreOption, errors) -/-- Errors from the pyAnalyzeLaurel pipeline. -/ -public inductive PipelineError where - /-- The Python source contains invalid code (bad method name, wrong arguments, etc.). -/ - | userCode (range : SourceRange := .none) (msg : String) - /-- The pipeline encountered a Python construct it intentionally does not yet support. -/ - | knownLimitation (msg : String) - /-- An unexpected failure — likely a bug in the tool itself. -/ - | internal (msg : String) - -public instance : ToString PipelineError where - toString - | .userCode _ msg => s!"User code error: {msg}" - | .knownLimitation msg => s!"Known limitation: {msg}" - | .internal msg => msg +/-- A batch of diagnostics emitted by the pyAnalyzeLaurel pipeline. Routing +to an exit category is driven by each entry's `DiagnosticType` via +`classifyDiagnostics`. -/ +public abbrev PipelineError := List DiagnosticModel + +public def mkUserCodeDiagnostic (filePath : String) (range : SourceRange) (msg : String) + : DiagnosticModel := + { fileRange := { file := .file filePath, range := range } + message := msg + type := .UserError } /-- Run the pyAnalyzeLaurel pipeline: read a Python Ion program, resolve overloads from dispatch files, load PySpec declarations, @@ -430,17 +426,19 @@ public def pythonAndSpecToLaurel (quiet : Bool := false) (warningSummaryFile : Option String := none) : EIO PipelineError Laurel.Program := do + let metadataPath := sourcePath.getD pythonIonPath + let internalErr (msg : String) : PipelineError := + [DiagnosticModel.fromMessage msg (type := .StrataBug)] let stmts ← profileStep profile "Read Python Ion" do match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with | .ok r => pure r - | .error msg => throw (.internal msg) + | .error msg => throw (internalErr msg) let result ← profileStep profile "Resolve and build Laurel prelude" do match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir (quiet := quiet) |>.toBaseIO with | .ok r => pure r - | .error msg => throw (.internal msg) + | .error msg => throw (internalErr msg) - -- Print and write PySpec warnings before later stages can fail let pyspecWarnings := result.pyspecWarnings if pyspecWarnings.size > 0 && !quiet then let _ ← IO.eprintln @@ -468,19 +466,20 @@ public def pythonAndSpecToLaurel let preludeInfo := buildPreludeInfo result - let metadataPath := sourcePath.getD pythonIonPath let (laurelProgram, _ctx) ← profileStep profile "Translate Python to Laurel" do match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with - | .error (.userPythonError range msg) => throw (.userCode range msg) + | .error (.userPythonError range msg) => + throw [mkUserCodeDiagnostic metadataPath range msg] | .error (.unsupportedConstruct msg ast) => - throw (.knownLimitation s!"Unsupported construct: {msg}\nAST: {ast}") - | .error e => throw (.internal s!"Python to Laurel translation failed: {e}") + throw [DiagnosticModel.fromMessage s!"Unsupported construct: {msg}\nAST: {ast}" + (type := .NotYetImplemented)] + | .error e => throw (internalErr s!"Python to Laurel translation failed: {e}") | .ok result => pure result let filteredPrelude ← profileStep profile "Filter prelude" do match Laurel.filterPrelude result.laurelProgram laurelProgram with | .ok prog => pure prog - | .error msg => throw (.internal msg) + | .error msg => throw (internalErr msg) profileStep profile "Combine PySpec and user Laurel" do return combinePySpecLaurel filteredPrelude laurelProgram diff --git a/Strata/Util/DiagnosticClassifier.lean b/Strata/Util/DiagnosticClassifier.lean new file mode 100644 index 0000000000..a85ad507f1 --- /dev/null +++ b/Strata/Util/DiagnosticClassifier.lean @@ -0,0 +1,36 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Util.FileRange + +/-! # Diagnostic Classifier + +Priority order: StrataBug > UserError > NotYetImplemented. +Empty or warnings-only batches fall through to `internalError`. +-/ + +public section +namespace Strata + +inductive DiagnosticOutcome where + | internalError + | userError + | knownLimitation + deriving DecidableEq, Repr, Inhabited + +def classifyDiagnostics (diags : List DiagnosticModel) : DiagnosticOutcome := + if diags.any (fun d => d.type == DiagnosticType.StrataBug) then + .internalError + else if diags.any (fun d => d.type == DiagnosticType.UserError) then + .userError + else if diags.any (fun d => d.type == DiagnosticType.NotYetImplemented) then + .knownLimitation + else + .internalError + +end Strata +end diff --git a/StrataMain.lean b/StrataMain.lean index 179d04a6c0..43d1b6f3b1 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -26,6 +26,7 @@ import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Languages.Laurel.Laurel import Strata.Languages.Core.EntryPoint import Strata.Transform.ProcedureInlining +import Strata.Util.DiagnosticClassifier import Strata.Util.IO import Strata.SimpleAPI @@ -506,6 +507,56 @@ private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do printPyAnalyzeResult "Known limitation" message IO.Process.exit ExitCode.knownLimitation +/-- Render diagnostics through `DiagnosticModel.format` so locations resolve + against the user's source. -/ +private def formatDiagnostics (diags : List DiagnosticModel) + (fileMap : Option Lean.FileMap) : String := + match fileMap with + | none => toString diags + | some _ => + String.intercalate "; " (diags.map (fun d => toString (d.format fileMap))) + +/-- Render a user-code diagnostic as "`msg` at line N, col M". -/ +private def formatUserErrorMessage (d : DiagnosticModel) (fileMap : Option Lean.FileMap) : String := + let location := if d.fileRange.range.isNone then "" else + match fileMap with + | some fm => + let pos := fm.toPosition d.fileRange.range.start + s!" at line {pos.line}, col {pos.column}" + | none => "" + s!"{d.message}{location}" + +/-- Classify `diags` and exit with the matching `pyAnalyzeLaurel` category. + `prefixMsg` is prepended only to internal-error details. -/ +private def classifyDiagnosticsAndExit {α} (prefixMsg : String) + (diags : List DiagnosticModel) (fileMap : Option Lean.FileMap) : IO α := do + let firstOf (t : DiagnosticType) (fmt : DiagnosticModel → String) : String := + match (diags.filter (·.type == t)).head? with + | some d => fmt d + | none => formatDiagnostics diags fileMap + match classifyDiagnostics diags with + | .internalError => + exitPyAnalyzeInternalError s!"{prefixMsg}: {formatDiagnostics diags fileMap}" + | .userError => + exitPyAnalyzeUserError (firstOf .UserError (formatUserErrorMessage · fileMap)) + | .knownLimitation => + exitPyAnalyzeKnownLimitation (firstOf .NotYetImplemented (·.message)) + +/-- Emit SMT `set-info` lines and write `user_errors.txt` for the first + user-code diagnostic in the batch. -/ +private def emitUserErrorsFile (diags : List DiagnosticModel) : IO Unit := do + let some d := (diags.filter (·.type == DiagnosticType.UserError)).head? | pure () + let .file filePath := d.fileRange.file + let range := d.fileRange.range + let mut lines := #[s!"(set-info :file {Strata.escapeSMTStringLit filePath})"] + unless range.isNone do + lines := lines.push s!"(set-info :start {range.start})" + lines := lines.push s!"(set-info :stop {range.stop})" + lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit d.message})" + for line in lines do + IO.println line + IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") + /-- Print the final RESULT/DETAIL lines based on solver outcomes. Always called on successful pipeline completion (as opposed to the exit helpers above, which are called on early pipeline failure). @@ -615,29 +666,10 @@ def pyAnalyzeLaurelCommand : Command where (quiet := quiet) (warningSummaryFile := warningSummaryFile) |>.toBaseIO with | .ok r => pure r - | .error (.userCode range msg) => - let location := if range.isNone then "" else - match mfm with - | some (_, fm) => - let pos := fm.toPosition range.start - s!" at line {pos.line}, col {pos.column}" - | none => "" - let filePath' := sourcePath.getD filePath - let mut lines := #[ - s!"(set-info :file {Strata.escapeSMTStringLit filePath'})" - ] - unless range.isNone do - lines := lines.push s!"(set-info :start {range.start})" - lines := lines.push s!"(set-info :stop {range.stop})" - lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit msg})" - for line in lines do - IO.println line - IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n") - exitPyAnalyzeUserError s!"{msg}{location}" - | .error (.knownLimitation msg) => - exitPyAnalyzeKnownLimitation msg - | .error (.internal msg) => - exitPyAnalyzeInternalError msg + | .error diags => + emitUserErrorsFile diags + let fileMap := mfm.map (·.2) + classifyDiagnosticsAndExit "Python to Laurel translation failed" diags fileMap if verbose then IO.println "\n==== Laurel Program ====" @@ -656,7 +688,10 @@ def pyAnalyzeLaurelCommand : Command where let coreProgram ← match coreProgramOption with | none => - exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}" + emitUserErrorsFile laurelTranslateErrors + let fileMap := mfm.map (·.2) + classifyDiagnosticsAndExit "Laurel to Core translation failed" + laurelTranslateErrors fileMap | some core => pure core if verbose then diff --git a/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected new file mode 100644 index 0000000000..60a198ab8a --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected @@ -0,0 +1,6 @@ +(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py") +(set-info :start 69) +(set-info :stop 77) +(set-info :error-message "calls to procedures are not supported in functions or contracts") +DETAIL: calls to procedures are not supported in functions or contracts at line 5, col 22 +RESULT: User error diff --git a/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected new file mode 100644 index 0000000000..8ee60742df --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected @@ -0,0 +1,4 @@ +(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py") +(set-info :start 69) +(set-info :stop 77) +(set-info :error-message "calls to procedures are not supported in functions or contracts") diff --git a/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py b/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py new file mode 100644 index 0000000000..6937e78589 --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py @@ -0,0 +1,5 @@ +def helper() -> int: + return 0 + +def main(): + assert helper() < helper() < 10, "chained compare with procedure calls" diff --git a/StrataTest/Util/DiagnosticClassifier.lean b/StrataTest/Util/DiagnosticClassifier.lean new file mode 100644 index 0000000000..10839de362 --- /dev/null +++ b/StrataTest/Util/DiagnosticClassifier.lean @@ -0,0 +1,31 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +meta import Strata.Util.DiagnosticClassifier +import Strata.Util.DiagnosticClassifier + +open Strata + +def mkDiag (t : DiagnosticType) : DiagnosticModel := + { fileRange := FileRange.unknown, message := "test", type := t } + +-- Individual arms +#guard classifyDiagnostics [mkDiag .StrataBug] = .internalError +#guard classifyDiagnostics [mkDiag .UserError] = .userError +#guard classifyDiagnostics [mkDiag .NotYetImplemented] = .knownLimitation + +-- Priority: StrataBug > UserError > NotYetImplemented +#guard classifyDiagnostics [mkDiag .UserError, mkDiag .StrataBug] = .internalError +#guard classifyDiagnostics [mkDiag .StrataBug, mkDiag .UserError] = .internalError +#guard classifyDiagnostics [mkDiag .NotYetImplemented, mkDiag .UserError] = .userError +#guard classifyDiagnostics + [mkDiag .NotYetImplemented, mkDiag .UserError, mkDiag .StrataBug] = .internalError + +-- Defensive fallthrough +#guard classifyDiagnostics [] = .internalError +#guard classifyDiagnostics [mkDiag .Warning] = .internalError +#guard classifyDiagnostics [mkDiag .Warning, mkDiag .Warning] = .internalError