DynamicSimplifier.java

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

import java.io.PrintWriter;
import java.util.HashMap;
import java.util.Map;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.DynamicSimplifierIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.MorphicSimplifierCacheIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ArrayValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.FunctionValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.PrimitiveValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.RecordValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ReferenceValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.VectorValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.MessageIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.RecordElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VariableReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VectorElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ArrayValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.CharacterValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.NullReferenceValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.RecordValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.SymbolicValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.UndefinedValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ValueFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.value.VectorValue;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.morph.Morphic;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.number.IF.IntervalIF;
import edu.udel.cis.vsl.tass.simplify.IF.SymbolicSimplifierFactoryIF;
import edu.udel.cis.vsl.tass.simplify.IF.SymbolicSimplifierIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicExpressionIF;
import edu.udel.cis.vsl.tass.util.TASSInternalException;

/**
 * This simplifier work only on canonic values: it takes as input canonic values
 * and returns canonic values. The reason for this restriction is that
 * simplifcation is much more expensive than canonicalization (I think), so it
 * should be a win to cache pre-post simplification pairs in a hash table.
 * 
 * A DyanmicSimplifier uses a cache which stores result of previous
 * simplifications of Morphic objects. Several instances of DynamicSimplifier
 * may use the same cache.
 * 
 * @author siegel
 * 
 */
// TODO: this should really be broken up into two classes and use
// polymorphism. The general cases just does substitution; a subclass
// treats the path condition special and uses a symbolic simplifier.
public class DynamicSimplifier implements DynamicSimplifierIF {

	/** The number of instances of class DynamicSimplifier created */
	private static int instanceCounter = 0;

	private MorphicSimplifierCacheIF cache;

	private ValueIF newAssumption;

	protected ValueIF oldAssumption;

	private DynamicFactoryIF dynamicFactory;

	private PrintWriter out;

	private SymbolicSimplifierIF symbolicSimplifier;

	private ValueFactory valueFactory;

	private boolean verbose;

	private boolean pathConditionIsSpecial;

	/** Unique ID number for this instance of class DynamicSimplifier. */
	private int instanceID;

	/** The number of calls made to one of the simplify methods. */
	private int numberSimplifyCalls = 0;

	public DynamicSimplifier(DynamicFactory dynamicFactory,
			MorphicSimplifierCacheIF cache, boolean pathConditionIsSpecial) {
		RunConfiguration configuration = dynamicFactory.configuration();

		this.out = configuration.out();
		this.verbose = configuration.verbose();
		this.dynamicFactory = dynamicFactory;
		this.cache = cache;
		this.valueFactory = (ValueFactory) dynamicFactory.valueFactory();
		this.pathConditionIsSpecial = pathConditionIsSpecial;
		this.instanceID = instanceCounter++;

		if (verbose) {
			out.println("Dynamic simplifier created with ID: " + instanceID);
			out.println();
		}

		// oldAssumption, newAssumption null by default.
	}

	public DynamicSimplifier(DynamicFactory dynamicFactory, ValueIF assumption,
			MorphicSimplifierCacheIF cache) {
		this(dynamicFactory, cache, true);
		assert assumption.isCanonic();

		SymbolicSimplifierFactoryIF simplifierFactory = dynamicFactory
				.simplifierFactory();
		SymbolicExpressionIF symAssumption = valueFactory
				.symExpression(assumption);

		this.oldAssumption = assumption;

		if (verbose) {
			out.println("Dynamic simplifier " + instanceID + " old assumption:");
			out.println("  " + oldAssumption);
			out.println();
		}

		this.symbolicSimplifier = simplifierFactory.simplifier(symAssumption);
		symAssumption = symbolicSimplifier.newAssumption();
		this.newAssumption = valueFactory.value(symAssumption,
				dynamicFactory.booleanType());

		if (verbose) {
			out.println("Dynamic simplifier " + instanceID + " new assumption:");
			out.println("  " + newAssumption);
			out.println();
			out.flush();
		}
	}

	public void cacheResult(Morphic before, Morphic after) {
		cache.cacheResult(this, before, after);
	}

	public Morphic getCachedResult(Morphic object) {
		return cache.getCachedResult(this, object);
	}

	@Override
	public ValueIF oldAssumption() {
		assert pathConditionIsSpecial;
		return oldAssumption;
	}

	public DynamicFactoryIF dynamicFactory() {
		return dynamicFactory;
	}

	public ValueIF newAssumption() {
		assert pathConditionIsSpecial;
		return newAssumption;
	}

	public MessageIF simplify(MessageIF message) throws DynamicException {
		message = dynamicFactory.canonic(message);

		MessageIF result = (MessageIF) getCachedResult(message);

		if (result != null) {
			return result;
		} else {
			ValueIF oldData = message.data();
			ValueIF newData = simplify(oldData);
			ValueIF oldTag = message.tag();
			ValueIF newTag = simplify(oldTag);

			if (oldData == newData && oldTag == newTag)
				result = message;
			else
				result = dynamicFactory.message(message.source(),
						message.destination(), newTag, newData);
			result = dynamicFactory.canonic(result);
			cacheResult(message, result);
			return result;
		}
	}

	public ValueIF simplify(ValueIF value) throws DynamicException {
		ValueIF result;
		int invocation = numberSimplifyCalls++;

		if (verbose) {
			out.println("Dynamic simplifier " + instanceID + " invocation "
					+ invocation + ":");
			out.println("  " + value);
			out.println();
			out.flush();
		}
		if (value == null) {
			result = null;
		} else {
			value = valueFactory.canonic(value);
			result = (ValueIF) getCachedResult(value);
			if (result == null) {
				ValueTypeIF oldType = value.valueType();
				ValueTypeIF newType = simplify(oldType);

				if (value instanceof SymbolicValue) {
					SymbolicExpressionIF oldExpression = ((SymbolicValue) value)
							.getSymbolicExpression();

					assert oldExpression != null;

					SymbolicExpressionIF newExpression = symbolicSimplifier
							.simplify(oldExpression);

					assert newExpression != null;

					if (newType == oldType && newExpression == oldExpression)
						result = value;
					else
						result = valueFactory.symbolicValue(newExpression,
								newType);
				} else if (value instanceof ArrayValue) {
					ArrayValue arrayValue = (ArrayValue) value;
					SymbolicExpressionIF oldOrigin = arrayValue.origin();
					SymbolicExpressionIF newOrigin = symbolicSimplifier
							.simplify(oldOrigin);
					MorphicVector<ValueIF> oldElements = arrayValue.elements();
					int numElements = oldElements.size();
					MorphicVector<ValueIF> newElements = null;
					boolean change = false;

					for (int i = 0; i < numElements; i++) {
						ValueIF oldElement = oldElements.get(i);
						ValueIF newElement = simplify(oldElement);

						if (!change && newElement != oldElement) {
							newElements = valueFactory.valueVectorFactory()
									.newVector(numElements);
							for (int j = 0; j < i; j++)
								newElements.set(j, oldElements.get(j));
							change = true;
						}
						if (change)
							newElements.set(i, newElement);
					}
					if (newType == oldType && newOrigin == oldOrigin && !change)
						result = value;
					else
						result = valueFactory.arrayValue(newOrigin,
								(change ? newElements : oldElements),
								(ArrayValueTypeIF) newType);
				} else if (value instanceof VectorValue) {
					VectorValue vectorValue = (VectorValue) value;
					VectorValueTypeIF vectorValueType = (VectorValueTypeIF) newType;
					MorphicVector<ValueIF> data = vectorValue.data();
					MorphicVector<ValueIF> newData = dynamicFactory
							.simplifyValueVector(this, data);

					if (newType == oldType && newData == data)
						result = value;
					else
						result = valueFactory.vectorValue(newData,
								vectorValueType);

				} else if (value instanceof RecordValue) {
					RecordValue recordValue = (RecordValue) value;
					boolean change = false;
					RecordValueTypeIF recordValueType = (RecordValueTypeIF) newType;
					RecordTypeIF recordType = recordValueType.type();
					int numFields = recordType.numFields();
					ValueIF[] newElements = new ValueIF[numFields];

					for (int i = 0; i < numFields; i++) {
						ValueIF oldElement = recordValue.element(i);

						newElements[i] = simplify(oldElement);
						if (newElements[i] != oldElement)
							change = true;
					}
					if (newType == oldType && !change)
						result = value;
					else
						result = valueFactory.recordValue(newElements,
								recordValueType);
				} else if (value instanceof ReferenceValueIF) {
					ReferenceValueIF referenceValue = (ReferenceValueIF) value;
					ReferenceValueIF oldParent = referenceValue.parent();
					ReferenceValueIF newParent = null;

					if (oldParent != null)
						newParent = (ReferenceValueIF) simplify(oldParent);
					if (referenceValue instanceof NullReferenceValue) {
						if (newType == oldType)
							result = value;
						else
							result = valueFactory
									.nullReferenceValue((ReferenceValueTypeIF) newType);
					} else if (referenceValue instanceof ArrayElementReferenceValueIF) {
						ArrayElementReferenceValueIF arrayElementReference = (ArrayElementReferenceValueIF) referenceValue;
						ValueIF oldIndex = arrayElementReference.index();
						ValueIF newIndex = simplify(oldIndex);

						if (newParent == oldParent && newIndex == oldIndex)
							result = value;
						else
							result = dynamicFactory.arrayElementReference(
									newParent, newIndex);
					} else if (referenceValue instanceof RecordElementReferenceValueIF) {
						if (newParent == oldParent)
							result = value;
						else
							result = dynamicFactory
									.recordElementReference(
											newParent,
											((RecordElementReferenceValueIF) referenceValue)
													.fieldIndex());
					} else if (referenceValue instanceof VectorElementReferenceValueIF) {
						if (newParent == oldParent)
							result = value;
						else
							result = dynamicFactory.vectorElementReference(
									newParent,
									((VectorElementReferenceValueIF) value)
											.index());
					} else if (referenceValue instanceof VariableReferenceValueIF) {
						if (newType == oldType)
							result = value;
						else
							result = dynamicFactory.referenceValue(
									((VariableReferenceValueIF) referenceValue)
											.variable(),
									(ReferenceValueTypeIF) newType,
									((VariableReferenceValueIF) referenceValue)
											.offset());
					} else {
						throw new RuntimeException(
								"TASS internal error: unknown reference value type: "
										+ referenceValue);
					}
				} else if (value instanceof UndefinedValue) {
					if (newType == oldType)
						result = value;
					else
						result = valueFactory.undefinedValue(newType);
				} else if (value instanceof CharacterValue) {
					// TODO (but already covered by SymbolicValue case)
					throw new TASSInternalException("Not yet implemented");
				} else {
					throw new TASSInternalException("Unknown kind of value: "
							+ value);
				}
			}
			result = dynamicFactory.canonic(result);
			cacheResult(value, result);
		}
		if (verbose) {
			out.println("Result of dynamic simplifier " + instanceID
					+ " invocation " + invocation + ":");
			out.println("  " + result);
			out.println();
			out.flush();
		}
		return result;
	}

	public ValueTypeIF simplify(ValueTypeIF type) throws DynamicException {
		if (type == null)
			return null;
		type = dynamicFactory.canonic(type);

		ValueTypeIF result = (ValueTypeIF) getCachedResult(type);

		if (result != null)
			return result;
		result = simplify(type, new HashMap<ValueTypeIF, ValueTypeIF>());
		result = dynamicFactory.canonic(result);
		cacheResult(type, result);
		return result;
	}

	private ValueTypeIF simplify(ValueTypeIF type,
			Map<ValueTypeIF, ValueTypeIF> map) throws DynamicException {
		if (type == null)
			return null;

		ValueTypeIF result = (ValueTypeIF) getCachedResult(type);

		if (result != null)
			return result;
		result = map.get(type);
		if (result != null)
			return result;
		if (type instanceof PrimitiveValueTypeIF) {
			result = type;
		} else if (type instanceof ArrayValueTypeIF) {
			ArrayValueTypeIF raggedType = (ArrayValueTypeIF) type;
			ValueTypeIF oldBaseType = raggedType.baseType();
			ValueTypeIF newBaseType = simplify(oldBaseType, map);
			ValueIF oldLengths = raggedType.lengthVector();
			ValueIF newLengths = simplify(oldLengths);

			if (newBaseType == oldBaseType && newLengths == oldLengths)
				result = type;
			else
				result = dynamicFactory.arrayValueType(newBaseType, newLengths);
		} else if (type instanceof RecordValueTypeIF) {
			RecordValueTypeIF recordValueType = (RecordValueTypeIF) type;
			RecordTypeIF recordType = recordValueType.type();
			int numFields = recordType.numFields();
			ValueTypeIF[] newFieldTypes = new ValueTypeIF[numFields];
			boolean change = false;

			for (int i = 0; i < numFields; i++) {
				ValueTypeIF oldFieldType = recordValueType.fieldType(i);

				newFieldTypes[i] = simplify(oldFieldType, map);
				if (newFieldTypes[i] != oldFieldType)
					change = true;
			}
			if (!change)
				result = type;
			else
				result = dynamicFactory.recordValueType(recordType,
						newFieldTypes);
			map.put(type, result);
		} else if (type instanceof ReferenceValueTypeIF) {
			ValueTypeIF oldBaseType = ((ReferenceValueTypeIF) type).baseType();
			ValueTypeIF newBaseType;

			result = dynamicFactory.newIncompleteReferenceValueType();
			map.put(type, result);
			newBaseType = simplify(oldBaseType, map);
			dynamicFactory.complete((ReferenceValueTypeIF) result, newBaseType);
		} else if (type instanceof FunctionValueTypeIF) {
			FunctionValueTypeIF functionValueType = (FunctionValueTypeIF) type;
			int numInputs = functionValueType.numArguments();
			ValueTypeIF[] newInputTypes = new ValueTypeIF[numInputs];
			ValueTypeIF oldReturnType = functionValueType.returnType();
			ValueTypeIF newReturnType = simplify(oldReturnType, map);
			boolean change = (oldReturnType != newReturnType);

			for (int i = 0; i < numInputs; i++) {
				ValueTypeIF oldInputType = functionValueType.argumentType(i);
				ValueTypeIF newInputType = simplify(oldInputType, map);

				change = change && newInputType != oldInputType;
				newInputTypes[i] = newInputType;
			}
			if (!change)
				result = type;
			else
				result = dynamicFactory.functionValueType(newInputTypes,
						newReturnType);
			map.put(type, result);
		} else
			throw new RuntimeException(
					"TASS internal error: unknown value type: " + type);
		if (verbose) {
			out.println("Result of simplify applied to value type\n  " + type
					+ "\nis\n  " + result + "\n");
			out.flush();
		}
		return result;
	}

	@Override
	public MorphicSimplifierCacheIF getCache() {
		return cache;
	}

	@Override
	public void setOldAssumption(ValueIF oldAssumption) {
		throw new RuntimeException("Not allowed");
	}

	@Override
	public boolean pathConditionIsSpecial() {
		return pathConditionIsSpecial;
	}

	@Override
	public IntervalIF assumptionAsInterval(SymbolicConstantIF symbolicConstant) {
		return symbolicSimplifier.assumptionAsInterval(symbolicConstant);
	}
}