diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 4329 |
1 files changed, 2173 insertions, 2156 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index a17ff9c7..2dda1dd9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1,2156 +1,2173 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Collections.Specialized;
-using System.IO;
-using System.Linq;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie {
- public class CommandLineOptionEngine
- {
- public readonly string ToolName;
- public readonly string DescriptiveToolName;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(ToolName != null);
- Contract.Invariant(DescriptiveToolName != null);
- Contract.Invariant(this._environment != null);
- Contract.Invariant(cce.NonNullElements(this._files));
- Contract.Invariant(this._fileTimestamp != null);
- }
-
- private string/*!*/ _environment = "";
-
- public string Environment {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return this._environment;
- }
- set {
- Contract.Requires(value != null);
- this._environment = value;
- }
- }
-
- private readonly List<string/*!*/>/*!*/ _files = new List<string/*!*/>();
-
- public IList<string/*!*/>/*!*/ Files {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IList<string>>()));
- Contract.Ensures(Contract.Result<IList<string>>().IsReadOnly);
- return this._files.AsReadOnly();
- }
- }
-
- public bool HelpRequested = false;
- public bool AttrHelpRequested = false;
-
- public CommandLineOptionEngine(string toolName, string descriptiveName) {
- Contract.Requires(toolName != null);
- Contract.Requires(descriptiveName != null);
- ToolName = toolName;
- DescriptiveToolName = descriptiveName;
- }
-
- public virtual string/*!*/ VersionNumber {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return cce.NonNull(cce.NonNull(System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)).FileVersion);
- }
- }
- public virtual string/*!*/ VersionSuffix {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return " version " + VersionNumber + ", Copyright (c) 2003-2014, Microsoft.";
- }
- }
- public virtual string/*!*/ Version {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return DescriptiveToolName + VersionSuffix;
- }
- }
-
- private string/*!*/ _fileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');
-
- public string FileTimestamp {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return this._fileTimestamp;
- }
- set {
- Contract.Requires(value != null);
- this._fileTimestamp = value;
- }
- }
-
- public void ExpandFilename(ref string pattern, string logPrefix, string fileTimestamp) {
- if (pattern != null) {
- pattern = pattern.Replace("@PREFIX@", logPrefix).Replace("@TIME@", fileTimestamp);
- string fn = Files.Count == 0 ? "" : Files[Files.Count - 1];
- fn = fn.Replace('/', '-').Replace('\\', '-');
- pattern = pattern.Replace("@FILE@", fn);
- }
- }
-
- /// <summary>
- /// Process the option and modify "ps" accordingly.
- /// Return true if the option is one that is recognized.
- /// </summary>
- protected virtual bool ParseOption(string name, CommandLineParseState ps) {
- Contract.Requires(name != null);
- Contract.Requires(ps != null);
-
- switch (name) {
- case "help":
- case "?":
- if (ps.ConfirmArgumentCount(0)) {
- HelpRequested = true;
- }
- return true;
- case "attrHelp":
- if (ps.ConfirmArgumentCount(0)) {
- AttrHelpRequested = true;
- }
- return true;
- default:
- break;
- }
- return false; // unrecognized option
- }
-
- protected class CommandLineParseState
- {
- public string s;
- public bool hasColonArgument;
- public readonly string[]/*!*/ args;
- public int i;
- public int nextIndex;
- public bool EncounteredErrors;
- public readonly string ToolName;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(args != null);
- Contract.Invariant(0 <= i && i <= args.Length);
- Contract.Invariant(0 <= nextIndex && nextIndex <= args.Length);
- }
-
-
- public CommandLineParseState(string[] args, string toolName) {
- Contract.Requires(args != null);
- Contract.Requires(Contract.ForAll(0, args.Length, i => args[i] != null));
- Contract.Requires(toolName != null);
- Contract.Ensures(this.args == args);
- this.ToolName = toolName;
- this.s = null; // set later by client
- this.hasColonArgument = false; // set later by client
- this.args = args;
- this.i = 0;
- this.nextIndex = 0; // set later by client
- this.EncounteredErrors = false;
- }
-
- public bool CheckBooleanFlag(string flagName, ref bool flag, bool valueWhenPresent) {
- Contract.Requires(flagName != null);
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- bool flagPresent = false;
-
- if ((s == "/" + flagName || s == "-" + flagName) && ConfirmArgumentCount(0)) {
- flag = valueWhenPresent;
- flagPresent = true;
- }
- return flagPresent;
- }
-
- public bool CheckBooleanFlag(string flagName, ref bool flag) {
- Contract.Requires(flagName != null);
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- return CheckBooleanFlag(flagName, ref flag, true);
- }
-
- /// <summary>
- /// If there is one argument and it is a non-negative integer, then set "arg" to that number and return "true".
- /// Otherwise, emit error message, leave "arg" unchanged, and return "false".
- /// </summary>
- public bool GetNumericArgument(ref int arg) {
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- return GetNumericArgument(ref arg, a => 0 <= a);
- }
-
- /// <summary>
- /// If there is one argument and the filtering predicate holds, then set "arg" to that number and return "true".
- /// Otherwise, emit error message, leave "arg" unchanged, and return "false".
- /// </summary>
- public bool GetNumericArgument(ref int arg, Predicate<int> filter) {
- Contract.Requires(filter != null);
-
- if (this.ConfirmArgumentCount(1)) {
- try {
- Contract.Assume(args[i] != null);
- Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent
- int d = Convert.ToInt32(this.args[this.i]);
- if (filter == null || filter(d)) {
- arg = d;
- return true;
- }
- } catch (System.FormatException) {
- } catch (System.OverflowException) {
- }
- } else {
- return false;
- }
- Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);
- return false;
- }
-
- /// <summary>
- /// If there is one argument and it is a non-negative integer less than "limit",
- /// then set "arg" to that number and return "true".
- /// Otherwise, emit error message, leave "arg" unchanged, and return "false".
- /// </summary>
- public bool GetNumericArgument(ref int arg, int limit) {
- Contract.Requires(this.i < args.Length);
- Contract.Ensures(Math.Min(arg, 0) <= Contract.ValueAtReturn(out arg) && Contract.ValueAtReturn(out arg) < limit);
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- int a = arg;
- if (!GetNumericArgument(ref a)) {
- return false;
- } else if (a < limit) {
- arg = a;
- return true;
- } else {
- Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);
- return false;
- }
- }
-
- /// <summary>
- /// If there is one argument and it is a non-negative real, then set "arg" to that number and return "true".
- /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".
- /// </summary>
- public bool GetNumericArgument(ref double arg) {
- Contract.Ensures(Contract.ValueAtReturn(out arg) >= 0);
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- if (this.ConfirmArgumentCount(1)) {
- try {
- Contract.Assume(args[i] != null);
- Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent
- double d = Convert.ToDouble(this.args[this.i]);
- if (0 <= d) {
- arg = d;
- return true;
- }
- } catch (System.FormatException) {
- } catch (System.OverflowException) {
- }
- } else {
- return false;
- }
- Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);
- return false;
- }
-
- public bool ConfirmArgumentCount(int argCount) {
- Contract.Requires(0 <= argCount);
- //modifies nextIndex, encounteredErrors, Console.Error.*;
- Contract.Ensures(Contract.Result<bool>() == (!(hasColonArgument && argCount != 1) && !(args.Length < i + argCount)));
- if (hasColonArgument && argCount != 1) {
- Error("\"{0}\" cannot take a colon argument", s);
- nextIndex = args.Length;
- return false;
- } else if (args.Length < i + argCount) {
- Error("\"{0}\" expects {1} argument{2}", s, argCount.ToString(), (string)(argCount == 1 ? "" : "s"));
- nextIndex = args.Length;
- return false;
- } else {
- nextIndex = i + argCount;
- return true;
- }
- }
-
- public void Error(string message, params string[] args) {
- Contract.Requires(args != null);
- Contract.Requires(message != null);
- //modifies encounteredErrors, Console.Error.*;
- Console.Error.WriteLine("{0}: Error: {1}", ToolName, String.Format(message, args));
- EncounteredErrors = true;
- }
- }
-
- public virtual void Usage() {
- Console.WriteLine("{0}: usage: {0} [ option ... ] [ filename ... ]", ToolName);
- Console.WriteLine(@" where <option> is one of
-
- ---- General options -------------------------------------------------------
-
- /help this message
- /attrHelp print a message about declaration attributes supported by
- this implementation");
- }
-
- public virtual void AttributeUsage() {
- }
-
- /// <summary>
- /// This method is called after all parsing is done, if no parse errors were encountered.
- /// </summary>
- public virtual void ApplyDefaultOptions() {
- }
-
- /// <summary>
- /// Parses the command-line arguments "args" into the global flag variables. Returns true
- /// if there were no errors.
- /// </summary>
- /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>
- public bool Parse([Captured] string[]/*!*/ args) {
- Contract.Requires(cce.NonNullElements(args));
-
- // save the command line options for the log files
- Environment += "Command Line Options: " + args.Concat(" ");
- args = cce.NonNull((string[])args.Clone()); // the operations performed may mutate the array, so make a copy
- var ps = new CommandLineParseState(args, ToolName);
-
- while (ps.i < args.Length) {
- cce.LoopInvariant(ps.args == args);
- string arg = args[ps.i];
- Contract.Assert(arg != null);
- ps.s = arg.Trim();
-
- bool isOption = ps.s.StartsWith("-") || ps.s.StartsWith("/");
- int colonIndex = ps.s.IndexOf(':');
- if (0 <= colonIndex && isOption) {
- ps.hasColonArgument = true;
- args[ps.i] = ps.s.Substring(colonIndex + 1);
- ps.s = ps.s.Substring(0, colonIndex);
- } else {
- ps.i++;
- ps.hasColonArgument = false;
- }
- ps.nextIndex = ps.i;
-
- if (isOption) {
- if (!ParseOption(ps.s.Substring(1), ps)) {
- if (Path.DirectorySeparatorChar == '/' && ps.s.StartsWith("/"))
- this._files.Add(arg);
- else
- ps.Error("unknown switch: {0}", ps.s);
- }
- } else {
- this._files.Add(arg);
- }
-
- ps.i = ps.nextIndex;
- }
-
- if (HelpRequested) {
- Usage();
- } else if (AttrHelpRequested) {
- AttributeUsage();
- } else if (ps.EncounteredErrors) {
- Console.WriteLine("Use /help for available options");
- }
-
- if (ps.EncounteredErrors) {
- return false;
- } else {
- this.ApplyDefaultOptions();
- return true;
- }
- }
-
- }
-
- /// <summary>
- /// Boogie command-line options (other tools can subclass this class in order to support a
- /// superset of Boogie's options.
- /// </summary>
- public class CommandLineOptions : CommandLineOptionEngine {
-
- public CommandLineOptions()
- : base("Boogie", "Boogie program verifier") {
- }
-
- protected CommandLineOptions(string toolName, string descriptiveName)
- : base(toolName, descriptiveName) {
- Contract.Requires(toolName != null);
- Contract.Requires(descriptiveName != null);
- }
-
- private static CommandLineOptions clo;
- public static CommandLineOptions/*!*/ Clo
- {
- get { return clo; }
- }
-
- public static void Install(CommandLineOptions options) {
- Contract.Requires(options != null);
- clo = options;
- }
-
- public const long Megabyte = 1048576;
-
- // Flags and arguments
-
- public bool RunningBoogieFromCommandLine = false; // "false" means running Boogie from the plug-in
-
- [ContractInvariantMethod]
- void ObjectInvariant2() {
- Contract.Invariant(LogPrefix != null);
- Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3); // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured
- }
-
- public int VerifySnapshots = -1;
- public bool VerifySeparately = false;
- public string PrintFile = null;
- public int PrintUnstructured = 0;
- public bool UseBaseNameForFileName = false;
- public int DoomStrategy = -1;
- public bool DoomRestartTP = false;
- public bool PrintDesugarings = false;
- public string SimplifyLogFilePath = null;
- public bool PrintInstrumented = false;
- public bool InstrumentWithAsserts = false;
- public enum InstrumentationPlaces {
- LoopHeaders,
- Everywhere
- }
- public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders;
- public bool PrintWithUniqueASTIds = false;
- private string XmlSinkFilename = null;
- [Peer]
- public XmlSink XmlSink = null;
- public bool Wait = false;
- public bool Trace = false;
- public bool TraceTimes = false;
- public bool TraceProofObligations = false;
- public bool TraceCachingForTesting
- {
- get
- {
- return TraceCaching == 1 || TraceCaching == 3;
- }
- }
- public bool TraceCachingForBenchmarking
- {
- get
- {
- return TraceCaching == 2 || TraceCaching == 3;
- }
- }
- public bool TraceCachingForDebugging
- {
- get
- {
- return TraceCaching == 3;
- }
- }
- internal int TraceCaching = 0;
- public bool NoResolve = false;
- public bool NoTypecheck = false;
- public bool OverlookBoogieTypeErrors = false;
- public bool Verify = true;
- public bool TraceVerify = false;
- public int /*(0:3)*/ ErrorTrace = 1;
- public bool IntraproceduralInfer = true;
- public bool ContractInfer = false;
- public bool ExplainHoudini = false;
- public bool ReverseHoudiniWorklist = false;
- public bool ConcurrentHoudini = false;
- public bool ModifyTopologicalSorting = false;
- public bool DebugConcurrentHoudini = false;
- public bool HoudiniUseCrossDependencies = false;
- public string StagedHoudini = null;
- public bool DebugStagedHoudini = false;
- public bool StagedHoudiniReachabilityAnalysis = false;
- public bool StagedHoudiniMergeIgnoredAnnotations = false;
- public int StagedHoudiniThreads = 1;
- public string VariableDependenceIgnore = null;
- public string AbstractHoudini = null;
- public bool UseUnsatCoreForContractInfer = false;
- public bool PrintAssignment = false;
- public int InlineDepth = -1;
- public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
- public bool UseUncheckedContracts = false;
- public bool SimplifyLogFileAppend = false;
- public bool SoundnessSmokeTest = false;
- public string Z3ExecutablePath = null;
- public string CVC4ExecutablePath = null;
- public int KInductionDepth = -1;
-
- private string/*!*/ _logPrefix = "";
-
- public string LogPrefix {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return this._logPrefix;
- }
- set {
- Contract.Requires(value != null);
- this._logPrefix = value;
- }
- }
-
- public bool PrettyPrint = true;
-
- public enum ProverWarnings {
- None,
- Stdout,
- Stderr
- }
- public ProverWarnings PrintProverWarnings = ProverWarnings.None;
- public int ProverShutdownLimit = 0;
-
- public enum SubsumptionOption {
- Never,
- NotForQuantifiers,
- Always
- }
- public SubsumptionOption UseSubsumption = SubsumptionOption.Always;
-
- public bool AlwaysAssumeFreeLoopInvariants = false;
-
- public enum ShowEnvironment {
- Never,
- DuringPrint,
- Always
- }
- public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint;
- public bool DontShowLogo = false;
- [ContractInvariantMethod]
- void ObjectInvariant3() {
- Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);
- Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);
- Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);
- Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
- Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
- Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);
- Contract.Invariant(cce.NonNullElements(this.proverOptions));
- }
-
- public int LoopUnrollCount = -1; // -1 means don't unroll loops
- public bool SoundLoopUnrolling = false;
- public int LoopFrameConditions = -1; // -1 means not specified -- this will be replaced by the "implications" section below
- public int ModifiesDefault = 5;
- public bool LocalModifiesChecks = true;
- public bool NoVerifyByDefault = false;
- public enum OwnershipModelOption {
- Standard,
- Experimental,
- Trivial
- }
- public OwnershipModelOption OwnershipModelEncoding = OwnershipModelOption.Standard;
- public int PrintErrorModel = 0;
- public string PrintErrorModelFile = null;
- public string/*?*/ ModelViewFile = null;
- public int EnhancedErrorMessages = 0;
- public string PrintCFGPrefix = null;
- public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
- public bool UseArrayTheory = false;
- public bool UseSmtOutputFormat = false;
- public bool WeakArrayTheory = false;
- public bool UseLabels = true;
- public bool RunDiagnosticsOnTimeout = false;
- public bool TraceDiagnosticsOnTimeout = false;
- public int TimeLimitPerAssertionInPercent = 20;
- public bool SIBoolControlVC = false;
- public bool MonomorphicArrays {
- get {
- return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;
- }
- }
- public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
- public bool DoModSetAnalysis = false;
- public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
- private int /*0..9*/stepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
-
- public int StepsBeforeWidening
- {
- get
- {
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= 9);
- return this.stepsBeforeWidening;
- }
- set
- {
- Contract.Requires(0 <= value && value <= 9);
- this.stepsBeforeWidening = value;
- }
- }
-
- public string OwickiGriesDesugaredOutputFile = null;
- public bool TrustAtomicityTypes = false;
- public bool TrustNonInterference = false;
- public int TrustLayersUpto = -1;
- public int TrustLayersDownto = int.MaxValue;
-
- public enum VCVariety {
- Structured,
- Block,
- Local,
- BlockNested,
- BlockReach,
- BlockNestedReach,
- Dag,
- DagIterative,
- Doomed,
- Unspecified
- }
- public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed
-
- public bool RemoveEmptyBlocks = true;
- public bool CoalesceBlocks = true;
- public bool PruneInfeasibleEdges = true;
-
- [Rep]
- public ProverFactory TheProverFactory;
- public string ProverName;
- [Peer]
- private List<string> proverOptions = new List<string>();
-
- public IEnumerable<string> ProverOptions
- {
- set
- {
- Contract.Requires(cce.NonNullElements(value));
-
- this.proverOptions = new List<string>(value);
- }
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));
-
- foreach (string s in this.proverOptions)
- yield return s;
- }
- }
-
- [Obsolete("use the setter for 'ProverOptions' directly")]
- public void AddProverOption(string option)
- {
- Contract.Requires(option != null);
-
- this.ProverOptions = this.ProverOptions.Concat1(option);
- }
-
- [Obsolete("use the setter for 'ProverOptions' directly")]
- public void RemoveAllProverOptions(Predicate<string> match)
- {
- this.ProverOptions = this.ProverOptions.Where(s => !match(s));
- }
-
- private int bracketIdsInVC = -1; // -1 - not specified, 0 - no, 1 - yes
-
- public int BracketIdsInVC {
- get {
- Contract.Ensures(-1 <= Contract.Result<int>() && Contract.Result<int>() <= 1);
- return this.bracketIdsInVC;
- }
- set {
- Contract.Requires(-1 <= value && value <= 1);
- this.bracketIdsInVC = value;
- }
- }
-
- public bool CausalImplies = false;
-
- public int SimplifyProverMatchDepth = -1; // -1 means not specified
- public int ProverKillTime = -1; // -1 means not specified
- public int SmokeTimeout = 10; // default to 10s
- public int ProverCCLimit = 5;
- public bool z3AtFlag = true;
- public bool RestartProverPerVC = false;
-
- public double VcsMaxCost = 1.0;
- public double VcsPathJoinMult = 0.8;
- public double VcsPathCostMult = 1.0;
- public double VcsAssumeMult = 0.01;
- public double VcsPathSplitMult = 0.5; // 0.5-always, 2-rarely do path splitting
- public int VcsMaxSplits = 1;
- public int VcsMaxKeepGoingSplits = 1;
- public int VcsFinalAssertTimeout = 30;
- public int VcsKeepGoingTimeout = 1;
- public int VcsCores = 1;
- public bool VcsDumpSplits = false;
-
- public bool DebugRefuted = false;
-
- public XmlSink XmlRefuted {
- get {
- if (DebugRefuted)
- return XmlSink;
- else
- return null;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant4() {
- Contract.Invariant(cce.NonNullElements(this.z3Options));
- Contract.Invariant(0 <= Z3lets && Z3lets < 4);
- }
-
- [Peer]
- private List<string> z3Options = new List<string>();
-
- public IEnumerable<string> Z3Options
- {
- get
- {
- Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
- foreach (string s in z3Options)
- yield return s;
- }
- }
-
- public void AddZ3Option(string option)
- {
- Contract.Requires(option != null);
- this.z3Options.Add(option);
- }
-
- public bool Z3types = false;
- public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
-
-
- // Maximum amount of virtual memory (in bytes) for the prover to use
- //
- // Non-positive number indicates unbounded.
- public long MaxProverMemory = 100 * Megabyte;
-
- // Minimum number of prover calls before restart
- public int MinNumOfProverCalls = 5;
-
- public enum PlatformType {
- notSpecified,
- v1,
- v11,
- v2,
- cli1
- }
- public PlatformType TargetPlatform;
- public string TargetPlatformLocation;
- public string StandardLibraryLocation;
-
- // whether procedure inlining is enabled at call sites.
- public enum Inlining {
- None,
- Assert,
- Assume,
- Spec
- };
- public Inlining ProcedureInlining = Inlining.Assume;
- public bool PrintInlined = false;
- public bool ExtractLoops = false;
- public bool DeterministicExtractLoops = false;
- public string SecureVcGen = null;
- public int StratifiedInlining = 0;
- public string FixedPointEngine = null;
- public int StratifiedInliningOption = 0;
- public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
- public int StratifiedInliningVerbose = 0; // verbosity level
- public int RecursionBound = 500;
- public bool NonUniformUnfolding = false;
- public int StackDepthBound = 0;
- public string inferLeastForUnsat = null;
-
- // Inference mode for fixed point engine
- public enum FixedPointInferenceMode {
- Corral,
- OldCorral,
- Flat,
- Procedure,
- Call
- };
- public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;
-
- public string PrintFixedPoint = null;
-
- public string PrintConjectures = null;
-
- public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)
-
- public enum TypeEncoding {
- None,
- Predicates,
- Arguments,
- Monomorphic
- };
- public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;
-
- public bool Monomorphize = false;
-
- public bool ReflectAdd = false;
-
- public int LiveVariableAnalysis = 1;
-
- // Static constructor
- static CommandLineOptions() {
- if (System.Type.GetType("Mono.Runtime") == null) { // MONO
- TraceListenerCollection/*!*/ dbl = Debug.Listeners;
- Contract.Assert(dbl != null);
- Contract.Assume(cce.IsPeerConsistent(dbl)); // hangs off static field
- dbl.Add(new DefaultTraceListener());
- }
- }
-
- public IEnumerable<string/*!*/> ProcsToCheck {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>>(), true));
- return this.procsToCheck != null ? this.procsToCheck.AsEnumerable() : null;
- }
- }
-
- private List<string/*!*/> procsToCheck = null; // null means "no restriction"
-
- [ContractInvariantMethod]
- void ObjectInvariant5() {
- Contract.Invariant(cce.NonNullElements(this.procsToCheck, true));
- Contract.Invariant(Ai != null);
- }
-
- public class AiFlags {
- public bool J_Trivial = false;
- public bool J_Intervals = false;
- public bool DebugStatistics = false;
- }
- public readonly AiFlags/*!*/ Ai = new AiFlags();
-
- public class ConcurrentHoudiniOptions
- {
- public List<string> ProverOptions = new List<string>();
- public int ProverCCLimit = 5;
- public bool DisableLoopInvEntryAssert = false;
- public bool DisableLoopInvMaintainedAssert = false;
- public bool ModifyTopologicalSorting = false;
- }
- public List<ConcurrentHoudiniOptions> Cho = new List<ConcurrentHoudiniOptions>();
-
- protected override bool ParseOption(string name, CommandLineOptionEngine.CommandLineParseState ps) {
- var args = ps.args; // convenient synonym
- switch (name) {
- case "infer":
- if (ps.ConfirmArgumentCount(1)) {
- foreach (char c in cce.NonNull(args[ps.i])) {
- switch (c) {
- case 't':
- Ai.J_Trivial = true;
- UseAbstractInterpretation = true;
- break;
- case 'j':
- Ai.J_Intervals = true;
- UseAbstractInterpretation = true;
- break;
- case 's':
- Ai.DebugStatistics = true;
- UseAbstractInterpretation = true;
- break;
- case '0':
- case '1':
- case '2':
- case '3':
- case '4':
- case '5':
- case '6':
- case '7':
- case '8':
- case '9':
- StepsBeforeWidening = (int)char.GetNumericValue(c);
- break;
- default:
- ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s);
- break;
- }
- }
- }
- return true;
-
- case "noinfer":
- if (ps.ConfirmArgumentCount(0)) {
- UseAbstractInterpretation = false;
- }
- return true;
-
- case "break":
- case "launch":
- if (ps.ConfirmArgumentCount(0)) {
- System.Diagnostics.Debugger.Launch();
- }
- return true;
-
- case "proc":
- if (this.procsToCheck == null) {
- this.procsToCheck = new List<string/*!*/>();
- }
- if (ps.ConfirmArgumentCount(1)) {
- this.procsToCheck.Add(cce.NonNull(args[ps.i]));
- }
- return true;
-
- case "xml":
- if (ps.ConfirmArgumentCount(1)) {
- XmlSinkFilename = args[ps.i];
- }
- return true;
-
- case "print":
- if (ps.ConfirmArgumentCount(1)) {
- PrintFile = args[ps.i];
- }
- return true;
-
- case "pretty":
- int val = 1;
- if (ps.GetNumericArgument(ref val, 2)) {
- PrettyPrint = val == 1;
- }
- return true;
-
- case "OwickiGries":
- if (ps.ConfirmArgumentCount(1)) {
- OwickiGriesDesugaredOutputFile = args[ps.i];
- }
- return true;
-
- case "trustLayersUpto":
- if (ps.ConfirmArgumentCount(1))
- {
- ps.GetNumericArgument(ref TrustLayersUpto);
- }
- return true;
-
- case "trustLayersDownto":
- if (ps.ConfirmArgumentCount(1))
- {
- ps.GetNumericArgument(ref TrustLayersDownto);
- }
- return true;
-
- case "proverLog":
- if (ps.ConfirmArgumentCount(1)) {
- SimplifyLogFilePath = args[ps.i];
- }
- return true;
-
- case "logPrefix":
- if (ps.ConfirmArgumentCount(1)) {
- string s = cce.NonNull(args[ps.i]);
- LogPrefix += s.Replace('/', '-').Replace('\\', '-');
- }
- return true;
-
- case "proverShutdownLimit":
- ps.GetNumericArgument(ref ProverShutdownLimit);
- return true;
-
- case "errorTrace":
- ps.GetNumericArgument(ref ErrorTrace, 3);
- return true;
-
- case "proverWarnings": {
- int pw = 0;
- if (ps.GetNumericArgument(ref pw, 3)) {
- switch (pw) {
- case 0:
- PrintProverWarnings = ProverWarnings.None;
- break;
- case 1:
- PrintProverWarnings = ProverWarnings.Stdout;
- break;
- case 2:
- PrintProverWarnings = ProverWarnings.Stderr;
- break;
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // postcondition of GetNumericArgument guarantees that we don't get here
- }
- }
- return true;
- }
-
- case "env": {
- int e = 0;
- if (ps.GetNumericArgument(ref e, 3)) {
- switch (e) {
- case 0:
- ShowEnv = ShowEnvironment.Never;
- break;
- case 1:
- ShowEnv = ShowEnvironment.DuringPrint;
- break;
- case 2:
- ShowEnv = ShowEnvironment.Always;
- break;
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // postcondition of GetNumericArgument guarantees that we don't get here
- }
- }
- return true;
- }
-
- case "loopUnroll":
- ps.GetNumericArgument(ref LoopUnrollCount);
- return true;
-
- case "printModel":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "0":
- PrintErrorModel = 0;
- break;
- case "1":
- PrintErrorModel = 1;
- break;
- case "2":
- PrintErrorModel = 2;
- break;
- case "4":
- PrintErrorModel = 4;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
-
- case "mv":
- if (ps.ConfirmArgumentCount(1)) {
- ModelViewFile = args[ps.i];
- }
- return true;
-
- case "printModelToFile":
- if (ps.ConfirmArgumentCount(1)) {
- PrintErrorModelFile = args[ps.i];
- }
- return true;
-
- case "enhancedErrorMessages":
- ps.GetNumericArgument(ref EnhancedErrorMessages, 2);
- return true;
-
- case "printCFG":
- if (ps.ConfirmArgumentCount(1)) {
- PrintCFGPrefix = args[ps.i];
- }
- return true;
-
- case "inlineDepth":
- ps.GetNumericArgument(ref InlineDepth);
- return true;
-
- case "subsumption": {
- int s = 0;
- if (ps.GetNumericArgument(ref s, 3)) {
- switch (s) {
- case 0:
- UseSubsumption = SubsumptionOption.Never;
- break;
- case 1:
- UseSubsumption = SubsumptionOption.NotForQuantifiers;
- break;
- case 2:
- UseSubsumption = SubsumptionOption.Always;
- break;
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // postcondition of GetNumericArgument guarantees that we don't get here
- }
- }
- return true;
- }
-
- case "liveVariableAnalysis": {
- int lva = 0;
- if (ps.GetNumericArgument(ref lva, 3)) {
- LiveVariableAnalysis = lva;
- }
- return true;
- }
-
- case "removeEmptyBlocks": {
- int reb = 0;
- if (ps.GetNumericArgument(ref reb, 2)) {
- RemoveEmptyBlocks = reb == 1;
- }
- return true;
- }
-
- case "coalesceBlocks": {
- int cb = 0;
- if (ps.GetNumericArgument(ref cb, 2)) {
- CoalesceBlocks = cb == 1;
- }
- return true;
- }
-
- case "noPruneInfeasibleEdges": {
- if (ps.ConfirmArgumentCount(0)) {
- PruneInfeasibleEdges = false;
- }
- return true;
- }
-
- case "stagedHoudini": {
- if (ps.ConfirmArgumentCount(1)) {
- if(args[ps.i] == "COARSE" ||
- args[ps.i] == "FINE" ||
- args[ps.i] == "BALANCED") {
- StagedHoudini = args[ps.i];
- } else {
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- }
- }
- return true;
- }
-
- case "stagedHoudiniThreads": {
- ps.GetNumericArgument(ref StagedHoudiniThreads);
- return true;
- }
-
- case "stagedHoudiniReachabilityAnalysis": {
- if (ps.ConfirmArgumentCount(0)) {
- StagedHoudiniReachabilityAnalysis = true;
- }
- return true;
- }
-
- case "stagedHoudiniMergeIgnoredAnnotations": {
- if (ps.ConfirmArgumentCount(0)) {
- StagedHoudiniMergeIgnoredAnnotations = true;
- }
- return true;
- }
-
- case "debugStagedHoudini": {
- if (ps.ConfirmArgumentCount(0)) {
- DebugStagedHoudini = true;
- }
- return true;
- }
-
- case "variableDependenceIgnore": {
- if (ps.ConfirmArgumentCount(1)) {
- VariableDependenceIgnore = args[ps.i];
- }
- return true;
- }
-
- case "abstractHoudini":
- {
- if (ps.ConfirmArgumentCount(1))
- {
- AbstractHoudini = args[ps.i];
- }
- return true;
- }
- case "vc":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "s":
- case "structured":
- vcVariety = VCVariety.Structured;
- break;
- case "b":
- case "block":
- vcVariety = VCVariety.Block;
- break;
- case "l":
- case "local":
- vcVariety = VCVariety.Local;
- break;
- case "n":
- case "nested":
- vcVariety = VCVariety.BlockNested;
- break;
- case "m":
- vcVariety = VCVariety.BlockNestedReach;
- break;
- case "r":
- vcVariety = VCVariety.BlockReach;
- break;
- case "d":
- case "dag":
- vcVariety = VCVariety.Dag;
- break;
- case "i":
- vcVariety = VCVariety.DagIterative;
- break;
- case "doomed":
- vcVariety = VCVariety.Doomed;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
-
- case "prover":
- if (ps.ConfirmArgumentCount(1)) {
- TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i]));
- ProverName = cce.NonNull(args[ps.i]).ToUpper();
- }
- return true;
-
- case "p":
- case "proverOpt":
- if (ps.ConfirmArgumentCount(1)) {
- ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i]));
- }
- return true;
-
- case "DoomStrategy":
- ps.GetNumericArgument(ref DoomStrategy);
- return true;
-
- case "DoomRestartTP":
- if (ps.ConfirmArgumentCount(0)) {
- DoomRestartTP = true;
- }
- return true;
-
- case "extractLoops":
- if (ps.ConfirmArgumentCount(0)) {
- ExtractLoops = true;
- }
- return true;
-
- case "deterministicExtractLoops":
- if (ps.ConfirmArgumentCount(0)) {
- DeterministicExtractLoops = true;
- }
- return true;
-
- case "inline":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "none":
- ProcedureInlining = Inlining.None;
- break;
- case "assert":
- ProcedureInlining = Inlining.Assert;
- break;
- case "assume":
- ProcedureInlining = Inlining.Assume;
- break;
- case "spec":
- ProcedureInlining = Inlining.Spec;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
- case "secure":
- if (ps.ConfirmArgumentCount(1))
- SecureVcGen = args[ps.i];
- return true;
- case "stratifiedInline":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "0":
- StratifiedInlining = 0;
- break;
- case "1":
- StratifiedInlining = 1;
- break;
- default:
- StratifiedInlining = Int32.Parse(cce.NonNull(args[ps.i]));
- //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
- case "fixedPointEngine":
- if (ps.ConfirmArgumentCount(1))
- {
- FixedPointEngine = args[ps.i];
- }
- return true;
- case "fixedPointInfer":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "corral":
- FixedPointMode = FixedPointInferenceMode.Corral;
- break;
- case "oldCorral":
- FixedPointMode = FixedPointInferenceMode.OldCorral;
- break;
- case "flat":
- FixedPointMode = FixedPointInferenceMode.Flat;
- break;
- case "procedure":
- FixedPointMode = FixedPointInferenceMode.Procedure;
- break;
- case "call":
- FixedPointMode = FixedPointInferenceMode.Call;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
- case "printFixedPoint":
- if (ps.ConfirmArgumentCount(1))
- {
- PrintFixedPoint = args[ps.i];
- }
- return true;
- case "printConjectures":
- if (ps.ConfirmArgumentCount(1))
- {
- PrintConjectures = args[ps.i];
- }
- return true;
- case "siVerbose":
- if (ps.ConfirmArgumentCount(1)) {
- StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));
- }
- return true;
- case "recursionBound":
- if (ps.ConfirmArgumentCount(1)) {
- RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));
- }
- return true;
- case "stackDepthBound":
- if (ps.ConfirmArgumentCount(1))
- {
- StackDepthBound = Int32.Parse(cce.NonNull(args[ps.i]));
- }
- return true;
- case "stratifiedInlineOption":
- if (ps.ConfirmArgumentCount(1)) {
- StratifiedInliningOption = Int32.Parse(cce.NonNull(args[ps.i]));
- }
- return true;
-
- case "inferLeastForUnsat":
- if (ps.ConfirmArgumentCount(1)) {
- inferLeastForUnsat = args[ps.i];
- }
- return true;
-
- case "typeEncoding":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "n":
- case "none":
- TypeEncodingMethod = TypeEncoding.None;
- break;
- case "p":
- case "predicates":
- TypeEncodingMethod = TypeEncoding.Predicates;
- break;
- case "a":
- case "arguments":
- TypeEncodingMethod = TypeEncoding.Arguments;
- break;
- case "m":
- case "monomorphic":
- TypeEncodingMethod = TypeEncoding.Monomorphic;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
-
- case "instrumentInfer":
- if (ps.ConfirmArgumentCount(1)) {
- switch (args[ps.i]) {
- case "e":
- InstrumentInfer = InstrumentationPlaces.Everywhere;
- break;
- case "h":
- InstrumentInfer = InstrumentationPlaces.LoopHeaders;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- return true;
-
- case "concurrentHoudini":
- if (ps.ConfirmArgumentCount(0)) {
- ConcurrentHoudini = true;
- }
- return true;
-
- case "modifyTopologicalSorting":
- if (ps.ConfirmArgumentCount(0)) {
- ModifyTopologicalSorting = true;
- }
- return true;
-
- case "debugConcurrentHoudini":
- if (ps.ConfirmArgumentCount(0)) {
- DebugConcurrentHoudini = true;
- }
- return true;
-
- case "vcBrackets":
- ps.GetNumericArgument(ref bracketIdsInVC, 2);
- return true;
-
- case "proverMemoryLimit": {
- int d = 0;
- if (ps.GetNumericArgument(ref d)) {
- MaxProverMemory = d * Megabyte;
- }
- return true;
- }
-
- case "vcsMaxCost":
- ps.GetNumericArgument(ref VcsMaxCost);
- return true;
-
- case "vcsPathJoinMult":
- ps.GetNumericArgument(ref VcsPathJoinMult);
- return true;
-
- case "vcsPathCostMult":
- ps.GetNumericArgument(ref VcsPathCostMult);
- return true;
-
- case "vcsAssumeMult":
- ps.GetNumericArgument(ref VcsAssumeMult);
- return true;
-
- case "vcsPathSplitMult":
- ps.GetNumericArgument(ref VcsPathSplitMult);
- return true;
-
- case "vcsMaxSplits":
- ps.GetNumericArgument(ref VcsMaxSplits);
- return true;
-
- case "vcsMaxKeepGoingSplits":
- ps.GetNumericArgument(ref VcsMaxKeepGoingSplits);
- return true;
-
- case "vcsFinalAssertTimeout":
- ps.GetNumericArgument(ref VcsFinalAssertTimeout);
- return true;
-
- case "vcsKeepGoingTimeout":
- ps.GetNumericArgument(ref VcsKeepGoingTimeout);
- return true;
-
- case "vcsCores":
- ps.GetNumericArgument(ref VcsCores, a => 1 <= a);
- return true;
-
- case "vcsLoad":
- double load = 0.0;
- if (ps.GetNumericArgument(ref load)) {
- if (3.0 <= load) {
- ps.Error("surprisingly high load specified; got {0}, expected nothing above 3.0", load.ToString());
- load = 3.0;
- }
- int p = (int)Math.Round(System.Environment.ProcessorCount * load);
- VcsCores = p < 1 ? 1 : p;
- }
- return true;
-
- case "simplifyMatchDepth":
- ps.GetNumericArgument(ref SimplifyProverMatchDepth);
- return true;
-
- case "timeLimit":
- ps.GetNumericArgument(ref ProverKillTime);
- return true;
-
- case "timeLimitPerAssertionInPercent":
- ps.GetNumericArgument(ref TimeLimitPerAssertionInPercent, a => 0 < a);
- return true;
-
- case "smokeTimeout":
- ps.GetNumericArgument(ref SmokeTimeout);
- return true;
-
- case "errorLimit":
- ps.GetNumericArgument(ref ProverCCLimit);
- return true;
-
- case "verifySnapshots":
- ps.GetNumericArgument(ref VerifySnapshots, 4);
- return true;
-
- case "traceCaching":
- ps.GetNumericArgument(ref TraceCaching, 4);
- return true;
-
- case "useSmtOutputFormat": {
- if (ps.ConfirmArgumentCount(0)) {
- UseSmtOutputFormat = true;
- }
- return true;
- }
-
- case "z3opt":
- if (ps.ConfirmArgumentCount(1)) {
- AddZ3Option(cce.NonNull(args[ps.i]));
- }
- return true;
-
- case "z3lets":
- ps.GetNumericArgument(ref Z3lets, 4);
- return true;
-
- case "platform":
- if (ps.ConfirmArgumentCount(1)) {
- StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]);
- if (platformOptions != null && platformOptions.Count > 0) {
- try {
- this.TargetPlatform = (PlatformType)cce.NonNull(Enum.Parse(typeof(PlatformType), cce.NonNull(platformOptions[0])));
- } catch {
- ps.Error("Bad /platform type '{0}'", platformOptions[0]);
- break;
- }
- if (platformOptions.Count > 1) {
- this.TargetPlatformLocation = platformOptions[1];
- if (!Directory.Exists(platformOptions[1])) {
- ps.Error("/platform directory '{0}' does not exist", platformOptions[1]);
- break;
- }
- }
- }
- }
- return true;
-
- case "z3exe":
- if (ps.ConfirmArgumentCount(1)) {
- Z3ExecutablePath = args[ps.i];
- }
- return true;
-
- case "cvc4exe":
- if (ps.ConfirmArgumentCount(1)) {
- CVC4ExecutablePath = args[ps.i];
- }
- return true;
-
- case "kInductionDepth":
- ps.GetNumericArgument(ref KInductionDepth);
- return true;
-
- default:
- bool optionValue = false;
- if (ps.CheckBooleanFlag("printUnstructured", ref optionValue)) {
- PrintUnstructured = optionValue ? 1 : 0;
- return true;
- }
-
- if (ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) ||
- ps.CheckBooleanFlag("printInstrumented", ref PrintInstrumented) ||
- ps.CheckBooleanFlag("printWithUniqueIds", ref PrintWithUniqueASTIds) ||
- ps.CheckBooleanFlag("wait", ref Wait) ||
- ps.CheckBooleanFlag("trace", ref Trace) ||
- ps.CheckBooleanFlag("traceTimes", ref TraceTimes) ||
- ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) ||
- ps.CheckBooleanFlag("noResolve", ref NoResolve) ||
- ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||
- ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) ||
- ps.CheckBooleanFlag("noVerify", ref Verify, false) ||
- ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||
- ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||
- ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||
- ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) ||
- ps.CheckBooleanFlag("soundLoopUnrolling", ref SoundLoopUnrolling) ||
- ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) ||
- ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) ||
- ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) ||
- ps.CheckBooleanFlag("printInlined", ref PrintInlined) ||
- ps.CheckBooleanFlag("smoke", ref SoundnessSmokeTest) ||
- ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) ||
- ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) ||
- ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||
- ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
- ps.CheckBooleanFlag("z3types", ref Z3types) ||
- ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
- ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
- ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
- ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) ||
- ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
- ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
- ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) ||
- ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", ref TraceDiagnosticsOnTimeout) ||
- ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||
- ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
- ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||
- ps.CheckBooleanFlag("reverseHoudiniWorklist", ref ReverseHoudiniWorklist) ||
- ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
- ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
- ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
- ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
- ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
- ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||
- ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
- ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
- ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName)
- ) {
- // one of the boolean flags matched
- return true;
- }
- break;
- }
-
- return base.ParseOption(name, ps); // defer to superclass
- }
-
- public override void ApplyDefaultOptions() {
- Contract.Ensures(TheProverFactory != null);
- Contract.Ensures(vcVariety != VCVariety.Unspecified);
-
- base.ApplyDefaultOptions();
-
- // expand macros in filenames, now that LogPrefix is fully determined
- ExpandFilename(ref XmlSinkFilename, LogPrefix, FileTimestamp);
- ExpandFilename(ref PrintFile, LogPrefix, FileTimestamp);
- ExpandFilename(ref SimplifyLogFilePath, LogPrefix, FileTimestamp);
- ExpandFilename(ref PrintErrorModelFile, LogPrefix, FileTimestamp);
-
- Contract.Assume(XmlSink == null); // XmlSink is to be set here
- if (XmlSinkFilename != null) {
- XmlSink = new XmlSink(XmlSinkFilename);
- }
-
- if (TheProverFactory == null) {
- TheProverFactory = ProverFactory.Load("SMTLib");
- ProverName = "SMTLib".ToUpper();
- }
-
- var proverOpts = TheProverFactory.BlankProverOptions();
- proverOpts.Parse(ProverOptions);
- if (!TheProverFactory.SupportsLabels(proverOpts)) {
- UseLabels = false;
- }
-
- if (vcVariety == VCVariety.Unspecified) {
- vcVariety = TheProverFactory.DefaultVCVariety;
- }
-
- if (UseArrayTheory) {
- Monomorphize = true;
- }
-
- if (inferLeastForUnsat != null) {
- StratifiedInlining = 1;
- }
-
- if (StratifiedInlining > 0) {
- TypeEncodingMethod = TypeEncoding.Monomorphic;
- UseArrayTheory = true;
- UseAbstractInterpretation = false;
- MaxProverMemory = 0; // no max: avoids restarts
- if (ProverName == "Z3API" || ProverName == "SMTLIB") {
- ProverCCLimit = 1;
- }
- if (UseProverEvaluate)
- StratifiedInliningWithoutModels = true;
- }
-
- if (Trace) {
- BoogieDebug.DoPrinting = true; // reuse the -trace option for debug printing
- }
- }
-
-
-
- public bool UserWantsToCheckRoutine(string methodFullname) {
- Contract.Requires(methodFullname != null);
- if (ProcsToCheck == null) {
- // no preference
- return true;
- }
- return ProcsToCheck.Any(s => 0 <= methodFullname.IndexOf(s));
- }
-
- public virtual StringCollection ParseNamedArgumentList(string argList) {
- if (argList == null || argList.Length == 0)
- return null;
- StringCollection result = new StringCollection();
- int i = 0;
- for (int n = argList.Length; i < n; ) {
- cce.LoopInvariant(0 <= i);
- int separatorIndex = this.GetArgumentSeparatorIndex(argList, i);
- if (separatorIndex > i) {
- result.Add(argList.Substring(i, separatorIndex - i));
- i = separatorIndex + 1;
- continue;
- }
- result.Add(argList.Substring(i));
- break;
- }
- return result;
- }
- public int GetArgumentSeparatorIndex(string argList, int startIndex) {
- Contract.Requires(argList != null);
- Contract.Requires(0 <= startIndex && startIndex <= argList.Length);
- Contract.Ensures(Contract.Result<int>() < argList.Length);
- int commaIndex = argList.IndexOf(",", startIndex);
- int semicolonIndex = argList.IndexOf(";", startIndex);
- if (commaIndex == -1)
- return semicolonIndex;
- if (semicolonIndex == -1)
- return commaIndex;
- if (commaIndex < semicolonIndex)
- return commaIndex;
- return semicolonIndex;
- }
-
- public override void AttributeUsage() {
- Console.WriteLine(
-@"Boogie: The following attributes are supported by this implementation.
-
- ---- On top-level declarations ---------------------------------------------
-
- {:ignore}
- Ignore the declaration (after checking for duplicate names).
-
- {:extern}
- If two top-level declarations introduce the same name (for example, two
- constants with the same name or two procedures with the same name), then
- Boogie usually produces an error message. However, if at least one of
- the declarations is declared with :extern, one of the declarations is
- ignored. If both declarations are :extern, Boogie arbitrarily chooses
- one of them to keep; otherwise, Boogie ignore the :extern declaration
- and keeps the other.
-
- {:checksum <string>}
- Attach a checksum to be used for verification result caching.
-
- ---- On implementations and procedures -------------------------------------
-
- {:inline N}
- Inline given procedure (can be also used on implementation).
- N should be a non-negative number and represents the inlining depth.
- With /inline:assume call is replaced with ""assume false"" once inlining depth is reached.
- With /inline:assert call is replaced with ""assert false"" once inlining depth is reached.
- With /inline:spec call is left as is once inlining depth is reached.
- With the above three options, methods with the attribute {:inline N} are not verified.
- With /inline:none the entire attribute is ignored.
-
- {:verify false}
- Skip verification of an implementation.
-
- {:vcs_max_cost N}
- {:vcs_max_splits N}
- {:vcs_max_keep_going_splits N}
- Per-implementation versions of
- /vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits.
-
- {:selective_checking true}
- Turn all asserts into assumes except for the ones reachable from
- assumptions marked with the attribute {:start_checking_here}.
- Thus, ""assume {:start_checking_here} something;"" becomes an inverse
- of ""assume false;"": the first one disables all verification before
- it, and the second one disables all verification after.
-
- {:priority N}
- Assign a positive priority 'N' to an implementation to control the order
- in which implementations are verified (default: N = 1).
-
- {:id <string>}
- Assign a unique ID to an implementation to be used for verification
- result caching (default: ""<impl. name>:0"").
-
- {:timeLimit N}
- Set the time limit for a given implementation.
-
- ---- On functions ----------------------------------------------------------
-
- {:builtin ""spec""}
- {:bvbuiltin ""spec""}
- Rewrite the function to built-in prover function symbol 'fn'.
-
- {:inline}
- {:inline true}
- Expand function according to its definition before going to the prover.
-
- {:never_pattern true}
- Terms starting with this function symbol will never be
- automatically selected as patterns. It does not prevent them
- from being used inside the triggers, and does not affect explicit
- trigger annotations. Internally it works by adding {:nopats ...}
- annotations to quantifiers.
-
- {:identity}
- {:identity true}
- If the function has 1 argument and the use of it has type X->X for
- some X, then the abstract interpreter will treat the function as an
- identity function. Note, the abstract interpreter trusts the
- attribute--it does not try to verify that the function really is an
- identity function.
-
- ---- On variables ----------------------------------------------------------
-
- {:existential true}
- Marks a global Boolean variable as existentially quantified. If
- used in combination with option /contractInfer Boogie will check
- whether there exists a Boolean assignment to the existentials
- that makes all verification conditions valid. Without option
- /contractInfer the attribute is ignored.
-
- ---- On assert statements --------------------------------------------------
-
- {:subsumption n}
- Overrides the /subsumption command-line setting for this assertion.
-
- {:split_here}
- Verifies code leading to this point and code leading from this point
- to the next split_here as separate pieces. May help with timeouts.
- May also occasionally double-report errors.
-
- ---- The end ---------------------------------------------------------------
-");
- }
-
- public override void Usage() {
- Console.WriteLine(@"
- /nologo suppress printing of version number, copyright message
- /env:<n> print command line arguments
- 0 - never, 1 (default) - during BPL print and prover log,
- 2 - like 1 and also to standard output
- /wait await Enter from keyboard before terminating program
- /xml:<file> also produce output in XML format to <file>
-
- ---- Boogie options --------------------------------------------------------
-
- Multiple .bpl files supplied on the command line are concatenated into one
- Boogie program.
-
- /proc:<p> : limits which procedures to check
- /noResolve : parse only
- /noTypecheck : parse and resolve only
-
- /print:<file> : print Boogie program after parsing it
- (use - as <file> to print to console)
- /pretty:<n>
- 0 - print each Boogie statement on one line (faster).
- 1 (default) - pretty-print with some line breaks.
- /printWithUniqueIds : print augmented information that uniquely
- identifies variables
- /printUnstructured : with /print option, desugars all structured statements
- /printDesugared : with /print option, desugars calls
-
- /overlookTypeErrors : skip any implementation with resolution or type
- checking errors
-
- /loopUnroll:<n>
- unroll loops, following up to n back edges (and then some)
- /soundLoopUnrolling
- sound loop unrolling
- /printModel:<n>
- 0 (default) - do not print Z3's error model
- 1 - print Z3's error model
- 2 - print Z3's error model plus reverse mappings
- 4 - print Z3's error model in a more human readable way
- /printModelToFile:<file>
- print model to <file> instead of console
- /mv:<file> Specify file where to save the model in BVD format
- /enhancedErrorMessages:<n>
- 0 (default) - no enhanced error messages
- 1 - Z3 error model enhanced error messages
-
- /printCFG:<prefix> : print control flow graph of each implementation in
- Graphviz format to files named:
- <prefix>.<procedure name>.dot
-
- /useBaseNameForFileName : When parsing use basename of file for tokens instead
- of the path supplied on the command line
-
- ---- Inference options -----------------------------------------------------
-
- /infer:<flags>
- use abstract interpretation to infer invariants
- The default is /infer:i"
- // This is not 100% true, as the /infer ALWAYS creates
- // a multilattice, whereas if nothing is specified then
- // intervals are isntantiated WITHOUT being embedded in
- // a multilattice
- + @"
- <flags> are as follows (missing <flags> means all)
- i = intervals
- c = constant propagation
- d = dynamic type
- n = nullness
- p = polyhedra for linear inequalities
- t = trivial bottom/top lattice (cannot be combined with
- other domains)
- j = stronger intervals (cannot be combined with other
- domains)
- or the following (which denote options, not domains):
- s = debug statistics
- 0..9 = number of iterations before applying a widen (default=0)
- /noinfer turn off the default inference, and overrides the /infer
- switch on its left
- /checkInfer instrument inferred invariants as asserts to be checked by
- theorem prover
- /interprocInfer
- perform interprocedural inference (deprecated, not supported)
- /contractInfer
- perform procedure contract inference
- /instrumentInfer
- h - instrument inferred invariants only at beginning of
- loop headers (default)
- e - instrument inferred invariants at beginning and end
- of every block (this mode is intended for use in
- debugging of abstract domains)
- /printInstrumented
- print Boogie program after it has been instrumented with
- invariants
-
- ---- Debugging and general tracing options ---------------------------------
-
- /trace blurt out various debug trace information
- /traceTimes output timing information at certain points in the pipeline
- /tracePOs output information about the number of proof obligations
- (also included in the /trace output)
- /log[:method] Print debug output during translation
-
- /break launch and break into debugger
-
- ---- Verification-condition generation options -----------------------------
-
- /liveVariableAnalysis:<c>
- 0 = do not perform live variable analysis
- 1 = perform live variable analysis (default)
- 2 = perform interprocedural live variable analysis
- /noVerify skip VC generation and invocation of the theorem prover
- /verifySnapshots:<n>
- verify several program snapshots (named <filename>.v0.bpl
- to <filename>.vN.bpl) using verification result caching:
- 0 - do not use any verification result caching (default)
- 1 - use the basic verification result caching
- 2 - use the more advanced verification result caching
- 3 - use the more advanced caching and report errors according
- to the new source locations for errors and their
- related locations (but not /errorTrace and CaptureState
- locations)
- /verifySeparately
- verify each input program separately
- /removeEmptyBlocks:<c>
- 0 - do not remove empty blocks during VC generation
- 1 - remove empty blocks (default)
- /coalesceBlocks:<c>
- 0 = do not coalesce blocks
- 1 = coalesce blocks (default)
- /vc:<variety> n = nested block (default for /prover:Simplify),
- m = nested block reach,
- b = flat block, r = flat block reach,
- s = structured, l = local,
- d = dag (default, except with /prover:Simplify)
- doomed = doomed
- /traceverify print debug output during verification condition generation
- /subsumption:<c>
- apply subsumption to asserted conditions:
- 0 - never, 1 - not for quantifiers, 2 (default) - always
- /alwaysAssumeFreeLoopInvariants
- usually, a free loop invariant (or assume
- statement in that position) is ignored in checking contexts
- (like other free things); this option includes these free
- loop invariants as assumes in both contexts
- /inline:<i> use inlining strategy <i> for procedures with the :inline
- attribute, see /attrHelp for details:
- none
- assume (default)
- assert
- spec
- /printInlined
- print the implementation after inlining calls to
- procedures with the :inline attribute (works with /inline)
- /lazyInline:1
- Use the lazy inlining algorithm
- /stratifiedInline:1
- Use the stratified inlining algorithm
- /fixedPointEngine:<engine>
- Use the specified fixed point engine for inference
- /recursionBound:<n>
- Set the recursion bound for stratified inlining to
- be n (default 500)
- /inferLeastForUnsat:<str>
- Infer the least number of constants (whose names
- are prefixed by <str>) that need to be set to
- true for the program to be correct. This turns
- on stratified inlining.
- /smoke Soundness Smoke Test: try to stick assert false; in some
- places in the BPL and see if we can still prove it
- /smokeTimeout:<n>
- Timeout, in seconds, for a single theorem prover
- invocation during smoke test, defaults to 10.
- /causalImplies
- Translate Boogie's A ==> B into prover's A ==> A && B.
- /typeEncoding:<m>
- how to encode types when sending VC to theorem prover
- n = none (unsound)
- p = predicates (default)
- a = arguments
- m = monomorphic
- /monomorphize
- Do not abstract map types in the encoding (this is an
- experimental feature that will not do the right thing if
- the program uses polymorphism)
- /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined
- to be +, instead of +.
-
- ---- Verification-condition splitting --------------------------------------
-
- /vcsMaxCost:<f>
- VC will not be split unless the cost of a VC exceeds this
- number, defaults to 2000.0. This does NOT apply in the
- keep-going mode after first round of splitting.
- /vcsMaxSplits:<n>
- Maximal number of VC generated per method. In keep
- going mode only applies to the first round.
- Defaults to 1.
- /vcsMaxKeepGoingSplits:<n>
- If set to more than 1, activates the keep
- going mode, where after the first round of splitting,
- VCs that timed out are split into <n> pieces and retried
- until we succeed proving them, or there is only one
- assertion on a single path and it timeouts (in which
- case error is reported for that assertion).
- Defaults to 1.
- /vcsKeepGoingTimeout:<n>
- Timeout in seconds for a single theorem prover
- invocation in keep going mode, except for the final
- single-assertion case. Defaults to 1s.
- /vcsFinalAssertTimeout:<n>
- Timeout in seconds for the single last
- assertion in the keep going mode. Defaults to 30s.
- /vcsPathJoinMult:<f>
- If more than one path join at a block, by how much
- multiply the number of paths in that block, to accomodate
- for the fact that the prover will learn something on one
- paths, before proceeding to another. Defaults to 0.8.
- /vcsPathCostMult:<f1>
- /vcsAssumeMult:<f2>
- The cost of a block is
- (<assert-cost> + <f2>*<assume-cost>) *
- (1.0 + <f1>*<entering-paths>)
- <f1> defaults to 1.0, <f2> defaults to 0.01.
- The cost of a single assertion or assumption is
- currently always 1.0.
- /vcsPathSplitMult:<f>
- If the best path split of a VC of cost A is into
- VCs of cost B and C, then the split is applied if
- A >= <f>*(B+C), otherwise assertion splitting will be
- applied. Defaults to 0.5 (always do path splitting if
- possible), set to more to do less path splitting
- and more assertion splitting.
- /vcsDumpSplits
- For split #n dump split.n.dot and split.n.bpl.
- Warning: Affects error reporting.
- /vcsCores:<n>
- Try to verify <n> VCs at once. Defaults to 1.
- /vcsLoad:<f> Sets vcsCores to the machine's ProcessorCount * f,
- rounded to the nearest integer (where 0.0 <= f <= 3.0),
- but never to less than 1.
-
- ---- Prover options --------------------------------------------------------
-
- /errorLimit:<num>
- Limit the number of errors produced for each procedure
- (default is 5, some provers may support only 1)
- /timeLimit:<num>
- Limit the number of seconds spent trying to verify
- each procedure
- /errorTrace:<n>
- 0 - no Trace labels in the error output,
- 1 (default) - include useful Trace labels in error output,
- 2 - include all Trace labels in the error output
- /vcBrackets:<b>
- bracket odd-charactered identifier names with |'s. <b> is:
- 0 - no (default with non-/prover:Simplify),
- 1 - yes (default with /prover:Simplify)
- /prover:<tp> use theorem prover <tp>, where <tp> is either the name of
- a DLL containing the prover interface located in the
- Boogie directory, or a full path to a DLL containing such
- an interface. The standard interfaces shipped include:
- SMTLib (default, uses the SMTLib2 format and calls Z3)
- Z3 (uses Z3 with the Simplify format)
- Simplify
- ContractInference (uses Z3)
- Z3api (Z3 using Managed .NET API)
- /proverOpt:KEY[=VALUE]
- Provide a prover-specific option (short form /p).
- /proverLog:<file>
- Log input for the theorem prover. Like filenames
- supplied as arguments to other options, <file> can use the
- following macros:
- @TIME@ expands to the current time
- @PREFIX@ expands to the concatenation of strings given
- by /logPrefix options
- @FILE@ expands to the last filename specified on the
- command line
- In addition, /proverLog can also use the macro '@PROC@',
- which causes there to be one prover log file per
- verification condition, and the macro then expands to the
- name of the procedure that the verification condition is for.
- /logPrefix:<str>
- Defines the expansion of the macro '@PREFIX@', which can
- be used in various filenames specified by other options.
- /proverLogAppend
- Append (not overwrite) the specified prover log file
- /proverWarnings
- 0 (default) - don't print, 1 - print to stdout,
- 2 - print to stderr
- /proverMemoryLimit:<num>
- Limit on the virtual memory for prover before
- restart in MB (default:100MB)
- /restartProver
- Restart the prover after each query
- /proverShutdownLimit<num>
- Time between closing the stream to the prover and
- killing the prover process (default: 0s)
- /platform:<ptype>,<location>
- ptype = v11,v2,cli1
- location = platform libraries directory
-
- Simplify specific options:
- /simplifyMatchDepth:<num>
- Set Simplify prover's matching depth limit
-
- Z3 specific options:
- /z3opt:<arg> specify additional Z3 options
- /z3multipleErrors
- report multiple counterexamples for each error
- /useArrayTheory
- use Z3's native theory (as opposed to axioms). Currently
- implies /monomorphize.
- /useSmtOutputFormat
- Z3 outputs a model in the SMTLIB2 format.
- /z3types generate multi-sorted VC that make use of Z3 types
- /z3lets:<n> 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
- 3 - (default) any
- /z3exe:<path>
- path to Z3 executable
-
- CVC4 specific options:
- /cvc4exe:<path>
- path to CVC4 executable
-");
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Collections.Specialized; +using System.IO; +using System.Linq; +using System.Diagnostics; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie { + public class CommandLineOptionEngine + { + public readonly string ToolName; + public readonly string DescriptiveToolName; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(ToolName != null); + Contract.Invariant(DescriptiveToolName != null); + Contract.Invariant(this._environment != null); + Contract.Invariant(cce.NonNullElements(this._files)); + Contract.Invariant(this._fileTimestamp != null); + } + + private string/*!*/ _environment = ""; + + public string Environment { + get { + Contract.Ensures(Contract.Result<string>() != null); + return this._environment; + } + set { + Contract.Requires(value != null); + this._environment = value; + } + } + + private readonly List<string/*!*/>/*!*/ _files = new List<string/*!*/>(); + + public IList<string/*!*/>/*!*/ Files { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result<IList<string>>())); + Contract.Ensures(Contract.Result<IList<string>>().IsReadOnly); + return this._files.AsReadOnly(); + } + } + + public bool HelpRequested = false; + public bool AttrHelpRequested = false; + + public CommandLineOptionEngine(string toolName, string descriptiveName) { + Contract.Requires(toolName != null); + Contract.Requires(descriptiveName != null); + ToolName = toolName; + DescriptiveToolName = descriptiveName; + } + + public virtual string/*!*/ VersionNumber { + get { + Contract.Ensures(Contract.Result<string>() != null); + return cce.NonNull(cce.NonNull(System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)).FileVersion); + } + } + public virtual string/*!*/ VersionSuffix { + get { + Contract.Ensures(Contract.Result<string>() != null); + return " version " + VersionNumber + ", Copyright (c) 2003-2014, Microsoft."; + } + } + public virtual string/*!*/ Version { + get { + Contract.Ensures(Contract.Result<string>() != null); + return DescriptiveToolName + VersionSuffix; + } + } + + private string/*!*/ _fileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.'); + + public string FileTimestamp { + get { + Contract.Ensures(Contract.Result<string>() != null); + return this._fileTimestamp; + } + set { + Contract.Requires(value != null); + this._fileTimestamp = value; + } + } + + public void ExpandFilename(ref string pattern, string logPrefix, string fileTimestamp) { + if (pattern != null) { + pattern = pattern.Replace("@PREFIX@", logPrefix).Replace("@TIME@", fileTimestamp); + string fn = Files.Count == 0 ? "" : Files[Files.Count - 1]; + fn = fn.Replace('/', '-').Replace('\\', '-'); + pattern = pattern.Replace("@FILE@", fn); + } + } + + /// <summary> + /// Process the option and modify "ps" accordingly. + /// Return true if the option is one that is recognized. + /// </summary> + protected virtual bool ParseOption(string name, CommandLineParseState ps) { + Contract.Requires(name != null); + Contract.Requires(ps != null); + + switch (name) { + case "help": + case "?": + if (ps.ConfirmArgumentCount(0)) { + HelpRequested = true; + } + return true; + case "attrHelp": + if (ps.ConfirmArgumentCount(0)) { + AttrHelpRequested = true; + } + return true; + default: + break; + } + return false; // unrecognized option + } + + protected class CommandLineParseState + { + public string s; + public bool hasColonArgument; + public readonly string[]/*!*/ args; + public int i; + public int nextIndex; + public bool EncounteredErrors; + public readonly string ToolName; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(args != null); + Contract.Invariant(0 <= i && i <= args.Length); + Contract.Invariant(0 <= nextIndex && nextIndex <= args.Length); + } + + + public CommandLineParseState(string[] args, string toolName) { + Contract.Requires(args != null); + Contract.Requires(Contract.ForAll(0, args.Length, i => args[i] != null)); + Contract.Requires(toolName != null); + Contract.Ensures(this.args == args); + this.ToolName = toolName; + this.s = null; // set later by client + this.hasColonArgument = false; // set later by client + this.args = args; + this.i = 0; + this.nextIndex = 0; // set later by client + this.EncounteredErrors = false; + } + + public bool CheckBooleanFlag(string flagName, ref bool flag, bool valueWhenPresent) { + Contract.Requires(flagName != null); + //modifies nextIndex, encounteredErrors, Console.Error.*; + bool flagPresent = false; + + if ((s == "/" + flagName || s == "-" + flagName) && ConfirmArgumentCount(0)) { + flag = valueWhenPresent; + flagPresent = true; + } + return flagPresent; + } + + public bool CheckBooleanFlag(string flagName, ref bool flag) { + Contract.Requires(flagName != null); + //modifies nextIndex, encounteredErrors, Console.Error.*; + return CheckBooleanFlag(flagName, ref flag, true); + } + + /// <summary> + /// If there is one argument and it is a non-negative integer, then set "arg" to that number and return "true". + /// Otherwise, emit error message, leave "arg" unchanged, and return "false". + /// </summary> + public bool GetNumericArgument(ref int arg) { + //modifies nextIndex, encounteredErrors, Console.Error.*; + return GetNumericArgument(ref arg, a => 0 <= a); + } + + /// <summary> + /// If there is one argument and the filtering predicate holds, then set "arg" to that number and return "true". + /// Otherwise, emit error message, leave "arg" unchanged, and return "false". + /// </summary> + public bool GetNumericArgument(ref int arg, Predicate<int> filter) { + Contract.Requires(filter != null); + + if (this.ConfirmArgumentCount(1)) { + try { + Contract.Assume(args[i] != null); + Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent + int d = Convert.ToInt32(this.args[this.i]); + if (filter == null || filter(d)) { + arg = d; + return true; + } + } catch (System.FormatException) { + } catch (System.OverflowException) { + } + } else { + return false; + } + Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s); + return false; + } + + /// <summary> + /// If there is one argument and it is a non-negative integer less than "limit", + /// then set "arg" to that number and return "true". + /// Otherwise, emit error message, leave "arg" unchanged, and return "false". + /// </summary> + public bool GetNumericArgument(ref int arg, int limit) { + Contract.Requires(this.i < args.Length); + Contract.Ensures(Math.Min(arg, 0) <= Contract.ValueAtReturn(out arg) && Contract.ValueAtReturn(out arg) < limit); + //modifies nextIndex, encounteredErrors, Console.Error.*; + int a = arg; + if (!GetNumericArgument(ref a)) { + return false; + } else if (a < limit) { + arg = a; + return true; + } else { + Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s); + return false; + } + } + + /// <summary> + /// If there is one argument and it is a non-negative real, then set "arg" to that number and return "true". + /// Otherwise, emit an error message, leave "arg" unchanged, and return "false". + /// </summary> + public bool GetNumericArgument(ref double arg) { + Contract.Ensures(Contract.ValueAtReturn(out arg) >= 0); + //modifies nextIndex, encounteredErrors, Console.Error.*; + if (this.ConfirmArgumentCount(1)) { + try { + Contract.Assume(args[i] != null); + Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent + double d = Convert.ToDouble(this.args[this.i]); + if (0 <= d) { + arg = d; + return true; + } + } catch (System.FormatException) { + } catch (System.OverflowException) { + } + } else { + return false; + } + Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s); + return false; + } + + public bool ConfirmArgumentCount(int argCount) { + Contract.Requires(0 <= argCount); + //modifies nextIndex, encounteredErrors, Console.Error.*; + Contract.Ensures(Contract.Result<bool>() == (!(hasColonArgument && argCount != 1) && !(args.Length < i + argCount))); + if (hasColonArgument && argCount != 1) { + Error("\"{0}\" cannot take a colon argument", s); + nextIndex = args.Length; + return false; + } else if (args.Length < i + argCount) { + Error("\"{0}\" expects {1} argument{2}", s, argCount.ToString(), (string)(argCount == 1 ? "" : "s")); + nextIndex = args.Length; + return false; + } else { + nextIndex = i + argCount; + return true; + } + } + + public void Error(string message, params string[] args) { + Contract.Requires(args != null); + Contract.Requires(message != null); + //modifies encounteredErrors, Console.Error.*; + Console.Error.WriteLine("{0}: Error: {1}", ToolName, String.Format(message, args)); + EncounteredErrors = true; + } + } + + public virtual void Usage() { + Console.WriteLine("{0}: usage: {0} [ option ... ] [ filename ... ]", ToolName); + Console.WriteLine(@" where <option> is one of + + ---- General options ------------------------------------------------------- + + /help this message + /attrHelp print a message about declaration attributes supported by + this implementation"); + } + + public virtual void AttributeUsage() { + } + + /// <summary> + /// This method is called after all parsing is done, if no parse errors were encountered. + /// </summary> + public virtual void ApplyDefaultOptions() { + } + + /// <summary> + /// Parses the command-line arguments "args" into the global flag variables. Returns true + /// if there were no errors. + /// </summary> + /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param> + public bool Parse([Captured] string[]/*!*/ args) { + Contract.Requires(cce.NonNullElements(args)); + + // save the command line options for the log files + Environment += "Command Line Options: " + args.Concat(" "); + args = cce.NonNull((string[])args.Clone()); // the operations performed may mutate the array, so make a copy + var ps = new CommandLineParseState(args, ToolName); + + while (ps.i < args.Length) { + cce.LoopInvariant(ps.args == args); + string arg = args[ps.i]; + Contract.Assert(arg != null); + ps.s = arg.Trim(); + + bool isOption = ps.s.StartsWith("-") || ps.s.StartsWith("/"); + int colonIndex = ps.s.IndexOf(':'); + if (0 <= colonIndex && isOption) { + ps.hasColonArgument = true; + args[ps.i] = ps.s.Substring(colonIndex + 1); + ps.s = ps.s.Substring(0, colonIndex); + } else { + ps.i++; + ps.hasColonArgument = false; + } + ps.nextIndex = ps.i; + + if (isOption) { + if (!ParseOption(ps.s.Substring(1), ps)) { + if (Path.DirectorySeparatorChar == '/' && ps.s.StartsWith("/")) + this._files.Add(arg); + else + ps.Error("unknown switch: {0}", ps.s); + } + } else { + this._files.Add(arg); + } + + ps.i = ps.nextIndex; + } + + if (HelpRequested) { + Usage(); + } else if (AttrHelpRequested) { + AttributeUsage(); + } else if (ps.EncounteredErrors) { + Console.WriteLine("Use /help for available options"); + } + + if (ps.EncounteredErrors) { + return false; + } else { + this.ApplyDefaultOptions(); + return true; + } + } + + } + + /// <summary> + /// Boogie command-line options (other tools can subclass this class in order to support a + /// superset of Boogie's options. + /// </summary> + public class CommandLineOptions : CommandLineOptionEngine { + + public CommandLineOptions() + : base("Boogie", "Boogie program verifier") { + } + + protected CommandLineOptions(string toolName, string descriptiveName) + : base(toolName, descriptiveName) { + Contract.Requires(toolName != null); + Contract.Requires(descriptiveName != null); + } + + private static CommandLineOptions clo; + public static CommandLineOptions/*!*/ Clo + { + get { return clo; } + } + + public static void Install(CommandLineOptions options) { + Contract.Requires(options != null); + clo = options; + } + + public const long Megabyte = 1048576; + + // Flags and arguments + + public bool RunningBoogieFromCommandLine = false; // "false" means running Boogie from the plug-in + + [ContractInvariantMethod] + void ObjectInvariant2() { + Contract.Invariant(LogPrefix != null); + Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3); // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured + } + + public int VerifySnapshots = -1; + public bool VerifySeparately = false; + public string PrintFile = null; + public int PrintUnstructured = 0; + public bool UseBaseNameForFileName = false; + public int DoomStrategy = -1; + public bool DoomRestartTP = false; + public bool PrintDesugarings = false; + public string SimplifyLogFilePath = null; + public bool PrintInstrumented = false; + public bool InstrumentWithAsserts = false; + public string ProverPreamble = null; + + public enum InstrumentationPlaces { + LoopHeaders, + Everywhere + } + public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders; + public bool PrintWithUniqueASTIds = false; + private string XmlSinkFilename = null; + [Peer] + public XmlSink XmlSink = null; + public bool Wait = false; + public bool Trace = false; + public bool TraceTimes = false; + public bool TraceProofObligations = false; + public bool TraceCachingForTesting + { + get + { + return TraceCaching == 1 || TraceCaching == 3; + } + } + public bool TraceCachingForBenchmarking + { + get + { + return TraceCaching == 2 || TraceCaching == 3; + } + } + public bool TraceCachingForDebugging + { + get + { + return TraceCaching == 3; + } + } + internal int TraceCaching = 0; + public bool NoResolve = false; + public bool NoTypecheck = false; + public bool OverlookBoogieTypeErrors = false; + public bool Verify = true; + public bool TraceVerify = false; + public int /*(0:3)*/ ErrorTrace = 1; + public bool IntraproceduralInfer = true; + public bool ContractInfer = false; + public bool ExplainHoudini = false; + public bool ReverseHoudiniWorklist = false; + public bool ConcurrentHoudini = false; + public bool ModifyTopologicalSorting = false; + public bool DebugConcurrentHoudini = false; + public bool HoudiniUseCrossDependencies = false; + public string StagedHoudini = null; + public bool DebugStagedHoudini = false; + public bool StagedHoudiniReachabilityAnalysis = false; + public bool StagedHoudiniMergeIgnoredAnnotations = false; + public int StagedHoudiniThreads = 1; + public string VariableDependenceIgnore = null; + public string AbstractHoudini = null; + public bool UseUnsatCoreForContractInfer = false; + public bool PrintAssignment = false; + public int InlineDepth = -1; + public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values + public bool UseUncheckedContracts = false; + public bool SimplifyLogFileAppend = false; + public bool SoundnessSmokeTest = false; + public string Z3ExecutablePath = null; + public string Z3ExecutableName = null; + public string CVC4ExecutablePath = null; + public int KInductionDepth = -1; + + private string/*!*/ _logPrefix = ""; + + public string LogPrefix { + get { + Contract.Ensures(Contract.Result<string>() != null); + return this._logPrefix; + } + set { + Contract.Requires(value != null); + this._logPrefix = value; + } + } + + public bool PrettyPrint = true; + + public enum ProverWarnings { + None, + Stdout, + Stderr + } + public ProverWarnings PrintProverWarnings = ProverWarnings.None; + public int ProverShutdownLimit = 0; + + public enum SubsumptionOption { + Never, + NotForQuantifiers, + Always + } + public SubsumptionOption UseSubsumption = SubsumptionOption.Always; + + public bool AlwaysAssumeFreeLoopInvariants = false; + + public enum ShowEnvironment { + Never, + DuringPrint, + Always + } + public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint; + public bool DontShowLogo = false; + [ContractInvariantMethod] + void ObjectInvariant3() { + Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3); + Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7); + Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4); + Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2); + Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9); + Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1); + Contract.Invariant(cce.NonNullElements(this.proverOptions)); + } + + public int LoopUnrollCount = -1; // -1 means don't unroll loops + public bool SoundLoopUnrolling = false; + public int LoopFrameConditions = -1; // -1 means not specified -- this will be replaced by the "implications" section below + public int ModifiesDefault = 5; + public bool LocalModifiesChecks = true; + public bool NoVerifyByDefault = false; + public enum OwnershipModelOption { + Standard, + Experimental, + Trivial + } + public OwnershipModelOption OwnershipModelEncoding = OwnershipModelOption.Standard; + public int PrintErrorModel = 0; + public string PrintErrorModelFile = null; + public string/*?*/ ModelViewFile = null; + public int EnhancedErrorMessages = 0; + public string PrintCFGPrefix = null; + public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present + public bool UseArrayTheory = false; + public bool UseSmtOutputFormat = false; + public bool WeakArrayTheory = false; + public bool UseLabels = true; + public bool RunDiagnosticsOnTimeout = false; + public bool TraceDiagnosticsOnTimeout = false; + public int TimeLimitPerAssertionInPercent = 10; + public bool SIBoolControlVC = false; + public bool MonomorphicArrays { + get { + return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; + } + } + public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically + public bool DoModSetAnalysis = false; + public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation + private int /*0..9*/stepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator + + public int StepsBeforeWidening + { + get + { + Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= 9); + return this.stepsBeforeWidening; + } + set + { + Contract.Requires(0 <= value && value <= 9); + this.stepsBeforeWidening = value; + } + } + + public string OwickiGriesDesugaredOutputFile = null; + public bool TrustAtomicityTypes = false; + public bool TrustNonInterference = false; + public int TrustLayersUpto = -1; + public int TrustLayersDownto = int.MaxValue; + + public enum VCVariety { + Structured, + Block, + Local, + BlockNested, + BlockReach, + BlockNestedReach, + Dag, + DagIterative, + Doomed, + Unspecified + } + public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed + + public bool RemoveEmptyBlocks = true; + public bool CoalesceBlocks = true; + public bool PruneInfeasibleEdges = true; + + [Rep] + public ProverFactory TheProverFactory; + public string ProverName; + [Peer] + private List<string> proverOptions = new List<string>(); + + public IEnumerable<string> ProverOptions + { + set + { + Contract.Requires(cce.NonNullElements(value)); + + this.proverOptions = new List<string>(value); + } + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>())); + + foreach (string s in this.proverOptions) + yield return s; + } + } + + [Obsolete("use the setter for 'ProverOptions' directly")] + public void AddProverOption(string option) + { + Contract.Requires(option != null); + + this.ProverOptions = this.ProverOptions.Concat1(option); + } + + [Obsolete("use the setter for 'ProverOptions' directly")] + public void RemoveAllProverOptions(Predicate<string> match) + { + this.ProverOptions = this.ProverOptions.Where(s => !match(s)); + } + + private int bracketIdsInVC = -1; // -1 - not specified, 0 - no, 1 - yes + + public int BracketIdsInVC { + get { + Contract.Ensures(-1 <= Contract.Result<int>() && Contract.Result<int>() <= 1); + return this.bracketIdsInVC; + } + set { + Contract.Requires(-1 <= value && value <= 1); + this.bracketIdsInVC = value; + } + } + + public bool CausalImplies = false; + + public int SimplifyProverMatchDepth = -1; // -1 means not specified + public int ProverKillTime = -1; // -1 means not specified + public int SmokeTimeout = 10; // default to 10s + public int ProverCCLimit = 5; + public bool z3AtFlag = true; + public bool RestartProverPerVC = false; + + public double VcsMaxCost = 1.0; + public double VcsPathJoinMult = 0.8; + public double VcsPathCostMult = 1.0; + public double VcsAssumeMult = 0.01; + public double VcsPathSplitMult = 0.5; // 0.5-always, 2-rarely do path splitting + public int VcsMaxSplits = 1; + public int VcsMaxKeepGoingSplits = 1; + public int VcsFinalAssertTimeout = 30; + public int VcsKeepGoingTimeout = 1; + public int VcsCores = 1; + public bool VcsDumpSplits = false; + + public bool DebugRefuted = false; + + public XmlSink XmlRefuted { + get { + if (DebugRefuted) + return XmlSink; + else + return null; + } + } + [ContractInvariantMethod] + void ObjectInvariant4() { + Contract.Invariant(cce.NonNullElements(this.z3Options)); + Contract.Invariant(0 <= Z3lets && Z3lets < 4); + } + + [Peer] + private List<string> z3Options = new List<string>(); + + public IEnumerable<string> Z3Options + { + get + { + Contract.Ensures(Contract.Result<IEnumerable<string>>() != null); + foreach (string s in z3Options) + yield return s; + } + } + + public void AddZ3Option(string option) + { + Contract.Requires(option != null); + this.z3Options.Add(option); + } + + public bool Z3types = false; + public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any + + + // Maximum amount of virtual memory (in bytes) for the prover to use + // + // Non-positive number indicates unbounded. + public long MaxProverMemory = 100 * Megabyte; + + // Minimum number of prover calls before restart + public int MinNumOfProverCalls = 5; + + public enum PlatformType { + notSpecified, + v1, + v11, + v2, + cli1 + } + public PlatformType TargetPlatform; + public string TargetPlatformLocation; + public string StandardLibraryLocation; + + // whether procedure inlining is enabled at call sites. + public enum Inlining { + None, + Assert, + Assume, + Spec + }; + public Inlining ProcedureInlining = Inlining.Assume; + public bool PrintInlined = false; + public bool ExtractLoops = false; + public bool DeterministicExtractLoops = false; + public string SecureVcGen = null; + public int StratifiedInlining = 0; + public string FixedPointEngine = null; + public int StratifiedInliningOption = 0; + public bool StratifiedInliningWithoutModels = false; // disable model generation for SI + public int StratifiedInliningVerbose = 0; // verbosity level + public int RecursionBound = 500; + public bool NonUniformUnfolding = false; + public int StackDepthBound = 0; + public string inferLeastForUnsat = null; + + // Inference mode for fixed point engine + public enum FixedPointInferenceMode { + Corral, + OldCorral, + Flat, + Procedure, + Call + }; + public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure; + + public string PrintFixedPoint = null; + + public string PrintConjectures = null; + + public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically) + + public enum TypeEncoding { + None, + Predicates, + Arguments, + Monomorphic + }; + public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates; + + public bool Monomorphize = false; + + public bool ReflectAdd = false; + + public int LiveVariableAnalysis = 1; + + // Static constructor + static CommandLineOptions() { + if (System.Type.GetType("Mono.Runtime") == null) { // MONO + TraceListenerCollection/*!*/ dbl = Debug.Listeners; + Contract.Assert(dbl != null); + Contract.Assume(cce.IsPeerConsistent(dbl)); // hangs off static field + dbl.Add(new DefaultTraceListener()); + } + } + + public IEnumerable<string/*!*/> ProcsToCheck { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>>(), true)); + return this.procsToCheck != null ? this.procsToCheck.AsEnumerable() : null; + } + } + + private List<string/*!*/> procsToCheck = null; // null means "no restriction" + + [ContractInvariantMethod] + void ObjectInvariant5() { + Contract.Invariant(cce.NonNullElements(this.procsToCheck, true)); + Contract.Invariant(Ai != null); + } + + public class AiFlags { + public bool J_Trivial = false; + public bool J_Intervals = false; + public bool DebugStatistics = false; + } + public readonly AiFlags/*!*/ Ai = new AiFlags(); + + public class ConcurrentHoudiniOptions + { + public List<string> ProverOptions = new List<string>(); + public int ProverCCLimit = 5; + public bool DisableLoopInvEntryAssert = false; + public bool DisableLoopInvMaintainedAssert = false; + public bool ModifyTopologicalSorting = false; + } + public List<ConcurrentHoudiniOptions> Cho = new List<ConcurrentHoudiniOptions>(); + + protected override bool ParseOption(string name, CommandLineOptionEngine.CommandLineParseState ps) { + var args = ps.args; // convenient synonym + switch (name) { + case "infer": + if (ps.ConfirmArgumentCount(1)) { + foreach (char c in cce.NonNull(args[ps.i])) { + switch (c) { + case 't': + Ai.J_Trivial = true; + UseAbstractInterpretation = true; + break; + case 'j': + Ai.J_Intervals = true; + UseAbstractInterpretation = true; + break; + case 's': + Ai.DebugStatistics = true; + UseAbstractInterpretation = true; + break; + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': + StepsBeforeWidening = (int)char.GetNumericValue(c); + break; + default: + ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s); + break; + } + } + } + return true; + + case "noinfer": + if (ps.ConfirmArgumentCount(0)) { + UseAbstractInterpretation = false; + } + return true; + + case "break": + case "launch": + if (ps.ConfirmArgumentCount(0)) { + System.Diagnostics.Debugger.Launch(); + } + return true; + + case "proc": + if (this.procsToCheck == null) { + this.procsToCheck = new List<string/*!*/>(); + } + if (ps.ConfirmArgumentCount(1)) { + this.procsToCheck.Add(cce.NonNull(args[ps.i])); + } + return true; + + case "xml": + if (ps.ConfirmArgumentCount(1)) { + XmlSinkFilename = args[ps.i]; + } + return true; + + case "print": + if (ps.ConfirmArgumentCount(1)) { + PrintFile = args[ps.i]; + } + return true; + + case "pretty": + int val = 1; + if (ps.GetNumericArgument(ref val, 2)) { + PrettyPrint = val == 1; + } + return true; + + case "OwickiGries": + if (ps.ConfirmArgumentCount(1)) { + OwickiGriesDesugaredOutputFile = args[ps.i]; + } + return true; + + case "trustLayersUpto": + if (ps.ConfirmArgumentCount(1)) + { + ps.GetNumericArgument(ref TrustLayersUpto); + } + return true; + + case "trustLayersDownto": + if (ps.ConfirmArgumentCount(1)) + { + ps.GetNumericArgument(ref TrustLayersDownto); + } + return true; + + case "proverLog": + if (ps.ConfirmArgumentCount(1)) { + SimplifyLogFilePath = args[ps.i]; + } + return true; + + case "proverPreamble": + if (ps.ConfirmArgumentCount(1)) + { + ProverPreamble = args[ps.i]; + } + return true; + + case "logPrefix": + if (ps.ConfirmArgumentCount(1)) { + string s = cce.NonNull(args[ps.i]); + LogPrefix += s.Replace('/', '-').Replace('\\', '-'); + } + return true; + + case "proverShutdownLimit": + ps.GetNumericArgument(ref ProverShutdownLimit); + return true; + + case "errorTrace": + ps.GetNumericArgument(ref ErrorTrace, 3); + return true; + + case "proverWarnings": { + int pw = 0; + if (ps.GetNumericArgument(ref pw, 3)) { + switch (pw) { + case 0: + PrintProverWarnings = ProverWarnings.None; + break; + case 1: + PrintProverWarnings = ProverWarnings.Stdout; + break; + case 2: + PrintProverWarnings = ProverWarnings.Stderr; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } + } + return true; + } + + case "env": { + int e = 0; + if (ps.GetNumericArgument(ref e, 3)) { + switch (e) { + case 0: + ShowEnv = ShowEnvironment.Never; + break; + case 1: + ShowEnv = ShowEnvironment.DuringPrint; + break; + case 2: + ShowEnv = ShowEnvironment.Always; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } + } + return true; + } + + case "loopUnroll": + ps.GetNumericArgument(ref LoopUnrollCount); + return true; + + case "printModel": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "0": + PrintErrorModel = 0; + break; + case "1": + PrintErrorModel = 1; + break; + case "2": + PrintErrorModel = 2; + break; + case "4": + PrintErrorModel = 4; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + + case "mv": + if (ps.ConfirmArgumentCount(1)) { + ModelViewFile = args[ps.i]; + } + return true; + + case "printModelToFile": + if (ps.ConfirmArgumentCount(1)) { + PrintErrorModelFile = args[ps.i]; + } + return true; + + case "enhancedErrorMessages": + ps.GetNumericArgument(ref EnhancedErrorMessages, 2); + return true; + + case "printCFG": + if (ps.ConfirmArgumentCount(1)) { + PrintCFGPrefix = args[ps.i]; + } + return true; + + case "inlineDepth": + ps.GetNumericArgument(ref InlineDepth); + return true; + + case "subsumption": { + int s = 0; + if (ps.GetNumericArgument(ref s, 3)) { + switch (s) { + case 0: + UseSubsumption = SubsumptionOption.Never; + break; + case 1: + UseSubsumption = SubsumptionOption.NotForQuantifiers; + break; + case 2: + UseSubsumption = SubsumptionOption.Always; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } + } + return true; + } + + case "liveVariableAnalysis": { + int lva = 0; + if (ps.GetNumericArgument(ref lva, 3)) { + LiveVariableAnalysis = lva; + } + return true; + } + + case "removeEmptyBlocks": { + int reb = 0; + if (ps.GetNumericArgument(ref reb, 2)) { + RemoveEmptyBlocks = reb == 1; + } + return true; + } + + case "coalesceBlocks": { + int cb = 0; + if (ps.GetNumericArgument(ref cb, 2)) { + CoalesceBlocks = cb == 1; + } + return true; + } + + case "noPruneInfeasibleEdges": { + if (ps.ConfirmArgumentCount(0)) { + PruneInfeasibleEdges = false; + } + return true; + } + + case "stagedHoudini": { + if (ps.ConfirmArgumentCount(1)) { + if(args[ps.i] == "COARSE" || + args[ps.i] == "FINE" || + args[ps.i] == "BALANCED") { + StagedHoudini = args[ps.i]; + } else { + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + } + } + return true; + } + + case "stagedHoudiniThreads": { + ps.GetNumericArgument(ref StagedHoudiniThreads); + return true; + } + + case "stagedHoudiniReachabilityAnalysis": { + if (ps.ConfirmArgumentCount(0)) { + StagedHoudiniReachabilityAnalysis = true; + } + return true; + } + + case "stagedHoudiniMergeIgnoredAnnotations": { + if (ps.ConfirmArgumentCount(0)) { + StagedHoudiniMergeIgnoredAnnotations = true; + } + return true; + } + + case "debugStagedHoudini": { + if (ps.ConfirmArgumentCount(0)) { + DebugStagedHoudini = true; + } + return true; + } + + case "variableDependenceIgnore": { + if (ps.ConfirmArgumentCount(1)) { + VariableDependenceIgnore = args[ps.i]; + } + return true; + } + + case "abstractHoudini": + { + if (ps.ConfirmArgumentCount(1)) + { + AbstractHoudini = args[ps.i]; + } + return true; + } + case "vc": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "s": + case "structured": + vcVariety = VCVariety.Structured; + break; + case "b": + case "block": + vcVariety = VCVariety.Block; + break; + case "l": + case "local": + vcVariety = VCVariety.Local; + break; + case "n": + case "nested": + vcVariety = VCVariety.BlockNested; + break; + case "m": + vcVariety = VCVariety.BlockNestedReach; + break; + case "r": + vcVariety = VCVariety.BlockReach; + break; + case "d": + case "dag": + vcVariety = VCVariety.Dag; + break; + case "i": + vcVariety = VCVariety.DagIterative; + break; + case "doomed": + vcVariety = VCVariety.Doomed; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + + case "prover": + if (ps.ConfirmArgumentCount(1)) { + TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i])); + ProverName = cce.NonNull(args[ps.i]).ToUpper(); + } + return true; + + case "p": + case "proverOpt": + if (ps.ConfirmArgumentCount(1)) { + ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i])); + } + return true; + + case "DoomStrategy": + ps.GetNumericArgument(ref DoomStrategy); + return true; + + case "DoomRestartTP": + if (ps.ConfirmArgumentCount(0)) { + DoomRestartTP = true; + } + return true; + + case "extractLoops": + if (ps.ConfirmArgumentCount(0)) { + ExtractLoops = true; + } + return true; + + case "deterministicExtractLoops": + if (ps.ConfirmArgumentCount(0)) { + DeterministicExtractLoops = true; + } + return true; + + case "inline": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "none": + ProcedureInlining = Inlining.None; + break; + case "assert": + ProcedureInlining = Inlining.Assert; + break; + case "assume": + ProcedureInlining = Inlining.Assume; + break; + case "spec": + ProcedureInlining = Inlining.Spec; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + case "secure": + if (ps.ConfirmArgumentCount(1)) + SecureVcGen = args[ps.i]; + return true; + case "stratifiedInline": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "0": + StratifiedInlining = 0; + break; + case "1": + StratifiedInlining = 1; + break; + default: + StratifiedInlining = Int32.Parse(cce.NonNull(args[ps.i])); + //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + case "fixedPointEngine": + if (ps.ConfirmArgumentCount(1)) + { + FixedPointEngine = args[ps.i]; + } + return true; + case "fixedPointInfer": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "corral": + FixedPointMode = FixedPointInferenceMode.Corral; + break; + case "oldCorral": + FixedPointMode = FixedPointInferenceMode.OldCorral; + break; + case "flat": + FixedPointMode = FixedPointInferenceMode.Flat; + break; + case "procedure": + FixedPointMode = FixedPointInferenceMode.Procedure; + break; + case "call": + FixedPointMode = FixedPointInferenceMode.Call; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + case "printFixedPoint": + if (ps.ConfirmArgumentCount(1)) + { + PrintFixedPoint = args[ps.i]; + } + return true; + case "printConjectures": + if (ps.ConfirmArgumentCount(1)) + { + PrintConjectures = args[ps.i]; + } + return true; + case "siVerbose": + if (ps.ConfirmArgumentCount(1)) { + StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i])); + } + return true; + case "recursionBound": + if (ps.ConfirmArgumentCount(1)) { + RecursionBound = Int32.Parse(cce.NonNull(args[ps.i])); + } + return true; + case "stackDepthBound": + if (ps.ConfirmArgumentCount(1)) + { + StackDepthBound = Int32.Parse(cce.NonNull(args[ps.i])); + } + return true; + case "stratifiedInlineOption": + if (ps.ConfirmArgumentCount(1)) { + StratifiedInliningOption = Int32.Parse(cce.NonNull(args[ps.i])); + } + return true; + + case "inferLeastForUnsat": + if (ps.ConfirmArgumentCount(1)) { + inferLeastForUnsat = args[ps.i]; + } + return true; + + case "typeEncoding": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "n": + case "none": + TypeEncodingMethod = TypeEncoding.None; + break; + case "p": + case "predicates": + TypeEncodingMethod = TypeEncoding.Predicates; + break; + case "a": + case "arguments": + TypeEncodingMethod = TypeEncoding.Arguments; + break; + case "m": + case "monomorphic": + TypeEncodingMethod = TypeEncoding.Monomorphic; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + + case "instrumentInfer": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { + case "e": + InstrumentInfer = InstrumentationPlaces.Everywhere; + break; + case "h": + InstrumentInfer = InstrumentationPlaces.LoopHeaders; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; + + case "concurrentHoudini": + if (ps.ConfirmArgumentCount(0)) { + ConcurrentHoudini = true; + } + return true; + + case "modifyTopologicalSorting": + if (ps.ConfirmArgumentCount(0)) { + ModifyTopologicalSorting = true; + } + return true; + + case "debugConcurrentHoudini": + if (ps.ConfirmArgumentCount(0)) { + DebugConcurrentHoudini = true; + } + return true; + + case "vcBrackets": + ps.GetNumericArgument(ref bracketIdsInVC, 2); + return true; + + case "proverMemoryLimit": { + int d = 0; + if (ps.GetNumericArgument(ref d)) { + MaxProverMemory = d * Megabyte; + } + return true; + } + + case "vcsMaxCost": + ps.GetNumericArgument(ref VcsMaxCost); + return true; + + case "vcsPathJoinMult": + ps.GetNumericArgument(ref VcsPathJoinMult); + return true; + + case "vcsPathCostMult": + ps.GetNumericArgument(ref VcsPathCostMult); + return true; + + case "vcsAssumeMult": + ps.GetNumericArgument(ref VcsAssumeMult); + return true; + + case "vcsPathSplitMult": + ps.GetNumericArgument(ref VcsPathSplitMult); + return true; + + case "vcsMaxSplits": + ps.GetNumericArgument(ref VcsMaxSplits); + return true; + + case "vcsMaxKeepGoingSplits": + ps.GetNumericArgument(ref VcsMaxKeepGoingSplits); + return true; + + case "vcsFinalAssertTimeout": + ps.GetNumericArgument(ref VcsFinalAssertTimeout); + return true; + + case "vcsKeepGoingTimeout": + ps.GetNumericArgument(ref VcsKeepGoingTimeout); + return true; + + case "vcsCores": + ps.GetNumericArgument(ref VcsCores, a => 1 <= a); + return true; + + case "vcsLoad": + double load = 0.0; + if (ps.GetNumericArgument(ref load)) { + if (3.0 <= load) { + ps.Error("surprisingly high load specified; got {0}, expected nothing above 3.0", load.ToString()); + load = 3.0; + } + int p = (int)Math.Round(System.Environment.ProcessorCount * load); + VcsCores = p < 1 ? 1 : p; + } + return true; + + case "simplifyMatchDepth": + ps.GetNumericArgument(ref SimplifyProverMatchDepth); + return true; + + case "timeLimit": + ps.GetNumericArgument(ref ProverKillTime); + return true; + + case "timeLimitPerAssertionInPercent": + ps.GetNumericArgument(ref TimeLimitPerAssertionInPercent, a => 0 < a); + return true; + + case "smokeTimeout": + ps.GetNumericArgument(ref SmokeTimeout); + return true; + + case "errorLimit": + ps.GetNumericArgument(ref ProverCCLimit); + return true; + + case "verifySnapshots": + ps.GetNumericArgument(ref VerifySnapshots, 4); + return true; + + case "traceCaching": + ps.GetNumericArgument(ref TraceCaching, 4); + return true; + + case "useSmtOutputFormat": { + if (ps.ConfirmArgumentCount(0)) { + UseSmtOutputFormat = true; + } + return true; + } + + case "z3opt": + if (ps.ConfirmArgumentCount(1)) { + AddZ3Option(cce.NonNull(args[ps.i])); + } + return true; + + case "z3lets": + ps.GetNumericArgument(ref Z3lets, 4); + return true; + + case "platform": + if (ps.ConfirmArgumentCount(1)) { + StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]); + if (platformOptions != null && platformOptions.Count > 0) { + try { + this.TargetPlatform = (PlatformType)cce.NonNull(Enum.Parse(typeof(PlatformType), cce.NonNull(platformOptions[0]))); + } catch { + ps.Error("Bad /platform type '{0}'", platformOptions[0]); + break; + } + if (platformOptions.Count > 1) { + this.TargetPlatformLocation = platformOptions[1]; + if (!Directory.Exists(platformOptions[1])) { + ps.Error("/platform directory '{0}' does not exist", platformOptions[1]); + break; + } + } + } + } + return true; + + case "z3exe": + if (ps.ConfirmArgumentCount(1)) { + Z3ExecutablePath = args[ps.i]; + } + return true; + // This sets name of z3 binary boogie binary directory, not path + case "z3name": + if (ps.ConfirmArgumentCount(1)) + { + Z3ExecutableName = args[ps.i]; + } + return true; + + case "cvc4exe": + if (ps.ConfirmArgumentCount(1)) { + CVC4ExecutablePath = args[ps.i]; + } + return true; + + case "kInductionDepth": + ps.GetNumericArgument(ref KInductionDepth); + return true; + + default: + bool optionValue = false; + if (ps.CheckBooleanFlag("printUnstructured", ref optionValue)) { + PrintUnstructured = optionValue ? 1 : 0; + return true; + } + + if (ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) || + ps.CheckBooleanFlag("printInstrumented", ref PrintInstrumented) || + ps.CheckBooleanFlag("printWithUniqueIds", ref PrintWithUniqueASTIds) || + ps.CheckBooleanFlag("wait", ref Wait) || + ps.CheckBooleanFlag("trace", ref Trace) || + ps.CheckBooleanFlag("traceTimes", ref TraceTimes) || + ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) || + ps.CheckBooleanFlag("noResolve", ref NoResolve) || + ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) || + ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) || + ps.CheckBooleanFlag("noVerify", ref Verify, false) || + ps.CheckBooleanFlag("traceverify", ref TraceVerify) || + ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) || + ps.CheckBooleanFlag("nologo", ref DontShowLogo) || + ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) || + ps.CheckBooleanFlag("soundLoopUnrolling", ref SoundLoopUnrolling) || + ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) || + ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) || + ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) || + ps.CheckBooleanFlag("printInlined", ref PrintInlined) || + ps.CheckBooleanFlag("smoke", ref SoundnessSmokeTest) || + ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) || + ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) || + ps.CheckBooleanFlag("causalImplies", ref CausalImplies) || + ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) || + ps.CheckBooleanFlag("z3types", ref Z3types) || + ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) || + ps.CheckBooleanFlag("monomorphize", ref Monomorphize) || + ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) || + ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || + ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || + ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || + ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) || + ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", ref TraceDiagnosticsOnTimeout) || + ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) || + ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || + ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) || + ps.CheckBooleanFlag("reverseHoudiniWorklist", ref ReverseHoudiniWorklist) || + ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || + ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || + ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || + ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || + ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || + ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) || + ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) || + ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) || + ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName) + ) { + // one of the boolean flags matched + return true; + } + break; + } + + return base.ParseOption(name, ps); // defer to superclass + } + + public override void ApplyDefaultOptions() { + Contract.Ensures(TheProverFactory != null); + Contract.Ensures(vcVariety != VCVariety.Unspecified); + + base.ApplyDefaultOptions(); + + // expand macros in filenames, now that LogPrefix is fully determined + ExpandFilename(ref XmlSinkFilename, LogPrefix, FileTimestamp); + ExpandFilename(ref PrintFile, LogPrefix, FileTimestamp); + ExpandFilename(ref SimplifyLogFilePath, LogPrefix, FileTimestamp); + ExpandFilename(ref PrintErrorModelFile, LogPrefix, FileTimestamp); + + Contract.Assume(XmlSink == null); // XmlSink is to be set here + if (XmlSinkFilename != null) { + XmlSink = new XmlSink(XmlSinkFilename); + } + + if (TheProverFactory == null) { + TheProverFactory = ProverFactory.Load("SMTLib"); + ProverName = "SMTLib".ToUpper(); + } + + var proverOpts = TheProverFactory.BlankProverOptions(); + proverOpts.Parse(ProverOptions); + if (!TheProverFactory.SupportsLabels(proverOpts)) { + UseLabels = false; + } + + if (vcVariety == VCVariety.Unspecified) { + vcVariety = TheProverFactory.DefaultVCVariety; + } + + if (UseArrayTheory) { + Monomorphize = true; + } + + if (inferLeastForUnsat != null) { + StratifiedInlining = 1; + } + + if (StratifiedInlining > 0) { + TypeEncodingMethod = TypeEncoding.Monomorphic; + UseArrayTheory = true; + UseAbstractInterpretation = false; + MaxProverMemory = 0; // no max: avoids restarts + if (ProverName == "Z3API" || ProverName == "SMTLIB") { + ProverCCLimit = 1; + } + if (UseProverEvaluate) + StratifiedInliningWithoutModels = true; + } + + if (Trace) { + BoogieDebug.DoPrinting = true; // reuse the -trace option for debug printing + } + } + + + + public bool UserWantsToCheckRoutine(string methodFullname) { + Contract.Requires(methodFullname != null); + if (ProcsToCheck == null) { + // no preference + return true; + } + return ProcsToCheck.Contains(methodFullname); + } + + public virtual StringCollection ParseNamedArgumentList(string argList) { + if (argList == null || argList.Length == 0) + return null; + StringCollection result = new StringCollection(); + int i = 0; + for (int n = argList.Length; i < n; ) { + cce.LoopInvariant(0 <= i); + int separatorIndex = this.GetArgumentSeparatorIndex(argList, i); + if (separatorIndex > i) { + result.Add(argList.Substring(i, separatorIndex - i)); + i = separatorIndex + 1; + continue; + } + result.Add(argList.Substring(i)); + break; + } + return result; + } + public int GetArgumentSeparatorIndex(string argList, int startIndex) { + Contract.Requires(argList != null); + Contract.Requires(0 <= startIndex && startIndex <= argList.Length); + Contract.Ensures(Contract.Result<int>() < argList.Length); + int commaIndex = argList.IndexOf(",", startIndex); + int semicolonIndex = argList.IndexOf(";", startIndex); + if (commaIndex == -1) + return semicolonIndex; + if (semicolonIndex == -1) + return commaIndex; + if (commaIndex < semicolonIndex) + return commaIndex; + return semicolonIndex; + } + + public override void AttributeUsage() { + Console.WriteLine( +@"Boogie: The following attributes are supported by this implementation. + + ---- On top-level declarations --------------------------------------------- + + {:ignore} + Ignore the declaration (after checking for duplicate names). + + {:extern} + If two top-level declarations introduce the same name (for example, two + constants with the same name or two procedures with the same name), then + Boogie usually produces an error message. However, if at least one of + the declarations is declared with :extern, one of the declarations is + ignored. If both declarations are :extern, Boogie arbitrarily chooses + one of them to keep; otherwise, Boogie ignore the :extern declaration + and keeps the other. + + {:checksum <string>} + Attach a checksum to be used for verification result caching. + + ---- On implementations and procedures ------------------------------------- + + {:inline N} + Inline given procedure (can be also used on implementation). + N should be a non-negative number and represents the inlining depth. + With /inline:assume call is replaced with ""assume false"" once inlining depth is reached. + With /inline:assert call is replaced with ""assert false"" once inlining depth is reached. + With /inline:spec call is left as is once inlining depth is reached. + With the above three options, methods with the attribute {:inline N} are not verified. + With /inline:none the entire attribute is ignored. + + {:verify false} + Skip verification of an implementation. + + {:vcs_max_cost N} + {:vcs_max_splits N} + {:vcs_max_keep_going_splits N} + Per-implementation versions of + /vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits. + + {:selective_checking true} + Turn all asserts into assumes except for the ones reachable from + assumptions marked with the attribute {:start_checking_here}. + Thus, ""assume {:start_checking_here} something;"" becomes an inverse + of ""assume false;"": the first one disables all verification before + it, and the second one disables all verification after. + + {:priority N} + Assign a positive priority 'N' to an implementation to control the order + in which implementations are verified (default: N = 1). + + {:id <string>} + Assign a unique ID to an implementation to be used for verification + result caching (default: ""<impl. name>:0""). + + {:timeLimit N} + Set the time limit for a given implementation. + + ---- On functions ---------------------------------------------------------- + + {:builtin ""spec""} + {:bvbuiltin ""spec""} + Rewrite the function to built-in prover function symbol 'fn'. + + {:inline} + {:inline true} + Expand function according to its definition before going to the prover. + + {:never_pattern true} + Terms starting with this function symbol will never be + automatically selected as patterns. It does not prevent them + from being used inside the triggers, and does not affect explicit + trigger annotations. Internally it works by adding {:nopats ...} + annotations to quantifiers. + + {:identity} + {:identity true} + If the function has 1 argument and the use of it has type X->X for + some X, then the abstract interpreter will treat the function as an + identity function. Note, the abstract interpreter trusts the + attribute--it does not try to verify that the function really is an + identity function. + + ---- On variables ---------------------------------------------------------- + + {:existential true} + Marks a global Boolean variable as existentially quantified. If + used in combination with option /contractInfer Boogie will check + whether there exists a Boolean assignment to the existentials + that makes all verification conditions valid. Without option + /contractInfer the attribute is ignored. + + ---- On assert statements -------------------------------------------------- + + {:subsumption n} + Overrides the /subsumption command-line setting for this assertion. + + {:split_here} + Verifies code leading to this point and code leading from this point + to the next split_here as separate pieces. May help with timeouts. + May also occasionally double-report errors. + + ---- The end --------------------------------------------------------------- +"); + } + + public override void Usage() { + Console.WriteLine(@" + /nologo suppress printing of version number, copyright message + /env:<n> print command line arguments + 0 - never, 1 (default) - during BPL print and prover log, + 2 - like 1 and also to standard output + /wait await Enter from keyboard before terminating program + /xml:<file> also produce output in XML format to <file> + + ---- Boogie options -------------------------------------------------------- + + Multiple .bpl files supplied on the command line are concatenated into one + Boogie program. + + /proc:<p> : limits which procedures to check + /noResolve : parse only + /noTypecheck : parse and resolve only + + /print:<file> : print Boogie program after parsing it + (use - as <file> to print to console) + /pretty:<n> + 0 - print each Boogie statement on one line (faster). + 1 (default) - pretty-print with some line breaks. + /printWithUniqueIds : print augmented information that uniquely + identifies variables + /printUnstructured : with /print option, desugars all structured statements + /printDesugared : with /print option, desugars calls + + /overlookTypeErrors : skip any implementation with resolution or type + checking errors + + /loopUnroll:<n> + unroll loops, following up to n back edges (and then some) + /soundLoopUnrolling + sound loop unrolling + /printModel:<n> + 0 (default) - do not print Z3's error model + 1 - print Z3's error model + 2 - print Z3's error model plus reverse mappings + 4 - print Z3's error model in a more human readable way + /printModelToFile:<file> + print model to <file> instead of console + /mv:<file> Specify file where to save the model in BVD format + /enhancedErrorMessages:<n> + 0 (default) - no enhanced error messages + 1 - Z3 error model enhanced error messages + + /printCFG:<prefix> : print control flow graph of each implementation in + Graphviz format to files named: + <prefix>.<procedure name>.dot + + /useBaseNameForFileName : When parsing use basename of file for tokens instead + of the path supplied on the command line + + ---- Inference options ----------------------------------------------------- + + /infer:<flags> + use abstract interpretation to infer invariants + The default is /infer:i" + // This is not 100% true, as the /infer ALWAYS creates + // a multilattice, whereas if nothing is specified then + // intervals are isntantiated WITHOUT being embedded in + // a multilattice + + @" + <flags> are as follows (missing <flags> means all) + i = intervals + c = constant propagation + d = dynamic type + n = nullness + p = polyhedra for linear inequalities + t = trivial bottom/top lattice (cannot be combined with + other domains) + j = stronger intervals (cannot be combined with other + domains) + or the following (which denote options, not domains): + s = debug statistics + 0..9 = number of iterations before applying a widen (default=0) + /noinfer turn off the default inference, and overrides the /infer + switch on its left + /checkInfer instrument inferred invariants as asserts to be checked by + theorem prover + /interprocInfer + perform interprocedural inference (deprecated, not supported) + /contractInfer + perform procedure contract inference + /instrumentInfer + h - instrument inferred invariants only at beginning of + loop headers (default) + e - instrument inferred invariants at beginning and end + of every block (this mode is intended for use in + debugging of abstract domains) + /printInstrumented + print Boogie program after it has been instrumented with + invariants + + ---- Debugging and general tracing options --------------------------------- + + /trace blurt out various debug trace information + /traceTimes output timing information at certain points in the pipeline + /tracePOs output information about the number of proof obligations + (also included in the /trace output) + /log[:method] Print debug output during translation + + /break launch and break into debugger + + ---- Verification-condition generation options ----------------------------- + + /liveVariableAnalysis:<c> + 0 = do not perform live variable analysis + 1 = perform live variable analysis (default) + 2 = perform interprocedural live variable analysis + /noVerify skip VC generation and invocation of the theorem prover + /verifySnapshots:<n> + verify several program snapshots (named <filename>.v0.bpl + to <filename>.vN.bpl) using verification result caching: + 0 - do not use any verification result caching (default) + 1 - use the basic verification result caching + 2 - use the more advanced verification result caching + 3 - use the more advanced caching and report errors according + to the new source locations for errors and their + related locations (but not /errorTrace and CaptureState + locations) + /verifySeparately + verify each input program separately + /removeEmptyBlocks:<c> + 0 - do not remove empty blocks during VC generation + 1 - remove empty blocks (default) + /coalesceBlocks:<c> + 0 = do not coalesce blocks + 1 = coalesce blocks (default) + /vc:<variety> n = nested block (default for /prover:Simplify), + m = nested block reach, + b = flat block, r = flat block reach, + s = structured, l = local, + d = dag (default, except with /prover:Simplify) + doomed = doomed + /traceverify print debug output during verification condition generation + /subsumption:<c> + apply subsumption to asserted conditions: + 0 - never, 1 - not for quantifiers, 2 (default) - always + /alwaysAssumeFreeLoopInvariants + usually, a free loop invariant (or assume + statement in that position) is ignored in checking contexts + (like other free things); this option includes these free + loop invariants as assumes in both contexts + /inline:<i> use inlining strategy <i> for procedures with the :inline + attribute, see /attrHelp for details: + none + assume (default) + assert + spec + /printInlined + print the implementation after inlining calls to + procedures with the :inline attribute (works with /inline) + /lazyInline:1 + Use the lazy inlining algorithm + /stratifiedInline:1 + Use the stratified inlining algorithm + /fixedPointEngine:<engine> + Use the specified fixed point engine for inference + /recursionBound:<n> + Set the recursion bound for stratified inlining to + be n (default 500) + /inferLeastForUnsat:<str> + Infer the least number of constants (whose names + are prefixed by <str>) that need to be set to + true for the program to be correct. This turns + on stratified inlining. + /smoke Soundness Smoke Test: try to stick assert false; in some + places in the BPL and see if we can still prove it + /smokeTimeout:<n> + Timeout, in seconds, for a single theorem prover + invocation during smoke test, defaults to 10. + /causalImplies + Translate Boogie's A ==> B into prover's A ==> A && B. + /typeEncoding:<m> + how to encode types when sending VC to theorem prover + n = none (unsound) + p = predicates (default) + a = arguments + m = monomorphic + /monomorphize + Do not abstract map types in the encoding (this is an + experimental feature that will not do the right thing if + the program uses polymorphism) + /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined + to be +, instead of +. + + ---- Verification-condition splitting -------------------------------------- + + /vcsMaxCost:<f> + VC will not be split unless the cost of a VC exceeds this + number, defaults to 2000.0. This does NOT apply in the + keep-going mode after first round of splitting. + /vcsMaxSplits:<n> + Maximal number of VC generated per method. In keep + going mode only applies to the first round. + Defaults to 1. + /vcsMaxKeepGoingSplits:<n> + If set to more than 1, activates the keep + going mode, where after the first round of splitting, + VCs that timed out are split into <n> pieces and retried + until we succeed proving them, or there is only one + assertion on a single path and it timeouts (in which + case error is reported for that assertion). + Defaults to 1. + /vcsKeepGoingTimeout:<n> + Timeout in seconds for a single theorem prover + invocation in keep going mode, except for the final + single-assertion case. Defaults to 1s. + /vcsFinalAssertTimeout:<n> + Timeout in seconds for the single last + assertion in the keep going mode. Defaults to 30s. + /vcsPathJoinMult:<f> + If more than one path join at a block, by how much + multiply the number of paths in that block, to accomodate + for the fact that the prover will learn something on one + paths, before proceeding to another. Defaults to 0.8. + /vcsPathCostMult:<f1> + /vcsAssumeMult:<f2> + The cost of a block is + (<assert-cost> + <f2>*<assume-cost>) * + (1.0 + <f1>*<entering-paths>) + <f1> defaults to 1.0, <f2> defaults to 0.01. + The cost of a single assertion or assumption is + currently always 1.0. + /vcsPathSplitMult:<f> + If the best path split of a VC of cost A is into + VCs of cost B and C, then the split is applied if + A >= <f>*(B+C), otherwise assertion splitting will be + applied. Defaults to 0.5 (always do path splitting if + possible), set to more to do less path splitting + and more assertion splitting. + /vcsDumpSplits + For split #n dump split.n.dot and split.n.bpl. + Warning: Affects error reporting. + /vcsCores:<n> + Try to verify <n> VCs at once. Defaults to 1. + /vcsLoad:<f> Sets vcsCores to the machine's ProcessorCount * f, + rounded to the nearest integer (where 0.0 <= f <= 3.0), + but never to less than 1. + + ---- Prover options -------------------------------------------------------- + + /errorLimit:<num> + Limit the number of errors produced for each procedure + (default is 5, some provers may support only 1) + /timeLimit:<num> + Limit the number of seconds spent trying to verify + each procedure + /errorTrace:<n> + 0 - no Trace labels in the error output, + 1 (default) - include useful Trace labels in error output, + 2 - include all Trace labels in the error output + /vcBrackets:<b> + bracket odd-charactered identifier names with |'s. <b> is: + 0 - no (default with non-/prover:Simplify), + 1 - yes (default with /prover:Simplify) + /prover:<tp> use theorem prover <tp>, where <tp> is either the name of + a DLL containing the prover interface located in the + Boogie directory, or a full path to a DLL containing such + an interface. The standard interfaces shipped include: + SMTLib (default, uses the SMTLib2 format and calls Z3) + Z3 (uses Z3 with the Simplify format) + Simplify + ContractInference (uses Z3) + Z3api (Z3 using Managed .NET API) + /proverOpt:KEY[=VALUE] + Provide a prover-specific option (short form /p). + /proverLog:<file> + Log input for the theorem prover. Like filenames + supplied as arguments to other options, <file> can use the + following macros: + @TIME@ expands to the current time + @PREFIX@ expands to the concatenation of strings given + by /logPrefix options + @FILE@ expands to the last filename specified on the + command line + In addition, /proverLog can also use the macro '@PROC@', + which causes there to be one prover log file per + verification condition, and the macro then expands to the + name of the procedure that the verification condition is for. + /logPrefix:<str> + Defines the expansion of the macro '@PREFIX@', which can + be used in various filenames specified by other options. + /proverLogAppend + Append (not overwrite) the specified prover log file + /proverWarnings + 0 (default) - don't print, 1 - print to stdout, + 2 - print to stderr + /proverMemoryLimit:<num> + Limit on the virtual memory for prover before + restart in MB (default:100MB) + /restartProver + Restart the prover after each query + /proverShutdownLimit<num> + Time between closing the stream to the prover and + killing the prover process (default: 0s) + /platform:<ptype>,<location> + ptype = v11,v2,cli1 + location = platform libraries directory + + Simplify specific options: + /simplifyMatchDepth:<num> + Set Simplify prover's matching depth limit + + Z3 specific options: + /z3opt:<arg> specify additional Z3 options + /z3multipleErrors + report multiple counterexamples for each error + /useArrayTheory + use Z3's native theory (as opposed to axioms). Currently + implies /monomorphize. + /useSmtOutputFormat + Z3 outputs a model in the SMTLIB2 format. + /z3types generate multi-sorted VC that make use of Z3 types + /z3lets:<n> 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA, + 3 - (default) any + /z3exe:<path> + path to Z3 executable + + CVC4 specific options: + /cvc4exe:<path> + path to CVC4 executable +"); + } + } +} |