diff options
Diffstat (limited to 'Source/Core/VCExp.ssc')
| -rw-r--r-- | Source/Core/VCExp.ssc | 190 |
1 files changed, 190 insertions, 0 deletions
diff --git a/Source/Core/VCExp.ssc b/Source/Core/VCExp.ssc new file mode 100644 index 00000000..4b42a639 --- /dev/null +++ b/Source/Core/VCExp.ssc @@ -0,0 +1,190 @@ +//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+
+namespace Microsoft.Boogie {
+
+ public class ProverOptions
+ {
+ public class OptionException : Exception {
+ public OptionException(string! msg) { base(msg); }
+ }
+
+ 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 CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;
+ public int Verbosity = 0;
+
+ private string! stringRepr = "";
+
+ [Pure]
+ public override string! ToString()
+ {
+ return stringRepr;
+ }
+
+ // The usual thing to override.
+ protected virtual bool Parse(string! opt)
+ {
+ 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);
+ // || base.Parse(opt)
+ }
+
+ public virtual void Parse(List<string!>! opts)
+ {
+ StringBuilder! sb = new StringBuilder(stringRepr);
+ foreach (string! opt in opts) {
+ if (!Parse(opt)) {
+ ReportError("Unrecognised prover option: " + opt);
+ }
+ sb.Append(opt).Append(" ");
+ }
+ stringRepr = sb.ToString();
+ PostParse();
+ }
+
+ protected virtual void PostParse()
+ {
+ if (LogFilename != null && LogFilename.Contains("@PROC@")) {
+ SeparateLogFiles = true;
+ }
+ }
+
+ protected void ReportError(string! msg)
+ {
+ throw new OptionException(msg);
+ }
+
+ protected virtual bool ParseString(string! opt, string! name, ref string field)
+ {
+ if (opt.Length >= name.Length && opt.StartsWith(name)) {
+ if (opt.Length == name.Length) {
+ field = "";
+ return true;
+ } else if (opt[name.Length] == '=') {
+ field = opt.Substring(name.Length + 1);
+ return true;
+ }
+ }
+ return false;
+ }
+
+ protected virtual bool ParseBool(string! opt, string! name, ref bool field)
+ {
+ string tmp = null;
+ if (ParseString(opt, name, ref tmp))
+ switch (((!)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)
+ {
+ string tmp = null;
+ int t2;
+ if (ParseString(opt, name, ref tmp)) {
+ if (int.TryParse((!)tmp, out t2)) {
+ field = t2;
+ return true;
+ } else {
+ ReportError("Invalid integer option \"" + opt + "\"");
+ }
+ }
+ return false;
+ }
+
+ static int sequenceNumber = 0;
+ public virtual TextWriter? OpenLog(string/*?*/ descName)
+ {
+ if (LogFilename != null) {
+ string! filename = LogFilename;
+ if (descName != null)
+ filename = Helpers.SubstituteAtPROC(descName, filename);
+ return new StreamWriter(filename, AppendLogFile);
+ } else {
+ return null;
+ }
+ }
+ }
+
+ public abstract class ProverFactory
+ {
+ // Really returns ProverInterface.
+ public abstract object! SpawnProver(ProverOptions! options, object! ctxt);
+
+ // Really returns ProverContext
+ public abstract object! NewProverContext(ProverOptions! options);
+
+ public virtual ProverOptions! BlankProverOptions()
+ {
+ 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
+ ensures result != CommandLineOptions.VCVariety.Unspecified;
+ { return CommandLineOptions.VCVariety.Dag; }
+ }
+
+ public virtual void Close()
+ {
+ }
+
+ public static ProverFactory! Load(string! proverName)
+ ensures result.IsNew && Microsoft.Contracts.Owner.New(result);
+ {
+ string! path;
+ if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) {
+ path = proverName;
+ } else {
+ string! codebase = (!) System.IO.Path.GetDirectoryName(
+ (!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll");
+ }
+ Assembly asm = (!)Assembly.LoadFrom(path);
+ string name = (!)asm.GetName().Name;
+ System.Type factoryType = (!)asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory");
+ return (ProverFactory!)Activator.CreateInstance(factoryType);
+ }
+ }
+}
|