diff options
author | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-10-03 12:32:19 -0700 |
---|---|---|
committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-10-03 12:32:19 -0700 |
commit | 8d7686cd88736d117e37eb9bf9dd17404a294ff4 (patch) | |
tree | 2d642b239ae7afcc7fb73fdda2881b6cbd008b64 /Source/Provers | |
parent | 2232875cd561e0ffe412cdb5cb5acd05b1ef2a3a (diff) |
bunch of refactorings
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/Simplify/Let2ImpliesVisitor.cs | 236 | ||||
-rw-r--r-- | Source/Provers/Simplify/Prover.cs | 656 | ||||
-rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 868 | ||||
-rw-r--r-- | Source/Provers/Simplify/Simplify.csproj | 210 | ||||
-rw-r--r-- | Source/Provers/Simplify/cce.cs | 193 | ||||
-rw-r--r-- | Source/Provers/Z3/Inspector.cs | 162 | ||||
-rw-r--r-- | Source/Provers/Z3/Prover.cs | 937 | ||||
-rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 427 | ||||
-rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 398 | ||||
-rw-r--r-- | Source/Provers/Z3/Z3.csproj | 218 | ||||
-rw-r--r-- | Source/Provers/Z3/cce.cs | 193 |
11 files changed, 0 insertions, 4498 deletions
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.cs b/Source/Provers/Simplify/Let2ImpliesVisitor.cs deleted file mode 100644 index 9b8328d1..00000000 --- a/Source/Provers/Simplify/Let2ImpliesVisitor.cs +++ /dev/null @@ -1,236 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Simplify
-{
- // Simplify does not understand the LET operator, so we have to replace
- // it with implications (previously, this was done in the VCExprGenerator), or
- // we have to apply the let as a substitution (in the case of terms)
-
- // This visitor expects that let-bindings are sorted, so that bound
- // variables only occur after their declaration
-
- public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
-
- public Let2ImpliesMutator(VCExpressionGenerator gen) :base(gen) {
- Contract.Requires(gen!=null);
- this.keepLetFormula = this.keepLetTerm = false;
- }
-
- public Let2ImpliesMutator(VCExpressionGenerator gen, bool keepLetTerm, bool keepLetFormula):base(gen) {
- Contract.Requires(gen!=null);
-
- this.keepLetTerm = keepLetTerm;
- this.keepLetFormula = keepLetFormula;
- }
-
- readonly bool keepLetTerm;
- readonly bool keepLetFormula;
-
- public VCExpr Mutate(VCExpr expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- return Mutate(expr, new VCExprSubstitution ());
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- private int polarity = 1; // 1 for positive, -1 for negative, 0 for both
-
- // we also track which variables occur in positive, negative, or
- // in both positions (to decide whether implications or equations
- // have to be used to define such a variable)
- private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
- private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
- switch(o1) {
- case OccurrenceTypes.None: return o2;
- case OccurrenceTypes.Pos:
- switch(o2) {
- case OccurrenceTypes.None:
- case OccurrenceTypes.Pos:
- return OccurrenceTypes.Pos;
- default:
- return OccurrenceTypes.PosNeg;
- }
- case OccurrenceTypes.Neg:
- switch(o2) {
- case OccurrenceTypes.None:
- case OccurrenceTypes.Neg:
- return OccurrenceTypes.Neg;
- default:
- return OccurrenceTypes.PosNeg;
- }
- default:
- return OccurrenceTypes.PosNeg;
- }
- }
-
- private IDictionary<VCExprVar/*!*/, OccurrenceTypes>/*!*/ VarOccurrences =
- new Dictionary<VCExprVar/*!*/, OccurrenceTypes>();
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(VarOccurrences != null);
-}
-
- ////////////////////////////////////////////////////////////////////////////
-
- public override VCExpr Visit(VCExprVar node,
- VCExprSubstitution substitution) {
- Contract.Requires(node!= null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr res = base.Visit(node, substitution);
- Contract.Assert(res!=null);
-
- VCExprVar resAsVar = res as VCExprVar;
- if (resAsVar != null) {
- OccurrenceTypes occ;
- if (polarity > 0)
- occ = OccurrenceTypes.Pos;
- else if (polarity < 0)
- occ = OccurrenceTypes.Neg;
- else
- occ = OccurrenceTypes.PosNeg;
-
- OccurrenceTypes oldOcc;
- if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
- occ = Union(occ, oldOcc);
- VarOccurrences[resAsVar] = occ;
- }
-
- return res;
- }
-
- public override VCExpr Visit(VCExprNAry node,
- VCExprSubstitution substitution) {
- Contract.Requires(node != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- // track the polarity to ensure that no implications are introduced
- // in negative positions
- // UGLY: the code for tracking polarities should be factored out
- // (similar code is used in the TypeEraser)
-
- VCExpr res;
- if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
- polarity = -polarity;
- res = base.Visit(node, substitution);
- polarity = -polarity;
- } else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
- polarity = -polarity;
- VCExpr newArg0 = Mutate(node[0], substitution);
- Contract.Assert(newArg0 != null);
- polarity = -polarity;
- VCExpr newArg1 = Mutate(node[1], substitution);
- Contract.Assert(newArg1 != null);
-
- res = Gen.Implies(newArg0, newArg1);
- } else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
- !node.Op.Equals(VCExpressionGenerator.OrOp) &&
- !(node.Op is VCExprLabelOp)) {
- // standard is to set the polarity to 0 (fits most operators)
- int oldPolarity = polarity;
- polarity = 0;
- res = base.Visit(node, substitution);
- polarity = oldPolarity;
- } else {
- res = base.Visit(node, substitution);
- }
-
- return res;
- }
-
- public override VCExpr Visit(VCExprLet originalNode,
- VCExprSubstitution substitution) {
- Contract.Requires(originalNode != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- // first sort the bindings to be able to apply substitutions
- LetBindingSorter letSorter = new LetBindingSorter (Gen);
- Contract.Assert(letSorter != null);
- VCExpr newNode = letSorter.Mutate(originalNode, true);
- Contract.Assert(newNode != null);
- VCExprLet node = newNode as VCExprLet;
-
- if (node == null)
- // it can happen that the complete let-expressions gets eliminated by the
- // sorter, which also checks whether let-bindings are actually used
- return newNode;
-
- substitution.PushScope(); try {
-
- // the bindings that remain and that are later handled using an implication
- List<VCExprLetBinding> bindings = new List<VCExprLetBinding> ();
- List<VCExprLetBinding> keepBindings = new List<VCExprLetBinding> ();
-
- foreach (VCExprLetBinding binding in node) {
- Contract.Assert(binding != null);
- // in all cases we apply the substitution up to this point
- // to the bound formula
- VCExpr newE = Mutate(binding.E, substitution);
- Contract.Assert(newE != null);
- if (binding.V.Type.IsBool) {
- // a bound formula is handled using an implication; we introduce
- // a fresh variable to avoid clashes
- Contract.Assert( polarity > 0);
-
- if (keepLetFormula) {
- keepBindings.Add(Gen.LetBinding(binding.V, newE));
-
- } else {
- VCExprVar newVar = Gen.Variable(binding.V.Name, Type.Bool);
- Contract.Assert(newVar != null);
- substitution[binding.V] = newVar;
-
- bindings.Add(Gen.LetBinding(newVar, newE));
- }
- } else {
- if (keepLetTerm) {
- keepBindings.Add(Gen.LetBinding(binding.V, newE));
- } else {
- // a bound term is substituted
- substitution[binding.V] = newE;
- }
- }
- }
-
- VCExpr newBody = Mutate(node.Body, substitution);
- Contract.Assert(newBody != null);
- if (keepBindings.Count > 0) {
- newBody = Gen.Let(keepBindings, newBody);
- }
-
- // Depending on the places where the variable occurs, we would
- // have to introduce implications or equations to define the
- // bound variables. For the time being, we just assert that all
- // occurrences are positive
- foreach (VCExprLetBinding b in bindings) {
- Contract.Assert(b != null);
- OccurrenceTypes occ;
- if (VarOccurrences.TryGetValue(b.V, out occ))
- Contract.Assert( occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos);
- }
-
- return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
-
- } finally {
- substitution.PopScope();
- }
- }
- }
-
-}
\ No newline at end of file diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs deleted file mode 100644 index 3faa18e1..00000000 --- a/Source/Provers/Simplify/Prover.cs +++ /dev/null @@ -1,656 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Collections;
-using System.Collections.Generic;
-//using util;
-using Microsoft.Boogie;
-
-// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
-namespace Microsoft.Boogie.Simplify {
- /// <summary>
- /// An interface to Simplify theorem prover.
- /// </summary>
- ///
- [ContractClass(typeof(ProverProcessContracts))]
- public abstract class ProverProcess {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(simplify != null);
- Contract.Invariant(fromSimplify != null);
- Contract.Invariant(toSimplify != null);
- Contract.Invariant(fromStdError != null);
- }
-
- [Rep]
- protected readonly Process simplify;
-
- [Rep]
- readonly TextReader fromSimplify;
- [Rep]
- readonly TextWriter toSimplify;
- [Rep]
- readonly TextReader fromStdError;
-
- protected bool readTimedOut;
-
- int nFormulasChecked = 0;
- public int NumFormulasChecked {
- get {
- return nFormulasChecked;
- }
- }
-
- // Note: In the Everett build (.NET framework < 2.0), Process.PeakVirtualMemorySize64
- // is not defined, but rather a version that returns an 'int' rather than a 'long'.
- public long PeakVirtualMemorySize {
- [NoDefaultContract]
- get
- //modifies this.*;
- {
- Contract.Requires(cce.IsPeerConsistent(this));
- try {
- cce.BeginExpose(this);
- simplify.Refresh();
-#if WHIDBEY
- return simplify.PeakVirtualMemorySize64;
-#else
- return simplify.PeakPagedMemorySize64;
-#endif
- } finally {
- cce.EndExpose();
- }
- }
- }
-
- public bool HasExited {
- get {
- return simplify.HasExited;
- }
- }
-
- public ProverProcess(ProcessStartInfo psi, string proverPath) { // throws ProverException
- Contract.Requires(psi != null);
- Contract.Requires(proverPath != null);
- try {
- Process simplify = Process.Start(psi);
- this.simplify = simplify;
- fromSimplify = simplify.StandardOutput;
- toSimplify = simplify.StandardInput;
- fromStdError = simplify.StandardError;
- } catch (System.ComponentModel.Win32Exception e) {
- throw new ProverException(string.Format("Unable to start the process {0}: {1}", proverPath, e.Message));
- }
- // base();
- }
-
- public abstract string OptionComments();
-
- //[Pure(false)]
- public virtual IEnumerable<string/*!>!*/> ParameterSettings {
- get {
- yield break;
- }
- }
-
- public void Close()
- //modifies this.*;
- {
- cce.BeginExpose(this);
- {
- toSimplify.Flush();
- if (this.simplify != null) {
- if (!simplify.HasExited) {
- this.Kill();
- }
- simplify.Close();
- }
- }
- cce.EndExpose();
- }
-
- [NoDefaultContract] // this method assumes nothing about the object, other than that it has been constructed (which means simplify!=null)
- [Verify(false)] // The call simplify.Kill will require simplify.IsPeerConsistent, but since we don't know the state of "this" and "simplify", we cannot afford the run-time check that an assume statement here would impose
- public void Kill() {
- try {
- if (CommandLineOptions.Clo.ProverShutdownLimit > 0) {
- toSimplify.Close();
- for (int i = 0; !simplify.HasExited && i <= CommandLineOptions.Clo.ProverShutdownLimit * 1000; i += 100) {
- System.Threading.Thread.Sleep(100);
- }
- }
- if (!simplify.HasExited) {
- simplify.Kill();
- }
- } catch (InvalidOperationException) { /* already exited */
- } catch (System.ComponentModel.Win32Exception) { /* already exiting */
- }
- }
-
- public virtual void AddAxioms(string s)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- toSimplify.Write("(BG_PUSH ");
- toSimplify.Write(s);
- toSimplify.WriteLine(")");
- cce.EndExpose();
- }
-
- public virtual void Feed(string s, int statementCount)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- toSimplify.Write(s);
- }
- cce.EndExpose();
- }
-
- public virtual void PopAxioms()
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- toSimplify.WriteLine("(BG_POP)");
- }
- cce.EndExpose();
- }
-
- public void ToFlush()
- //modifies this.*;
- {
- cce.BeginExpose(this);
- {
- toSimplify.Flush();
- }
- cce.EndExpose();
- }
-
- public enum ProverOutcome {
- Valid,
- NotValid,
- TimeOut,
- OutOfMemory,
- Inconclusive
- }
-
- /// <summary>
- /// Passes the formula to Simplify.
- /// </summary>
- public void BeginCheck(string descriptiveName, string formula)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(formula != null);
- DoBeginCheck(descriptiveName, formula);
- nFormulasChecked++;
- }
-
- /// <summary>
- /// Reports the outcome of formula checking. If the outcome is Invalid,
- /// then the "handler" is invoked with each counterexample.
- /// </summary>
- public abstract ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler);
- //modifies this.**;
- //modifies Console.Out.*, Console.Error.*;
- //modifies handler.*;
-
- protected abstract void DoBeginCheck(string descriptiveName, string formula);
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
-
- /// <summary>
- /// Returns an array of the labels in "labels", with "|" brackets (if any)
- /// stripped off.
- /// Assumes that every label begins with "|+" or "|@", or just "+" or "@",
- /// and ends with "|" if it started with one, and that these "|" brackets are
- /// the only "|"s in "labels".
- /// </summary>
- protected static List<string/*!>!*/> ParseLabels(string labels) {
- Contract.Requires(labels != null);
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- List<string> list = new List<string>();
- int j = 0;
- while (true)
- // invariant: j is the number of characters of "labels" consumed so far
- // invariant: an even number of '|' characters remain in "labels"
- {
- cce.LoopInvariant(0 <= j && j <= labels.Length);
- j = labels.IndexOfAny(new char[] { '|', '+', '@' }, j);
- if (j < 0) {
- // no more labels
- return list;
- }
- char ch = labels[j];
- if (ch == '|') {
- j++; // skip the '|'
- Contract.Assume(j < labels.Length); // there should now be a '+' or '@'
- ch = labels[j];
- }
- Contract.Assume(ch == '+' || ch == '@');
- j++; // skip the '+' or '@'
- int k = labels.IndexOfAny(new char[] { '|', ' ', ')' }, j);
- Contract.Assume(j + 2 <= k);
- string s = labels.Substring(j, k - j);
- list.Add(s);
- j = k + 1;
- }
- }
-
- [Rep]
- char[] expectBuffer = null;
-
- /// <summary>
- /// Expects s[0]==ch and the next s.Length-1 characters of the input to be s[1,..]
- /// If not, more characters may be read from "fromSimplify" to provide additional context
- /// for the UnexpectedProverOutputException exception that will be thrown.
- /// </summary>
- protected void Expect(int ch, string s)
- //modifies this.*;
- {
- Contract.Requires(s != null);
- Contract.Requires(1 <= s.Length);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- if (ch == -1) {
- // a return of -1 from FromReadChar means that there is no StdOutput
- // to treat this we can return the error message we get from Z3 on StdError and then
- // declare this case to be inconclusive
- string str = FromStdErrorAll();
- if (str == "") {
- throw new ProverDiedException();
- } else {
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + str + "<<<end>>>");
- }
- }
-
- string badInputPrefix;
- if (ch != s[0]) {
- badInputPrefix = Char.ToString((char)ch);
- } else {
- int len = s.Length - 1;
- if (expectBuffer == null || expectBuffer.Length < len) {
- cce.BeginExpose(this);
- {
- expectBuffer = new char[len];
- }
- cce.EndExpose();
- }
- try {
- string s0;
- cce.BeginExpose(this);
- {
- fromSimplify.ReadBlock(expectBuffer, 0, len);
- s0 = new string(expectBuffer, 0, len);
- }
- cce.EndExpose();
- string s1 = s.Substring(1, len);
- if (s0.CompareTo(s1) == 0) {
- badInputPrefix = null; // no error
- } else {
- badInputPrefix = (char)ch + s0;
- }
- } catch (IOException) {
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", encountered IO exception.");
- }
- }
-
- if (badInputPrefix != null) {
- // Read the rest of the available input, without blocking!
- // Despite the confusing documentation for the Read method, it seems
- // that Read does block. It if didn't, I would have written:
- // string remaining = "";
- // char[] buf = new char[1024];
- // while (true) {
- // int len = fromSimplify.Read(buf, 0, buf.Length);
- // remaining += new String(buf, 0, len);
- // if (len != buf.Length) {
- // break;
- // }
- // }
- // But instead, I'll just hope that one line of input is available and read
- // it.
- string remaining = fromSimplify.ReadLine() + "\r\n";
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + badInputPrefix + remaining + "<<<end>>>");
- }
- }
-
- protected int FromReadChar()
- //modifies this.*;
- {
- try {
- cce.BeginExpose(this);
- return fromSimplify.Read();
- } finally {
- cce.EndExpose();
- }
- }
-
- private void KillProver(object state) {
- cce.BeginExpose(this);
- {
- this.readTimedOut = true;
- simplify.Kill();
- }
- cce.EndExpose();
- }
-
- protected int FromReadChar(int timeout)
- //modifies this.*;
- {
- Contract.Requires(-1 <= timeout);
- try {
- cce.BeginExpose(this);
- this.readTimedOut = false;
- System.Threading.Timer t = new System.Threading.Timer(this.KillProver, null, timeout, System.Threading.Timeout.Infinite);
- int ch = fromSimplify.Read();
- t.Change(System.Threading.Timeout.Infinite, System.Threading.Timeout.Infinite);
- t.Dispose();
- return ch;
- } finally {
- cce.EndExpose();
- }
- }
-
- protected string FromReadLine()
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<string>() != null);
- try {
- cce.BeginExpose(this);
- string s = fromSimplify.ReadLine();
- if (s == null) {
- // this is what ReadLine returns if all characters have been read
- s = "";
- }
- return s;
- } finally {
- cce.EndExpose();
- }
- }
-
- protected string FromStdErrorAll()
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<string>() != null);
-
- try {
- cce.BeginExpose(this);
- if (fromStdError != null) {
- string s = fromStdError.ReadToEnd();
- if (s == null) {
- // this is what ReadLine returns if all characters have been read
- s = "";
- }
- return s;
- } else {
- // there is no StdErrorReader available
- return "";
- }
- } finally {
- cce.EndExpose();
- }
- }
-
- protected void ToWriteLine(string s)
- //modifies this.*;
- {
- Contract.Requires(s != null);
- cce.BeginExpose(this);
- {
- toSimplify.WriteLine(s);
- }
- cce.EndExpose();
- }
- }
- [ContractClassFor(typeof(ProverProcess))]
- public abstract class ProverProcessContracts : ProverProcess {
- private ProverProcessContracts() : base(null, null) { }
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
- throw new NotImplementedException();
- }
-
- public override ProverProcess.ProverOutcome CheckOutcome(ProverInterface.ErrorHandler handler) {
- Contract.Requires(handler != null);
- throw new NotImplementedException();
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(formula != null);
- throw new NotImplementedException();
- }
- }
- // derived by Z3ProverProcess
- public class SimplifyProverProcess : ProverProcess {
- public SimplifyProverProcess(string proverPath, bool dummy) :base(getPSI(proverPath),proverPath) {
- Contract.Requires(proverPath != null);
- // throws ProverException
- }
- private static ProcessStartInfo getPSI(string proverPath){ProcessStartInfo psi = new ProcessStartInfo(proverPath, "-labelsonly");
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = true;
- Contract.Assume(psi.EnvironmentVariables != null); // by inspecting the code through Reflector; the documentation says this property is "null by default", whatever that means --KRML
- if (0 <= CommandLineOptions.Clo.ProverKillTime) {
- psi.EnvironmentVariables["PROVER_KILL_TIME"] = CommandLineOptions.Clo.ProverKillTime.ToString();
- }
- if (0 <= CommandLineOptions.Clo.SimplifyProverMatchDepth) {
- psi.EnvironmentVariables["PROVER_MATCH_DEPTH"] = CommandLineOptions.Clo.SimplifyProverMatchDepth.ToString();
- }
- if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
- psi.EnvironmentVariables["PROVER_CC_LIMIT"] = CommandLineOptions.Clo.ProverCCLimit.ToString();
- }
- return psi;
- }
-
-
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- // would we want the timeout stuff here?
- return "";
- }
-
- [NotDelayed]
- // TODO it complains about things not beeing peer consistent upon call to EatPrompt()
- // not sure what is it about... --micmo
- [Verify(false)]
- public SimplifyProverProcess(string proverPath):base(getPSI(proverPath),proverPath)
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(proverPath != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- EatPrompt();
- }
-
- private void EatPrompt()
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- // skips text matching the regular expression: (white space)* ">\t"
- ToFlush();
-
- int ch = 0;
- do {
- ch = FromReadChar();
- } while (Char.IsWhiteSpace((char)ch));
-
- while (ch == 'W') {
- ch = ConsumeWarnings(ch, null);
- }
-
- Expect(ch, ">\t");
- }
-
- public override void AddAxioms(string s) {
- //Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ToWriteLine("(PROMPT_OFF)");
- base.AddAxioms(s);
- //ToWriteLine("(PROMPT_ON)");
- EatPrompt();
- }
-
- public override void Feed(string s, int statementCount) {
- //Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ToWriteLine("(PROMPT_OFF)");
- base.Feed(s, statementCount);
- //ToWriteLine("(PROMPT_ON)");
- for (int i = 0; i < statementCount; i++) {
- EatPrompt();
- }
- }
-
- public override void PopAxioms() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- base.PopAxioms();
- EatPrompt();
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(formula != null);
- //simplify.Refresh();
- //this.Comment("@@@@ Virtual Memory: " + simplify.PeakVirtualMemorySize64);
- //this.Comment("@@@@ Working Set: " + simplify.PeakWorkingSet64);
- //this.Comment("@@@@ Paged Memory: " + simplify.PeakPagedMemorySize64);
-
- ToWriteLine(formula);
- ToFlush();
- }
-
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- ProverOutcome outcome;
-
- if (this.simplify == null) {
- return ProverOutcome.Inconclusive;
- }
-
- int ch = FromReadChar();
- while (ch == 'W') {
- ch = ConsumeWarnings(ch, handler);
- }
- if (ch == 'E') {
- Expect(ch, "Exceeded PROVER_KILL_TIME -- discontinuing search for counterexamples.");
- FromReadLine();
- ch = FromReadChar();
- if (ch == '\n') {
- ch = FromReadChar();
- }
- Expect(ch, " labels:");
- FromReadLine();
- ch = FromReadChar();
- ch = FromReadChar();
- ch = FromReadChar();
- FromReadLine();
- ch = FromReadChar();
- ch = FromReadChar();
- ch = FromReadChar();
- return ProverOutcome.TimeOut;
- }
- if ('0' <= ch && ch <= '9') {
- // Valid!
- do {
- ch = FromReadChar();
- } while ('0' <= ch && ch <= '9');
- Expect(ch, ": Valid.");
- outcome = ProverOutcome.Valid;
- ToWriteLine(String.Format("; FORMULA {0} IS VALID!", NumFormulasChecked + 1 /*Simplify starts at 1*/));
- } else {
- // now we expect one or more counterexample contexts, each proving a list of labels
- do {
- List<string> labels = ReadLabels(ch);
- handler.OnModel(labels, null);
- ch = FromReadChar();
- } while (ch == 'C');
- // now we expect "<N>: Invalid" where <N> is some number
- while ('0' <= ch && ch <= '9') {
- ch = FromReadChar();
- }
- Expect(ch, ": Invalid.");
- outcome = ProverOutcome.NotValid;
- ToWriteLine(String.Format("; FORMULA {0} IS INVALID", NumFormulasChecked + 1 /*Simplify starts at 1*/));
- }
-
- EatPrompt();
- return outcome;
- }
-
- List<string/*!>!*/> ReadLabels(int ch)
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Expect(ch, "Counterexample:\n"); // FIX! ? Is there a problem with \r\n here?
- ch = FromReadChar();
- List<string> theLabels;
- if (ch == ' ') {
- // there are labels
- Expect(ch, " labels: ");
- string labels = FromReadLine(); // reads "(A B C ...)\n"
- theLabels = ParseLabels(labels);
- ch = FromReadChar();
- } else {
- theLabels = new List<string>();
- }
- Expect(ch, "\n"); // empty line
-
- return theLabels;
- }
-
- int ConsumeWarnings(int ch, Microsoft.Boogie.ProverInterface.ErrorHandler handler)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(ch == 'W');
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Expect(ch, "Warning: ");
- string w = FromReadLine();
- if (w.StartsWith("triggerless quantifier body")) {
- FromReadLine(); // blank line
- w = "triggerless quantifier body: " + FromReadLine(); // expression (body)
- FromReadLine(); // blank line
- FromReadLine(); // "with X pattern variable(s)...
- FromReadLine(); // blank line
- FromReadLine(); // expression (entire quantifier)
- }
-
- if (handler != null)
- handler.OnProverWarning(w);
-
- ch = FromReadChar();
- if (ch == '\n') {
- // make up for a poorly designed ReadLine routine (only the first
- // character of the DOS end-of-line sequence "\r\n" is read)
- ch = FromReadChar();
- }
- return ch;
- }
- }
-
-}
\ No newline at end of file diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs deleted file mode 100644 index 4584b2e7..00000000 --- a/Source/Provers/Simplify/ProverInterface.cs +++ /dev/null @@ -1,868 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Text;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.TypeErasure;
-using System.Text.RegularExpressions;
-
-namespace Microsoft.Boogie.Simplify {
- public abstract class LogProverInterface : ProverInterface {
- [NotDelayed]
- protected LogProverInterface(ProverOptions options,
- string openComment, string closeComment,
- string openActivity, string closeActivity,
- VCExpressionGenerator gen) {
- Contract.Requires(options != null);
- Contract.Requires(openComment != null);
- Contract.Requires(closeComment != null);
- Contract.Requires(openActivity != null);
- Contract.Requires(closeActivity != null);
- Contract.Requires(gen != null);
- Contract.Ensures(this.gen == gen);
- if (options.SeparateLogFiles) {
- this.commonPrefix = new List<string>();
- } else {
- this.logFileWriter = options.OpenLog(null);
- }
- this.openCommentString = openComment;
- this.closeCommentString = closeComment;
- this.openActivityString = openActivity;
- this.closeActivityString = closeActivity;
- this.gen = gen;
- this.options = options;
-
- if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
- // Emit version comment in the log
- LogCommonComment(CommandLineOptions.Clo.Version);
- LogCommonComment(CommandLineOptions.Clo.Environment);
- }
- }
-
- [StrictReadonly]
- [Additive]
- protected readonly VCExpressionGenerator gen;
-
- private TextWriter/*?*/ logFileWriter;
- [StrictReadonly]
- private readonly string openCommentString;
- [StrictReadonly]
- private readonly string closeCommentString;
- [StrictReadonly]
- private readonly string openActivityString;
- [StrictReadonly]
- private readonly string closeActivityString;
- [StrictReadonly]
- protected readonly ProverOptions options;
- [StrictReadonly]
- private readonly List<string>/*?*/ commonPrefix;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(openCommentString != null);
- Contract.Invariant(closeCommentString != null);
- Contract.Invariant(openActivityString != null);
- Contract.Invariant(closeActivityString != null);
- Contract.Invariant(options != null);
- Contract.Invariant(commonPrefix == null || cce.NonNullElements(commonPrefix));
- }
-
-
- public void LogActivity(string s) {
- Contract.Requires(s != null);
- LogActivity(s, false);
- }
-
- public void LogCommon(string s) {
- Contract.Requires(s != null);
- LogActivity(s, true);
- }
-
- private void LogActivity(string s, bool common) {
- Contract.Requires(s != null);
- Contract.Assume(common || !options.SeparateLogFiles || logFileWriter != null);
- if (logFileWriter != null) {
- logFileWriter.Write(openActivityString);
- logFileWriter.Write(s);
- logFileWriter.WriteLine(closeActivityString);
- logFileWriter.Flush();
- }
- if (common && commonPrefix != null) {
- commonPrefix.Add(openActivityString + s + closeActivityString);
- }
- }
-
- /// <summary>
- /// Write "comment" to logfile, if any, formatted as a comment for the theorem prover at hand.
- /// Assumes that "comment" does not contain any characters that would prematurely terminate
- /// the comment (like, perhaps, a newline or "*/").
- /// </summary>
- public override void LogComment(string comment) {
- //Contract.Requires(comment != null);
- LogComment(comment, false);
- }
-
- public void LogCommonComment(string comment) {
- Contract.Requires(comment != null);
- LogComment(comment, true);
- }
-
- private void LogComment(string comment, bool common) {
- Contract.Requires(comment != null);
- Contract.Assume(common || !options.SeparateLogFiles || logFileWriter != null);
- if (logFileWriter != null) {
- logFileWriter.Write(openCommentString);
- logFileWriter.Write(comment);
- logFileWriter.WriteLine(closeCommentString);
- logFileWriter.Flush();
- }
- if (common && commonPrefix != null) {
- commonPrefix.Add(openCommentString + comment + closeCommentString);
- }
- }
-
- public virtual void NewProblem(string descName) {
- Contract.Requires(descName != null);
- if (commonPrefix != null) {
- if (logFileWriter != null) {
- logFileWriter.Close();
- }
- logFileWriter = options.OpenLog(descName);
- if (logFileWriter != null) {
- foreach (string s in commonPrefix) {
- Contract.Assert(s != null);
- logFileWriter.WriteLine(s);
- }
- }
- }
- LogComment("Proof obligation: " + descName);
- }
-
- public override void Close() {
- if (logFileWriter != null) {
- logFileWriter.Close();
- logFileWriter = null;
- }
- }
-
- public override VCExpressionGenerator VCExprGen {
- get {
- Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
- return this.gen;
- }
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- [ContractClass(typeof(ProcessTheoremProverContracts))]
- public abstract class ProcessTheoremProver : LogProverInterface {
- private static string _proverPath;
-
- protected AxiomVCExprTranslator vcExprTranslator {
- get {
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return cce.NonNull((AxiomVCExprTranslator)ctx.exprTranslator);
- }
- }
-
- protected abstract AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p);
-
- // Return the number of axioms pushed to the theorem prover
- protected int FeedNewAxiomsDecls2Prover() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- if (thmProver == null)
- return 0;
- int ret = 0;
- foreach (string s in vcExprTranslator.NewTypeDecls) {
- Contract.Assert(s != null);
- LogCommon(s);
- thmProver.Feed(s, 0);
- }
- foreach (string s in vcExprTranslator.NewAxioms) {
- Contract.Assert(s != null);
- LogBgPush(s);
- thmProver.AddAxioms(s);
- ret++;
- }
- return ret;
- }
-
- protected static string CodebaseString() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(BackgroundPredicates));
- Contract.Invariant(BackgroundPredFilename != null);
- Contract.Invariant(ctx != null);
- }
-
- private static IDictionary<string/*!*/, string/*!>!*/> BackgroundPredicates =
- new Dictionary<string/*!*/, string/*!*/>();
-
- protected static string GetBackgroundPredicate(string filename) {
- Contract.Requires(filename != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- string res;
- if (!BackgroundPredicates.TryGetValue(filename, out res)) {
- // do we have to lock/synchronise anything?
- string univBackPredPath = Path.Combine(CodebaseString(), filename);
- using (StreamReader reader = new System.IO.StreamReader(univBackPredPath)) {
- res = reader.ReadToEnd();
- }
- BackgroundPredicates.Add(filename, res);
- }
- return cce.NonNull(res);
- }
-
- static void InitializeGlobalInformation(string proverExe)
- // throws ProverException, System.IO.FileNotFoundException;
- {
- Contract.Requires(proverExe != null);
- Contract.Ensures(_proverPath != null);
-
- if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
- _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
- }
-
- if (_proverPath == null) {
- // Initialize '_proverPath'
- _proverPath = Path.Combine(CodebaseString(), proverExe);
- string firstTry = _proverPath;
-
- if (File.Exists(firstTry))
- return;
-
- string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");
- Contract.Assert(programFiles != null);
- string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)");
- if (programFiles.Equals(programFilesX86)) {
- // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead.
- programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
- }
-
-
- List<string> z3Dirs = new List<string>();
- if (Directory.Exists(programFiles + @"\Microsoft Research\")) {
- string msrDir = programFiles + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
- if (Directory.Exists(programFilesX86 + @"\Microsoft Research\")) {
- string msrDir = programFilesX86 + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
-
- // Look for the most recent version of Z3.
- int minor = 0, major = 0;
- string winner = null;
- Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");
- foreach (string d in z3Dirs) {
- string name = new DirectoryInfo(d).Name;
- foreach (Match m in r.Matches(name)) {
- int ma, mi;
- ma = int.Parse(m.Groups[1].ToString());
- mi = int.Parse(m.Groups[2].ToString());
- if (major < ma || (major == ma && minor < mi)) {
- major = ma;
- minor = mi;
- winner = d;
- }
- }
- }
-
- if (major == 0 && minor == 0) {
- throw new ProverException("Cannot find executable: " + firstTry);
- }
- Contract.Assert(winner != null);
-
- _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);
- if (!File.Exists(_proverPath)) {
- throw new ProverException("Cannot find prover: " + _proverPath);
- }
-
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("[TRACE] Using prover: " + _proverPath);
- }
- }
- }
-
- [Rep]
- protected internal ProverProcess thmProver;
- bool currentProverHasBeenABadBoy = false;
- // invariant currentProverHasBeenABadBoy ==> thmProver != null;
- protected int restarts = 0;
- protected DeclFreeProverContext ctx;
- protected string BackgroundPredFilename;
- protected ConsoleCancelEventHandler cancelEvent;
-
- [NotDelayed]
- public ProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx,
- string proverExe, string backgroundPred)
- : base(options, "; ", "", "", "", gen) {
- Contract.Requires(options != null);
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(proverExe != null);
- Contract.Requires(backgroundPred != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- BackgroundPredFilename = backgroundPred;
- InitializeGlobalInformation(proverExe);
- this.ctx = ctx;
-
-
- // ensure that a VCExprTranslator is available
- // if none exists so far, we have to create a new one
- // from scratch and feed the axioms to it
- if (ctx.exprTranslator == null) {
- AxiomVCExprTranslator tl = SpawnVCExprTranslator(options);
- ctx.exprTranslator = tl;
- tl.AddAxiom(tl.translate(ctx.Axioms, -1));
- // we clear the lists with new axioms and declarations;
- // they are not needed at this point
- List<string> x = tl.NewAxioms;
- //x = x; // make the compiler happy: somebody uses the value of x
- x = tl.NewTypeDecls;
- }
- }
-
- /// <summary>
- /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
- /// </summary>
- public override void PushVCExpression(VCExpr vc) {
- //Contract.Requires(vc != null);
- vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));
- }
-
- public override string VCExpressionToString(VCExpr vc) {
- //Contract.Requires(vc != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- return vcExprTranslator.translate(vc, 1);
- }
-
- // Number of axioms pushed since the last call to Check
- public override int NumAxiomsPushed() {
- return vcExprTranslator.NewAxiomsCount;
- }
-
- // Feed the axioms pushed since the last call to Check to the theorem prover
- public override int FlushAxiomsToTheoremProver() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- return FeedNewAxiomsDecls2Prover();
- }
-
- public override void Pop() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Contract.Assert(thmProver != null);
- LogCommon("(BG_POP)");
- thmProver.PopAxioms();
- }
-
- [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked
- void ControlCHandler(object o, ConsoleCancelEventArgs a) {
- if (thmProver != null) {
- thmProver.Kill();
- }
- }
-
- public override void Close() {
- if (cancelEvent != null) {
- Console.CancelKeyPress -= cancelEvent;
- cancelEvent = null;
- }
- if (thmProver != null) {
- cce.BeginExpose(this);
- {
- thmProver.Close();
- thmProver = null;
- currentProverHasBeenABadBoy = false;
- }
- cce.EndExpose();
- }
- base.Close();
- }
-
- private UnexpectedProverOutputException proverException;
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- this.NewProblem(descriptiveName);
- this.proverException = null;
-
- try {
- this.ResurrectProver();
-
- string vcString = vcExprTranslator.translate(vc, 1);
-
- Helpers.ExtraTraceInformation("Sending data to theorem prover");
-
- int num_axioms_pushed =
- FeedNewAxiomsDecls2Prover();
-
- LogActivity(vcString);
-
- Contract.Assert(thmProver != null);
- thmProver.BeginCheck(descriptiveName, vcString);
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0) {
- // Pop all the axioms that were pushed by FeedNewAxiomsDecls2Prover
- for (int i = 0; i < num_axioms_pushed; i++) {
- LogBgPop();
- thmProver.PopAxioms();
- }
- }
-
- if (CommandLineOptions.Clo.RestartProverPerVC) {
- LogComment("Will restart the prover due to /restartProver option");
- currentProverHasBeenABadBoy = true;
- }
- } catch (UnexpectedProverOutputException e) {
- proverException = e;
- }
- }
-
- public override Outcome CheckOutcome(ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- if (this.thmProver == null) {
- return Outcome.Undetermined;
- }
-
- if (proverException == null) {
- try {
- ProverProcess.ProverOutcome result = thmProver.CheckOutcome(handler);
-
- if (options.ForceLogStatus) {
- switch (result) {
- case ProverProcess.ProverOutcome.Valid:
- LogActivity("DBG_WAS_VALID");
- break;
- case ProverProcess.ProverOutcome.NotValid:
- LogActivity("DBG_WAS_INVALID");
- break;
- }
- }
-
- switch (result) {
- case ProverProcess.ProverOutcome.Valid:
- return Outcome.Valid;
- case ProverProcess.ProverOutcome.TimeOut:
- return Outcome.TimeOut;
- case ProverProcess.ProverOutcome.OutOfMemory:
- return Outcome.OutOfMemory;
- case ProverProcess.ProverOutcome.Inconclusive:
- return Outcome.Undetermined;
- case ProverProcess.ProverOutcome.NotValid:
- return Outcome.Invalid;
- }
- } catch (UnexpectedProverOutputException e) {
- proverException = e;
- }
- }
-
- Contract.Assume(proverException != null);
- LogComment("***** Unexpected prover output");
- cce.BeginExpose(this);
- {
- currentProverHasBeenABadBoy = true; // this will cause the next resurrect to restart the prover
- }
- cce.EndExpose();
- throw proverException;
- }
-
- protected virtual void ResurrectProver() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- if (thmProver != null) {
- if (thmProver.HasExited) {
- DateTime now = DateTime.Now;
- LogComment("***** Prover Crashed at or before " + now.ToString("G"));
-
- } else if (CommandLineOptions.Clo.MaxProverMemory > 0 &&
- thmProver.NumFormulasChecked > CommandLineOptions.Clo.MinNumOfProverCalls &&
- thmProver.PeakVirtualMemorySize > CommandLineOptions.Clo.MaxProverMemory) {
- LogComment("***** Exceeded memory limit. Peak memory usage so far: " +
- thmProver.PeakVirtualMemorySize / CommandLineOptions.Megabyte + "MB");
-
- } else if (!currentProverHasBeenABadBoy) {
- // prover is ready to go
- return;
- }
-
- thmProver.Close();
- thmProver = null;
- currentProverHasBeenABadBoy = false;
- restarts++;
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- Console.WriteLine("Warning: restarting theorem prover. Context could be lost");
- }
- }
-
- FireUpNewProver();
- }
- cce.EndExpose();
- }
-
- protected abstract ProverProcess CreateProverProcess(string proverPath);
-
- public void LogBgPush(string s) {
- Contract.Requires(s != null);
- LogCommon("(BG_PUSH ");
- LogCommon(s);
- LogCommon(")");
- }
-
- public void LogBgPop() {
- LogCommon("(BG_POP)");
- }
-
- [NoDefaultContract]
- private void FireUpNewProver()
- {
- Contract.Requires( cce.IsExposed(this));
- Contract.Requires( thmProver == null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
- cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
- Console.CancelKeyPress += cancelEvent;
- }
- thmProver = CreateProverProcess(_proverPath);
- if (restarts == 0) {
- foreach (string s in thmProver.OptionComments().Split('\n')) {Contract.Assert(s != null);
- LogCommonComment(s);
- }
- foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
- LogCommon(parmsetting);
- }
- }
- foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
- thmProver.Feed(parmsetting, 0);
- }
- thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
-
- if (restarts == 0) {
- // log the stuff before feeding it into the prover, so when it dies
- // and takes Boogie with it, we know what happened
- LogCommon(GetBackgroundPredicate(BackgroundPredFilename));
-
- foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
- LogCommon(s);}
- foreach (string s in vcExprTranslator.AllAxioms){Contract.Assert(s != null);
- LogBgPush(s);}
-
- LogCommonComment("Initialized all axioms.");
- }
-
- foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
- thmProver.Feed(s, 0);}
- foreach (string s in vcExprTranslator.AllAxioms){Contract.Assert(s != null);
- thmProver.AddAxioms(s);}
-
- // we have sent everything to the prover and can clear the lists with
- // new axioms and declarations
- List<string> x = vcExprTranslator.NewAxioms;
- //x = x; // make the compiler happy: somebody uses the value of x
- x = vcExprTranslator.NewTypeDecls;
- }
-
- public override ProverContext Context {
- get {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
- return this.ctx;
- }
- }
- }
- [ContractClassFor(typeof(ProcessTheoremProver))]
- public abstract class ProcessTheoremProverContracts :ProcessTheoremProver{
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p) {
- Contract.Requires(p != null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
- throw new NotImplementedException();
-
- }
- protected override ProverProcess CreateProverProcess(string proverPath) {
- Contract.Requires(proverPath != null);
- Contract.Ensures(Contract.Result<ProverProcess>() != null);
- throw new NotImplementedException();
- }
- [NotDelayed]
- public ProcessTheoremProverContracts(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx,
- string proverExe, string backgroundPred):base(options,gen,ctx,proverExe,backgroundPred)
- {throw new NotImplementedException();}
- }
-
- public class SimplifyTheoremProver : ProcessTheoremProver {
- [NotDelayed]
- public SimplifyTheoremProver(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx)
- : base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx") {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- }
-
- protected override ProverProcess CreateProverProcess(string proverPath) {
- //Contract.Requires(proverPath != null);
- Contract.Ensures(Contract.Result<ProverProcess>() != null);
-
- return new SimplifyProverProcess(proverPath);
- }
-
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
- //Contract.Requires(opts!=null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return new SimplifyVCExprTranslator(gen);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public abstract class AxiomVCExprTranslator : VCExprTranslator {
- protected AxiomVCExprTranslator() {
- AllAxioms = new List<string> ();
- NewAxiomsAttr = new List<string> ();
- AllTypeDecls = new List<string> ();
- NewTypeDeclsAttr = new List<string> ();
- }
-
- protected AxiomVCExprTranslator(AxiomVCExprTranslator tl) {
- Contract.Requires(tl != null);
- AllAxioms = new List<string>(tl.AllAxioms);
- NewAxiomsAttr = new List<string>(tl.NewAxiomsAttr);
- AllTypeDecls = new List<string>(tl.AllTypeDecls);
- NewTypeDeclsAttr = new List<string>(tl.NewTypeDeclsAttr);
- }
-
- // we store all typing-related axioms that have been sent to the prover
- // so that the prover can be re-initialised in case it dies
- public readonly List<string/*!>!*/> AllAxioms;
- private List<string/*!>!*/> NewAxiomsAttr;
-
- // The length of the list NewAxiomsAttr
- public int NewAxiomsCount {
- get {
- return NewAxiomsAttr.Count;
- }
- }
-
- public List<string/*!>!*/> NewAxioms {
- get {
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- List<string/*!>!*/> res = NewAxiomsAttr;
- NewAxiomsAttr = new List<string>();
- return res;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(AllAxioms != null);
- Contract.Invariant(NewAxiomsAttr != null);
- Contract.Invariant(AllTypeDecls != null);
- Contract.Invariant(NewTypeDeclsAttr != null);
- }
-
-
- // similarly, a list of declarations that have been sent to the prover
- public readonly List<string/*!>!*/> AllTypeDecls;
- private List<string/*!>!*/> NewTypeDeclsAttr;
-
- public List<string>/*!>!*/ NewTypeDecls {
- get {
- List<string/*!>!*/> res = NewTypeDeclsAttr;
- NewTypeDeclsAttr = new List<string/*!*/>();
- return res;
- }
- }
-
- public void AddAxiom(string axiom) {
- Contract.Requires(axiom != null);
- AllAxioms.Add(axiom);
- NewAxiomsAttr.Add(axiom);
- }
-
- public void AddTypeDecl(string typeDecl) {
- Contract.Requires(typeDecl != null);
- AllTypeDecls.Add(typeDecl);
- NewTypeDeclsAttr.Add(typeDecl);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class SimplifyVCExprTranslator : AxiomVCExprTranslator {
- public SimplifyVCExprTranslator(VCExpressionGenerator gen) {
- Contract.Requires(gen != null);
- Gen = gen;
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments(gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- }
- axBuilder.Setup();
- AxBuilder = axBuilder;
- Namer = new UniqueNamer();
- LitAbstracter = new BigLiteralAbstracter(gen);
- }
-
- private SimplifyVCExprTranslator(SimplifyVCExprTranslator tl)
- : base(tl) {
- Contract.Requires(tl != null);
- Gen = tl.Gen;
- AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
- Namer = (UniqueNamer)tl.Namer.Clone();
- LitAbstracter = (BigLiteralAbstracter)tl.LitAbstracter.Clone();
- }
-
- public override Object Clone() {
- Contract.Ensures(Contract.Result<object>() != null);
-
- return new SimplifyVCExprTranslator(this);
- }
-
- private readonly VCExpressionGenerator Gen;
- private readonly TypeAxiomBuilder AxBuilder;
- private readonly UniqueNamer Namer;
- private readonly BigLiteralAbstracter LitAbstracter;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Gen != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(LitAbstracter != null);
- }
-
-
- public override string Lookup(VCExprVar var) {
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- VCExprVar v = AxBuilder.TryTyped2Untyped(var);
- if (v != null) {
- var = v;
- }
- return Namer.Lookup(var);
- }
-
- public override string translate(VCExpr expr, int polarity) {
- //Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen);
- Contract.Assert(letImplier != null);
-
- // handle the types in the VCExpr
- TypeEraser eraser;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
- break;
- }
- VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
- Contract.Assert(exprWithoutTypes != null);
-
- TermFormulaFlattener flattener = new TermFormulaFlattener(Gen);
- Contract.Assert(flattener != null);
- VCExpr exprWithLet = flattener.Flatten(exprWithoutTypes);
- Contract.Assert(exprWithLet != null);
- VCExpr exprWithoutLet = letImplier.Mutate(exprWithLet);
- Contract.Assert(exprWithoutLet != null);
-
- // big integer literals
- VCExpr exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);
- Contract.Assert(exprWithoutBigLits != null);
- AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),
- Namer));
-
- // type axioms
- VCExpr axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
- Contract.Assert(axiomsWithLet != null);
- VCExpr axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
- Contract.Assert(axiomsWithoutLet != null);
-
- AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(axiomsWithoutLet, Namer));
- return SimplifyLikeExprLineariser.ToSimplifyString(exprWithoutBigLits, Namer);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Factory : ProverFactory {
- public override object SpawnProver(ProverOptions options, object ctxt) {
- //Contract.Requires(options != null);
- //Contract.Requires(ctxt != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- return new SimplifyTheoremProver(options,
- cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
- cce.NonNull((DeclFreeProverContext)ctxt));
- }
-
- public override object NewProverContext(ProverOptions options) {
- //Contract.Requires(options != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
- CommandLineOptions.Clo.BracketIdsInVC = 1;
- }
- VCExpressionGenerator gen = new VCExpressionGenerator();
- Contract.Assert(gen != null);
- List<string>/*!>!*/ proverCommands = new List<string> ();
- Contract.Assert(cce.NonNullElements(proverCommands));
- proverCommands.Add("simplify");
- return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));
- }
-
- public override CommandLineOptions.VCVariety DefaultVCVariety {
- get {
- return CommandLineOptions.VCVariety.BlockNested;
- }
- }
-
- // needed to make test7 pass
- public override bool SupportsDags {
- get {
- return true;
- }
- }
- }
-}
diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj deleted file mode 100644 index 81d2f90a..00000000 --- a/Source/Provers/Simplify/Simplify.csproj +++ /dev/null @@ -1,210 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Microsoft.Boogie.Simplify</RootNamespace>
- <AssemblyName>Provers.Simplify</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile>Client</TargetFrameworkProfile>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for Simplify.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.Simplify.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Let2ImpliesVisitor.cs" />
- <Compile Include="Prover.cs" />
- <Compile Include="ProverInterface.cs" />
- <Compile Include="..\..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Graph\Graph.csproj">
- <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
- <Name>Graph</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </ItemGroup>
- <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
-</Project>
\ No newline at end of file diff --git a/Source/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs deleted file mode 100644 index ef594484..00000000 --- a/Source/Provers/Simplify/cce.cs +++ /dev/null @@ -1,193 +0,0 @@ -using System;
-using SA=System.Attribute;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using Microsoft.Boogie;
-
-/// <summary>
-/// A class containing static methods to extend the functionality of Code Contracts
-/// </summary>
-
-public static class cce {
- //[Pure]
- //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
- // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
- //}
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
- }
- //[Pure]
- //public static bool NonNullElements(VariableSeq collection) {
- // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- //}
- /// <summary>
- /// For possibly-null lists of non-null elements
- /// </summary>
- /// <typeparam name="T"></typeparam>
- /// <param name="collection"></param>
- /// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param>
- /// <returns></returns>
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
- return (nullability && collection == null) || cce.NonNullElements(collection);
- //Should be the same as:
- /*if(nullability&&collection==null)
- * return true;
- * return cce.NonNullElements(collection)
- */
-
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
- return kvp.Key != null && kvp.Value != null;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
- return iEnumerator != null;
- }
- //[Pure]
- //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
- // return cce.NonNullElements(graph.TopologicalSort());
- //}
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- [Pure]
- public static bool IsNew(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- [Pure]
- public static bool Different(object o, object p) {
- return true;
- }
- [Pure]
- public static bool New(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
- //[Pure]
- //public static bool IsValid(Microsoft.Dafny.Expression expression) {
- // return true;
- //}
- //public static List<T> toList<T>(PureCollections.Sequence s) {
- // List<T> toRet = new List<T>();
- // foreach (T t in s.elems)
- // if(t!=null)
- // toRet.Add(t);
- // return toRet;
- //}
-
- //internal static bool NonNullElements(Set set) {
- // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
- //}
-}
-
-public class PeerAttribute : SA {
-}
-public class RepAttribute : SA {
-}
-public class CapturedAttribute : SA {
-}
-public class NotDelayedAttribute : SA {
-}
-public class NoDefaultContractAttribute : SA {
-}
-public class VerifyAttribute : SA {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : SA {
-}
-public class AdditiveAttribute : SA {
-}
-public class ReadsAttribute : SA {
- public enum Reads {
- Nothing,
- Everything,
- };
- public ReadsAttribute(object o) {
- }
-}
-public class GlobalAccessAttribute : SA {
- public GlobalAccessAttribute(bool b) {
- }
-}
-public class EscapesAttribute : SA {
- public EscapesAttribute(bool b, bool b_2) {
- }
-}
-public class NeedsContractsAttribute : SA {
- public NeedsContractsAttribute() {
- }
- public NeedsContractsAttribute(bool ret, bool parameters) {
- }
- public NeedsContractsAttribute(bool ret, int[] parameters) {
- }
-}
-public class ImmutableAttribute : SA {
-}
-public class InsideAttribute : SA {
-}
-public class SpecPublicAttribute : SA {
-}
-public class ElementsPeerAttribute : SA {
-}
-public class ResultNotNewlyAllocatedAttribute : SA {
-}
-public class OnceAttribute : SA {
-}
\ No newline at end of file diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs deleted file mode 100644 index c9bdfa31..00000000 --- a/Source/Provers/Z3/Inspector.cs +++ /dev/null @@ -1,162 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-//using util;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
- public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNull(Labels));
- }
-
-
- public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>()));
-
- FindLabelsVisitor visitor = new FindLabelsVisitor();
- visitor.Traverse(expr, true);
- return visitor.Labels;
- }
-
- protected override bool StandardResult(VCExpr node, bool arg) {
- //Contract.Requires(node!=null);
- VCExprNAry nary = node as VCExprNAry;
- if (nary != null) {
- VCExprLabelOp lab = nary.Op as VCExprLabelOp;
- if (lab != null) {
- Labels.Add(lab.label);
- }
- }
- return true;
- }
- }
-
- internal class Inspector {
- [Rep] protected readonly Process inspector;
- [Rep] readonly TextReader fromInspector;
- [Rep] readonly TextWriter toInspector;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(inspector!=null);
- Contract.Invariant(fromInspector!=null);
- Contract.Invariant(toInspector != null);
- }
-
-
- public Inspector(Z3InstanceOptions opts)
- {
- Contract.Requires(opts != null);
- ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector);
- Contract.Assert(psi!=null);
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = false;
-
- try
- {
- Process inspector = Process.Start(psi);
- this.inspector = inspector;
- fromInspector = inspector.StandardOutput;
- toInspector = inspector.StandardInput;
- }
- catch (System.ComponentModel.Win32Exception e)
- {
- throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
- }
- }
-
- public void NewProver()
- {
- }
-
- public void NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(vc != null);
- Contract.Requires(handler != null);
- HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);
- Contract.Assert(labels!=null);
- toInspector.WriteLine("PROBLEM " + descriptiveName);
- toInspector.WriteLine("TOKEN BEGIN");
- foreach (string lab in labels) {
- Contract.Assert(lab!=null);
- string no = lab.Substring(1);
- Absy absy = handler.Label2Absy(no);
-
- IToken tok = absy.tok;
- AssertCmd assrt = absy as AssertCmd;
- Block blk = absy as Block;
- string val = tok.val; // might require computation, so cache it
- if (val == "foo" || tok.filename == null) continue; // no token
-
- toInspector.Write("TOKEN ");
- toInspector.Write(lab);
- toInspector.Write(" ");
-
- if (assrt != null) {
- toInspector.Write("ASSERT");
- string errData = assrt.ErrorData as string;
- if (errData != null) {
- val = errData;
- } else if (assrt.ErrorMessage != null) {
- val = assrt.ErrorMessage;
- }
- } else if (blk != null) {
- toInspector.Write("BLOCK ");
- toInspector.Write(blk.Label);
- } else {
- Contract.Assume( false);
- }
- if (val == null || val == "assert" || val == "ensures") { val = ""; }
-
- if (absy is LoopInitAssertCmd) {
- val += " (loop entry)";
- } else if (absy is LoopInvMaintainedAssertCmd) {
- val += " (loop body)";
- } else if (val.IndexOf("#VCCERR") >= 0) {
- // skip further transformations
- } else if (absy is AssertRequiresCmd) {
- AssertRequiresCmd req = (AssertRequiresCmd)absy;
- IToken t2 = req.Requires.tok;
- string tval = t2.val;
- if (tval == "requires")
- tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);
- string call = "";
- if (val != "call") call = " in call to " + val;
- val = string.Format("precondition {0}{1}", tval, call);
- }
-
- val = val.Replace("\r", "").Replace("\n", " ");
-
- toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
- }
- toInspector.WriteLine("TOKEN END");
- }
-
- public void StatsLine(string line)
- {
- Contract.Requires(line != null);
- toInspector.WriteLine(line);
- toInspector.Flush();
- }
- }
-}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs deleted file mode 100644 index 6a066f1f..00000000 --- a/Source/Provers/Z3/Prover.cs +++ /dev/null @@ -1,937 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-// #define RECENT_Z3 // 2.20 or newer
-
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using util;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-
-// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
-namespace Microsoft.Boogie.Z3
-{
- internal class Z3ProverProcess : ProverProcess
- {
- [Peer]
- private Z3InstanceOptions opts;
- [Peer]
- private readonly Inspector/*?*/ inspector;
- private readonly bool expectingModel = false;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(opts != null);
- Contract.Invariant(cce.NonNullElements(parameterSettings));
- }
-
- class OptionValue
- {
- public readonly string Option;
- public readonly string Value;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Option != null);
- Contract.Invariant(Value != null);
- }
-
- public OptionValue(string option, string value) { Contract.Requires(option != null); Contract.Requires(value != null); Option = option; Value = value; }
- }
-
- static void AddOption(List<OptionValue> parms, string option, string value)
- //modifies parms.*; TODO:
- {
- Contract.Requires(option != null);
- Contract.Requires(value != null);
- Contract.Requires(cce.NonNullElements(parms));
- OptionValue ov = new OptionValue(option, value);
- cce.Owner.AssignSame(ov, cce.Owner.ElementProxy(parms));
- parms.Add(ov);
- }
-
- private List<OptionValue/*!>!*/> parameterSettings;
-
- static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name, object value) {
- cmdLineBldr.Append(' ').Append(OptionChar()).Append(name).Append(':').Append(value);
- }
-
- static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name) {
- cmdLineBldr.Append(' ').Append(OptionChar()).Append(name);
- }
-
- static bool ExpectingModel()
- {
- return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ModelViewFile != null ||
- CommandLineOptions.Clo.ContractInfer ||
- CommandLineOptions.Clo.LazyInlining > 0 ||
- CommandLineOptions.Clo.StratifiedInlining > 0;
- }
-
- static string/*!*/ CreateCommandLineArgsForOptions(Z3InstanceOptions opts)
- {
- StringBuilder cmdLineArgsBldr = new StringBuilder();
- AppendCmdLineOption(cmdLineArgsBldr, "si");
-
- if (CommandLineOptions.Clo.z3AtFlag)
- AppendCmdLineOption(cmdLineArgsBldr, "@");
-
- if (0 <= CommandLineOptions.Clo.ProverCCLimit)
- AppendCmdLineOption(cmdLineArgsBldr, "cex", CommandLineOptions.Clo.ProverCCLimit);
-
- if (0 <= opts.Timeout)
- AppendCmdLineOption(cmdLineArgsBldr, "t", opts.Timeout);
-
- if (ExpectingModel())
- AppendCmdLineOption(cmdLineArgsBldr, "m");
-
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- cmdLineArgsBldr.Append(" \"").Append(opt).Append('\"');
- }
-
- return cmdLineArgsBldr.ToString();
- }
-
- static List<OptionValue/*!*/>/*!*/ CreateParameterListForOptions(Z3InstanceOptions opts, Inspector inspector)
- {
- List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();
-
- AddOption(result, "MODEL_PARTIAL", "true");
-
- AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
- AddOption(result, "MODEL_V1", "true");
- AddOption(result, "ASYNC_COMMANDS", "false");
-
-#if RECENT_Z3
- AddOption(result, "AUTO_CONFIG", "false");
- AddOption(result, "MBQI", "false");
-#else
- AddOption(result, "MODEL_VALUE_COMPLETION", "false");
-#endif
-
- if (!opts.OptimizeForBv) {
- // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
- // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- AddOption(result, "PHASE_SELECTION", "0");
- AddOption(result, "RESTART_STRATEGY", "0");
- AddOption(result, "RESTART_FACTOR", "|1.5|");
-
- // Make the integer model more diverse by default, speeds up some benchmarks a lot.
- AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");
-
- // The left-to-right structural case-splitting strategy.
-#if !RECENT_Z3
- AddOption(result, "SORT_AND_OR", "false");
-#endif
- AddOption(result, "CASE_SPLIT", "3");
-
- // In addition delay adding unit conflicts.
- AddOption(result, "DELAY_UNITS", "true");
- AddOption(result, "DELAY_UNITS_THRESHOLD", "16");
- }
-
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- AddOption(result, "NNF_SK_HACK", "true");
-
- // More or less like MAM=0.
- AddOption(result, "QI_EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
- // the following will make the :weight option more usable
- AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");
-
- if (opts.Inspector != null)
- AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
-
- AddOption(result, "TYPE_CHECK", "true");
- AddOption(result, "BV_REFLECT", "true");
-
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- int eq = opt.IndexOf("=");
- // we add them both to command line and the input file:
- // - allow for overriding default options
- // - some options (like TRACE) work only from command line
- // Also options with spaces do not work with (SETPARAMETER ...)
- if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
- AddOption(result, opt.Substring(0, eq), opt.Substring(eq + 1));
- }
- }
-
- return result;
- }
-
- //[NotDelayed]
- [Captured]
- public Z3ProverProcess(Z3InstanceOptions opts, Inspector inspector)
- : base(ComputeProcessStartInfo(opts), opts.ExeName) { // throws ProverException
- Contract.Requires(opts != null);
- Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));
- this.parameterSettings = CreateParameterListForOptions(opts, inspector);
- cce.Owner.AssignSame(this, opts);
- this.opts = opts;
- this.inspector = inspector;
- this.expectingModel = ExpectingModel();
- }
-
- private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts)
- {
- return new ProcessStartInfo(opts.ExeName, CreateCommandLineArgsForOptions(opts))
- {
- CreateNoWindow = true,
- UseShellExecute = false,
- RedirectStandardInput = true,
- RedirectStandardOutput = true,
- RedirectStandardError = true
- };
- }
-
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- StringBuilder sb = new StringBuilder();
- sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
- opts.ExeName, this.simplify.StartInfo.Arguments);
- Contract.Assume(cce.IsPeerConsistent(CommandLineOptions.Clo));
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- sb.Append(" ").Append(opt);
- }
- sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
- return sb.ToString();
- }
-
- //[Pure(false)]
- public override IEnumerable<string/*!>!*/> ParameterSettings {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));
- foreach (OptionValue opt in parameterSettings) {
- yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
- }
- }
- }
-
- // z3 uses different magic characters for options on linux/unix and on windows
- private static string OptionChar() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- Contract.Assume(Environment.OSVersion != null);
- switch (Environment.OSVersion.Platform) {
- case PlatformID.Unix:
- return "-";
- default:
- return "/";
- }
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(formula != null);
- ToWriteLine(formula);
- ToWriteLine(String.Format("; END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
- ToFlush();
- }
-
- protected int TimedFromReadChar() {
- if (opts.Timeout > 0)
- return FromReadChar((opts.Timeout + 1) * 1000);
- else
- return FromReadChar();
- }
-
- private void Trace(string msg) {
- Contract.Requires(msg != null);
- Console.WriteLine("Z3: " + msg);
- }
-
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ProverOutcome outcome;
- bool isInvalid = false;
-
- if (this.simplify == null) {
- return ProverOutcome.Inconclusive;
- }
-
-
- while (true) {
- int ch = TimedFromReadChar();
- if (ch == -1 && this.readTimedOut) {
- handler.OnResourceExceeded("timeout (forced)");
- return ProverOutcome.TimeOut;
- }
-
- if (ch == -1)
- throw new UnexpectedProverOutputException("z3 crashed and produced no output");
-
- string line = new string((char)ch, 1) + FromReadLine();
-
- if (line.StartsWith("STATS ")) {
- if (inspector != null) {
- inspector.StatsLine(line);
- }
- continue;
- }
-
- if (opts.Verbosity > 2) {
- Trace("INPUT: " + line);
- }
-
- if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
- handler.OnResourceExceeded("memory");
- return ProverOutcome.OutOfMemory;
- }
-
-
- if (line.StartsWith("WARNING: ")) {
- string w = line.Substring(9);
- handler.OnProverWarning(w);
- continue;
- }
-
- if (line.ToUpper().StartsWith("ERROR")) {
- Console.WriteLine("Z3 returns the following error:");
- Console.WriteLine(" " + line);
- return ProverOutcome.Inconclusive;
- }
-
- int beg = 0;
- while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9') {
- cce.LoopInvariant(beg <= line.Length);
- beg++;
- }
-
- if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
- string status = line.Substring(beg + 2);
-
- if (status.StartsWith("Valid")) {
- return ProverOutcome.Valid;
- }
-
- if (status.StartsWith("Timeout")) {
- handler.OnResourceExceeded("timeout");
- return ProverOutcome.TimeOut;
- }
-
- if (status.StartsWith("Inconclusive")) {
- return ProverOutcome.Inconclusive;
- }
-
- if (status.StartsWith("Memout")) {
- handler.OnResourceExceeded("memory");
- return ProverOutcome.OutOfMemory;
- }
-
- if (status.StartsWith("Invalid")) {
- isInvalid = true;
- continue;
- }
- }
-
- if (isInvalid && line == ".") {
- return ProverOutcome.NotValid;
- }
-
- if (isInvalid && line.StartsWith("labels: (")) {
- List<string/*!*/>/*!*/ l = ParseLabels(line);
- Contract.Assert(cce.NonNullElements(l));
- Z3ErrorModel errModel = null;
- if (expectingModel) {
- if (opts.Verbosity > 2) {
- Trace("waiting for model");
- }
- line = FromReadLine();
- if (line.StartsWith("partitions:")) {
- line = ParseModel(out errModel);
- if (opts.Verbosity > 2) {
- Trace("model parsed, final line " + line);
- }
- // Z3 always ends the model with END_OF_MODEL, not with labels: or .
- Contract.Assume(line == "END_OF_MODEL");
- } else {
- throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
- }
- }
- handler.OnModel(l, errModel);
- continue;
- }
-
- throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
- }
- }
-
- /* ----------------------------------------------------------------------------
- BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:
-
- Output ::= VC*
- VC ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
- VCI ::= number ": " "Invalid"
- ("labels: " "(" ID* ")"
- [MODEL] "END_OF_MODEL")+
- "."
- MODEL ::= MBOOL MFUNC
- MBOOL ::= "boolean assignment:"
- "partitions:"
- MAPPING*
- MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
- BITVECTOR ::= ulong ":bv" int
- MFUNC ::= "function interpretations:"
- F*
- F ::= Id "->" "{"
- MAPLET*
- "else" "->" ZID
- "}"
- MAPLET ::= ZID* "->" ZID
-
- -----------------------------------------------------------------------------*/
- private string ParseModel(out Z3ErrorModel errModel)
- //modifies this.*;
- //throws UnexpectedProverOutputException;
- {
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.Ensures(Contract.Result<string>() != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- //Format in the grammar:
- // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
- // storing the model:
- // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
- Dictionary<string/*!*/, int> identifierToPartition = new Dictionary<string/*!*/, int>();
- // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
- List<List<string/*!*/>> partitionToIdentifiers = new List<List<string/*!*/>>();
- // map each ZID to the number or boolean given, if any:
- List<Object> partitionToValue = new List<Object>();
- // map each value (number or boolean) to the ZID, reverse map of partitionToValue
- Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
- cce.Owner.AssignSame(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition));
-
- int ch;
-
- // read the MAPPING
- for (int zID = 0; true; zID++) {
- ch = FromReadChar();
- if (ch == 'f') {
- break;
- }
- ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
- }// end MAPPING
-
- // add the fake partition for the 'else -> #undefined' clause
- List<string/*!*/> emptyList = new List<string/*!*/>();
- cce.Owner.AssignSame(emptyList, cce.Owner.ElementProxy(partitionToIdentifiers));
- partitionToIdentifiers.Add(emptyList);
- partitionToValue.Add(null);
-
- // continue in ParseModelFunctions, which breaks up this long method and enables its verification
- return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
- }
-
- private void ParseModelMapping(int zID,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<Object, int>/*!*/ valueToPartition)
- //modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
- {
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Requires(identifierToPartition != null);
- Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
- Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
- string s = FromReadLine();
- {
- // sanity check
- int pos = s.IndexOf(' ');
- string n = s;
- int k;
- if (pos >= 0) {
- n = s.Substring(0, pos);
- }
- if (!(int.TryParse(n, out k) && zID == k)) {
- System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
- Contract.Assume(false);
- }
- }
-
- int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
-
- j = s.IndexOf(" -> ", j);
- if (0 <= j) {
- j += 4;
- }
- Contract.Assume(j == -1 || j < s.Length); // if ' -> ' is present, then more should remain of the line
- if (j == -1) {
- // no "-> " found, end of this line, store that there is no value:
- partitionToValue.Add(null);
- int idForNull;
- if (identifierToPartition.TryGetValue("nullObject", out idForNull) && idForNull == zID) {
- Contract.Assume(!valueToPartition.ContainsKey("nullObject")); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add("nullObject", zID);
- // In this case partitionToValue (as the reverse of valueToPartition) should include
- // a map from zID -> "nullObject", but doing that breaks printing out the model as
- // it is printed out by Z3. Also, that information is not required, valueToPartition
- // works well enough by itself.
- }
-
- } else if (s[j] == 't'/*rue*/) {
- partitionToValue.Add(true);
- object boxedTrue = true;
- Contract.Assume(!valueToPartition.ContainsKey(boxedTrue)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedTrue, zID);
- } else if (s[j] == 'f'/*alse*/) {
- object boxedFalse = false;
- cce.Owner.AssignSame(boxedFalse, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(boxedFalse);
- Contract.Assume(!valueToPartition.ContainsKey(boxedFalse)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedFalse, zID);
- } else if (s[j] == 'v') {
- // -> val!..., i.e. no value
- partitionToValue.Add(null);
- } else if (s[j] == '{') {
- // array
- List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
- Contract.Assert(Contract.ForAll(arrayModel, a => a != null));
- string array = s.Substring(j + 1);
- int index1, index2;
- string from, to;
- List<int> tuple = new List<int>();
- while (0 <= array.IndexOf(';')) {
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf(' ');
- from = array.Substring(index1, index2 - index1);
- tuple.Add(int.Parse(from));
- array = array.Substring(index2);
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf(';');
- to = array.Substring(index1, index2 - index1);
- array = array.Substring(index2 + 2);
- tuple.Add(int.Parse(to));
- arrayModel.Add(tuple);
- tuple = new List<int>();
- }
- Contract.Assert(array.StartsWith("else ->"));
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf('}');
- to = array.Substring(index1, index2 - index1);
- tuple.Add(int.Parse(to));
- arrayModel.Add(tuple);
- partitionToValue.Add(arrayModel);
- } else {
- string numberOrBv = s.Substring(j);
- // make number an int, then store it:
- BigNum bvVal;
- int bvSize;
- string number, type;
-
- int l = numberOrBv.IndexOf(':', 0);
- if (0 <= l) {
- number = numberOrBv.Substring(0, l);
- type = numberOrBv.Substring(l + 1);
- } else {
- l = numberOrBv.IndexOf('[', 0);
- if (0 <= l) {
- number = numberOrBv.Substring(2, l - 2);
- int closingBracePosition = numberOrBv.IndexOf(']', l);
- if (l < closingBracePosition)
- type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
- else type = "int";
- } else {
- number = numberOrBv;
- type = "int";
- }
- }
-
- if (type == "int") {
- object boxedN = BigNum.FromString(number);
- Contract.Assume(cce.Owner.None(boxedN));
- cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(boxedN);
- Contract.Assume(!valueToPartition.ContainsKey(boxedN)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedN, zID);
- } else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
- BvConst bitV = new BvConst(bvVal, bvSize);
- cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(bitV);
- Contract.Assume(!valueToPartition.ContainsKey(bitV)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(bitV, zID);
- } else {
- System.Console.WriteLine("cannot parse type: '{0}':'{1}'", number, type);
- Contract.Assume(false);
- }
-
- }
- }
-
- private static int ParseModelZidAndIdentifiers(int zID, string s,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers)
- //modifies identifierToPartition.*, partitionToIdentifiers.*;
- {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
- Contract.Requires(s != null);
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= s.Length);
-
- List<string/*!*/> identifiers = new List<string/*!*/>();
- int arrowIndex = s.IndexOf('>');
- Contract.Assert(0 < arrowIndex);
- int j = s.IndexOf('{', 0) + 1; // skip the '{', if present, and set j to 0 otherwise
- if (1 <= j && j < arrowIndex) {
- // There is a list of ID's.
- Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
- //ID*
- while (true) {
- cce.LoopInvariant(cce.IsPeerConsistent(identifiers) && cce.IsPeerConsistent(identifierToPartition) && cce.IsPeerConsistent(partitionToIdentifiers));
- cce.LoopInvariant(0 <= j && j < s.Length);
- int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
- Contract.Assume(j <= k);
- string id = s.Substring(j, k - j);
- j = k + 1;
- Contract.Assume(!identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
- identifierToPartition.Add(id, zID);
- identifiers.Add(id);
- if (s[k] == '}') {
- // end of reading ID*
- break;
- }
- Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
- }//end ID*
- } else {
- j = 0;
- }
- cce.Owner.AssignSame(identifiers, cce.Owner.ElementProxy(partitionToIdentifiers));
- partitionToIdentifiers.Add(identifiers);
- return j;
- }
-
- private string ParseModelFunctions(int ch, out Z3ErrorModel errModel,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<Object, int>/*!*/ valueToPartition
- )
- //modifies this.*;
- {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Ensures(Contract.Result<string>() != null);
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- // read the function F
- Expect(ch, "function interpretations:");
- FromReadLine();
-
- // mapping of function names to function definitions
- Dictionary<string/*!*/, List<List<int>>/*!*/> definedFunctions = new Dictionary<string/*!*/, List<List<int>>/*!*/>();
- // function definition given as list of 'pointwise definitions' in the form of the arguments and result
- // the last element here will always be a list with just one entry which corresponds to the else case
- List<List<int>> functionDefinition = new List<List<int>>();
- // list of arguments, followed by the result, the last element of this list is always the result
- List<int> argumentsAndResult = new List<int>();
-
- // read F
- while (true) {
- functionDefinition = new List<List<int>>();
- string s = FromReadLine();
- // end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
- // whenever there is a model this will end with "END_OF_MODEL", the other cases can only
- // happen when there is no model printed!
- if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
- errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
- return s;
- }
- int j = s.IndexOf(' ', 0);
- Contract.Assume(0 <= j);
- string id = s.Substring(0, j);
- // id is stored into definedFunctions once the function definition for it has
- // been completely parsed.
-
- if (s.IndexOf("-> {") < 0) {
- // This function was a macro and we are not parsing its definition currently.
- // Just move on to the next function.
- while (true) {
- s = FromReadLine();
- if (0 <= s.IndexOf("{" + id + "}"))
- break;
- }
- continue;
- }
-
- // just ignore the "-> {" by dropping string s
- string zIDstring;
-
- // MAPLET
- while (true) {
- argumentsAndResult = new List<int>();
- // remove the 2 spaces that are here
- FromReadChar();
- FromReadChar();
- s = FromReadLine();
- if (s.StartsWith("else ->")) break;
- j = 0;
-
- //ZID*
- while (true) {
- cce.LoopInvariant(0 <= j && j <= s.Length);
-
- j = s.IndexOfAny(new Char[] { '*', '-' }, j);
- // true because this always ends with a "->":
- Contract.Assume(0 <= j);
-
- // reading -> means end of ZID*
- if (s[j] == '-'/*>*/) break;
-
- // start reading the ZID* with the number, not the *
- j = j + 1;
- // by input string format:
- Contract.Assume(j < s.Length);
- int k = s.IndexOf(' ', j);
- // by input string format:
- Contract.Assume(j <= k);
- zIDstring = s.Substring(j, k - j);
- // add the arguments
- argumentsAndResult.Add(int.Parse(zIDstring));
- j = k;
- }// end ZID*
-
- // j is the beginning of "-> *", we want the first character after this
- j = j + 4;
- // by input string format:
- Contract.Assume(j <= s.Length);
- zIDstring = s.Substring(j);
- // add the result
- argumentsAndResult.Add(int.Parse(zIDstring));
- // add the input line as another 'pointwise defined' element to the functions definition
- functionDefinition.Add(argumentsAndResult);
- }// end MAPLET
-
- // this is the 'else -> #unspecified' case
- // by input string format:
- Contract.Assume(s.IndexOf("#unspec") >= 0);
- // this stores the else line as another argumentsAndResult list
- argumentsAndResult = new List<int>();
- argumentsAndResult.Add(partitionToIdentifiers.Count - 1); // use the fake partition we have created before
- // which is then added to the function definition, which is now complete
- cce.Owner.AssignSame(argumentsAndResult, cce.Owner.ElementProxy(functionDefinition));
- functionDefinition.Add(argumentsAndResult);
-
- /*
- // this is the 'else -> *' case, that string is already in s
- j = s.IndexOf('*', 0) + 1;
- // by input string format:
- assume 0 < j && j < s.Length;
- zIDstring = s.Substring(j);
- // this stores the else line as another argumentsAndResult list
- argumentsAndResult = new List<int>();
- argumentsAndResult.Add(int.Parse(zIDstring));
- // which is then added to the function definition, which is now complete
- functionDefinition.Add(argumentsAndResult); */
-
- // and therefore added to the map of defined functions, together with the name 'id'
- // which had been extracted before
- Contract.Assume(!definedFunctions.ContainsKey(id)); // each function name in the model is listed only once
- definedFunctions.Add(id, functionDefinition);
-
- // read the line with "}"
- ch = FromReadChar();
- Expect(ch, "}");
- FromReadLine();
- }// end F
- }
-
- }
-
-
- public class Z3ErrorModel : ErrorModel
- {
- public Z3ErrorModel(Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<object, int>/*!*/ valueToPartition,
- Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions)
- : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions) {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, x => cce.NonNullElements(x)));
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Requires(definedFunctions != null && cce.NonNullElements(definedFunctions.Keys) && cce.NonNullElements(definedFunctions.Values));
-
- this.partitionNames = new string/*?*/[partitionToIdentifiers.Count];
- this.prevPartitionNames = new string/*?*/[partitionToIdentifiers.Count];
- }
-
- private string/*?*/[]/*!*/ partitionNames;
- private string/*?*/[]/*!*/ prevPartitionNames;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(partitionNames != null);
- Contract.Invariant(prevPartitionNames != null);
- }
-
-
- private void SetNames() {
- int len = partitionToIdentifiers.Count;
- for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
- prevPartitionNames = partitionNames;
- partitionNames = new string[len];
- for (int pos = 0; pos < len; ++pos)
- GetPartitionName(pos);
- }
- }
-
- private int NameBadness(string name) {
- Contract.Requires(name != null);
- int badness = name.Length;
- if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
- badness += 1000;
- if (name.IndexOf("(") > 0)
- badness += 500;
- return badness;
- }
-
- private string GetPartitionName(int pos) {
- Contract.Ensures(Contract.Result<string>() != null);
-
- string name = partitionNames[pos];
- if (name != null) {
- return name;
- }
-
- object tmp = partitionToValue[pos];
- if (tmp != null) {
- partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
- } else {
- List<string/*!*/>/*!*/ possible_names = new List<string/*!*/>();
- List<string/*!*/> pti = partitionToIdentifiers[pos];
- Contract.Assert(cce.NonNullElements(pti));
-
- // make sure we're not called recursively
- string prevName = prevPartitionNames[pos];
- if (prevName == null) prevName = "*" + pos;
- partitionNames[pos] = prevName;
-
- if (pti != null && pti.Count > 0) {
- // add identifiers
- foreach (string n in pti) {
- Contract.Assert(n != null);
- possible_names.Add(n);
- }
- }
-
- // Then also look for functions,
- // and then collect possible functional definitions
- foreach (KeyValuePair<string/*!*/, List<List<int>>/*!*/> kv in definedFunctions) {
- Contract.Assert(kv.Key != null);
- Contract.Assert(kv.Value != null);
- foreach (List<int> parms in kv.Value) {
- if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
- string s = kv.Key + "(";
- for (int i = 0; i < parms.Count - 1; ++i) {
- if (i != 0) s += ", ";
- s += GetPartitionName(parms[i]);
- }
- s += ")";
- possible_names.Add(s);
- }
- }
- }
-
- // choose the shortest possible name
- if (possible_names.Count > 0) {
- string best = possible_names[0];
- foreach (string s in possible_names) {
- Contract.Assert(s != null);
- if (NameBadness(s) < NameBadness(best)) best = s;
- }
- if (best.Length < 120)
- partitionNames[pos] = best;
- }
- }
-
- return cce.NonNull(partitionNames[pos]);
- }
-
- private void PrintReadableModel(TextWriter writer) {
- Contract.Requires(writer != null);
- writer.WriteLine("Z3 error model: ");
- SetNames();
- writer.WriteLine("partitions:");
- Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
- for (int i = 0; i < partitionToIdentifiers.Count; i++) {
- writer.Write("{0,5}: {1} ", "*" + i, GetPartitionName(i));
- List<string/*!*/> pti = partitionToIdentifiers[i];
- Contract.Assert(cce.NonNullElements(pti));
- if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
- writer.Write("{");
- for (int k = 0; k < pti.Count - 1; k++) {
- writer.Write(pti[k] + " ");
- }
- //extra work to make sure no " " is at the end of the list of identifiers
- if (pti.Count != 0) {
- writer.Write(pti[pti.Count - 1]);
- }
- writer.Write("}");
- }
- writer.WriteLine();
- }
-
- writer.WriteLine();
- writer.WriteLine("function interpretations:");
- List<string> funNames = new List<string>(definedFunctions.Keys);
- funNames.Sort();
- foreach (string name in funNames) {
- Contract.Assert(name != null);
- if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
- foreach (List<int> parms in definedFunctions[name]) {
- Contract.Assert(parms != null);
- string s = name + "(";
- if (parms.Count == 1) {
- continue;
- // s += "*";
- } else {
- for (int i = 0; i < parms.Count - 1; ++i) {
- if (i != 0) s += ", ";
- s += GetPartitionName(parms[i]);
- }
- }
- s += ")";
- string res = GetPartitionName(parms[parms.Count - 1]);
- if (res == s)
- res = "*" + parms[parms.Count - 1] + " (SELF)";
- writer.WriteLine("{0} = {1}", s, res);
- }
- writer.WriteLine();
- }
- writer.WriteLine("The end.");
- writer.WriteLine();
- }
-
- public override void Print(TextWriter writer) {
- //Contract.Requires(writer != null);
- if (CommandLineOptions.Clo.PrintErrorModel == 4) {
- PrintReadableModel(writer);
- } else {
- base.Print(writer);
- }
- }
- }
-}
-
-
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs deleted file mode 100644 index 3718372b..00000000 --- a/Source/Provers/Z3/ProverInterface.cs +++ /dev/null @@ -1,427 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-//using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-//using System.IO;
-using System.Text;
-//using ExternalProver;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.Clustering;
-using Microsoft.Boogie.TypeErasure;
-using Microsoft.Boogie.Z3;
-using Microsoft.Boogie.Simplify;
-
-namespace Microsoft.Boogie.Z3
-{
- public class Z3ProcessTheoremProver : ProcessTheoremProver
- {
- private Z3InstanceOptions opts;
- private Inspector inspector;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(opts!=null);
-}
-
-
- [NotDelayed]
- public Z3ProcessTheoremProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName, "TypedUnivBackPred2.sx")
- {
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(opts != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- this.opts = opts;
-
- }
-
- private void FireUpInspector()
- {
- if (inspector == null && opts.Inspector != null) {
- inspector = new Inspector(opts);
- }
- }
-
- protected override Microsoft.Boogie.Simplify.ProverProcess CreateProverProcess(string proverPath) {
- //Contract.Requires(proverPath!= null);
- Contract.Ensures(Contract.Result<Microsoft.Boogie.Simplify.ProverProcess>() != null);
-
-
- opts.ExeName = proverPath;
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProver();
- }
- return new Z3ProverProcess(opts, inspector);
- }
-
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
- //Contract.Requires(opts != null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);
- }
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProblem(descriptiveName, vc, handler);
- }
- base.BeginCheck(descriptiveName, vc, handler);
- }
- }
-
- public class Z3InstanceOptions : ProverOptions
- {
- public int Timeout { get { return TimeLimit / 1000; } }
- public int Lets {
- get
- {
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
- return CommandLineOptions.Clo.Z3lets;
- }
- }
- public bool DistZ3 = false;
- public string ExeName = "z3.exe";
- public bool InverseImplies = false;
- public string Inspector = null;
- public bool OptimizeForBv = false;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ExeName!=null);
- }
-
- protected override bool Parse(string opt)
- {
- //Contract.Requires(opt!=null);
- return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
- ParseString(opt, "INSPECTOR", ref Inspector) ||
- ParseBool(opt, "DIST", ref DistZ3) ||
- ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
- base.Parse(opt);
- }
-
- public override void PostParse()
- {
- base.PostParse();
-
- if (DistZ3) {
- ExeName = "z3-dist.exe";
- CommandLineOptions.Clo.RestartProverPerVC = true;
- }
- }
-
- public override string Help
- {
- get
- {
- return
-@"
-Z3-specific options:
-~~~~~~~~~~~~~~~~~~~~
-INSPECTOR=<string> Use the specified Z3Inspector binary.
-OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
-
-Obscure options:
-~~~~~~~~~~~~~~~~
-DIST=<bool> Use z3-dist.exe binary.
-REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
-
-" + base.Help;
- // DIST requires non-public binaries
- }
- }
- }
-
- public class Z3LineariserOptions : LineariserOptions {
- private readonly Z3InstanceOptions opts;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(opts!=null);
- }
-
-
- public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {
- Contract.Requires(opts != null);
- Contract.Requires(cce.NonNullElements(letVariables));
-
- this.opts = opts;
- this.LetVariablesAttr = letVariables;
- }
-
- public override bool UseWeights { get {
- return true;
- } }
-
- public override bool UseTypes { get {
- return true;
- } }
-
- public override bool QuantifierIds { get {
- return true;
- } }
-
- public override bool InverseImplies { get {
- return opts.InverseImplies;
- } }
-
- public override LineariserOptions SetAsTerm(bool newVal) {
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- if (newVal == AsTerm)
- return this;
- return new Z3LineariserOptions(newVal, opts, LetVariables);
- }
-
- // variables representing formulas in let-bindings have to be
- // printed in a different way than other variables
- private readonly List<VCExprVar/*!>!*/> LetVariablesAttr;
- public override List<VCExprVar/*!>!*/> LetVariables { get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
-
- return LetVariablesAttr;
- } }
-
- public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
- //Contract.Requires(furtherVar != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
- allVars.AddRange(LetVariables);
- allVars.Add(furtherVar);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
-
- public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
- //Contract.Requires(furtherVars != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/> ();
- allVars.AddRange(LetVariables);
- allVars.AddRange(furtherVars);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Z3VCExprTranslator : AxiomVCExprTranslator {
- public Z3VCExprTranslator(VCExpressionGenerator gen, Z3InstanceOptions opts) {
- Contract.Requires(gen != null);
- Contract.Requires(opts != null);
- Gen = gen;
- Opts = opts;
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments (gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses (gen);
- break;
- }
- axBuilder.Setup();
- AxBuilder = axBuilder;
- UniqueNamer namer = new UniqueNamer ();
- Namer = namer;
- this.DeclCollector =
- new TypeDeclCollector (namer, true);
- }
-
- private Z3VCExprTranslator(Z3VCExprTranslator tl) :base(tl){
- Contract.Requires(tl!=null);
- Gen = tl.Gen;
- Opts = tl.Opts; // we assume that the options have not changed
- AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
- UniqueNamer namer = (UniqueNamer)tl.Namer.Clone();
- Namer = namer;
- DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
- }
-
- public override Object Clone() {
- Contract.Ensures(Contract.Result<Object>() != null);
-
- return new Z3VCExprTranslator(this);
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(Opts!=null);
- Contract.Invariant(Gen != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
- }
-
- private readonly Z3InstanceOptions Opts;
- private readonly VCExpressionGenerator Gen;
- private readonly TypeAxiomBuilder AxBuilder;
- private readonly UniqueNamer Namer;
- private readonly TypeDeclCollector DeclCollector;
-
- public override string Lookup(VCExprVar var)
- {
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- VCExprVar v = AxBuilder.TryTyped2Untyped(var);
- if (v != null) {
- var = v;
- }
- return Namer.Lookup(var);
- }
-
- public override string translate(VCExpr expr, int polarity) {
- //Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- DateTime start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace)
- Console.Write("Linearising ... ");
-
- // handle the types in the VCExpr
- TypeEraser eraser;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
- break;
- }
- VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
- Contract.Assert(exprWithoutTypes!=null);
-
- LetBindingSorter letSorter = new LetBindingSorter(Gen);
- Contract.Assert(letSorter!=null);
- VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
- Contract.Assert(sortedExpr!=null);
- VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
- Contract.Assert(sortedAxioms!=null);
-
- DeclCollector.Collect(sortedAxioms);
- DeclCollector.Collect(sortedExpr);
- FeedTypeDeclsToProver();
- if (Opts.Lets != 3) {
- // replace let expressions with implies
- Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);
- sortedExpr = letImplier.Mutate(sortedExpr);
- sortedAxioms = letImplier.Mutate(sortedAxioms);
- }
-
- //////////////////////////////////////////////////////////////////////////
- //SubtermCollector! coll = new SubtermCollector (gen);
- //coll.Traverse(sortedExpr, true);
- //coll.Traverse(sortedAxioms, true);
- //coll.UnifyClusters();
- //Console.WriteLine(coll);
- //////////////////////////////////////////////////////////////////////////
-
- LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar/*!*/>());
-
- AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
-
- string res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
- Contract.Assert(res!=null);
-
- if (CommandLineOptions.Clo.Trace) {
- TimeSpan elapsed = DateTime.UtcNow - start;
- Console.WriteLine("finished [{0} s]", elapsed.TotalSeconds);
- }
- return res;
- }
-
- private void FeedTypeDeclsToProver() {
- foreach (string s in DeclCollector.GetNewDeclarations()) {
- Contract.Assert(s != null);
- AddTypeDecl(s);
- }
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Factory : ProverFactory
- {
-
- public override object SpawnProver(ProverOptions popts, object ctxt)
- {
- //Contract.Requires(popts != null);
- //Contract.Requires(ctxt != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)popts);
- return this.SpawnProver(cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
- cce.NonNull((DeclFreeProverContext)ctxt),
- opts);
- }
-
- public override object NewProverContext(ProverOptions options) {
- //Contract.Requires(options != null);
- //Contract.Ensures(Contract.Result<object>() != null);
-
- if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
- CommandLineOptions.Clo.BracketIdsInVC = 0;
- }
-
- Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)options);
- VCExpressionGenerator gen = new VCExpressionGenerator ();
- List<string/*!>!*/> proverCommands = new List<string/*!*/> ();
- proverCommands.Add("z3");
- proverCommands.Add("simplifyLike");
- VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
-
- return NewProverContext(gen, genOptions, opts);
- }
-
- public override ProverOptions BlankProverOptions()
- {
- Contract.Ensures(Contract.Result<ProverOptions>() != null);
- return new Z3InstanceOptions();
- }
-
- protected virtual Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx,
- Z3InstanceOptions opts) {
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(opts != null);
- Contract.Ensures(Contract.Result<Z3ProcessTheoremProver>() != null);
-
- return new Z3ProcessTheoremProver(gen, ctx, opts);
- }
-
- protected virtual DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,
- VCGenerationOptions genOptions,
- Z3InstanceOptions opts)
- {
- return new DeclFreeProverContext(gen, genOptions);
- }
- }
-}
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs deleted file mode 100644 index 19c88409..00000000 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ /dev/null @@ -1,398 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- // Visitor for collecting the occurring function symbols in a VCExpr,
- // and for creating the corresponding declarations that can be fed into
- // Z3
-
- // (should this be rather done by Context.DeclareFunction? right now,
- // the TypeErasure visitor introduces new function symbols that are
- // not passed to this method)
-
- public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
-
- private readonly UniqueNamer Namer;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Namer!=null);
- Contract.Invariant(AllDecls != null);
- Contract.Invariant(IncDecls != null);
- Contract.Invariant(cce.NonNull(KnownFunctions));
- Contract.Invariant(cce.NonNull(KnownVariables));
- Contract.Invariant(cce.NonNull(KnownTypes));
- Contract.Invariant(cce.NonNull(KnownBvOps));
- Contract.Invariant(cce.NonNull(KnownSelectFunctions));
- Contract.Invariant(cce.NonNull(KnownStoreFunctions));
-}
-
-
- private readonly bool NativeBv;
-
- public TypeDeclCollector(UniqueNamer namer, bool nativeBv) {
- Contract.Requires(namer != null);
- this.Namer = namer;
- this.NativeBv = nativeBv;
- AllDecls = new List<string/*!*/> ();
- IncDecls = new List<string/*!*/> ();
- KnownFunctions = new HashSet<Function/*!*/>();
- KnownVariables = new HashSet<VCExprVar/*!*/>();
- KnownTypes = new HashSet<Type/*!*/>();
- KnownBvOps = new HashSet<string/*!*/>();
-
- KnownStoreFunctions = new HashSet<string/*!*/>();
- KnownSelectFunctions = new HashSet<string/*!*/>();
- }
-
- internal TypeDeclCollector(UniqueNamer namer, TypeDeclCollector coll) {
- Contract.Requires(namer!=null);
- Contract.Requires(coll!=null);
- this.Namer = namer;
- this.NativeBv = coll.NativeBv;
- AllDecls = new List<string/*!*/> (coll.AllDecls);
- IncDecls = new List<string/*!*/> (coll.IncDecls);
- KnownFunctions = new HashSet<Function/*!*/>(coll.KnownFunctions);
- KnownVariables = new HashSet<VCExprVar/*!*/>(coll.KnownVariables);
- KnownTypes = new HashSet<Type/*!*/>(coll.KnownTypes);
- KnownBvOps = new HashSet<string/*!*/>(coll.KnownBvOps);
-
- KnownStoreFunctions = new HashSet<string/*!*/>(coll.KnownStoreFunctions);
- KnownSelectFunctions = new HashSet<string/*!*/>(coll.KnownSelectFunctions);
- }
-
- // not used
- protected override bool StandardResult(VCExpr node, bool arg) {
- //Contract.Requires(node != null);
- return true;
- }
-
- private readonly List<string/*!>!*/> AllDecls;
- private readonly List<string/*!>!*/> IncDecls;
-
- private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions;
- private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables;
-
- // bitvector types have to be registered as well
- private readonly HashSet<Type/*!*/>/*!*/ KnownTypes;
-
- // the names of registered BvConcatOps and BvExtractOps
- private readonly HashSet<string/*!*/>/*!*/ KnownBvOps;
-
- private readonly HashSet<string/*!*/>/*!*/ KnownStoreFunctions;
- private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions;
-
- public List<string/*!>!*/> AllDeclarations { get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));
-
- List<string/*!>!*/> res = new List<string/*!*/> ();
- res.AddRange(AllDecls);
- return res;
- } }
-
- public List<string/*!>!*/> GetNewDeclarations() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));
- List<string/*!>!*/> res = new List<string/*!*/> ();
- res.AddRange(IncDecls);
- IncDecls.Clear();
- return res;
- }
-
- private void AddDeclaration(string decl) {
- Contract.Requires(decl != null);
- AllDecls.Add(decl);
- IncDecls.Add(decl);
- }
-
- public void Collect(VCExpr expr) {
- Contract.Requires(expr != null);
- Traverse(expr, true);
- }
-
- ///////////////////////////////////////////////////////////////////////////
-
- private static string TypeToString(Type t) {
- Contract.Requires(t!= null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- return SimplifyLikeExprLineariser.TypeToString(t);
- }
-
- private void RegisterType(Type type)
- {
- Contract.Requires(type != null);
- if (KnownTypes.Contains(type)) return;
-
- if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {
- KnownTypes.Add(type);
- string declString = "";
- MapType mapType = type.AsMap;
- Contract.Assert(mapType != null);
-
- foreach (Type t in mapType.Arguments) {
- Contract.Assert(t != null);
- RegisterType(t);
- }
- RegisterType(mapType.Result);
-
- declString += "(DEFTYPE " + TypeToString(type);
-
- if (CommandLineOptions.Clo.UseArrayTheory) {
- declString += " :BUILTIN Array ";
- foreach (Type t in mapType.Arguments) {
- declString += TypeToString(t);
- declString += " ";
- }
- declString += TypeToString(mapType.Result);
- }
-
- declString += ")";
- AddDeclaration(declString);
- return;
- }
-
- if (type.IsBv && NativeBv) {
- int bits = type.BvBits;
- string name = TypeToString(type);
-
- AddDeclaration("(DEFTYPE " + name + " :BUILTIN BitVec " + bits + ")");
- // If we add the BUILTIN then the conversion axiom does not work
- AddDeclaration("(DEFOP " + name + "_to_int " + name + " $int)"); // :BUILTIN bv2int $int)");
- AddDeclaration("(DEFOP $make_bv" + bits + " $int " + name + " :BUILTIN int2bv " + bits + ")");
- string expr = "($make_bv" + bits + " (" + name + "_to_int x))";
- AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
- + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
-
- KnownTypes.Add(type);
- return;
- }
-
- if (type.IsBool || type.IsInt)
- return;
-
- if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {
- AddDeclaration("(DEFTYPE " + TypeToString(type) + ")");
- KnownTypes.Add(type);
- return;
- }
-
- }
-
- public override bool Visit(VCExprNAry node, bool arg) {
- Contract.Requires(node != null);
- // there are a couple cases where operators have to be
- // registered by generating appropriate Z3 statements
-
- if (node.Op is VCExprBvOp) {
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node.Type);
- }
- } else if (node.Op is VCExprBvConcatOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node.Type);
-
- string name = SimplifyLikeExprLineariser.BvConcatOpName(node);
- if (!KnownBvOps.Contains(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN concat)");
- KnownBvOps.Add(name);
- }
- }
- //
- } else if (node.Op is VCExprBvExtractOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node.Type);
-
- VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
- Contract.Assert(op!=null);
- string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
- if (!KnownBvOps.Contains(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN extract " +
- (op.End - 1) + " " + op.Start + ")");
- KnownBvOps.Add(name);
- }
- }
- //
- } else if (node.Op is VCExprStoreOp) {
- RegisterType(node.Type); // this is the map type, registering it should register also the index and value types
- string name = SimplifyLikeExprLineariser.StoreOpName(node);
- if (!KnownStoreFunctions.Contains(name)) {
- string decl = "(DEFOP " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- if (CommandLineOptions.Clo.UseArrayTheory)
- decl += " :BUILTIN store";
- decl += ")";
- AddDeclaration(decl);
-
- if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {
- var sel = SimplifyLikeExprLineariser.SelectOpName(node);
-
- if (!KnownSelectFunctions.Contains(name)) {
- // need to declare it before reference
- string seldecl = "(DEFOP " + sel;
- foreach (VCExpr ch in node) {
- seldecl += " " + TypeToString(ch.Type);
- }
- AddDeclaration(seldecl + ")");
- KnownSelectFunctions.Add(name);
- }
-
- var eq = "EQ";
- if (node[node.Arity - 1].Type.IsBool)
- eq = "IFF";
-
- string ax1 = "(BG_PUSH (FORALL (";
- string ax2 = "(BG_PUSH (FORALL (";
- string argX = "", argY = "";
- string dist = "";
- for (int i = 0; i < node.Arity; i++) {
- var t = " :TYPE " + TypeToString(node[i].Type);
- var x = " x" + i;
- var y = " y" + i;
- ax1 += x + t;
- ax2 += x + t;
- if (i != 0 && i != node.Arity - 1) {
- argX += x;
- argY += y;
- ax2 += y + t;
- dist += " (NEQ" + x + y + ")";
- }
- }
- string v = " x" + (node.Arity - 1);
- ax1 += ") ";
- ax1 += "(" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argX + ") " + v + ")";
- ax1 += "))";
-
- ax2 += ") ";
- ax2 += "(IMPLIES (OR " + dist + ") (" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argY + ") (" + sel + " x0" + argY + ")))";
- ax2 += "))";
-
- AddDeclaration(ax1);
- AddDeclaration(ax2);
- }
-
- KnownStoreFunctions.Add(name);
- }
- //
- } else if (node.Op is VCExprSelectOp) {
- //
- RegisterType(node[0].Type);
- string name = SimplifyLikeExprLineariser.SelectOpName(node);
- if (!KnownSelectFunctions.Contains(name)) {
- string decl = "(DEFOP " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- if (CommandLineOptions.Clo.UseArrayTheory)
- decl += " :BUILTIN select";
- decl += ")";
- AddDeclaration(decl);
- KnownSelectFunctions.Add(name);
- }
- //
- } else {
- //
- VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
- if (op != null && !KnownFunctions.Contains(op.Func)) {
- Function f = op.Func;
- Contract.Assert(f!=null);
- string printedName = Namer.GetName(f, f.Name);
- Contract.Assert(printedName!=null);
- string decl = "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName);
-
- foreach (Variable v in f.InParams) {
- Contract.Assert(v!=null);
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
- Contract.Assert(f.OutParams.Length == 1);
- foreach (Variable v in f.OutParams) {
- Contract.Assert(v!=null);
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
-
- string builtin = ExtractBuiltin(f);
- if (builtin != null)
- decl += " :BUILTIN " + builtin;
-
- decl += ")";
-
- AddDeclaration(decl);
- KnownFunctions.Add(f);
- }
- //
- }
-
- return base.Visit(node, arg);
- }
-
- private string ExtractBuiltin(Function f) {
- Contract.Requires(f != null);
- string retVal = null;
- if (NativeBv) {
- retVal = f.FindStringAttribute("bvbuiltin");
- }
- if (retVal == null) {
- retVal = f.FindStringAttribute("builtin");
- }
- return retVal;
- }
-
- public override bool Visit(VCExprVar node, bool arg) {
- Contract.Requires(node != null);
- if (!BoundTermVars.Contains(node) && !KnownVariables.Contains(node)) {
- RegisterType(node.Type);
- string printedName = Namer.GetName(node, node.Name);
- Contract.Assert(printedName!=null);
- string decl =
- "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
- + " " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
- KnownVariables.Add(node);
- }
-
- return base.Visit(node, arg);
- }
-
- public override bool Visit(VCExprQuantifier node, bool arg) {
- Contract.Requires(node != null);
- foreach (VCExprVar v in node.BoundVars) {
- Contract.Assert(v != null);
- RegisterType(v.Type);
- }
-
- return base.Visit(node, arg);
- }
- }
-}
\ No newline at end of file diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj deleted file mode 100644 index e559b663..00000000 --- a/Source/Provers/Z3/Z3.csproj +++ /dev/null @@ -1,218 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Microsoft.Boogie.Z3</RootNamespace>
- <AssemblyName>Provers.Z3</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile>Client</TargetFrameworkProfile>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for Z3.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core">
- <RequiredTargetFramework>3.5</RequiredTargetFramework>
- </Reference>
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Inspector.cs" />
- <Compile Include="Prover.cs" />
- <Compile Include="ProverInterface.cs" />
- <Compile Include="TypeDeclCollector.cs" />
- <Compile Include="..\..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- <ProjectReference Include="..\Simplify\Simplify.csproj">
- <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
- <Name>Simplify</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </ItemGroup>
- <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
-</Project>
\ No newline at end of file diff --git a/Source/Provers/Z3/cce.cs b/Source/Provers/Z3/cce.cs deleted file mode 100644 index ef594484..00000000 --- a/Source/Provers/Z3/cce.cs +++ /dev/null @@ -1,193 +0,0 @@ -using System;
-using SA=System.Attribute;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using Microsoft.Boogie;
-
-/// <summary>
-/// A class containing static methods to extend the functionality of Code Contracts
-/// </summary>
-
-public static class cce {
- //[Pure]
- //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
- // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
- //}
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
- }
- //[Pure]
- //public static bool NonNullElements(VariableSeq collection) {
- // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- //}
- /// <summary>
- /// For possibly-null lists of non-null elements
- /// </summary>
- /// <typeparam name="T"></typeparam>
- /// <param name="collection"></param>
- /// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param>
- /// <returns></returns>
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
- return (nullability && collection == null) || cce.NonNullElements(collection);
- //Should be the same as:
- /*if(nullability&&collection==null)
- * return true;
- * return cce.NonNullElements(collection)
- */
-
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
- return kvp.Key != null && kvp.Value != null;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
- return iEnumerator != null;
- }
- //[Pure]
- //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
- // return cce.NonNullElements(graph.TopologicalSort());
- //}
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- [Pure]
- public static bool IsNew(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- [Pure]
- public static bool Different(object o, object p) {
- return true;
- }
- [Pure]
- public static bool New(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
- //[Pure]
- //public static bool IsValid(Microsoft.Dafny.Expression expression) {
- // return true;
- //}
- //public static List<T> toList<T>(PureCollections.Sequence s) {
- // List<T> toRet = new List<T>();
- // foreach (T t in s.elems)
- // if(t!=null)
- // toRet.Add(t);
- // return toRet;
- //}
-
- //internal static bool NonNullElements(Set set) {
- // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
- //}
-}
-
-public class PeerAttribute : SA {
-}
-public class RepAttribute : SA {
-}
-public class CapturedAttribute : SA {
-}
-public class NotDelayedAttribute : SA {
-}
-public class NoDefaultContractAttribute : SA {
-}
-public class VerifyAttribute : SA {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : SA {
-}
-public class AdditiveAttribute : SA {
-}
-public class ReadsAttribute : SA {
- public enum Reads {
- Nothing,
- Everything,
- };
- public ReadsAttribute(object o) {
- }
-}
-public class GlobalAccessAttribute : SA {
- public GlobalAccessAttribute(bool b) {
- }
-}
-public class EscapesAttribute : SA {
- public EscapesAttribute(bool b, bool b_2) {
- }
-}
-public class NeedsContractsAttribute : SA {
- public NeedsContractsAttribute() {
- }
- public NeedsContractsAttribute(bool ret, bool parameters) {
- }
- public NeedsContractsAttribute(bool ret, int[] parameters) {
- }
-}
-public class ImmutableAttribute : SA {
-}
-public class InsideAttribute : SA {
-}
-public class SpecPublicAttribute : SA {
-}
-public class ElementsPeerAttribute : SA {
-}
-public class ResultNotNewlyAllocatedAttribute : SA {
-}
-public class OnceAttribute : SA {
-}
\ No newline at end of file |