From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/VCExp.cs | 476 +++++++++++++++++++++++++-------------------------- 1 file changed, 238 insertions(+), 238 deletions(-) (limited to 'Source/Core/VCExp.cs') diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index 87b8f3e6..63dca024 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -1,238 +1,238 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.IO; -using System.Collections; -using System.Collections.Generic; -using System.Reflection; -using System.Text; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -namespace Microsoft.Boogie { - - public class ProverOptions { - public class OptionException : Exception { - public OptionException(string msg) - : base(msg) { - Contract.Requires(msg != null); - } - } - - public string/*?*/ LogFilename = null; - public bool AppendLogFile = false; - public bool SeparateLogFiles = false; - // Say (DBG_WAS_VALID) or (DBG_WAS_INVALID) after query - public bool ForceLogStatus = false; - public int TimeLimit = 0; - public int MemoryLimit = 0; - public int Verbosity = 0; - public string ProverPath; - - private string/*!*/ stringRepr = ""; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(stringRepr != null); - } - - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return stringRepr; - } - - // The usual thing to override. - protected virtual bool Parse(string opt) { - Contract.Requires(opt != null); - return ParseString(opt, "LOG_FILE", ref LogFilename) || - ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) || - ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) || - ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) || - ParseInt(opt, "VERBOSITY", ref Verbosity) || - ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || - ParseString(opt, "PROVER_PATH", ref ProverPath); - // || base.Parse(opt) - } - - public virtual string Help - { - get - { - return -@" -Generic prover options : -~~~~~~~~~~~~~~~~~~~~~~~ -LOG_FILE= Log input for the theorem prover. The string @PROC@ in the filename - causes there to be one prover log file per verification condition, - and is expanded to the name of the procedure that the verification - condition is for. -APPEND_LOG_FILE= Append, rather than overwrite the log file. -MEMORY_LIMIT= Memory limit of the prover in megabytes. -VERBOSITY= The higher, the more verbose. -TIME_LIMIT= Time limit per verification condition in miliseconds. -PROVER_PATH= Path to the prover to use. - -The generic options may or may not be used by the prover plugin. -"; - - } - } - - public virtual void Parse(IEnumerable/*!*/ opts) { - Contract.Requires(cce.NonNullElements(opts)); - StringBuilder sb = new StringBuilder(stringRepr); - Contract.Assert(sb != null); - foreach (string/*!*/ opt in opts) { - Contract.Assert(opt != null); - if (!Parse(opt)) { - ReportError("Unrecognised prover option: " + opt); - } - sb.Append(opt).Append(" "); - } - stringRepr = sb.ToString(); - PostParse(); - } - - public virtual void PostParse() { - if (LogFilename != null && LogFilename.Contains("@PROC@")) { - SeparateLogFiles = true; - } - } - - protected void ReportError(string msg) { - Contract.Requires(msg != null); - throw new OptionException(msg + "\n\n" + Help); - } - - protected virtual bool ParseString(string opt, string name, ref string field) { - Contract.Requires(name != null); - Contract.Requires(opt != null); - if (opt.Length >= name.Length && opt.StartsWith(name)) { - if (opt.Length == name.Length) { - field = ""; - return true; - } else if (opt[name.Length] == '=' || opt[name.Length] == ':') { - field = opt.Substring(name.Length + 1); - return true; - } - } - return false; - } - - protected virtual bool ParseBool(string opt, string name, ref bool field) { - Contract.Requires(name != null); - Contract.Requires(opt != null); - string tmp = null; - if (ParseString(opt, name, ref tmp)) - switch (cce.NonNull(tmp).ToLower()) { - case "1": - case "true": - case "": - field = true; - return true; - case "0": - case "false": - field = false; - return true; - default: - ReportError("Invalid Boolean option \"" + opt + "\""); - return false; - } - return false; - } - - protected virtual bool ParseInt(string opt, string name, ref int field) { - Contract.Requires(name != null); - Contract.Requires(opt != null); - string tmp = null; - int t2; - if (ParseString(opt, name, ref tmp)) { - if (int.TryParse(cce.NonNull(tmp), out t2)) { - field = t2; - return true; - } else { - ReportError("Invalid integer option \"" + opt + "\""); - } - } - return false; - } - - public virtual TextWriter OpenLog(string/*?*/ descName) { - if (LogFilename != null) { - string filename = LogFilename; - Contract.Assert(filename != null); - if (descName != null) - filename = Helpers.SubstituteAtPROC(descName, filename); - return new StreamWriter(filename, AppendLogFile); - } else { - return null; - } - } - } - - [ContractClass(typeof(ProverFactoryContracts))] - public abstract class ProverFactory { - // Really returns ProverInterface. - //public abstract object! SpawnProver(ProverOptions! options, object! ctxt); - public abstract object SpawnProver(ProverOptions options, object ctxt); - - // Really returns ProverContext - public abstract object/*!*/ NewProverContext(ProverOptions/*!*/ options); - - public virtual ProverOptions BlankProverOptions() { - Contract.Ensures(Contract.Result() != null); - return new ProverOptions(); - } - - // return true if the prover supports DAG AST as opposed to LET AST - public virtual bool SupportsDags { - get { - return false; - } - } - - public virtual CommandLineOptions.VCVariety DefaultVCVariety { - get { - Contract.Ensures(Contract.Result() != CommandLineOptions.VCVariety.Unspecified); - return CommandLineOptions.VCVariety.DagIterative; - } - } - - public virtual bool SupportsLabels(ProverOptions options) { - return true; - } - - public virtual void Close() { - } - - public static ProverFactory Load(string proverName) { - Contract.Requires(proverName != null); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(cce.IsNew(Contract.Result()) && cce.Owner.New(Contract.Result())); - string/*!*/ path; - if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) { - path = proverName; - } else { - string codebase = cce.NonNull(System.IO.Path.GetDirectoryName( - cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location))); - path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll"); - } - Assembly asm = cce.NonNull(Assembly.LoadFrom(path)); - string name = cce.NonNull(asm.GetName().Name); - System.Type factoryType = cce.NonNull(asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory")); - return cce.NonNull((ProverFactory/*!*/)Activator.CreateInstance(factoryType)); - } - } - [ContractClassFor(typeof(ProverFactory))] - public abstract class ProverFactoryContracts : ProverFactory { - public override object NewProverContext(ProverOptions options) { - Contract.Requires(options != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using System.Reflection; +using System.Text; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +namespace Microsoft.Boogie { + + public class ProverOptions { + public class OptionException : Exception { + public OptionException(string msg) + : base(msg) { + Contract.Requires(msg != null); + } + } + + public string/*?*/ LogFilename = null; + public bool AppendLogFile = false; + public bool SeparateLogFiles = false; + // Say (DBG_WAS_VALID) or (DBG_WAS_INVALID) after query + public bool ForceLogStatus = false; + public int TimeLimit = 0; + public int MemoryLimit = 0; + public int Verbosity = 0; + public string ProverPath; + + private string/*!*/ stringRepr = ""; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(stringRepr != null); + } + + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return stringRepr; + } + + // The usual thing to override. + protected virtual bool Parse(string opt) { + Contract.Requires(opt != null); + return ParseString(opt, "LOG_FILE", ref LogFilename) || + ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) || + ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) || + ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) || + ParseInt(opt, "VERBOSITY", ref Verbosity) || + ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || + ParseString(opt, "PROVER_PATH", ref ProverPath); + // || base.Parse(opt) + } + + public virtual string Help + { + get + { + return +@" +Generic prover options : +~~~~~~~~~~~~~~~~~~~~~~~ +LOG_FILE= Log input for the theorem prover. The string @PROC@ in the filename + causes there to be one prover log file per verification condition, + and is expanded to the name of the procedure that the verification + condition is for. +APPEND_LOG_FILE= Append, rather than overwrite the log file. +MEMORY_LIMIT= Memory limit of the prover in megabytes. +VERBOSITY= The higher, the more verbose. +TIME_LIMIT= Time limit per verification condition in miliseconds. +PROVER_PATH= Path to the prover to use. + +The generic options may or may not be used by the prover plugin. +"; + + } + } + + public virtual void Parse(IEnumerable/*!*/ opts) { + Contract.Requires(cce.NonNullElements(opts)); + StringBuilder sb = new StringBuilder(stringRepr); + Contract.Assert(sb != null); + foreach (string/*!*/ opt in opts) { + Contract.Assert(opt != null); + if (!Parse(opt)) { + ReportError("Unrecognised prover option: " + opt); + } + sb.Append(opt).Append(" "); + } + stringRepr = sb.ToString(); + PostParse(); + } + + public virtual void PostParse() { + if (LogFilename != null && LogFilename.Contains("@PROC@")) { + SeparateLogFiles = true; + } + } + + protected void ReportError(string msg) { + Contract.Requires(msg != null); + throw new OptionException(msg + "\n\n" + Help); + } + + protected virtual bool ParseString(string opt, string name, ref string field) { + Contract.Requires(name != null); + Contract.Requires(opt != null); + if (opt.Length >= name.Length && opt.StartsWith(name)) { + if (opt.Length == name.Length) { + field = ""; + return true; + } else if (opt[name.Length] == '=' || opt[name.Length] == ':') { + field = opt.Substring(name.Length + 1); + return true; + } + } + return false; + } + + protected virtual bool ParseBool(string opt, string name, ref bool field) { + Contract.Requires(name != null); + Contract.Requires(opt != null); + string tmp = null; + if (ParseString(opt, name, ref tmp)) + switch (cce.NonNull(tmp).ToLower()) { + case "1": + case "true": + case "": + field = true; + return true; + case "0": + case "false": + field = false; + return true; + default: + ReportError("Invalid Boolean option \"" + opt + "\""); + return false; + } + return false; + } + + protected virtual bool ParseInt(string opt, string name, ref int field) { + Contract.Requires(name != null); + Contract.Requires(opt != null); + string tmp = null; + int t2; + if (ParseString(opt, name, ref tmp)) { + if (int.TryParse(cce.NonNull(tmp), out t2)) { + field = t2; + return true; + } else { + ReportError("Invalid integer option \"" + opt + "\""); + } + } + return false; + } + + public virtual TextWriter OpenLog(string/*?*/ descName) { + if (LogFilename != null) { + string filename = LogFilename; + Contract.Assert(filename != null); + if (descName != null) + filename = Helpers.SubstituteAtPROC(descName, filename); + return new StreamWriter(filename, AppendLogFile); + } else { + return null; + } + } + } + + [ContractClass(typeof(ProverFactoryContracts))] + public abstract class ProverFactory { + // Really returns ProverInterface. + //public abstract object! SpawnProver(ProverOptions! options, object! ctxt); + public abstract object SpawnProver(ProverOptions options, object ctxt); + + // Really returns ProverContext + public abstract object/*!*/ NewProverContext(ProverOptions/*!*/ options); + + public virtual ProverOptions BlankProverOptions() { + Contract.Ensures(Contract.Result() != null); + return new ProverOptions(); + } + + // return true if the prover supports DAG AST as opposed to LET AST + public virtual bool SupportsDags { + get { + return false; + } + } + + public virtual CommandLineOptions.VCVariety DefaultVCVariety { + get { + Contract.Ensures(Contract.Result() != CommandLineOptions.VCVariety.Unspecified); + return CommandLineOptions.VCVariety.DagIterative; + } + } + + public virtual bool SupportsLabels(ProverOptions options) { + return true; + } + + public virtual void Close() { + } + + public static ProverFactory Load(string proverName) { + Contract.Requires(proverName != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(cce.IsNew(Contract.Result()) && cce.Owner.New(Contract.Result())); + string/*!*/ path; + if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) { + path = proverName; + } else { + string codebase = cce.NonNull(System.IO.Path.GetDirectoryName( + cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location))); + path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll"); + } + Assembly asm = cce.NonNull(Assembly.LoadFrom(path)); + string name = cce.NonNull(asm.GetName().Name); + System.Type factoryType = cce.NonNull(asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory")); + return cce.NonNull((ProverFactory/*!*/)Activator.CreateInstance(factoryType)); + } + } + [ContractClassFor(typeof(ProverFactory))] + public abstract class ProverFactoryContracts : ProverFactory { + public override object NewProverContext(ProverOptions options) { + Contract.Requires(options != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + } +} -- cgit v1.2.3