Fix bug in Duplicator. Previously when cloning an entire Program

a cloned Implementation.Proc would not be the same Procedure in
the TopLevelDeclarations.

The reason for this is that Procedure would be cloned twice, once
when visiting it from the TopLevelDeclarations and once when visiting
each Implementation of that Procedure's Implementation.Proc.

To fix this a Procedure is only duplicated once by caching it based
on reference value (this assumes the original Program has Procedure
and Implementation.Proc correctly resolved). This also assumes that
Procedure.Equals() and Procedure.GetHashCode() have not been overidden.

1 files changed, 40 insertions, 3 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 9843a2c6..f52ff858 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -14,6 +14,10 @@ using System.Linq;
 

 namespace Microsoft.Boogie {

   public class Duplicator : StandardVisitor {

+    // This is used to ensure that Procedures get duplicated only once

+    // and that Implementation.Proc is resolved to the correct duplicated

+    // Procedure.

+    private Dictionary<Procedure,Procedure> OldToNewProcedureMap = null;

 

     public override Absy Visit(Absy node) {

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

@@ -164,7 +168,24 @@ namespace Microsoft.Boogie {
     public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {

       //Contract.Requires(cce.NonNullElements(declarationList));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));

-      return base.VisitDeclarationList(declarationList);

+

+      // For Implementation.Proc to resolve correctly to duplicated Procedures

+      // we need to visit the procedures first

+      for (int i = 0, n = declarationList.Count; i < n; i++) {

+        if (!( declarationList[i] is Procedure ))

+          continue;

+

+        declarationList[i] = cce.NonNull((Declaration) this.Visit(declarationList[i]));

+      }

+

+      // Now visit everything else

+      for (int i = 0, n = declarationList.Count; i < n; i++) {

+        if (declarationList[i] is Procedure)

+          continue;

+

+        declarationList[i] = cce.NonNull((Declaration) this.Visit(declarationList[i]));

+      }

+      return declarationList;

     }

     public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {

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

@@ -313,12 +334,28 @@ namespace Microsoft.Boogie {
     public override Procedure VisitProcedure(Procedure node) {

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

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

-      return base.VisitProcedure((Procedure)node.Clone());

+      Procedure newProcedure = null;

+      if (OldToNewProcedureMap != null && OldToNewProcedureMap.ContainsKey(node)) {

+        newProcedure = OldToNewProcedureMap[node];

+      } else {

+        newProcedure = base.VisitProcedure((Procedure) node.Clone());

+        if (OldToNewProcedureMap != null)

+          OldToNewProcedureMap[node] = newProcedure;

+      }

+      return newProcedure;

     }

     public override Program VisitProgram(Program node) {

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

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

-      return base.VisitProgram((Program)node.Clone());

+

+      // If cloning an entire program we need to ensure that

+      // Implementation.Proc gets resolved to the right Procedure

+      // (i.e. we don't duplicate Procedure twice).

+      // The map below is used to achieve this.

+      OldToNewProcedureMap = new Dictionary<Procedure, Procedure>();

+      var program = base.VisitProgram((Program)node.Clone());

+      OldToNewProcedureMap = null; // This Visitor could be used for other things later so remove the map.

+      return program;

     }

     public override QKeyValue VisitQKeyValue(QKeyValue node) {

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