Runner.java

package edu.udel.cis.vsl.tass.ui;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.Map;

import edu.udel.cis.vsl.tass.ast.ASTs;
import edu.udel.cis.vsl.tass.ast.IF.ASTParserException;
import edu.udel.cis.vsl.tass.ast.IF.ASTParserIF;
import edu.udel.cis.vsl.tass.ast.IF.AbstractSyntaxTreeIF;
import edu.udel.cis.vsl.tass.ast2model.IF.ModelBuilderIF;
import edu.udel.cis.vsl.tass.ast2model.impl.ModelBuilder;
import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration.Frontend;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.front.minimp.ModelExtractor;
import edu.udel.cis.vsl.tass.front.minimp.ModelPair;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.util.Strings;
import edu.udel.cis.vsl.tass.util.TASSInternalException;
import edu.udel.cis.vsl.tass.verify.Verify;

/**
 * A runner is responsible for invoking the various TASS components to solve a
 * problem specified in a RunConfiguration object. It invokes front-end
 * components to parse source code and construct a model, and invokes the
 * verification engine to verify a single model or establish equivalence of two
 * models.
 */
public class Runner {

	/**
	 * The configuration object encoding the information specifying the problem
	 * to solve, including all options, filenames, etc.
	 */
	private RunConfiguration configuration;

	/**
	 * A shortcut to configuration.out(), where all standard output is to be
	 * sent.
	 */
	private PrintWriter out;

	public Runner(RunConfiguration configuration) {
		this.configuration = configuration;
		out = configuration.out();
	}

	private void checkInputs(ModelIF model, Map<String, Object> inputMap)
			throws CommandLineException {
		for (String variableName : inputMap.keySet()) {
			SharedVariableIF variable = model.scope().variableWithName(
					variableName);

			if (variable == null) {
				throw new CommandLineException("Model " + model
						+ " does not contain an input variable " + variableName);
			}
			if (!variable.isInput()) {
				throw new CommandLineException("Variable " + variableName
						+ " of model " + model + " is not an input variable");
			}
		}
	}

	private File sourceToXML(RunConfiguration configuration, File sourceFile)
			throws IOException {
		Runtime runtime = Runtime.getRuntime();
		File xmlFile = new File(configuration.workingDirectory(),
				sourceFile.getName() + ".xml");
		String command = configuration.getClangBinary() + " -cc1 -load "
				+ configuration.getClangAstLib() + " -iwithsysroot "
				+ configuration.getTassIncludePath()
				+ " -plugin print-tass -plugin-arg-print-tass "
				+ xmlFile.getAbsolutePath() + " "
				+ sourceFile.getAbsolutePath();
		Process clangProcess;

		out.println(command);
		out.flush();
		clangProcess = runtime.exec(command);
		try {
			clangProcess.waitFor();
		} catch (InterruptedException e) {
			e.printStackTrace();
			throw new TASSInternalException(
					"Clang process was unable to complete.");
		}
		return xmlFile;
	}

	private AbstractSyntaxTreeIF parseXML(RunConfiguration configuration,
			File xmlFile) throws IOException, SyntaxException {
		File schemaFile = configuration.getAstXmlSchema();
		ASTParserIF parser;
		AbstractSyntaxTreeIF ast;

		if (schemaFile == null) {
			throw new TASSInternalException(
					"TASS has not been configured correctly: no XML schema file found.\n"
							+ "Please set tass.xml.path in build.properties.");
		}
		parser = ASTs.makeASTParser(xmlFile, schemaFile);
		try {
			ast = parser.parseDocument();
		} catch (ASTParserException e) {
			throw new SyntaxException("Error parsing AST file " + xmlFile
					+ ":\n" + e);
		}
		return ast;
	}

	private ModelIF astToModel(VerifyConfiguration configuration,
			AbstractSyntaxTreeIF ast) throws SyntaxException {
		ModelBuilderIF modelBuilder = new ModelBuilder();
		ModelIF model = modelBuilder.buildModel(configuration, ast);

		return model;
	}

	/**
	 * Executes the necessary TASS components to solve the problem.
	 */
	public boolean run() throws IOException, SyntaxException,
			CommandLineException {
		configuration.print(out);
		if (configuration instanceof VerifyConfiguration) {
			VerifyConfiguration verifyConfiguration = (VerifyConfiguration) configuration;
			boolean verbose = configuration.verbose();
			ModelIF model = null;
			Frontend frontend = configuration.getFrontend();

			if (verbose) {
				out.println("Extracting model...");
				out.flush();
			}
			if (frontend == Frontend.ANTLR) {
				model = ModelExtractor.extractModel(verifyConfiguration);
			} else if (frontend == Frontend.CLANG) {
				File sourceFile = verifyConfiguration.sourceFile();
				String sourceFilename = sourceFile.getName();
				String suffix = Strings.getSuffix(sourceFilename);
				File xmlFile;
				AbstractSyntaxTreeIF ast;

				if ("c".equals(suffix)) {
					xmlFile = sourceToXML(configuration, sourceFile);
				} else if ("xml".equals(suffix)) {
					xmlFile = sourceFile;
				} else {
					throw new CommandLineException("Unknown file suffix in: "
							+ sourceFilename + "\n Expected \".c\" or \".xml\"");
				}
				ast = parseXML(configuration, xmlFile);
				if (verbose) {
					ast.print(out);
				}
				model = astToModel(verifyConfiguration, ast);
			} else {
				throw new CommandLineException("Unknown frontend: " + frontend);
			}
			if (verbose || configuration.showModel()) {
				out.println();
				model.print(out, true);
				out.println();
				out.flush();
			}
			checkInputs(model, configuration.inputMap());
			return Verify.verify(model, verifyConfiguration, false);
		} else if (configuration instanceof CompareConfiguration) {
			CompareConfiguration compareConfiguration = (CompareConfiguration) configuration;
			boolean verbose = configuration.verbose();
			ModelPair pair;

			if (verbose) {
				out.println("Extracting models...");
				out.flush();
			}
			pair = ModelExtractor.extractModelPair(compareConfiguration);
			if (verbose || configuration.showModel()) {
				out.println();
				pair.spec().print(out, true);
				out.println();
				pair.impl().print(out, true);
				out.println();
				out.flush();
			}
			checkInputs(pair.impl(), configuration.inputMap());
			return Verify.compare(pair.spec(), pair.impl(),
					compareConfiguration, false);
		} else {
			throw new TASSInternalException("Unknown type of configuration");
		}
	}
}