Executor.java

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

import java.util.Map;
import java.util.Vector;

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.cell.CellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.HeapCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.LiteralCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ArrayValueTypeIF;
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.value.ArrayElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayValueIF;
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.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.dynamic.IF.value.VariableReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.impl.value.RecordElementReferenceValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.VariableReferenceValue;
import edu.udel.cis.vsl.tass.model.IF.FunctionIF;
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.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.SystemFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF.ExpressionKind;
import edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ObjectLiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.UnaryExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.InvocationLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ModelScopeIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AllocateStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssertionStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssignmentStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssumeStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.InvocationStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.NoopStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReturnStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF.StatementKind;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF.TypeKind;
import edu.udel.cis.vsl.tass.model.IF.variable.LocalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.ProcessVariableIF;
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.NumberIF;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.EnvironmentIF;
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.ExecutionProblem;
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.semantics.IF.ExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorLoaderIF;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.util.Sourceable;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * An executor is used to execute a MiniMP statement. The basic method provided
 * by this interface take an environment and a statement, and modifies the
 * environment according to the semantics of that statement.
 * 
 * Execution of every statement involves moving a process to a new location. For
 * an invocation or return statement, the new location may be in another
 * function, and the stack will change. For every other statement, the new
 * location will be in the same function. Call a move from such a statement a
 * "local move."
 * 
 * When performing a local move from l0 to l1, the scope may need to be
 * adjusted. Let s0 be the scope of l0 and s1 the scope of l1. Find the unique
 * shortest path from s0 to s1 in the scope tree. This will involve some number
 * of moves up the tree followed by some number of moves down. For each up move,
 * you need to remove the scope from the environment. For each down move, you
 * need to add the scope to the environment. Each time a scope is added, its
 * variables need to be initialized to undefined values.
 */
public class Executor implements ExecutorIF {

	private LibraryExecutorLoaderIF loader;

	protected Evaluator evaluator;

	protected DynamicFactoryIF dynamicFactory;

	private LogIF log;

	private int symbolicConstantCounter = 0;

	private ValueIF zero;

	private ValueIF trueValue, falseValue;

	// use array instead....

	private Vector<LibraryExecutorIF> loadedLibraries = new Vector<LibraryExecutorIF>();

	// private Map<String, LibraryExecutorIF> loadedLibraries = new
	// HashMap<String, LibraryExecutorIF>();

	/**
	 * Create a new executor with the given dynamic factory. The bufferSize
	 * argument specifies the upper bound on the total number of buffered
	 * messages.
	 */
	public Executor(LibraryExecutorLoaderIF loader,
			DynamicFactoryIF dynamicFactory, int bufferSize, LogIF log) {
		assert loader != null;
		assert dynamicFactory != null;
		assert log != null;
		this.loader = loader;
		this.dynamicFactory = dynamicFactory;
		this.log = log;
		this.falseValue = dynamicFactory.falseValue();
		this.trueValue = dynamicFactory.trueValue();
		evaluator = (Evaluator) Semantics.newEvaluator(dynamicFactory,
				bufferSize, log);
		zero = dynamicFactory.zero();
	}

	public LogIF log() {
		return log;
	}

	/**
	 * Used to set the new location for a local move, i.e., when the new
	 * location is in the same function as the old location. I.e., this may be
	 * used for all statements other than a function invocation or return
	 * statement. It initializes any new local variables that have just come
	 * into scope (though not formals).
	 */
	private void setTargetLocation(EnvironmentIF environment,
			StatementIF statement) throws ExecutionException {
		LocationIF targetLocation = statement.targetLocation();
		ProcessIF process = statement.process();
		LocalScopeIF newScope = targetLocation.scope();
		int numNewScopes = environment.setLocation(process, targetLocation);
		LocalScopeIF[] ancestors = newScope.localAncestors();
		int numAncestors = ancestors.length;

		for (int i = numAncestors - numNewScopes; i < numAncestors; i++) {
			LocalScopeIF scope = ancestors[i];

			for (LocalVariableIF variable : scope.properLocals())
				initializeVariable(environment, variable, null, false, false);
		}
	}

	/**
	 * Executes the given statement. The environment is read and modified,
	 * according to the semantics of the particular statement.
	 */
	public void execute(EnvironmentIF environment, StatementIF statement) {
		StatementKind kind = statement.kind();

		switch (kind) {
		case ALLOCATE:
			executeAllocate(environment, (AllocateStatementIF) statement);
			break;
		case ASSERTION:
			executeAssertion(environment, (AssertionStatementIF) statement);
			break;
		case ASSIGNMENT:
			executeAssignment(environment, (AssignmentStatementIF) statement);
			break;
		case ASSUME:
			executeAssume(environment, (AssumeStatementIF) statement);
			break;
		case INVOCATION:
			executeInvocation(environment, (InvocationStatementIF) statement);
			return;
		case NOOP:
			executeNoopStatement(environment, (NoopStatementIF) statement);
			break;
		case RECEIVE:
			executeReceiveStatement(environment, (ReceiveStatementIF) statement);
			break;
		case RETURN:
			executeReturnStatement(environment, (ReturnStatementIF) statement);
			return;
		case SEND:
			executeSendStatement(environment, (SendStatementIF) statement);
			break;
		default:
			environment.setAssumption(falseValue);
			throw new RuntimeException(
					"TASS internal error: Unknown statement type: " + statement);
		}
	}

	/**
	 * Executes a noop statement.
	 */
	private void executeNoopStatement(EnvironmentIF environment,
			NoopStatementIF statement) {
		try {
			setTargetLocation(environment, statement);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}
	}

	/**
	 * Executes an allocate (malloc) statement. If anything goes wrong, abort.
	 * 
	 * @param environment
	 * @param statement
	 * @throws ExecutionException
	 */
	private void executeAllocate(EnvironmentIF environment,
			AllocateStatementIF statement) {
		try {
			ValueIF assumption = environment.getAssumption();
			TypeIF elementType = statement.elementType();
			ValueTypeIF elementValueType = evaluator.valueType(environment,
					elementType);
			ValueIF size = evaluator.evaluate(environment, statement.size());
			ValueIF elementSize = dynamicFactory.sizeof(elementValueType);
			ValueIF claim = dynamicFactory.equals(assumption, zero,
					dynamicFactory.modulo(assumption, size, elementSize));
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that argument to malloc is exact multiple of type size:";
					certainty = Certainty.MAYBE;
				} else {
					message = "It is possible for argument to malloc to not be a multiple of the type size:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n  element type       : " + elementType
						+ "\n  element type size  : " + elementSize
						+ "\n  argument to malloc : " + size;
				log.report(new ExecutionException(statement, ErrorKind.MALLOC,
						certainty, message));
				environment.addAssumption(claim);
			}

			ValueIF numElements = dynamicFactory.intDivide(assumption, size,
					elementSize);
			ArrayValueTypeIF arrayValueType = dynamicFactory.arrayValueType(
					elementValueType, numElements);
			ProcessIF process = statement.process();
			int heapSize = environment.heapSize(process);
			HeapCellIF heapVariable = dynamicFactory
					.heapCell(process, heapSize);
			VariableReferenceValueIF reference = dynamicFactory.referenceValue(
					heapVariable,
					dynamicFactory.referenceValueType(arrayValueType));
			ValueIF initialValue = initialValue(environment, reference, false);
			LHSExpressionIF lhs = statement.lhs();
			ArrayElementReferenceValueIF firstElementReference = dynamicFactory
					.arrayElementReference(reference, zero);

			environment.setValue(heapVariable, initialValue);
			assignValue(environment, lhs, firstElementReference);
			setTargetLocation(environment, statement);
			environment.canonicalizeHeap(process, statement);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		} catch (DynamicException error) {
			log.report(new ExecutionException(statement, error, Certainty.NONE));
			environment.setAssumption(falseValue);
		}
	}

	/**
	 * Execute an assertion statement by attempting to prove the assertion holds
	 * in the given environment. If the assertion cannot be proven to hold, an
	 * ExecutionException of type ASSERTION_VIOLATION is thrown. In addition,
	 * recovery is dealt with by setting the path condition to pc && e, where e
	 * is the asserted expression, so that execution may still proceed. Of
	 * course, if pc && e is equivalent to false, the path will be pruned from
	 * the search.
	 * 
	 * @param environment
	 * @param statement
	 */
	private void executeAssertion(EnvironmentIF environment,
			AssertionStatementIF statement) {
		try {
			ExpressionIF assertion = statement.assertion();
			ValueIF claim = evaluator.evaluate(environment, assertion);
			ValueIF assumption = environment.getAssumption();
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that assertion holds.";
					certainty = Certainty.MAYBE;
				} else {
					message = "Assertion can be violated.";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n" + statement.message()
						+ "\n    path condition : " + assumption
						+ "\n         assertion : " + claim;
				log.report(new ExecutionException(statement,
						ErrorKind.ASSERTION_VIOLATION, certainty, message));
			}
			environment.addAssumption(claim);
			setTargetLocation(environment, statement);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		} catch (DynamicException error) {
			log.report(new ExecutionException(statement, error, Certainty.NONE));
			environment.setAssumption(falseValue);
		}
	}

	@Override
	public void assignValue(EnvironmentIF environment,
			ReferenceValueIF reference, ValueIF value, Sourceable element) {
		ValueIF assumption = environment.getAssumption();

		try {
			if (reference instanceof VariableReferenceValueIF) {
				CellIF cell = ((VariableReferenceValueIF) reference).variable();

				if (cell instanceof LiteralCellIF) {
					throw new ExecutionException(element, ErrorKind.OTHER,
							Certainty.PROVEABLE,
							"Attempt to write to literal value: " + value);
				}
				environment.setValue((ModelCellIF) cell, value);
			} else if (reference instanceof ArrayElementReferenceValueIF) {
				ArrayElementReferenceValueIF elementReference = (ArrayElementReferenceValueIF) reference;
				ReferenceValueIF parent = elementReference.parent();
				ArrayValueIF parentValue = (ArrayValueIF) evaluator
						.dereference(environment, parent, element);
				ValueIF index = elementReference.index();
				ValueIF extent = parentValue.valueType().extent();
				ValueIF claim = dynamicFactory.lessThan(assumption, index,
						extent);
				ResultType truth = dynamicFactory.valid(assumption, claim);
				ValueIF newParentValue;

				if (truth != ResultType.YES) {
					String message;
					Certainty certainty;
					ExecutionException error;

					if (truth == ResultType.MAYBE) {
						message = "Cannot prove array index is within bounds:";
						certainty = Certainty.MAYBE;
					} else { /* truth == ResultType.NO */
						message = "It is possible for the array index to be out of bounds:";
						certainty = Certainty.PROVEABLE;
					}
					message += "\n       index value : " + index
							+ "\n      array extent : " + extent
							+ "\n    path condition : " + assumption;
					error = new ExecutionException(element,
							ErrorKind.OUT_OF_BOUNDS, certainty, message);
					log.report(error);
					environment.addAssumption(claim);
				}
				newParentValue = dynamicFactory.arrayWrite(assumption,
						parentValue, index, value);
				assignValue(environment, parent, newParentValue, element);
			} else if (reference instanceof RecordElementReferenceValueIF) {
				RecordElementReferenceValueIF elementReference = (RecordElementReferenceValueIF) reference;
				ReferenceValueIF parent = elementReference.parent();
				RecordValueIF parentValue = (RecordValueIF) evaluator
						.dereference(environment, parent, element);
				int fieldIndex = elementReference.fieldIndex();
				ValueIF newParentValue = dynamicFactory.recordWrite(assumption,
						parentValue, fieldIndex, value);

				// note: parentValue is not necessarily a substructure of
				// the state, as dereference can create new values that are
				// not necessarily in the state. This makes the following
				// optimization unsafe:
				// if (newParentValue != parentValue)
				// possible solution: modify dereference so that it returns
				// value and boolean value saying whether the object returns
				// is "contained in" parent.
				assignValue(environment, parent, newParentValue, element);
			} else {
				log.report(new ExecutionException(element, ErrorKind.INTERNAL,
						Certainty.NONE, "Unknown reference type:\n" + reference));
				environment.setAssumption(falseValue);
			}
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(element, error));
			environment.setAssumption(falseValue);
		} catch (DynamicException error) {
			log.report(new ExecutionException(element, error, Certainty.NONE));
			environment.setAssumption(falseValue);
		}
	}

	private void assignValue(EnvironmentIF environment, LHSExpressionIF lhs,
			ValueIF value) {
		try {
			ReferenceValueIF reference = evaluator.referenceValue(environment,
					lhs);

			assignValue(environment, reference, value, lhs);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}

	}

	private void executeAssignment(EnvironmentIF environment,
			AssignmentStatementIF statement) {
		try {
			assignValue(environment, statement.lhs(),
					evaluator.evaluate(environment, statement.rhs()));
			setTargetLocation(environment, statement);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		}
	}

	private void executeAssume(EnvironmentIF environment,
			AssumeStatementIF statement) {
		try {
			environment.addAssumption(evaluator.evaluate(environment,
					statement.assumption()));
			setTargetLocation(environment, statement);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		}
	}

	private void executeInvocation(EnvironmentIF environment,
			ProcessIF process, FunctionIF callee, ExpressionIF[] arguments) {
		LocationIF location = callee.startLocation();
		int numArgs = arguments.length;
		ValueIF[] argumentValues = new ValueIF[numArgs];

		try {
			/* evaluate actual arguments */
			for (int i = 0; i < arguments.length; i++) {
				ExpressionIF arg = arguments[i];

				if (arg != null) {
					if (arg.type().kind() == TypeKind.ARRAY)
						argumentValues[i] = evaluator.referenceValue(
								environment, (LHSExpressionIF) arg);
					else
						argumentValues[i] = evaluator
								.evaluate(environment, arg);
				}
			}
			environment.push(process, location);
			// note: function is not necessarily in outermost scope,
			// since the initial location could be in an inner scope.
			/* assign values to formals */
			for (int i = 0; i < numArgs; i++) {
				ValueIF argumentValue = argumentValues[i];

				if (argumentValue != null)
					environment.setValue(
							evaluator.cell(environment, callee.formal(i)),
							argumentValue);
			}
			/* initialize local variables */
			for (LocalScopeIF scope : location.scope().localAncestors()) {
				assert scope != null;
				for (LocalVariableIF variable : scope.properLocals())
					initializeVariable(environment, variable, null, false,
							false);
			}
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}
	}

	private void executeInvocation(EnvironmentIF environment,
			InvocationStatementIF statement) {
		FunctionIF callee = statement.callee();

		if (callee instanceof SystemFunctionIF) {
			try {
				executeSystemFunctionCall((SystemFunctionIF) callee,
						environment, statement);
			} catch (ExecutionException e) {
				log.report(e);
				environment.setAssumption(falseValue);
			}
		} else {
			executeInvocation(environment, statement.process(),
					statement.callee(), statement.arguments());
		}
	}

	private void executeReturnStatement(EnvironmentIF environment,
			ReturnStatementIF statement) {
		try {
			ExpressionIF returnExpression = statement.result();
			ValueIF returnValue = null;
			FunctionIF function = statement.function();
			ProcessIF process = function.process();

			if (returnExpression != null) {
				returnValue = evaluator.evaluate(environment,
						statement.result());
			}
			environment.pop(process);
			if (!environment.emptyStack(process)) {
				InvocationLocationIF callingLocation = (InvocationLocationIF) environment
						.location(process);
				InvocationStatementIF callStatement = callingLocation
						.statement();
				LHSExpressionIF lhs = callStatement.lhs();

				if (lhs != null) {
					if (returnValue == null)
						throw new RuntimeException(
								"TASS internal error: No return value: "
										+ statement);
					assignValue(environment, lhs, returnValue);
				}
				environment
						.setLocation(process, callStatement.targetLocation());
			}
			environment.canonicalizeHeap(process, statement);
			if (environment.emptyStack(process)) {
				// main just returned...
				wrapUpLibraries(statement, environment);
				if (process.pid() == 0) {
					ModelIF model = process.model();
					SharedVariableIF mainOut = model.mainOutput();

					if (mainOut != null)
						assignValue(environment, model.modelFactory()
								.variableExpression(mainOut), returnValue);
				}
			}
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		} catch (DynamicException error) {
			log.report(new ExecutionException(statement, error, Certainty.NONE));
			environment.setAssumption(falseValue);
		}
	}

	private void executeSendStatement(EnvironmentIF environment,
			SendStatementIF statement) {
		try {
			ModelIF model = statement.model();
			ProcessIF sourceProcess = statement.process();
			ProcessIF destinationProcess;
			ValueIF destinationValue = evaluator.evaluate(environment,
					statement.destination());
			ValueIF tagValue = evaluator.evaluate(environment, statement.tag());
			ValueIF assumption = environment.getAssumption();
			MessageIF message;
			IntegerNumberIF pidNumber = (IntegerNumberIF) dynamicFactory
					.numericValue(assumption, destinationValue);

			if (pidNumber != null) {
				int pid = pidNumber.intValue();

				if (pid < 0 || pid >= model.numProcs()) {
					log.report(new ExecutionException(statement,
							ErrorKind.INVALID_PID, Certainty.PROVEABLE,
							"Invalid destination value in send (" + pid
									+ ") for model " + model.name() + " with "
									+ model.numProcs() + " processes"));
					environment.setAssumption(falseValue);
					return;
				}
				destinationProcess = model.process(pid);
			} else {
				log.report(new ExecutionException(statement,
						ErrorKind.INTERNAL, Certainty.MAYBE,
						"Destination process cannot be resolved to concrete value: "
								+ destinationValue));
				environment.setAssumption(falseValue);
				return;
			}
			message = dynamicFactory.message(sourceProcess, destinationProcess,
					tagValue,
					evaluator.evaluate(environment, statement.buffer()));
			environment.enqueue(message);
			setTargetLocation(environment, statement);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}
	}

	/*
	 * No any source allowed, so statement is deterministic.
	 */
	private void executeReceiveStatement(EnvironmentIF environment,
			ReceiveStatementIF statement) {
		try {
			ModelIF model = statement.model();
			ProcessIF destinationProcess = statement.process();
			ExpressionIF sourceExpression = statement.source();
			ExpressionIF tagExpression = statement.tag();
			LHSExpressionIF buffer = statement.buffer();
			LHSExpressionIF sizeExpression = statement.size();
			ValueIF assumption = environment.getAssumption();
			ReferenceValueIF reference = evaluator.referenceValue(environment,
					buffer);
			ProcessIF sourceProcess;
			LHSExpressionIF tagLHS = null;
			ValueIF tagValue, sourceValue;
			MessageIF message;
			ValueIF data;
			IntegerNumberIF pidNumber;

			if (sourceExpression.kind() == ExpressionKind.ANY) {
				log.report(new ExecutionException(sourceExpression,
						ErrorKind.COMMUNICATION, Certainty.NONE,
						"Source expression in receive should not use \"any\""));
				environment.setAssumption(falseValue);
				return;
			}
			sourceValue = evaluator.evaluate(environment, sourceExpression);
			pidNumber = (IntegerNumberIF) dynamicFactory.numericValue(
					assumption, sourceValue);
			if (pidNumber != null) {
				int pid = pidNumber.intValue();

				if (pid < 0 || pid >= model.numProcs()) {
					log.report(new ExecutionException(statement,
							ErrorKind.INVALID_PID, Certainty.PROVEABLE,
							"Illegal source value in receive (" + pid
									+ ") for model " + model.name() + " with "
									+ model.numProcs() + " processes"));
					environment.setAssumption(falseValue);
					return;
				}
				sourceProcess = model.process(pid);
			} else {
				log.report(new ExecutionException(statement,
						ErrorKind.INTERNAL, Certainty.MAYBE,
						"Source process cannot be resolved to concrete value: "
								+ sourceValue));
				environment.setAssumption(falseValue);
				return;
			}
			if (tagExpression.kind() == ExpressionKind.ANY) {
				tagValue = null;
				tagLHS = (LHSExpressionIF) ((UnaryExpressionIF) tagExpression)
						.expression();
			} else {
				tagValue = evaluator.evaluate(environment, tagExpression);
			}
			message = environment.dequeue(sourceProcess, destinationProcess,
					tagValue);
			if (message == null)
				throw new RuntimeException(
						"TASS internal error: no message to receive: "
								+ statement);
			if (tagLHS != null)
				assignValue(environment, tagLHS, message.tag());
			data = message.data();
			writeToRecvBuffer(environment, reference, data, buffer);
			if (sizeExpression != null)
				assignValue(environment, sizeExpression,
						dynamicFactory.sizeof(data.valueType()));
			setTargetLocation(environment, statement);
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		} catch (ExecutionProblem error) {
			log.report(new ExecutionException(statement, error));
			environment.setAssumption(falseValue);
		} catch (DynamicException error) {
			log.report(new ExecutionException(statement, error, Certainty.NONE));
			environment.setAssumption(falseValue);
		}
	}

	/**
	 * This method is used to execute a system-level library function.
	 * 
	 * @param name
	 *            the name of the library
	 * @param environment
	 *            the environment to be read and modified by executing the
	 *            library function
	 * @param statement
	 *            the invocation statement that calls the library function
	 * 
	 * */

	private void executeSystemFunctionCall(SystemFunctionIF callee,
			EnvironmentIF environment, InvocationStatementIF statement)
			throws ExecutionException {
		int libraryId = callee.libraryId();
		LibraryExecutorIF libraryExecutor;

		if (libraryId >= loadedLibraries.size())
			loadedLibraries.setSize(libraryId + 1);
		libraryExecutor = loadedLibraries.get(libraryId);
		if (libraryExecutor == null) {
			String libraryName = callee.libraryName();

			libraryExecutor = loader.getLibraryExecutor("lib" + libraryName,
					this);
			if (libraryExecutor == null)
				throw new ExecutionException(statement, ErrorKind.LIBRARY,
						Certainty.NONE, "Unsupported library: " + libraryName);
			loadedLibraries.set(libraryId, libraryExecutor);
		}
		libraryExecutor.execute(environment, statement);
		setTargetLocation(environment, statement);
	}

	/**
	 * Called when a process terminates, to wrap up any library-related tasks.
	 * Eventually a general mechanism should be put in place to handle this with
	 * a designated wrap up function in each library.
	 */
	private void wrapUpLibraries(ReturnStatementIF statement,
			EnvironmentIF environment) throws DynamicException {
		ProcessIF process = statement.process();
		ProcessVariableIF mpiStateVariable = process.scope().variableWithName(
				"MPIX_State");

		if (mpiStateVariable != null) {
			ModelCellIF cell = dynamicFactory.processCell(mpiStateVariable);
			ValueIF value = environment.valueOf(cell);
			NumberIF number = dynamicFactory.numericValue(trueValue, value);

			if (number.isOne()) {
				log.report(new ExecutionException(statement,
						ErrorKind.COMMUNICATION, Certainty.PROVEABLE, process
								+ " terminated without calling MPI_Finalize."));
			}
			// TODO: check for un-received messages, etc.
		}
	}

	/**************************** INITIALIZATION **********************************/

	/**
	 * Finds the maximum integer m such that a symbolic constant named Xm occurs
	 * as a value in the map, and return the integer m+1. If there is no
	 * symbolic constant with name of the form Xm occurring as a value in the
	 * map, or if the map is null, returns 0. It is then safe to create new
	 * symbolic constants of the name Xi, where i is any integer greater than or
	 * equal to the returned value.
	 */
	private void computeInitialIndex(Map<VariableIF, ValueIF> inputs) {
		symbolicConstantCounter = 0;
		if (inputs != null) {
			for (ValueIF value : inputs.values()) {
				String name = value.toString();

				if (name.startsWith("X")) {
					String suffix = name.substring(1);
					int xid;

					try {
						xid = new Integer(suffix);
					} catch (NumberFormatException e) {
						xid = -1;
					}
					if (xid >= symbolicConstantCounter)
						symbolicConstantCounter = xid + 1;
				}
			}
		}
	}

	/**
	 * There is a unique symbolic constant associated to each variable and each
	 * field of a variable of record type. This symbolic constant is used to
	 * represent the initial undefined value of that variable. It is used to
	 * initialize that variable or field as soon as control enters the
	 * variable's scope. This method returns the symbolic constant, given a
	 * reference to the variable or field.
	 * 
	 * Note: perhaps cache this symbolic constant somewhere? note safety issue:
	 * when returning, should check no more references to local symbolic
	 * constant exist in state.
	 */
	// TODO: illegal use of implementation classes VariableReferenceValue,
	// RecordElementReferenceValue
	private ValueIF theSymbolicConstant(ReferenceValueIF reference) {
		ValueTypeIF dynamicType = reference.valueType().baseType();

		if (reference instanceof VariableReferenceValueIF) {
			VariableReferenceValue variableReference = (VariableReferenceValue) reference;
			String fullName = variableReference.fullName();

			return dynamicFactory.symbolicConstant(fullName, dynamicType);
		} else if (reference instanceof RecordElementReferenceValueIF) {
			RecordElementReferenceValue recordElementReference = (RecordElementReferenceValue) reference;
			String fullName = recordElementReference.fullName();

			return dynamicFactory.symbolicConstant(fullName, dynamicType);
		}
		throw new IllegalArgumentException(
				"Reference must be to variable or record element:\n"
						+ reference);
	}

	/**
	 * Computes the initial "undefined" value for the memory location specified
	 * by a given reference. This is used to initialize variables that are not
	 * given any initialization expression. For scalar values (i.e., not record
	 * or array), there is simply a special "undefined value" of the relevant
	 * type that is returned. For arrays, a designated symbolic constant of the
	 * correct array type is used. For records, the function is called
	 * recursively on each record element.
	 * 
	 * Note that the reference does not have to be to a variable: it can be to
	 * the element of a record or to a variable. Any other kind of reference
	 * will lead to an exception being thrown.
	 */
	private ValueIF initialValue(EnvironmentIF environment,
			ReferenceValueIF reference, boolean isInput) {
		ValueIF assumption = environment.getAssumption();
		ReferenceValueTypeIF referenceValueType = reference.valueType();
		ValueTypeIF dynamicType = referenceValueType.baseType();
		ValueIF result = null;

		if (dynamicType instanceof PrimitiveValueTypeIF
				|| dynamicType instanceof ReferenceValueTypeIF) {
			if (isInput) {
				result = dynamicFactory.symbolicConstant("X"
						+ symbolicConstantCounter, dynamicType);
				symbolicConstantCounter++;
			} else {
				result = dynamicFactory.undefinedValue(dynamicType);
			}
		} else if (dynamicType instanceof RecordValueTypeIF) {
			RecordValueTypeIF recordValueType = (RecordValueTypeIF) dynamicType;
			RecordTypeIF recordType = recordValueType.type();
			int numFields = recordType.numFields();
			ValueIF[] fieldValues = new ValueIF[numFields];

			for (int i = 0; i < numFields; i++) {
				ReferenceValueIF fieldReference = dynamicFactory
						.recordElementReference(reference, i);

				fieldValues[i] = initialValue(environment, fieldReference,
						isInput);
			}
			result = dynamicFactory.recordValue(assumption, recordValueType,
					fieldValues);
		} else if (dynamicType instanceof ArrayValueTypeIF) {
			// an array object: corresponds to variable or to record element
			// type had better contain dimensions, else exception is thrown
			if (isInput) {
				result = dynamicFactory.symbolicConstant("X"
						+ symbolicConstantCounter, dynamicType);
				symbolicConstantCounter++;
			} else {
				result = theSymbolicConstant(reference);
			}
		} else {
			throw new RuntimeException(
					"Unknown dynamic type resulting from reference:\n"
							+ dynamicType + "\n" + reference);
		}
		return result;
	}

	/**
	 * Initializes a global, or proper local variable. Should not be called on a
	 * formal parameter variable. Uses input map for initial value if variable
	 * is found in the map, else creates appropriate symbolic constants. Arrays
	 * are also allocated as necessary. Assumptions are also updated based on
	 * given arguments and the assumption expression associated to the variable.
	 */
	private void initializeVariable(EnvironmentIF environment,
			VariableIF variable, Map<VariableIF, ValueIF> inputs,
			boolean useKeyAssumptions, boolean useNonKeyAssumptions)
			throws ExecutionException {
		try {
			ValueIF initialValue = null;
			ModelCellIF cell = evaluator.cell(environment, variable);
			boolean isInput = variable instanceof SharedVariableIF
					&& ((SharedVariableIF) variable).isInput();
			boolean isKey;

			if (inputs != null) {
				initialValue = inputs.get(variable);
			}
			isKey = (initialValue != null);
			if (initialValue == null) {
				ExpressionIF expression = variable.initializationExpression();

				if (expression != null) {
					if (expression instanceof ObjectLiteralExpressionIF) {
						ValueTypeIF partialValueType = evaluator
								.variableValueType(environment, variable);

						initialValue = evaluator.evaluateObjectLiteral(
								environment,
								(ObjectLiteralExpressionIF) expression,
								partialValueType);
					} else {
						initialValue = evaluator.evaluate(environment,
								expression);
					}
				}
			}
			if (initialValue == null) {
				ValueTypeIF dynamicType = evaluator.variableValueType(
						environment, variable);
				ReferenceValueTypeIF referenceValueType = dynamicFactory
						.referenceValueType(dynamicType);
				ReferenceValueIF reference = dynamicFactory.referenceValue(
						cell, referenceValueType);

				initialValue = initialValue(environment, reference, isInput);
			}
			environment.setValue(cell, initialValue);
			// would also like to accumulate initial conditions for variables
			// that occur in map and return these, regardless of the
			// use[Non]KeyAssumptions flags
			if (isInput
					&& ((useNonKeyAssumptions && !isKey) || (useKeyAssumptions && isKey))) {
				ExpressionIF assumption = ((SharedVariableIF) variable)
						.assumption();

				if (assumption != null) {
					try {
						environment.addAssumption(evaluator.evaluate(
								environment, assumption));
					} catch (ExecutionProblem error) {
						throw new ExecutionException(assumption, error);
					}
				}
			}
		} catch (ExecutionException error) {
			environment.setAssumption(falseValue);
			throw error;
		}
	}

	/**
	 * Puts the environment into the initial state. The initial path condition
	 * is given. An optional map inputs may also be given. (This argument may be
	 * null.) It specifies the initial value for any number of input variables
	 * in the model. For any variable occuring as a key in this map, the value
	 * specified in the map will be used, instead of creating a new value. Also,
	 * any predicate associated to such a variable will be ignored.
	 * 
	 * Input variables come with associated assumption expressions. In some
	 * cases you may want to use these assumptions, i.e., evaluate them and add
	 * them to the path condition. In other situations, you may want to just
	 * ignore these assumptions. If useKeyAssumptions is true, then the
	 * assumptions for "key variables" (input variables which occur as keys in
	 * the inputs map) will be used, otherwise they will be ignored. If
	 * useNonKeyAssumptions is true, then the assumptions for "nonkey variables"
	 * (input variables which do not occur as keys in the inputs maps) will be
	 * used, otherwise they will be ignored.
	 */
	public void initialize(EnvironmentIF environment, ModelIF model,
			ValueIF initialPathCondition, Map<VariableIF, ValueIF> inputs,
			boolean useKeyAssumptions, boolean useNonKeyAssumptions) {
		int numProcs = model.numProcs();
		ModelScopeIF sharedScope = model.scope();

		try {
			environment.setAssumption(initialPathCondition);
			computeInitialIndex(inputs);
			for (SharedVariableIF variable : sharedScope.inputVariables())
				initializeVariable(environment, variable, inputs,
						useKeyAssumptions, useNonKeyAssumptions);
			for (SharedVariableIF variable : sharedScope.outputVariables())
				initializeVariable(environment, variable, null, false, false);
			for (SharedVariableIF variable : sharedScope
					.properSharedVariables())
				initializeVariable(environment, variable, null, false, false);
			for (int i = 0; i < numProcs; i++) {
				for (VariableIF variable : model.process(i).scope().variables())
					initializeVariable(environment, variable, null, false,
							false);
			}

			ProcessIF proc0 = model.process(0);
			FunctionIF main0 = proc0.mainFunction();
			int numFormals0 = main0.numFormals();
			int startProc = 0;

			if (numFormals0 > 0) {
				// arg0 is: int argc. arg1 is: char *argv[].
				SharedVariableIF argc = model.argcInput(); // argc
				ProcessVariableIF argv = model.argvGlobal(); // argv on proc 0
				ModelFactoryIF factory = dynamicFactory.modelFactory();
				ExpressionIF argcExpression = factory.variableExpression(argc);
				ExpressionIF argvExpression = factory.variableExpression(argv);
				ExpressionIF[] actuals = new ExpressionIF[] { argcExpression,
						argvExpression };

				executeInvocation(environment, proc0, main0, actuals);
				startProc = 1;
			}

			for (int i = startProc; i < numProcs; i++) {
				ProcessIF process = model.process(i);
				FunctionIF mainFunction = process.mainFunction();
				int numFormals = mainFunction.numFormals();
				ExpressionIF[] actuals = new ExpressionIF[numFormals];

				// for (int i=0; i< numFormals; i++) {
				// actuals[i] = initialValue(environment, )
				// }

				// for now, use null for values of args to main on procs
				// of positive rank...
				executeInvocation(environment, process, mainFunction, actuals);
			}
		} catch (ExecutionException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}
	}

	public void initialize(EnvironmentIF environment, ModelIF model) {
		initialize(environment, model, dynamicFactory.trueValue(), null, true,
				true);
	}

	/*********************************** Compatibility ************************************/

	/**
	 * Asserts that the two types are strictly compatible. Adjusts path
	 * condition if possible to make them so (after logging error). If they
	 * cannot be made compatible, throws exception.
	 */
	private void assertCompatibility(EnvironmentIF environment,
			ValueTypeIF type1, ValueTypeIF type2, Sourceable sourceable)
			throws ExecutionException {
		try {
			if (type1.equals(type2))
				return;
			if (type1 instanceof ArrayValueTypeIF
					&& type2 instanceof ArrayValueTypeIF) {
				ValueIF assumption = environment.getAssumption();
				ArrayValueTypeIF atype1 = (ArrayValueTypeIF) type1;
				ArrayValueTypeIF atype2 = (ArrayValueTypeIF) type2;
				ValueIF length1 = atype1.lengthVector();
				ValueIF length2 = atype2.lengthVector();
				ValueTypeIF baseType1 = atype1.baseType();
				ValueTypeIF baseType2 = atype2.baseType();

				if (length1 == null) {
					if (length2 != null)
						throw new ExecutionException(
								sourceable,
								ErrorKind.COMMUNICATION,
								Certainty.MAYBE,
								"Incompatible array types:"
										+ "\n    extent for array type 1 : none"
										+ "\n    extent for array type 2 : "
										+ length2);
				} else {
					if (length2 == null)
						throw new ExecutionException(
								sourceable,
								ErrorKind.COMMUNICATION,
								Certainty.MAYBE,
								"Incompatible array types:"
										+ "\n    extent for array type 1 : "
										+ length1
										+ "\n    extent for array type 2 : none");

					ValueIF claim = dynamicFactory.equals(assumption, length1,
							length2);
					ResultType truth = dynamicFactory.valid(assumption, claim);

					if (truth != ResultType.YES) {
						Certainty certainty;
						String message;

						if (truth == ResultType.MAYBE) {
							certainty = Certainty.MAYBE;
							message = "Unable to prove array types have same extent:";
						} else {
							certainty = Certainty.PROVEABLE;
							message = "It is possible for the array types to have different extents:";
						}
						message += "\n   extent of type 1: " + length1
								+ "\n   extent of type 2: " + length2;
						log.report(new ExecutionException(sourceable,
								ErrorKind.COMMUNICATION, certainty, message));
						environment.addAssumption(claim);
					}
					assertCompatibility(environment, baseType1, baseType2,
							sourceable);
				}
			} else {
				throw new ExecutionException(sourceable,
						ErrorKind.COMMUNICATION, Certainty.PROVEABLE,
						"Incompatible types:" + "\n    type 1 : " + type1
								+ "\n    type 2 : " + type2);
			}
		} catch (DynamicException error) {
			throw new ExecutionException(sourceable, error, Certainty.NONE);
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(sourceable, problem);
		}
	}

	/**
	 * Given a reference and a value, this method tells you whether or not it is
	 * OK (type-safe) to stick that value into the referenced location.
	 * 
	 * Example 1: a_obj is real[n][m][l]; r = &a_obj[i]; Check that v is a
	 * symbolic value of type real[m'][l'] and that the assertions m=m' and l=l'
	 * are valid under the assumption.
	 * 
	 * Example 2: same as above, but r=&a_obj[i][j][k]. Then check that v has
	 * type real, the base type of a_obj.
	 */
	// private ResultType isCompatible(ValueIF assumption,
	// ReferenceValueIF reference, ValueIF value) throws ExecutionProblem {
	// ReferenceValueTypeIF referenceType = reference.valueType();
	// ValueTypeIF valueType1 = referenceType.baseType();
	// ValueTypeIF valueType2 = value.valueType();
	//
	// return isCompatible(assumption, valueType1, valueType2);
	// }

	/**
	 * Copies data into a receive buffer. Checks a number of things and throws
	 * exception if any of those things are violated.
	 * 
	 * reference: a reference to the receive buffer. Note that this is a
	 * reference to the whole buffer, not just to the first element of the
	 * buffer. For example, if the buffer is an array, this is a reference to an
	 * array.
	 * 
	 * data: the message data. This may be an array of elements or just a single
	 * element.
	 * 
	 * Let type1 denote the type of the thing referenced by reference. For
	 * example, if the receive buffer is an array of length 10 of int, then
	 * type1 will be "array of length 10 of int".
	 * 
	 * Let type2 be the type of the message data. For example, if the message
	 * data is an array of length 8 of int, type2 will be
	 * "array of length 8 of int".
	 * 
	 * type1 and type2 must be suitably compatible. The type compatibility
	 * requirements are relaxed somewhat to reflect the flexible nature of an
	 * MPI receive operation:
	 * 
	 * if type1 equals type2 then OK: assign the data to the referenced buffer
	 * 
	 * if type2 is an array of length 0, also fine: do nothing.
	 * 
	 * if type1 is an array of length N of T1 and type2 is an array of length M
	 * of T2, and T1 and T2 are compatible (strict compatibility) and M=N, then
	 * OK: again assign the data to the reference buffer
	 * 
	 * if type1 is an array of length N of T1 and type2 is an array of length M
	 * of T2, and T1 and T2 are compatible (strict compatibility) and M<=N, then
	 * OK: iterate over the elements of the data array and assign them to the
	 * corresponding cells in the referenced buffer
	 * 
	 * if type1 is an array of length N of T, and type2 is T, then OK: assign
	 * data to the first element of the array.
	 * 
	 * if type is T, and type2 is an array of length 1 of T, then OK: assign the
	 * first (and only) element of the data to the buffer.
	 * 
	 * */
	private void writeToRecvBuffer(EnvironmentIF environment,
			ReferenceValueIF reference, ValueIF data, Sourceable sourceable)
			throws ExecutionProblem, DynamicException {
		ValueIF assumption = environment.getAssumption();
		ReferenceValueTypeIF referenceType = reference.valueType();
		ValueTypeIF type1 = referenceType.baseType();
		ValueTypeIF type2 = data.valueType();
		ArrayValueTypeIF arrayType1 = null, arrayType2 = null;
		ValueIF extent1 = null, extent2 = null;

		if (type1.equals(type2)) {
			assignValue(environment, reference, data, sourceable);
			return;
		}
		if (type1 instanceof ArrayValueTypeIF) {
			arrayType1 = (ArrayValueTypeIF) type1;
			extent1 = arrayType1.extent();
		}
		if (type2 instanceof ArrayValueTypeIF) {
			ValueIF claim;

			arrayType2 = (ArrayValueTypeIF) type2;
			extent2 = arrayType2.extent();
			claim = dynamicFactory.equals(assumption, zero, extent2);
			if (dynamicFactory.isValid(assumption, claim)) {
				// message size 0: nothing to do:
				return;
			}
		}
		// ragged array not supported for messages!
		assert arrayType1 == null || arrayType1.dimension() == 1;
		assert arrayType2 == null || arrayType2.dimension() == 1;
		if (arrayType1 != null && arrayType2 != null) {
			// if both are arrays, they have to have the same element type
			// and extent2 <= extent1...

			ValueIF claim;
			ResultType truth;

			assertCompatibility(environment, arrayType1.baseType(),
					arrayType2.baseType(), sourceable);
			claim = dynamicFactory.equals(assumption, extent1, extent2);
			truth = dynamicFactory.valid(assumption, claim);

			if (truth == ResultType.YES) {
				assignValue(environment, reference, data, sourceable);
				return;
			}

			claim = dynamicFactory.lessThanOrEquals(assumption, extent2,
					extent1);
			truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				Certainty certainty;
				String message;

				if (truth == ResultType.MAYBE) {
					certainty = Certainty.MAYBE;
					message = "Cannot prove that the length of the message is less than"
							+ "\nor equal to the length of the receive buffer:";
				} else {
					certainty = Certainty.PROVEABLE;
					message = "It is possible for the length of the message to be"
							+ "\ngreater than the length of the receive buffer:";
				}
				message += "\n   buffer length : " + extent1
						+ "\n  message length : " + extent2;
				log.report(new ExecutionException(sourceable,
						ErrorKind.COMMUNICATION, certainty, message));
				environment.addAssumption(claim);
			}

			// get concrete count and iterate over message doing assignment:
			IntegerNumberIF messageLengthNumber = (IntegerNumberIF) dynamicFactory
					.numericValue(assumption, extent2);

			if (messageLengthNumber == null) {
				throw new ExecutionException(sourceable,
						ErrorKind.COMMUNICATION, Certainty.NONE,
						"TASS is unable to extract a concrete length from message:"
								+ "\n   message length : " + extent2);
			}

			int messageLength = messageLengthNumber.intValue();

			for (int i = 0; i < messageLength; i++) {
				ValueIF index = dynamicFactory.symbolicValue(i);
				ValueIF message = dynamicFactory.arrayRead(assumption,
						(ArrayValueIF) data, index);
				ArrayElementReferenceValueIF bufferElementReference = dynamicFactory
						.arrayElementReference(reference, index);

				assignValue(environment, bufferElementReference, message,
						sourceable);
			}
			return;
		}
		if (arrayType1 != null) {
			ArrayElementReferenceValueIF bufferElementReference = dynamicFactory
					.arrayElementReference(reference, zero);

			assignValue(environment, bufferElementReference, data, sourceable);
			return;
		}
		if (arrayType2 != null) {
			ValueIF message = dynamicFactory.arrayRead(assumption,
					(ArrayValueIF) data, zero);

			assignValue(environment, reference, message, sourceable);
		}
		throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
				Certainty.PROVEABLE,
				"Receive buffer is incompatible with type of incoming message:"
						+ "\n    buffer type  : " + type1
						+ "\n    message type : " + type2);
	}

	/** Returns the evaluator used by this executor. */
	@Override
	public EvaluatorIF evaluator() {
		return evaluator;
	}

	@Override
	public LibraryExecutorLoaderIF libraryExecutorLoader() {
		// TODO Auto-generated method stub
		return null;
	}

}