[DAG-copy] Implement deep-copying the AST without unfolding the DAG

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph.
On copying wewant to preserve this structure.
The identification of duplicates is non-local since duplicates may appear everywhere in the AST/DAG.

The implementation introduces a new visitor to keep track of duplicate nodes
and makes copying a two-step process:
1. Cloning a node and its internal container types via Object::clone
2. Deep-copying AST child nodes using the visitor

Author: Steffen Märcker

prism/src/parser/ast/ASTElement.java

@@ -35,7 +35,7 @@
 
 // Abstract class for PRISM language AST elements
 
-public abstract class ASTElement
+public abstract class ASTElement implements Cloneable
 {
 	// Type - default to null (unknown)
 	protected Type type = null;
@@ -186,7 +186,39 @@ public String getEndString()
 	/**
 	 * Perform a deep copy.
 	 */
-	public abstract ASTElement deepCopy();
+	public ASTElement deepCopy()
+	{
+		try {
+			return new DeepCopy().copy(this);
+		} catch (PrismLangException e) {
+			throw new Error(e);
+		}
+	}
+
+	/**
+	 * Perform a deep copy of all internal ASTElements using a deep copy visitor.
+	 * This method is usually called after {@code clone()} and must return the receiver.
+	 *
+	 * @param copier the copy visitor
+	 * @returns the receiver with deep-copied subcomponents
+	 * @throws PrismLangException
+	 * @see #clone()
+	 */
+	public abstract ASTElement deepCopy(DeepCopy copier) throws PrismLangException;
+
+	/**
+	 * Perform a shallow copy of the receiver and
+	 * clone all internal container, e.g., lists and vectors, too.
+	 */
+	@Override
+	public ASTElement clone()
+	{
+		try {
+			return (ASTElement) super.clone();
+		} catch (CloneNotSupportedException e) {
+			throw new InternalError("Object#clone is expected to work for Cloneable objects.", e);
+		}
+	}
 
 	// Various methods based on AST traversals (implemented using the visitor
 	// pattern):

prism/src/parser/ast/Command.java

@@ -137,19 +137,20 @@ public String toString()
 		s += "] " + guard + " -> " + updates;
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public Command deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		guard   = copier.copy(guard);
+		updates = copier.copy(updates);
+
+		return this;
+	}
+
+	@Override
+	public Command clone()
 	{
-		Command ret = new Command();
-		ret.setSynch(getSynch());
-		ret.setSynchIndex(getSynchIndex());
-		ret.setGuard(getGuard().deepCopy());
-		ret.setUpdates((Updates)getUpdates().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		return (Command) super.clone();
 	}
 }
 

prism/src/parser/ast/ConstantList.java

@@ -39,7 +39,7 @@
 /**
  * Class to store list of (defined and undefined) constants
  */
-public class ConstantList extends ASTElement
+public class ConstantList extends ASTElement implements Cloneable
 {
 	// Name/expression/type triples to define constants
 	private Vector<String> names = new Vector<String>();
@@ -80,7 +80,7 @@ public void addConstant(ExpressionIdent n, Expression c, Type t)
 		types.addElement(t);
 		nameIdents.addElement(n);
 	}
-	
+
 	public void setConstant(int i, Expression c)
 	{
 		constants.setElementAt(c, i);
@@ -429,21 +429,29 @@ public String toString()
 
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public ConstantList deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		int i, n;
-		ConstantList ret = new ConstantList();
-		n = size();
-		for (i = 0; i < n; i++) {
-			Expression constantNew = (getConstant(i) == null) ? null : getConstant(i).deepCopy();
-			ret.addConstant((ExpressionIdent)getConstantNameIdent(i).deepCopy(), constantNew, getConstantType(i));
-		}
-		ret.setPosition(this);
-		return ret;
+		copier.copyAll(constants);
+		copier.copyAll(nameIdents);
+
+		return this;
+	}
+
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public ConstantList clone()
+	{
+		ConstantList clone = (ConstantList) super.clone();
+
+		clone.constants  = (Vector<Expression>)      constants.clone();
+		clone.nameIdents = (Vector<ExpressionIdent>) nameIdents.clone();
+		clone.names      = (Vector<String>)          names.clone();
+		clone.types      = (Vector<Type>)            types.clone();
+
+		return clone;
 	}
 }
 

prism/src/parser/ast/Declaration.java

@@ -138,17 +138,19 @@ public String toString()
 		return s;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public Declaration deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		declType = copier.copy(declType);
+		start    = copier.copy(start);
+
+		return this;
+	}
+
+	@Override
+	public Declaration clone()
 	{
-		Declaration ret = new Declaration(getName(), (DeclarationType)getDeclType().deepCopy());
-		if (getStart() != null)
-			ret.setStart(getStart().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		return (Declaration) super.clone();
 	}
 }
 

prism/src/parser/ast/DeclarationArray.java

@@ -29,6 +29,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationArray extends DeclarationType
@@ -121,17 +122,19 @@ public String toString()
 		return "array [" + low + ".." + high + "] of " + subtype;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationArray deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		low     = copier.copy(low);
+		high    = copier.copy(high);
+		subtype = copier.copy(subtype);
+
+		return this;
+	}
+
+	@Override
+	public DeclarationArray clone()
 	{
-		Expression lowCopy = (low == null) ? null : low.deepCopy();
-		Expression highCopy = (high == null) ? null : high.deepCopy();
-		DeclarationType subtypeCopy = (DeclarationType) subtype.deepCopy();
-		DeclarationArray ret = new DeclarationArray(lowCopy, highCopy, subtypeCopy);
-		ret.setPosition(this);
-		return ret;
+		return (DeclarationArray) super.clone();
 	}
 }

prism/src/parser/ast/DeclarationBool.java

@@ -29,6 +29,7 @@
 
 import parser.type.TypeBool;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationBool extends DeclarationType
@@ -75,13 +76,15 @@ public String toString()
 		return "bool";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+	@Override
+	public DeclarationBool deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		return this;
+	}
+
+	@Override
+	public DeclarationBool clone()
 	{
-		DeclarationBool ret = new DeclarationBool();
-		ret.setPosition(this);
-		return ret;
+		return (DeclarationBool) super.clone();
 	}
 }

prism/src/parser/ast/DeclarationClock.java

@@ -28,6 +28,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationClock extends DeclarationType
@@ -78,14 +79,15 @@ public String toString()
 		return "clock";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationClock deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		return this;
+	}
+
+	@Override
+	public DeclarationClock clone()
 	{
-		DeclarationClock ret = new DeclarationClock();
-		ret.setPosition(this);
-		return ret;
+		return (DeclarationClock) super.clone();
 	}
 }

prism/src/parser/ast/DeclarationInt.java

@@ -29,6 +29,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationInt extends DeclarationType
@@ -106,16 +107,18 @@ public String toString()
 		return "[" + low + ".." + high + "]";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationInt deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		low = copier.copy(low);
+		high = copier.copy(high);
+
+		return this;
+	}
+
+	@Override
+	public DeclarationInt clone()
 	{
-		Expression lowCopy = (low == null) ? null : low.deepCopy();
-		Expression highCopy = (high == null) ? null : high.deepCopy();
-		DeclarationInt ret = new DeclarationInt(lowCopy, highCopy);
-		ret.setPosition(this);
-		return ret;
+		return (DeclarationInt) super.clone();
 	}
 }

prism/src/parser/ast/DeclarationIntUnbounded.java

@@ -28,6 +28,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationIntUnbounded extends DeclarationType
@@ -78,14 +79,15 @@ public String toString()
 		return "int";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationIntUnbounded deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		return this;
+	}
+
+	@Override
+	public DeclarationIntUnbounded clone()
 	{
-		DeclarationIntUnbounded ret = new DeclarationIntUnbounded();
-		ret.setPosition(this);
-		return ret;
+		return (DeclarationIntUnbounded) super.clone();
 	}
 }

prism/src/parser/ast/DeclarationType.java

@@ -33,4 +33,10 @@ public abstract class DeclarationType extends ASTElement
 	 * Return the default start value for a variable of this type.
 	 */
 	public abstract Expression getDefaultStart();
+
+	@Override
+	public DeclarationType clone()
+	{
+		return (DeclarationType) super.clone();
+	}
 }