ComparisonPredicate.java

package edu.udel.cis.vsl.tass.predicate.impl;

import java.util.Map;

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.type.ArrayValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.RecordValueTypeIF;
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.ArrayValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.RecordValueIF;
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.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.predicate.IF.TASSPredicateIF;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.ErrorKind;
import edu.udel.cis.vsl.tass.state.States;
import edu.udel.cis.vsl.tass.state.IF.StateFactoryIF;
import edu.udel.cis.vsl.tass.state.IF.StateIF;
import edu.udel.cis.vsl.tass.state.IF.StatefulEnvironmentIF;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

public class ComparisonPredicate implements TASSPredicateIF {

	private ModelSequence modelSequence;
	private int numModels;
	private ModelIF specModel;
	private DynamicFactoryIF dynamicFactory;
	private ModelFactoryIF modelFactory;
	private EvaluatorIF evaluator;
	private StatefulEnvironmentIF environment;
	private Map<VariableIF, ValueIF> expectedValues;
	private TASSPredicateIF deadlockPredicate;
	private StateIF holdState = null;
	String explanation;
	ExecutionStateException exception;
	private LogIF log;
	private NumberFactoryIF numberFactory;
	private IntegerNumberIF ZERO, ONE;

	public ComparisonPredicate(ModelSequence modelSequence,
			DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
			TASSPredicateIF deadlockPredicate, int bufferSize, LogIF log) {
		this.modelSequence = modelSequence;
		this.numModels = modelSequence.numModels();
		this.specModel = modelSequence.modelWithIndex(0);
		this.dynamicFactory = dynamicFactory;
		this.modelFactory = dynamicFactory.modelFactory();
		this.deadlockPredicate = deadlockPredicate;
		this.evaluator = Semantics
				.newEvaluator(dynamicFactory, bufferSize, log);
		this.environment = States.newEnvironment(modelSequence, stateFactory,
				log);
		this.log = log;
		this.numberFactory = dynamicFactory.numberFactory();
		ZERO = numberFactory.zeroInteger();
		ONE = numberFactory.oneInteger();
	}

	public String toString() {
		return "ComparisonPredicate";
	}

	Map<VariableIF, ValueIF> expectedValues() {
		return expectedValues;
	}

	public boolean holdsAt(StateIF state) {
		holdState = null;
		exception = null;
		if (state == null)
			throw new NullPointerException("null state");
		if (deadlockPredicate != null && deadlockPredicate.holdsAt(state)) {
			holdState = state;
			explanation = "Possible deadlock detected in implementation.\n";
			explanation += deadlockPredicate.explanation();
			exception = deadlockPredicate.getException();
			return true;
		}
		environment.setState(state);
		if (!environment.terminated(specModel))
			return false;

		// improvement: get last transition. what model was it in?

		for (int i = 1; i < numModels; i++) {
			ModelIF model = modelSequence.modelWithIndex(i);

			if (environment.terminated(model)
					&& compareOutputs(specModel, model, state))
				return true;
		}
		return false;
	}

	/**
	 * Returns true if error is found, i.e. discrepancy between output
	 * variables.
	 */
	private boolean compareOutputs(ModelIF model1, ModelIF model2, StateIF state) {
		environment.setState(state);
		ValueIF assumption = environment.getAssumption();

		for (SharedVariableIF variable2 : model2.scope().outputVariables()) {
			try {
				SharedVariableIF variable1 = variable2.correspondingVariable();
				ValueIF expectedValue = evaluator.evaluateOverride(environment,
						modelFactory.variableExpression(variable1));
				ValueIF actualValue = evaluator.evaluateOverride(environment,
						modelFactory.variableExpression(variable2));
				ValueIF assertion = dynamicFactory.equals(assumption,
						expectedValue, actualValue);
				ResultType truth = dynamicFactory.valid(assumption, assertion);

				if (truth != ResultType.YES) {
					ReferenceValueIF expectedReference = dynamicFactory
							.referenceValue(dynamicFactory
									.sharedCell(variable1), dynamicFactory
									.referenceValueType(expectedValue
											.valueType()));
					ReferenceValueIF actualReference = dynamicFactory
							.referenceValue(dynamicFactory
									.sharedCell(variable2),
									dynamicFactory
											.referenceValueType(actualValue
													.valueType()));
					Certainty certainty = (truth == ResultType.MAYBE ? Certainty.MAYBE
							: Certainty.PROVEABLE);
					Discrepancy discrepancy = new Discrepancy(dynamicFactory,
							assumption, expectedReference, expectedValue,
							actualReference, actualValue, certainty);

					discrepancy = pinpoint(discrepancy);
					holdState = state;
					explanation = discrepancy.explanation()
							+ "\npath condition:\n  " + state.pathCondition();
					exception = new ExecutionStateException(environment
							.locations(), ErrorKind.FUNCTIONAL_COMPATIBILITY,
							certainty, explanation);
					log.report(exception);
					return true;
				}
			} catch (ExecutionException error) {
				log.report(error);
				environment.setAssumption(dynamicFactory.falseValue());
				return true;
			} catch (DynamicException error) {
				log.report(new ExecutionException(variable2, error,
						Certainty.NONE));
				environment.setAssumption(dynamicFactory.falseValue());
				return true;
			}
		}
		return false;
	}

	/**
	 * If the given discrepancy d is discrepant, this will return a descendant e
	 * of d such that e is discrepant and e has no child which is discrepant.
	 * The point is to report to the user a small piece of an output variable on
	 * which the two programs disagree, as opposed to the whole variable, which
	 * may be large. "Descenedant" is under the transitive, reflexive closure of
	 * the relation d->d' where d' is a sub-component of the stuctured (array,
	 * record, vector) data d. Note e may equal d. If d is not discrepant, this
	 * returns null.
	 */
	private Discrepancy pinpoint(Discrepancy discrepancy)
			throws DynamicException {
		if (!discrepancy.isDiscrepant()) {
			return null;
		} else {
			ValueIF assumption = discrepancy.assumption();
			ValueTypeIF type = discrepancy.expectedValue().valueType();
			ReferenceValueIF expectedReference = discrepancy
					.expectedReference();
			ValueIF expectedValue = discrepancy.expectedValue();
			ReferenceValueIF actualReference = discrepancy.actualReference();
			ValueIF actualValue = discrepancy.actualValue();

			if (type instanceof ArrayValueTypeIF) {
				ValueIF extent = ((ArrayValueTypeIF) type).extent();
				IntegerNumberIF extentNumber = (IntegerNumberIF) dynamicFactory
						.numericValue(assumption, extent);
				if (extentNumber != null) {
					for (IntegerNumberIF i = ZERO; numberFactory.compare(
							extentNumber, i) > 0; i = numberFactory.add(i, ONE)) {
						ValueIF index = dynamicFactory.symbolicValue(i);
						Discrepancy child = new Discrepancy(dynamicFactory,
								assumption,
								dynamicFactory.arrayElementReference(
										(ReferenceValueIF) expectedReference,
										index), dynamicFactory.arrayRead(
										assumption,
										(ArrayValueIF) expectedValue, index),
								dynamicFactory.arrayElementReference(
										(ReferenceValueIF) actualReference,
										index), dynamicFactory.arrayRead(
										assumption, (ArrayValueIF) actualValue,
										index));
						Discrepancy childPinpoint = pinpoint(child);

						if (childPinpoint != null) {
							return childPinpoint;
						}
					}
				}
			} else if (type instanceof VectorValueTypeIF) {
				// TODO
			} else if (type instanceof RecordValueTypeIF) {
				RecordValueTypeIF recordValueType = (RecordValueTypeIF) type;
				RecordTypeIF recordType = recordValueType.type();
				int numFields = recordType.numFields();

				for (int i = 0; i < numFields; i++) {
					Discrepancy child = new Discrepancy(dynamicFactory,
							assumption, dynamicFactory.recordElementReference(
									expectedReference, i), dynamicFactory
									.recordRead(assumption,
											(RecordValueIF) expectedValue, i),
							dynamicFactory.recordElementReference(
									actualReference, i), dynamicFactory
									.recordRead(assumption,
											(RecordValueIF) actualValue, i));
					Discrepancy childPinpoint = pinpoint(child);

					if (childPinpoint != null) {
						return childPinpoint;
					}
				}
			}
			return discrepancy;
		}
	}

	public String explanation() {
		if (holdState == null) {
			return "No violation possible at this state.";
		} else {
			return explanation;
		}
	}

	@Override
	public ExecutionStateException getException() {
		return exception;
	}

}