RunConfiguration.java

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

import java.io.File;
import java.io.PrintWriter;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;

import edu.udel.cis.vsl.tass.number.Numbers;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.number.IF.NumberIF;

public class RunConfiguration {

	/**
	 * State reduction strategy type.
	 */
	public enum ReductionStrategy {
		STANDARD, URGENT
	};

	/**
	 * How to deal with deadlocks in the model(s). MPI has the notion of
	 * "potential" deadlock: a state in which deadlock may occur if all
	 * buffering is turned off.
	 * 
	 * IGNORE: don't worry about deadlocks at all. ABSOLUTE: report absolute
	 * deadlocks, but not potential deadlocks that are not absolute. POTENTIAL:
	 * report any potential deadlock (including absolute ones).
	 * 
	 * @author siegel
	 * 
	 */
	public enum DeadlockStrategy {
		IGNORE, ABSOLUTE, POTENTIAL
	};

	public enum Frontend {
		ANTLR, CLANG
	}

	public enum TheoremProverType {
		CVC3
	};

	public enum RunningMode {
		COMPARE, VERIFY, EXTRACT
	};

	/** Used when reading a trace file only. */
	private File traceFile = null;

	/** Used when reading trace file: result of parsing trace file. */
	private int[] guide;

	private Map<String, Object> inputMap = new LinkedHashMap<String, Object>();

	private TheoremProverType proverType = TheoremProverType.CVC3;

	private RunningMode runningMode = null;

	private boolean verbose = false;

	private ReductionStrategy reductionStrategy = ReductionStrategy.URGENT;

	private DeadlockStrategy deadlockStrategy = DeadlockStrategy.ABSOLUTE;

	/** Use standard symbolic simplification routine */
	private boolean simplify = true;

	private boolean useConcreteArrays = true;

	private int bufferBound = 10;

	private boolean useLoopTechnique = false;

	private PrintWriter out = new PrintWriter(System.out);

	private PrintWriter debugOut = null;

	private File workingDirectory = null;

	private static NumberFactoryIF numberFactory = Numbers.REAL_FACTORY;

	private Frontend frontend = Frontend.ANTLR;

	private boolean useCollectiveAssertions = false;

	private boolean detectCycles = false;

	private boolean showProverQueries = false;

	private boolean showQueries = false;

	private boolean showStates = false;

	private boolean showTransitions = false;

	private boolean showSavedStates = false;

	private boolean drawGraph = false;

	private boolean showSimplifications = false;

	private boolean showModel = false;

	private boolean cqmin = true;

	/** Stop searching after finding this many errors */
	private int errorBound = 1;

	/** The arguments from the command-line */
	// TODO: get rid of this and instead generate the args from
	// the config fields...
	// private String[] args = new String[0];

	RunConfiguration(File repository) {
		setWorkingDirectory(repository);
	}

	RunConfiguration() {
		// for absolute path, use: File(System.getProperty("user.dir"));
		this(new File(new File("."), "TASSREP"));
	}

	RunConfiguration(RunConfiguration that) {
		this(that.workingDirectory);
		this.proverType = that.proverType;
		this.runningMode = that.runningMode;
		this.verbose = that.verbose;
		this.reductionStrategy = that.reductionStrategy;
		this.deadlockStrategy = that.deadlockStrategy;
		this.simplify = that.simplify;
		this.bufferBound = that.bufferBound;
		this.useLoopTechnique = that.useLoopTechnique;
		this.out = that.out;
		this.debugOut = that.debugOut;
		this.workingDirectory = that.workingDirectory;
		this.inputMap.putAll(that.inputMap);
		this.frontend = that.frontend;
		this.errorBound = that.errorBound;
		this.detectCycles = that.detectCycles;
		this.useCollectiveAssertions = that.useCollectiveAssertions;
		this.showQueries = that.showQueries;
		this.showProverQueries = that.showProverQueries;
		this.showStates = that.showStates;
		this.showSavedStates = that.showSavedStates;
		this.showTransitions = that.showTransitions;
		this.showSimplifications = that.showSimplifications;
		this.showModel = that.showModel;
		this.cqmin = that.cqmin;
		// this.args = that.args;
		this.traceFile = that.traceFile;
		this.guide = that.guide;
	}

	/**
	 * Returns a map containing all input variables associated with this
	 * configuration.
	 * 
	 * @return A map containing all input variabls.
	 */
	public Map<String, Object> inputMap() {
		return inputMap;
	}

	/**
	 * Add an input variable to the input map.
	 * 
	 * @param name
	 *            Name of the variable.
	 * @param value
	 *            Value of the variable.
	 */
	public void setInput(String name, Object value) {
		if (value instanceof Boolean || value instanceof NumberIF) {
			// OK
		} else if (value instanceof Integer) {
			value = numberFactory.integer((Integer) value);
		} else if (value instanceof Double || value instanceof Float) {
			value = numberFactory.rational(value.toString());
		} else {
			throw new IllegalArgumentException("Illegal kind of input value: "
					+ value);
		}
		inputMap.put(name, value);
	}

	/**
	 * Returns <code>true<code> if concrete value array is used in verification
	 * process.
	 * 
	 * @return <code>true<code> if verification uses concrete value arrays.
	 */
	public boolean useConcreteArrays() {
		return useConcreteArrays;
	}

	/**
	 * Uses (or don't use) concrete value arrays in verification.
	 * 
	 * @param value
	 *            <code>true<code> to use concrete value arrays, otherwise don't use them.
	 */
	public void setUseConcreteArrays(boolean value) {
		this.useConcreteArrays = value;
	}

	/**
	 * Returns
	 * <code>true<code> if in verbose mode. In verbose mode, TASS will output extra 
	 * information about the verification process such as states and variable values.
	 * 
	 * @return <code>true<code> if TASS is in verbose running mode.
	 */
	public boolean verbose() {
		return verbose;
	}

	/**
	 * Turn on (or off) verbose mode.
	 * 
	 * @param verbose
	 *            <code>true<code> to turn on verbose mode, <code>false<code> to turn it off.
	 */
	public void setVerbose(boolean verbose) {
		if (verbose) {
			this.showProverQueries = true;
			this.showQueries = true;
			this.showStates = true;
			this.showTransitions = true;
			this.showSavedStates = true;
			this.showSimplifications = true;
			this.showModel = true;
		}
		this.verbose = verbose;
	}

	/**
	 * Returns the current running mode of TASS. TASS has three running modes:
	 * verify, compare and extract.
	 * 
	 * @return Running mode of TASS.
	 */
	public RunningMode runningMode() {
		return runningMode;
	}

	/**
	 * Set the running mode for TASS.
	 * 
	 * @param runningMode
	 *            Running mode for TASS, should be one of verify, compare or
	 *            extract.
	 */
	protected void setRunningMode(RunningMode runningMode) {
		this.runningMode = runningMode;
	}

	/**
	 * Returns the prover type used by TASS.
	 * 
	 * @return Prover type used by TASS in verification.
	 */
	public TheoremProverType proverType() {
		return proverType;
	}

	/**
	 * Set the prover type for TASS.
	 * 
	 * @param proverType
	 *            Prover type used by TASS.
	 */
	public void setProverType(TheoremProverType proverType) {
		this.proverType = proverType;
	}

	public void setUseCollectiveAssertions(boolean value) {
		this.useCollectiveAssertions = value;
	}

	public boolean useCollectiveAssertions() {
		return useCollectiveAssertions;
	}

	public void setDetectCycles(boolean value) {
		this.detectCycles = value;
	}

	public boolean detectCycles() {
		return detectCycles;
	}

	/**
	 * Returns the reduction strategy used by TASS.
	 * 
	 * @return State reduction strategy used by TASS.
	 */
	public ReductionStrategy reductionStrategy() {
		return reductionStrategy;
	}

	/**
	 * Set the reduction strategy for TASS.
	 * 
	 * @param strategy
	 *            State reduction strategy.
	 */
	public void setReductionStrategy(ReductionStrategy strategy) {
		this.reductionStrategy = strategy;
	}

	/**
	 * Returns the deadlock detection strategy used by TASS.
	 * 
	 * @return Deadlock detection strategy used by TASS.
	 */
	public DeadlockStrategy deadlockStrategy() {
		return deadlockStrategy;
	}

	/**
	 * Set the deadlock detection strategy for TASS.
	 * 
	 * @param strategy
	 *            Deadlock detection strategy for TASS.
	 */
	public void setDeadlockStrategy(DeadlockStrategy strategy) {
		this.deadlockStrategy = strategy;
	}

	/**
	 * Returns <code>true<code> if TASS will simplify symbolic expressions
	 * during verification process.
	 * 
	 * @return <code>true<code> if TASS will simplify symbolic expressions.
	 */
	public boolean simplify() {
		return this.simplify;
	}

	/**
	 * Simplify (or do not simplify) symbolic expressions during execution.
	 * 
	 * @param value
	 *            <code>true<code> to let TASS simplify symbolic expression, <code>false<code> otherwise.
	 */
	public void setSimplify(boolean value) {
		this.simplify = value;
	}

	/**
	 * Returns the maximum size of buffer used by TASS.
	 * 
	 * @return Maximum size of buffer.
	 */
	public int bufferBound() {
		return this.bufferBound;
	}

	/**
	 * Set the buffer bound for TASS.
	 * 
	 * @param bound
	 *            Buffer bound used by TASS in verification.
	 */
	public void setBufferBound(int bound) {
		if (bound <= 0) {
			System.err.println("Buffer bound must be greater than 0.");
			System.exit(-1);
		}
		this.bufferBound = bound;
	}

	/**
	 * Returns <code>true<code> if the loop joint invariant technique is used.
	 * 
	 * @return <code>true<code> if TASS uses the loop joint invariant technique.
	 */
	public boolean useLoopTechnique() {
		return this.useLoopTechnique;
	}

	/**
	 * Use (or don't use) the loop joint invariant technique.
	 * 
	 * @param value
	 *            <code>true<code> to use the loop joint invariant technique, <code>false<code> otherwise.
	 */
	public void setLoopTechnique(boolean value) {
		this.useLoopTechnique = value;
	}

	public PrintWriter out() {
		return out;
	}

	public PrintWriter debugOut() {
		return debugOut;
	}

	public void setOut(PrintWriter out) {
		this.out = out;
	}

	public void setDebugOut(PrintWriter debugOut) {
		this.debugOut = debugOut;
	}

	public void setWorkingDirectory(File directory) {
		if (!directory.isDirectory()) {
			if (directory.exists()) {
				throw new RuntimeException("Not a directory: " + directory);
			}
			directory.mkdir();
			if (!directory.isDirectory()) {
				throw new RuntimeException("Unable to create directory: "
						+ directory);
			}
		}
		workingDirectory = directory;
	}

	public File workingDirectory() {
		return workingDirectory;
	}

	public Frontend getFrontend() {
		return frontend;
	}

	public void setFrontend(Frontend frontend2) {
		this.frontend = frontend2;
	}

	public int errorBound() {
		return errorBound;
	}

	public void setErrorBound(int bound) {
		this.errorBound = bound;
	}

	public boolean showProverQueries() {
		return showProverQueries;
	}

	public void setShowProverQueries(boolean showProverQueries) {
		this.showProverQueries = showProverQueries;
	}

	public boolean showQueries() {
		return showQueries;
	}

	public void setShowQueries(boolean showQueries) {
		this.showQueries = showQueries;
	}

	public boolean showStates() {
		return showStates;
	}

	public void setShowStates(boolean showStates) {
		this.showStates = showStates;
	}

	public boolean showTransitions() {
		return showTransitions;
	}

	public void setShowTransitions(boolean showTransitions) {
		this.showTransitions = showTransitions;
	}

	public boolean showSavedStates() {
		return showSavedStates;
	}

	public void setShowSavedStates(boolean showSavedStates) {
		this.showSavedStates = showSavedStates;
	}

	public boolean drawGraph() {
		return drawGraph;
	}

	public void setDrawGraph(boolean drawGraph) {
		this.drawGraph = drawGraph;
	}

	public boolean showSimplifications() {
		return showSimplifications;
	}

	public void setShowSimplifications(boolean showSimplifications) {
		this.showSimplifications = showSimplifications;
	}

	public boolean showModel() {
		return showModel;
	}

	public void setShowModel(boolean showModel) {
		this.showModel = showModel;
	}

	public boolean cqmin() {
		return cqmin;
	}

	public void setCqmin(boolean cqmin) {
		this.cqmin = cqmin;
	}

	// public void setArgs(String[] args) {
	// this.args = args;
	// }
	//
	// public String[] args() {
	// return args;
	// }

	public File traceFile() {
		return traceFile;
	}

	public void setTraceFile(File traceFile) {
		this.traceFile = traceFile;
	}

	public boolean replay() {
		return traceFile != null;
	}

	public int[] guide() {
		return guide;
	}

	public void setGuide(int[] guide) {
		this.guide = guide;
	}

	public void print(PrintWriter out) {
		out.println("                mode : " + runningMode);
		if (replay()) {
			out.println("           traceFile : " + traceFile);
		}
		out.println("              prover : " + proverType);
		out.println("            deadlock : " + deadlockStrategy);
		out.println("           reduction : " + reductionStrategy);
		out.println("            simplify : " + simplify);
		out.println("         bufferBound : " + bufferBound);
		out.println("             verbose : " + verbose);
		out.println("         loop method : " + useLoopTechnique);
		out.println("   collectiveAsserts : " + useCollectiveAssertions);
		out.println("               cqmin : " + cqmin);
		out.println("        detectCycles : " + detectCycles);
		out.println("          repository : " + workingDirectory);
		out.println("            frontend : " + frontend);
		out.println("          errorBound : " + errorBound);
		for (String variable : inputMap.keySet()) {
			int length = variable.length();
			int numSpaces = 20 - length;

			if (numSpaces < 0)
				numSpaces = 0;
			for (int i = 0; i < numSpaces; i++)
				out.print(" ");
			out.println(variable + " = " + inputMap.get(variable));
		}
		out.println();
		out.flush();
	}

	public void write(PrintWriter out) {
		for (Option option : Options.options()) {
			if (Options.isApplicable(this, option))
				out.println("-" + option.name() + "=" + option.get(this));
		}
		for (Entry<String, Object> entry : inputMap.entrySet()) {
			out.println("-input" + entry.getKey() + "=" + entry.getValue());
		}
	}

	@Override
	public RunConfiguration clone() {
		return new RunConfiguration(this);
	}

	/**
	 * Returns the file containing the XML schema tass_ast.xsd.
	 */
	public File getAstXmlSchema() {
		// the directory containing the schema should be here:
		String path = System.getProperty("tass.xml.path");

		if (path == null) {
			return null;
		} else {
			File xmlDirectory = new File(path);
			File schema = new File(xmlDirectory, "tass_ast.xsd");

			return schema;
		}
	}

	/** Returns absolute path to libPrintTassAST.dylib */
	public File getClangAstLib() {
		String result = System.getProperty("clang.ast.lib");

		if (result == null) {
			return null;
		} else {
			return new File(result);
		}
	}
	
	/** Returns absolute path to the clang binary */
	public File getClangBinary() {
		String result = System.getProperty("clang.bin.path");
		
		if (result == null) {
			// Hope that the right clang is in the default path
			return new File("clang");
		} else {
			return new File(result);
		}
	}

	/**
	 * Returns absolute path to the "include" directory where TASS's special
	 * include header files for libraries is located.
	 */
	public File getTassIncludePath() {
		String result = System.getProperty("tass.include.path");

		if (result == null) {
			return null;
		} else {
			return new File(result);
		}
	}

}