Fix issue #297 and #268, make proc inlining visit subblocks (#302)

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
- In fact, 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. This is all under the
assumption that the spec of the inlining procedure exactly represents
the actual behavior of the contents of the procedure.
- 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.

*Issue #, if available:*

*Description of changes:*


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

Author: aqjune-aws

Strata/Languages/Python/BoogiePrelude.lean

@@ -190,14 +190,13 @@ procedure timedelta(days: IntOrNone, hours: IntOrNone) returns (delta : int, may
 spec{
 }
 {
-  havoc delta;
   var days_i : int := 0;
   if (IntOrNone..isIntOrNone_mk_int(days)) {
         days_i := IntOrNone_int_val(days);
   }
   var hours_i : int := 0;
   if (IntOrNone..isIntOrNone_mk_int(hours)) {
-        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);
 };
@@ -244,7 +243,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));
 };
 
@@ -253,7 +251,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));
 };
 
@@ -282,8 +279,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;
 
@@ -295,7 +291,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)));
 };
 
@@ -310,24 +305,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;
 

Strata/Transform/BoogieTransform.lean

@@ -187,32 +187,64 @@ 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
+  all_goals (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
   | [] => return []
   | d :: ds =>
     match d with
     | .proc p md =>
-      return Decl.proc { p with body := ← (runStmts f p.body inputProg ) } md ::
-        (← (runProcedures f ds inputProg))
+      return Decl.proc {
+          p with body := ← (runStmtsRec f p.body inputProg)
+        } md :: (← (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 }

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

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 ∈
@@ -3291,7 +3289,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

Strata/Transform/ProcedureInlining.lean

@@ -191,12 +191,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 inlineCallStmt (st: Statement) (p : Program)
+def inlineCallCmd (excluded_calls:List String := [])
+                  (cmd: Command) (p : Program)
   : BoogieTransformM (List Statement) :=
     open Lambda in do
-    match st with
+    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"
 
@@ -223,12 +226,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 :=
@@ -243,29 +248,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 md =>
-      return Decl.proc { p with body := ← (inlineCallStmts p.body prog ) } md ::
-        (← (inlineCallL ds prog))
-    | _       => return d :: (← (inlineCallL ds prog))
+  runProcedures inlineCallCmd dcls prog
 
 end ProcedureInlining
 end Boogie

StrataMain.lean

@@ -9,9 +9,10 @@ import Strata.DDM.Elab
 import Strata.DDM.Ion
 import Strata.Util.IO
 
-import Strata.Languages.Python.Python
 import Strata.DDM.Integration.Java.Gen
-import StrataTest.Transform.ProcedureInlining
+import Strata.Languages.Python.Python
+import Strata.Transform.BoogieTransform
+import Strata.Transform.ProcedureInlining
 
 def exitFailure {α} (message : String) : IO α := do
   IO.eprintln (message  ++ "\n\nRun strata --help for additional help.")
@@ -202,18 +203,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 javaGenCommand : Command where
   name := "javaGen"

StrataTest/Languages/Boogie/ExprEvalTest.lean

@@ -186,7 +186,7 @@ open Lambda.LTy.Syntax
   (.app () (.app () (.op () (BoogieIdent.unres "Int.Add") .none) eb[#100]) eb[#50]))
 
 
--- This may take a while (~ 1min)
+-- This may take a while (~ 5min)
 #eval (checkFactoryOps false)
 
 open Plausible TestGen