LibstdlibExecutor.java

package edu.udel.cis.vsl.tass.library.libstdlib;

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.value.ArrayElementReferenceValueIF;
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.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.statement.InvocationStatementIF;
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.ExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorIF;
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;

public class LibstdlibExecutor implements LibraryExecutorIF {

	private EvaluatorIF evaluator;

	private DynamicFactoryIF dynamicFactory;

	private LogIF log;

	public LibstdlibExecutor(ExecutorIF executor, EvaluatorIF evaluator) {
		this.evaluator = evaluator;
		this.dynamicFactory = evaluator.dynamicFactory();
		this.log = evaluator.log();
	}

	@Override
	public boolean containsFunction(String name) {
		if ("free".equals(name))
			return true;
		return false;
	}

	@Override
	public void execute(EnvironmentIF environment,
			InvocationStatementIF invocation) throws ExecutionException {
		String name = invocation.callee().name();

		if ("free".equals(name))
			executeFree(environment, invocation);
		else {
			throw new ExecutionException(invocation, ErrorKind.LIBRARY,
					Certainty.MAYBE, "Unknown function: " + name);
		}
	}

	private void executeFree(EnvironmentIF environment,
			InvocationStatementIF statement) {
		ExpressionIF pointerExpression = statement.arguments()[0];
		ReferenceValueIF reference;

		try {
			reference = (ReferenceValueIF) evaluator.evaluate(environment,
					pointerExpression);
		} catch (ExecutionProblem problem) {
			log.report(new ExecutionException(statement, problem));
			return;
		}
		if (reference instanceof ArrayElementReferenceValueIF) {
			ArrayElementReferenceValueIF arrayElementReference = (ArrayElementReferenceValueIF) reference;
			ValueIF index = arrayElementReference.index();

			if (dynamicFactory.zero().equals(index)) {
				ReferenceValueIF parent = arrayElementReference.parent();

				if (parent instanceof VariableReferenceValueIF) {
					VariableReferenceValueIF parentReference = (VariableReferenceValueIF) parent;
					CellIF parentVariable = parentReference.variable();

					if (parentVariable instanceof HeapCellIF) {
						HeapCellIF heapVariable = (HeapCellIF) parentVariable;
						ValueIF oldValue = environment.valueOf(heapVariable);

						if (oldValue == null) {
							ExecutionException error = new ExecutionException(
									statement, ErrorKind.POINTER,
									Certainty.PROVEABLE,
									"Invalid heap reference:\nexpression: "
											+ pointerExpression
											+ "\nvariable: " + heapVariable);

							log.report(error);
						}
						environment.setValue(heapVariable, null);
						try {
							environment.canonicalizeHeap(statement.process(),
									statement);
						} catch (ExecutionProblem error) {
							log
									.report(new ExecutionException(statement,
											error));
						}
						return;
					}
				}
			}
		}
		// invalid call to free: report and treat as no-op...
		log.report(new ExecutionException(statement, ErrorKind.POINTER,
				Certainty.PROVEABLE,
				"Attempt to call free on a pointer that was not returned by malloc:\n"
						+ reference));

	}

	@Override
	public String name() {
		return "libstdlib";
	}

	@Override
	public void initialize(EnvironmentIF environment) throws ExecutionException {
	}

	@Override
	public void wrapUp(EnvironmentIF environment) throws ExecutionException {
		// TODO Auto-generated method stub
		// check there are no unfreeded objects in heap, ...

	}

}