ArrayValue.java

package edu.udel.cis.vsl.tass.dynamic.impl.value;

import edu.udel.cis.vsl.tass.dynamic.IF.type.ArrayValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.dynamic.impl.type.ValueTypeFactory;
import edu.udel.cis.vsl.tass.morph.Morphic;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicExpressionIF;

/**
 * A value of array type. The array value consists of two parts. The first is
 * the "origin": this is a symbolic expression of array type. The second is a
 * (possibly empty) set of assignments to concrete indices, represented as an
 * array of elements. The represented array is what you would get by starting
 * with the origin, and then performing the assignments represented by the
 * concrete sequence of elements.
 * 
 * Neither of these two components can be null. The elements sequence can be
 * emtpy, however.
 * 
 * The symExpression associated to the array can be formed by starting with the
 * origin, then performing a sequence of symbolic assignments (symWrites) based
 * on the non-null elements of the elements array. Note that since the
 * symExpression is a function of the other two components, there is no need to
 * store it. Our approach is to use a field which is initially null, and to
 * compute it only if the user asked for it, then cache the result in the field.
 * The value stored in the field can then be returned the next time the user
 * asks for it, since array values (like all values) are immutable.
 * 
 * A read on index i is performed as follows: if i is symbolic, of if i is
 * concrete and elements[i] is null, get the symExpression and perform a
 * symbolic arrayRead. If i is concrete and elements[i] is non-null, return
 * elements[i].
 * 
 * A write of v to index i is performed as follows: if i is symbolic, get the
 * symExpression and perform a symbolic arrayWrite. If i is concrete, set
 * elements[i] to v (i.e., create a new array object in which the elements
 * sequence is the same as the original except in position i, where it is set to
 * v). Note that this is the same whether or not elements[i] was originally
 * null.
 * 
 * Example: consider a two-dimensional array a declared as followed:
 * 
 * <pre>
 * int[N][M] a;
 * </pre>
 * 
 * Let's say the system assigns the symbolic constant X to a. Call a's initial
 * value A0. A0 looks like this:
 * 
 * <pre>
 * ArrayValue A0: 
 *   type: int[N][M]
 *   origin: X
 *   elements: {}
 *   symExpression: X
 * </pre>
 * 
 * Now let's say the following statement is executed: a[0][0] = 1;. This
 * requires first _reading_ a[0]. Since A0 does not have any element in its
 * concrete list of elements in index 0, this read must be done symbolically.
 * The result of that read will be an array value
 * 
 * <pre>
 * ArrayValue A1:
 *   type: int[M]
 *   origin: X[0]
 *   elements: {}
 *   symExpression: X[0]
 * </pre>
 * 
 * The next step in executing the assignment is to write 1 to index 0 of A1,
 * resulting in this array value:
 * 
 * <pre>
 * ArrayValue A2:
 *   type: int[M]
 *   origin: X[0]
 *   elements: {1}
 *   symExpression: X[0]<0,1>
 * </pre>
 * 
 * The next step is to write A2 back to index 0 of A0, resulting in:
 * 
 * <pre>
 * ArrayValue A3:
 *   type: int[N][M]
 *   origin: X
 *   elements: {A2}
 *   symExpression: X<0, X[0]<0,1>>
 * </pre>
 * 
 * Now let's say the user askes for A3.symExpression(). This is computed by
 * starting with symExpression of the origin, i.e., A0, which is X. We then
 * symbolically execute the assignments in the list of elements. Here this is
 * one element in position 0, namely A2. The indexes are all concrete so there
 * is no problem getting symExpressions for them (in this case, just 0). But we
 * also need symExpressions for the elements. In this case we need
 * A2.symExpression. To compute that, we get the symExpression of the origin,
 * i.e., A1.symExpression = X[0]. Then we execute the assignment symbolically to
 * get A2.symExpression = X[0]<0,1>. Finally we get A3.symExpression = X<0,
 * X[0]<0,1>>.
 * 
 * Suppose there is a second assignment a[2][0] = 2;. Now we are starting with
 * A3 as the value of a. We read A3[2]. Since A3 has no entry in position 2, we
 * perform the operation symbolically:
 * 
 * <pre>
 * ArrayValue A4:
 *   type: int[M]
 *   origin: X[2]
 *   elements: {}
 *   symExpression: X[2]
 * </pre>
 * 
 * We write 2 to A4 in position 0 to produce:
 * 
 * <pre>
 * ArrayValue A5:
 *   type: int[M]
 *   origin: X[2]
 *   elements: { 2 }
 *   symExpression: X[2]<0,2>
 * </pre>
 * 
 * Then we write A5 to A3 in position 1 to yield A6:
 * 
 * <pre>
 * ArrayValue A6:
 *   type: int[M][N]
 *   origin: X
 *   elements: { A2, null, A5 }
 *   symExpression: X<0, X[0]<0,1>><1, X[1]<0,2>>
 * </pre>
 */
public class ArrayValue extends Value implements ArrayValueIF {

	private static int classHashCode = ArrayValue.class.hashCode();

	/**
	 * Original symbolic value (before sequence of concrete assignments). Never
	 * null.
	 */
	private SymbolicExpressionIF origin;

	/**
	 * Values assigned to the array in concrete index positions after origin. If
	 * elements[i] is non-null, then elements[i] was assigned to index i of the
	 * original array. Never null, but may have length 0. Entries may be null
	 * due to gaps in assignment indices. (I.e., this is not a "sparse"
	 * representation.)
	 */
	private MorphicVector<ValueIF> elements;


	/** Constructs new array value. */
	public ArrayValue(SymbolicExpressionIF origin,
			MorphicVector<ValueIF> elements, ArrayValueTypeIF valueType) {
		super(valueType);
		if (origin == null)
			throw new RuntimeException("Null origin");
		if (elements == null)
			throw new RuntimeException("Null elements");
		this.origin = origin;
		this.elements = elements;
	}

	@Override
	protected int computeHashCode() {
		return super.computeHashCode() + classHashCode + origin.hashCode()
				+ elements.hashCode();
	}

	public MorphicVector<ValueIF> elements() {
		return elements;
	}

	public void setElements(MorphicVector<ValueIF> elements) {
		assert !isCommitted();
		this.elements = elements;
	}

	public void setElement(int index, ValueIF value) {
		assert !isCommitted();
		assert !elements.isCommitted();
		elements.setExtend(index, value);
	}

	public SymbolicExpressionIF origin() {
		return origin;
	}

	@Override
	public ArrayValueTypeIF valueType() {
		return (ArrayValueTypeIF) super.valueType();
	}

	@Override
	protected boolean computeEquals(Morphic component) {
		if (component instanceof ArrayValue) {
			ArrayValue that = (ArrayValue) component;

			return origin.equals(that.origin) && elements.equals(that.elements);
		}
		return false;
	}

	@Override
	public String toString() {
		String result = origin.toString();
		int numElements = elements.size();

		for (int i = 0; i < numElements; i++) {
			ValueIF element = elements.get(i);

			if (element != null) {
				result += "<" + i + "," + element + ">";
			}
		}
		return result;
	}

	@Override
	protected void commitChildren() {
		super.commitChildren();
		elements.commit();
	}

	@Override
	protected void canonicalizeChildren(ValueFactory valueFactory,
			ValueTypeFactory typeFactory) {
		super.canonicalizeChildren(valueFactory, typeFactory);
		elements = valueFactory.valueVectorFactory().canonic(elements);
	}
}