Add support for SARIF output to pyAnalyze and pyAnalyzeLaurel

.github/workflows/ci.yml

@@ -91,7 +91,10 @@ jobs:
       - name: Run pyAnalyze tests
         working-directory: StrataTest/Languages/Python
         shell: bash
-        run: ./run_py_analyze.sh
+        run: |
+          ./run_py_analyze.sh
+          python run_py_analyze_sarif.py
+          python run_py_analyze_sarif.py --laurel
 
   lint_checks:
     name: Run lint checks

Strata/Languages/Core/SarifOutput.lean

@@ -85,3 +85,19 @@ def vcResultsToSarif (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResult
     runs := #[run] }
 
 end Core.Sarif
+
+/-- Write SARIF output for verification results to a file.
+    `files` maps source URIs to their file maps for location resolution.
+    `vcResults` are the verification results to encode.
+    `outputPath` is the path to write the SARIF JSON to. -/
+def Core.Sarif.writeSarifOutput
+    (files : Map Strata.Uri Lean.FileMap)
+    (vcResults : Core.VCResults)
+    (outputPath : String) : IO Unit := do
+  let sarifDoc := Core.Sarif.vcResultsToSarif files vcResults
+  let sarifJson := Strata.Sarif.toPrettyJsonString sarifDoc
+  try
+    IO.FS.writeFile outputPath sarifJson
+    IO.println s!"SARIF output written to {outputPath}"
+  catch e =>
+    IO.eprintln s!"Error writing SARIF output to {outputPath}: {e.toString}"

StrataMain.lean

@@ -6,6 +6,7 @@
 
 -- Executable with utilities for working with Strata files.
 import Strata.DDM.Integration.Java.Gen
+import Strata.Languages.Core.SarifOutput
 import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
 import Strata.Languages.Laurel.LaurelToCoreTranslator
 import Strata.Languages.Python.Python
@@ -309,10 +310,12 @@ def tryReadPythonSource (ionPath : String) : IO (Option (String × Lean.FileMap)
 def pyAnalyzeCommand : Command where
   name := "pyAnalyze"
   args := [ "file" ]
-  flags := [{ name := "verbose", help := "Enable verbose output." }]
+  flags := [{ name := "verbose", help := "Enable verbose output." },
+            { name := "sarif", help := "Write results as SARIF to <file>.sarif." }]
   help := "Verify a Python Ion program. Translates to Core, inlines procedures, and runs SMT verification."
   callback := fun v pflags => do
     let verbose := pflags.getBool "verbose"
+    let outputSarif := pflags.getBool "sarif"
     let filePath := v[0]
     let pgm ← readPythonStrata filePath
     -- Try to read the Python source for line number conversion
@@ -384,6 +387,12 @@ def pyAnalyzeCommand : Command where
           | none => ("", "")
         s := s ++ s!"\n{locationPrefix}{vcResult.obligation.label}: {Std.format vcResult.result}{locationSuffix}\n"
       IO.println s
+      -- Output in SARIF format if requested
+      if outputSarif then
+        let files := match pySourceOpt with
+          | some (pyPath, fileMap) => Map.empty.insert (Strata.Uri.file pyPath) fileMap
+          | none => Map.empty
+        Core.Sarif.writeSarifOutput files vcResults (filePath ++ ".sarif")
 
 /-- Result of building the PySpec-augmented prelude. -/
 structure PySpecPrelude where
@@ -451,10 +460,12 @@ def pyAnalyzeLaurelCommand : Command where
             { name := "dispatch",
               help := "Extract overload dispatch table from a \
                 PySpec Ion file (no Laurel translation).",
-              takesArg := .repeat "ion_file" }]
-  help := "Verify a Python Ion program via the Laurel pipeline."
+              takesArg := .repeat "ion_file" },
+            { name := "sarif", help := "Write results as SARIF to <file>.sarif." }]
+  help := "Verify a Python Ion program via the Laurel pipeline. Translates Python to Laurel to Core, then runs SMT verification."
   callback := fun v pflags => do
     let verbose := pflags.getBool "verbose"
+    let outputSarif := pflags.getBool "sarif"
     let filePath := v[0]
     let pgm ← readPythonStrata filePath
     let pySourceOpt ← tryReadPythonSource filePath
@@ -559,6 +570,12 @@ def pyAnalyzeLaurelCommand : Command where
               | none => ("", "")
             s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: {Std.format vcResult.result}{locationSuffix}\n"
           IO.println s
+          -- Output in SARIF format if requested
+          if outputSarif then
+            let files := match pySourceOpt with
+              | some (pyPath, fileMap) => Map.empty.insert (Strata.Uri.file pyPath) fileMap
+              | none => Map.empty
+            Core.Sarif.writeSarifOutput files vcResults (filePath ++ ".sarif")
 
 def javaGenCommand : Command where
   name := "javaGen"

StrataTest/Languages/Python/.gitignore

@@ -1 +1,2 @@
-*.python.st.ion
+*.python.st.ion
+*.sarif

StrataTest/Languages/Python/run_py_analyze_sarif.py

@@ -0,0 +1,93 @@
+#!/usr/bin/env python3
+"""Test SARIF output for pyAnalyze / pyAnalyzeLaurel commands.
+
+Runs pyAnalyze --sarif (or pyAnalyzeLaurel --sarif with --laurel) on selected
+test files and validates the SARIF output.
+Run from StrataTest/Languages/Python/ (same as run_py_analyze.sh).
+"""
+
+import argparse
+import subprocess
+import sys
+from pathlib import Path
+
+from validate_sarif import validate
+
+REPO_ROOT = Path(__file__).resolve().parent.parent.parent.parent
+TEST_DIR = Path(__file__).resolve().parent
+TEST_FILES = sorted(
+    f"tests/{p.name}" for p in (Path(__file__).resolve().parent / "tests").glob("test_*.py")
+)
+SKIP_TESTS = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"}
+SKIP_TESTS_LAUREL = SKIP_TESTS | {"test_class_decl", "test_datetime", "test_strings"}
+
+
+def run(test_file: str, *, laurel: bool) -> bool:
+    test_path = TEST_DIR / test_file
+    if not test_path.exists():
+        return True
+
+    base_name = Path(test_file).stem
+    skip = SKIP_TESTS_LAUREL if laurel else SKIP_TESTS
+    if base_name in skip:
+        print(f"Skipping: {base_name}")
+        return True
+
+    ion_rel = f"StrataTest/Languages/Python/tests/{base_name}.python.st.ion"
+    ion_abs = REPO_ROOT / ion_rel
+    sarif_abs = REPO_ROOT / f"{ion_rel}.sarif"
+
+    cmd_name = "pyAnalyzeLaurel" if laurel else "pyAnalyze"
+    print(f"Testing SARIF output for {cmd_name} {base_name}...")
+
+    # Generate Ion file
+    subprocess.run(
+        [
+            sys.executable, "-m", "strata.gen", "py_to_strata",
+            "--dialect", "dialects/Python.dialect.st.ion",
+            str(test_path),
+            str(ion_abs),
+        ],
+        cwd=REPO_ROOT / "Tools" / "Python",
+        check=True,
+    )
+
+    # Run analysis with --sarif
+    subprocess.run(
+        ["lake", "exe", "strata", cmd_name, "--sarif", ion_rel],
+        cwd=REPO_ROOT,
+        stdout=subprocess.DEVNULL,
+    )
+
+    ok = True
+    if not sarif_abs.exists():
+        print(f"ERROR: SARIF file not created for {base_name} (expected {sarif_abs})")
+        ok = False
+    else:
+        result = validate(str(sarif_abs), base_name, laurel=laurel)
+        if result != "OK":
+            print(f"ERROR: SARIF validation failed for {base_name}: {result}")
+            ok = False
+        else:
+            print(f"Test passed: {base_name}")
+
+    # Clean up generated files
+    ion_abs.unlink(missing_ok=True)
+    sarif_abs.unlink(missing_ok=True)
+    return ok
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description="Test SARIF output for pyAnalyze commands.")
+    parser.add_argument("--laurel", action="store_true", help="Use pyAnalyzeLaurel instead of pyAnalyze")
+    args = parser.parse_args()
+
+    failed = 0
+    for tf in TEST_FILES:
+        if not run(tf, laurel=args.laurel):
+            failed = 1
+    return failed
+
+
+if __name__ == "__main__":
+    sys.exit(main())

StrataTest/Languages/Python/validate_sarif.py

@@ -0,0 +1,67 @@
+#!/usr/bin/env python3
+"""Validate a SARIF file produced by Strata's pyAnalyze --sarif."""
+
+import json
+import sys
+
+
+def validate(sarif_path: str, base_name: str, *, laurel: bool = False) -> str:
+    with open(sarif_path) as f:
+        d = json.load(f)
+
+    errors = []
+    if d.get("version") != "2.1.0":
+        errors.append("wrong version")
+    if "runs" not in d or len(d["runs"]) != 1:
+        errors.append("missing or wrong runs")
+        return "FAIL: " + "; ".join(errors)
+
+    run = d["runs"][0]
+    if run.get("tool", {}).get("driver", {}).get("name") != "Strata":
+        errors.append("wrong tool name")
+    results = run.get("results", [])
+    if len(results) == 0:
+        errors.append("no results")
+    for r in results:
+        if r.get("level") not in ("none", "error", "warning", "note"):
+            errors.append(f"invalid level: {r.get('level')}")
+        if "ruleId" not in r:
+            errors.append("missing ruleId")
+        if "message" not in r or "text" not in r.get("message", {}):
+            errors.append("missing message text")
+
+    error_results = [r for r in results if r.get("level") == "error"]
+    located_results = [r for r in results if r.get("locations")]
+
+    if base_name == "test_precondition_verification":
+        if laurel:
+            # Laurel path produces "unknown" (warning) instead of "fail" (error)
+            warning_results = [r for r in results if r.get("level") == "warning"]
+            if len(warning_results) < 1:
+                errors.append(
+                    f"expected warnings, got {len(warning_results)} warning-level results"
+                )
+        else:
+            if len(error_results) < 1:
+                errors.append(
+                    f"expected failures, got {len(error_results)} error-level results"
+                )
+
+    if base_name == "test_arithmetic":
+        if len(error_results) != 0:
+            errors.append(f"expected 0 errors, got {len(error_results)}")
+        if len(located_results) < 1:
+            errors.append(
+                f"expected results with locations, got {len(located_results)}"
+            )
+
+    return "FAIL: " + "; ".join(errors) if errors else "OK"
+
+
+if __name__ == "__main__":
+    if len(sys.argv) != 3:
+        print(f"Usage: {sys.argv[0]} <sarif_path> <base_name>", file=sys.stderr)
+        sys.exit(2)
+    result = validate(sys.argv[1], sys.argv[2])
+    print(result)
+    sys.exit(0 if result == "OK" else 1)

StrataVerify.lean

@@ -129,14 +129,7 @@ def main (args : List String) : IO UInt32 := do
             -- 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
-              IO.FS.writeFile sarifFile sarifJson
-              println! f!"SARIF output written to {sarifFile}"
-            catch e =>
-              println! f!"Error writing SARIF output to {sarifFile}: {e.toString}"
+            Core.Sarif.writeSarifOutput files vcResults (file ++ ".sarif")
 
         -- Also output standard format
         for vcResult in vcResults do