diff options
Diffstat (limited to 'Source/Core/VCExp.cs')
-rw-r--r-- | Source/Core/VCExp.cs | 476 |
1 files changed, 238 insertions, 238 deletions
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<string>() != 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=<string> 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=<bool> Append, rather than overwrite the log file.
-MEMORY_LIMIT=<int> Memory limit of the prover in megabytes.
-VERBOSITY=<int> The higher, the more verbose.
-TIME_LIMIT=<int> Time limit per verification condition in miliseconds.
-PROVER_PATH=<string> Path to the prover to use.
-
-The generic options may or may not be used by the prover plugin.
-";
-
- }
- }
-
- public virtual void Parse(IEnumerable<string/*!*/>/*!*/ 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<ProverOptions>() != 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>() != 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<ProverFactory>() != null);
- Contract.Ensures(cce.IsNew(Contract.Result<ProverFactory>()) && cce.Owner.New(Contract.Result<ProverFactory>()));
- 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<object>() != 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<string>() != 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=<string> 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=<bool> Append, rather than overwrite the log file. +MEMORY_LIMIT=<int> Memory limit of the prover in megabytes. +VERBOSITY=<int> The higher, the more verbose. +TIME_LIMIT=<int> Time limit per verification condition in miliseconds. +PROVER_PATH=<string> Path to the prover to use. + +The generic options may or may not be used by the prover plugin. +"; + + } + } + + public virtual void Parse(IEnumerable<string/*!*/>/*!*/ 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<ProverOptions>() != 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>() != 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<ProverFactory>() != null); + Contract.Ensures(cce.IsNew(Contract.Result<ProverFactory>()) && cce.Owner.New(Contract.Result<ProverFactory>())); + 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<object>() != null); + + throw new NotImplementedException(); + } + } +} |