LibstdioExecutor.java

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

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
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.cell.ProcessCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.SharedCellIF;
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.RecordValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VectorValueIF;
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.statement.InvocationStatementIF;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
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.morph.MorphicVectorFactory;
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.ErrorKind;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;

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.util.TASSInternalException;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * Provides execution semantics for library stdio.
 * 
 * THIS IS A WORK IN PROGRESS.
 * 
 * FILE *fopen(const char * restrict filename, const char * restrict mode);
 * 
 * Provides method to initialize state.
 * 
 * Provides executors for the following system functions:
 * 
 * int fclose(FILE *stream);
 * 
 * int fflush(FILE *stream);
 * 
 * int fprintf(FILE * restrict stream, const char * restrict format, ...);
 * 
 * int fscanf(FILE * restrict stream, const char * restrict format, ...);
 * 
 * int printf(const char * restrict format, ...);
 * 
 * The types defined in stdio.h (inserted by AST transformer):
 * 
 * 
 * TODO: might need to add pid to the following:
 * 
 * <code>
 * typedef struct STDIO_File {
 *   char filename[];    // the name of the file (including path)
 *   boolean isOutput;   // is this an output file? 
 *   boolean isInput;    // is this an input file? 
 *   boolean isBinary;   // can be binary or text 
 *   boolean isWide;     // wide orientation 
 *   char[][] contents;  // file contents: ragged array 
 * } STDIO_File;
 * 
 * typedef struct STDIO_Stream {
 *   STDIO_File *file; // file to which this stream refers
 *   boolean isOpen;   // is this stream open?
 *   int position1;    // current word in file
 *   int position2;    // character index in word
 *   int mode;         // Stream mode: r/w/a
 * } FILE;
 * </code>
 * 
 * The value types corresponding to these types: will have null for array
 * extents.
 * 
 * @author siegel
 * 
 */
public class LibstdioExecutor implements LibraryExecutorIF {

	/**
	 * The concrete integer constant corresponding to text stream mode "r"
	 * (read).
	 */
	public final static int MODE_R = 1;

	/**
	 * The concrete integer constant corresponding to text stream mode "w"
	 * (write).
	 */
	public final static int MODE_W = 2;

	/**
	 * The concrete integer constant corresponding to text stream mode "a"
	 * (append).
	 */
	public final static int MODE_A = 3;

	/**
	 * Integer values corresponding to the conrete integers MODE_R, etc.
	 */
	private ValueIF modeValue_r, modeValue_w, modeValue_a;

	/**
	 * String values "r", "w", "a", etc.
	 */
	private ValueIF modeString_r, modeString_w, modeString_a;

	private ValueIF trueValue;

	private int filenameFieldIndex, isOutputFieldIndex, isInputFieldIndex,
			isBinaryFieldIndex, isWideFieldIndex, contentsFieldIndex,
			fileFieldIndex, isOpenFieldIndex, position1FieldIndex,
			position2FieldIndex, modeFieldIndex;

	private EvaluatorIF evaluator;

	private RunConfiguration configuration;

	private LogIF log;

	private DynamicFactoryIF dynamicFactory;

	private MorphicVectorFactory<ValueIF> valueVectorFactory;

	private RecordTypeIF fileType;

	private RecordTypeIF streamType;

	private ValueTypeIF characterValueType, booleanValueType, integerValueType;

	private ArrayValueTypeIF stringValueType;

	private RecordValueTypeIF fileValueType;

	private RecordValueTypeIF streamValueType;

	private VectorValueTypeIF fileVectorValueType, streamVectorValueType;

	/**
	 * Cache of process global variables named "STDIO_files". Cache by model ID,
	 * process ID. Some entries could be null, if the process does not have this
	 * variable, which should happen only if the process never performs I/O.
	 */
	private ProcessVariableIF[][] filesystemVariables;

	/**
	 * For comparison mode, cache of output variables for output files.
	 * Variables have name "STDIO_outputFiles". Cached by model ID. Some entries
	 * could be null, if the model does not use the library.
	 * 
	 * If verification mode, null.
	 */
	private SharedVariableIF[] outputFileVariables = null;

	private ProcessCellIF[][] filesystemCells;

	/**
	 * In verification mode, null.
	 */
	private SharedCellIF[] outputFileCells = null;

	private ModelFactoryIF modelFactory;

	public LibstdioExecutor(ExecutorIF executor, EvaluatorIF evaluator) {
		int numModels;

		this.evaluator = evaluator;
		this.log = evaluator.log();
		this.dynamicFactory = evaluator.dynamicFactory();
		this.modeString_r = dynamicFactory.canonic(dynamicFactory.string("r"));
		this.modeString_w = dynamicFactory.canonic(dynamicFactory.string("w"));
		this.modeString_a = dynamicFactory.canonic(dynamicFactory.string("a"));
		this.modeValue_r = dynamicFactory.canonic(dynamicFactory
				.symbolicValue(MODE_R));
		this.modeValue_w = dynamicFactory.canonic(dynamicFactory
				.symbolicValue(MODE_W));
		this.modeValue_a = dynamicFactory.canonic(dynamicFactory
				.symbolicValue(MODE_A));
		this.configuration = dynamicFactory.configuration();
		this.modelFactory = evaluator.modelFactory();
		this.fileType = modelFactory.getRecordType("STDIO_File");
		this.streamType = modelFactory.getRecordType("STDIO_Stream");
		this.valueVectorFactory = dynamicFactory.valueVectorFactory();
		this.filenameFieldIndex = fileType.getFieldIndex("filename");
		this.isOutputFieldIndex = fileType.getFieldIndex("isOutput");
		this.isInputFieldIndex = fileType.getFieldIndex("isInput");
		this.isBinaryFieldIndex = fileType.getFieldIndex("isBinary");
		this.isWideFieldIndex = fileType.getFieldIndex("isWide");
		this.contentsFieldIndex = streamType.getFieldIndex("contents");
		this.fileFieldIndex = streamType.getFieldIndex("file");
		this.isOpenFieldIndex = streamType.getFieldIndex("isOpen");
		this.position1FieldIndex = streamType.getFieldIndex("position1");
		this.position2FieldIndex = streamType.getFieldIndex("position2");
		this.modeFieldIndex = streamType.getFieldIndex("mode");
		this.booleanValueType = dynamicFactory.booleanType();
		this.characterValueType = dynamicFactory.characterType();
		this.integerValueType = dynamicFactory.integerType();
		this.stringValueType = dynamicFactory.arrayValueType(
				characterValueType, null);
		this.fileValueType = dynamicFactory.recordValueType(fileType,
				new ValueTypeIF[] { stringValueType, booleanValueType,
						booleanValueType, booleanValueType, booleanValueType,
						dynamicFactory.arrayValueType(stringValueType, null) });
		this.streamValueType = dynamicFactory.recordValueType(
				streamType,
				new ValueTypeIF[] {
						dynamicFactory.referenceValueType(fileValueType),
						booleanValueType, integerValueType, integerValueType,
						integerValueType });
		this.fileVectorValueType = dynamicFactory
				.vectorValueType(fileValueType);
		this.streamVectorValueType = dynamicFactory
				.vectorValueType(streamValueType);
		numModels = modelFactory.numModels();
		if (configuration instanceof CompareConfiguration) {
			this.outputFileVariables = new SharedVariableIF[numModels];
			this.outputFileCells = new SharedCellIF[numModels];
		}
		this.filesystemVariables = new ProcessVariableIF[numModels][];
		this.filesystemCells = new ProcessCellIF[numModels][];
		for (int i = 0; i < numModels; i++) {
			ModelIF model = modelFactory.getModel(i);
			int numProcs = model.numProcs();

			if (outputFileVariables != null) {
				outputFileVariables[i] = model.scope().variableWithName(
						"STDIO_outputFiles");
				outputFileCells[i] = dynamicFactory
						.sharedCell(outputFileVariables[i]);
			}
			filesystemVariables[i] = new ProcessVariableIF[numProcs];
			filesystemCells[i] = new ProcessCellIF[numProcs];
			for (int j = 0; j < numProcs; j++) {
				ProcessIF process = model.process(j);

				filesystemVariables[i][j] = process.scope().variableWithName(
						"STDIO_files");
				filesystemCells[i][j] = dynamicFactory
						.processCell(filesystemVariables[i][j]);
			}
		}
	}

	private ProcessVariableIF getFilesystemVariable(ProcessIF process) {
		return filesystemVariables[process.model().id()][process.pid()];
	}

	private ProcessCellIF getFilesystemCell(ProcessIF process) {
		return filesystemCells[process.model().id()][process.pid()];
	}

	@Override
	public boolean containsFunction(String name) {
		// TODO Auto-generated method stub
		return false;
	}

	@Override
	public void execute(EnvironmentIF environment,
			InvocationStatementIF invocation) throws ExecutionException {
		// TODO Auto-generated method stub

	}

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

	public DynamicFactoryIF dynamicFactory() {
		return dynamicFactory;
	}

	public EvaluatorIF evaluator() {
		return evaluator;
	}

	public LogIF log() {
		return log;
	}

	// when processing model, you can process some of this information
	// once and store somewhere--associate to statement. or cache by
	// mid, pid, statement

	/**
	 * Given mode value as string ("r", "w", ...), convert to integer value (1,
	 * 2, ...).
	 * 
	 * @param modeString
	 * @return
	 * @throws DynamicException
	 */
	private ValueIF modeToInt(ValueIF assumption, ValueIF modeString)
			throws DynamicException, ExecutionProblem {
		if (dynamicFactory.isValid(assumption,
				dynamicFactory.equals(assumption, modeString_r, modeString)))
			return modeValue_r;
		if (dynamicFactory.isValid(assumption,
				dynamicFactory.equals(assumption, modeString_w, modeString)))
			return modeValue_w;
		if (dynamicFactory.isValid(assumption,
				dynamicFactory.equals(assumption, modeString_a, modeString)))
			return modeValue_a;
		throw new ExecutionProblem(ErrorKind.LIBRARY, Certainty.MAYBE,
				"stdlio:Unknown file stream mode: " + modeString);
	}

	/**
	 * Initialize the state components related to the stdio library.
	 * 
	 * Stdin: created on first process that issues read on stdin. If another
	 * process attempts to access stdin, error.
	 * 
	 * Stdout and stderr: for each of these:
	 * 
	 * if single program verification mode: ignore them.
	 * 
	 * if comparison mode: the first process that writes to stdout is the one
	 * that owns it. No other process may do so, else an error ensues. Ditto for
	 * stderr.
	 * 
	 */
	@Override
	public void initialize(EnvironmentIF environment) throws ExecutionException {
		int numModels = modelFactory.numModels();

		if (outputFileCells != null) {
			for (int mid = 0; mid < numModels; mid++) {
				SharedCellIF outputCell = this.outputFileCells[mid];

				if (outputCell != null) {
					environment.setValue(outputCell, dynamicFactory
							.emptyVectorValue(fileVectorValueType));
				}
			}
		}
		for (int mid = 0; mid < numModels; mid++) {
			ProcessCellIF[] filesystems = filesystemCells[mid];

			if (filesystems != null) {
				int numProcs = filesystems.length;

				for (int pid = 0; pid < numProcs; pid++) {
					ProcessCellIF filesystem = filesystems[pid];

					if (filesystem != null) {
						environment.setValue(filesystem, dynamicFactory
								.emptyVectorValue(fileVectorValueType));
					}
				}
			}
		}
	}

	@Override
	public void wrapUp(EnvironmentIF environment) throws ExecutionException {
		// TODO Auto-generated method stub
		// check there are no open streams
		// if compare mode, copy output files to output variable
	}

	/**
	 * Opens file with given filename and mode. Both arguments are given as
	 * dynamic values of string (array of char) type.
	 * 
	 * Only certain modes are currently handled: "r", "w".
	 * 
	 * Returns a stream (value of type FILE = struct STDIO_Stream) referring to
	 * the file.
	 * 
	 * @param filename
	 * @param mode
	 */
	private ValueIF openFile(EnvironmentIF environment, ProcessIF process,
			ValueIF filename, ValueIF mode) throws DynamicException {
		// loop through current files and see if matching filename
		ProcessCellIF filesystemCell = getFilesystemCell(process);
		VectorValueIF files;
		int numFiles;
		ValueIF assumption = environment.getAssumption();

		if (filesystemCell == null) {
			throw new TASSInternalException(
					"Attempt to open file on process that does not"
							+ " include stdlib: " + process);
		}
		files = (VectorValueIF) environment.valueOf(filesystemCell);
		numFiles = files.size();
		for (int i = 0; i < numFiles; i++) {
			RecordValueIF file = (RecordValueIF) files.get(i);
			ValueIF oldName = file.element(filenameFieldIndex);
			ValueIF predicate = dynamicFactory.equals(assumption, filename,
					oldName);
			ResultType result = dynamicFactory.valid(assumption, predicate);

			switch (result) {
			case YES: {
				// return new stream for this file.
				dynamicFactory
						.recordValue(
								assumption,
								streamValueType,
								new ValueIF[] {
										// reference to i-th element of
										// filesystem
										// variable
										dynamicFactory.vectorElementReference(
												dynamicFactory
														.referenceValue(
																filesystemCell,
																dynamicFactory
																		.referenceValueType(fileVectorValueType)),
												i), dynamicFactory.trueValue(),
										dynamicFactory.zero(),
										dynamicFactory.zero(), });
				break;
			}
			case MAYBE: // assume no, issue warning, add to path condition
			case NO:
				break;
			default:

			}

		}
		return null;
	}
}