fixed a completeness problem in houdini with inlining

4 files changed, 76 insertions, 20 deletions

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 07a8e8a9..71f7bbb4 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -406,6 +406,16 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private CmdSeq RemoveAsserts(CmdSeq cmds) {

+      CmdSeq newCmdSeq = new CmdSeq();

+      for (int i = 0; i < cmds.Length; i++) {

+        Cmd cmd = cmds[i];

+        if (cmd is AssertCmd) continue;

+        newCmdSeq.Add(cmd);

+      }

+      return newCmdSeq;

+    }

+

     // result[0] is the entry block

     protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {

       Contract.Requires(nextBlockLabel != null);

@@ -439,16 +449,6 @@ namespace Microsoft.Boogie {
       for (int i = 0; i < proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

         inCmds.Add(InlinedRequires(impl, callCmd, req));

-        /*

-        if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {

-          Requires reqCopy = (Requires)cce.NonNull(req.Clone());

-          reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

-          AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);

-          Contract.Assert(a != null);

-          a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

-          inCmds.Add(a);

-        }

-        */

       }

 

       VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);

@@ -495,6 +495,9 @@ namespace Microsoft.Boogie {
       Block intBlock;

       foreach (Block block in implBlocks) {

         CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);

+        if (0 <= inlineDepth) {

+          copyCmds = RemoveAsserts(copyCmds);

+        }

         TransferCmd transferCmd = CreateInlinedTransferCmd(cce.NonNull(block.TransferCmd), GetInlinedProcLabel(proc.Name));

         intBlock = new Block(block.tok, GetInlinedProcLabel(proc.Name) + "$" + block.Label, copyCmds, transferCmd);

         inlinedBlocks.Add(intBlock);

@@ -507,15 +510,6 @@ namespace Microsoft.Boogie {
       for (int i = 0; i < proc.Ensures.Length; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

         outCmds.Add(InlinedEnsures(impl, callCmd, ens));

-        /*

-        if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {

-          Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());

-          ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

-          AssertCmd a = new AssertEnsuresCmd(ensCopy);

-          Contract.Assert(a != null);

-          outCmds.Add(a);

-        }

-        */

       }

 

       // assign out params

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 6cd961ac..ce02d173 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -247,6 +247,49 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+  public class InlineRequiresVisitor : StandardVisitor {

+    public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

+      Contract.Requires(cmdSeq != null);

+      Contract.Ensures(Contract.Result<CmdSeq>() != null);

+      CmdSeq newCmdSeq = new CmdSeq();

+      for (int i = 0, n = cmdSeq.Length; i < n; i++) {

+        Cmd cmd = cmdSeq[i];

+        CallCmd callCmd = cmd as CallCmd;

+        if (callCmd != null) {

+          newCmdSeq.AddRange(InlineRequiresForCallCmd(callCmd));

+        }

+        else {

+          newCmdSeq.Add((Cmd)this.Visit(cmd));

+        }

+      }

+      return newCmdSeq;

+    }

+    private CmdSeq InlineRequiresForCallCmd(CallCmd node) {

+      Hashtable substMap = new Hashtable();

+      for (int i = 0; i < node.Proc.InParams.Length; i++) {

+        substMap.Add(node.Proc.InParams[i], node.Ins[i]);

+      }

+      Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);

+      CmdSeq cmds = new CmdSeq();

+      foreach (Requires requires in node.Proc.Requires) {

+        if (requires.Free) continue;

+        Requires requiresCopy = new Requires(false, Substituter.Apply(substitution, requires.Condition));

+        cmds.Add(new AssertRequiresCmd(node, requiresCopy));

+      }

+      cmds.Add(node);

+      return cmds;

+    }

+  }

+

+  public class FreeRequiresVisitor : StandardVisitor {

+    public override Requires VisitRequires(Requires requires) {

+      if (requires.Free)

+        return base.VisitRequires(requires);

+      else 

+        return new Requires(true, requires.Condition);

+    }

+  }

+

   public class Houdini : ObservableHoudini {

     private Program program;

     private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;

@@ -306,6 +349,16 @@ namespace Microsoft.Boogie.Houdini {
         return;

 

       foreach (Implementation impl in callGraph.Nodes) {

+        InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();

+        inlineRequiresVisitor.Visit(impl);

+      }

+

+      foreach (Implementation impl in callGraph.Nodes) {

+        FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();

+        freeRequiresVisitor.Visit(impl);

+      }

+

+      foreach (Implementation impl in callGraph.Nodes) {

         impl.OriginalBlocks = impl.Blocks;

         impl.OriginalLocVars = impl.LocVars;

       }

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index b8e22af3..6053b442 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -146,3 +146,12 @@ b15 = False
 b16 = False

 

 Boogie program verifier finished with 5 verified, 0 errors

+.

+-------------------- test10.bpl --------------------

+Assignment computed by Houdini:

+b1 = True

+b2 = True

+b3 = True

+b4 = True

+

+Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index de2e6099..f0065b0d 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp
   %BGEXE% %* /nologo /noinfer /contractInfer %%f

 )

 

-for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl) do (

+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (

   echo .

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /contractInfer /inlineDepth:1 %%f