ValueSubstituter.java

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

import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;

import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.ValueSubstituterIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.RecordValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicExpressionIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;
import edu.udel.cis.vsl.tass.symbolic.IF.tree.TreeExpressionIF;

/**
 * A value substituter.
 * 
 * @author siegel
 * 
 */
public class ValueSubstituter implements ValueSubstituterIF {

	private ValueFactory valueFactory;

	private Map<ValueIF, ValueIF> valueMap;

	private Map<TreeExpressionIF, TreeExpressionIF> treeMap;

	public static ValueSubstituter valueSubstituterFromTreeMap(
			ValueFactory valueFactory,
			Map<TreeExpressionIF, TreeExpressionIF> treeMap) {
		ValueSubstituter result = new ValueSubstituter(valueFactory);

		result.treeMap = treeMap;
		/*
		 * Don't have enough info to make values from trees (symbolic
		 * expressions) because don't know dynamic types of those symbolic
		 * expressions (maybe could figure them out, but why bother?)
		 */
		result.valueMap = null;
		return result;
	}

	/**
	 * This constructor is optimized for a substitution map which permutes
	 * symbolic constants. It takes as input a map from symbolic constants to
	 * symbolic constants.
	 * 
	 * @param valueFactory
	 *            the value factory responsible for the values that will be
	 *            manipulated by the substituter
	 * @param symbolicConstantMap
	 *            a map from symbolic constants to symbolic constants specifying
	 *            the subsitutions to be made
	 * @return a new value subsituter which will modify values by replacing all
	 *         occurrences of symbolic constants which occur as keys in the map
	 *         with their corresponding values in the map
	 */
	public static ValueSubstituter valueSubstituterFromSymbolicConstantMap(
			ValueFactory valueFactory,
			Map<SymbolicConstantIF, SymbolicConstantIF> symbolicConstantMap) {
		SymbolicUniverseIF universe = valueFactory.universe();
		Map<TreeExpressionIF, TreeExpressionIF> treeMap = new LinkedHashMap<TreeExpressionIF, TreeExpressionIF>();

		for (Entry<SymbolicConstantIF, SymbolicConstantIF> entry : symbolicConstantMap
				.entrySet()) {
			SymbolicConstantIF x = entry.getKey();
			SymbolicConstantIF y = entry.getValue();

			treeMap.put(universe.symbolicConstantTreeExpression(x), universe
					.symbolicConstantTreeExpression(y));
		}
		return valueSubstituterFromTreeMap(valueFactory, treeMap);
	}

	public static ValueSubstituter valueSubstituterFromSymbolicConstantValue(
			ValueFactory valueFactory, SymbolicConstantIF symbolicConstant,
			ValueIF newValue) {
		SymbolicUniverseIF universe = valueFactory.universe();
		Map<TreeExpressionIF, TreeExpressionIF> treeMap = new LinkedHashMap<TreeExpressionIF, TreeExpressionIF>();

		TreeExpressionIF symbolicConstantTree = universe
				.symbolicConstantTreeExpression(symbolicConstant);
		TreeExpressionIF newValueTree = universe.tree(valueFactory
				.symExpression(newValue));
		treeMap.put(symbolicConstantTree, newValueTree);
		return valueSubstituterFromTreeMap(valueFactory, treeMap);
	}

	private ValueSubstituter(ValueFactory valueFactory) {
		this.valueFactory = valueFactory;
	}

	public ValueSubstituter(ValueFactory valueFactory,
			Map<ValueIF, ValueIF> valueMap) throws DynamicException {
		this(valueFactory);
		this.valueMap = valueMap;
		this.treeMap = new HashMap<TreeExpressionIF, TreeExpressionIF>();
		for (Entry<ValueIF, ValueIF> entry : valueMap.entrySet()) {

			// problem : these can be undefined values, in which case
			// they do not have a symExpression.

			// could make Undefined Value have a symbolic representation:
			// create special constant UNDEFINED_t17 for each type?.
			// just be careful not to compare for equality.

			// BUT: Undefined value should never occur as a component
			// of any value. Can only occur at top level. So just don't
			// put in tree map.

			ValueIF entryKey = entry.getKey();
			ValueIF entryValue = entry.getValue();

			if (!(entryKey instanceof UndefinedValue)
					&& !(entryValue instanceof UndefinedValue)) {
				TreeExpressionIF key = universe().tree(
						valueFactory.symExpression(symTrue(), entry.getKey()));
				TreeExpressionIF value = universe()
						.tree(
								valueFactory.symExpression(symTrue(), entry
										.getValue()));

				treeMap.put(key, value);
			}
		}
	}

	/**
	 * Returns a new value which is equivalent to the old value, except that
	 * occurrences of certain subexpressions are replaced by possibly different
	 * expressions. The map of old to new subexpressions is specified by the
	 * valueMap.
	 * */
	public ValueIF substitute(ValueIF value) {
		if (valueMap != null) {
			ValueIF result = valueMap.get(value);

			if (result != null)
				return result;
		}
		if (value instanceof SymbolicValue) {
			return substituteTree((SymbolicValue) value);
		} else if (value instanceof ArrayValue) {
			return substituteTree((ArrayValue) value);
		} else if (value instanceof RecordValue) {
			return substituteTree((RecordValue) value);
		} else if (value instanceof ReferenceValue) {
			return substituteTree((ReferenceValue) value);
		}
		return value;
	}

	private ValueIF substituteTree(ArrayValue array) {
		SymbolicExpressionIF origin = array.origin();
		TreeExpressionIF originTree = universe().tree(origin);
		TreeExpressionIF newTree = substituteTree(originTree, treeMap);
		SymbolicExpressionIF newOrigin = universe().canonicalize(newTree);
		MorphicVector<ValueIF> elements = array.elements();
		int size = elements.size();
		MorphicVector<ValueIF> newElements = valueVectorFactory().newVector(
				size);

		for (int i = 0; i < size; i++)
			newElements.set(i, substitute(elements.get(i)));
		return valueFactory.arrayValue(newOrigin, newElements, array
				.valueType());
	}

	private ValueIF substituteTree(RecordValue record) {
		RecordValueTypeIF valueType = record.valueType();
		int numElements = valueType.type().numFields();
		ValueIF[] newElements = new ValueIF[numElements];

		for (int i = 0; i < numElements; i++)
			newElements[i] = substitute(record.element(i));
		return valueFactory.recordValue(newElements, valueType);
	}

	private ValueIF substituteTree(ReferenceValue reference) {
		if (reference.isNull()) {
			return reference;
		} else if (reference instanceof VariableReferenceValue) {
			// offset?
			return reference;
		} else if (reference instanceof ArrayElementReferenceValue) {
			ArrayElementReferenceValue arrayElementReference = (ArrayElementReferenceValue) reference;
			ValueIF parent = substitute(arrayElementReference.parent());

			if (parent instanceof UndefinedValue)
				return valueFactory.undefinedValue(reference.valueType());
			else
				return valueFactory.arrayElementReferenceValue(
						(ReferenceValue) parent, arrayElementReference.index());
		} else if (reference instanceof RecordElementReferenceValue) {
			RecordElementReferenceValue recordElementReference = (RecordElementReferenceValue) reference;
			ValueIF parent = substitute(recordElementReference.parent());

			if (parent instanceof UndefinedValue)
				return valueFactory.undefinedValue(reference.valueType());
			else
				return valueFactory.recordElementReferenceValue(
						(ReferenceValue) parent, recordElementReference
								.fieldIndex());
		} else {
			throw new RuntimeException("Unknown reference type: " + reference);
		}
	}

	private ValueIF substituteTree(SymbolicValue value) {
		TreeExpressionIF oldTree = universe().tree(
				value.getSymbolicExpression());
		TreeExpressionIF newTree = substituteTree(oldTree, treeMap);

		return valueFactory.symbolicValue(universe().canonicalize(newTree),
				value.valueType());
	}

	private TreeExpressionIF substituteTree(TreeExpressionIF original,
			Map<TreeExpressionIF, TreeExpressionIF> treeMap) {
		TreeExpressionIF newTree = treeMap.get(original);

		if (newTree != null)
			return newTree;

		int numArgs = original.numArguments();

		if (numArgs == 0)
			return original;

		TreeExpressionIF[] newArgs = new TreeExpressionIF[numArgs];

		for (int i = 0; i < numArgs; i++)
			newArgs[i] = substituteTree(original.argument(i), treeMap);
		return (TreeExpressionIF) treeUniverse().make(original.kind(),
				original.type(), newArgs);
	}

	private SymbolicUniverseIF universe() {
		return valueFactory.universe();
	}

	private SymbolicUniverseIF treeUniverse() {
		return valueFactory.treeUniverse();
	}

	private SymbolicExpressionIF symTrue() {
		return valueFactory.symTrue();
	}

	private MorphicVectorFactory<ValueIF> valueVectorFactory() {
		return valueFactory.valueVectorFactory();
	}

}