Fix bug in Duplicator where GotoCmd's LabelTargets and LabelNames

where not updated during duplication to point to duplicated BasicBlocks.

Because the lists weren't being duplicated and resolved to the new basic blocks
a duplicated Implementation pointed into Blocks in the old implementation via
GotoCmds. This is bad and is not the expected behaviour.

Now if VisitImplementation() is called during duplication GotoCmds will be
resolved to point to duplicated Blocks.

2 files changed, 34 insertions, 22 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 69e6b318..964bf024 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -19,7 +19,6 @@ namespace Microsoft.Boogie
         Implementation enclosingImpl;

         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

         public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */

-        public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */

         public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */

         public HashSet<Procedure> yieldingProcs;

         public List<Implementation> impls;

@@ -32,7 +31,6 @@ namespace Microsoft.Boogie
             this.enclosingImpl = null;

             this.procMap = new Dictionary<Procedure, Procedure>();

             this.absyMap = new Dictionary<Absy, Absy>();

-            this.blockMap = new Dictionary<Block, Block>();

             this.implMap = new Dictionary<Implementation, Implementation>();

             this.yieldingProcs = new HashSet<Procedure>();

             this.impls = new List<Implementation>();

@@ -124,7 +122,6 @@ namespace Microsoft.Boogie
         public override Block VisitBlock(Block node)

         {

             Block block = base.VisitBlock(node);

-            blockMap[node] = block;

             absyMap[block] = node;

             return block;

         }

@@ -215,21 +212,6 @@ namespace Microsoft.Boogie
             implMap[impl] = node;

             impl.LocVars.Add(dummyLocalVar);

             impl.Name = impl.Proc.Name;

-            foreach (Block block in impl.Blocks)

-            {

-                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

-                if (gotoCmd == null) continue;

-                List<Block> labelTargets = new List<Block>();

-                List<string> labelNames = new List<string>();

-                foreach (Block x in gotoCmd.labelTargets)

-                {

-                    Block y = (Block)blockMap[x];

-                    labelTargets.Add(y);

-                    labelNames.Add(y.Label);

-                }

-                gotoCmd.labelTargets = labelTargets;

-                gotoCmd.labelNames = labelNames;

-            }

             return impl;

         }

 

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index b275288a..a351e205 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -14,6 +14,9 @@ using System.Linq;
 

 namespace Microsoft.Boogie {

   public class Duplicator : StandardVisitor {

+    // Used to resolve GotoCmd labelTargets by VisitImplementation after duplication

+    private Dictionary<Block,Block> BlockDuplicationMapping = null;

+

     public override Absy Visit(Absy node) {

       //Contract.Requires(node != null);

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

@@ -70,7 +73,12 @@ namespace Microsoft.Boogie {
     public override Block VisitBlock(Block node) {

       //Contract.Requires(node != null);

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

-      return base.VisitBlock((Block)node.Clone());

+      var newBlock = base.VisitBlock((Block) node.Clone());

+

+      if (BlockDuplicationMapping != null)

+        BlockDuplicationMapping[node] = newBlock;

+

+      return newBlock;

     }

     public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {

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

@@ -220,7 +228,10 @@ namespace Microsoft.Boogie {
     public override GotoCmd VisitGotoCmd(GotoCmd node) {

       //Contract.Requires(node != null);

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

-      return base.VisitGotoCmd((GotoCmd)node.Clone());

+      // NOTE: This doesn't duplicate the labelTarget basic blocks

+      // or resolve them to the new blocks

+      // VisitImplementation() and VisitBlock() handle this

+      return base.VisitGotoCmd( (GotoCmd)node.Clone());

     }

     public override Cmd VisitHavocCmd(HavocCmd node) {

       //Contract.Requires(node != null);

@@ -240,7 +251,26 @@ namespace Microsoft.Boogie {
     public override Implementation VisitImplementation(Implementation node) {

       //Contract.Requires(node != null);

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

-      return base.VisitImplementation((Implementation)node.Clone());

+      BlockDuplicationMapping = new Dictionary<Block, Block>();

+

+      var impl = base.VisitImplementation((Implementation)node.Clone());

+

+      // The GotoCmds and blocks have now been duplicated.

+      // Resolve GotoCmd targets to the duplicated blocks

+      foreach (GotoCmd gotoCmd in impl.Blocks.Select( bb => bb.TransferCmd).OfType<GotoCmd>()) {

+        var newLabelTargets = new List<Block>();

+        var newLabelNames = new List<string>();

+        for (int index = 0; index < gotoCmd.labelTargets.Count; ++index) {

+          var newBlock = BlockDuplicationMapping[gotoCmd.labelTargets[index]];

+          newLabelTargets.Add(newBlock);

+          newLabelNames.Add(newBlock.Label);

+        }

+        gotoCmd.labelTargets = newLabelTargets;

+        gotoCmd.labelNames = newLabelNames;

+      }

+      BlockDuplicationMapping.Clear();

+

+      return impl;

     }

     public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

       //Contract.Requires(node != null);

@@ -694,4 +724,4 @@ namespace Microsoft.Boogie {
     }

   }

   #endregion

-}
\ No newline at end of file
+}