1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume.

2. Fix for deterministic loop extraction, and a new regression.
3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.

6 files changed, 61 insertions, 18 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d7fcca7a..148a739d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -590,7 +590,25 @@ namespace Microsoft.Boogie {
                     if (!found) {

                         Block auxNewBlock = new Block();

                         auxNewBlock.Label = ((Block)bl).Label;

-                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds);

+                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);

+                        //add restoration code for such blocks

+                        if (loopHeaderToAssignCmd.ContainsKey(header))

+                        {

+                            AssignCmd assignCmd = loopHeaderToAssignCmd[header];

+                            auxNewBlock.Cmds.Add(assignCmd);

+                        }

+                        List<AssignLhs> lhsg = new List<AssignLhs>();

+                        IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

+                        foreach (IdentifierExpr gl in globalsMods)

+                            lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));

+                        List<Expr> rhsg = new List<Expr>();

+                        foreach (IdentifierExpr gl in globalsMods)

+                            rhsg.Add(new OldExpr(Token.NoToken, gl));

+                        if (lhsg.Count != 0)

+                        {

+                            AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);

+                            auxNewBlock.Cmds.Add(globalAssignCmd);

+                        }

                         blockMap[(Block)bl] = auxNewBlock;

                     }

                 }

@@ -666,21 +684,6 @@ namespace Microsoft.Boogie {
             if (newTargets.Length == 0) {

                 if (!detLoopExtract)

                     newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

-                else {

-                    if (loopHeaderToAssignCmd.ContainsKey(header)) {

-                        AssignCmd assignCmd = loopHeaderToAssignCmd[header];

-                        newBlock.Cmds.Add(assignCmd);

-                    }

-                    List<AssignLhs> lhsg = new List<AssignLhs>();

-                    IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

-                    foreach (IdentifierExpr gl in globalsMods)

-                        lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));

-                    List<Expr> rhsg = new List<Expr>();

-                    foreach (IdentifierExpr gl in globalsMods)

-                        rhsg.Add(new OldExpr(Token.NoToken, gl));

-                    AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);

-                    newBlock.Cmds.Add(globalAssignCmd);

-                }

                 newBlock.TransferCmd = new ReturnCmd(Token.NoToken);

             } else {

               newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5baf8667..c28d8c8a 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1222,7 +1222,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

-              ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)

+              ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

+              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 71f7bbb4..88512025 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -402,7 +402,8 @@ namespace Microsoft.Boogie {
         return new AssertEnsuresCmd(ensCopy);

       }

       else {

-        return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

+        //return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

+        return new AssumeCmd(ens.tok, Expr.True);

       }

     }

 

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index b9083fae..48ca65e9 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4
 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

+Stratified Inlining: Reached recursion bound of 4

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl
new file mode 100644
index 00000000..8388cd57
--- /dev/null
+++ b/Test/extractloops/detLoopExtract1.bpl
@@ -0,0 +1,30 @@
+var g:int;
+
+procedure {:entrypoint} Foo(a:int)
+requires a >= 0;
+modifies g;
+{
+   var b: int;
+   b := 0;
+   g := a;
+  
+LH:
+   goto L_true, L_false;
+
+L_true:
+   assume (b < a); 
+   goto L6;
+
+L6: 
+  b := b + 1;
+  g := 5;
+  goto LH;
+
+L_false:
+   assume (b >= a);	      
+   goto L_end;
+
+L_end:
+   assume (b != a); //modeling assert for stratified inlining
+   return;
+}
diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index 05bfae55..6bd151cb 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -19,4 +19,7 @@ echo -----
 echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops

 %BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl

 echo -----

+echo ----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

+%BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract1.bpl

+echo -----