From 024611ec49293264462235e6b9205e3d9ec3559c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 14 May 2026 16:51:36 +0000 Subject: [PATCH 1/6] feat: split StrataMain.lean into importable library and thin exe root (#1163) Extract all command definitions, helpers, and dispatch logic into StrataMainLib.lean (a lean_lib that downstream packages can import). StrataMain.lean becomes a thin executable root that imports StrataMainLib and calls runCommandMap. Parameterize pyAnalyzeCommand and pyAnalyzeLaurelCommand with moreFns (the Lambda.Factory extension point) so downstream users can plug in custom solver backends without copying the entire file. Add runCommandMap as the shared dispatcher entry point. --- StrataMain.lean | 1065 +------------------------------------------ StrataMainLib.lean | 1071 ++++++++++++++++++++++++++++++++++++++++++++ lakefile.toml | 5 +- 3 files changed, 1079 insertions(+), 1062 deletions(-) create mode 100644 StrataMainLib.lean diff --git a/StrataMain.lean b/StrataMain.lean index 19141a75a4..961d5007d1 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -3,1065 +3,8 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +import StrataMainLib --- Executable with utilities for working with Strata files. -import Strata.DDM.Integration.Java.Gen -import Strata.Languages.Core.Options -import Strata.Languages.Core.SarifOutput -import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator -import Strata.Languages.Laurel.LaurelToCoreTranslator -import Strata.Languages.Python.Python -import Strata.Languages.Python.PySpecPipeline -import Strata.Languages.Python.Specs -import Strata.Languages.Python.Specs.DDM -import Strata.Languages.Python.Specs.IdentifyOverloads -import Strata.Languages.Python.Specs.ToLaurel -import Strata.Languages.Laurel.LaurelFormat -import Strata.Languages.Laurel.Laurel -import Strata.Transform.ProcedureInlining -import Strata.Languages.Python.CorePrelude -import Strata.Languages.Python.PythonRuntimeLaurelPart -import Strata.Languages.Python.PythonLaurelCorePrelude -import Strata.Backends.CBMC.CollectSymbols -import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline - -import Strata.SimpleAPI - -open Strata - -open Core (VerifyOptions VerboseMode VerificationMode CheckLevel) - -def exitFailure {α} (message : String) (hint : String := "strata --help") : IO α := do - IO.eprintln s!"Exception: {message}\n\nRun {hint} for additional help." - IO.Process.exit 1 - -/-- Exit with code 1 for user code errors (detected bugs in the Python source). -/ -def exitUserCodeError {α} (message : String) : IO α := do - IO.eprintln s!"❌ {message}" - IO.Process.exit 1 - -/-- Exit with code 2 for internal errors (tool limitations or crashes). -/ -def exitInternalError {α} (message : String) : IO α := do - IO.eprintln s!"Exception: {message}" - IO.Process.exit 2 - -def exitCmdFailure {α} (cmdName : String) (message : String) : IO α := - exitFailure message (hint := s!"strata {cmdName} --help") - -/-- How a flag consumes arguments. -/ -inductive FlagArg where - | none -- boolean flag, e.g. --verbose - | arg (name : String) -- takes one value, e.g. --output - | repeat (name : String) -- takes one value, may appear multiple times, e.g. --include - -/-- A flag that a command accepts. -/ -structure Flag where - name : String -- flag name without "--", used as lookup key - help : String - takesArg : FlagArg := .none - -/-- Parsed flags from the command line. -/ -structure ParsedFlags where - flags : Std.HashMap String (Option String) := {} - repeated : Std.HashMap String (Array String) := {} - -namespace ParsedFlags - -def getBool (pf : ParsedFlags) (name : String) : Bool := - pf.flags.contains name - -def getString (pf : ParsedFlags) (name : String) : Option String := - match pf.flags[name]? with - | some (some v) => some v - | _ => Option.none - -def getRepeated (pf : ParsedFlags) (name : String) : Array String := - pf.repeated[name]?.getD #[] - -def insertFlag (pf : ParsedFlags) (name : String) (value : Option String) : ParsedFlags := - { pf with flags := pf.flags.insert name value } - -def insertRepeated (pf : ParsedFlags) (name : String) (value : String) : ParsedFlags := - let arr := pf.repeated[name]?.getD #[] - { pf with repeated := pf.repeated.insert name (arr.push value) } - -def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do - let preloaded := Strata.Elab.LoadedDialects.builtin - |>.addDialect! Strata.Python.Python - |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs - |>.addDialect! Strata.Core - |>.addDialect! Strata.Laurel.Laurel - |>.addDialect! Strata.smtReservedKeywordsDialect - |>.addDialect! Strata.SMTCore - |>.addDialect! Strata.SMT - |>.addDialect! Strata.SMTResponse - let mut sp ← Strata.DialectFileMap.new preloaded - for path in pflags.getRepeated "include" do - match ← sp.add path |>.toBaseIO with - | .error msg => exitFailure msg - | .ok sp' => sp := sp' - return sp - -end ParsedFlags - -def parseCheckMode (pflags : ParsedFlags) : IO VerificationMode := - match pflags.getString "check-mode" with - | .none => pure .deductive - | .some s => match VerificationMode.ofString? s with - | .some m => pure m - | .none => exitFailure s!"Invalid check mode: '{s}'. Must be {VerificationMode.options}." - -def parseCheckLevel (pflags : ParsedFlags) : IO CheckLevel := - match pflags.getString "check-level" with - | .none => pure .minimal - | .some s => match CheckLevel.ofString? s with - | .some l => pure l - | .none => exitFailure s!"Invalid check level: '{s}'. Must be {CheckLevel.options}." - -def checkModeFlag : Flag := - { name := "check-mode", - help := s!"Check mode: {VerificationMode.options}. Default: 'deductive'.", - takesArg := .arg "mode" } - -def checkLevelFlag : Flag := - { name := "check-level", - help := s!"Check level: {CheckLevel.options}. Default: 'minimal'.", - takesArg := .arg "level" } - -structure Command where - name : String - args : List String - flags : List Flag := [] - help : String - callback : Vector String args.length → ParsedFlags → IO Unit - -def includeFlag : Flag := - { name := "include", help := "Add a dialect search path.", takesArg := .repeat "path" } - -def checkCommand : Command where - name := "check" - args := [ "file" ] - flags := [includeFlag] - help := "Parse and validate a Strata file (text or Ion). Reports errors and exits." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let _ ← Strata.readStrataFile fm v[0] - -def toIonCommand : Command where - name := "toIon" - args := [ "input", "output" ] - flags := [includeFlag] - help := "Convert a Strata text file to Ion binary format." - callback := fun v pflags => do - let searchPath ← pflags.buildDialectFileMap - let pd ← Strata.readStrataFile searchPath v[0] - match pd with - | .dialect d => - IO.FS.writeBinFile v[1] d.toIon - | .program pgm => - IO.FS.writeBinFile v[1] pgm.toIon - -def printCommand : Command where - name := "print" - args := [ "file" ] - flags := [includeFlag] - help := "Pretty-print a Strata file (text or Ion) to stdout." - callback := fun v pflags => do - let searchPath ← pflags.buildDialectFileMap - -- Special case for already loaded dialects. - let ld ← searchPath.getLoaded - if mem : v[0] ∈ ld.dialects then - IO.print <| ld.dialects.format v[0] mem - return - let pd ← Strata.readStrataFile searchPath v[0] - match pd with - | .dialect d => - let ld ← searchPath.getLoaded - let .isTrue mem := inferInstanceAs (Decidable (d.name ∈ ld.dialects)) - | exitFailure "Internal error reading file." - IO.print <| ld.dialects.format d.name mem - | .program pgm => - IO.print <| toString pgm - -def diffCommand : Command where - name := "diff" - args := [ "file1", "file2" ] - flags := [includeFlag] - help := "Compare two program files for syntactic equality. Reports the first difference found." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let p1 ← Strata.readStrataFile fm v[0] - let p2 ← Strata.readStrataFile fm v[1] - match p1, p2 with - | .program p1, .program p2 => - if p1.dialect != p2.dialect then - exitFailure s!"Dialects differ: {p1.dialect} and {p2.dialect}" - let Decidable.isTrue eq := inferInstanceAs (Decidable (p1.commands.size = p2.commands.size)) - | exitFailure s!"Number of commands differ {p1.commands.size} and {p2.commands.size}" - for (c1, c2) in Array.zip p1.commands p2.commands do - if c1 != c2 then - exitFailure s!"Commands differ: {repr c1} and {repr c2}" - | _, _ => - exitFailure "Cannot compare dialect def with another dialect/program." - -def readPythonStrata (strataPath : String) : IO Strata.Program := do - let bytes ← Strata.Util.readBinInputSource strataPath - if ! Ion.isIonFile bytes then - exitFailure s!"pyAnalyze expected Ion file" - match Strata.Program.fromIon Strata.Python.Python_map Strata.Python.Python.name bytes with - | .ok pgm => pure pgm - | .error msg => exitFailure msg - -def pySpecsCommand : Command where - name := "pySpecs" - args := [ "python_path", "strata_path" ] - flags := [ - { name := "quiet", help := "Suppress default logging." }, - { name := "log", help := "Enable logging for an event type.", - takesArg := .repeat "event" }, - { name := "skip", - help := "Skip a top-level definition (module.name). Overloads are kept.", - takesArg := .repeat "name" } - ] - help := "Translate a Python specification (.py) file into Strata DDM Ion format. Creates the output directory if needed. (Experimental)" - callback := fun v pflags => do - let quiet := pflags.getBool "quiet" - let mut events : Std.HashSet String := {} - if !quiet then - events := events.insert "import" - for e in pflags.getRepeated "log" do - events := events.insert e - let skipNames := pflags.getRepeated "skip" - let warningOutput : Strata.WarningOutput := - if quiet then .none else .detail - -- Serialize embedded dialect for Python subprocess - IO.FS.withTempFile fun _handle dialectFile => do - IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon - let r ← Strata.pySpecs (events := events) - (skipNames := skipNames) - (warningOutput := warningOutput) - v[0] v[1] dialectFile |>.toBaseIO - match r with - | .ok () => pure () - | .error msg => exitFailure msg - -def pyTranslateCommand : Command where - name := "pyTranslate" - args := [ "file" ] - help := "Translate a Python Ion program to Core and print the result to stdout." - callback := fun v _ => do - let pgm ← readPythonStrata v[0] - let preludePgm := Strata.Python.Core.prelude - let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm - let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } - IO.print newPgm - -/-- Derive Python source file path from Ion file path. - E.g., "tests/test_foo.python.st.ion" -> "tests/test_foo.py" -/ -def ionPathToPythonPath (ionPath : String) : Option String := - if ionPath.endsWith ".python.st.ion" then - let basePath := ionPath.dropEnd ".python.st.ion".length |>.toString - some (basePath ++ ".py") - else if ionPath.endsWith ".py.ion" then - some (ionPath.dropEnd ".ion".length |>.toString) - else - none - -/-- Try to read Python source file for source location reconstruction -/ -def tryReadPythonSource (ionPath : String) : IO (Option (String × String)) := do - match ionPathToPythonPath ionPath with - | none => return none - | some pyPath => - try - let content ← IO.FS.readFile pyPath - return some (pyPath, content) - catch _ => - return none - -def pyAnalyzeCommand : Command where - name := "pyAnalyze" - args := [ "file" ] - flags := [{ name := "verbose", help := "Enable verbose output." }, - { name := "sarif", help := "Write results as SARIF to .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 - let pySourceOpt ← tryReadPythonSource filePath - if verbose then - IO.print pgm - let preludePgm := Strata.Python.Core.prelude - -- Use the Python source path if available, otherwise fall back to Ion path - let sourcePathForMetadata := match pySourceOpt with - | some (pyPath, _) => pyPath - | none => filePath - let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm sourcePathForMetadata - let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } - if verbose then - IO.print newPgm - match Core.Transform.runProgram (targetProcList := .none) - (Core.ProcedureInlining.inlineCallCmd - (doInline := λ name _ => name ≠ "main")) - newPgm .emp with - | ⟨.error e, _⟩ => panic! e - | ⟨.ok (_changed, newPgm), _⟩ => - if verbose then - IO.println "Inlined: " - IO.print newPgm - let solverName : String := "Strata/Languages/Python/z3_parallel.py" - let verboseMode := VerboseMode.ofBool verbose - let options := - { VerifyOptions.default with - stopOnFirstError := false, - verbose := verboseMode, - removeIrrelevantAxioms := true, - solver := solverName } - let runVerification tempDir := - EIO.toIO - (fun f => IO.Error.userError (toString f)) - (Core.verify newPgm tempDir .none options - (moreFns := Strata.Python.ReFactory)) - let vcResults ← match options.vcDirectory with - | .none => IO.FS.withTempDir runVerification - | .some tempDir => runVerification tempDir - let mfm : Option (String × Lean.FileMap) := match pySourceOpt with - | some (pyPath, srcText) => some (pyPath, .ofString srcText) - | none => none - let mut s := "" - for vcResult in vcResults do - -- Build location string based on available metadata - let (locationPrefix, locationSuffix) := match Imperative.getFileRange vcResult.obligation.metadata with - | some fr => - if fr.range.isNone then ("", "") - else - match mfm with - | some (pyPath, fm) => - -- Check if this metadata is from the Python source (not CorePrelude) - match fr.file with - | .file path => - if path == pyPath then - let pos := fm.toPosition fr.range.start - -- For failures, show at beginning; for passes, show at end - if vcResult.isFailure then - (s!"Assertion failed at line {pos.line}, col {pos.column}: ", "") - else - ("", s!" (at line {pos.line}, col {pos.column})") - else - -- From CorePrelude or other source, show byte offsets - if vcResult.isFailure then - (s!"Assertion failed for prelude: ", "") - else - ("", s!" (in prelude)") - | none => - if vcResult.isFailure then - (s!"Assertion failed at byte offset: ", "") - else - ("", s!" (at byte offset)") - | none => ("", "") - let outcomeStr := vcResult.formatOutcome - s := s ++ s!"\n{locationPrefix}{vcResult.obligation.label}: \ - {outcomeStr}{locationSuffix}\n" - IO.println s - -- Output in SARIF format if requested - if outputSarif then - let files := match mfm with - | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm - | none => Map.empty - Core.Sarif.writeSarifOutput .deductive files vcResults (filePath ++ ".sarif") - -def pyAnalyzeLaurelCommand : Command where - name := "pyAnalyzeLaurel" - args := [ "file" ] - flags := [{ name := "verbose", help := "Enable verbose output." }, - { name := "pyspec", - help := "Add PySpec-derived Laurel declarations.", - takesArg := .repeat "ion_file" }, - { name := "dispatch", - help := "Extract overload dispatch table from a \ - PySpec Ion file (no Laurel translation).", - takesArg := .repeat "ion_file" }, - { name := "sarif", help := "Write results as SARIF to .sarif." }, - { name := "vc-directory", - help := "Store VCs in SMT-Lib format in .", - takesArg := .arg "dir" }, - checkModeFlag, checkLevelFlag] - 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 pySourceOpt ← tryReadPythonSource filePath - - if verbose then - let pgm ← readPythonStrata filePath - IO.println "==== Python AST ====" - IO.print pgm - - let dispatchFiles := pflags.getRepeated "dispatch" - let pyspecFiles := pflags.getRepeated "pyspec" - let sourcePath := pySourceOpt.map (·.1) - -- Build FileMap for source position resolution. - let mfm : Option (String × Lean.FileMap) := match pySourceOpt with - | some (pyPath, srcText) => some (pyPath, .ofString srcText) - | none => none - let combinedLaurel ← - match ← Strata.pyAnalyzeLaurel filePath dispatchFiles pyspecFiles sourcePath |>.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 => "" - exitUserCodeError s!"{msg}{location}" - | .error (.internal msg) => exitInternalError msg - - if verbose then - IO.println "\n==== Laurel Program ====" - IO.println f!"{combinedLaurel}" - - let coreProgram ← - match Strata.translateCombinedLaurel combinedLaurel with - | .error diagnostics => - exitInternalError s!"Laurel to Core translation failed: {diagnostics}" - | .ok (core, _) => pure core - - if verbose then - IO.println "\n==== Core Program ====" - IO.print coreProgram - - -- Verify using Core verifier - let checkMode ← parseCheckMode pflags - let checkLevel ← parseCheckLevel pflags - let baseOptions : VerifyOptions := - { VerifyOptions.default with - stopOnFirstError := false, verbose := .quiet, solver := "z3", - checkMode := checkMode, checkLevel := checkLevel } - let options : VerifyOptions := match pflags.getString "vc-directory" with - | .some dir => { baseOptions with vcDirectory := some (dir : System.FilePath) } - | .none => baseOptions - let vcResults ← - match ← Strata.verifyCore coreProgram options |>.toBaseIO with - | .ok r => pure r - | .error msg => exitInternalError msg - - -- Print results - IO.println "\n==== Verification Results ====" - let mut s := "" - for vcResult in vcResults do - let (locationPrefix, locationSuffix) := match Imperative.getFileRange vcResult.obligation.metadata with - | some fr => - if fr.range.isNone then ("", "") - else - match mfm with - | some (_, fm) => - match fr.file with - | .file "" => - if vcResult.isFailure then - (s!"Assertion failed in prelude file: ", "") - else - ("", s!" (in prelude file)") - | .file path => - let pos := fm.toPosition fr.range.start - if vcResult.isFailure then - (s!"Assertion failed at line {pos.line}, col {pos.column}: ", "") - else - ("", s!" (at line {pos.line}, col {pos.column})") - | none => - if vcResult.isFailure then - (s!"Assertion failed: ", "") - else - ("", "") - | none => ("", "") - let outcomeStr := vcResult.formatOutcome - s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: \ - {outcomeStr}{locationSuffix}\n" - IO.println s - -- Output in SARIF format if requested - if outputSarif then - let files := match mfm with - | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm - | none => Map.empty - Core.Sarif.writeSarifOutput checkMode files vcResults (filePath ++ ".sarif") - -private def deriveBaseName (file : String) : String := - let name := System.FilePath.fileName file |>.getD file - if name.endsWith ".python.st.ion" then (name.dropEnd 14).toString - else if name.endsWith ".py.ion" then (name.dropEnd 7).toString - else if name.endsWith ".st.ion" then (name.dropEnd 7).toString - else if name.endsWith ".st" then (name.dropEnd 3).toString - else name - -def pyAnalyzeToGotoCommand : Command where - name := "pyAnalyzeToGoto" - args := [ "file" ] - help := "Translate a Strata Python Ion file to CProver GOTO JSON files." - callback := fun v _ => do - let filePath := v[0] - let pgm ← readPythonStrata filePath - let pySourceOpt ← tryReadPythonSource filePath - let preludePgm := Strata.Python.Core.prelude - let sourcePathForMetadata := match pySourceOpt with - | some (pyPath, _) => pyPath - | none => filePath - let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm sourcePathForMetadata - let sourceText := pySourceOpt.map (·.2) - let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } - match Core.Transform.runProgram (targetProcList := .none) - (Core.ProcedureInlining.inlineCallCmd - (doInline := λ name _ => name ≠ "main")) - newPgm .emp with - | ⟨.error e, _⟩ => panic! e - | ⟨.ok (_changed, newPgm), _⟩ => - -- Type-check the full program (registers Python types like ExceptOrNone) - let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } - let Env := Lambda.TEnv.default - let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env newPgm with - | .ok r => pure r - | .error e => panic! s!"{e.format none}" - -- Find the main procedure - let some mainDecl := tcPgm.decls.find? fun d => - match d with - | .proc p _ => Core.CoreIdent.toPretty p.header.name == "main" - | _ => false - | panic! "No main procedure found" - let some p := mainDecl.getProc? - | panic! "main is not a procedure" - -- Translate procedure to GOTO (mirrors CoreToGOTO.transformToGoto post-typecheck logic) - let baseName := deriveBaseName filePath - let procName := Core.CoreIdent.toPretty p.header.name - let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? - let distincts := tcPgm.decls.filterMap fun d => match d with - | .distinct name es _ => some (name, es) | _ => none - match procedureToGotoCtx Env p sourceText (axioms := axioms) (distincts := distincts) - (varTypes := tcPgm.getVarTy?) with - | .error e => panic! s!"{e}" - | .ok (ctx, liftedFuncs) => - let extraSyms ← match collectExtraSymbols tcPgm with - | .ok s => pure (Lean.toJson s) - | .error e => panic! s!"{e}" - let (symtab, goto) ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms - let symTabFile := s!"{baseName}.symtab.json" - let gotoFile := s!"{baseName}.goto.json" - IO.FS.writeFile symTabFile symtab.pretty - IO.FS.writeFile gotoFile goto.pretty - IO.println s!"Written {symTabFile} and {gotoFile}" - -def pyTranslateLaurelCommand : Command where - name := "pyTranslateLaurel" - args := [ "file" ] - flags := [{ name := "pyspec", - help := "Add PySpec-derived Laurel declarations.", - takesArg := .repeat "ion_file" }, - { name := "dispatch", - help := "Extract overload dispatch table from a \ - PySpec Ion file (no Laurel translation).", - takesArg := .repeat "ion_file" }] - help := "Translate a Strata Python Ion file through Laurel to Strata Core. Write results to stdout." - callback := fun v pflags => do - let dispatchFiles := pflags.getRepeated "dispatch" - let pyspecFiles := pflags.getRepeated "pyspec" - let coreProgram ← - match ← Strata.pyTranslateLaurel v[0] dispatchFiles pyspecFiles |>.toBaseIO with - | .ok r => pure r - | .error msg => exitFailure msg - IO.print coreProgram - -def pyAnalyzeLaurelToGotoCommand : Command where - name := "pyAnalyzeLaurelToGoto" - args := [ "file" ] - flags := [{ name := "pyspec", - help := "Add PySpec-derived Laurel declarations.", - takesArg := .repeat "ion_file" }, - { name := "dispatch", - help := "Extract overload dispatch table from a \ - PySpec Ion file (no Laurel translation).", - takesArg := .repeat "ion_file" }] - help := "Translate a Strata Python Ion file through Laurel to CProver GOTO JSON files." - callback := fun v pflags => do - let filePath := v[0] - let dispatchFiles := pflags.getRepeated "dispatch" - let pyspecFiles := pflags.getRepeated "pyspec" - let coreProgram ← - match ← Strata.pyTranslateLaurel filePath dispatchFiles pyspecFiles |>.toBaseIO with - | .ok r => pure r - | .error msg => exitFailure msg - let sourceText := (← tryReadPythonSource filePath).map (·.2) - let baseName := deriveBaseName filePath - match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText |>.toBaseIO with - | .ok () => pure () - | .error msg => exitFailure msg - -def javaGenCommand : Command where - name := "javaGen" - args := [ "dialect", "package", "output-dir" ] - flags := [includeFlag] - help := "Generate Java source files from a DDM dialect definition. Accepts a dialect name (e.g. Laurel) or a dialect file path." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let ld ← fm.getLoaded - let d ← if mem : v[0] ∈ ld.dialects then - pure ld.dialects[v[0]] - else - match ← Strata.readStrataFile fm v[0] with - | .dialect d => pure d - | .program _ => exitFailure "Expected a dialect file, not a program file." - match Strata.Java.generateDialect d v[1] with - | .ok files => - Strata.Java.writeJavaFiles v[2] v[1] files - IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.packageToPath v[1]}" - | .error msg => - exitFailure s!"Error generating Java: {msg}" - -def laurelVerifyOptions : VerifyOptions := { VerifyOptions.default with solver := "z3" } - -def deserializeIonToLaurelFiles (bytes : ByteArray) : IO (List Strata.StrataFile) := do - match Strata.Program.filesFromIon Strata.Laurel.Laurel_map bytes with - | .ok files => pure files - | .error msg => exitFailure msg - -def laurelAnalyzeBinaryCommand : Command where - name := "laurelAnalyzeBinary" - args := [] - help := "Verify Laurel Ion programs read from stdin and print diagnostics. Combines multiple input files." - callback := fun _ _ => do - -- Read bytes from stdin - let stdinBytes ← (← IO.getStdin).readBinToEnd - - let strataFiles ← deserializeIonToLaurelFiles stdinBytes - - let mut combinedProgram : Strata.Laurel.Program := { - staticProcedures := [] - staticFields := [] - types := [] - } - - for strataFile in strataFiles do - - let transResult := Strata.Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Strata.Laurel.parseProgram strataFile.program) - match transResult with - | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}" - | .ok laurelProgram => - - combinedProgram := { - staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures - staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields - types := combinedProgram.types ++ laurelProgram.types - } - - let diagnostics ← Strata.Laurel.verifyToDiagnosticModels combinedProgram laurelVerifyOptions - - IO.println s!"==== DIAGNOSTICS ====" - for diag in diagnostics do - IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}" - -def pySpecToLaurelCommand : Command where - name := "pySpecToLaurel" - args := [ "python_path", "strata_path" ] - help := "Translate a PySpec Ion file to Laurel declarations. The Ion file must already exist." - callback := fun v _ => do - let pythonFile : System.FilePath := v[0] - let strataDir : System.FilePath := v[1] - let some mod := pythonFile.fileStem - | exitFailure s!"No stem {pythonFile}" - let .ok mod := Strata.Python.Specs.ModuleName.ofString mod - | exitFailure s!"Invalid module {mod}" - let ionFile := strataDir / mod.strataFileName - let sigs ← - match ← Strata.Python.Specs.readDDM ionFile |>.toBaseIO with - | .ok t => pure t - | .error msg => exitFailure s!"Could not read {ionFile}: {msg}" - let result := Strata.Python.Specs.ToLaurel.signaturesToLaurel pythonFile sigs - if result.errors.size > 0 then - IO.eprintln s!"{result.errors.size} translation warning(s):" - for err in result.errors do - IO.eprintln s!" {err.file}: {err.message}" - let pgm := result.program - IO.println s!"Laurel: {pgm.staticProcedures.length} procedure(s), {pgm.types.length} type(s)" - IO.println s!"Overloads: {result.overloads.size} function(s)" - for td in pgm.types do - IO.println s!" {Strata.Laurel.formatTypeDefinition td}" - for proc in pgm.staticProcedures do - IO.println s!" {Strata.Laurel.formatProcedure proc}" - -def pyResolveOverloadsCommand : Command where - name := "pyResolveOverloads" - args := [ "python_path", "dispatch_ion" ] - help := "Identify which overloaded service modules a \ - Python program uses. Prints one module name per \ - line to stdout." - callback := fun v _ => do - let pythonFile : System.FilePath := v[0] - let dispatchPath := v[1] - -- Read dispatch overload table - let overloads ← - match ← readDispatchOverloads #[dispatchPath] |>.toBaseIO with - | .ok r => pure r - | .error msg => exitFailure msg - -- Convert .py to Python AST - let stmts ← - IO.FS.withTempFile fun _handle dialectFile => do - IO.FS.writeBinFile dialectFile - Strata.Python.Python.toIon - match ← Strata.Python.pythonToStrata dialectFile pythonFile |>.toBaseIO with - | .ok s => pure s - | .error msg => exitFailure msg - -- Walk AST and collect modules - let state := - Strata.Python.Specs.IdentifyOverloads.resolveOverloads - overloads stmts - for w in state.warnings do - IO.eprintln s!"warning: {w}" - let sorted := state.modules.toArray.qsort (· < ·) - for m in sorted do - IO.println m - -def laurelParseCommand : Command where - name := "laurelParse" - args := [ "file" ] - help := "Parse a Laurel source file (no verification)." - callback := fun v _ => do - let path : System.FilePath := v[0] - let content ← IO.FS.readFile path - let input := Strata.Parser.stringInputContext path content - let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] - let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input - - let uri := Strata.Uri.file path.toString - let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) - match transResult with - | .error transErrors => exitFailure s!"Translation errors: {transErrors}" - | .ok _ => IO.println "Parse successful" - -def laurelAnalyzeCommand : Command where - name := "laurelAnalyze" - args := [ "file" ] - help := "Analyze a Laurel source file. Write diagnostics to stdout." - callback := fun v _ => do - let path : System.FilePath := v[0] - let content ← IO.FS.readFile path - let input := Strata.Parser.stringInputContext path content - let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] - let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input - - let uri := Strata.Uri.file path.toString - let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) - match transResult with - | .error transErrors => exitFailure s!"Translation errors: {transErrors}" - | .ok laurelProgram => - let results ← Strata.Laurel.verifyToVcResults laurelProgram laurelVerifyOptions - match results with - | .error errors => - IO.println s!"==== ERRORS ====" - for err in errors do - IO.println s!"{err.message}" - | .ok vcResults => - IO.println s!"==== RESULTS ====" - for vc in vcResults do - IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => e}" - -def laurelAnalyzeToGotoCommand : Command where - name := "laurelAnalyzeToGoto" - args := [ "file" ] - help := "Translate a Laurel source file to CProver GOTO JSON files." - callback := fun v _ => do - let path : System.FilePath := v[0] - let content ← IO.FS.readFile path - let input := Strata.Parser.stringInputContext path content - let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] - let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input - - let uri := Strata.Uri.file path.toString - let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) - match transResult with - | .error transErrors => exitFailure s!"Translation errors: {transErrors}" - | .ok laurelProgram => - match Strata.Laurel.translate {} laurelProgram with - | .error diags => exitFailure s!"Core translation errors: {diags.map (·.message)}" - | .ok coreProgram => - let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } - let Env := Lambda.TEnv.default - let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env coreProgram.fst with - | .ok r => pure r - | .error e => panic! s!"{e.format none}" - let procs := tcPgm.decls.filterMap fun d => d.getProc? - let funcs := tcPgm.decls.filterMap fun d => - match d.getFunc? with - | some f => - let name := Core.CoreIdent.toPretty f.name - if f.body.isSome && f.typeArgs.isEmpty - && name != "Int.DivT" && name != "Int.ModT" - then some f else none - | none => none - if procs.isEmpty && funcs.isEmpty then panic! "No procedures or functions found" - let baseName := deriveBaseName path.toString - let typeSyms ← match collectExtraSymbols tcPgm with - | .ok s => pure s - | .error e => panic! s!"{e}" - let typeSymsJson := Lean.toJson typeSyms - let sourceText := some content - let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? - let distincts := tcPgm.decls.filterMap fun d => match d with - | .distinct name es _ => some (name, es) | _ => none - let mut symtabPairs : List (String × Lean.Json) := [] - let mut gotoFns : Array Lean.Json := #[] - let mut allLiftedFuncs : List Core.Function := [] - for p in procs do - let procName := Core.CoreIdent.toPretty p.header.name - match procedureToGotoCtx Env p (sourceText := sourceText) (axioms := axioms) (distincts := distincts) - (varTypes := tcPgm.getVarTy?) with - | .error e => panic! s!"{e}" - | .ok (ctx, liftedFuncs) => - allLiftedFuncs := allLiftedFuncs ++ liftedFuncs - let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx) - match json.symtab with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - match json.goto with - | .obj m => - match m.toList.find? (·.1 == "functions") with - | some (_, .arr fns) => gotoFns := gotoFns ++ fns - | _ => pure () - | _ => pure () - for f in funcs ++ allLiftedFuncs do - let funcName := Core.CoreIdent.toPretty f.name - match functionToGotoCtx Env f with - | .error e => panic! s!"{e}" - | .ok ctx => - let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx) - match json.symtab with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - match json.goto with - | .obj m => - match m.toList.find? (·.1 == "functions") with - | some (_, .arr fns) => gotoFns := gotoFns ++ fns - | _ => pure () - | _ => pure () - match typeSymsJson with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - -- Deduplicate: keep first occurrence of each symbol name (proper function - -- symbols come before basic symbol references from callers) - let mut seen : Std.HashSet String := {} - let mut dedupPairs : List (String × Lean.Json) := [] - for (k, v) in symtabPairs do - if !seen.contains k then - seen := seen.insert k - dedupPairs := dedupPairs ++ [(k, v)] - let symtab := Lean.Json.mkObj dedupPairs - let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)] - let symTabFile := s!"{baseName}.symtab.json" - let gotoFile := s!"{baseName}.goto.json" - IO.FS.writeFile symTabFile symtab.pretty - IO.FS.writeFile gotoFile goto.pretty - IO.println s!"Written {symTabFile} and {gotoFile}" - -def laurelPrintCommand : Command where - name := "laurelPrint" - args := [] - help := "Read Laurel Ion from stdin and print in concrete syntax to stdout." - callback := fun _ _ => do - let stdinBytes ← (← IO.getStdin).readBinToEnd - let strataFiles ← deserializeIonToLaurelFiles stdinBytes - for strataFile in strataFiles do - IO.println s!"// File: {strataFile.filePath}" - let p := strataFile.program - let c := p.formatContext {} - let s := p.formatState - let fmt := p.commands.foldl (init := f!"") fun f cmd => - f ++ (Strata.mformat cmd c s).format - IO.println (fmt.pretty 100) - IO.println "" - -def prettyPrintCore (p : Core.Program) : String := - let decls := p.decls.map fun d => - let s := toString (Std.format d) - -- Add newlines after major sections in procedures - s.replace "preconditions:" "\n preconditions:" - |>.replace "postconditions:" "\n postconditions:" - |>.replace "body:" "\n body:\n " - |>.replace "assert [" "\n assert [" - |>.replace "init (" "\n init (" - |>.replace "while (" "\n while (" - |>.replace "if (" "\n if (" - |>.replace "call [" "\n call [" - |>.replace "else{" "\n else {" - |>.replace "}}" "}\n }" - String.intercalate "\n" decls - -def laurelToCoreCommand : Command where - name := "laurelToCore" - args := [ "file" ] - help := "Translate a Laurel source file to Core and print to stdout." - callback := fun v _ => do - let path : System.FilePath := v[0] - let content ← IO.FS.readFile path - let input := Strata.Parser.stringInputContext path content - let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] - let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input - - let uri := Strata.Uri.file path.toString - let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) - match transResult with - | .error transErrors => exitFailure s!"Translation errors: {transErrors}" - | .ok laurelProgram => - match Strata.Laurel.translate {} laurelProgram with - | .error diags => exitFailure s!"Core translation errors: {diags.map (·.message)}" - | .ok coreProgram => IO.println (prettyPrintCore coreProgram.fst) - -/-- Print a string word-wrapped to `width` columns with `indent` spaces of indentation. -/ -private def printIndented (indent : Nat) (s : String) (width : Nat := 80) : IO Unit := do - let pad := "".pushn ' ' indent - let words := s.splitOn " " |>.filter (!·.isEmpty) - let mut line := pad - let mut first := true - for word in words do - if first then - line := line ++ word - first := false - else if line.length + 1 + word.length > width then - IO.println line - line := pad ++ word - else - line := line ++ " " ++ word - unless line.length ≤ indent do - IO.println line - -structure CommandGroup where - name : String - commands : List Command - commonFlags : List Flag := [] - -def commandGroups : List CommandGroup := [ - { name := "Core" - commands := [checkCommand, toIonCommand, printCommand, diffCommand] - commonFlags := [includeFlag] }, - { name := "Code Generation" - commands := [javaGenCommand] }, - { name := "Python" - commands := [pyAnalyzeCommand, pyAnalyzeLaurelCommand, - pyResolveOverloadsCommand, - pySpecsCommand, pySpecToLaurelCommand, - pyAnalyzeLaurelToGotoCommand, - pyAnalyzeToGotoCommand, - pyTranslateCommand, - pyTranslateLaurelCommand] }, - { name := "Laurel" - commands := [laurelAnalyzeCommand, laurelAnalyzeBinaryCommand, - laurelAnalyzeToGotoCommand, laurelParseCommand, - laurelPrintCommand, laurelToCoreCommand] }, -] - -def commandList : List Command := - commandGroups.foldl (init := []) fun acc g => acc ++ g.commands - -def commandMap : Std.HashMap String Command := - commandList.foldl (init := {}) fun m c => m.insert c.name c - -/-- Print a single flag's name and help text at the given indentation. -/ -private def printFlag (indent : Nat) (flag : Flag) : IO Unit := do - let pad := "".pushn ' ' indent - match flag.takesArg with - | .arg argName | .repeat argName => - IO.println s!"{pad}--{flag.name} <{argName}> {flag.help}" - | .none => - IO.println s!"{pad}--{flag.name} {flag.help}" - -/-- Print help for all command groups. -/ -private def printGlobalHelp : IO Unit := do - IO.println "Usage: strata [flags]...\n" - IO.println "Command-line utilities for working with Strata.\n" - for group in commandGroups do - IO.println s!"{group.name}:" - for cmd in group.commands do - let cmdLine := cmd.args.foldl (init := cmd.name) fun s a => s!"{s} <{a}>" - IO.println s!" {cmdLine}" - printIndented 4 cmd.help - let perCmdFlags := cmd.flags.filter fun f => - !group.commonFlags.any fun cf => cf.name == f.name - if !perCmdFlags.isEmpty then - IO.println "" - IO.println " Flags:" - for flag in perCmdFlags do - printFlag 6 flag - IO.println "" - if !group.commonFlags.isEmpty then - IO.println " Common flags:" - for flag in group.commonFlags do - printFlag 4 flag - IO.println "" - -/-- Print help for a single command. -/ -private def printCommandHelp (cmd : Command) : IO Unit := do - let cmdLine := cmd.args.foldl (init := s!"strata {cmd.name}") fun s a => s!"{s} <{a}>" - let flagSummary := cmd.flags.foldl (init := "") fun s f => - match f.takesArg with - | .arg argName | .repeat argName => s!"{s} [--{f.name} <{argName}>]" - | .none => s!"{s} [--{f.name}]" - IO.println s!"Usage: {cmdLine}{flagSummary}\n" - printIndented 0 cmd.help - if !cmd.flags.isEmpty then - IO.println "\nFlags:" - for flag in cmd.flags do - printFlag 2 flag - -/-- Parse interleaved flags and positional arguments. Returns the collected - positional arguments and parsed flags. -/ -private def parseArgs (cmdName : String) - (flagMap : Std.HashMap String Flag) - (acc : Array String) (pflags : ParsedFlags) - (cmdArgs : List String) : IO (Array String × ParsedFlags) := do - match cmdArgs with - | arg :: cmdArgs => - if arg.startsWith "--" then - let flagName := (arg.drop 2).toString - match flagMap[flagName]? with - | some flag => - match flag.takesArg with - | .none => - parseArgs cmdName flagMap acc (pflags.insertFlag flagName Option.none) cmdArgs - | .arg _ => - let value :: cmdArgs := cmdArgs - | exitCmdFailure cmdName s!"Expected value after {arg}." - parseArgs cmdName flagMap acc (pflags.insertFlag flagName (some value)) cmdArgs - | .repeat _ => - let value :: cmdArgs := cmdArgs - | exitCmdFailure cmdName s!"Expected value after {arg}." - parseArgs cmdName flagMap acc (pflags.insertRepeated flagName value) cmdArgs - | none => - exitCmdFailure cmdName s!"Unknown option {arg}." - else - parseArgs cmdName flagMap (acc.push arg) pflags cmdArgs - | [] => - pure (acc, pflags) - -def main (args : List String) : IO Unit := do - try do - match args with - | ["--help"] => printGlobalHelp - | cmd :: args => - match commandMap[cmd]? with - | none => exitFailure s!"Expected subcommand, got {cmd}." - | some cmd => - -- Handle per-command help before parsing flags. - if args.contains "--help" then - printCommandHelp cmd - return - -- Index the command's flags by name for O(1) lookup during parsing. - let flagMap : Std.HashMap String Flag := - cmd.flags.foldl (init := {}) fun m f => m.insert f.name f - -- Split raw args into positional arguments and parsed flags. - let (args, pflags) ← parseArgs cmd.name flagMap #[] {} args - if p : args.size = cmd.args.length then - cmd.callback ⟨args, p⟩ pflags - else - exitCmdFailure cmd.name s!"{cmd.name} expects {cmd.args.length} argument(s)." - | [] => do - exitFailure "Expected subcommand." - catch e => - exitFailure e.toString +def main (args : List String) : IO Unit := + runCommandMap (commandMap Strata.Python.ReFactory) + (commandGroups Strata.Python.ReFactory) args diff --git a/StrataMainLib.lean b/StrataMainLib.lean new file mode 100644 index 0000000000..52631903a1 --- /dev/null +++ b/StrataMainLib.lean @@ -0,0 +1,1071 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +-- Importable library for the Strata CLI. Downstream packages can import this +-- module to reuse or customize the command definitions. +import Strata.DDM.Integration.Java.Gen +import Strata.Languages.Core.Options +import Strata.Languages.Core.SarifOutput +import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator +import Strata.Languages.Laurel.LaurelToCoreTranslator +import Strata.Languages.Python.Python +import Strata.Languages.Python.PySpecPipeline +import Strata.Languages.Python.Specs +import Strata.Languages.Python.Specs.DDM +import Strata.Languages.Python.Specs.IdentifyOverloads +import Strata.Languages.Python.Specs.ToLaurel +import Strata.Languages.Laurel.LaurelFormat +import Strata.Languages.Laurel.Laurel +import Strata.Transform.ProcedureInlining +import Strata.Languages.Python.CorePrelude +import Strata.Languages.Python.PythonRuntimeLaurelPart +import Strata.Languages.Python.PythonLaurelCorePrelude +import Strata.Backends.CBMC.CollectSymbols +import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline + +import Strata.SimpleAPI + +open Strata + +open Core (VerifyOptions VerboseMode VerificationMode CheckLevel) + +def exitFailure {α} (message : String) (hint : String := "strata --help") : IO α := do + IO.eprintln s!"Exception: {message}\n\nRun {hint} for additional help." + IO.Process.exit 1 + +/-- Exit with code 1 for user code errors (detected bugs in the Python source). -/ +def exitUserCodeError {α} (message : String) : IO α := do + IO.eprintln s!"❌ {message}" + IO.Process.exit 1 + +/-- Exit with code 2 for internal errors (tool limitations or crashes). -/ +def exitInternalError {α} (message : String) : IO α := do + IO.eprintln s!"Exception: {message}" + IO.Process.exit 2 + +def exitCmdFailure {α} (cmdName : String) (message : String) : IO α := + exitFailure message (hint := s!"strata {cmdName} --help") + +/-- How a flag consumes arguments. -/ +inductive FlagArg where + | none -- boolean flag, e.g. --verbose + | arg (name : String) -- takes one value, e.g. --output + | repeat (name : String) -- takes one value, may appear multiple times, e.g. --include + +/-- A flag that a command accepts. -/ +structure Flag where + name : String -- flag name without "--", used as lookup key + help : String + takesArg : FlagArg := .none + +/-- Parsed flags from the command line. -/ +structure ParsedFlags where + flags : Std.HashMap String (Option String) := {} + repeated : Std.HashMap String (Array String) := {} + +namespace ParsedFlags + +def getBool (pf : ParsedFlags) (name : String) : Bool := + pf.flags.contains name + +def getString (pf : ParsedFlags) (name : String) : Option String := + match pf.flags[name]? with + | some (some v) => some v + | _ => Option.none + +def getRepeated (pf : ParsedFlags) (name : String) : Array String := + pf.repeated[name]?.getD #[] + +def insertFlag (pf : ParsedFlags) (name : String) (value : Option String) : ParsedFlags := + { pf with flags := pf.flags.insert name value } + +def insertRepeated (pf : ParsedFlags) (name : String) (value : String) : ParsedFlags := + let arr := pf.repeated[name]?.getD #[] + { pf with repeated := pf.repeated.insert name (arr.push value) } + +def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do + let preloaded := Strata.Elab.LoadedDialects.builtin + |>.addDialect! Strata.Python.Python + |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs + |>.addDialect! Strata.Core + |>.addDialect! Strata.Laurel.Laurel + |>.addDialect! Strata.smtReservedKeywordsDialect + |>.addDialect! Strata.SMTCore + |>.addDialect! Strata.SMT + |>.addDialect! Strata.SMTResponse + let mut sp ← Strata.DialectFileMap.new preloaded + for path in pflags.getRepeated "include" do + match ← sp.add path |>.toBaseIO with + | .error msg => exitFailure msg + | .ok sp' => sp := sp' + return sp + +end ParsedFlags + +def parseCheckMode (pflags : ParsedFlags) : IO VerificationMode := + match pflags.getString "check-mode" with + | .none => pure .deductive + | .some s => match VerificationMode.ofString? s with + | .some m => pure m + | .none => exitFailure s!"Invalid check mode: '{s}'. Must be {VerificationMode.options}." + +def parseCheckLevel (pflags : ParsedFlags) : IO CheckLevel := + match pflags.getString "check-level" with + | .none => pure .minimal + | .some s => match CheckLevel.ofString? s with + | .some l => pure l + | .none => exitFailure s!"Invalid check level: '{s}'. Must be {CheckLevel.options}." + +def checkModeFlag : Flag := + { name := "check-mode", + help := s!"Check mode: {VerificationMode.options}. Default: 'deductive'.", + takesArg := .arg "mode" } + +def checkLevelFlag : Flag := + { name := "check-level", + help := s!"Check level: {CheckLevel.options}. Default: 'minimal'.", + takesArg := .arg "level" } + +structure Command where + name : String + args : List String + flags : List Flag := [] + help : String + callback : Vector String args.length → ParsedFlags → IO Unit + +def includeFlag : Flag := + { name := "include", help := "Add a dialect search path.", takesArg := .repeat "path" } + +def checkCommand : Command where + name := "check" + args := [ "file" ] + flags := [includeFlag] + help := "Parse and validate a Strata file (text or Ion). Reports errors and exits." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let _ ← Strata.readStrataFile fm v[0] + +def toIonCommand : Command where + name := "toIon" + args := [ "input", "output" ] + flags := [includeFlag] + help := "Convert a Strata text file to Ion binary format." + callback := fun v pflags => do + let searchPath ← pflags.buildDialectFileMap + let pd ← Strata.readStrataFile searchPath v[0] + match pd with + | .dialect d => + IO.FS.writeBinFile v[1] d.toIon + | .program pgm => + IO.FS.writeBinFile v[1] pgm.toIon + +def printCommand : Command where + name := "print" + args := [ "file" ] + flags := [includeFlag] + help := "Pretty-print a Strata file (text or Ion) to stdout." + callback := fun v pflags => do + let searchPath ← pflags.buildDialectFileMap + -- Special case for already loaded dialects. + let ld ← searchPath.getLoaded + if mem : v[0] ∈ ld.dialects then + IO.print <| ld.dialects.format v[0] mem + return + let pd ← Strata.readStrataFile searchPath v[0] + match pd with + | .dialect d => + let ld ← searchPath.getLoaded + let .isTrue mem := inferInstanceAs (Decidable (d.name ∈ ld.dialects)) + | exitFailure "Internal error reading file." + IO.print <| ld.dialects.format d.name mem + | .program pgm => + IO.print <| toString pgm + +def diffCommand : Command where + name := "diff" + args := [ "file1", "file2" ] + flags := [includeFlag] + help := "Compare two program files for syntactic equality. Reports the first difference found." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let p1 ← Strata.readStrataFile fm v[0] + let p2 ← Strata.readStrataFile fm v[1] + match p1, p2 with + | .program p1, .program p2 => + if p1.dialect != p2.dialect then + exitFailure s!"Dialects differ: {p1.dialect} and {p2.dialect}" + let Decidable.isTrue eq := inferInstanceAs (Decidable (p1.commands.size = p2.commands.size)) + | exitFailure s!"Number of commands differ {p1.commands.size} and {p2.commands.size}" + for (c1, c2) in Array.zip p1.commands p2.commands do + if c1 != c2 then + exitFailure s!"Commands differ: {repr c1} and {repr c2}" + | _, _ => + exitFailure "Cannot compare dialect def with another dialect/program." + +def readPythonStrata (strataPath : String) : IO Strata.Program := do + let bytes ← Strata.Util.readBinInputSource strataPath + if ! Ion.isIonFile bytes then + exitFailure s!"pyAnalyze expected Ion file" + match Strata.Program.fromIon Strata.Python.Python_map Strata.Python.Python.name bytes with + | .ok pgm => pure pgm + | .error msg => exitFailure msg + +def pySpecsCommand : Command where + name := "pySpecs" + args := [ "python_path", "strata_path" ] + flags := [ + { name := "quiet", help := "Suppress default logging." }, + { name := "log", help := "Enable logging for an event type.", + takesArg := .repeat "event" }, + { name := "skip", + help := "Skip a top-level definition (module.name). Overloads are kept.", + takesArg := .repeat "name" } + ] + help := "Translate a Python specification (.py) file into Strata DDM Ion format. Creates the output directory if needed. (Experimental)" + callback := fun v pflags => do + let quiet := pflags.getBool "quiet" + let mut events : Std.HashSet String := {} + if !quiet then + events := events.insert "import" + for e in pflags.getRepeated "log" do + events := events.insert e + let skipNames := pflags.getRepeated "skip" + let warningOutput : Strata.WarningOutput := + if quiet then .none else .detail + -- Serialize embedded dialect for Python subprocess + IO.FS.withTempFile fun _handle dialectFile => do + IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon + let r ← Strata.pySpecs (events := events) + (skipNames := skipNames) + (warningOutput := warningOutput) + v[0] v[1] dialectFile |>.toBaseIO + match r with + | .ok () => pure () + | .error msg => exitFailure msg + +def pyTranslateCommand : Command where + name := "pyTranslate" + args := [ "file" ] + help := "Translate a Python Ion program to Core and print the result to stdout." + callback := fun v _ => do + let pgm ← readPythonStrata v[0] + let preludePgm := Strata.Python.Core.prelude + let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm + let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } + IO.print newPgm + +/-- Derive Python source file path from Ion file path. + E.g., "tests/test_foo.python.st.ion" -> "tests/test_foo.py" -/ +def ionPathToPythonPath (ionPath : String) : Option String := + if ionPath.endsWith ".python.st.ion" then + let basePath := ionPath.dropEnd ".python.st.ion".length |>.toString + some (basePath ++ ".py") + else if ionPath.endsWith ".py.ion" then + some (ionPath.dropEnd ".ion".length |>.toString) + else + none + +/-- Try to read Python source file for source location reconstruction -/ +def tryReadPythonSource (ionPath : String) : IO (Option (String × String)) := do + match ionPathToPythonPath ionPath with + | none => return none + | some pyPath => + try + let content ← IO.FS.readFile pyPath + return some (pyPath, content) + catch _ => + return none + +def pyAnalyzeCommand (moreFns : @Lambda.Factory Core.CoreLParams) : Command where + name := "pyAnalyze" + args := [ "file" ] + flags := [{ name := "verbose", help := "Enable verbose output." }, + { name := "sarif", help := "Write results as SARIF to .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 + let pySourceOpt ← tryReadPythonSource filePath + if verbose then + IO.print pgm + let preludePgm := Strata.Python.Core.prelude + -- Use the Python source path if available, otherwise fall back to Ion path + let sourcePathForMetadata := match pySourceOpt with + | some (pyPath, _) => pyPath + | none => filePath + let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm sourcePathForMetadata + let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } + if verbose then + IO.print newPgm + match Core.Transform.runProgram (targetProcList := .none) + (Core.ProcedureInlining.inlineCallCmd + (doInline := λ name _ => name ≠ "main")) + newPgm .emp with + | ⟨.error e, _⟩ => panic! e + | ⟨.ok (_changed, newPgm), _⟩ => + if verbose then + IO.println "Inlined: " + IO.print newPgm + let solverName : String := "Strata/Languages/Python/z3_parallel.py" + let verboseMode := VerboseMode.ofBool verbose + let options := + { VerifyOptions.default with + stopOnFirstError := false, + verbose := verboseMode, + removeIrrelevantAxioms := true, + solver := solverName } + let runVerification tempDir := + EIO.toIO + (fun f => IO.Error.userError (toString f)) + (Core.verify newPgm tempDir .none options + (moreFns := moreFns)) + let vcResults ← match options.vcDirectory with + | .none => IO.FS.withTempDir runVerification + | .some tempDir => runVerification tempDir + let mfm : Option (String × Lean.FileMap) := match pySourceOpt with + | some (pyPath, srcText) => some (pyPath, .ofString srcText) + | none => none + let mut s := "" + for vcResult in vcResults do + -- Build location string based on available metadata + let (locationPrefix, locationSuffix) := match Imperative.getFileRange vcResult.obligation.metadata with + | some fr => + if fr.range.isNone then ("", "") + else + match mfm with + | some (pyPath, fm) => + -- Check if this metadata is from the Python source (not CorePrelude) + match fr.file with + | .file path => + if path == pyPath then + let pos := fm.toPosition fr.range.start + -- For failures, show at beginning; for passes, show at end + if vcResult.isFailure then + (s!"Assertion failed at line {pos.line}, col {pos.column}: ", "") + else + ("", s!" (at line {pos.line}, col {pos.column})") + else + -- From CorePrelude or other source, show byte offsets + if vcResult.isFailure then + (s!"Assertion failed for prelude: ", "") + else + ("", s!" (in prelude)") + | none => + if vcResult.isFailure then + (s!"Assertion failed at byte offset: ", "") + else + ("", s!" (at byte offset)") + | none => ("", "") + let outcomeStr := vcResult.formatOutcome + s := s ++ s!"\n{locationPrefix}{vcResult.obligation.label}: \ + {outcomeStr}{locationSuffix}\n" + IO.println s + -- Output in SARIF format if requested + if outputSarif then + let files := match mfm with + | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm + | none => Map.empty + Core.Sarif.writeSarifOutput .deductive files vcResults (filePath ++ ".sarif") + +def pyAnalyzeLaurelCommand (moreFns : @Lambda.Factory Core.CoreLParams) : Command where + name := "pyAnalyzeLaurel" + args := [ "file" ] + flags := [{ name := "verbose", help := "Enable verbose output." }, + { name := "pyspec", + help := "Add PySpec-derived Laurel declarations.", + takesArg := .repeat "ion_file" }, + { name := "dispatch", + help := "Extract overload dispatch table from a \ + PySpec Ion file (no Laurel translation).", + takesArg := .repeat "ion_file" }, + { name := "sarif", help := "Write results as SARIF to .sarif." }, + { name := "vc-directory", + help := "Store VCs in SMT-Lib format in .", + takesArg := .arg "dir" }, + checkModeFlag, checkLevelFlag] + 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 pySourceOpt ← tryReadPythonSource filePath + + if verbose then + let pgm ← readPythonStrata filePath + IO.println "==== Python AST ====" + IO.print pgm + + let dispatchFiles := pflags.getRepeated "dispatch" + let pyspecFiles := pflags.getRepeated "pyspec" + let sourcePath := pySourceOpt.map (·.1) + -- Build FileMap for source position resolution. + let mfm : Option (String × Lean.FileMap) := match pySourceOpt with + | some (pyPath, srcText) => some (pyPath, .ofString srcText) + | none => none + let combinedLaurel ← + match ← Strata.pyAnalyzeLaurel filePath dispatchFiles pyspecFiles sourcePath |>.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 => "" + exitUserCodeError s!"{msg}{location}" + | .error (.internal msg) => exitInternalError msg + + if verbose then + IO.println "\n==== Laurel Program ====" + IO.println f!"{combinedLaurel}" + + let coreProgram ← + match Strata.translateCombinedLaurel combinedLaurel with + | .error diagnostics => + exitInternalError s!"Laurel to Core translation failed: {diagnostics}" + | .ok (core, _) => pure core + + if verbose then + IO.println "\n==== Core Program ====" + IO.print coreProgram + + -- Verify using Core verifier + let checkMode ← parseCheckMode pflags + let checkLevel ← parseCheckLevel pflags + let baseOptions : VerifyOptions := + { VerifyOptions.default with + stopOnFirstError := false, verbose := .quiet, solver := "z3", + checkMode := checkMode, checkLevel := checkLevel } + let options : VerifyOptions := match pflags.getString "vc-directory" with + | .some dir => { baseOptions with vcDirectory := some (dir : System.FilePath) } + | .none => baseOptions + let vcResults ← + match ← Strata.verifyCore coreProgram options moreFns |>.toBaseIO with + | .ok r => pure r + | .error msg => exitInternalError msg + + -- Print results + IO.println "\n==== Verification Results ====" + let mut s := "" + for vcResult in vcResults do + let (locationPrefix, locationSuffix) := match Imperative.getFileRange vcResult.obligation.metadata with + | some fr => + if fr.range.isNone then ("", "") + else + match mfm with + | some (_, fm) => + match fr.file with + | .file "" => + if vcResult.isFailure then + (s!"Assertion failed in prelude file: ", "") + else + ("", s!" (in prelude file)") + | .file path => + let pos := fm.toPosition fr.range.start + if vcResult.isFailure then + (s!"Assertion failed at line {pos.line}, col {pos.column}: ", "") + else + ("", s!" (at line {pos.line}, col {pos.column})") + | none => + if vcResult.isFailure then + (s!"Assertion failed: ", "") + else + ("", "") + | none => ("", "") + let outcomeStr := vcResult.formatOutcome + s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: \ + {outcomeStr}{locationSuffix}\n" + IO.println s + -- Output in SARIF format if requested + if outputSarif then + let files := match mfm with + | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm + | none => Map.empty + Core.Sarif.writeSarifOutput checkMode files vcResults (filePath ++ ".sarif") + +private def deriveBaseName (file : String) : String := + let name := System.FilePath.fileName file |>.getD file + if name.endsWith ".python.st.ion" then (name.dropEnd 14).toString + else if name.endsWith ".py.ion" then (name.dropEnd 7).toString + else if name.endsWith ".st.ion" then (name.dropEnd 7).toString + else if name.endsWith ".st" then (name.dropEnd 3).toString + else name + +def pyAnalyzeToGotoCommand : Command where + name := "pyAnalyzeToGoto" + args := [ "file" ] + help := "Translate a Strata Python Ion file to CProver GOTO JSON files." + callback := fun v _ => do + let filePath := v[0] + let pgm ← readPythonStrata filePath + let pySourceOpt ← tryReadPythonSource filePath + let preludePgm := Strata.Python.Core.prelude + let sourcePathForMetadata := match pySourceOpt with + | some (pyPath, _) => pyPath + | none => filePath + let bpgm := Strata.pythonToCore Strata.Python.coreSignatures pgm preludePgm sourcePathForMetadata + let sourceText := pySourceOpt.map (·.2) + let newPgm : Core.Program := { decls := preludePgm.decls ++ bpgm.decls } + match Core.Transform.runProgram (targetProcList := .none) + (Core.ProcedureInlining.inlineCallCmd + (doInline := λ name _ => name ≠ "main")) + newPgm .emp with + | ⟨.error e, _⟩ => panic! e + | ⟨.ok (_changed, newPgm), _⟩ => + -- Type-check the full program (registers Python types like ExceptOrNone) + let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } + let Env := Lambda.TEnv.default + let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env newPgm with + | .ok r => pure r + | .error e => panic! s!"{e.format none}" + -- Find the main procedure + let some mainDecl := tcPgm.decls.find? fun d => + match d with + | .proc p _ => Core.CoreIdent.toPretty p.header.name == "main" + | _ => false + | panic! "No main procedure found" + let some p := mainDecl.getProc? + | panic! "main is not a procedure" + -- Translate procedure to GOTO (mirrors CoreToGOTO.transformToGoto post-typecheck logic) + let baseName := deriveBaseName filePath + let procName := Core.CoreIdent.toPretty p.header.name + let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? + let distincts := tcPgm.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + match procedureToGotoCtx Env p sourceText (axioms := axioms) (distincts := distincts) + (varTypes := tcPgm.getVarTy?) with + | .error e => panic! s!"{e}" + | .ok (ctx, liftedFuncs) => + let extraSyms ← match collectExtraSymbols tcPgm with + | .ok s => pure (Lean.toJson s) + | .error e => panic! s!"{e}" + let (symtab, goto) ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms + let symTabFile := s!"{baseName}.symtab.json" + let gotoFile := s!"{baseName}.goto.json" + IO.FS.writeFile symTabFile symtab.pretty + IO.FS.writeFile gotoFile goto.pretty + IO.println s!"Written {symTabFile} and {gotoFile}" + +def pyTranslateLaurelCommand : Command where + name := "pyTranslateLaurel" + args := [ "file" ] + flags := [{ name := "pyspec", + help := "Add PySpec-derived Laurel declarations.", + takesArg := .repeat "ion_file" }, + { name := "dispatch", + help := "Extract overload dispatch table from a \ + PySpec Ion file (no Laurel translation).", + takesArg := .repeat "ion_file" }] + help := "Translate a Strata Python Ion file through Laurel to Strata Core. Write results to stdout." + callback := fun v pflags => do + let dispatchFiles := pflags.getRepeated "dispatch" + let pyspecFiles := pflags.getRepeated "pyspec" + let coreProgram ← + match ← Strata.pyTranslateLaurel v[0] dispatchFiles pyspecFiles |>.toBaseIO with + | .ok r => pure r + | .error msg => exitFailure msg + IO.print coreProgram + +def pyAnalyzeLaurelToGotoCommand : Command where + name := "pyAnalyzeLaurelToGoto" + args := [ "file" ] + flags := [{ name := "pyspec", + help := "Add PySpec-derived Laurel declarations.", + takesArg := .repeat "ion_file" }, + { name := "dispatch", + help := "Extract overload dispatch table from a \ + PySpec Ion file (no Laurel translation).", + takesArg := .repeat "ion_file" }] + help := "Translate a Strata Python Ion file through Laurel to CProver GOTO JSON files." + callback := fun v pflags => do + let filePath := v[0] + let dispatchFiles := pflags.getRepeated "dispatch" + let pyspecFiles := pflags.getRepeated "pyspec" + let coreProgram ← + match ← Strata.pyTranslateLaurel filePath dispatchFiles pyspecFiles |>.toBaseIO with + | .ok r => pure r + | .error msg => exitFailure msg + let sourceText := (← tryReadPythonSource filePath).map (·.2) + let baseName := deriveBaseName filePath + match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText |>.toBaseIO with + | .ok () => pure () + | .error msg => exitFailure msg + +def javaGenCommand : Command where + name := "javaGen" + args := [ "dialect", "package", "output-dir" ] + flags := [includeFlag] + help := "Generate Java source files from a DDM dialect definition. Accepts a dialect name (e.g. Laurel) or a dialect file path." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let ld ← fm.getLoaded + let d ← if mem : v[0] ∈ ld.dialects then + pure ld.dialects[v[0]] + else + match ← Strata.readStrataFile fm v[0] with + | .dialect d => pure d + | .program _ => exitFailure "Expected a dialect file, not a program file." + match Strata.Java.generateDialect d v[1] with + | .ok files => + Strata.Java.writeJavaFiles v[2] v[1] files + IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.packageToPath v[1]}" + | .error msg => + exitFailure s!"Error generating Java: {msg}" + +def laurelVerifyOptions : VerifyOptions := { VerifyOptions.default with solver := "z3" } + +def deserializeIonToLaurelFiles (bytes : ByteArray) : IO (List Strata.StrataFile) := do + match Strata.Program.filesFromIon Strata.Laurel.Laurel_map bytes with + | .ok files => pure files + | .error msg => exitFailure msg + +def laurelAnalyzeBinaryCommand : Command where + name := "laurelAnalyzeBinary" + args := [] + help := "Verify Laurel Ion programs read from stdin and print diagnostics. Combines multiple input files." + callback := fun _ _ => do + -- Read bytes from stdin + let stdinBytes ← (← IO.getStdin).readBinToEnd + + let strataFiles ← deserializeIonToLaurelFiles stdinBytes + + let mut combinedProgram : Strata.Laurel.Program := { + staticProcedures := [] + staticFields := [] + types := [] + } + + for strataFile in strataFiles do + + let transResult := Strata.Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Strata.Laurel.parseProgram strataFile.program) + match transResult with + | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}" + | .ok laurelProgram => + + combinedProgram := { + staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures + staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields + types := combinedProgram.types ++ laurelProgram.types + } + + let diagnostics ← Strata.Laurel.verifyToDiagnosticModels combinedProgram laurelVerifyOptions + + IO.println s!"==== DIAGNOSTICS ====" + for diag in diagnostics do + IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}" + +def pySpecToLaurelCommand : Command where + name := "pySpecToLaurel" + args := [ "python_path", "strata_path" ] + help := "Translate a PySpec Ion file to Laurel declarations. The Ion file must already exist." + callback := fun v _ => do + let pythonFile : System.FilePath := v[0] + let strataDir : System.FilePath := v[1] + let some mod := pythonFile.fileStem + | exitFailure s!"No stem {pythonFile}" + let .ok mod := Strata.Python.Specs.ModuleName.ofString mod + | exitFailure s!"Invalid module {mod}" + let ionFile := strataDir / mod.strataFileName + let sigs ← + match ← Strata.Python.Specs.readDDM ionFile |>.toBaseIO with + | .ok t => pure t + | .error msg => exitFailure s!"Could not read {ionFile}: {msg}" + let result := Strata.Python.Specs.ToLaurel.signaturesToLaurel pythonFile sigs + if result.errors.size > 0 then + IO.eprintln s!"{result.errors.size} translation warning(s):" + for err in result.errors do + IO.eprintln s!" {err.file}: {err.message}" + let pgm := result.program + IO.println s!"Laurel: {pgm.staticProcedures.length} procedure(s), {pgm.types.length} type(s)" + IO.println s!"Overloads: {result.overloads.size} function(s)" + for td in pgm.types do + IO.println s!" {Strata.Laurel.formatTypeDefinition td}" + for proc in pgm.staticProcedures do + IO.println s!" {Strata.Laurel.formatProcedure proc}" + +def pyResolveOverloadsCommand : Command where + name := "pyResolveOverloads" + args := [ "python_path", "dispatch_ion" ] + help := "Identify which overloaded service modules a \ + Python program uses. Prints one module name per \ + line to stdout." + callback := fun v _ => do + let pythonFile : System.FilePath := v[0] + let dispatchPath := v[1] + -- Read dispatch overload table + let overloads ← + match ← readDispatchOverloads #[dispatchPath] |>.toBaseIO with + | .ok r => pure r + | .error msg => exitFailure msg + -- Convert .py to Python AST + let stmts ← + IO.FS.withTempFile fun _handle dialectFile => do + IO.FS.writeBinFile dialectFile + Strata.Python.Python.toIon + match ← Strata.Python.pythonToStrata dialectFile pythonFile |>.toBaseIO with + | .ok s => pure s + | .error msg => exitFailure msg + -- Walk AST and collect modules + let state := + Strata.Python.Specs.IdentifyOverloads.resolveOverloads + overloads stmts + for w in state.warnings do + IO.eprintln s!"warning: {w}" + let sorted := state.modules.toArray.qsort (· < ·) + for m in sorted do + IO.println m + +def laurelParseCommand : Command where + name := "laurelParse" + args := [ "file" ] + help := "Parse a Laurel source file (no verification)." + callback := fun v _ => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok _ => IO.println "Parse successful" + +def laurelAnalyzeCommand : Command where + name := "laurelAnalyze" + args := [ "file" ] + help := "Analyze a Laurel source file. Write diagnostics to stdout." + callback := fun v _ => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok laurelProgram => + let results ← Strata.Laurel.verifyToVcResults laurelProgram laurelVerifyOptions + match results with + | .error errors => + IO.println s!"==== ERRORS ====" + for err in errors do + IO.println s!"{err.message}" + | .ok vcResults => + IO.println s!"==== RESULTS ====" + for vc in vcResults do + IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => e}" + +def laurelAnalyzeToGotoCommand : Command where + name := "laurelAnalyzeToGoto" + args := [ "file" ] + help := "Translate a Laurel source file to CProver GOTO JSON files." + callback := fun v _ => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok laurelProgram => + match Strata.Laurel.translate {} laurelProgram with + | .error diags => exitFailure s!"Core translation errors: {diags.map (·.message)}" + | .ok coreProgram => + let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } + let Env := Lambda.TEnv.default + let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env coreProgram.fst with + | .ok r => pure r + | .error e => panic! s!"{e.format none}" + let procs := tcPgm.decls.filterMap fun d => d.getProc? + let funcs := tcPgm.decls.filterMap fun d => + match d.getFunc? with + | some f => + let name := Core.CoreIdent.toPretty f.name + if f.body.isSome && f.typeArgs.isEmpty + && name != "Int.DivT" && name != "Int.ModT" + then some f else none + | none => none + if procs.isEmpty && funcs.isEmpty then panic! "No procedures or functions found" + let baseName := deriveBaseName path.toString + let typeSyms ← match collectExtraSymbols tcPgm with + | .ok s => pure s + | .error e => panic! s!"{e}" + let typeSymsJson := Lean.toJson typeSyms + let sourceText := some content + let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? + let distincts := tcPgm.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + let mut symtabPairs : List (String × Lean.Json) := [] + let mut gotoFns : Array Lean.Json := #[] + let mut allLiftedFuncs : List Core.Function := [] + for p in procs do + let procName := Core.CoreIdent.toPretty p.header.name + match procedureToGotoCtx Env p (sourceText := sourceText) (axioms := axioms) (distincts := distincts) + (varTypes := tcPgm.getVarTy?) with + | .error e => panic! s!"{e}" + | .ok (ctx, liftedFuncs) => + allLiftedFuncs := allLiftedFuncs ++ liftedFuncs + let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx) + match json.symtab with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + match json.goto with + | .obj m => + match m.toList.find? (·.1 == "functions") with + | some (_, .arr fns) => gotoFns := gotoFns ++ fns + | _ => pure () + | _ => pure () + for f in funcs ++ allLiftedFuncs do + let funcName := Core.CoreIdent.toPretty f.name + match functionToGotoCtx Env f with + | .error e => panic! s!"{e}" + | .ok ctx => + let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx) + match json.symtab with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + match json.goto with + | .obj m => + match m.toList.find? (·.1 == "functions") with + | some (_, .arr fns) => gotoFns := gotoFns ++ fns + | _ => pure () + | _ => pure () + match typeSymsJson with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + -- Deduplicate: keep first occurrence of each symbol name (proper function + -- symbols come before basic symbol references from callers) + let mut seen : Std.HashSet String := {} + let mut dedupPairs : List (String × Lean.Json) := [] + for (k, v) in symtabPairs do + if !seen.contains k then + seen := seen.insert k + dedupPairs := dedupPairs ++ [(k, v)] + let symtab := Lean.Json.mkObj dedupPairs + let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)] + let symTabFile := s!"{baseName}.symtab.json" + let gotoFile := s!"{baseName}.goto.json" + IO.FS.writeFile symTabFile symtab.pretty + IO.FS.writeFile gotoFile goto.pretty + IO.println s!"Written {symTabFile} and {gotoFile}" + +def laurelPrintCommand : Command where + name := "laurelPrint" + args := [] + help := "Read Laurel Ion from stdin and print in concrete syntax to stdout." + callback := fun _ _ => do + let stdinBytes ← (← IO.getStdin).readBinToEnd + let strataFiles ← deserializeIonToLaurelFiles stdinBytes + for strataFile in strataFiles do + IO.println s!"// File: {strataFile.filePath}" + let p := strataFile.program + let c := p.formatContext {} + let s := p.formatState + let fmt := p.commands.foldl (init := f!"") fun f cmd => + f ++ (Strata.mformat cmd c s).format + IO.println (fmt.pretty 100) + IO.println "" + +def prettyPrintCore (p : Core.Program) : String := + let decls := p.decls.map fun d => + let s := toString (Std.format d) + -- Add newlines after major sections in procedures + s.replace "preconditions:" "\n preconditions:" + |>.replace "postconditions:" "\n postconditions:" + |>.replace "body:" "\n body:\n " + |>.replace "assert [" "\n assert [" + |>.replace "init (" "\n init (" + |>.replace "while (" "\n while (" + |>.replace "if (" "\n if (" + |>.replace "call [" "\n call [" + |>.replace "else{" "\n else {" + |>.replace "}}" "}\n }" + String.intercalate "\n" decls + +def laurelToCoreCommand : Command where + name := "laurelToCore" + args := [ "file" ] + help := "Translate a Laurel source file to Core and print to stdout." + callback := fun v _ => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok laurelProgram => + match Strata.Laurel.translate {} laurelProgram with + | .error diags => exitFailure s!"Core translation errors: {diags.map (·.message)}" + | .ok coreProgram => IO.println (prettyPrintCore coreProgram.fst) + +/-- Print a string word-wrapped to `width` columns with `indent` spaces of indentation. -/ +private def printIndented (indent : Nat) (s : String) (width : Nat := 80) : IO Unit := do + let pad := "".pushn ' ' indent + let words := s.splitOn " " |>.filter (!·.isEmpty) + let mut line := pad + let mut first := true + for word in words do + if first then + line := line ++ word + first := false + else if line.length + 1 + word.length > width then + IO.println line + line := pad ++ word + else + line := line ++ " " ++ word + unless line.length ≤ indent do + IO.println line + +structure CommandGroup where + name : String + commands : List Command + commonFlags : List Flag := [] + +def commandGroups (moreFns : @Lambda.Factory Core.CoreLParams) : List CommandGroup := [ + { name := "Core" + commands := [checkCommand, toIonCommand, printCommand, diffCommand] + commonFlags := [includeFlag] }, + { name := "Code Generation" + commands := [javaGenCommand] }, + { name := "Python" + commands := [pyAnalyzeCommand moreFns, pyAnalyzeLaurelCommand moreFns, + pyResolveOverloadsCommand, + pySpecsCommand, pySpecToLaurelCommand, + pyAnalyzeLaurelToGotoCommand, + pyAnalyzeToGotoCommand, + pyTranslateCommand, + pyTranslateLaurelCommand] }, + { name := "Laurel" + commands := [laurelAnalyzeCommand, laurelAnalyzeBinaryCommand, + laurelAnalyzeToGotoCommand, laurelParseCommand, + laurelPrintCommand, laurelToCoreCommand] }, +] + +def commandList (moreFns : @Lambda.Factory Core.CoreLParams) : List Command := + (commandGroups moreFns).foldl (init := []) fun acc g => acc ++ g.commands + +def commandMap (moreFns : @Lambda.Factory Core.CoreLParams) : Std.HashMap String Command := + (commandList moreFns).foldl (init := {}) fun m c => m.insert c.name c + +/-- Print a single flag's name and help text at the given indentation. -/ +private def printFlag (indent : Nat) (flag : Flag) : IO Unit := do + let pad := "".pushn ' ' indent + match flag.takesArg with + | .arg argName | .repeat argName => + IO.println s!"{pad}--{flag.name} <{argName}> {flag.help}" + | .none => + IO.println s!"{pad}--{flag.name} {flag.help}" + +/-- Print help for all command groups. -/ +private def printGlobalHelp (groups : List CommandGroup) : IO Unit := do + IO.println "Usage: strata [flags]...\n" + IO.println "Command-line utilities for working with Strata.\n" + for group in groups do + IO.println s!"{group.name}:" + for cmd in group.commands do + let cmdLine := cmd.args.foldl (init := cmd.name) fun s a => s!"{s} <{a}>" + IO.println s!" {cmdLine}" + printIndented 4 cmd.help + let perCmdFlags := cmd.flags.filter fun f => + !group.commonFlags.any fun cf => cf.name == f.name + if !perCmdFlags.isEmpty then + IO.println "" + IO.println " Flags:" + for flag in perCmdFlags do + printFlag 6 flag + IO.println "" + if !group.commonFlags.isEmpty then + IO.println " Common flags:" + for flag in group.commonFlags do + printFlag 4 flag + IO.println "" + +/-- Print help for a single command. -/ +private def printCommandHelp (cmd : Command) : IO Unit := do + let cmdLine := cmd.args.foldl (init := s!"strata {cmd.name}") fun s a => s!"{s} <{a}>" + let flagSummary := cmd.flags.foldl (init := "") fun s f => + match f.takesArg with + | .arg argName | .repeat argName => s!"{s} [--{f.name} <{argName}>]" + | .none => s!"{s} [--{f.name}]" + IO.println s!"Usage: {cmdLine}{flagSummary}\n" + printIndented 0 cmd.help + if !cmd.flags.isEmpty then + IO.println "\nFlags:" + for flag in cmd.flags do + printFlag 2 flag + +/-- Parse interleaved flags and positional arguments. Returns the collected + positional arguments and parsed flags. -/ +private def parseArgs (cmdName : String) + (flagMap : Std.HashMap String Flag) + (acc : Array String) (pflags : ParsedFlags) + (cmdArgs : List String) : IO (Array String × ParsedFlags) := do + match cmdArgs with + | arg :: cmdArgs => + if arg.startsWith "--" then + let flagName := (arg.drop 2).toString + match flagMap[flagName]? with + | some flag => + match flag.takesArg with + | .none => + parseArgs cmdName flagMap acc (pflags.insertFlag flagName Option.none) cmdArgs + | .arg _ => + let value :: cmdArgs := cmdArgs + | exitCmdFailure cmdName s!"Expected value after {arg}." + parseArgs cmdName flagMap acc (pflags.insertFlag flagName (some value)) cmdArgs + | .repeat _ => + let value :: cmdArgs := cmdArgs + | exitCmdFailure cmdName s!"Expected value after {arg}." + parseArgs cmdName flagMap acc (pflags.insertRepeated flagName value) cmdArgs + | none => + exitCmdFailure cmdName s!"Unknown option {arg}." + else + parseArgs cmdName flagMap (acc.push arg) pflags cmdArgs + | [] => + pure (acc, pflags) + +/-- Dispatch CLI arguments against a command map. This is the shared entry point + that both the default executable and downstream custom executables use. -/ +def runCommandMap (map : Std.HashMap String Command) + (groups : List CommandGroup) (args : List String) : IO Unit := do + try do + match args with + | ["--help"] => printGlobalHelp groups + | cmd :: args => + match map[cmd]? with + | none => exitFailure s!"Expected subcommand, got {cmd}." + | some cmd => + -- Handle per-command help before parsing flags. + if args.contains "--help" then + printCommandHelp cmd + return + -- Index the command's flags by name for O(1) lookup during parsing. + let flagMap : Std.HashMap String Flag := + cmd.flags.foldl (init := {}) fun m f => m.insert f.name f + -- Split raw args into positional arguments and parsed flags. + let (args, pflags) ← parseArgs cmd.name flagMap #[] {} args + if p : args.size = cmd.args.length then + cmd.callback ⟨args, p⟩ pflags + else + exitCmdFailure cmd.name s!"{cmd.name} expects {cmd.args.length} argument(s)." + | [] => do + exitFailure "Expected subcommand." + catch e => + exitFailure e.toString diff --git a/lakefile.toml b/lakefile.toml index 867892fd38..795f56bb63 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,6 @@ name = "Strata" version = "0.1.0" -defaultTargets = ["Strata", "strata", "StrataMain", "StrataVerify", "StrataToCBMC", "StrataCoreToGoto"] +defaultTargets = ["Strata", "StrataMainLib", "strata", "StrataMain", "StrataVerify", "StrataToCBMC", "StrataCoreToGoto"] testDriver = "StrataTest" [[require]] @@ -11,6 +11,9 @@ rev = "bump_to_v4.27.0" [[lean_lib]] name = "Strata" +[[lean_lib]] +name = "StrataMainLib" + [[lean_exe]] name = "strata" root = "StrataMain" From 4586b49f7ddcbe8a2e98c70e5dd05879448152bc Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 14 May 2026 17:54:34 +0000 Subject: [PATCH 2/6] feat: parameterize verifyCommand and pyAnalyzeLaurelCommand with mkDischarge Allows downstream executables to plug in a custom solver backend by passing a custom MkDischargeFn to these commands without copying code. --- StrataMainLib.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/StrataMainLib.lean b/StrataMainLib.lean index c6da3da992..036a73fbd9 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -575,7 +575,7 @@ private def deriveBaseName (file : String) : String := | none => name -def pyAnalyzeLaurelCommand : Command where +def pyAnalyzeLaurelCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where name := "pyAnalyzeLaurel" args := [ "file" ] flags := verifyOptionsFlags ++ [ @@ -747,6 +747,7 @@ def pyAnalyzeLaurelCommand : Command where (externalPhases := [Strata.frontEndPhase]) (prefixPhases := inlinePhases) (keepAllFilesPrefix := keepPrefix) + (mkDischarge := mkDischarge) |>.toBaseIO with | .ok r => pure r.mergeByAssertion | .error msg => exitPyAnalyzeInternalError msg @@ -1268,7 +1269,7 @@ def transformCommand : Command where | .ok program => IO.print (Core.formatProgram program) | .error e => exitFailure s!"Transform failed: {e}" -def verifyCommand : Command where +def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where name := "verify" args := [ "file" ] flags := verifyOptionsFlags ++ [ @@ -1337,7 +1338,7 @@ def verifyCommand : Command where else if pgm.dialect == "Boole" then Boole.verify opts.solver pgm inputCtx proceduresToVerify opts else - verify pgm inputCtx proceduresToVerify opts + verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge) catch e => println! f!"{e}" IO.Process.exit ExitCode.internalError From 63d96f78ebcedadb8834c0d3a5e3f81ece617e6f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 14 May 2026 23:40:33 +0000 Subject: [PATCH 3/6] ci: retrigger benchmarks after AWS token expiration From 4fce04dc550aa34409a1d4aaf27c71766775ddf3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 15 May 2026 19:16:01 +0000 Subject: [PATCH 4/6] Remove StrataMainLib.lean and restore StrataMain.lean to full content Preparation for recreating StrataMainLib.lean via git rename for proper change tracking across branches. --- StrataMain.lean | 1566 ++++++++++++++++++++++++++++++++++++++++++- StrataMainLib.lean | 1571 -------------------------------------------- 2 files changed, 1563 insertions(+), 1574 deletions(-) delete mode 100644 StrataMainLib.lean diff --git a/StrataMain.lean b/StrataMain.lean index 826504e67f..9ae4839a21 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -3,7 +3,1567 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import StrataMainLib +module -def main (args : List String) : IO Unit := - runCommandMap commandMap commandGroups args +-- Executable with utilities for working with Strata files. +import Lean.Parser.Extension +import Strata.Backends.CBMC.CollectSymbols +import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline +import Strata.DDM.Integration.Java.Gen +import Strata.Languages.Core.Verifier +import Strata.Languages.Core.SarifOutput +import Strata.Languages.Core.ProgramEval +import Strata.Languages.Core.StatementEval +import Strata.Languages.C_Simp.Verify +import Strata.Languages.B3.Verifier.Program +import Strata.Languages.Laurel.LaurelCompilationPipeline +import Strata.Languages.Boole.Boole +import Strata.Languages.Boole.Verify +import Strata.Languages.Python.Python +import Strata.Languages.Python.Specs.IdentifyOverloads +import Strata.Languages.Python.Specs.ToLaurel +import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator +import Strata.Languages.Laurel.Laurel +import Strata.Languages.Core.EntryPoint +import Strata.Transform.ProcedureInlining +import Strata.Util.IO + +import Strata.SimpleAPI +import Strata.Util.Profile +import Strata.Util.Json +import Strata.DDM.BuiltinDialects +import Strata.DDM.Util.String +import Strata.Languages.Python.PyFactory +import Strata.Languages.Python.Specs +import Strata.Languages.Python.Specs.DDM +import Strata.Languages.Python.ReadPython + +open Strata + +open Core (VerifyOptions VerboseMode VerificationMode CheckLevel EntryPoint) +open Laurel (LaurelVerifyOptions LaurelTranslateOptions) + +/-! ## Exit codes + +All `strata` subcommands use a common exit code scheme: + +| Code | Category | Meaning | +|------|--------------------|-----------------------------------------------------------| +| 0 | Success | Analysis passed, inconclusive, or `--no-solve` completed. | +| 1 | User error | Bad input: invalid arguments, malformed source, etc. | +| 2 | Failures found | Analysis completed and found failures. | +| 3 | Internal error | SMT encoding failure, solver crash, or translation bug. | +| 4 | Known limitation | Intentionally unsupported language construct. | + +Codes 1–2 are **user-actionable** (fix the input or the code under analysis). +Codes 3–4 are **tool-side** (report as a bug or wait for support). +Exit 0 covers success, inconclusive results, and solver timeouts. -/ + +namespace ExitCode + def userError : UInt8 := 1 + def failuresFound : UInt8 := 2 + def internalError : UInt8 := 3 + def knownLimitation : UInt8 := 4 +end ExitCode + +def exitFailure {α} (message : String) (hint : String := "strata --help") : IO α := do + IO.eprintln s!"Exception: {message}\n\nRun {hint} for additional help." + IO.Process.exit ExitCode.userError + +/-- Exit with code 1 for user errors (bad input, malformed source, etc.). -/ +def exitUserError {α} (message : String) : IO α := do + IO.eprintln s!"❌ {message}" + IO.Process.exit ExitCode.userError + +/-- Exit with code 2 for analysis failures found. -/ +def exitFailuresFound {α} (message : String) : IO α := do + IO.eprintln s!"Failures found: {message}" + IO.Process.exit ExitCode.failuresFound + +/-- Exit with code 3 for internal errors (tool limitations or crashes). -/ +def exitInternalError {α} (message : String) : IO α := do + IO.eprintln s!"Exception: {message}" + IO.Process.exit ExitCode.internalError + +/-- Exit with code 4 for known limitations (unsupported constructs). -/ +def exitKnownLimitation {α} (message : String) : IO α := do + IO.eprintln s!"Known limitation: {message}" + IO.Process.exit ExitCode.knownLimitation + +/-- Like `exitFailure` but tailors the help hint to a specific subcommand. -/ +def exitCmdFailure {α} (cmdName : String) (message : String) : IO α := + exitFailure message (hint := s!"strata {cmdName} --help") + +/-- How a flag consumes arguments. -/ +inductive FlagArg where + | none -- boolean flag, e.g. --verbose + | arg (name : String) -- takes one value, e.g. --output + | repeat (name : String) -- takes one value, may appear multiple times, e.g. --include + +/-- A flag that a command accepts. -/ +structure Flag where + name : String -- flag name without "--", used as lookup key + help : String + takesArg : FlagArg := .none + +/-- Parsed flags from the command line. Stored as an ordered array so that + command-line position is preserved (needed by `transform` to bind + `--procedures`/`--functions` to the preceding `--pass`). + For `.arg` flags that appear more than once, `getString` returns the + **last** occurrence (last-writer-wins). -/ +structure ParsedFlags where + entries : Array (String × Option String) := #[] + +namespace ParsedFlags + +def getBool (pf : ParsedFlags) (name : String) : Bool := + pf.entries.any (·.1 == name) + +def getString (pf : ParsedFlags) (name : String) : Option String := + -- Scan from the end so last occurrence wins. + match pf.entries.findRev? (·.1 == name) with + | some (_, some v) => some v + | _ => Option.none + +def getRepeated (pf : ParsedFlags) (name : String) : Array String := + pf.entries.foldl (init := #[]) fun acc (n, v) => + if n == name then match v with | some s => acc.push s | none => acc else acc + +def insert (pf : ParsedFlags) (name : String) (value : Option String) : ParsedFlags := + { pf with entries := pf.entries.push (name, value) } + +def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do + let preloaded := Strata.Elab.LoadedDialects.builtin + |>.addDialect! Strata.Python.Python + |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs + |>.addDialect! Strata.Core + |>.addDialect! Strata.Boole + |>.addDialect! Strata.Laurel.Laurel + |>.addDialect! Strata.smtReservedKeywordsDialect + |>.addDialect! Strata.SMTCore + |>.addDialect! Strata.SMT + |>.addDialect! Strata.SMTResponse + let mut sp ← Strata.DialectFileMap.new preloaded + for path in pflags.getRepeated "include" do + match ← sp.add path |>.toBaseIO with + | .error msg => exitFailure msg + | .ok sp' => sp := sp' + return sp + +end ParsedFlags + +def parseCheckMode (pflags : ParsedFlags) + (default : VerificationMode := .deductive) : IO VerificationMode := + match pflags.getString "check-mode" with + | .none => pure default + | .some s => match VerificationMode.ofString? s with + | .some m => pure m + | .none => exitFailure s!"Invalid check mode: '{s}'. Must be {VerificationMode.options}." + +def parseCheckLevel (pflags : ParsedFlags) + (default : CheckLevel := .minimal) : IO CheckLevel := + match pflags.getString "check-level" with + | .none => pure default + | .some s => match CheckLevel.ofString? s with + | .some l => pure l + | .none => exitFailure s!"Invalid check level: '{s}'. Must be {CheckLevel.options}." + +/-- Common CLI flags for VerifyOptions fields. + Commands can append these to their own flags list. + Note: `parseOnly`, `typeCheckOnly`, and `checkOnly` are omitted here + because they are specific to the `verify` command. -/ +def verifyOptionsFlags : List Flag := [ + { name := "check-mode", + help := s!"Check mode: {VerificationMode.options}. Default: 'deductive'.", + takesArg := .arg "mode" }, + { name := "check-level", + help := s!"Check level: {CheckLevel.options}. Default: 'minimal'.", + takesArg := .arg "level" }, + { name := "verbose", help := "Enable verbose output." }, + { name := "quiet", help := "Suppress warnings on stderr." }, + { name := "profile", help := "Print elapsed time for each pipeline step." }, + { name := "sarif", help := "Write results as SARIF to .sarif." }, + { name := "solver", + help := s!"SMT solver executable (default: {Core.defaultSolver}).", + takesArg := .arg "name" }, + { name := "solver-timeout", + help := "Solver timeout in seconds (default: 10).", + takesArg := .arg "seconds" }, + { name := "vc-directory", + help := "Store VCs in SMT-Lib format in .", + takesArg := .arg "dir" }, + { name := "no-solve", + help := "Generate SMT-Lib files but do not invoke the solver." }, + { name := "stop-on-first-error", + help := "Exit after the first verification error." }, + { name := "unique-bound-names", + help := "Use globally unique names for quantifier-bound variables." }, + { name := "use-array-theory", + help := "Use SMT-LIB Array theory instead of axiomatized maps." }, + { name := "remove-irrelevant-axioms", + help := "Prune irrelevant axioms: 'off', 'aggressive', or 'precise'.", + takesArg := .arg "mode" }, + { name := "overflow-checks", + help := "Comma-separated overflow checks to enable (signed,unsigned,float64,all,none).", + takesArg := .arg "checks" }, + { name := "incremental", + help := "Use incremental solver backend (stdin/stdout) instead of batch file I/O." }, + { name := "path-cap", + help := "Maximum continuing paths between statements. 'none' (default) disables; N merges paths when count exceeds N.", + takesArg := .arg "N|none" }, + { name := "parallel", + help := "Number of parallel solver workers (default: 1, sequential).", + takesArg := .arg "N" } +] + +/-- Build a VerifyOptions from parsed CLI flags, starting from a base config. + Fields not present in the flags keep their base values. + Note: boolean flags can only enable a setting; a `true` in the base + cannot be turned off from the CLI (there is no `--no-X` syntax). -/ +def parseVerifyOptions (pflags : ParsedFlags) + (base : VerifyOptions := VerifyOptions.default) : IO VerifyOptions := do + let checkMode ← parseCheckMode pflags base.checkMode + let checkLevel ← parseCheckLevel pflags base.checkLevel + let solverTimeout ← match pflags.getString "solver-timeout" with + | .none => pure base.solverTimeout + | .some s => match s.toNat? with + | .some n => pure n + | .none => exitFailure s!"Invalid solver timeout: '{s}'" + let noSolve := pflags.getBool "no-solve" + let removeIrrelevantAxioms ← match pflags.getString "remove-irrelevant-axioms" with + | .none => pure base.removeIrrelevantAxioms + | .some "off" => pure .Off + | .some "aggressive" => pure .Aggressive + | .some "precise" => pure .Precise + | .some s => exitFailure s!"Invalid remove-irrelevant-axioms mode: '{s}'. Must be 'off', 'aggressive', or 'precise'." + let overflowChecks := match pflags.getString "overflow-checks" with + | .none => base.overflowChecks + | .some s => s.splitOn "," |>.foldl (fun acc c => + match c.trimAscii.toString with + | "signed" => { acc with signedBV := true } + | "unsigned" => { acc with unsignedBV := true } + | "float64" => { acc with float64 := true } + | "none" => { signedBV := false, unsignedBV := false, float64 := false } + | "all" => { signedBV := true, unsignedBV := true, float64 := true } + | _ => acc) { signedBV := false, unsignedBV := false, float64 := false } + let pathCap ← match pflags.getString "path-cap" with + | .none => pure base.pathCap + | .some "none" => pure .none + | .some s => match s.toNat? with + | .some n => if n == 0 then exitFailure "--path-cap must be at least 1 or 'none'." + else pure (.some n) + | .none => exitFailure s!"Invalid path-cap: '{s}'. Must be a positive number or 'none'." + let parallelWorkers ← match pflags.getString "parallel" with + | .none => pure base.parallelWorkers + | .some s => match s.toNat? with + | .some n => if n == 0 then exitFailure "--parallel must be at least 1." + else pure n + | .none => exitFailure s!"Invalid parallel workers: '{s}'. Must be a positive number." + let vcDirectory := (pflags.getString "vc-directory" |>.map (⟨·⟩ : String → System.FilePath)).orElse (fun _ => base.vcDirectory) + let skipSolver := noSolve || base.skipSolver + if skipSolver && vcDirectory.isNone then + exitFailure "--no-solve requires --vc-directory to specify where SMT files are stored." + pure { base with + verbose := if pflags.getBool "verbose" then .normal + else if pflags.getBool "quiet" then .quiet + else base.verbose, + solver := pflags.getString "solver" |>.getD base.solver, + solverTimeout, + checkMode, checkLevel, + stopOnFirstError := pflags.getBool "stop-on-first-error" || base.stopOnFirstError, + uniqueBoundNames := pflags.getBool "unique-bound-names" || base.uniqueBoundNames, + useArrayTheory := pflags.getBool "use-array-theory" || base.useArrayTheory, + removeIrrelevantAxioms, + outputSarif := pflags.getBool "sarif" || base.outputSarif, + profile := pflags.getBool "profile" || base.profile, + incremental := if noSolve then false else pflags.getBool "incremental" || base.incremental, + skipSolver, + alwaysGenerateSMT := noSolve || base.alwaysGenerateSMT, + overflowChecks, + vcDirectory, + pathCap, + parallelWorkers + } + +/-- Additional CLI flags for `LaurelVerifyOptions` fields that are not already + covered by `verifyOptionsFlags`. -/ +def laurelTranslateFlags : List Flag := [ + { name := "keep-all-files", + help := "Store intermediate Laurel and Core programs in .", + takesArg := .arg "dir" } +] + +/-- All CLI flags accepted by Laurel verify commands. -/ +def laurelVerifyOptionsFlags : List Flag := verifyOptionsFlags ++ laurelTranslateFlags + +/-- Build a `LaurelVerifyOptions` from parsed CLI flags. -/ +def parseLaurelVerifyOptions (pflags : ParsedFlags) + (base : LaurelVerifyOptions := default) : IO LaurelVerifyOptions := do + let verifyOptions ← parseVerifyOptions pflags base.verifyOptions + let keepAllFilesPrefix := (pflags.getString "keep-all-files").orElse + (fun _ => base.translateOptions.keepAllFilesPrefix) + let translateOptions : LaurelTranslateOptions := + { base.translateOptions with + keepAllFilesPrefix + overflowChecks := verifyOptions.overflowChecks + profile := verifyOptions.profile } + return { translateOptions, verifyOptions } + +/-- Read and parse a Strata program file, loading the Core, C_Simp, and B3CST + dialects. Returns the parsed program and the input context (for source + location resolution), or an array of error messages on failure. -/ +private def readStrataProgram (file : String) + : IO (Except (Array Lean.Message) (Strata.Program × Lean.Parser.InputContext)) := do + let text ← Strata.Util.readInputSource file + let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) + let dctx := Elab.LoadedDialects.builtin + let dctx := dctx.addDialect! Core + let dctx := dctx.addDialect! Boole + let dctx := dctx.addDialect! C_Simp + let dctx := dctx.addDialect! B3CST + let leanEnv ← Lean.mkEmptyEnvironment 0 + match Strata.Elab.elabProgram dctx leanEnv inputCtx with + | .ok pgm => pure (.ok (pgm, inputCtx)) + | .error msgs => pure (.error msgs) + +structure Command where + name : String + args : List String + flags : List Flag := [] + help : String + callback : Vector String args.length → ParsedFlags → IO Unit + +def includeFlag : Flag := + { name := "include", help := "Add a dialect search path.", takesArg := .repeat "path" } + +def checkCommand : Command where + name := "check" + args := [ "file" ] + flags := [includeFlag] + help := "Parse and validate a Strata file (text or Ion). Reports errors and exits." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let _ ← Strata.readStrataFile fm v[0] + +def toIonCommand : Command where + name := "toIon" + args := [ "input", "output" ] + flags := [includeFlag] + help := "Convert a Strata text file to Ion binary format." + callback := fun v pflags => do + let searchPath ← pflags.buildDialectFileMap + let pd ← Strata.readStrataFile searchPath v[0] + match pd with + | .dialect d => + IO.FS.writeBinFile v[1] d.toIon + | .program pgm => + IO.FS.writeBinFile v[1] pgm.toIon + +def printCommand : Command where + name := "print" + args := [ "file" ] + flags := [includeFlag] + help := "Pretty-print a Strata file (text or Ion) to stdout." + callback := fun v pflags => do + let searchPath ← pflags.buildDialectFileMap + -- Special case for already loaded dialects. + let ld ← searchPath.getLoaded + if mem : v[0] ∈ ld.dialects then + IO.print <| ld.dialects.format v[0] mem + return + let pd ← Strata.readStrataFile searchPath v[0] + match pd with + | .dialect d => + let ld ← searchPath.getLoaded + let .isTrue mem := (inferInstance : Decidable (d.name ∈ ld.dialects)) + | exitInternalError "Internal error reading file." + IO.print <| ld.dialects.format d.name mem + | .program pgm => + IO.print <| toString pgm + +def diffCommand : Command where + name := "diff" + args := [ "file1", "file2" ] + flags := [includeFlag] + help := "Compare two program files for syntactic equality. Reports the first difference found." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let p1 ← Strata.readStrataFile fm v[0] + let p2 ← Strata.readStrataFile fm v[1] + match p1, p2 with + | .program p1, .program p2 => + if p1.dialect != p2.dialect then + exitFailure s!"Dialects differ: {p1.dialect} and {p2.dialect}" + let Decidable.isTrue eq := (inferInstance : Decidable (p1.commands.size = p2.commands.size)) + | exitFailure s!"Number of commands differ {p1.commands.size} and {p2.commands.size}" + for (c1, c2) in Array.zip p1.commands p2.commands do + if c1 != c2 then + exitFailure s!"Commands differ: {repr c1} and {repr c2}" + | _, _ => + exitFailure "Cannot compare dialect def with another dialect/program." + +def pySpecsCommand : Command where + name := "pySpecs" + args := [ "source_dir", "output_dir" ] + flags := [ + { name := "quiet", help := "Suppress default logging." }, + { name := "log", help := "Enable logging for an event type.", + takesArg := .repeat "event" }, + { name := "skip", + help := "Skip a top-level definition (module.name). Overloads are kept.", + takesArg := .repeat "name" }, + { name := "module", + help := "Translate only the named module (dot-separated). May be repeated.", + takesArg := .repeat "module" } + ] + help := "Translate Python specification files in a directory into Strata DDM Ion format. If --module is given, translates only those modules; otherwise translates all .py files. Creates subdirectories as needed. (Experimental)" + callback := fun v pflags => do + let quiet := pflags.getBool "quiet" + let mut events : Std.HashSet String := {} + if !quiet then + events := events.insert "import" + for e in pflags.getRepeated "log" do + events := events.insert e + let skipNames := pflags.getRepeated "skip" + let modules := pflags.getRepeated "module" + let warningOutput : Strata.WarningOutput := + if quiet then .none else .detail + -- Serialize embedded dialect for Python subprocess + IO.FS.withTempFile fun _handle dialectFile => do + IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon + let r ← Strata.pySpecsDir (events := events) + (skipNames := skipNames) + (modules := modules) + (warningOutput := warningOutput) + v[0] v[1] dialectFile |>.toBaseIO + match r with + | .ok () => pure () + | .error msg => exitFailure msg + +/-- Derive Python source file path from Ion file path. + E.g., "tests/test_foo.python.st.ion" -> "tests/test_foo.py" -/ +def ionPathToPythonPath (ionPath : String) : Option String := + if ionPath.endsWith ".python.st.ion" then + let basePath := ionPath.dropEnd ".python.st.ion".length |>.toString + some (basePath ++ ".py") + else if ionPath.endsWith ".py.ion" then + some (ionPath.dropEnd ".ion".length |>.toString) + else + none + +/-- Try to read Python source file for source location reconstruction -/ +def tryReadPythonSource (ionPath : String) : IO (Option (String × String)) := do + match ionPathToPythonPath ionPath with + | none => return none + | some pyPath => + try + let content ← IO.FS.readFile pyPath + return some (pyPath, content) + catch _ => + return none + +/-- Format related position strings from metadata, if present. -/ +def formatRelatedPositions (md : Imperative.MetaData Core.Expression) + (mfm : Option (String × Lean.FileMap)) : String := + let ranges := Imperative.getRelatedFileRanges md + if ranges.isEmpty then "" else + match mfm with + | none => "" + | some (_, fm) => + let lines := ranges.filterMap fun fr => + if fr.range.isNone then none else + match fr.file with + | .file "" => some "\n Related location: in prelude file" + | .file _ => + let pos := fm.toPosition fr.range.start + some s!"\n Related location: line {pos.line}, col {pos.column}" + String.join lines.toList + +/-! ### pyAnalyzeLaurel result helpers + +The `pyAnalyzeLaurel` command emits two structured lines on stdout: +- `RESULT: ` — machine-readable category, always the last line. +- `DETAIL: ` — human-readable context (error message or VC counts). + +Exit codes follow the common scheme (see `ExitCode` above). +A successful run exits 0 with `RESULT: Analysis success` or `RESULT: Inconclusive`. -/ + +/-- Determines which VC results count as successes and which count as failures + for the purposes of the `pyAnalyzeLaurel` summary and exit code. + Implementation-error results are partitioned out first; the classifier then + partitions the rest into success / failure / inconclusive. + Narrowing `isFailure` (e.g. to only `alwaysFalseAndReachable`) automatically + widens inconclusive. + Future: may be extended with `isWarning` for non-fatal diagnostic categories. -/ +structure ResultClassifier where + isSuccess : Core.VCResult → Bool := (·.isSuccess) + isFailure : Core.VCResult → Bool := (·.isFailure) + +private def printPyAnalyzeResult (category : String) (detail : String) : IO Unit := do + IO.println s!"DETAIL: {detail}" + IO.println s!"RESULT: {category}" + +private def exitPyAnalyzeUserError {α} (message : String) : IO α := do + printPyAnalyzeResult "User error" message + IO.Process.exit ExitCode.userError + +private def exitPyAnalyzeFailuresFound {α} (detail : String) : IO α := do + printPyAnalyzeResult "Failures found" detail + IO.Process.exit ExitCode.failuresFound + +private def exitPyAnalyzeInternalError {α} (message : String) : IO α := do + printPyAnalyzeResult "Internal error" message + IO.Process.exit ExitCode.internalError + +private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do + printPyAnalyzeResult "Known limitation" message + IO.Process.exit ExitCode.knownLimitation + +/-- 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). + Classification uses successive partitioning: timeouts and implementation + errors are removed first, then the classifier partitions the rest into + success / failure / inconclusive (guaranteeing disjointness). + Unreachable count is reported as supplementary info. + + Exit-code priority (highest wins): + - Internal error (exit 3): encoding failures or solver crashes + - Failures found (exit 2): assertion violations + - Inconclusive / success / solver timeout (exit 0) -/ +private def printPyAnalyzeSummary (vcResults : Array Core.VCResult) + (checkMode : VerificationMode := .deductive) : IO Unit := do + let classifier : ResultClassifier := + match checkMode with + | .bugFinding | .bugFindingAssumingCompleteSpec => + { isSuccess := (·.isBugFindingSuccess) + isFailure := (·.isBugFindingFailure) } + | _ => {} + -- 1. Partition out implementation errors and timeouts (not classifiable). + let (implError, rest1) := + vcResults.partition (fun r => r.isImplementationError || r.hasSMTError) + let (timeouts, classifiable) := rest1.partition (·.isTimeout) + -- 2. Successive partitioning via the classifier: success → failure → inconclusive. + let (success, rest) := classifiable.partition classifier.isSuccess + let (failure, inconclusive) := rest.partition classifier.isFailure + -- 3. Unreachable is informational (not a separate partition). + let nUnreachable := vcResults.filter (·.isUnreachable) |>.size + let nImplError := implError.size + let nTimeout := timeouts.size + let nSuccess := success.size + let nFailure := failure.size + let nInconclusive := inconclusive.size + let unreachableStr := if nUnreachable > 0 then s!", {nUnreachable} unreachable" else "" + let implErrorStr := if nImplError > 0 then s!", {nImplError} internal errors" else "" + let timeoutStr := if nTimeout > 0 then s!", {nTimeout} solver timeouts" else "" + let counts := s!"{nSuccess} passed, {nFailure} failed, {nInconclusive} inconclusive{unreachableStr}{timeoutStr}{implErrorStr}" + if nImplError > 0 then + exitPyAnalyzeInternalError s!"An unexpected result was produced. {counts}" + else if nFailure > 0 then + exitPyAnalyzeFailuresFound counts + else + let label := + if nTimeout > 0 then "Solver timeout" + else if nInconclusive > 0 then "Inconclusive" + else "Analysis success" + printPyAnalyzeResult label counts + +private def deriveBaseName (file : String) : String := + let name := System.FilePath.fileName file |>.getD file + let suffixes := [".python.st.ion", ".py.ion", ".st.ion", ".st"] + match suffixes.find? (name.endsWith ·) with + | some sfx => (name.dropEnd sfx.length).toString + | none => name + + +def pyAnalyzeLaurelCommand : Command where + name := "pyAnalyzeLaurel" + args := [ "file" ] + flags := verifyOptionsFlags ++ [ + { name := "spec-dir", + help := "Directory containing compiled PySpec Ion files.", + takesArg := .arg "dir" }, + { name := "dispatch", + help := "Dispatch module name (e.g., servicelib).", + takesArg := .repeat "module" }, + { name := "pyspec", + help := "PySpec module name (e.g., servicelib.Storage).", + takesArg := .repeat "module" }, + { name := "keep-all-files", + help := "Store intermediate Laurel and Core programs in .", + takesArg := .arg "dir" }, + { name := "entry-point", + help := "Which procedures to verify: main (main fn only), roots (user procs with no user callers, default), or all (all user procs). Only valid in bugFinding mode.", + takesArg := .arg "mode" }, + { name := "warning-summary", + help := "Write PySpec warning summary as JSON to .", + takesArg := .arg "file" }, + { name := "skip-verification", + help := "Run Python-to-Laurel and Laurel-to-Core translation only (skip SMT verification).", + takesArg := .none }] + 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 profile := pflags.getBool "profile" + let quiet := pflags.getBool "quiet" + let outputSarif := pflags.getBool "sarif" + let filePath := v[0] + let pySourceOpt ← tryReadPythonSource filePath + let keepDir := pflags.getString "keep-all-files" + let baseName := deriveBaseName filePath + if let some dir := keepDir then + IO.FS.createDirAll dir + + let dispatchModules := pflags.getRepeated "dispatch" + let pyspecModules := pflags.getRepeated "pyspec" + let specDir := pflags.getString "spec-dir" |>.getD "." + unless ← System.FilePath.isDir specDir do + exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" + let sourcePath := pySourceOpt.map (·.1) + -- Build FileMap for source position resolution. + let mfm : Option (String × Lean.FileMap) := match pySourceOpt with + | some (pyPath, srcText) => some (pyPath, .ofString srcText) + | none => none + let warningSummaryFile := pflags.getString "warning-summary" + let combinedLaurel ← + match ← Strata.pythonAndSpecToLaurel filePath dispatchModules pyspecModules sourcePath + (specDir := specDir) (profile := profile) + (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 + + if verbose then + IO.println "\n==== Laurel Program ====" + IO.println f!"{combinedLaurel}" + + let keepPrefix := keepDir.map (s!"{·}/{baseName}") + + let (coreProgramOption, laurelTranslateErrors, _loweredLaurel, laurelPassStats) ← + profileStep profile "Laurel to Core translation" do + Strata.translateCombinedLaurelWithLowered combinedLaurel + (keepAllFilesPrefix := keepPrefix) (profile := profile) + + if profile && !laurelPassStats.data.isEmpty then + IO.println laurelPassStats.format + + let coreProgram ← + match coreProgramOption with + | none => + exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}" + | some core => pure core + + if verbose then + IO.println "\n==== Core Program ====" + IO.print (Core.formatProgram coreProgram) + + -- When --skip-verification is set, report translation diagnostics and exit + -- without running SMT verification (stages 3-4). + if pflags.getBool "skip-verification" then do + if !laurelTranslateErrors.isEmpty then + IO.eprintln "\n==== Errors ====" + for err in laurelTranslateErrors do + IO.eprintln err + if outputSarif then + let files := match mfm with + | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm + | none => Map.empty + Core.Sarif.writeSarifOutput .deductive files #[] (filePath ++ ".sarif") + let nStrataBug := laurelTranslateErrors.filter (·.type == .StrataBug) |>.length + let nNotYetImpl := laurelTranslateErrors.filter (·.type == .NotYetImplemented) |>.length + let nUserError := laurelTranslateErrors.filter (·.type == .UserError) |>.length + let nWarning := laurelTranslateErrors.filter (·.type == .Warning) |>.length + let counts := s!"{nUserError} user errors, {nWarning} warnings, {nNotYetImpl} not yet implemented, {nStrataBug} internal errors" + if nStrataBug > 0 then + exitPyAnalyzeInternalError s!"Translation produced internal errors. {counts}" + else if nNotYetImpl > 0 then + exitPyAnalyzeKnownLimitation s!"Translation encountered unsupported constructs. {counts}" + else + printPyAnalyzeResult "Analysis success" counts + return + + -- Verify using Core verifier + -- --keep-all-files implies vc-directory if not explicitly set + let baseVcDir := keepDir.map (fun dir => (s!"{dir}/{baseName}" : System.FilePath)) + let pyAnalyzeBase : VerifyOptions := + { VerifyOptions.default with + verbose := .quiet, removeIrrelevantAxioms := .Precise, + vcDirectory := baseVcDir } + let options ← parseVerifyOptions pflags pyAnalyzeBase + let isBugFinding := options.checkMode == .bugFinding + || options.checkMode == .bugFindingAssumingCompleteSpec + + -- Parse --entry-point flag (only supported in bug-finding modes). + let entryPointFlag := pflags.getString "entry-point" + let entryPoint : EntryPoint ← + if isBugFinding then + match entryPointFlag with + | some s => + match EntryPoint.ofString? s with + | some ep => pure ep + | none => + exitPyAnalyzeUserError s!"Invalid --entry-point value '{s}'. Must be {EntryPoint.options}." + | none => pure .roots + else + if entryPointFlag.isSome then + exitPyAnalyzeUserError s!"--entry-point is unsupported in {options.checkMode} mode" + else pure .all + + -- Pick the procedures to verify and set up inlining phases. + let userSourcePath := sourcePath.getD filePath + let (_, userProcNames) := + Strata.splitProcNames coreProgram [userSourcePath] + let (proceduresToVerify, inlinePhases) := + if isBugFinding then + let ⟨p, i⟩ := Core.chooseEntryProceduresAndBuildInlinePhases coreProgram userProcNames entryPoint + (p, [i]) + else (userProcNames, []) + + let vcResults ← profileStep profile "SMT verification" do + match ← Core.verifyProgram coreProgram options + (moreFns := Strata.Python.ReFactory) + (proceduresToVerify := some proceduresToVerify) + (externalPhases := [Strata.frontEndPhase]) + (prefixPhases := inlinePhases) + (keepAllFilesPrefix := keepPrefix) + |>.toBaseIO with + | .ok r => pure r.mergeByAssertion + | .error msg => exitPyAnalyzeInternalError msg + + -- Print translation errors (always on stderr) + if !laurelTranslateErrors.isEmpty then + IO.eprintln "\n==== Errors ====" + for err in laurelTranslateErrors do + IO.eprintln err + + -- Print per-VC results by default, unless SARIF mode is used + if !outputSarif then + let mut s := "" + for vcResult in vcResults do + let fileMap := mfm.map (·.2) + let location := match Imperative.getFileRange vcResult.obligation.metadata with + | some fr => + if fr.range.isNone then "" + else s!"{fr.format fileMap (includeEnd? := false)}" + | none => "" + let messageSuffix := match vcResult.obligation.metadata.getPropertySummary with + | some msg => s!" - {msg}" + | none => s!" - {vcResult.obligation.label}" + let outcomeStr := vcResult.formatOutcome + let loc := if !location.isEmpty then s!"{location}: " else "unknown location: " + s := s ++ s!"{loc}{outcomeStr}{messageSuffix}\n" + IO.print s + -- Output in SARIF format if requested + if outputSarif then + let files := match mfm with + | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm + | none => Map.empty + Core.Sarif.writeSarifOutput options.checkMode files vcResults (filePath ++ ".sarif") + printPyAnalyzeSummary vcResults options.checkMode + +def pyAnalyzeToGotoCommand : Command where + name := "pyAnalyzeToGoto" + args := [ "file" ] + help := "Translate a Strata Python Ion file to CProver GOTO JSON files." + callback := fun v _ => do + let filePath := v[0] + let pySourceOpt ← tryReadPythonSource filePath + let sourcePathForMetadata := match pySourceOpt with + | some (pyPath, _) => pyPath + | none => filePath + let sourceText := pySourceOpt.map (·.2) + let newPgm ← Strata.pythonDirectToCore filePath sourcePathForMetadata + match Core.inlineProcedures newPgm { doInline := (fun _caller callee _ => callee ≠ "main") } with + | .error e => exitInternalError (toString e) + | .ok newPgm => + -- Type-check the full program (registers Python types like ExceptOrNone) + let Ctx := { Lambda.LContext.default with functions := Strata.Python.PythonFactory, knownTypes := Core.KnownTypes } + let Env := Lambda.TEnv.default + let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env newPgm with + | .ok r => pure r + | .error e => exitInternalError s!"{e.format none}" + -- Find the main procedure + let some mainDecl := tcPgm.decls.find? fun d => + match d with + | .proc p _ => Core.CoreIdent.toPretty p.header.name == "main" + | _ => false + | exitInternalError "No main procedure found" + let some p := mainDecl.getProc? + | exitInternalError "main is not a procedure" + -- Translate procedure to GOTO (mirrors CoreToGOTO.transformToGoto post-typecheck logic) + let baseName := deriveBaseName filePath + let procName := Core.CoreIdent.toPretty p.header.name + let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? + let distincts := tcPgm.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + match procedureToGotoCtx Env p sourceText (axioms := axioms) (distincts := distincts) + with + | .error e => exitInternalError s!"{e}" + | .ok (ctx, liftedFuncs) => + let extraSyms ← match collectExtraSymbols tcPgm with + | .ok s => pure (Lean.toJson s) + | .error e => exitInternalError s!"{e}" + let (symtab, goto) ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms + (moduleName := baseName) + let symTabFile := s!"{baseName}.symtab.json" + let gotoFile := s!"{baseName}.goto.json" + writeJsonFile symTabFile symtab + writeJsonFile gotoFile goto + IO.println s!"Written {symTabFile} and {gotoFile}" + +def pyTranslateLaurelCommand : Command where + name := "pyTranslateLaurel" + args := [ "file" ] + flags := [{ name := "pyspec", + help := "PySpec module name (e.g., servicelib.Storage).", + takesArg := .repeat "module" }, + { name := "dispatch", + help := "Dispatch module name (e.g., servicelib).", + takesArg := .repeat "module" }, + { name := "spec-dir", + help := "Directory containing compiled PySpec Ion files.", + takesArg := .arg "dir" }] + help := "Translate a Strata Python Ion file through Laurel to Strata Core. Write results to stdout." + callback := fun v pflags => do + let dispatchModules := pflags.getRepeated "dispatch" + let pyspecModules := pflags.getRepeated "pyspec" + let specDir := pflags.getString "spec-dir" |>.getD "." + unless ← System.FilePath.isDir specDir do + exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" + let coreProgram ← + match ← Strata.pyTranslateLaurel v[0] dispatchModules pyspecModules (specDir := specDir) |>.toBaseIO with + | .ok r => pure r + | .error msg => exitFailure msg + IO.print coreProgram + +def pyAnalyzeLaurelToGotoCommand : Command where + name := "pyAnalyzeLaurelToGoto" + args := [ "file" ] + flags := [{ name := "pyspec", + help := "PySpec module name (e.g., servicelib.Storage).", + takesArg := .repeat "module" }, + { name := "dispatch", + help := "Dispatch module name (e.g., servicelib).", + takesArg := .repeat "module" }, + { name := "spec-dir", + help := "Directory containing compiled PySpec Ion files.", + takesArg := .arg "dir" }] + help := "Translate a Strata Python Ion file through Laurel to CProver GOTO JSON files." + callback := fun v pflags => do + let filePath := v[0] + let dispatchModules := pflags.getRepeated "dispatch" + let pyspecModules := pflags.getRepeated "pyspec" + let specDir := pflags.getString "spec-dir" |>.getD "." + unless ← System.FilePath.isDir specDir do + exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" + let (coreProgram, laurelTranslateErrors) ← + match ← Strata.pyTranslateLaurel filePath dispatchModules pyspecModules (specDir := specDir) |>.toBaseIO with + | .ok r => pure r + | .error msg => exitFailure msg + let sourceText := (← tryReadPythonSource filePath).map (·.2) + let baseName := deriveBaseName filePath + match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText + (factory := Strata.Python.PythonFactory) |>.toBaseIO with + | .ok () => pure () + | .error msg => exitFailure msg + +def javaGenCommand : Command where + name := "javaGen" + args := [ "dialect", "package", "output-dir" ] + flags := [includeFlag] + help := "Generate Java source files from a DDM dialect definition. Accepts a dialect name (e.g. Laurel) or a dialect file path." + callback := fun v pflags => do + let fm ← pflags.buildDialectFileMap + let ld ← fm.getLoaded + let d ← if mem : v[0] ∈ ld.dialects then + pure ld.dialects[v[0]] + else + match ← Strata.readStrataFile fm v[0] with + | .dialect d => pure d + | .program _ => exitFailure "Expected a dialect file, not a program file." + match Strata.Java.generateDialect d v[1] with + | .ok files => + Strata.Java.writeJavaFiles v[2] v[1] files + IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.packageToPath v[1]}" + | .error msg => + exitFailure s!"Error generating Java: {msg}" + +def laurelAnalyzeBinaryCommand : Command where + name := "laurelAnalyzeBinary" + args := [] + flags := laurelVerifyOptionsFlags + help := "Verify Laurel Ion programs read from stdin and print diagnostics. Combines multiple input files." + callback := fun _ pflags => do + let options ← parseLaurelVerifyOptions pflags + let stdinBytes ← (← IO.getStdin).readBinToEnd + let combinedProgram ← Strata.readLaurelIonProgram stdinBytes + let diagnostics ← Strata.Laurel.verifyToDiagnosticModels combinedProgram options + + IO.println s!"==== DIAGNOSTICS ====" + for diag in diagnostics do + IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}" + +def pySpecToLaurelCommand : Command where + name := "pySpecToLaurel" + args := [ "python_path", "strata_path" ] + help := "Translate a PySpec Ion file to Laurel declarations. The Ion file must already exist." + callback := fun v _ => do + let pythonFile : System.FilePath := v[0] + let strataDir : System.FilePath := v[1] + let some mod := pythonFile.fileStem + | exitFailure s!"No stem {pythonFile}" + let .ok mod := Strata.Python.Specs.ModuleName.ofString mod + | exitFailure s!"Invalid module {mod}" + let ionFile := strataDir / mod.strataFileName + let sigs ← + match ← Strata.Python.Specs.readDDM ionFile |>.toBaseIO with + | .ok t => pure t + | .error msg => exitFailure s!"Could not read {ionFile}: {msg}" + let result := Strata.Python.Specs.ToLaurel.signaturesToLaurel pythonFile sigs "" + if result.errors.size > 0 then + IO.eprintln s!"{result.errors.size} translation warning(s):" + for err in result.errors do + IO.eprintln s!" {err.file}: {err.message}" + let pgm := result.program + IO.println s!"Laurel: {pgm.staticProcedures.length} procedure(s), {pgm.types.length} type(s)" + IO.println s!"Overloads: {result.overloads.size} function(s)" + for td in pgm.types do + IO.println s!" {Strata.Laurel.formatTypeDefinition td}" + for proc in pgm.staticProcedures do + IO.println s!" {Strata.Laurel.formatProcedure proc}" + +def pyResolveOverloadsCommand : Command where + name := "pyResolveOverloads" + args := [ "python_path", "dispatch_ion" ] + help := "Identify which overloaded service modules a \ + Python program uses. Prints one module name per \ + line to stdout." + callback := fun v _ => do + let pythonFile : System.FilePath := v[0] + let dispatchPath := v[1] + -- Read dispatch overload table + let overloads ← + match ← readDispatchOverloads #[dispatchPath] |>.toBaseIO with + | .ok (r, _) => pure r + | .error msg => exitFailure msg + -- Convert .py to Python AST + let stmts ← + IO.FS.withTempFile fun _handle dialectFile => do + IO.FS.writeBinFile dialectFile + Strata.Python.Python.toIon + match ← Strata.Python.pythonToStrata dialectFile pythonFile |>.toBaseIO with + | .ok s => pure s + | .error msg => exitFailure msg + -- Walk AST and collect modules + let state := + Strata.Python.Specs.IdentifyOverloads.resolveOverloads + overloads stmts + for w in state.warnings do + IO.eprintln s!"warning: {w}" + let sorted := state.modules.toArray.qsort (· < ·) + for m in sorted do + IO.println m + +def laurelParseCommand : Command where + name := "laurelParse" + args := [ "file" ] + help := "Parse a Laurel source file (no verification)." + callback := fun v _ => do + let _ ← Strata.readLaurelTextFile v[0] + IO.println "Parse successful" + +def laurelAnalyzeCommand : Command where + name := "laurelAnalyze" + args := [ "file" ] + flags := laurelVerifyOptionsFlags + help := "Analyze a Laurel source file. Write diagnostics to stdout." + callback := fun v pflags => do + let options ← parseLaurelVerifyOptions pflags + let laurelProgram ← Strata.readLaurelTextFile v[0] + let (vcResultsOption, errors) ← Strata.Laurel.verifyToVcResults laurelProgram options + if !errors.isEmpty then + IO.println s!"==== ERRORS ====" + for err in errors do + IO.println s!"{err.message}" + match vcResultsOption with + | none => return + | some vcResults => + IO.println s!"==== RESULTS ====" + for vc in vcResults do + IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => toString e}" + +def laurelAnalyzeToGotoCommand : Command where + name := "laurelAnalyzeToGoto" + args := [ "file" ] + help := "Translate a Laurel source file to CProver GOTO JSON files." + callback := fun v _ => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let laurelProgram ← Strata.parseLaurelText path content + match ← Strata.Laurel.translate {} laurelProgram with + | (none, diags) => exitFailure s!"Core translation errors: {diags.map (·.message)}" + | (some coreProgram, errors) => + let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } + let Env := Lambda.TEnv.default + let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env coreProgram with + | .ok r => pure r + | .error e => exitInternalError s!"{e.format none}" + let procs := tcPgm.decls.filterMap fun d => d.getProc? + let funcs := tcPgm.decls.filterMap fun d => + match d.getFunc? with + | some f => + let name := Core.CoreIdent.toPretty f.name + if f.body.isSome && f.typeArgs.isEmpty + && name != "Int.DivT" && name != "Int.ModT" + then some f else none + | none => none + if procs.isEmpty && funcs.isEmpty then exitInternalError "No procedures or functions found" + let baseName := deriveBaseName path.toString + let typeSyms ← match collectExtraSymbols tcPgm with + | .ok s => pure s + | .error e => exitInternalError s!"{e}" + let typeSymsJson := Lean.toJson typeSyms + let sourceText := some content + let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? + let distincts := tcPgm.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + let mut symtabPairs : List (String × Lean.Json) := [] + let mut gotoFns : Array Lean.Json := #[] + let mut allLiftedFuncs : List Core.Function := [] + for p in procs do + let procName := Core.CoreIdent.toPretty p.header.name + match procedureToGotoCtx Env p (sourceText := sourceText) (axioms := axioms) (distincts := distincts) + with + | .error e => exitInternalError s!"{e}" + | .ok (ctx, liftedFuncs) => + allLiftedFuncs := allLiftedFuncs ++ liftedFuncs + let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx) + match json.symtab with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + match json.goto with + | .obj m => + match m.toList.find? (·.1 == "functions") with + | some (_, .arr fns) => gotoFns := gotoFns ++ fns + | _ => pure () + | _ => pure () + for f in funcs ++ allLiftedFuncs do + let funcName := Core.CoreIdent.toPretty f.name + match functionToGotoCtx Env f with + | .error e => exitInternalError s!"{e}" + | .ok ctx => + let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx) + match json.symtab with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + match json.goto with + | .obj m => + match m.toList.find? (·.1 == "functions") with + | some (_, .arr fns) => gotoFns := gotoFns ++ fns + | _ => pure () + | _ => pure () + match typeSymsJson with + | .obj m => symtabPairs := symtabPairs ++ m.toList + | _ => pure () + -- Deduplicate: keep first occurrence of each symbol name (proper function + -- symbols come before basic symbol references from callers) + let mut seen : Std.HashSet String := {} + let mut dedupPairs : List (String × Lean.Json) := [] + for (k, v) in symtabPairs do + if !seen.contains k then + seen := seen.insert k + dedupPairs := dedupPairs ++ [(k, v)] + -- Add CBMC default symbols (architecture constants, builtins) + -- and wrap in {"symbolTable": ...} for symtab2gb + let symtabObj := dedupPairs.foldl + (fun (acc : Std.TreeMap.Raw String Lean.Json) (k, v) => acc.insert k v) + .empty + let symtab := CProverGOTO.wrapSymtab symtabObj (moduleName := baseName) + let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)] + let symTabFile := s!"{baseName}.symtab.json" + let gotoFile := s!"{baseName}.goto.json" + writeJsonFile symTabFile symtab + writeJsonFile gotoFile goto + IO.println s!"Written {symTabFile} and {gotoFile}" + +def laurelPrintCommand : Command where + name := "laurelPrint" + args := [] + help := "Read Laurel Ion from stdin and print in concrete syntax to stdout." + callback := fun _ _ => do + let stdinBytes ← (← IO.getStdin).readBinToEnd + let strataFiles ← Strata.readLaurelIonFiles stdinBytes + for strataFile in strataFiles do + IO.println s!"// File: {strataFile.filePath}" + let p := strataFile.program + let c := p.formatContext {} + let s := p.formatState + let fmt := p.commands.foldl (init := f!"") fun f cmd => + f ++ (Strata.mformat cmd c s).format + IO.println (fmt.pretty 100) + IO.println "" + +def prettyPrintCore (p : Core.Program) : String := + let decls := p.decls.map fun d => + let s := toString (Std.format d) + -- Add newlines after major sections in procedures + s.replace "preconditions:" "\n preconditions:" + |>.replace "postconditions:" "\n postconditions:" + |>.replace "body:" "\n body:\n " + |>.replace "assert [" "\n assert [" + |>.replace "init (" "\n init (" + |>.replace "while (" "\n while (" + |>.replace "if (" "\n if (" + |>.replace "call [" "\n call [" + |>.replace "else{" "\n else {" + |>.replace "}}" "}\n }" + String.intercalate "\n" decls + +def laurelToCoreCommand : Command where + name := "laurelToCore" + args := [ "file" ] + help := "Translate a Laurel source file to Core and print to stdout." + callback := fun v _ => do + let laurelProgram ← Strata.readLaurelTextFile v[0] + let (coreProgramOption, errors) ← Strata.Laurel.translate {} laurelProgram + if !errors.isEmpty then + IO.println s!"Core translation errors: {errors.map (·.message)}" + match coreProgramOption with + | none => return + | some coreProgram => IO.println (prettyPrintCore coreProgram) + +/-- Print a string word-wrapped to `width` columns with `indent` spaces of indentation. -/ +private def printIndented (indent : Nat) (s : String) (width : Nat := 80) : IO Unit := do + let pad := "".pushn ' ' indent + let words := s.splitOn " " |>.filter (!·.isEmpty) + let mut line := pad + let mut first := true + for word in words do + if first then + line := line ++ word + first := false + else if line.length + 1 + word.length > width then + IO.println line + line := pad ++ word + else + line := line ++ " " ++ word + unless line.length ≤ indent do + IO.println line + +structure CommandGroup where + name : String + commands : List Command + commonFlags : List Flag := [] + +private def validPasses := + "inlineProcedures, loopElim, callElim, filterProcedures, removeIrrelevantAxioms" + +/-- A single transform pass together with the `--procedures`/`--functions` + that were specified immediately after it on the command line. -/ +private structure PassConfig where + name : String + procedures : List String := [] + functions : List String := [] +deriving Inhabited + +/-- Walk the ordered flag entries and bind each `--procedures`/`--functions` + to the most recent `--pass`. -/ +private def buildPassConfigs (entries : Array (String × Option String)) + : IO (Array PassConfig) := do + let mut configs : Array PassConfig := #[] + for (flag, value) in entries do + match flag with + | "pass" => configs := configs.push { name := value.getD "" } + | "procedures" => + let some cur := configs.back? | exitFailure "--procedures must appear after a --pass" + let procs := (value.getD "").splitToList (· == ',') + configs := configs.pop.push { cur with procedures := cur.procedures ++ procs } + | "functions" => + let some cur := configs.back? | exitFailure "--functions must appear after a --pass" + let fns := (value.getD "").splitToList (· == ',') + configs := configs.pop.push { cur with functions := cur.functions ++ fns } + | _ => pure () + return configs + +def transformCommand : Command where + name := "transform" + args := [ "file" ] + flags := [ + { name := "pass", + help := s!"Transform pass to apply (repeatable, applied left to right). \ + Valid passes: {validPasses}. \ + --procedures and --functions after a --pass apply to that pass.", + takesArg := .repeat "name" }, + { name := "procedures", + help := "Comma-separated procedure names for the preceding --pass. \ + For filterProcedures: procedures to keep. \ + For inlineProcedures: procedures to inline.", + takesArg := .repeat "procs" }, + { name := "functions", + help := "Comma-separated function names for the preceding --pass (used by removeIrrelevantAxioms).", + takesArg := .repeat "funcs" }] + help := "Apply one or more transforms to a Core program and print the result." + callback := fun v pflags => do + let file := v[0] + let passConfigs ← buildPassConfigs pflags.entries + if passConfigs.isEmpty then + exitFailure s!"No --pass specified. Valid passes: {validPasses}." + -- Read and parse the Core program + let (pgm, _) ← match ← readStrataProgram file with + | .ok r => pure r + | .error msgs => + for e in msgs do println! s!"Error: {← e.toString}" + exitFailure s!"{msgs.size} parse error(s)" + match Strata.genericToCore pgm with + | .error msg => + exitFailure msg + | .ok initProgram => + -- Validate and convert pass configs to TransformPass values + let mut passes : List Strata.Core.TransformPass := [] + for pc in passConfigs do + match pc.name with + | "inlineProcedures" => + let opts : Core.InlineTransformOptions := + if pc.procedures.isEmpty then {} + else { doInline := (fun _caller callee _ => callee ∈ pc.procedures) } + passes := passes ++ [.inlineProcedures opts] + | "loopElim" => + passes := passes ++ [.loopElim] + | "callElim" => + passes := passes ++ [.callElim] + | "filterProcedures" => + if pc.procedures.isEmpty then + exitFailure "filterProcedures requires --procedures" + passes := passes ++ [.filterProcedures pc.procedures] + | "removeIrrelevantAxioms" => + if pc.functions.isEmpty then + exitFailure "removeIrrelevantAxioms requires --functions" + passes := passes ++ [.removeIrrelevantAxioms pc.functions] + | other => + exitFailure s!"Unknown pass '{other}'. Valid passes: {validPasses}." + -- Run all passes in a single CoreTransformM chain so fresh variable + -- counters accumulate and cached analyses are reused across passes. + match Strata.Core.runTransforms initProgram passes with + | .ok program => IO.print (Core.formatProgram program) + | .error e => exitFailure s!"Transform failed: {e}" + +def verifyCommand : Command where + name := "verify" + args := [ "file" ] + flags := verifyOptionsFlags ++ [ + { name := "check", help := "Process up until SMT generation, but don't solve." }, + { name := "type-check", help := "Exit after semantic dialect's type inference/checking." }, + { name := "parse-only", help := "Exit after DDM parsing and type checking." }, + { name := "output-format", help := "Output format (only 'sarif' supported).", takesArg := .arg "format" }, + { name := "procedures", help := "Verify only the specified procedures (comma-separated).", takesArg := .arg "procs" }] + help := "Verify a Strata program file (.core.st, .csimp.st, or .b3.st)." + callback := fun v pflags => do + let file := v[0] + let proceduresToVerify := pflags.getString "procedures" |>.map (·.splitToList (· == ',')) + let opts ← parseVerifyOptions pflags { VerifyOptions.default with verbose := .quiet } + let opts := { opts with + checkOnly := pflags.getBool "check", + typeCheckOnly := pflags.getBool "type-check", + parseOnly := pflags.getBool "parse-only", + outputSarif := opts.outputSarif || pflags.getString "output-format" == some "sarif" } + let (pgm, inputCtx) ← match ← readStrataProgram file with + | .ok r => pure r + | .error errors => + for e in errors do + let msg ← e.toString + println! s!"Error: {msg}" + println! f!"Finished with {errors.size} errors." + IO.Process.exit ExitCode.userError + println! s!"Successfully parsed." + if opts.parseOnly then return + if opts.typeCheckOnly then + let ans := if file.endsWith ".csimp.st" then + C_Simp.typeCheck pgm opts + else if pgm.dialect == "Boole" then + Boole.typeCheck pgm opts + else + typeCheck inputCtx pgm opts + match ans with + | .error e => + println! f!"{e.formatRange (some inputCtx.fileMap) true} {e.message}" + IO.Process.exit ExitCode.userError + | .ok _ => + println! f!"Program typechecked." + return + -- Full verification + let vcResults ← try + if file.endsWith ".csimp.st" then + C_Simp.verify pgm opts + else if file.endsWith ".b3.st" || file.endsWith ".b3cst.st" then + let ast ← match B3.Verifier.programToB3AST pgm with + | Except.error msg => throw (IO.userError s!"Failed to convert to B3 AST: {msg}") + | Except.ok ast => pure ast + let solver ← B3.Verifier.createInteractiveSolver opts.solver + let reports ← B3.Verifier.programToSMT ast solver + for report in reports do + IO.println s!"\nProcedure: {report.procedureName}" + for (result, _) in report.results do + let marker := if result.result.isError then "✗" else "✓" + let desc := match result.result with + | .error .counterexample => "counterexample found" + | .error .unknown => "unknown" + | .error .refuted => "refuted" + | .success .verified => "verified" + | .success .reachable => "reachable" + | .success .reachabilityUnknown => "reachability unknown" + IO.println s!" {marker} {desc}" + pure #[] + else if pgm.dialect == "Boole" then + Boole.verify opts.solver pgm inputCtx proceduresToVerify opts + else + verify pgm inputCtx proceduresToVerify opts + catch e => + println! f!"{e}" + IO.Process.exit ExitCode.internalError + if opts.outputSarif then + 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 uri := Strata.Uri.file file + let files := Map.empty.insert uri inputCtx.fileMap + Core.Sarif.writeSarifOutput opts.checkMode files vcResults (file ++ ".sarif") + for vcResult in vcResults do + let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata (some inputCtx.fileMap) + println! f!"{posStr} [{vcResult.obligation.label}]: \ + {vcResult.formatOutcome}" + let success := vcResults.all Core.VCResult.isSuccess + if success && !opts.checkOnly then + println! f!"All {vcResults.size} goals passed." + else if success && opts.checkOnly then + println! f!"Skipping verification." + else + let provedGoalCount := (vcResults.filter Core.VCResult.isSuccess).size + let failedGoalCount := (vcResults.filter Core.VCResult.isNotSuccess).size + -- Encoding failures, solver crashes, or per-check SMT errors (exit 3) + let hasImplError := vcResults.any (fun r => r.isImplementationError || r.hasSMTError) + -- Assertion violations that are not timeouts or internal errors (exit 2) + let hasFailure := vcResults.any (fun r => !r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError) + println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed." + if hasImplError then + IO.Process.exit ExitCode.internalError + else if hasFailure then + IO.Process.exit ExitCode.failuresFound + +def pyInterpretCommand : Command where + name := "pyInterpret" + args := [ "file" ] + flags := [{ name := "fuel", help := "Maximum execution steps.", takesArg := .arg "n" }] + ++ laurelTranslateFlags + help := "Interpret a Python Ion program concretely (Python → Laurel → Core → execute)." + callback := fun v pflags => do + let filePath := v[0] + let keepDir := pflags.getString "keep-all-files" + let fuel ← match pflags.getString "fuel" with + | some s => match s.toNat? with + | .some n => pure n + | .none => exitFailure s!"Invalid fuel: '{s}'" + | none => pure 10000 + + let (core, _diags) ← + match ← Strata.pythonAndSpecToLaurel filePath (specDir := ".") |>.toBaseIO with + | .ok laurel => + if let some dir := keepDir then + IO.FS.createDirAll dir + IO.FS.writeFile (dir ++ "/laurel.st") (toString (Std.format laurel)) + match ← Strata.translateCombinedLaurel laurel with + | (some core, diags) => pure (core, diags) + | (none, diags) => exitFailure s!"Laurel to Core translation failed: {diags}" + | .error msg => exitFailure (toString msg) + if let some dir := keepDir then + IO.FS.writeFile (dir ++ "/core.st") (toString (Std.format core)) + let core ← match Core.typeCheck Core.VerifyOptions.quiet core + (moreFns := Strata.Python.ReFactory) with + | .ok prog => pure prog + | .error e => + println! s!"Core type checking failed: {e.message}" + IO.Process.exit ExitCode.userError + match core.run with + | .ok E => + let mainProc := Core.Program.Procedure.find? core ⟨"__main__", ()⟩ + let outputNames := match mainProc with + | some p => p.header.outputs.keys.map (·.name) + | none => [] + let (lhs, exprEnv) := Core.Env.genVars outputNames E.exprEnv + let E := { E with exprEnv } + let E := Core.Statement.Command.runCall lhs "__main__" [] fuel E + match E.error with + | none => + IO.println "Execution completed successfully." + | some e => + IO.println s!"{Std.format e}" + IO.Process.exit ExitCode.failuresFound + | .error diag => + IO.eprintln s!"Error: {diag}" + IO.Process.exit ExitCode.failuresFound + +def commandGroups : List CommandGroup := [ + { name := "Core" + commands := [verifyCommand, transformCommand, checkCommand, toIonCommand, printCommand, diffCommand] + commonFlags := [includeFlag] }, + { name := "Code Generation" + commands := [javaGenCommand] }, + { name := "Python" + commands := [pyAnalyzeLaurelCommand, + pyResolveOverloadsCommand, + pySpecsCommand, pySpecToLaurelCommand, + pyAnalyzeLaurelToGotoCommand, + pyAnalyzeToGotoCommand, + pyTranslateLaurelCommand, + pyInterpretCommand] }, + { name := "Laurel" + commands := [laurelAnalyzeCommand, laurelAnalyzeBinaryCommand, + laurelAnalyzeToGotoCommand, laurelParseCommand, + laurelPrintCommand, laurelToCoreCommand] }, +] + +def commandList : List Command := + commandGroups.foldl (init := []) fun acc g => acc ++ g.commands + +def commandMap : Std.HashMap String Command := + commandList.foldl (init := {}) fun m c => m.insert c.name c + +/-- Print a single flag's name and help text at the given indentation. -/ +private def printFlag (indent : Nat) (flag : Flag) : IO Unit := do + let pad := "".pushn ' ' indent + match flag.takesArg with + | .arg argName | .repeat argName => + IO.println s!"{pad}--{flag.name} <{argName}> {flag.help}" + | .none => + IO.println s!"{pad}--{flag.name} {flag.help}" + +/-- Print help for all command groups. -/ +private def printGlobalHelp : IO Unit := do + IO.println "Usage: strata [flags]...\n" + IO.println "Command-line utilities for working with Strata.\n" + for group in commandGroups do + IO.println s!"{group.name}:" + for cmd in group.commands do + let cmdLine := cmd.args.foldl (init := cmd.name) fun s a => s!"{s} <{a}>" + IO.println s!" {cmdLine}" + printIndented 4 cmd.help + let perCmdFlags := cmd.flags.filter fun f => + !group.commonFlags.any fun cf => cf.name == f.name + if !perCmdFlags.isEmpty then + IO.println "" + IO.println " Flags:" + for flag in perCmdFlags do + printFlag 6 flag + IO.println "" + if !group.commonFlags.isEmpty then + IO.println " Common flags:" + for flag in group.commonFlags do + printFlag 4 flag + IO.println "" + +/-- Print help for a single command. -/ +private def printCommandHelp (cmd : Command) : IO Unit := do + let cmdLine := cmd.args.foldl (init := s!"strata {cmd.name}") fun s a => s!"{s} <{a}>" + let flagSummary := cmd.flags.foldl (init := "") fun s f => + match f.takesArg with + | .arg argName | .repeat argName => s!"{s} [--{f.name} <{argName}>]" + | .none => s!"{s} [--{f.name}]" + IO.println s!"Usage: {cmdLine}{flagSummary}\n" + printIndented 0 cmd.help + if !cmd.flags.isEmpty then + IO.println "\nFlags:" + for flag in cmd.flags do + printFlag 2 flag + +/-- Parse interleaved flags and positional arguments. Returns the collected + positional arguments and parsed flags. -/ +private def parseArgs (cmdName : String) + (flagMap : Std.HashMap String Flag) + (acc : Array String) (pflags : ParsedFlags) + (cmdArgs : List String) : IO (Array String × ParsedFlags) := do + match cmdArgs with + | arg :: cmdArgs => + if arg.startsWith "--" then + let raw := (arg.drop 2).toString + -- Support --flag=value syntax by splitting on first '=' + let (flagName, inlineValue) ← match raw.splitOn "=" with + | name :: value :: rest => + if !rest.isEmpty then + exitCmdFailure cmdName s!"Invalid option format: {arg}. Values must not contain '='." + pure (name, some value) + | _ => pure (raw, none) + match flagMap[flagName]? with + | some flag => + match flag.takesArg with + | .none => + parseArgs cmdName flagMap acc (pflags.insert flagName Option.none) cmdArgs + | .arg _ => + match inlineValue with + | some value => + parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs + | none => + let value :: cmdArgs := cmdArgs + | exitCmdFailure cmdName s!"Expected value after {arg}." + parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs + | .repeat _ => + match inlineValue with + | some value => + parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs + | none => + let value :: cmdArgs := cmdArgs + | exitCmdFailure cmdName s!"Expected value after {arg}." + parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs + | none => + exitCmdFailure cmdName s!"Unknown option {arg}." + else + parseArgs cmdName flagMap (acc.push arg) pflags cmdArgs + | [] => + pure (acc, pflags) + +public +def main (args : List String) : IO Unit := do + try do + match args with + | ["--help"] => printGlobalHelp + | cmd :: args => + match commandMap[cmd]? with + | none => exitFailure s!"Expected subcommand, got {cmd}." + | some cmd => + -- Handle per-command help before parsing flags. + if args.contains "--help" then + printCommandHelp cmd + return + -- Index the command's flags by name for O(1) lookup during parsing. + let flagMap : Std.HashMap String Flag := + cmd.flags.foldl (init := {}) fun m f => m.insert f.name f + -- Split raw args into positional arguments and parsed flags. + let (args, pflags) ← parseArgs cmd.name flagMap #[] {} args + if p : args.size = cmd.args.length then + cmd.callback ⟨args, p⟩ pflags + else + exitCmdFailure cmd.name s!"{cmd.name} expects {cmd.args.length} argument(s)." + | [] => do + exitFailure "Expected subcommand." + catch e => + exitFailure e.toString diff --git a/StrataMainLib.lean b/StrataMainLib.lean deleted file mode 100644 index 036a73fbd9..0000000000 --- a/StrataMainLib.lean +++ /dev/null @@ -1,1571 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - --- Executable with utilities for working with Strata files. -import Lean.Parser.Extension -import Strata.Backends.CBMC.CollectSymbols -import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline -import Strata.DDM.Integration.Java.Gen -import Strata.Languages.Core.Verifier -import Strata.Languages.Core.SarifOutput -import Strata.Languages.Core.ProgramEval -import Strata.Languages.Core.StatementEval -import Strata.Languages.C_Simp.Verify -import Strata.Languages.B3.Verifier.Program -import Strata.Languages.Laurel.LaurelCompilationPipeline -import Strata.Languages.Boole.Boole -import Strata.Languages.Boole.Verify -import Strata.Languages.Python.Python -import Strata.Languages.Python.Specs.IdentifyOverloads -import Strata.Languages.Python.Specs.ToLaurel -import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator -import Strata.Languages.Laurel.Laurel -import Strata.Languages.Core.EntryPoint -import Strata.Transform.ProcedureInlining -import Strata.Util.IO - -import Strata.SimpleAPI -import Strata.Util.Profile -import Strata.Util.Json -import Strata.DDM.BuiltinDialects -import Strata.DDM.Util.String -import Strata.Languages.Python.PyFactory -import Strata.Languages.Python.Specs -import Strata.Languages.Python.Specs.DDM -import Strata.Languages.Python.ReadPython - -open Strata - -open Core (VerifyOptions VerboseMode VerificationMode CheckLevel EntryPoint) -open Laurel (LaurelVerifyOptions LaurelTranslateOptions) - -/-! ## Exit codes - -All `strata` subcommands use a common exit code scheme: - -| Code | Category | Meaning | -|------|--------------------|-----------------------------------------------------------| -| 0 | Success | Analysis passed, inconclusive, or `--no-solve` completed. | -| 1 | User error | Bad input: invalid arguments, malformed source, etc. | -| 2 | Failures found | Analysis completed and found failures. | -| 3 | Internal error | SMT encoding failure, solver crash, or translation bug. | -| 4 | Known limitation | Intentionally unsupported language construct. | - -Codes 1–2 are **user-actionable** (fix the input or the code under analysis). -Codes 3–4 are **tool-side** (report as a bug or wait for support). -Exit 0 covers success, inconclusive results, and solver timeouts. -/ - -namespace ExitCode - def userError : UInt8 := 1 - def failuresFound : UInt8 := 2 - def internalError : UInt8 := 3 - def knownLimitation : UInt8 := 4 -end ExitCode - -def exitFailure {α} (message : String) (hint : String := "strata --help") : IO α := do - IO.eprintln s!"Exception: {message}\n\nRun {hint} for additional help." - IO.Process.exit ExitCode.userError - -/-- Exit with code 1 for user errors (bad input, malformed source, etc.). -/ -def exitUserError {α} (message : String) : IO α := do - IO.eprintln s!"❌ {message}" - IO.Process.exit ExitCode.userError - -/-- Exit with code 2 for analysis failures found. -/ -def exitFailuresFound {α} (message : String) : IO α := do - IO.eprintln s!"Failures found: {message}" - IO.Process.exit ExitCode.failuresFound - -/-- Exit with code 3 for internal errors (tool limitations or crashes). -/ -def exitInternalError {α} (message : String) : IO α := do - IO.eprintln s!"Exception: {message}" - IO.Process.exit ExitCode.internalError - -/-- Exit with code 4 for known limitations (unsupported constructs). -/ -def exitKnownLimitation {α} (message : String) : IO α := do - IO.eprintln s!"Known limitation: {message}" - IO.Process.exit ExitCode.knownLimitation - -/-- Like `exitFailure` but tailors the help hint to a specific subcommand. -/ -def exitCmdFailure {α} (cmdName : String) (message : String) : IO α := - exitFailure message (hint := s!"strata {cmdName} --help") - -/-- How a flag consumes arguments. -/ -inductive FlagArg where - | none -- boolean flag, e.g. --verbose - | arg (name : String) -- takes one value, e.g. --output - | repeat (name : String) -- takes one value, may appear multiple times, e.g. --include - -/-- A flag that a command accepts. -/ -structure Flag where - name : String -- flag name without "--", used as lookup key - help : String - takesArg : FlagArg := .none - -/-- Parsed flags from the command line. Stored as an ordered array so that - command-line position is preserved (needed by `transform` to bind - `--procedures`/`--functions` to the preceding `--pass`). - For `.arg` flags that appear more than once, `getString` returns the - **last** occurrence (last-writer-wins). -/ -structure ParsedFlags where - entries : Array (String × Option String) := #[] - -namespace ParsedFlags - -def getBool (pf : ParsedFlags) (name : String) : Bool := - pf.entries.any (·.1 == name) - -def getString (pf : ParsedFlags) (name : String) : Option String := - -- Scan from the end so last occurrence wins. - match pf.entries.findRev? (·.1 == name) with - | some (_, some v) => some v - | _ => Option.none - -def getRepeated (pf : ParsedFlags) (name : String) : Array String := - pf.entries.foldl (init := #[]) fun acc (n, v) => - if n == name then match v with | some s => acc.push s | none => acc else acc - -def insert (pf : ParsedFlags) (name : String) (value : Option String) : ParsedFlags := - { pf with entries := pf.entries.push (name, value) } - -def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do - let preloaded := Strata.Elab.LoadedDialects.builtin - |>.addDialect! Strata.Python.Python - |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs - |>.addDialect! Strata.Core - |>.addDialect! Strata.Boole - |>.addDialect! Strata.Laurel.Laurel - |>.addDialect! Strata.smtReservedKeywordsDialect - |>.addDialect! Strata.SMTCore - |>.addDialect! Strata.SMT - |>.addDialect! Strata.SMTResponse - let mut sp ← Strata.DialectFileMap.new preloaded - for path in pflags.getRepeated "include" do - match ← sp.add path |>.toBaseIO with - | .error msg => exitFailure msg - | .ok sp' => sp := sp' - return sp - -end ParsedFlags - -def parseCheckMode (pflags : ParsedFlags) - (default : VerificationMode := .deductive) : IO VerificationMode := - match pflags.getString "check-mode" with - | .none => pure default - | .some s => match VerificationMode.ofString? s with - | .some m => pure m - | .none => exitFailure s!"Invalid check mode: '{s}'. Must be {VerificationMode.options}." - -def parseCheckLevel (pflags : ParsedFlags) - (default : CheckLevel := .minimal) : IO CheckLevel := - match pflags.getString "check-level" with - | .none => pure default - | .some s => match CheckLevel.ofString? s with - | .some l => pure l - | .none => exitFailure s!"Invalid check level: '{s}'. Must be {CheckLevel.options}." - -/-- Common CLI flags for VerifyOptions fields. - Commands can append these to their own flags list. - Note: `parseOnly`, `typeCheckOnly`, and `checkOnly` are omitted here - because they are specific to the `verify` command. -/ -def verifyOptionsFlags : List Flag := [ - { name := "check-mode", - help := s!"Check mode: {VerificationMode.options}. Default: 'deductive'.", - takesArg := .arg "mode" }, - { name := "check-level", - help := s!"Check level: {CheckLevel.options}. Default: 'minimal'.", - takesArg := .arg "level" }, - { name := "verbose", help := "Enable verbose output." }, - { name := "quiet", help := "Suppress warnings on stderr." }, - { name := "profile", help := "Print elapsed time for each pipeline step." }, - { name := "sarif", help := "Write results as SARIF to .sarif." }, - { name := "solver", - help := s!"SMT solver executable (default: {Core.defaultSolver}).", - takesArg := .arg "name" }, - { name := "solver-timeout", - help := "Solver timeout in seconds (default: 10).", - takesArg := .arg "seconds" }, - { name := "vc-directory", - help := "Store VCs in SMT-Lib format in .", - takesArg := .arg "dir" }, - { name := "no-solve", - help := "Generate SMT-Lib files but do not invoke the solver." }, - { name := "stop-on-first-error", - help := "Exit after the first verification error." }, - { name := "unique-bound-names", - help := "Use globally unique names for quantifier-bound variables." }, - { name := "use-array-theory", - help := "Use SMT-LIB Array theory instead of axiomatized maps." }, - { name := "remove-irrelevant-axioms", - help := "Prune irrelevant axioms: 'off', 'aggressive', or 'precise'.", - takesArg := .arg "mode" }, - { name := "overflow-checks", - help := "Comma-separated overflow checks to enable (signed,unsigned,float64,all,none).", - takesArg := .arg "checks" }, - { name := "no-incremental", - help := "Use batch file I/O solver backend instead of incremental (stdin/stdout). Also implied by --no-solve." }, - { name := "path-cap", - help := "Maximum continuing paths between statements. 'none' (default) disables; N merges paths when count exceeds N.", - takesArg := .arg "N|none" }, - { name := "parallel", - help := "Number of parallel solver workers (default: 1, sequential).", - takesArg := .arg "N" } -] - -/-- Build a VerifyOptions from parsed CLI flags, starting from a base config. - Fields not present in the flags keep their base values. - Note: boolean flags can only enable a setting; a `true` in the base - cannot be turned off from the CLI (there is no `--no-X` syntax). -/ -def parseVerifyOptions (pflags : ParsedFlags) - (base : VerifyOptions := VerifyOptions.default) : IO VerifyOptions := do - let checkMode ← parseCheckMode pflags base.checkMode - let checkLevel ← parseCheckLevel pflags base.checkLevel - let solverTimeout ← match pflags.getString "solver-timeout" with - | .none => pure base.solverTimeout - | .some s => match s.toNat? with - | .some n => pure n - | .none => exitFailure s!"Invalid solver timeout: '{s}'" - let noSolve := pflags.getBool "no-solve" - let removeIrrelevantAxioms ← match pflags.getString "remove-irrelevant-axioms" with - | .none => pure base.removeIrrelevantAxioms - | .some "off" => pure .Off - | .some "aggressive" => pure .Aggressive - | .some "precise" => pure .Precise - | .some s => exitFailure s!"Invalid remove-irrelevant-axioms mode: '{s}'. Must be 'off', 'aggressive', or 'precise'." - let overflowChecks := match pflags.getString "overflow-checks" with - | .none => base.overflowChecks - | .some s => s.splitOn "," |>.foldl (fun acc c => - match c.trimAscii.toString with - | "signed" => { acc with signedBV := true } - | "unsigned" => { acc with unsignedBV := true } - | "float64" => { acc with float64 := true } - | "none" => { signedBV := false, unsignedBV := false, float64 := false } - | "all" => { signedBV := true, unsignedBV := true, float64 := true } - | _ => acc) { signedBV := false, unsignedBV := false, float64 := false } - let pathCap ← match pflags.getString "path-cap" with - | .none => pure base.pathCap - | .some "none" => pure .none - | .some s => match s.toNat? with - | .some n => if n == 0 then exitFailure "--path-cap must be at least 1 or 'none'." - else pure (.some n) - | .none => exitFailure s!"Invalid path-cap: '{s}'. Must be a positive number or 'none'." - let parallelWorkers ← match pflags.getString "parallel" with - | .none => pure base.parallelWorkers - | .some s => match s.toNat? with - | .some n => if n == 0 then exitFailure "--parallel must be at least 1." - else pure n - | .none => exitFailure s!"Invalid parallel workers: '{s}'. Must be a positive number." - let vcDirectory := (pflags.getString "vc-directory" |>.map (⟨·⟩ : String → System.FilePath)).orElse (fun _ => base.vcDirectory) - let skipSolver := noSolve || base.skipSolver - if skipSolver && vcDirectory.isNone then - exitFailure "--no-solve requires --vc-directory to specify where SMT files are stored." - pure { base with - verbose := if pflags.getBool "verbose" then .normal - else if pflags.getBool "quiet" then .quiet - else base.verbose, - solver := pflags.getString "solver" |>.getD base.solver, - solverTimeout, - checkMode, checkLevel, - stopOnFirstError := pflags.getBool "stop-on-first-error" || base.stopOnFirstError, - uniqueBoundNames := pflags.getBool "unique-bound-names" || base.uniqueBoundNames, - useArrayTheory := pflags.getBool "use-array-theory" || base.useArrayTheory, - removeIrrelevantAxioms, - outputSarif := pflags.getBool "sarif" || base.outputSarif, - profile := pflags.getBool "profile" || base.profile, - incremental := if noSolve || pflags.getBool "no-incremental" then false else base.incremental, - skipSolver, - alwaysGenerateSMT := noSolve || base.alwaysGenerateSMT, - overflowChecks, - vcDirectory, - pathCap, - parallelWorkers - } - -/-- Additional CLI flags for `LaurelVerifyOptions` fields that are not already - covered by `verifyOptionsFlags`. -/ -def laurelTranslateFlags : List Flag := [ - { name := "keep-all-files", - help := "Store intermediate Laurel and Core programs in .", - takesArg := .arg "dir" } -] - -/-- All CLI flags accepted by Laurel verify commands. -/ -def laurelVerifyOptionsFlags : List Flag := verifyOptionsFlags ++ laurelTranslateFlags - -/-- Build a `LaurelVerifyOptions` from parsed CLI flags. -/ -def parseLaurelVerifyOptions (pflags : ParsedFlags) - (base : LaurelVerifyOptions := default) : IO LaurelVerifyOptions := do - let verifyOptions ← parseVerifyOptions pflags base.verifyOptions - let keepAllFilesPrefix := (pflags.getString "keep-all-files").orElse - (fun _ => base.translateOptions.keepAllFilesPrefix) - let translateOptions : LaurelTranslateOptions := - { base.translateOptions with - keepAllFilesPrefix - overflowChecks := verifyOptions.overflowChecks - profile := verifyOptions.profile } - return { translateOptions, verifyOptions } - -/-- Read and parse a Strata program file, loading the Core, C_Simp, and B3CST - dialects. Returns the parsed program and the input context (for source - location resolution), or an array of error messages on failure. -/ -private def readStrataProgram (file : String) - : IO (Except (Array Lean.Message) (Strata.Program × Lean.Parser.InputContext)) := do - let text ← Strata.Util.readInputSource file - let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) - let dctx := Elab.LoadedDialects.builtin - let dctx := dctx.addDialect! Core - let dctx := dctx.addDialect! Boole - let dctx := dctx.addDialect! C_Simp - let dctx := dctx.addDialect! B3CST - let leanEnv ← Lean.mkEmptyEnvironment 0 - match Strata.Elab.elabProgram dctx leanEnv inputCtx with - | .ok pgm => pure (.ok (pgm, inputCtx)) - | .error msgs => pure (.error msgs) - -structure Command where - name : String - args : List String - flags : List Flag := [] - help : String - callback : Vector String args.length → ParsedFlags → IO Unit - -def includeFlag : Flag := - { name := "include", help := "Add a dialect search path.", takesArg := .repeat "path" } - -def checkCommand : Command where - name := "check" - args := [ "file" ] - flags := [includeFlag] - help := "Parse and validate a Strata file (text or Ion). Reports errors and exits." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let _ ← Strata.readStrataFile fm v[0] - -def toIonCommand : Command where - name := "toIon" - args := [ "input", "output" ] - flags := [includeFlag] - help := "Convert a Strata text file to Ion binary format." - callback := fun v pflags => do - let searchPath ← pflags.buildDialectFileMap - let pd ← Strata.readStrataFile searchPath v[0] - match pd with - | .dialect d => - IO.FS.writeBinFile v[1] d.toIon - | .program pgm => - IO.FS.writeBinFile v[1] pgm.toIon - -def printCommand : Command where - name := "print" - args := [ "file" ] - flags := [includeFlag] - help := "Pretty-print a Strata file (text or Ion) to stdout." - callback := fun v pflags => do - let searchPath ← pflags.buildDialectFileMap - -- Special case for already loaded dialects. - let ld ← searchPath.getLoaded - if mem : v[0] ∈ ld.dialects then - IO.print <| ld.dialects.format v[0] mem - return - let pd ← Strata.readStrataFile searchPath v[0] - match pd with - | .dialect d => - let ld ← searchPath.getLoaded - let .isTrue mem := (inferInstance : Decidable (d.name ∈ ld.dialects)) - | exitInternalError "Internal error reading file." - IO.print <| ld.dialects.format d.name mem - | .program pgm => - IO.print <| toString pgm - -def diffCommand : Command where - name := "diff" - args := [ "file1", "file2" ] - flags := [includeFlag] - help := "Compare two program files for syntactic equality. Reports the first difference found." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let p1 ← Strata.readStrataFile fm v[0] - let p2 ← Strata.readStrataFile fm v[1] - match p1, p2 with - | .program p1, .program p2 => - if p1.dialect != p2.dialect then - exitFailure s!"Dialects differ: {p1.dialect} and {p2.dialect}" - let Decidable.isTrue eq := (inferInstance : Decidable (p1.commands.size = p2.commands.size)) - | exitFailure s!"Number of commands differ {p1.commands.size} and {p2.commands.size}" - for (c1, c2) in Array.zip p1.commands p2.commands do - if c1 != c2 then - exitFailure s!"Commands differ: {repr c1} and {repr c2}" - | _, _ => - exitFailure "Cannot compare dialect def with another dialect/program." - -def pySpecsCommand : Command where - name := "pySpecs" - args := [ "source_dir", "output_dir" ] - flags := [ - { name := "quiet", help := "Suppress default logging." }, - { name := "log", help := "Enable logging for an event type.", - takesArg := .repeat "event" }, - { name := "skip", - help := "Skip a top-level definition (module.name). Overloads are kept.", - takesArg := .repeat "name" }, - { name := "module", - help := "Translate only the named module (dot-separated). May be repeated.", - takesArg := .repeat "module" } - ] - help := "Translate Python specification files in a directory into Strata DDM Ion format. If --module is given, translates only those modules; otherwise translates all .py files. Creates subdirectories as needed. (Experimental)" - callback := fun v pflags => do - let quiet := pflags.getBool "quiet" - let mut events : Std.HashSet String := {} - if !quiet then - events := events.insert "import" - for e in pflags.getRepeated "log" do - events := events.insert e - let skipNames := pflags.getRepeated "skip" - let modules := pflags.getRepeated "module" - let warningOutput : Strata.WarningOutput := - if quiet then .none else .detail - -- Serialize embedded dialect for Python subprocess - IO.FS.withTempFile fun _handle dialectFile => do - IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon - let r ← Strata.pySpecsDir (events := events) - (skipNames := skipNames) - (modules := modules) - (warningOutput := warningOutput) - v[0] v[1] dialectFile |>.toBaseIO - match r with - | .ok () => pure () - | .error msg => exitFailure msg - -/-- Derive Python source file path from Ion file path. - E.g., "tests/test_foo.python.st.ion" -> "tests/test_foo.py" -/ -def ionPathToPythonPath (ionPath : String) : Option String := - if ionPath.endsWith ".python.st.ion" then - let basePath := ionPath.dropEnd ".python.st.ion".length |>.toString - some (basePath ++ ".py") - else if ionPath.endsWith ".py.ion" then - some (ionPath.dropEnd ".ion".length |>.toString) - else - none - -/-- Try to read Python source file for source location reconstruction -/ -def tryReadPythonSource (ionPath : String) : IO (Option (String × String)) := do - match ionPathToPythonPath ionPath with - | none => return none - | some pyPath => - try - let content ← IO.FS.readFile pyPath - return some (pyPath, content) - catch _ => - return none - -/-- Format related position strings from metadata, if present. -/ -def formatRelatedPositions (md : Imperative.MetaData Core.Expression) - (mfm : Option (String × Lean.FileMap)) : String := - let ranges := Imperative.getRelatedFileRanges md - if ranges.isEmpty then "" else - match mfm with - | none => "" - | some (_, fm) => - let lines := ranges.filterMap fun fr => - if fr.range.isNone then none else - match fr.file with - | .file "" => some "\n Related location: in prelude file" - | .file _ => - let pos := fm.toPosition fr.range.start - some s!"\n Related location: line {pos.line}, col {pos.column}" - String.join lines.toList - -/-! ### pyAnalyzeLaurel result helpers - -The `pyAnalyzeLaurel` command emits two structured lines on stdout: -- `RESULT: ` — machine-readable category, always the last line. -- `DETAIL: ` — human-readable context (error message or VC counts). - -Exit codes follow the common scheme (see `ExitCode` above). -A successful run exits 0 with `RESULT: Analysis success` or `RESULT: Inconclusive`. -/ - -/-- Determines which VC results count as successes and which count as failures - for the purposes of the `pyAnalyzeLaurel` summary and exit code. - Implementation-error results are partitioned out first; the classifier then - partitions the rest into success / failure / inconclusive. - Narrowing `isFailure` (e.g. to only `alwaysFalseAndReachable`) automatically - widens inconclusive. - Future: may be extended with `isWarning` for non-fatal diagnostic categories. -/ -structure ResultClassifier where - isSuccess : Core.VCResult → Bool := (·.isSuccess) - isFailure : Core.VCResult → Bool := (·.isFailure) - -private def printPyAnalyzeResult (category : String) (detail : String) : IO Unit := do - IO.println s!"DETAIL: {detail}" - IO.println s!"RESULT: {category}" - -private def exitPyAnalyzeUserError {α} (message : String) : IO α := do - printPyAnalyzeResult "User error" message - IO.Process.exit ExitCode.userError - -private def exitPyAnalyzeFailuresFound {α} (detail : String) : IO α := do - printPyAnalyzeResult "Failures found" detail - IO.Process.exit ExitCode.failuresFound - -private def exitPyAnalyzeInternalError {α} (message : String) : IO α := do - printPyAnalyzeResult "Internal error" message - IO.Process.exit ExitCode.internalError - -private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do - printPyAnalyzeResult "Known limitation" message - IO.Process.exit ExitCode.knownLimitation - -/-- 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). - Classification uses successive partitioning: timeouts and implementation - errors are removed first, then the classifier partitions the rest into - success / failure / inconclusive (guaranteeing disjointness). - Unreachable count is reported as supplementary info. - - Exit-code priority (highest wins): - - Internal error (exit 3): encoding failures or solver crashes - - Failures found (exit 2): assertion violations - - Inconclusive / success / solver timeout (exit 0) -/ -private def printPyAnalyzeSummary (vcResults : Array Core.VCResult) - (checkMode : VerificationMode := .deductive) : IO Unit := do - let classifier : ResultClassifier := - match checkMode with - | .bugFinding | .bugFindingAssumingCompleteSpec => - { isSuccess := (·.isBugFindingSuccess) - isFailure := (·.isBugFindingFailure) } - | _ => {} - -- 1. Partition out implementation errors and timeouts (not classifiable). - let (implError, rest1) := - vcResults.partition (fun r => r.isImplementationError || r.hasSMTError) - let (timeouts, classifiable) := rest1.partition (·.isTimeout) - -- 2. Successive partitioning via the classifier: success → failure → inconclusive. - let (success, rest) := classifiable.partition classifier.isSuccess - let (failure, inconclusive) := rest.partition classifier.isFailure - -- 3. Unreachable is informational (not a separate partition). - let nUnreachable := vcResults.filter (·.isUnreachable) |>.size - let nImplError := implError.size - let nTimeout := timeouts.size - let nSuccess := success.size - let nFailure := failure.size - let nInconclusive := inconclusive.size - let unreachableStr := if nUnreachable > 0 then s!", {nUnreachable} unreachable" else "" - let implErrorStr := if nImplError > 0 then s!", {nImplError} internal errors" else "" - let timeoutStr := if nTimeout > 0 then s!", {nTimeout} solver timeouts" else "" - let counts := s!"{nSuccess} passed, {nFailure} failed, {nInconclusive} inconclusive{unreachableStr}{timeoutStr}{implErrorStr}" - if nImplError > 0 then - exitPyAnalyzeInternalError s!"An unexpected result was produced. {counts}" - else if nFailure > 0 then - exitPyAnalyzeFailuresFound counts - else - let label := - if nTimeout > 0 then "Solver timeout" - else if nInconclusive > 0 then "Inconclusive" - else "Analysis success" - printPyAnalyzeResult label counts - -private def deriveBaseName (file : String) : String := - let name := System.FilePath.fileName file |>.getD file - let suffixes := [".python.st.ion", ".py.ion", ".st.ion", ".st"] - match suffixes.find? (name.endsWith ·) with - | some sfx => (name.dropEnd sfx.length).toString - | none => name - - -def pyAnalyzeLaurelCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where - name := "pyAnalyzeLaurel" - args := [ "file" ] - flags := verifyOptionsFlags ++ [ - { name := "spec-dir", - help := "Directory containing compiled PySpec Ion files.", - takesArg := .arg "dir" }, - { name := "dispatch", - help := "Dispatch module name (e.g., servicelib).", - takesArg := .repeat "module" }, - { name := "pyspec", - help := "PySpec module name (e.g., servicelib.Storage).", - takesArg := .repeat "module" }, - { name := "keep-all-files", - help := "Store intermediate Laurel and Core programs in .", - takesArg := .arg "dir" }, - { name := "entry-point", - help := "Which procedures to verify: main (main fn only), roots (user procs with no user callers, default), or all (all user procs). Only valid in bugFinding mode.", - takesArg := .arg "mode" }, - { name := "warning-summary", - help := "Write PySpec warning summary as JSON to .", - takesArg := .arg "file" }, - { name := "skip-verification", - help := "Run Python-to-Laurel and Laurel-to-Core translation only (skip SMT verification).", - takesArg := .none }] - 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 profile := pflags.getBool "profile" - let quiet := pflags.getBool "quiet" - let outputSarif := pflags.getBool "sarif" - let filePath := v[0] - let pySourceOpt ← tryReadPythonSource filePath - let keepDir := pflags.getString "keep-all-files" - let baseName := deriveBaseName filePath - if let some dir := keepDir then - IO.FS.createDirAll dir - - let dispatchModules := pflags.getRepeated "dispatch" - let pyspecModules := pflags.getRepeated "pyspec" - let specDir := pflags.getString "spec-dir" |>.getD "." - unless ← System.FilePath.isDir specDir do - exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" - let sourcePath := pySourceOpt.map (·.1) - -- Build FileMap for source position resolution. - let mfm : Option (String × Lean.FileMap) := match pySourceOpt with - | some (pyPath, srcText) => some (pyPath, .ofString srcText) - | none => none - let warningSummaryFile := pflags.getString "warning-summary" - let combinedLaurel ← - match ← Strata.pythonAndSpecToLaurel filePath dispatchModules pyspecModules sourcePath - (specDir := specDir) (profile := profile) - (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 - - if verbose then - IO.println "\n==== Laurel Program ====" - IO.println f!"{combinedLaurel}" - - let keepPrefix := keepDir.map (s!"{·}/{baseName}") - - let (coreProgramOption, laurelTranslateErrors, _loweredLaurel, laurelPassStats) ← - profileStep profile "Laurel to Core translation" do - Strata.translateCombinedLaurelWithLowered combinedLaurel - (keepAllFilesPrefix := keepPrefix) (profile := profile) - - if profile && !laurelPassStats.data.isEmpty then - IO.println laurelPassStats.format - - let coreProgram ← - match coreProgramOption with - | none => - exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}" - | some core => pure core - - if verbose then - IO.println "\n==== Core Program ====" - IO.print (Core.formatProgram coreProgram) - - -- When --skip-verification is set, report translation diagnostics and exit - -- without running SMT verification (stages 3-4). - if pflags.getBool "skip-verification" then do - if !laurelTranslateErrors.isEmpty then - IO.eprintln "\n==== Errors ====" - for err in laurelTranslateErrors do - IO.eprintln err - if outputSarif then - let files := match mfm with - | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm - | none => Map.empty - Core.Sarif.writeSarifOutput .deductive files #[] (filePath ++ ".sarif") - let nStrataBug := laurelTranslateErrors.filter (·.type == .StrataBug) |>.length - let nNotYetImpl := laurelTranslateErrors.filter (·.type == .NotYetImplemented) |>.length - let nUserError := laurelTranslateErrors.filter (·.type == .UserError) |>.length - let nWarning := laurelTranslateErrors.filter (·.type == .Warning) |>.length - let counts := s!"{nUserError} user errors, {nWarning} warnings, {nNotYetImpl} not yet implemented, {nStrataBug} internal errors" - if nStrataBug > 0 then - exitPyAnalyzeInternalError s!"Translation produced internal errors. {counts}" - else if nNotYetImpl > 0 then - exitPyAnalyzeKnownLimitation s!"Translation encountered unsupported constructs. {counts}" - else - printPyAnalyzeResult "Analysis success" counts - return - - -- Verify using Core verifier - -- --keep-all-files implies vc-directory if not explicitly set - let baseVcDir := keepDir.map (fun dir => (s!"{dir}/{baseName}" : System.FilePath)) - let pyAnalyzeBase : VerifyOptions := - { VerifyOptions.default with - verbose := .quiet, removeIrrelevantAxioms := .Precise, - vcDirectory := baseVcDir } - let options ← parseVerifyOptions pflags pyAnalyzeBase - let isBugFinding := options.checkMode == .bugFinding - || options.checkMode == .bugFindingAssumingCompleteSpec - - -- Parse --entry-point flag (only supported in bug-finding modes). - let entryPointFlag := pflags.getString "entry-point" - let entryPoint : EntryPoint ← - if isBugFinding then - match entryPointFlag with - | some s => - match EntryPoint.ofString? s with - | some ep => pure ep - | none => - exitPyAnalyzeUserError s!"Invalid --entry-point value '{s}'. Must be {EntryPoint.options}." - | none => pure .roots - else - if entryPointFlag.isSome then - exitPyAnalyzeUserError s!"--entry-point is unsupported in {options.checkMode} mode" - else pure .all - - -- Pick the procedures to verify and set up inlining phases. - let userSourcePath := sourcePath.getD filePath - let (_, userProcNames) := - Strata.splitProcNames coreProgram [userSourcePath] - let (proceduresToVerify, inlinePhases) := - if isBugFinding then - let ⟨p, i⟩ := Core.chooseEntryProceduresAndBuildInlinePhases coreProgram userProcNames entryPoint - (p, [i]) - else (userProcNames, []) - - let vcResults ← profileStep profile "SMT verification" do - match ← Core.verifyProgram coreProgram options - (moreFns := Strata.Python.ReFactory) - (proceduresToVerify := some proceduresToVerify) - (externalPhases := [Strata.frontEndPhase]) - (prefixPhases := inlinePhases) - (keepAllFilesPrefix := keepPrefix) - (mkDischarge := mkDischarge) - |>.toBaseIO with - | .ok r => pure r.mergeByAssertion - | .error msg => exitPyAnalyzeInternalError msg - - -- Print translation errors (always on stderr) - if !laurelTranslateErrors.isEmpty then - IO.eprintln "\n==== Errors ====" - for err in laurelTranslateErrors do - IO.eprintln err - - -- Print per-VC results by default, unless SARIF mode is used - if !outputSarif then - let mut s := "" - for vcResult in vcResults do - let fileMap := mfm.map (·.2) - let location := match Imperative.getFileRange vcResult.obligation.metadata with - | some fr => - if fr.range.isNone then "" - else s!"{fr.format fileMap (includeEnd? := false)}" - | none => "" - let messageSuffix := match vcResult.obligation.metadata.getPropertySummary with - | some msg => s!" - {msg}" - | none => s!" - {vcResult.obligation.label}" - let outcomeStr := vcResult.formatOutcome - let loc := if !location.isEmpty then s!"{location}: " else "unknown location: " - s := s ++ s!"{loc}{outcomeStr}{messageSuffix}\n" - IO.print s - -- Output in SARIF format if requested - if outputSarif then - let files := match mfm with - | some (pyPath, fm) => Map.empty.insert (Strata.Uri.file pyPath) fm - | none => Map.empty - Core.Sarif.writeSarifOutput options.checkMode files vcResults (filePath ++ ".sarif") - printPyAnalyzeSummary vcResults options.checkMode - -def pyAnalyzeToGotoCommand : Command where - name := "pyAnalyzeToGoto" - args := [ "file" ] - help := "Translate a Strata Python Ion file to CProver GOTO JSON files." - callback := fun v _ => do - let filePath := v[0] - let pySourceOpt ← tryReadPythonSource filePath - let sourcePathForMetadata := match pySourceOpt with - | some (pyPath, _) => pyPath - | none => filePath - let sourceText := pySourceOpt.map (·.2) - let newPgm ← Strata.pythonDirectToCore filePath sourcePathForMetadata - match Core.inlineProcedures newPgm { doInline := (fun _caller callee _ => callee ≠ "main") } with - | .error e => exitInternalError (toString e) - | .ok newPgm => - -- Type-check the full program (registers Python types like ExceptOrNone) - let Ctx := { Lambda.LContext.default with functions := Strata.Python.PythonFactory, knownTypes := Core.KnownTypes } - let Env := Lambda.TEnv.default - let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env newPgm with - | .ok r => pure r - | .error e => exitInternalError s!"{e.format none}" - -- Find the main procedure - let some mainDecl := tcPgm.decls.find? fun d => - match d with - | .proc p _ => Core.CoreIdent.toPretty p.header.name == "main" - | _ => false - | exitInternalError "No main procedure found" - let some p := mainDecl.getProc? - | exitInternalError "main is not a procedure" - -- Translate procedure to GOTO (mirrors CoreToGOTO.transformToGoto post-typecheck logic) - let baseName := deriveBaseName filePath - let procName := Core.CoreIdent.toPretty p.header.name - let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? - let distincts := tcPgm.decls.filterMap fun d => match d with - | .distinct name es _ => some (name, es) | _ => none - match procedureToGotoCtx Env p sourceText (axioms := axioms) (distincts := distincts) - with - | .error e => exitInternalError s!"{e}" - | .ok (ctx, liftedFuncs) => - let extraSyms ← match collectExtraSymbols tcPgm with - | .ok s => pure (Lean.toJson s) - | .error e => exitInternalError s!"{e}" - let (symtab, goto) ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms - (moduleName := baseName) - let symTabFile := s!"{baseName}.symtab.json" - let gotoFile := s!"{baseName}.goto.json" - writeJsonFile symTabFile symtab - writeJsonFile gotoFile goto - IO.println s!"Written {symTabFile} and {gotoFile}" - -def pyTranslateLaurelCommand : Command where - name := "pyTranslateLaurel" - args := [ "file" ] - flags := [{ name := "pyspec", - help := "PySpec module name (e.g., servicelib.Storage).", - takesArg := .repeat "module" }, - { name := "dispatch", - help := "Dispatch module name (e.g., servicelib).", - takesArg := .repeat "module" }, - { name := "spec-dir", - help := "Directory containing compiled PySpec Ion files.", - takesArg := .arg "dir" }] - help := "Translate a Strata Python Ion file through Laurel to Strata Core. Write results to stdout." - callback := fun v pflags => do - let dispatchModules := pflags.getRepeated "dispatch" - let pyspecModules := pflags.getRepeated "pyspec" - let specDir := pflags.getString "spec-dir" |>.getD "." - unless ← System.FilePath.isDir specDir do - exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" - let coreProgram ← - match ← Strata.pyTranslateLaurel v[0] dispatchModules pyspecModules (specDir := specDir) |>.toBaseIO with - | .ok r => pure r - | .error msg => exitFailure msg - IO.print coreProgram - -def pyAnalyzeLaurelToGotoCommand : Command where - name := "pyAnalyzeLaurelToGoto" - args := [ "file" ] - flags := [{ name := "pyspec", - help := "PySpec module name (e.g., servicelib.Storage).", - takesArg := .repeat "module" }, - { name := "dispatch", - help := "Dispatch module name (e.g., servicelib).", - takesArg := .repeat "module" }, - { name := "spec-dir", - help := "Directory containing compiled PySpec Ion files.", - takesArg := .arg "dir" }] - help := "Translate a Strata Python Ion file through Laurel to CProver GOTO JSON files." - callback := fun v pflags => do - let filePath := v[0] - let dispatchModules := pflags.getRepeated "dispatch" - let pyspecModules := pflags.getRepeated "pyspec" - let specDir := pflags.getString "spec-dir" |>.getD "." - unless ← System.FilePath.isDir specDir do - exitFailure s!"spec-dir '{specDir}' does not exist or is not a directory" - let (coreProgram, laurelTranslateErrors) ← - match ← Strata.pyTranslateLaurel filePath dispatchModules pyspecModules (specDir := specDir) |>.toBaseIO with - | .ok r => pure r - | .error msg => exitFailure msg - let sourceText := (← tryReadPythonSource filePath).map (·.2) - let baseName := deriveBaseName filePath - match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText - (factory := Strata.Python.PythonFactory) |>.toBaseIO with - | .ok () => pure () - | .error msg => exitFailure msg - -def javaGenCommand : Command where - name := "javaGen" - args := [ "dialect", "package", "output-dir" ] - flags := [includeFlag] - help := "Generate Java source files from a DDM dialect definition. Accepts a dialect name (e.g. Laurel) or a dialect file path." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let ld ← fm.getLoaded - let d ← if mem : v[0] ∈ ld.dialects then - pure ld.dialects[v[0]] - else - match ← Strata.readStrataFile fm v[0] with - | .dialect d => pure d - | .program _ => exitFailure "Expected a dialect file, not a program file." - match Strata.Java.generateDialect d v[1] with - | .ok files => - Strata.Java.writeJavaFiles v[2] v[1] files - IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.packageToPath v[1]}" - | .error msg => - exitFailure s!"Error generating Java: {msg}" - -def laurelAnalyzeBinaryCommand : Command where - name := "laurelAnalyzeBinary" - args := [] - flags := laurelVerifyOptionsFlags - help := "Verify Laurel Ion programs read from stdin and print diagnostics. Combines multiple input files." - callback := fun _ pflags => do - let options ← parseLaurelVerifyOptions pflags - let stdinBytes ← (← IO.getStdin).readBinToEnd - let combinedProgram ← Strata.readLaurelIonProgram stdinBytes - let diagnostics ← Strata.Laurel.verifyToDiagnosticModels combinedProgram options - - IO.println s!"==== DIAGNOSTICS ====" - for diag in diagnostics do - IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}" - -def pySpecToLaurelCommand : Command where - name := "pySpecToLaurel" - args := [ "python_path", "strata_path" ] - help := "Translate a PySpec Ion file to Laurel declarations. The Ion file must already exist." - callback := fun v _ => do - let pythonFile : System.FilePath := v[0] - let strataDir : System.FilePath := v[1] - let some mod := pythonFile.fileStem - | exitFailure s!"No stem {pythonFile}" - let .ok mod := Strata.Python.Specs.ModuleName.ofString mod - | exitFailure s!"Invalid module {mod}" - let ionFile := strataDir / mod.strataFileName - let sigs ← - match ← Strata.Python.Specs.readDDM ionFile |>.toBaseIO with - | .ok t => pure t - | .error msg => exitFailure s!"Could not read {ionFile}: {msg}" - let result := Strata.Python.Specs.ToLaurel.signaturesToLaurel pythonFile sigs "" - if result.errors.size > 0 then - IO.eprintln s!"{result.errors.size} translation warning(s):" - for err in result.errors do - IO.eprintln s!" {err.file}: {err.message}" - let pgm := result.program - IO.println s!"Laurel: {pgm.staticProcedures.length} procedure(s), {pgm.types.length} type(s)" - IO.println s!"Overloads: {result.overloads.size} function(s)" - for td in pgm.types do - IO.println s!" {Strata.Laurel.formatTypeDefinition td}" - for proc in pgm.staticProcedures do - IO.println s!" {Strata.Laurel.formatProcedure proc}" - -def pyResolveOverloadsCommand : Command where - name := "pyResolveOverloads" - args := [ "python_path", "dispatch_ion" ] - help := "Identify which overloaded service modules a \ - Python program uses. Prints one module name per \ - line to stdout." - callback := fun v _ => do - let pythonFile : System.FilePath := v[0] - let dispatchPath := v[1] - -- Read dispatch overload table - let overloads ← - match ← readDispatchOverloads #[dispatchPath] |>.toBaseIO with - | .ok (r, _) => pure r - | .error msg => exitFailure msg - -- Convert .py to Python AST - let stmts ← - IO.FS.withTempFile fun _handle dialectFile => do - IO.FS.writeBinFile dialectFile - Strata.Python.Python.toIon - match ← Strata.Python.pythonToStrata dialectFile pythonFile |>.toBaseIO with - | .ok s => pure s - | .error msg => exitFailure msg - -- Walk AST and collect modules - let state := - Strata.Python.Specs.IdentifyOverloads.resolveOverloads - overloads stmts - for w in state.warnings do - IO.eprintln s!"warning: {w}" - let sorted := state.modules.toArray.qsort (· < ·) - for m in sorted do - IO.println m - -def laurelParseCommand : Command where - name := "laurelParse" - args := [ "file" ] - help := "Parse a Laurel source file (no verification)." - callback := fun v _ => do - let _ ← Strata.readLaurelTextFile v[0] - IO.println "Parse successful" - -def laurelAnalyzeCommand : Command where - name := "laurelAnalyze" - args := [ "file" ] - flags := laurelVerifyOptionsFlags - help := "Analyze a Laurel source file. Write diagnostics to stdout." - callback := fun v pflags => do - let options ← parseLaurelVerifyOptions pflags - let laurelProgram ← Strata.readLaurelTextFile v[0] - let (vcResultsOption, errors) ← Strata.Laurel.verifyToVcResults laurelProgram options - if !errors.isEmpty then - IO.println s!"==== ERRORS ====" - for err in errors do - IO.println s!"{err.message}" - match vcResultsOption with - | none => return - | some vcResults => - IO.println s!"==== RESULTS ====" - for vc in vcResults do - IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => toString e}" - -def laurelAnalyzeToGotoCommand : Command where - name := "laurelAnalyzeToGoto" - args := [ "file" ] - help := "Translate a Laurel source file to CProver GOTO JSON files." - callback := fun v _ => do - let path : System.FilePath := v[0] - let content ← IO.FS.readFile path - let laurelProgram ← Strata.parseLaurelText path content - match ← Strata.Laurel.translate {} laurelProgram with - | (none, diags) => exitFailure s!"Core translation errors: {diags.map (·.message)}" - | (some coreProgram, errors) => - let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } - let Env := Lambda.TEnv.default - let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env coreProgram with - | .ok r => pure r - | .error e => exitInternalError s!"{e.format none}" - let procs := tcPgm.decls.filterMap fun d => d.getProc? - let funcs := tcPgm.decls.filterMap fun d => - match d.getFunc? with - | some f => - let name := Core.CoreIdent.toPretty f.name - if f.body.isSome && f.typeArgs.isEmpty - && name != "Int.DivT" && name != "Int.ModT" - then some f else none - | none => none - if procs.isEmpty && funcs.isEmpty then exitInternalError "No procedures or functions found" - let baseName := deriveBaseName path.toString - let typeSyms ← match collectExtraSymbols tcPgm with - | .ok s => pure s - | .error e => exitInternalError s!"{e}" - let typeSymsJson := Lean.toJson typeSyms - let sourceText := some content - let axioms := tcPgm.decls.filterMap fun d => d.getAxiom? - let distincts := tcPgm.decls.filterMap fun d => match d with - | .distinct name es _ => some (name, es) | _ => none - let mut symtabPairs : List (String × Lean.Json) := [] - let mut gotoFns : Array Lean.Json := #[] - let mut allLiftedFuncs : List Core.Function := [] - for p in procs do - let procName := Core.CoreIdent.toPretty p.header.name - match procedureToGotoCtx Env p (sourceText := sourceText) (axioms := axioms) (distincts := distincts) - with - | .error e => exitInternalError s!"{e}" - | .ok (ctx, liftedFuncs) => - allLiftedFuncs := allLiftedFuncs ++ liftedFuncs - let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx) - match json.symtab with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - match json.goto with - | .obj m => - match m.toList.find? (·.1 == "functions") with - | some (_, .arr fns) => gotoFns := gotoFns ++ fns - | _ => pure () - | _ => pure () - for f in funcs ++ allLiftedFuncs do - let funcName := Core.CoreIdent.toPretty f.name - match functionToGotoCtx Env f with - | .error e => exitInternalError s!"{e}" - | .ok ctx => - let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx) - match json.symtab with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - match json.goto with - | .obj m => - match m.toList.find? (·.1 == "functions") with - | some (_, .arr fns) => gotoFns := gotoFns ++ fns - | _ => pure () - | _ => pure () - match typeSymsJson with - | .obj m => symtabPairs := symtabPairs ++ m.toList - | _ => pure () - -- Deduplicate: keep first occurrence of each symbol name (proper function - -- symbols come before basic symbol references from callers) - let mut seen : Std.HashSet String := {} - let mut dedupPairs : List (String × Lean.Json) := [] - for (k, v) in symtabPairs do - if !seen.contains k then - seen := seen.insert k - dedupPairs := dedupPairs ++ [(k, v)] - -- Add CBMC default symbols (architecture constants, builtins) - -- and wrap in {"symbolTable": ...} for symtab2gb - let symtabObj := dedupPairs.foldl - (fun (acc : Std.TreeMap.Raw String Lean.Json) (k, v) => acc.insert k v) - .empty - let symtab := CProverGOTO.wrapSymtab symtabObj (moduleName := baseName) - let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)] - let symTabFile := s!"{baseName}.symtab.json" - let gotoFile := s!"{baseName}.goto.json" - writeJsonFile symTabFile symtab - writeJsonFile gotoFile goto - IO.println s!"Written {symTabFile} and {gotoFile}" - -def laurelPrintCommand : Command where - name := "laurelPrint" - args := [] - help := "Read Laurel Ion from stdin and print in concrete syntax to stdout." - callback := fun _ _ => do - let stdinBytes ← (← IO.getStdin).readBinToEnd - let strataFiles ← Strata.readLaurelIonFiles stdinBytes - for strataFile in strataFiles do - IO.println s!"// File: {strataFile.filePath}" - let p := strataFile.program - let c := p.formatContext {} - let s := p.formatState - let fmt := p.commands.foldl (init := f!"") fun f cmd => - f ++ (Strata.mformat cmd c s).format - IO.println (fmt.pretty 100) - IO.println "" - -def prettyPrintCore (p : Core.Program) : String := - let decls := p.decls.map fun d => - let s := toString (Std.format d) - -- Add newlines after major sections in procedures - s.replace "preconditions:" "\n preconditions:" - |>.replace "postconditions:" "\n postconditions:" - |>.replace "body:" "\n body:\n " - |>.replace "assert [" "\n assert [" - |>.replace "init (" "\n init (" - |>.replace "while (" "\n while (" - |>.replace "if (" "\n if (" - |>.replace "call [" "\n call [" - |>.replace "else{" "\n else {" - |>.replace "}}" "}\n }" - String.intercalate "\n" decls - -def laurelToCoreCommand : Command where - name := "laurelToCore" - args := [ "file" ] - help := "Translate a Laurel source file to Core and print to stdout." - callback := fun v _ => do - let laurelProgram ← Strata.readLaurelTextFile v[0] - let (coreProgramOption, errors) ← Strata.Laurel.translate {} laurelProgram - if !errors.isEmpty then - IO.println s!"Core translation errors: {errors.map (·.message)}" - match coreProgramOption with - | none => return - | some coreProgram => IO.println (prettyPrintCore coreProgram) - -/-- Print a string word-wrapped to `width` columns with `indent` spaces of indentation. -/ -private def printIndented (indent : Nat) (s : String) (width : Nat := 80) : IO Unit := do - let pad := "".pushn ' ' indent - let words := s.splitOn " " |>.filter (!·.isEmpty) - let mut line := pad - let mut first := true - for word in words do - if first then - line := line ++ word - first := false - else if line.length + 1 + word.length > width then - IO.println line - line := pad ++ word - else - line := line ++ " " ++ word - unless line.length ≤ indent do - IO.println line - -structure CommandGroup where - name : String - commands : List Command - commonFlags : List Flag := [] - -private def validPasses := - "inlineProcedures, loopElim, callElim, filterProcedures, removeIrrelevantAxioms" - -/-- A single transform pass together with the `--procedures`/`--functions` - that were specified immediately after it on the command line. -/ -private structure PassConfig where - name : String - procedures : List String := [] - functions : List String := [] -deriving Inhabited - -/-- Walk the ordered flag entries and bind each `--procedures`/`--functions` - to the most recent `--pass`. -/ -private def buildPassConfigs (entries : Array (String × Option String)) - : IO (Array PassConfig) := do - let mut configs : Array PassConfig := #[] - for (flag, value) in entries do - match flag with - | "pass" => configs := configs.push { name := value.getD "" } - | "procedures" => - let some cur := configs.back? | exitFailure "--procedures must appear after a --pass" - let procs := (value.getD "").splitToList (· == ',') - configs := configs.pop.push { cur with procedures := cur.procedures ++ procs } - | "functions" => - let some cur := configs.back? | exitFailure "--functions must appear after a --pass" - let fns := (value.getD "").splitToList (· == ',') - configs := configs.pop.push { cur with functions := cur.functions ++ fns } - | _ => pure () - return configs - -def transformCommand : Command where - name := "transform" - args := [ "file" ] - flags := [ - { name := "pass", - help := s!"Transform pass to apply (repeatable, applied left to right). \ - Valid passes: {validPasses}. \ - --procedures and --functions after a --pass apply to that pass.", - takesArg := .repeat "name" }, - { name := "procedures", - help := "Comma-separated procedure names for the preceding --pass. \ - For filterProcedures: procedures to keep. \ - For inlineProcedures: procedures to inline.", - takesArg := .repeat "procs" }, - { name := "functions", - help := "Comma-separated function names for the preceding --pass (used by removeIrrelevantAxioms).", - takesArg := .repeat "funcs" }] - help := "Apply one or more transforms to a Core program and print the result." - callback := fun v pflags => do - let file := v[0] - let passConfigs ← buildPassConfigs pflags.entries - if passConfigs.isEmpty then - exitFailure s!"No --pass specified. Valid passes: {validPasses}." - -- Read and parse the Core program - let (pgm, _) ← match ← readStrataProgram file with - | .ok r => pure r - | .error msgs => - for e in msgs do println! s!"Error: {← e.toString}" - exitFailure s!"{msgs.size} parse error(s)" - match Strata.genericToCore pgm with - | .error msg => - exitFailure msg - | .ok initProgram => - -- Validate and convert pass configs to TransformPass values - let mut passes : List Strata.Core.TransformPass := [] - for pc in passConfigs do - match pc.name with - | "inlineProcedures" => - let opts : Core.InlineTransformOptions := - if pc.procedures.isEmpty then {} - else { doInline := (fun _caller callee _ => callee ∈ pc.procedures) } - passes := passes ++ [.inlineProcedures opts] - | "loopElim" => - passes := passes ++ [.loopElim] - | "callElim" => - passes := passes ++ [.callElim] - | "filterProcedures" => - if pc.procedures.isEmpty then - exitFailure "filterProcedures requires --procedures" - passes := passes ++ [.filterProcedures pc.procedures] - | "removeIrrelevantAxioms" => - if pc.functions.isEmpty then - exitFailure "removeIrrelevantAxioms requires --functions" - passes := passes ++ [.removeIrrelevantAxioms pc.functions] - | other => - exitFailure s!"Unknown pass '{other}'. Valid passes: {validPasses}." - -- Run all passes in a single CoreTransformM chain so fresh variable - -- counters accumulate and cached analyses are reused across passes. - match Strata.Core.runTransforms initProgram passes with - | .ok program => IO.print (Core.formatProgram program) - | .error e => exitFailure s!"Transform failed: {e}" - -def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where - name := "verify" - args := [ "file" ] - flags := verifyOptionsFlags ++ [ - { name := "check", help := "Process up until SMT generation, but don't solve." }, - { name := "type-check", help := "Exit after semantic dialect's type inference/checking." }, - { name := "parse-only", help := "Exit after DDM parsing and type checking." }, - { name := "output-format", help := "Output format (only 'sarif' supported).", takesArg := .arg "format" }, - { name := "procedures", help := "Verify only the specified procedures (comma-separated).", takesArg := .arg "procs" }] - help := "Verify a Strata program file (.core.st, .csimp.st, or .b3.st)." - callback := fun v pflags => do - let file := v[0] - let proceduresToVerify := pflags.getString "procedures" |>.map (·.splitToList (· == ',')) - let opts ← parseVerifyOptions pflags { VerifyOptions.default with verbose := .quiet } - let opts := { opts with - checkOnly := pflags.getBool "check", - typeCheckOnly := pflags.getBool "type-check", - parseOnly := pflags.getBool "parse-only", - outputSarif := opts.outputSarif || pflags.getString "output-format" == some "sarif" } - let (pgm, inputCtx) ← match ← readStrataProgram file with - | .ok r => pure r - | .error errors => - for e in errors do - let msg ← e.toString - println! s!"Error: {msg}" - println! f!"Finished with {errors.size} errors." - IO.Process.exit ExitCode.userError - println! s!"Successfully parsed." - if opts.parseOnly then return - if opts.typeCheckOnly then - let ans := if file.endsWith ".csimp.st" then - C_Simp.typeCheck pgm opts - else if pgm.dialect == "Boole" then - Boole.typeCheck pgm opts - else - typeCheck inputCtx pgm opts - match ans with - | .error e => - println! f!"{e.formatRange (some inputCtx.fileMap) true} {e.message}" - IO.Process.exit ExitCode.userError - | .ok _ => - println! f!"Program typechecked." - return - -- Full verification - let vcResults ← try - if file.endsWith ".csimp.st" then - C_Simp.verify pgm opts - else if file.endsWith ".b3.st" || file.endsWith ".b3cst.st" then - let ast ← match B3.Verifier.programToB3AST pgm with - | Except.error msg => throw (IO.userError s!"Failed to convert to B3 AST: {msg}") - | Except.ok ast => pure ast - let solver ← B3.Verifier.createInteractiveSolver opts.solver - let reports ← B3.Verifier.programToSMT ast solver - for report in reports do - IO.println s!"\nProcedure: {report.procedureName}" - for (result, _) in report.results do - let marker := if result.result.isError then "✗" else "✓" - let desc := match result.result with - | .error .counterexample => "counterexample found" - | .error .unknown => "unknown" - | .error .refuted => "refuted" - | .success .verified => "verified" - | .success .reachable => "reachable" - | .success .reachabilityUnknown => "reachability unknown" - IO.println s!" {marker} {desc}" - pure #[] - else if pgm.dialect == "Boole" then - Boole.verify opts.solver pgm inputCtx proceduresToVerify opts - else - verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge) - catch e => - println! f!"{e}" - IO.Process.exit ExitCode.internalError - if opts.outputSarif then - 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 uri := Strata.Uri.file file - let files := Map.empty.insert uri inputCtx.fileMap - Core.Sarif.writeSarifOutput opts.checkMode files vcResults (file ++ ".sarif") - for vcResult in vcResults do - let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata (some inputCtx.fileMap) - println! f!"{posStr} [{vcResult.obligation.label}]: \ - {vcResult.formatOutcome}" - let success := vcResults.all Core.VCResult.isSuccess - if success && !opts.checkOnly then - println! f!"All {vcResults.size} goals passed." - else if success && opts.checkOnly then - println! f!"Skipping verification." - else - let provedGoalCount := (vcResults.filter Core.VCResult.isSuccess).size - let failedGoalCount := (vcResults.filter Core.VCResult.isNotSuccess).size - -- Encoding failures, solver crashes, or per-check SMT errors (exit 3) - let hasImplError := vcResults.any (fun r => r.isImplementationError || r.hasSMTError) - -- Assertion violations that are not timeouts or internal errors (exit 2) - let hasFailure := vcResults.any (fun r => !r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError) - println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed." - if hasImplError then - IO.Process.exit ExitCode.internalError - else if hasFailure then - IO.Process.exit ExitCode.failuresFound - -def pyInterpretCommand : Command where - name := "pyInterpret" - args := [ "file" ] - flags := [{ name := "fuel", help := "Maximum execution steps.", takesArg := .arg "n" }] - ++ laurelTranslateFlags - help := "Interpret a Python Ion program concretely (Python → Laurel → Core → execute)." - callback := fun v pflags => do - let filePath := v[0] - let keepDir := pflags.getString "keep-all-files" - let fuel ← match pflags.getString "fuel" with - | some s => match s.toNat? with - | .some n => pure n - | .none => exitFailure s!"Invalid fuel: '{s}'" - | none => pure 10000 - - let (core, _diags) ← - match ← Strata.pythonAndSpecToLaurel filePath (specDir := ".") |>.toBaseIO with - | .ok laurel => - if let some dir := keepDir then - IO.FS.createDirAll dir - IO.FS.writeFile (dir ++ "/laurel.st") (toString (Std.format laurel)) - match ← Strata.translateCombinedLaurel laurel with - | (some core, diags) => pure (core, diags) - | (none, diags) => exitFailure s!"Laurel to Core translation failed: {diags}" - | .error msg => exitFailure (toString msg) - if let some dir := keepDir then - IO.FS.writeFile (dir ++ "/core.st") (toString (Std.format core)) - let core ← match Core.typeCheck Core.VerifyOptions.quiet core - (moreFns := Strata.Python.ReFactory) with - | .ok prog => pure prog - | .error e => - println! s!"Core type checking failed: {e.message}" - IO.Process.exit ExitCode.userError - match core.run with - | .ok E => - let mainProc := Core.Program.Procedure.find? core ⟨"__main__", ()⟩ - let outputNames := match mainProc with - | some p => p.header.outputs.keys.map (·.name) - | none => [] - let (lhs, exprEnv) := Core.Env.genVars outputNames E.exprEnv - let E := { E with exprEnv } - let E := Core.Statement.Command.runCall lhs "__main__" [] fuel E - match E.error with - | none => - IO.println "Execution completed successfully." - | some e => - IO.println s!"{Std.format e}" - IO.Process.exit ExitCode.failuresFound - | .error diag => - IO.eprintln s!"Error: {diag}" - IO.Process.exit ExitCode.failuresFound - -def commandGroups : List CommandGroup := [ - { name := "Core" - commands := [verifyCommand, transformCommand, checkCommand, toIonCommand, printCommand, diffCommand] - commonFlags := [includeFlag] }, - { name := "Code Generation" - commands := [javaGenCommand] }, - { name := "Python" - commands := [pyAnalyzeLaurelCommand, - pyResolveOverloadsCommand, - pySpecsCommand, pySpecToLaurelCommand, - pyAnalyzeLaurelToGotoCommand, - pyAnalyzeToGotoCommand, - pyTranslateLaurelCommand, - pyInterpretCommand] }, - { name := "Laurel" - commands := [laurelAnalyzeCommand, laurelAnalyzeBinaryCommand, - laurelAnalyzeToGotoCommand, laurelParseCommand, - laurelPrintCommand, laurelToCoreCommand] }, -] - -def commandList : List Command := - commandGroups.foldl (init := []) fun acc g => acc ++ g.commands - -def commandMap : Std.HashMap String Command := - commandList.foldl (init := {}) fun m c => m.insert c.name c - -/-- Print a single flag's name and help text at the given indentation. -/ -private def printFlag (indent : Nat) (flag : Flag) : IO Unit := do - let pad := "".pushn ' ' indent - match flag.takesArg with - | .arg argName | .repeat argName => - IO.println s!"{pad}--{flag.name} <{argName}> {flag.help}" - | .none => - IO.println s!"{pad}--{flag.name} {flag.help}" - -/-- Print help for all command groups. -/ -def printGlobalHelp (groups : List CommandGroup := commandGroups) : IO Unit := do - IO.println "Usage: strata [flags]...\n" - IO.println "Command-line utilities for working with Strata.\n" - for group in groups do - IO.println s!"{group.name}:" - for cmd in group.commands do - let cmdLine := cmd.args.foldl (init := cmd.name) fun s a => s!"{s} <{a}>" - IO.println s!" {cmdLine}" - printIndented 4 cmd.help - let perCmdFlags := cmd.flags.filter fun f => - !group.commonFlags.any fun cf => cf.name == f.name - if !perCmdFlags.isEmpty then - IO.println "" - IO.println " Flags:" - for flag in perCmdFlags do - printFlag 6 flag - IO.println "" - if !group.commonFlags.isEmpty then - IO.println " Common flags:" - for flag in group.commonFlags do - printFlag 4 flag - IO.println "" - -/-- Print help for a single command. -/ -def printCommandHelp (cmd : Command) : IO Unit := do - let cmdLine := cmd.args.foldl (init := s!"strata {cmd.name}") fun s a => s!"{s} <{a}>" - let flagSummary := cmd.flags.foldl (init := "") fun s f => - match f.takesArg with - | .arg argName | .repeat argName => s!"{s} [--{f.name} <{argName}>]" - | .none => s!"{s} [--{f.name}]" - IO.println s!"Usage: {cmdLine}{flagSummary}\n" - printIndented 0 cmd.help - if !cmd.flags.isEmpty then - IO.println "\nFlags:" - for flag in cmd.flags do - printFlag 2 flag - -/-- Parse interleaved flags and positional arguments. Returns the collected - positional arguments and parsed flags. -/ -def parseArgs (cmdName : String) - (flagMap : Std.HashMap String Flag) - (acc : Array String) (pflags : ParsedFlags) - (cmdArgs : List String) : IO (Array String × ParsedFlags) := do - match cmdArgs with - | arg :: cmdArgs => - if arg.startsWith "--" then - let raw := (arg.drop 2).toString - -- Support --flag=value syntax by splitting on first '=' - let (flagName, inlineValue) ← match raw.splitOn "=" with - | name :: value :: rest => - if !rest.isEmpty then - exitCmdFailure cmdName s!"Invalid option format: {arg}. Values must not contain '='." - pure (name, some value) - | _ => pure (raw, none) - match flagMap[flagName]? with - | some flag => - match flag.takesArg with - | .none => - parseArgs cmdName flagMap acc (pflags.insert flagName Option.none) cmdArgs - | .arg _ => - match inlineValue with - | some value => - parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs - | none => - let value :: cmdArgs := cmdArgs - | exitCmdFailure cmdName s!"Expected value after {arg}." - parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs - | .repeat _ => - match inlineValue with - | some value => - parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs - | none => - let value :: cmdArgs := cmdArgs - | exitCmdFailure cmdName s!"Expected value after {arg}." - parseArgs cmdName flagMap acc (pflags.insert flagName (some value)) cmdArgs - | none => - exitCmdFailure cmdName s!"Unknown option {arg}." - else - parseArgs cmdName flagMap (acc.push arg) pflags cmdArgs - | [] => - pure (acc, pflags) - -/-- Dispatch CLI arguments against a command map. This is the shared entry point - that both the default executable and downstream custom executables use. -/ -def runCommandMap (map : Std.HashMap String Command) - (groups : List CommandGroup) (args : List String) : IO Unit := do - try do - match args with - | ["--help"] => printGlobalHelp groups - | cmd :: args => - match map[cmd]? with - | none => exitFailure s!"Expected subcommand, got {cmd}." - | some cmd => - -- Handle per-command help before parsing flags. - if args.contains "--help" then - printCommandHelp cmd - return - -- Index the command's flags by name for O(1) lookup during parsing. - let flagMap : Std.HashMap String Flag := - cmd.flags.foldl (init := {}) fun m f => m.insert f.name f - -- Split raw args into positional arguments and parsed flags. - let (args, pflags) ← parseArgs cmd.name flagMap #[] {} args - if p : args.size = cmd.args.length then - cmd.callback ⟨args, p⟩ pflags - else - exitCmdFailure cmd.name s!"{cmd.name} expects {cmd.args.length} argument(s)." - | [] => do - exitFailure "Expected subcommand." - catch e => - exitFailure e.toString From 9ff52b32fa194cf9a20364624c1039a73d6a79da Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 15 May 2026 19:16:04 +0000 Subject: [PATCH 5/6] Rename StrataMain.lean to StrataMainLib.lean (git mv for merge tracking) --- StrataMain.lean => StrataMainLib.lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename StrataMain.lean => StrataMainLib.lean (100%) diff --git a/StrataMain.lean b/StrataMainLib.lean similarity index 100% rename from StrataMain.lean rename to StrataMainLib.lean From 887e55630552e8a020a46e139342a37529ab8f4f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 15 May 2026 19:16:34 +0000 Subject: [PATCH 6/6] Split into importable library and thin executable - Remove 'module' keyword from StrataMainLib (now a library) - Parameterize verifyCommand and pyAnalyzeLaurelCommand with mkDischarge - Make printGlobalHelp, printCommandHelp, parseArgs public - Replace main with runCommandMap dispatcher for downstream reuse - Create thin StrataMain.lean that imports StrataMainLib --- StrataMain.lean | 9 +++++++++ StrataMainLib.lean | 26 ++++++++++++++------------ 2 files changed, 23 insertions(+), 12 deletions(-) create mode 100644 StrataMain.lean diff --git a/StrataMain.lean b/StrataMain.lean new file mode 100644 index 0000000000..826504e67f --- /dev/null +++ b/StrataMain.lean @@ -0,0 +1,9 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataMainLib + +def main (args : List String) : IO Unit := + runCommandMap commandMap commandGroups args diff --git a/StrataMainLib.lean b/StrataMainLib.lean index 9ae4839a21..0d9290c6e5 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -3,7 +3,6 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -module -- Executable with utilities for working with Strata files. import Lean.Parser.Extension @@ -576,7 +575,7 @@ private def deriveBaseName (file : String) : String := | none => name -def pyAnalyzeLaurelCommand : Command where +def pyAnalyzeLaurelCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where name := "pyAnalyzeLaurel" args := [ "file" ] flags := verifyOptionsFlags ++ [ @@ -748,6 +747,7 @@ def pyAnalyzeLaurelCommand : Command where (externalPhases := [Strata.frontEndPhase]) (prefixPhases := inlinePhases) (keepAllFilesPrefix := keepPrefix) + (mkDischarge := mkDischarge) |>.toBaseIO with | .ok r => pure r.mergeByAssertion | .error msg => exitPyAnalyzeInternalError msg @@ -1269,7 +1269,7 @@ def transformCommand : Command where | .ok program => IO.print (Core.formatProgram program) | .error e => exitFailure s!"Transform failed: {e}" -def verifyCommand : Command where +def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where name := "verify" args := [ "file" ] flags := verifyOptionsFlags ++ [ @@ -1338,7 +1338,7 @@ def verifyCommand : Command where else if pgm.dialect == "Boole" then Boole.verify opts.solver pgm inputCtx proceduresToVerify opts else - verify pgm inputCtx proceduresToVerify opts + verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge) catch e => println! f!"{e}" IO.Process.exit ExitCode.internalError @@ -1459,10 +1459,10 @@ private def printFlag (indent : Nat) (flag : Flag) : IO Unit := do IO.println s!"{pad}--{flag.name} {flag.help}" /-- Print help for all command groups. -/ -private def printGlobalHelp : IO Unit := do +def printGlobalHelp (groups : List CommandGroup := commandGroups) : IO Unit := do IO.println "Usage: strata [flags]...\n" IO.println "Command-line utilities for working with Strata.\n" - for group in commandGroups do + for group in groups do IO.println s!"{group.name}:" for cmd in group.commands do let cmdLine := cmd.args.foldl (init := cmd.name) fun s a => s!"{s} <{a}>" @@ -1483,7 +1483,7 @@ private def printGlobalHelp : IO Unit := do IO.println "" /-- Print help for a single command. -/ -private def printCommandHelp (cmd : Command) : IO Unit := do +def printCommandHelp (cmd : Command) : IO Unit := do let cmdLine := cmd.args.foldl (init := s!"strata {cmd.name}") fun s a => s!"{s} <{a}>" let flagSummary := cmd.flags.foldl (init := "") fun s f => match f.takesArg with @@ -1498,7 +1498,7 @@ private def printCommandHelp (cmd : Command) : IO Unit := do /-- Parse interleaved flags and positional arguments. Returns the collected positional arguments and parsed flags. -/ -private def parseArgs (cmdName : String) +def parseArgs (cmdName : String) (flagMap : Std.HashMap String Flag) (acc : Array String) (pflags : ParsedFlags) (cmdArgs : List String) : IO (Array String × ParsedFlags) := do @@ -1541,13 +1541,15 @@ private def parseArgs (cmdName : String) | [] => pure (acc, pflags) -public -def main (args : List String) : IO Unit := do +/-- Dispatch CLI arguments against a command map. This is the shared entry point + that both the default executable and downstream custom executables use. -/ +def runCommandMap (map : Std.HashMap String Command) + (groups : List CommandGroup) (args : List String) : IO Unit := do try do match args with - | ["--help"] => printGlobalHelp + | ["--help"] => printGlobalHelp groups | cmd :: args => - match commandMap[cmd]? with + match map[cmd]? with | none => exitFailure s!"Expected subcommand, got {cmd}." | some cmd => -- Handle per-command help before parsing flags.