Boogie: Committing my port of simplify, along with the slightly changed references of simplify's dependents.

1 files changed, 392 insertions, 258 deletions

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index dbd3ac19..923a62ef 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -10,25 +10,28 @@ using System.Threading;
 using System.IO;

 using System.Text;

 using System.Diagnostics;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.Simplify;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Boogie.TypeErasure;

 

-namespace Microsoft.Boogie.Simplify

-{

-  public abstract class LogProverInterface : ProverInterface

-  {

+namespace Microsoft.Boogie.Simplify {

+  public abstract class LogProverInterface : ProverInterface {

     [NotDelayed]

-    protected LogProverInterface(ProverOptions! options,

-        string! openComment, string! closeComment,

-        string! openActivity, string! closeActivity,

-        VCExpressionGenerator! gen)

-      ensures this.gen == gen;

-    {

+    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!> ();

+        this.commonPrefix = new List<string>();

       } else {

         this.logFileWriter = options.OpenLog(null);

       }

@@ -38,7 +41,6 @@ namespace Microsoft.Boogie.Simplify
       this.closeActivityString = closeActivity;

       this.gen = gen;

       this.options = options;

-      base();

 

       if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {

         // Emit version comment in the log

@@ -46,34 +48,49 @@ namespace Microsoft.Boogie.Simplify
         LogCommonComment(CommandLineOptions.Clo.Environment);

       }

     }

-    

-    [StrictReadonly][Additive]

-    protected readonly VCExpressionGenerator! gen;

+

+    [StrictReadonly]

+    [Additive]

+    protected readonly VCExpressionGenerator gen;

 

     private TextWriter/*?*/ logFileWriter;

-    [Microsoft.Contracts.StrictReadonly]

-    private readonly string! openCommentString;

-    [Microsoft.Contracts.StrictReadonly]

-    private readonly string! closeCommentString;

-    [Microsoft.Contracts.StrictReadonly]

-    private readonly string! openActivityString;

-    [Microsoft.Contracts.StrictReadonly]

-    private readonly string! closeActivityString;

-    [Microsoft.Contracts.StrictReadonly]

-    protected readonly ProverOptions! options;

-    [Microsoft.Contracts.StrictReadonly]

-    private readonly List<string!>/*?*/ commonPrefix;

-

-    public void LogActivity(string! s) {

+    [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(cce.NonNullElements(commonPrefix));

+    }

+

+

+    public void LogActivity(string s) {

+      Contract.Requires(s != null);

       LogActivity(s, false);

     }

 

-    public void LogCommon(string! s) {

+    public void LogCommon(string s) {

+      Contract.Requires(s != null);

       LogActivity(s, true);

     }

 

-    private void LogActivity(string! s, bool common) {

-      assume common || !options.SeparateLogFiles || logFileWriter != null;

+    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);

@@ -90,19 +107,19 @@ namespace Microsoft.Boogie.Simplify
     /// 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)

-    {

+    public override void LogComment(string comment) {

+      Contract.Requires(comment != null);

       LogComment(comment, false);

     }

 

-    public void LogCommonComment(string! comment)

-    {

+    public void LogCommonComment(string comment) {

+      Contract.Requires(comment != null);

       LogComment(comment, true);

     }

 

-    private void LogComment(string! comment, bool common)

-    {

-      assume common || !options.SeparateLogFiles || logFileWriter != null;

+    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);

@@ -114,16 +131,18 @@ namespace Microsoft.Boogie.Simplify
       }

     }

 

-    public virtual void NewProblem(string! descName)

-    {

+    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)

+          foreach (string s in commonPrefix) {

+            Contract.Assert(s != null);

             logFileWriter.WriteLine(s);

+          }

         }

       }

       LogComment("Proof obligation: " + descName);

@@ -136,82 +155,104 @@ namespace Microsoft.Boogie.Simplify
       }

     }

 

-    public override VCExpressionGenerator! VCExprGen

-    {

-      get { return this.gen; }

+    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;

 

-  public abstract class ProcessTheoremProver : LogProverInterface

-  {

-    private static string! _proverPath;

+    protected AxiomVCExprTranslator vcExprTranslator {

+      get {

+        Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);

 

-    protected AxiomVCExprTranslator! vcExprTranslator { get {

-      return (AxiomVCExprTranslator!)ctx.exprTranslator;

-    } }

+        return cce.NonNull((AxiomVCExprTranslator)ctx.exprTranslator);

+      }

+    }

 

-    protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator(ProverOptions! p);

+    protected abstract AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p);

 

     // Return the number of axioms pushed to the theorem prover

-    protected int FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

+    protected int FeedNewAxiomsDecls2Prover() {

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       if (thmProver == null)

         return 0;

       int ret = 0;

-      foreach (string! s in vcExprTranslator.NewTypeDecls) {

+      foreach (string s in vcExprTranslator.NewTypeDecls) {

+        Contract.Assert(s != null);

         LogCommon(s);

         thmProver.Feed(s, 0);

       }

-      foreach (string! s in vcExprTranslator.NewAxioms) {

+      foreach (string s in vcExprTranslator.NewAxioms) {

+        Contract.Assert(s != null);

         LogBgPush(s);

         thmProver.AddAxioms(s);

-        ret ++;

+        ret++;

       }

       return ret;

     }

 

-    protected static string! CodebaseString() {

-      return Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);

+    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.NonNullElements(BackgroundPredicates));

+      Contract.Invariant(BackgroundPredFilename != null);

+      Contract.Invariant(ctx != null);

     }

 

-    private static IDictionary<string!, string!>! BackgroundPredicates =

-      new Dictionary<string!, string!> ();

+    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);

 

-    protected static string! GetBackgroundPredicate(string! filename) {

       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))

-        {

+        using (StreamReader reader = new System.IO.StreamReader(univBackPredPath)) {

           res = reader.ReadToEnd();

         }

         BackgroundPredicates.Add(filename, res);

       }

-      return (!)res;

+      return cce.NonNull(res);

     }

 

-    static void InitializeGlobalInformation(string! proverExe)

-      ensures _proverPath != null;

+    static void InitializeGlobalInformation(string proverExe)

+

       //throws ProverException, System.IO.FileNotFoundException;

     {

+

+      Contract.Requires(proverExe != null);

+      Contract.Ensures(_proverPath != null);

       if (_proverPath == null) {

         // Initialize '_proverPath'

         _proverPath = Path.Combine(CodebaseString(), proverExe);

         string firstTry = _proverPath;

 

         string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");

-        assert programFiles != null;

+        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!> attempts = new List<string!>();

+        List<string> attempts = new List<string>();

         for (int minorVersion = 15; true; minorVersion--) {

           if (File.Exists(_proverPath)) {

             break;  // all seems good

@@ -242,24 +283,30 @@ namespace Microsoft.Boogie.Simplify
       }

     }

 

-    [Rep] protected internal ProverProcess thmProver;

+    [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;

-    

+    protected DeclFreeProverContext ctx;

+    protected string BackgroundPredFilename;

+    protected ConsoleCancelEventHandler cancelEvent;

+

     [NotDelayed]

-    public ProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx,

-                                string! proverExe, string! backgroundPred)

-      throws UnexpectedProverOutputException;

-    {

+    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;

-      base(options, "; ", "", "", "", gen);

-      

+

+

       // 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

@@ -269,8 +316,8 @@ namespace Microsoft.Boogie.Simplify
         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

+        List<string> x = tl.NewAxioms;

+        //x = x;  // make the compiler happy: somebody uses the value of x

         x = tl.NewTypeDecls;

       }

     }

@@ -278,40 +325,38 @@ namespace Microsoft.Boogie.Simplify
     /// <summary>

     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)

     /// </summary>

-    public override void PushVCExpression(VCExpr! vc) 

-    {

-      vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) ); 

+    public override void PushVCExpression(VCExpr vc) {

+      Contract.Requires(vc != null);

+      vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));

     }

-    

-    public override string! VCExpressionToString(VCExpr! vc)

-    {

+

+    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;

+    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() 

-      throws UnexpectedProverOutputException;

-    {

-       return FeedNewAxiomsDecls2Prover();

+    public override int FlushAxiomsToTheoremProver() {

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+      return FeedNewAxiomsDecls2Prover();

     }

 

-    public override void Pop() 

-      throws UnexpectedProverOutputException;

-    {

-       assert thmProver != null;

-       LogCommon("(BG_POP)");

-       thmProver.PopAxioms();

+    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)

-    {

+    void ControlCHandler(object o, ConsoleCancelEventArgs a) {

       if (thmProver != null) {

         thmProver.Kill();

       }

@@ -323,46 +368,50 @@ namespace Microsoft.Boogie.Simplify
         cancelEvent = null;

       }

       if (thmProver != null) {

-        expose (this) {

+        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)

-    {

+    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 = 

+        int num_axioms_pushed =

            FeedNewAxiomsDecls2Prover();

-        

-        string! prelude = ctx.GetProverCommands(false);

+

+        string prelude = ctx.GetProverCommands(false);

+        Contract.Assert(prelude != null);

         vcString = prelude + vcString;

         LogActivity(vcString);

 

-        assert thmProver != null;

+        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.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) {

@@ -374,9 +423,10 @@ namespace Microsoft.Boogie.Simplify
       }

     }

 

-    public override Outcome CheckOutcome(ErrorHandler! handler)

-      throws UnexpectedProverOutputException;

-    {

+    public override Outcome CheckOutcome(ErrorHandler handler) {

+      Contract.Requires(handler != null);

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

       if (this.thmProver == null) {

         return Outcome.Undetermined;

       }

@@ -387,61 +437,62 @@ namespace Microsoft.Boogie.Simplify
 

           if (options.ForceLogStatus) {

             switch (result) {

-            case ProverProcess.ProverOutcome.Valid:

-              LogActivity("DBG_WAS_VALID");

-              break;

-            case ProverProcess.ProverOutcome.NotValid:

-              LogActivity("DBG_WAS_INVALID");

-              break;

+              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;

+            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;

         }

       }

 

-      assume proverException != null;

+      Contract.Assume(proverException != null);

       LogComment("***** Unexpected prover output");

-      expose (this) {

+      cce.BeginExpose(this);

+      {

         currentProverHasBeenABadBoy = true;  // this will cause the next resurrect to restart the prover

       }

+      cce.EndExpose();

       throw proverException;

     }

 

-    protected virtual void ResurrectProver()

-      throws UnexpectedProverOutputException;

-    {

-      expose (this) {

+    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)

-          {

+              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;

@@ -449,11 +500,13 @@ namespace Microsoft.Boogie.Simplify
         }

         FireUpNewProver();

       }

+      cce.EndExpose();

     }

-    

-    protected abstract ProverProcess! CreateProverProcess(string! proverPath);

-    

-    public void LogBgPush(string! s) {

+

+    protected abstract ProverProcess CreateProverProcess(string proverPath);

+

+    public void LogBgPush(string s) {

+      Contract.Requires(s != null);

       LogCommon("(BG_PUSH ");

       LogCommon(s);

       LogCommon(")");

@@ -462,33 +515,37 @@ namespace Microsoft.Boogie.Simplify
     public void LogBgPop() {

       LogCommon("(BG_POP)");

     }

-    

+

     [NoDefaultContract]

     private void FireUpNewProver()

-      requires IsExposed;

-      requires thmProver == null;

-      throws UnexpectedProverOutputException;

     {

+            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')) {

+        foreach (string s in thmProver.OptionComments().Split('\n')) {Contract.Assert(s != null);

           LogCommonComment(s);

         }

-        foreach (string! parmsetting in thmProver.ParameterSettings) {

+        foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);

           LogCommon(parmsetting);

         }

       }

-      foreach (string! parmsetting in thmProver.ParameterSettings) {

+      foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);

         thmProver.Feed(parmsetting, 0);

       }

       thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);

-      string! incProverCommands = ctx.GetProverCommands(false);

-      string! proverCommands = ctx.GetProverCommands(true);

-      string! prelude = ctx.GetProverCommands(false);

+      string incProverCommands = ctx.GetProverCommands(false);

+      Contract.Assert(incProverCommands != null);

+      string proverCommands = ctx.GetProverCommands(true);

+      Contract.Assert(proverCommands != null);

+      string prelude = ctx.GetProverCommands(false);

+      Contract.Assert(prelude != null);

 

       if (restarts == 0) {

         // log the stuff before feeding it into the prover, so when it dies

@@ -497,10 +554,10 @@ namespace Microsoft.Boogie.Simplify
         LogCommon(prelude);

         LogCommon(proverCommands);

 

-        foreach (string! s in vcExprTranslator.AllTypeDecls)

-          LogCommon(s);

-        foreach (string! s in vcExprTranslator.AllAxioms)

-          LogBgPush(s);

+        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.");

       } else {

@@ -510,38 +567,62 @@ namespace Microsoft.Boogie.Simplify
       thmProver.Feed(prelude, 0);

       thmProver.Feed(proverCommands, 0);

 

-      foreach (string! s in vcExprTranslator.AllTypeDecls)

-        thmProver.Feed(s, 0);

-      foreach (string! s in vcExprTranslator.AllAxioms)

-        thmProver.AddAxioms(s);

+      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

+      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 { return this.ctx; }

+    public override ProverContext Context {

+      get {

+        Contract.Ensures(Contract.Result<ProverContext>() != null);

+        return this.ctx;

+      }

     }

   }

-  

-  public class SimplifyTheoremProver : ProcessTheoremProver

-  {

+  [ContractClassFor(typeof(ProcessTheoremProver))]

+  public 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 SimplifyTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx)

-      throws UnexpectedProverOutputException;

-    {

-      base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx");

+    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) {

+

+    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) {

+    protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {

+      Contract.Requires(opts!=null);

+      Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);

+

       return new SimplifyVCExprTranslator(gen);

     }

   }

@@ -552,51 +633,70 @@ namespace Microsoft.Boogie.Simplify
 

   public abstract class AxiomVCExprTranslator : VCExprTranslator {

     protected AxiomVCExprTranslator() {

-      AllAxioms = new List<string!> ();

-      NewAxiomsAttr = new List<string!> ();

-      AllTypeDecls = new List<string!> ();

-      NewTypeDeclsAttr = new List<string!> ();

+      AllAxioms = new List<string> ();

+      NewAxiomsAttr = new List<string> ();

+      AllTypeDecls = new List<string> ();

+      NewTypeDeclsAttr = new List<string> ();

     }

 

-    protected AxiomVCExprTranslator(AxiomVCExprTranslator! tl) {

-      AllAxioms = new List<string!> (tl.AllAxioms);

-      NewAxiomsAttr = new List<string!> (tl.NewAxiomsAttr);

-      AllTypeDecls = new List<string!> (tl.AllTypeDecls);

-      NewTypeDeclsAttr = new List<string!> (tl.NewTypeDeclsAttr);

+    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;

+    public readonly List<string/*!>!*/> AllAxioms;

+    private List<string/*!>!*/> NewAxiomsAttr;

 

     // The length of the list NewAxiomsAttr

-    public int NewAxiomsCount { get {

-      return NewAxiomsAttr.Count;

-    } }

+    public int NewAxiomsCount {

+      get {

+        return NewAxiomsAttr.Count;

+      }

+    }

 

-    public List<string!>! NewAxioms { get {

-      List<string!>! res = NewAxiomsAttr;

-      NewAxiomsAttr = new List<string!> ();

-      return res;

-    } }

+    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;

-    } }

+    // 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) {

+    public void AddAxiom(string axiom) {

+      Contract.Requires(axiom != null);

       AllAxioms.Add(axiom);

       NewAxiomsAttr.Add(axiom);

     }

 

-    public void AddTypeDecl(string! typeDecl) {

+    public void AddTypeDecl(string typeDecl) {

+      Contract.Requires(typeDecl != null);

       AllTypeDecls.Add(typeDecl);

       NewTypeDeclsAttr.Add(typeDecl);

     }

@@ -607,47 +707,65 @@ namespace Microsoft.Boogie.Simplify
   // -----------------------------------------------------------------------------------------------

 

   public class SimplifyVCExprTranslator : AxiomVCExprTranslator {

-    public SimplifyVCExprTranslator(VCExpressionGenerator! gen) {

+    public SimplifyVCExprTranslator(VCExpressionGenerator gen) {

+      Contract.Requires(gen != null);

       Gen = gen;

-      TypeAxiomBuilder! axBuilder;

+      TypeAxiomBuilder axBuilder;

       switch (CommandLineOptions.Clo.TypeEncodingMethod) {

         case CommandLineOptions.TypeEncoding.Arguments:

-          axBuilder = new TypeAxiomBuilderArguments (gen);

+          axBuilder = new TypeAxiomBuilderArguments(gen);

           break;

         default:

-          axBuilder = new TypeAxiomBuilderPremisses (gen);

+          axBuilder = new TypeAxiomBuilderPremisses(gen);

           break;

       }

       axBuilder.Setup();

       AxBuilder = axBuilder;

-      Namer = new UniqueNamer ();

-      LitAbstracter = new BigLiteralAbstracter (gen);

+      Namer = new UniqueNamer();

+      LitAbstracter = new BigLiteralAbstracter(gen);

     }

 

-    private SimplifyVCExprTranslator(SimplifyVCExprTranslator! tl) {

-      base(tl);

+    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() {

+    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;

+    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);

 

-    public override string! Lookup(VCExprVar! var)

-    {

       return Namer.Lookup(var);

     }

-    

-    public override string! translate(VCExpr! expr, int polarity) {

-      Let2ImpliesMutator! letImplier = new Let2ImpliesMutator(Gen);

+

+    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;

@@ -662,20 +780,27 @@ namespace Microsoft.Boogie.Simplify
           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);

           break;

       }

-      VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;

+      VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;

+      Contract.Assert(exprWithoutTypes != null);

 

-      TermFormulaFlattener! flattener = new TermFormulaFlattener(Gen);

-      VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);

-      VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);

+      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);

+      VCExpr exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);

+      Contract.Assert(exprWithoutBigLits != null);

       AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),

                                                            Namer));

 

       // type axioms

-      VCExpr! axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());

-      VCExpr! axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);

+      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);

@@ -686,36 +811,45 @@ namespace Microsoft.Boogie.Simplify
   // -----------------------------------------------------------------------------------------------

   // -----------------------------------------------------------------------------------------------

 

-  public class Factory : ProverFactory

-  {

-    public override object! SpawnProver(ProverOptions! options, object! ctxt)

-    {

+  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,

-                                       ((DeclFreeProverContext!)ctxt).ExprGen,

-                                       (DeclFreeProverContext!)ctxt);

+                                       cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,

+                                       cce.NonNull((DeclFreeProverContext)ctxt));

     }

 

-    public override object! NewProverContext(ProverOptions! options) {

+    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();

-      List<string!>! proverCommands = new List<string!> ();

+      VCExpressionGenerator gen = new VCExpressionGenerator();

+      Contract.Assert(gen != null);

+      List<string>/*!>!*/ proverCommands = new List<string> ();

+      Contract.Assert(cce.NonNullElements(proverCommands));

       proverCommands.Add("all");

       proverCommands.Add("simplify");

       proverCommands.Add("simplifyLike");

       return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));

     }

 

-    public override CommandLineOptions.VCVariety DefaultVCVariety

-    {

-      get { return CommandLineOptions.VCVariety.BlockNested; }

+    public override CommandLineOptions.VCVariety DefaultVCVariety {

+      get {

+        return CommandLineOptions.VCVariety.BlockNested;

+      }

     }

 

     // needed to make test7 pass

-    public override bool SupportsDags

-    {

-      get { return true; }

+    public override bool SupportsDags {

+      get {

+        return true;

+      }

     }

   }

 }