CommandLineParser.java

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

import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.LinkedList;
import java.util.Vector;

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.Option;
import edu.udel.cis.vsl.tass.config.Options;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.config.Option.OptionType;
import edu.udel.cis.vsl.tass.number.Numbers;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.util.Strings;

public class CommandLineParser {

	private RunConfiguration configuration = null;

	private NumberFactoryIF numberFactory = Numbers.REAL_FACTORY;

	private PrintWriter out;

	public CommandLineParser(PrintWriter out, PrintWriter err) {
		this.out = out;
	}

	private void err(String message) throws CommandLineException {
		CommandLineException e = new CommandLineException(
				"Command-line error: " + message);

		throw e;
	}

	/**
	 * Parse command-line for replay command. Requires special handling: gather
	 * all arguments in an array, get the trace filename (only args not starting
	 * with "-"), open it, get its arg list into an array, append the given args
	 * onto the ones from the file, call parse method on the resulting array,
	 * set the traceFile field, set the guide.
	 */
	private RunConfiguration processReplay(String args[])
			throws CommandLineException, IOException {
		int numArgs = args.length;
		LinkedList<String> additionalArgs = new LinkedList<String>();
		String traceFilename = null;

		for (int j = 1; j < numArgs; j++) {
			String arg = args[j];

			if (arg.startsWith("-")) {
				additionalArgs.add(arg);
			} else {
				if (traceFilename != null) {
					err("Only one trace filename expected: " + arg);
				}
				traceFilename = arg;
			}
		}
		if (traceFilename == null) {
			err("Expected trace filename.");
		}

		File traceFile = new File(traceFilename);
		FileReader reader = new FileReader(traceFile);
		StringBuilder builder = new StringBuilder();
		Vector<String> argumentVector = new Vector<String>();

		// now read original args. two \n in a row means configs done.
		while (true) {
			int read = reader.read();

			if (read == '\n') {
				if (builder.length() == 0)
					break;
				argumentVector.add(builder.toString());
				builder = new StringBuilder();
			} else if (read < 0) {
				if (builder.length() != 0)
					err("Malformed trace file: did not end with newline: "
							+ builder.toString());
				break;
			} else {
				builder.append((char) read);
			}
		}
		for (String arg : additionalArgs)
			argumentVector.add(arg);

		String[] newArgs = argumentVector.toArray(new String[0]);
		Vector<Integer> intVector = new Vector<Integer>();

		while (true) {
			int read = reader.read();

			if (read == '\n') {
				String word = builder.toString();

				builder = new StringBuilder();
				try {
					int theInt = new Integer(word);

					if (theInt < 0) {
						err("Malformed trace file: transition index is negative: "
								+ theInt);
					}
					intVector.add(new Integer(word));
				} catch (NumberFormatException e) {
					err("Expected integer: " + word);
				}
			} else if (read < 0) {
				if (builder.length() != 0) {
					err("Malformed trace file: file ended without newline.");
				}
				break;
			} else {
				char character = (char) read;

				builder.append(character);
			}
		}
		reader.close();

		int numInts = intVector.size();
		int[] guide = new int[numInts];

		for (int i = 0; i < numInts; i++) {
			guide[i] = intVector.elementAt(i);
		}

		RunConfiguration configuration = parse(newArgs);

		configuration.setTraceFile(traceFile);
		configuration.setGuide(guide);
		return configuration;
	}

	public RunConfiguration parse(String args[]) throws CommandLineException,
			IOException {
		int numArgs = args.length;
		int numFilenames = 0;
		boolean verify = true;
		// Set<Option> usedOptions = new HashSet<Option>();

		if (numArgs == 0) {
			out.println("Type 'tass help' for usage.");
			out.flush();
			System.exit(0);
		}

		String command = args[0];

		if ("help".equals(command)) {
			printUsage();
			return null;
		} else if ("verify".equals(command)) {
			configuration = new VerifyConfiguration();
			verify = true;
		} else if ("compare".equals(command)) {
			configuration = new CompareConfiguration();
			verify = false;
		} else if ("replay".equals(command)) {
			return processReplay(args);
		} else {
			err("Unknown command: " + command);
		}
		configuration.setOut(out);
		// configuration.setArgs(args);
		for (int i = 1; i < numArgs; i++) {
			String arg = args[i];

			if (!arg.startsWith("-")) {
				// arg is filename
				numFilenames++;
				if (verify) {
					if (numFilenames > 1) {
						err("Only one filename expected for verify command: "
								+ arg);
					}
					((VerifyConfiguration) configuration)
							.setSourceFile(new File(arg));
				} else {
					if (numFilenames > 2) {
						err("Only two filenames expected for compare command: "
								+ arg);
					}
					if (numFilenames == 1)
						((CompareConfiguration) configuration)
								.setSpecSourceFile(new File(arg));
					else
						((CompareConfiguration) configuration)
								.setImplSourceFile(new File(arg));
				}
			} else {
				String key;
				String valueString;
				Object value = null;
				int equalsPos = arg.indexOf('=');

				if (equalsPos < 0) {
					key = arg.substring(1, arg.length());
					valueString = "true";
				} else {
					key = arg.substring(1, equalsPos);
					valueString = arg.substring(equalsPos + 1, arg.length());
				}
				if (key.startsWith("input")) {
					// put variable and value in input map
					String variableName = key.substring("input".length());

					if ("true".equals(valueString))
						value = true;
					else if ("false".equals(valueString))
						value = false;
					else {
						int decimalPosition = valueString.indexOf('.');

						if (decimalPosition < 0) {
							try {
								value = numberFactory.integer(valueString);
							} catch (Exception e) {
								err("Illegal numeric value for input: " + arg);
							}
						} else {
							try {
								value = numberFactory.rational(valueString);
							} catch (Exception e) {
								err("Illegal numeric value for input: " + arg);
							}
						}
					}
					configuration.setInput(variableName, value);
				} else {
					Option option = Options.getOption(key);
					// boolean seen = !usedOptions.add(option);

					if (option == null) {
						err("Unknown option: " + option);
					}
					// if (seen) {
					// err("Option " + option.name() + " already set: " + arg);
					// }

					OptionType type = option.type();

					switch (type) {
					case BOOLEAN: {
						if ("true".equals(valueString))
							value = true;
						else if ("false".equals(valueString))
							value = false;
						else
							err("Expected true or false value: " + arg);
						break;
					}
					case INTEGER: {
						try {
							value = new Integer(valueString);
						} catch (Exception e) {
							err("Expected integer value: " + arg);
						}
						break;
					}
					case DOUBLE: {
						try {
							value = new Double(valueString);
						} catch (Exception e) {
							err("Expected numeric value: " + arg);
						}
						break;
					}
					case STRING: {
						value = valueString;
						break;
					}
					default:
						err("TASS internal error: unknown option type: " + type);
					}
					try {
						option.set(configuration, value);
					} catch (Exception e) {
						err(e.getMessage());
					}
				}
			}
		}

		if (verify) {
			VerifyConfiguration verifyConfiguration = (VerifyConfiguration) configuration;
			File file = verifyConfiguration.sourceFile();

			if (file == null)
				err("No source file specified");
			verifyConfiguration.setModelName(Strings.rootName(file.getName()));
		} else {
			CompareConfiguration compareConfiguration = (CompareConfiguration) configuration;
			File spec = compareConfiguration.specSourceFile();
			File impl = compareConfiguration.implSourceFile();

			if (spec == null)
				err("No specification file specified");
			if (impl == null)
				err("No implementation file specified");
			compareConfiguration.setSpecModelName(Strings.rootName(spec
					.getName()));
			compareConfiguration.setImplModelName(Strings.rootName(impl
					.getName()));
		}
		return configuration;
	}

	public void printUsage() {
		out.println("Usage:");
		out.println("  tass help");
		out.println("  tass verify [options] model.c");
		out.println("  tass compare [options] spec.c impl.c");
		out.println("  tass replay [options] name.trace");
		out.println();
		out.println("Description of sub-commands:");
		out.println("      help: print this message");
		out
				.println("    verify: verify safety properties hold for one program");
		out
				.println("   compare: verify functional equivalence of two programs");
		out.println("    replay: replay trace generated from previous run");
		out.println();
		out.println("Options:");
		for (Option option : Options.options()) {
			out.println(option);
		}
		out.println("-inputVARIABLE=VALUE");
		out
				.println("    specify concrete initial value for input variable VARIABLE");
		out.flush();
	}
}