CIVLCommand.java

package dev.civl.mc.run.common;
import static dev.civl.mc.config.IF.CIVLConstants.CIVLMacroO;
import static dev.civl.mc.config.IF.CIVLConstants.analyzeAbsO;
import static dev.civl.mc.config.IF.CIVLConstants.astO;
import static dev.civl.mc.config.IF.CIVLConstants.collectHeapsO;
import static dev.civl.mc.config.IF.CIVLConstants.collectOutputO;
import static dev.civl.mc.config.IF.CIVLConstants.collectProcessesO;
import static dev.civl.mc.config.IF.CIVLConstants.collectScopesO;
import static dev.civl.mc.config.IF.CIVLConstants.collectSymbolicConstantsO;
import static dev.civl.mc.config.IF.CIVLConstants.debugO;
import static dev.civl.mc.config.IF.CIVLConstants.direct0;
import static dev.civl.mc.config.IF.CIVLConstants.enablePrintfO;
import static dev.civl.mc.config.IF.CIVLConstants.errorBoundO;
import static dev.civl.mc.config.IF.CIVLConstants.guidedO;
import static dev.civl.mc.config.IF.CIVLConstants.idO;
import static dev.civl.mc.config.IF.CIVLConstants.inputO;
import static dev.civl.mc.config.IF.CIVLConstants.intBit;
import static dev.civl.mc.config.IF.CIVLConstants.intOperationTransformer;
import static dev.civl.mc.config.IF.CIVLConstants.loopO;
import static dev.civl.mc.config.IF.CIVLConstants.macroO;
import static dev.civl.mc.config.IF.CIVLConstants.maxProcsO;
import static dev.civl.mc.config.IF.CIVLConstants.maxdepthO;
import static dev.civl.mc.config.IF.CIVLConstants.minO;
import static dev.civl.mc.config.IF.CIVLConstants.mpiContractO;
import static dev.civl.mc.config.IF.CIVLConstants.ompLoopDecompO;
import static dev.civl.mc.config.IF.CIVLConstants.ompNoSimplifyO;
import static dev.civl.mc.config.IF.CIVLConstants.ompOnlySimplifierO;
import static dev.civl.mc.config.IF.CIVLConstants.preprocO;
import static dev.civl.mc.config.IF.CIVLConstants.procBoundO;
import static dev.civl.mc.config.IF.CIVLConstants.quietO;
import static dev.civl.mc.config.IF.CIVLConstants.randomO;
import static dev.civl.mc.config.IF.CIVLConstants.saveStatesO;
import static dev.civl.mc.config.IF.CIVLConstants.seedO;
import static dev.civl.mc.config.IF.CIVLConstants.showAmpleSetO;
import static dev.civl.mc.config.IF.CIVLConstants.showAmpleSetWtStatesO;
import static dev.civl.mc.config.IF.CIVLConstants.showInputVarsO;
import static dev.civl.mc.config.IF.CIVLConstants.showMemoryUnitsO;
import static dev.civl.mc.config.IF.CIVLConstants.showModelO;
import static dev.civl.mc.config.IF.CIVLConstants.showPathConditionO;
import static dev.civl.mc.config.IF.CIVLConstants.showProgramO;
import static dev.civl.mc.config.IF.CIVLConstants.showProverQueriesO;
import static dev.civl.mc.config.IF.CIVLConstants.showQueriesO;
import static dev.civl.mc.config.IF.CIVLConstants.showSavedStatesO;
import static dev.civl.mc.config.IF.CIVLConstants.showStatesO;
import static dev.civl.mc.config.IF.CIVLConstants.showTimeO;
import static dev.civl.mc.config.IF.CIVLConstants.showTransitionsO;
import static dev.civl.mc.config.IF.CIVLConstants.showUnreachedCodeO;
import static dev.civl.mc.config.IF.CIVLConstants.simplifyO;
import static dev.civl.mc.config.IF.CIVLConstants.sliceAnalysisO;
import static dev.civl.mc.config.IF.CIVLConstants.solveO;
import static dev.civl.mc.config.IF.CIVLConstants.statelessPrintfO;
import static dev.civl.mc.config.IF.CIVLConstants.strictCompareO;
import static dev.civl.mc.config.IF.CIVLConstants.svcomp16O;
import static dev.civl.mc.config.IF.CIVLConstants.svcomp17O;
import static dev.civl.mc.config.IF.CIVLConstants.sysIncludePathO;
import static dev.civl.mc.config.IF.CIVLConstants.timeoutO;
import static dev.civl.mc.config.IF.CIVLConstants.traceO;
import static dev.civl.mc.config.IF.CIVLConstants.unpreprocO;
import static dev.civl.mc.config.IF.CIVLConstants.userIncludePathO;
import static dev.civl.mc.config.IF.CIVLConstants.verboseO;
import static dev.civl.mc.config.IF.CIVLConstants.witnessO;
import static dev.civl.mc.config.IF.CIVLConstants.fairO;

import java.io.PrintStream;
import java.util.Collection;
import java.util.SortedMap;
import java.util.TreeMap;

import dev.civl.gmc.Option;
import dev.civl.mc.model.IF.CIVLInternalException;
import dev.civl.mc.model.IF.CIVLProperty;
import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.run.IF.CommandLine;
import dev.civl.mc.run.IF.CommandLine.CommandLineKind;
import dev.civl.mc.run.common.NormalCommandLine.NormalCommandKind;

public class CIVLCommand {

	private static SortedMap<String, Option> showOptions = new TreeMap<>();
	private static SortedMap<String, Option> verifyOptions = new TreeMap<>();
	private static SortedMap<String, Option> compareOptions = new TreeMap<>();
	private static SortedMap<String, Option> replayOptions = new TreeMap<>();
	private static SortedMap<String, Option> runOptions = new TreeMap<>();

	static {
		CIVLCommand.addShowOption(showModelO, verboseO, debugO,
				userIncludePathO, sysIncludePathO, svcomp16O, svcomp17O,
				showInputVarsO, showProgramO, ompNoSimplifyO,
				ompOnlySimplifierO, ompLoopDecompO, macroO, preprocO, astO,
				showTimeO, CIVLMacroO, quietO, unpreprocO, direct0, intBit,
				intOperationTransformer, maxProcsO);
		CIVLCommand.addVerifyOption(errorBoundO, verboseO, debugO,
				userIncludePathO, sysIncludePathO, showTransitionsO,
				showStatesO, showSavedStatesO, showQueriesO, showProverQueriesO,
				inputO, minO, loopO, mpiContractO, maxdepthO, procBoundO,
				saveStatesO, simplifyO, solveO, enablePrintfO, showAmpleSetO,
				showAmpleSetWtStatesO, statelessPrintfO, svcomp16O, svcomp17O,
				showProgramO, showPathConditionO, ompNoSimplifyO,
				ompOnlySimplifierO, ompLoopDecompO, collectProcessesO,
				collectScopesO, collectSymbolicConstantsO, collectHeapsO,
				macroO, preprocO, astO, showTimeO, showMemoryUnitsO, CIVLMacroO,
				showUnreachedCodeO, analyzeAbsO, collectOutputO, timeoutO,
				quietO, unpreprocO, direct0, intBit, intOperationTransformer,
				maxProcsO, fairO);
		CIVLCommand.addVerifyOption(
				CIVLProperty.getAllConfigurableProperties().stream()
						.map(e -> e.getOption()).toArray(Option[]::new));
		CIVLCommand.addCompareOption(errorBoundO, verboseO, debugO,
				userIncludePathO, sysIncludePathO, showTransitionsO,
				showStatesO, showSavedStatesO, showQueriesO, showProverQueriesO,
				inputO, minO, maxdepthO, procBoundO, saveStatesO, simplifyO,
				solveO, enablePrintfO, showAmpleSetO, showAmpleSetWtStatesO,
				statelessPrintfO, svcomp16O, svcomp17O, showProgramO,
				showPathConditionO, ompNoSimplifyO, ompOnlySimplifierO,
				ompLoopDecompO, collectProcessesO, collectScopesO,
				collectHeapsO, macroO, preprocO, astO, showTimeO,
				showMemoryUnitsO, CIVLMacroO, showUnreachedCodeO, analyzeAbsO,
				strictCompareO, timeoutO, quietO, unpreprocO, intBit,
				intOperationTransformer, maxProcsO, fairO);
		CIVLCommand.addCompareOption(CIVLProperty.getAllConfigurableProperties()
				.stream().map(e -> e.getOption()).toArray(Option[]::new));
		CIVLCommand.addReplayOption(showModelO, verboseO, debugO,
				showTransitionsO, showStatesO, showSavedStatesO, showQueriesO,
				showProverQueriesO, idO, traceO, enablePrintfO, showAmpleSetO,
				showAmpleSetWtStatesO, statelessPrintfO, showProgramO,
				showPathConditionO, preprocO, astO, showMemoryUnitsO,
				collectOutputO, CIVLProperty.DIVISION_BY_ZERO.getOption(),
				CIVLProperty.MEMORY_LEAK.getOption(), quietO, unpreprocO,
				svcomp16O, svcomp17O, sliceAnalysisO, witnessO, intBit,
				intOperationTransformer, maxProcsO);
		CIVLCommand.addRunOption(errorBoundO, verboseO, randomO, guidedO, seedO,
				debugO, userIncludePathO, sysIncludePathO, showTransitionsO,
				showStatesO, showSavedStatesO, showQueriesO, showProverQueriesO,
				inputO, maxdepthO, procBoundO, simplifyO, enablePrintfO,
				showAmpleSetO, showAmpleSetWtStatesO, statelessPrintfO,
				svcomp16O, svcomp17O, showProgramO, showPathConditionO,
				ompNoSimplifyO, ompOnlySimplifierO, ompLoopDecompO,
				collectProcessesO, collectScopesO, collectHeapsO, macroO,
				preprocO, astO, showMemoryUnitsO, CIVLMacroO, collectOutputO,
				timeoutO, quietO, unpreprocO, intBit, intOperationTransformer,
				maxProcsO, fairO);
		CIVLCommand.addRunOption(CIVLProperty.getAllConfigurableProperties()
				.stream().map(e -> e.getOption()).toArray(Option[]::new));
	}

	private static void addShowOption(Option... options) {
		for (Option option : options) {
			if (showOptions.containsKey(option.name()))
				throw new CIVLInternalException(
						"Option " + option.name()
								+ " has already been added to show option map.",
						(CIVLSource) null);
			showOptions.put(option.name(), option);
		}
	}

	private static void addVerifyOption(Option... options) {
		for (Option option : options) {
			if (verifyOptions.containsKey(option.name()))
				throw new CIVLInternalException("Option " + option.name()
						+ " has already been added to verify option map.",
						(CIVLSource) null);
			verifyOptions.put(option.name(), option);
		}
	}

	private static void addCompareOption(Option... options) {
		for (Option option : options) {
			if (compareOptions.containsKey(option.name()))
				throw new CIVLInternalException("Option " + option.name()
						+ " has already been added to compare option map.",
						(CIVLSource) null);
			compareOptions.put(option.name(), option);
		}
	}

	private static void addReplayOption(Option... options) {
		for (Option option : options) {
			if (replayOptions.containsKey(option.name()))
				throw new CIVLInternalException("Option " + option.name()
						+ " has already been added to replay option map.",
						(CIVLSource) null);
			replayOptions.put(option.name(), option);
		}
	}

	private static void addRunOption(Option... options) {
		for (Option option : options) {
			if (runOptions.containsKey(option.name()))
				throw new CIVLInternalException(
						"Option " + option.name()
								+ " has already been added to run option map.",
						(CIVLSource) null);
			runOptions.put(option.name(), option);
		}
	}

	public static void printOptionsOfCommand(String command, PrintStream out) {
		switch (command) {
			case CommandLine.COMPARE :
				printOptions(verifyOptions.values(), out);
				break;
			case CommandLine.VERIFY :
				printOptions(verifyOptions.values(), out);
				break;
			case CommandLine.REPLAY :
				printOptions(replayOptions.values(), out);
				break;
			case CommandLine.RUN :
				printOptions(runOptions.values(), out);
				break;
			case CommandLine.SHOW :
				printOptions(showOptions.values(), out);
				break;
			case CommandLine.GUI :
			case CommandLine.CONFIG : // no options for "civl config"
			default :
		}
	}

	private static void printOptions(Collection<Option> options,
			PrintStream out) {
		for (Option option : options)
			out.println(option);
	}

	public static boolean isValid(CommandLine commandLine, Option option) {
		CommandLineKind kind = commandLine.commandLineKind();

		if (kind == CommandLineKind.NORMAL) {
			NormalCommandLine cmd = (NormalCommandLine) commandLine;
			NormalCommandKind cmdKind = cmd.normalCommandKind();

			switch (cmdKind) {
				case SHOW :
					return showOptions.containsKey(option.name());
				case VERIFY :
					return verifyOptions.containsKey(option.name());
				case REPLAY :
				case RUN :
					return replayOptions.containsKey(option.name());
				case CONFIG :
					return false; // no options for "civl config"
				default :
					return false;
			}
		} else {
			return verifyOptions.containsKey(option.name());
		}
	}

	public static SortedMap<String, Option> getReplayOptions() {
		return replayOptions;
	}

	public static SortedMap<String, Option> getRunOptions() {
		return runOptions;
	}

	public static SortedMap<String, Option> getShowOptions() {
		return showOptions;
	}

	public static SortedMap<String, Option> getVerifyOrCompareOptions() {
		return verifyOptions;
	}
}