From 8ad82b7723d3ede12853b8770a0b89966a77cf5e Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Mon, 5 Jan 2026 19:02:47 -0600 Subject: [PATCH 1/6] Fix issue #297 and #268, make proc inlining visit subblocks This patch fixes - Issue #297: BoogiePrelude.lean's `timedelta` was not updating `hours_i` - Issue #268: procedure inlining was reducing nondeterminism because it was missing havocs to output vars (this depends on how the "correctness" of procedure inlining is defined; if we say that procedure inlining is allowed to reduce nondeterminism, the original implementation was correct of course, but since this makes procedure inlining inherently unsound to use for deductive verification I chose to fix it.) - Procedure inlining wasn't visiting subblocks, which was fixed here. This required small updates in the function signature of `inlineCallCmd` and `callElimCmd` so that they receive Command rather than Statement. For these changes, checks are needed to confirm whether Python applications of interest are not affected. --- Strata/Languages/Python/BoogiePrelude.lean | 25 ++------ Strata/Transform/BoogieTransform.lean | 50 ++++++++++++--- Strata/Transform/CallElim.lean | 15 ++--- Strata/Transform/CallElimCorrect.lean | 10 ++- Strata/Transform/ProcedureInlining.lean | 35 +++++------ StrataTest/Transform/ProcedureInlining.lean | 67 ++++++++++++++++++--- 6 files changed, 135 insertions(+), 67 deletions(-) diff --git a/Strata/Languages/Python/BoogiePrelude.lean b/Strata/Languages/Python/BoogiePrelude.lean index 80715e2b8..d27fe01a1 100644 --- a/Strata/Languages/Python/BoogiePrelude.lean +++ b/Strata/Languages/Python/BoogiePrelude.lean @@ -373,14 +373,13 @@ procedure timedelta(days: IntOrNone, hours: IntOrNone) returns (delta : int, may spec{ } { - havoc delta; var days_i : int := 0; if (IntOrNone_tag(days) == IN_INT_TAG) { days_i := IntOrNone_int_val(days); } var hours_i : int := 0; if (IntOrNone_tag(hours) == IN_INT_TAG) { - days_i := IntOrNone_int_val(hours); + hours_i := IntOrNone_int_val(hours); } assume [assume_timedelta_sign_matches]: (delta == (((days_i * 24) + hours_i) * 3600) * 1000000); }; @@ -427,7 +426,6 @@ spec { ensures (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0)); } { - havoc d; assume [assume_datetime_now]: (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0)); }; @@ -436,7 +434,6 @@ spec { ensures (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0)); } { - havoc d; assume [assume_datetime_now]: (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0)); }; @@ -465,8 +462,7 @@ axiom [Datetime_lt_ax]: type Date; procedure datetime_date(dt: Datetime) returns (d : Datetime, maybe_except: ExceptOrNone) -spec{} -{havoc d;}; +spec{}; function datetime_to_str(dt : Datetime) : string; @@ -478,7 +474,6 @@ spec{ ensures [ensures_str_strp_reverse]: (forall dt : Datetime :: {d == dt} ((time == datetime_to_str(dt)) <==> (d == dt))); } { - havoc d; assume [assume_str_strp_reverse]: (forall dt : Datetime :: {d == dt} ((time == datetime_to_str(dt)) <==> (d == dt))); }; @@ -493,24 +488,16 @@ procedure import(names : ListStr) returns (); procedure print(msg : string, opt : StrOrNone) returns (); procedure json_dumps(msg : DictStrAny, opt_indent : IntOrNone) returns (s: string, maybe_except: ExceptOrNone) -spec{} -{havoc s;} -; +spec{}; procedure json_loads(msg : string) returns (d: DictStrAny, maybe_except: ExceptOrNone) -spec{} -{havoc d;} -; +spec{}; procedure input(msg : string) returns (result: string, maybe_except: ExceptOrNone) -spec{} -{havoc result;} -; +spec{}; procedure random_choice(l : ListStr) returns (result: string, maybe_except: ExceptOrNone) -spec{} -{havoc result;} -; +spec{}; function str_in_list_str(s : string, l: ListStr) : bool; diff --git a/Strata/Transform/BoogieTransform.lean b/Strata/Transform/BoogieTransform.lean index 1ecb9698e..8096c1f1d 100644 --- a/Strata/Transform/BoogieTransform.lean +++ b/Strata/Transform/BoogieTransform.lean @@ -187,20 +187,55 @@ def createOldVarsSubst | ((v', _), v) => (v, createFvar v') - /- Generic runner functions -/ -def runStmts (f : Statement → Program → BoogieTransformM (List Statement)) +-- Only visit top-level statements and run f +def runStmts (f : Command → Program → BoogieTransformM (List Statement)) (ss : List Statement) (inputProg : Program) : BoogieTransformM (List Statement) := do match ss with | [] => return [] | s :: ss => - let s' := (f s inputProg) + let s' := match s with + | .cmd c => f c inputProg + | s => return [s] let ss' := (runStmts f ss inputProg) return (← s') ++ (← ss') -def runProcedures (f : Statement → Program → BoogieTransformM (List Statement)) +-- Recursively visit all blocks and run f +def runStmtsRec (f : Command → Program → BoogieTransformM (List Statement)) + (ss : List Statement) (inputProg : Program) + : BoogieTransformM (List Statement) := do + match ss with + | [] => return [] + | s :: ss' => + let ss'' ← (runStmtsRec f ss' inputProg) + let sres ← (match s with + | .cmd c => do + let res ← f c inputProg + return res + | .block lbl b md => do + let b' ← runStmtsRec f b inputProg + return [.block lbl b' md] + | .ite c thenb elseb md => do + let thenb' ← runStmtsRec f thenb inputProg + let elseb' ← runStmtsRec f elseb inputProg + return [.ite c thenb' elseb' md] + | .loop guard measure invariant body md => do + let body' ← runStmtsRec f body inputProg + return [.loop guard measure invariant body' md] + | .goto _lbl _md => + return [s]) + return (sres ++ ss'') +termination_by sizeOf ss +decreasing_by + · unfold Imperative.instSizeOfBlock; decreasing_tactic + · unfold Imperative.instSizeOfBlock; decreasing_tactic + · unfold Imperative.instSizeOfBlock; decreasing_tactic + · unfold Imperative.instSizeOfBlock; decreasing_tactic + · unfold Imperative.instSizeOfBlock; decreasing_tactic + +def runProcedures (f : Command → Program → BoogieTransformM (List Statement)) (dcls : List Decl) (inputProg : Program) : BoogieTransformM (List Decl) := do match dcls with @@ -208,11 +243,12 @@ def runProcedures (f : Statement → Program → BoogieTransformM (List Statemen | d :: ds => match d with | .proc p => - return Decl.proc { p with body := ← (runStmts f p.body inputProg ) } :: - (← (runProcedures f ds inputProg)) + return Decl.proc { + p with body := ← (runStmtsRec f p.body inputProg) + } :: (← (runProcedures f ds inputProg)) | _ => return d :: (← (runProcedures f ds inputProg)) -def runProgram (f : Statement → Program → BoogieTransformM (List Statement)) +def runProgram (f : Command → Program → BoogieTransformM (List Statement)) (p : Program) : BoogieTransformM Program := do let newDecls ← runProcedures f p.decls p return { decls := newDecls } diff --git a/Strata/Transform/CallElim.lean b/Strata/Transform/CallElim.lean index cb1f4e8f1..96748474f 100644 --- a/Strata/Transform/CallElim.lean +++ b/Strata/Transform/CallElim.lean @@ -14,12 +14,12 @@ namespace CallElim open Boogie.Transform /-- -The main call elimination transformation algorithm on a single statement. +The main call elimination transformation algorithm on a single command. The returned result is a sequence of statements -/ -def callElimStmt (st: Statement) (p : Program) +def callElimCmd (cmd: Command) (p : Program) : BoogieTransformM (List Statement) := do - match st with + match cmd with | .call lhs procName args _ => let some proc := Program.Procedure.find? p procName | throw s!"Procedure {procName} not found in program" @@ -83,18 +83,19 @@ def callElimStmt (st: Statement) (p : Program) (arg_subst ++ ret_subst) return argInit ++ outInit ++ oldInit ++ asserts ++ havocs ++ assumes - | _ => return [ st ] + | _ => return [ .cmd cmd ] +-- Visits top-level statements and do call elimination def callElimStmts (ss: List Statement) (prog : Program) := - runStmts callElimStmt ss prog + runStmts callElimCmd ss prog def callElimL (dcls : List Decl) (prog : Program) := - runProcedures callElimStmt dcls prog + runProcedures callElimCmd dcls prog /-- Call Elimination for an entire program by walking through all procedure bodies -/ def callElim' (p : Program) : BoogieTransformM Program := - runProgram callElimStmt p + runProgram callElimCmd p end CallElim end Boogie diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean index f41d33dbe..710481c25 100644 --- a/Strata/Transform/CallElimCorrect.lean +++ b/Strata/Transform/CallElimCorrect.lean @@ -173,7 +173,7 @@ theorem callElimBlockNoExcept : -- ∧ WF.WFStatementsProp p sts := by intros st p wf - simp [Transform.run, runStmts, CallElim.callElimStmts, CallElim.callElimStmt] + simp [Transform.run, runStmts, CallElim.callElimStmts, CallElim.callElimCmd] cases st with | block l b md => exists [.block l b md] | ite cd tb eb md => exists [.ite cd tb eb md] @@ -188,6 +188,7 @@ theorem callElimBlockNoExcept : next heq => cases heq next st => + simp only [] -- reduce match split <;> simp only [StateT.run, bind, ExceptT.bind, ExceptT.mk, StateT.bind, genArgExprIdentsTrip, ne_eq, liftM, monadLift, MonadLift.monadLift, ExceptT.lift, Functor.map, List.unzip_snd, ite_not, ExceptT.bindCont, ExceptT.map, @@ -272,10 +273,7 @@ theorem callElimBlockNoExcept : unfold BoogieIdent.unres at * split at wf <;> simp_all . -- other case - exfalso - next st Hfalse => - specialize Hfalse lhs procName args md - simp_all + grind theorem postconditions_subst_unwrap : substPost ∈ @@ -3443,7 +3441,7 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] : := by intros Hp Hgv Heval Hwfc Hwf Hwfp Hwfgen Hwfgenst Helim cases st <;> - simp [Transform.runWith, StateT.run, callElimStmts, runStmts, callElimStmt, + simp [Transform.runWith, StateT.run, callElimStmts, runStmts, callElimCmd, pure, ExceptT.pure, ExceptT.mk, StateT.pure, bind, ExceptT.bind, ExceptT.bindCont, StateT.bind, ] at Helim diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean index 28851bb73..e2ba1aaff 100644 --- a/Strata/Transform/ProcedureInlining.lean +++ b/Strata/Transform/ProcedureInlining.lean @@ -179,10 +179,10 @@ This function does not update the specification because inlineCallStmt will not use the specification. This will have to change if Strata also wants to support the reachability query. -/ -def inlineCallStmt (st: Statement) (p : Program) +def inlineCallCmd (cmd: Command) (p : Program) : BoogieTransformM (List Statement) := open Lambda in do - match st with + match cmd with | .call lhs procName args _ => let some proc := Program.Procedure.find? p procName @@ -211,12 +211,14 @@ def inlineCallStmt (st: Statement) (p : Program) -- Create a fresh var statement for each LHS let outputTrips ← genOutExprIdentsTrip sigOutputs sigOutputs.unzip.fst - let outputInit := createInitVars + let outputInits := createInitVars (outputTrips.map (fun ((tmpvar,ty),orgvar) => ((orgvar,ty),tmpvar))) + let outputHavocs := outputTrips.map (fun + (_,orgvar) => Statement.havoc orgvar) -- Create a var statement for each procedure input arguments. -- The input parameter expression is assigned to these new vars. --let inputTrips ← genArgExprIdentsTrip sigInputs args - let inputInit := createInits (sigInputs.zip args) + let inputInits := createInits (sigInputs.zip args) -- Assign the output variables in the signature to the actual output -- variables used in the callee. let outputSetStmts := @@ -231,29 +233,20 @@ def inlineCallStmt (st: Statement) (p : Program) outs_lhs_and_sig let stmts:List (Imperative.Stmt Boogie.Expression Boogie.Command) - := inputInit ++ outputInit ++ proc.body ++ outputSetStmts + := inputInits ++ outputInits ++ outputHavocs ++ proc.body ++ + outputSetStmts return [.block (procName ++ "$inlined") stmts] - | _ => return [st] -def inlineCallStmts (ss: List Statement) (prog : Program) - : BoogieTransformM (List Statement) := do match ss with - | [] => return [] - | s :: ss => - let s' := (inlineCallStmt s prog) - let ss' := (inlineCallStmts ss prog) - return (← s') ++ (← ss') + | _ => return [.cmd cmd] + +def inlineCallStmtsRec (ss: List Statement) (prog : Program) + : BoogieTransformM (List Statement) := + runStmtsRec inlineCallCmd ss prog def inlineCallL (dcls : List Decl) (prog : Program) : BoogieTransformM (List Decl) := - match dcls with - | [] => return [] - | d :: ds => - match d with - | .proc p => - return Decl.proc { p with body := ← (inlineCallStmts p.body prog ) } :: - (← (inlineCallL ds prog)) - | _ => return d :: (← (inlineCallL ds prog)) + runProcedures inlineCallCmd dcls prog end ProcedureInlining end Boogie diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean index 29875c250..73c422761 100644 --- a/StrataTest/Transform/ProcedureInlining.lean +++ b/StrataTest/Transform/ProcedureInlining.lean @@ -205,9 +205,8 @@ end private def alphaEquiv (p1 p2:Boogie.Procedure):Except Format Bool := do if p1.body.length ≠ p2.body.length then - dbg_trace f!"p1: {p1}" - dbg_trace f!"p2: {p2}" - .error (s!"# statements do not match: inlined fn one has {p1.body.length}" + .error (s!"# statements do not match: in {p1.header.name}, " + ++ s!"inlined fn one has {p1.body.length}" ++ s!" whereas the answer has {p2.body.length}") else let newmap:IdMap := IdMap.mk ([], []) [] @@ -224,7 +223,7 @@ def translate (t : Strata.Program) : Boogie.Program := (TransM.run Inhabited.default (translateProgram t)).fst def runInlineCall (p : Boogie.Program) : Boogie.Program := - match (runProgram inlineCallStmt p .emp) with + match (runProgram inlineCallCmd p .emp) with | ⟨.ok res, _⟩ => res | ⟨.error e, _⟩ => panic! e @@ -238,7 +237,9 @@ def checkInlining (prog : Boogie.Program) (progAns : Boogie.Program) match alphaEquiv p p' with | .ok _ => return .true | .error msg => + dbg_trace s!"----- Inlined program ----" dbg_trace s!"{toString prog'}" + dbg_trace s!"----- Answer ----" dbg_trace s!"{toString progAns}" .error msg | _, _ => .error "?") @@ -249,7 +250,6 @@ def Test1 := #strata program Boogie; procedure f(x : bool) returns (y : bool) { - havoc x; y := !x; }; @@ -264,7 +264,6 @@ def Test1Ans := #strata program Boogie; procedure f(x : bool) returns (y : bool) { - havoc x; y := !x; }; @@ -274,7 +273,7 @@ procedure h() returns () { inlined: { var tmp_arg_0 : bool := b_in; var tmp_arg_1 : bool; - havoc tmp_arg_0; + havoc tmp_arg_1; tmp_arg_1 := !tmp_arg_0; b_out := tmp_arg_1; } @@ -322,6 +321,7 @@ procedure h() returns () { inlined: { var f_x : bool := b_in; var f_y : bool; + havoc f_y; if (f_x) { goto f_end; } else { @@ -340,4 +340,57 @@ procedure h() returns () { #eval checkInlining (translate Test2) (translate Test2Ans) +--- Test procedure calls inside subblocks + +def Test3 := +#strata +program Boogie; +procedure f(x : int) returns (y : int) { + y := x; +}; + +procedure g() returns () { + var f_out : int; + if (true) { + call f_out := f(1); + } else { + call f_out := f(2); + } +}; +#end + +def Test3Ans := +#strata +program Boogie; +procedure f(x : int) returns (y : int) { + y := x; +}; + +procedure g() returns () { + var f_out : int; + if (true) { + inlined1: { + var f_x : int := 1; + var f_y : int; + havoc f_y; + f_y := f_x; + f_out := f_y; + } + } else { + inlined1: { + var f_x2 : int := 2; + var f_y2 : int; + havoc f_y2; + f_y2 := f_x2; + f_out := f_y2; + } + } +}; +#end + +/-- info: ok: true -/ +#guard_msgs in +#eval checkInlining (translate Test3) (translate Test3Ans) + + end ProcedureInliningExamples From 23d2bbd07fe6d7601f9667d4fc6cc64390651da6 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Tue, 6 Jan 2026 09:56:53 -0600 Subject: [PATCH 2/6] simplify proof --- Strata/Transform/BoogieTransform.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Strata/Transform/BoogieTransform.lean b/Strata/Transform/BoogieTransform.lean index 8096c1f1d..12ea29942 100644 --- a/Strata/Transform/BoogieTransform.lean +++ b/Strata/Transform/BoogieTransform.lean @@ -229,11 +229,7 @@ def runStmtsRec (f : Command → Program → BoogieTransformM (List Statement)) return (sres ++ ss'') termination_by sizeOf ss decreasing_by - · unfold Imperative.instSizeOfBlock; decreasing_tactic - · unfold Imperative.instSizeOfBlock; decreasing_tactic - · unfold Imperative.instSizeOfBlock; decreasing_tactic - · unfold Imperative.instSizeOfBlock; decreasing_tactic - · unfold Imperative.instSizeOfBlock; decreasing_tactic + all_goals (unfold Imperative.instSizeOfBlock; decreasing_tactic) def runProcedures (f : Command → Program → BoogieTransformM (List Statement)) (dcls : List Decl) (inputProg : Program) From 37f00c5b924ed63555fc8b80edfe683a54a01e3e Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Wed, 7 Jan 2026 14:00:49 -0600 Subject: [PATCH 3/6] Add excluded_calls to the inlining fn, omit --include arg of strata pyAnalyze because it is redundant --- Strata/Transform/ProcedureInlining.lean | 5 ++- StrataMain.lean | 31 +++++++++++-------- .../test_precondition_verification.expected | 24 +++++++------- StrataTest/Languages/Python/run_py_analyze.sh | 3 +- 4 files changed, 36 insertions(+), 27 deletions(-) diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean index e2ba1aaff..18081da05 100644 --- a/Strata/Transform/ProcedureInlining.lean +++ b/Strata/Transform/ProcedureInlining.lean @@ -179,12 +179,15 @@ This function does not update the specification because inlineCallStmt will not use the specification. This will have to change if Strata also wants to support the reachability query. -/ -def inlineCallCmd (cmd: Command) (p : Program) +def inlineCallCmd (excluded_calls:List String := []) + (cmd: Command) (p : Program) : BoogieTransformM (List Statement) := open Lambda in do match cmd with | .call lhs procName args _ => + if procName ∈ excluded_calls then return [.cmd cmd] else + let some proc := Program.Procedure.find? p procName | throw s!"Procedure {procName} not found in program" diff --git a/StrataMain.lean b/StrataMain.lean index 5affa4614..02e160262 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -10,7 +10,8 @@ import Strata.DDM.Ion import Strata.Util.IO import Strata.Languages.Python.Python -import StrataTest.Transform.ProcedureInlining +import Strata.Transform.BoogieTransform +import Strata.Transform.ProcedureInlining def exitFailure {α} (message : String) : IO α := do IO.eprintln (message ++ "\n\nRun strata --help for additional help.") @@ -201,18 +202,22 @@ def pyAnalyzeCommand : Command where let newPgm : Boogie.Program := { decls := preludePgm.decls ++ bpgm.decls } if verbose then IO.print newPgm - let newPgm := runInlineCall newPgm - if verbose then - IO.println "Inlined: " - IO.print newPgm - let solverName : String := "Strata/Languages/Python/z3_parallel.py" - let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true } - (moreFns := Strata.Python.ReFactory)) - let mut s := "" - for vcResult in vcResults do - s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n" - IO.println s + match Boogie.Transform.runProgram + (Boogie.ProcedureInlining.inlineCallCmd (excluded_calls := ["main"])) + newPgm .emp with + | ⟨.error e, _⟩ => panic! e + | ⟨.ok newPgm, _⟩ => + if verbose then + IO.println "Inlined: " + IO.print newPgm + let solverName : String := "Strata/Languages/Python/z3_parallel.py" + let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f)) + (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true } + (moreFns := Strata.Python.ReFactory)) + let mut s := "" + for vcResult in vcResults do + s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n" + IO.println s def commandList : List Command := [ checkCommand, diff --git a/StrataTest/Languages/Python/expected/test_precondition_verification.expected b/StrataTest/Languages/Python/expected/test_precondition_verification.expected index f62d653e1..d30d5492a 100644 --- a/StrataTest/Languages/Python/expected/test_precondition_verification.expected +++ b/StrataTest/Languages/Python/expected/test_precondition_verification.expected @@ -13,27 +13,27 @@ assert_opt_name_none_or_bar: verified ensures_maybe_except_none: verified -test_helper_procedure_assert_name_is_foo_3: verified +test_helper_procedure_assert_name_is_foo_27: verified -test_helper_procedure_assert_opt_name_none_or_str_4: verified +test_helper_procedure_assert_opt_name_none_or_str_28: verified -test_helper_procedure_assert_opt_name_none_or_bar_5: verified +test_helper_procedure_assert_opt_name_none_or_bar_29: verified -test_helper_procedure_assert_name_is_foo_11: verified +test_helper_procedure_assert_name_is_foo_19: verified -test_helper_procedure_assert_opt_name_none_or_str_12: verified +test_helper_procedure_assert_opt_name_none_or_str_20: verified -test_helper_procedure_assert_opt_name_none_or_bar_13: verified +test_helper_procedure_assert_opt_name_none_or_bar_21: verified -test_helper_procedure_assert_name_is_foo_19: failed +test_helper_procedure_assert_name_is_foo_11: failed CEx: -test_helper_procedure_assert_opt_name_none_or_str_20: verified +test_helper_procedure_assert_opt_name_none_or_str_12: verified -test_helper_procedure_assert_opt_name_none_or_bar_21: verified +test_helper_procedure_assert_opt_name_none_or_bar_13: verified -test_helper_procedure_assert_name_is_foo_27: verified +test_helper_procedure_assert_name_is_foo_3: verified -test_helper_procedure_assert_opt_name_none_or_str_28: verified +test_helper_procedure_assert_opt_name_none_or_str_4: verified -test_helper_procedure_assert_opt_name_none_or_bar_29: unknown +test_helper_procedure_assert_opt_name_none_or_bar_5: unknown diff --git a/StrataTest/Languages/Python/run_py_analyze.sh b/StrataTest/Languages/Python/run_py_analyze.sh index d15bac8b6..4167f1b6b 100755 --- a/StrataTest/Languages/Python/run_py_analyze.sh +++ b/StrataTest/Languages/Python/run_py_analyze.sh @@ -9,9 +9,10 @@ for test_file in tests/test_*.py; do expected_file="expected/${base_name}.expected" if [ -f "$expected_file" ]; then + echo "------ $test_file -----" (cd ../../../Tools/Python && python -m strata.gen py_to_strata "../../StrataTest/Languages/Python/$test_file" "../../StrataTest/Languages/Python/$ion_file") - output=$(cd ../../.. && lake exe strata pyAnalyze --include Tools/Python/test_results/dialects "StrataTest/Languages/Python/${ion_file}" 0) + output=$(cd ../../.. && lake exe strata pyAnalyze "StrataTest/Languages/Python/${ion_file}" 0) if ! echo "$output" | diff -q "$expected_file" - > /dev/null; then echo "ERROR: Analysis output for $base_name does not match expected result" From fabe3b197402197f2772cf0f8ec77b7901b56891 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Tue, 13 Jan 2026 16:47:40 -0600 Subject: [PATCH 4/6] space --- .../Python/expected/test_precondition_verification.expected | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/StrataTest/Languages/Python/expected/test_precondition_verification.expected b/StrataTest/Languages/Python/expected/test_precondition_verification.expected index 8f18ba4b9..b7dd6b0b9 100644 --- a/StrataTest/Languages/Python/expected/test_precondition_verification.expected +++ b/StrataTest/Languages/Python/expected/test_precondition_verification.expected @@ -37,4 +37,5 @@ test_helper_procedure_assert_name_is_foo_3: verified test_helper_procedure_assert_opt_name_none_or_str_4: verified test_helper_procedure_assert_opt_name_none_or_bar_5: failed -CEx: \ No newline at end of file +CEx: + From 670fdaa8282ae04a655d6cc25ba5448bc3b45fc6 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Tue, 13 Jan 2026 17:02:47 -0600 Subject: [PATCH 5/6] nospace? --- .../Python/expected/test_precondition_verification.expected | 1 - 1 file changed, 1 deletion(-) diff --git a/StrataTest/Languages/Python/expected/test_precondition_verification.expected b/StrataTest/Languages/Python/expected/test_precondition_verification.expected index b7dd6b0b9..a0bbc7124 100644 --- a/StrataTest/Languages/Python/expected/test_precondition_verification.expected +++ b/StrataTest/Languages/Python/expected/test_precondition_verification.expected @@ -38,4 +38,3 @@ test_helper_procedure_assert_opt_name_none_or_str_4: verified test_helper_procedure_assert_opt_name_none_or_bar_5: failed CEx: - From bdf36a1af4ed650b654b3dc357030737d7e99aa4 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Wed, 14 Jan 2026 12:04:27 -0600 Subject: [PATCH 6/6] Update README --- .../Languages/Python/expected/README.md | 38 +++++++++++-------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/StrataTest/Languages/Python/expected/README.md b/StrataTest/Languages/Python/expected/README.md index e93a56d3d..e98538107 100644 --- a/StrataTest/Languages/Python/expected/README.md +++ b/StrataTest/Languages/Python/expected/README.md @@ -3,6 +3,12 @@ `StrataTest/Languages/Python/expected/test_precondition_verification.expected` looks like this: ``` +datetime_now_ensures_0: verified + +datetime_utcnow_ensures_0: verified + +ensures_str_strp_reverse: verified + assert_name_is_foo: verified assert_opt_name_none_or_str: verified @@ -11,31 +17,31 @@ assert_opt_name_none_or_bar: verified ensures_maybe_except_none: verified -test_helper_procedure_assert_name_is_foo_3: verified +test_helper_procedure_assert_name_is_foo_27: verified -test_helper_procedure_assert_opt_name_none_or_str_4: verified +test_helper_procedure_assert_opt_name_none_or_str_28: verified -test_helper_procedure_assert_opt_name_none_or_bar_5: verified +test_helper_procedure_assert_opt_name_none_or_bar_29: verified -test_helper_procedure_assert_name_is_foo_11: verified +test_helper_procedure_assert_name_is_foo_19: verified -test_helper_procedure_assert_opt_name_none_or_str_12: verified +test_helper_procedure_assert_opt_name_none_or_str_20: verified -test_helper_procedure_assert_opt_name_none_or_bar_13: verified +test_helper_procedure_assert_opt_name_none_or_bar_21: verified -test_helper_procedure_assert_name_is_foo_19: failed +test_helper_procedure_assert_name_is_foo_11: failed CEx: -test_helper_procedure_assert_opt_name_none_or_str_20: verified +test_helper_procedure_assert_opt_name_none_or_str_12: verified -test_helper_procedure_assert_opt_name_none_or_bar_21: verified +test_helper_procedure_assert_opt_name_none_or_bar_13: verified -test_helper_procedure_assert_name_is_foo_27: verified +test_helper_procedure_assert_name_is_foo_3: verified -test_helper_procedure_assert_opt_name_none_or_str_28: verified +test_helper_procedure_assert_opt_name_none_or_str_4: verified -test_helper_procedure_assert_opt_name_none_or_bar_29: failure -CEx: +test_helper_procedure_assert_opt_name_none_or_bar_5: failed +CEx: ``` This can be read as: @@ -71,9 +77,9 @@ Each of the following triples: ``` test_helper_procedure_assert_name_is_foo_3: verified -test_helper_procedure_assert_opt_name_none_or_str_5: verified +test_helper_procedure_assert_opt_name_none_or_str_4: verified -test_helper_procedure_assert_opt_name_none_or_bar_5: verified +test_helper_procedure_assert_opt_name_none_or_bar_5: failed ``` -Comes from checking the assertions in the inlined calls of `test_helper_procedure`. The first two triples succeed, the third has a failure because `"Foo" != "foo"`, and the final has a failure because `"Bar" != "bar"`. \ No newline at end of file +Comes from checking the assertions in the inlined calls of `test_helper_procedure`. The first two triples succeed, the third has a failure because `"Foo" != "foo"`, and the final has a failure because `"Bar" != "bar"`.