Rewrite StrataCoreToGoto for multi-procedure programs with contracts

.kiro/steering/structure.md

@@ -180,8 +180,7 @@ Program-to-program translations for simplification and verification. Each has op
 **Main module:** `Strata.lean`
 
 **Executables:**
-- `strata` - Main CLI (includes `verify`, `check`, `toIon`, `print`, etc.)
-- `StrataCoreToGoto` - Strata Core to GOTO translation
+- `strata` - Main CLI (includes `verify`, `coreToGoto`, `check`, `toIon`, `print`, etc.)
 - `StrataToCBMC` - CBMC backend
 
 **Commands:**

README.md

@@ -42,7 +42,7 @@ Unit tests are run with `#guard_msgs` commands. No output means the tests passed
 To build executable files only and omit proof checks that might take a long time, use
 
 ```bash
-lake build strata:exe strata StrataToCBMC StrataCoreToGoto
+lake build strata:exe strata StrataToCBMC
 ```
 
 ## Running Analyses on Existing Strata Programs

StrataMain.lean

@@ -26,7 +26,9 @@ import Strata.Languages.Python.PythonRuntimeLaurelPart
 import Strata.Languages.Python.PythonLaurelCorePrelude
 import Strata.Backends.CBMC.CollectSymbols
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
 
+import Strata.Transform.CallElim
 import Strata.SimpleAPI
 
 open Strata
@@ -486,7 +488,7 @@ private def printPyAnalyzeSummary (vcResults : Array Core.VCResult)
 
 private def deriveBaseName (file : String) : String :=
   let name := System.FilePath.fileName file |>.getD file
-  let suffixes := [".python.st.ion", ".py.ion", ".st.ion", ".st"]
+  let suffixes := [".python.st.ion", ".py.ion", ".core.st", ".st.ion", ".st"]
   match suffixes.find? (name.endsWith ·) with
   | some sfx => (name.dropEnd sfx.length).toString
   | none     => name
@@ -1265,9 +1267,164 @@ def verifyCommand : Command where
       println! f!"Finished with {errors.size} errors."
       IO.Process.exit 1
 
+/-- Sanitize a program name to prevent path traversal in output filenames. -/
+private def sanitizeProgramName (name : String) : Option String :=
+  let s := name.replace "/" "" |>.replace "\\" "" |>.replace ".." ""
+  if s.isEmpty then none else some s
+
+def coreToGotoCommand : Command where
+  name := "coreToGoto"
+  args := [ "file" ]
+  flags := [
+    { name := "output-dir", help := "Directory for output files (default: current directory).",
+      takesArg := .arg "dir" },
+    { name := "program-name", help := "Program name for GOTO output (default: derived from filename).",
+      takesArg := .arg "name" },
+    { name := "no-call-elim", help := "Skip call elimination (keep raw calls for external DFCC)." } ]
+  help := "Translate a Strata Core program (.core.st) to CProver GOTO JSON files."
+  callback := fun v pflags => do
+    let file := v[0]
+    unless file.endsWith ".core.st" do
+      exitCmdFailure "coreToGoto" "expected a .core.st file"
+    let baseName := deriveBaseName file
+    let programName ← match sanitizeProgramName (pflags.getString "program-name" |>.getD baseName) with
+      | some n => pure n
+      | none => exitCmdFailure "coreToGoto" "invalid program name"
+    let dir := System.FilePath.mk (pflags.getString "output-dir" |>.getD ".")
+    IO.FS.createDirAll dir
+    let callElim := !pflags.getBool "no-call-elim"
+
+    let text ← Strata.Util.readInputSource file
+    let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
+    let dctx := Elab.LoadedDialects.builtin |>.addDialect! Core
+    let leanEnv ← Lean.mkEmptyEnvironment 0
+    match Strata.Elab.elabProgram dctx leanEnv inputCtx with
+    | .error errors =>
+      for e in errors do IO.println s!"Error: {← e.toString}"
+      exitUserError "parsing failed"
+    | .ok pgm =>
+      let Env := Lambda.TEnv.default
+      let tcPgm ← match Strata.typeCheck inputCtx pgm with
+        | .ok p => pure p
+        | .error e => exitUserError s!"Type check error: {e.message}"
+      IO.println "[Strata.Core] Type Checking Succeeded!"
+
+      let tcPgm ← if callElim then
+        match Core.Transform.run tcPgm (fun p => do
+              let (_, p) ← Core.CallElim.callElim' p; return p) with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Call elimination error: {e}"
+      else pure tcPgm
+
+      let tcPgm ← match Core.typeCheck .default tcPgm with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Re-type-check error: {e}"
+
+      let tcPgm := inlineFuncDefsInProgram tcPgm
+      let tcPgm := inlineRecFuncDefsInProgram tcPgm
+      let tcPgm := partialEvalDatatypesInProgram tcPgm
+
+      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
+        exitUserError "No procedures or functions found"
+
+      let axioms := tcPgm.decls.filterMap fun d => d.getAxiom?
+      let dtAxioms := generateDatatypeAxioms tcPgm
+      let recAxioms := generateRecFuncAxioms tcPgm (unrollDepth := 0)
+      let axioms := axioms ++ dtAxioms ++ recAxioms
+      let distincts := tcPgm.decls.filterMap fun d => match d with
+        | .distinct name es _ => some (name, es) | _ => none
+      let typeSyms ← match collectExtraSymbols tcPgm with
+        | .ok s => pure s
+        | .error e => exitInternalError s!"Error collecting symbols: {e}"
+      let gotoDtInfo := collectGotoDatatypeInfo tcPgm
+
+      let mut symtabPairs : Array (String × Lean.Json) := #[]
+      let mut gotoFns : Array Lean.Json := #[]
+      let mut errors : Nat := 0
+      let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+        tcPgm.decls.filterMap fun d =>
+          match d with
+          | .var name ty _ _ => some (name, ty)
+          | _ => none
+      let Env := Lambda.TEnv.addInNewestContext
+        (T := ⟨Core.ExpressionMetadata, Unit⟩) Env globalVarEntries
+
+      let mut allLiftedFuncs : List Core.Function := []
+
+      for p in procs do
+        let procName := Core.CoreIdent.toPretty p.header.name
+        match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
+              (varTypes := tcPgm.getVarTy?) with
+        | .error e => IO.println s!"Error: skipping procedure {procName}: {e}"; errors := errors + 1
+        | .ok (ctx, liftedFuncs) =>
+          allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
+          let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
+          let ctx ← lowerAddressOfInCtx ctx
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => 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 => IO.println s!"Error: skipping function {funcName}: {e}"; errors := errors + 1
+        | .ok ctx =>
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      if errors > 0 then
+        exitInternalError s!"{errors} procedure/function translation(s) failed"
+
+      match Lean.toJson typeSyms with
+      | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+      | _ => pure ()
+
+      let mut symtabMap : Std.HashMap String Lean.Json := {}
+      for (k, v) in symtabPairs do
+        symtabMap := symtabMap.insert k v
+
+      for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
+        if !symtabMap.contains k then
+          symtabMap := symtabMap.insert k (Lean.toJson v)
+
+      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj symtabMap.toList)]
+      let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
+
+      let symTabFile := dir / s!"{programName}.symtab.json"
+      let gotoFile := dir / s!"{programName}.goto.json"
+      IO.FS.writeFile symTabFile symtab.pretty
+      IO.FS.writeFile gotoFile goto.pretty
+      IO.println s!"Translated {procs.length} procedures and {funcs.length} functions"
+      IO.println s!"Written {symTabFile} and {gotoFile}"
+
 def commandGroups : List CommandGroup := [
   { name := "Core"
-    commands := [verifyCommand, checkCommand, toIonCommand, printCommand, diffCommand]
+    commands := [verifyCommand, coreToGotoCommand, checkCommand, toIonCommand, printCommand, diffCommand]
     commonFlags := [includeFlag] },
   { name := "Code Generation"
     commands := [javaGenCommand] },

StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st

@@ -0,0 +1,23 @@
+program Core;
+
+var g : int;
+
+procedure helper(x : int) returns (r : int)
+spec {
+  ensures (r > x);
+  modifies g;
+}
+{
+  g := x;
+  r := x + 1;
+};
+
+procedure checker(a : int) returns (result : int)
+spec {
+  requires (a > 0);
+  ensures (result > a);
+}
+{
+  result := a + 1;
+  assert (result > a);
+};

StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh

@@ -0,0 +1,76 @@
+#!/bin/bash
+# Test: strata coreToGoto translates multi-procedure programs with contracts.
+#
+# Exercises:
+# 1. Multi-procedure translation (two procedures)
+# 2. Global variable in symbol table
+# 3. Contract annotations on procedures
+# 4. Assertions in GOTO output
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
+STRATA="$PROJECT_ROOT/.lake/build/bin/strata"
+PYTHON=${PYTHON:-python3}
+
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+
+INPUT="$SCRIPT_DIR/test_multi_proc.core.st"
+
+# Test 1: Multi-procedure translation succeeds
+echo "Test 1: Multi-procedure translation"
+"$STRATA" coreToGoto --output-dir "$WORK" "$INPUT" 2>&1 | grep -q "Translated 2 procedures"
+echo "  OK: translated 2 procedures"
+
+# Test 2: Both procedures in symbol table
+"$PYTHON" -c "
+import json, sys
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'helper' in st, 'helper not in symtab'
+assert 'checker' in st, 'checker not in symtab'
+print('  OK: helper and checker in symbol table')
+"
+
+# Test 3: Global variable in symbol table with correct attributes
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'g' in st, 'global variable g not in symtab'
+assert st['g'].get('isStaticLifetime') is True, 'global variable g does not have static lifetime'
+print('  OK: global variable g with static lifetime in symbol table')
+"
+
+# Test 4: Contract annotations present
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+helper_type = json.dumps(st['helper']['type'])
+assert '#spec_ensures' in helper_type, 'No ensures on helper'
+assert '#spec_assigns' in helper_type, 'No assigns on helper'
+checker_type = json.dumps(st['checker']['type'])
+assert '#spec_requires' in checker_type, 'No requires on checker'
+print('  OK: contract annotations present')
+"
+
+# Test 5: GOTO output has assertions
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.goto.json') as f:
+    data = json.load(f)
+fn_names = [fn['name'] for fn in data['functions']]
+assert 'helper' in fn_names, f'helper not in goto functions: {fn_names}'
+assert 'checker' in fn_names, f'checker not in goto functions: {fn_names}'
+for fn in data['functions']:
+    if fn['name'] == 'checker':
+        types = [i['instructionId'] for i in fn['instructions']]
+        assert 'ASSERT' in types, f'No ASSERT in checker: {types}'
+        print('  OK: checker has ASSERT instruction')
+        break
+"
+
+echo "PASS: all strata coreToGoto tests passed"

StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh

@@ -6,7 +6,7 @@ rm -f *.gb
 
 echo "Writing out JSON files from a Strata Core program SimpleAdd"
 pushd ../../../../
-lake exe StrataCoreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
+lake exe strata coreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
 popd
 
 # The symtab.json now includes CBMC default symbols directly.