Boogie: VCGeneration port part 1/3: Replacing old source files with ported version

1 files changed, 178 insertions, 93 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 4bd6edea..20f4035b 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -9,7 +9,7 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Basetypes;

@@ -24,9 +24,17 @@ namespace Microsoft.Boogie
   /// </summary>

   public sealed class Checker 

   {

-    private readonly VCExpressionGenerator! gen;

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(gen!=null);

+      Contract.Invariant(thmProver != null);

+      Contract.Invariant(ProverDone != null);

+}

+

+    private readonly VCExpressionGenerator gen;

     

-    private ProverInterface! thmProver;

+    private ProverInterface thmProver;

     private CommandLineOptions.BvHandling bitvectors;

     private int timeout;

 

@@ -40,14 +48,14 @@ namespace Microsoft.Boogie
     private volatile ProverInterface.ErrorHandler handler;

     private volatile bool closed;

 

-    public readonly AutoResetEvent! ProverDone = new AutoResetEvent(false);

+    public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);

 

     private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl)

     {

       if (impl == null) return CommandLineOptions.Clo.Bitvectors;

       bool force_int = false;

       bool force_native = false;

-      ((!)impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

+      cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

       impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

       impl.CheckBooleanAttribute("forceBvInt", ref force_int);

       impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

@@ -61,24 +69,33 @@ namespace Microsoft.Boogie
       return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);

     }

 

-    public VCExpressionGenerator! VCExprGen

+    public VCExpressionGenerator VCExprGen

     {

-      get { return this.gen; }

+      get {Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);

+ return this.gen; }

     }

-    public ProverInterface! TheoremProver

+    public ProverInterface TheoremProver

     {

-      get { return this.thmProver; }

+      get {Contract.Ensures(Contract.Result<ProverInterface>() != null);

+ return this.thmProver; }

     }

 

     /////////////////////////////////////////////////////////////////////////////////

     // We share context information for the same program between different Checkers

 

     private struct ContextCacheKey {

-      public readonly Program! program;

+      [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(program!=null);

+}

+

+      public readonly Program program;

       public readonly CommandLineOptions.BvHandling bitvectors;

 

-      public ContextCacheKey(Program! prog,

+      public ContextCacheKey(Program prog,

                              CommandLineOptions.BvHandling bitvectors) {

+        Contract.Requires(prog != null);

         this.program = prog;

         this.bitvectors = bitvectors;

       }

@@ -104,12 +121,14 @@ namespace Microsoft.Boogie
     /// <summary>

     /// Constructor.  Initialize a checker with the program and log file.

     /// </summary>

-    public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout)

+    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout)

     {

+      Contract.Requires(vcgen != null);

+      Contract.Requires(prog != null);

       this.bitvectors = BvHandlingForImpl(impl);

       this.timeout = timeout;

 

-      ProverOptions! options = ((!)CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

+      ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

 

       if (logFilePath != null) {

         options.LogFilename = logFilePath;

@@ -129,25 +148,27 @@ namespace Microsoft.Boogie
       ProverInterface prover;

 

       if (vcgen.CheckerCommonState == null) {

-        vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext!> ();

+        vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext> ();

       }

-      IDictionary<ContextCacheKey, ProverContext!>! cachedContexts = (IDictionary<ContextCacheKey, ProverContext!>) vcgen.CheckerCommonState;

+      IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>) vcgen.CheckerCommonState;

 

       if (cachedContexts.TryGetValue(key, out ctx)) {

-        ctx = (ProverContext!)((!)ctx).Clone();

+        ctx = (ProverContext)cce.NonNull(ctx).Clone();

         prover = (ProverInterface)

           CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

       } else {

-        ctx = (ProverContext!)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

+        ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

         // set up the context

-        foreach (Declaration! decl in prog.TopLevelDeclarations) {

+        foreach (Declaration decl in prog.TopLevelDeclarations) {

+          Contract.Assert(decl != null);

           TypeCtorDecl t = decl as TypeCtorDecl;

           if (t != null) {

             ctx.DeclareType(t, null);

           }

         }

-        foreach (Declaration! decl in prog.TopLevelDeclarations) {

+        foreach (Declaration decl in prog.TopLevelDeclarations) {

+          Contract.Assert(decl != null);

           Constant c = decl as Constant;

           if (c != null) {

             ctx.DeclareConstant(c, c.Unique, null);

@@ -158,7 +179,8 @@ namespace Microsoft.Boogie
             }

           }

         }

-        foreach (Declaration! decl in prog.TopLevelDeclarations) {

+        foreach (Declaration decl in prog.TopLevelDeclarations) {

+          Contract.Assert(decl != null);

           bool expand = false;

           Axiom ax = decl as Axiom;

           decl.CheckBooleanAttribute("inline", ref expand);

@@ -166,7 +188,8 @@ namespace Microsoft.Boogie
             ctx.AddAxiom(ax, null);

           }

         }

-        foreach (Declaration! decl in prog.TopLevelDeclarations) {

+        foreach (Declaration decl in prog.TopLevelDeclarations) {

+          Contract.Assert(decl != null);

           GlobalVariable v = decl as GlobalVariable;

           if (v != null) {

             ctx.DeclareGlobalVariable(v, null);

@@ -178,7 +201,7 @@ namespace Microsoft.Boogie
         // the context to be cached

         prover = (ProverInterface)

           CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

-        cachedContexts.Add(key, (ProverContext!)ctx.Clone());

+        cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone()));

       }

       

       this.thmProver = prover;

@@ -201,8 +224,9 @@ namespace Microsoft.Boogie
     /// Push a Verification Condition as an Axiom 

     /// (Required for Doomed Program Point detection)

     /// </summary>

-    public void PushVCExpr(VCExpr! vc)

+    public void PushVCExpr(VCExpr vc)

     {

+      Contract.Requires(vc != null);

       //thmProver.Context.AddAxiom(vc);      

       thmProver.PushVCExpression(vc);

     }

@@ -230,7 +254,7 @@ namespace Microsoft.Boogie
     private void WaitForOutput(object dummy)

     {

       try {

-        outcome = thmProver.CheckOutcome((!)handler);

+        outcome = thmProver.CheckOutcome(cce.NonNull(handler));

       } catch (UnexpectedProverOutputException e) {

         outputExn = e;

       }

@@ -253,17 +277,20 @@ namespace Microsoft.Boogie
           break;

       }

 

-      assert busy;

+      Contract.Assert( busy);

       hasOutput = true;

       proverRunTime = DateTime.Now - proverStart;

 

       ProverDone.Set();

     }

     

-    public void BeginCheck(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler) 

-      requires !IsBusy;

-    {

-      assert !busy;

+    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler){

+      Contract.Requires(descriptiveName != null);

+      Contract.Requires(vc != null);

+      Contract.Requires(handler != null);

+      

+      Contract.Requires( !IsBusy);

+      Contract.Assert( !busy);

       busy = true;

       hasOutput = false;

       outputExn = null;

@@ -276,11 +303,11 @@ namespace Microsoft.Boogie
       ThreadPool.QueueUserWorkItem(WaitForOutput);

     }

 

-    public ProverInterface.Outcome ReadOutcome()

-      throws UnexpectedProverOutputException;

-      requires IsBusy;

-      requires HasOutput;

-    {

+    public ProverInterface.Outcome ReadOutcome(){

+      

+      Contract.Requires( IsBusy);

+      Contract.Requires( HasOutput);

+      Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

       hasOutput = false;

       busy = false;

 

@@ -297,13 +324,31 @@ namespace Microsoft.Boogie
   // -----------------------------------------------------------------------------------------------

 

   public class ErrorModel {

-    public Dictionary<string!, int>! identifierToPartition;

-    public List<List<string!>>! partitionToIdentifiers;

-    public List<Object>! partitionToValue;  

-    public Dictionary<object, int>! valueToPartition;

-    public Dictionary<string!, List<List<int>>!>! definedFunctions;

+    public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;

+    public List<List<string/*!>>!*/>> partitionToIdentifiers;

+    public List<Object>/*!*/ partitionToValue;  

+    public Dictionary<object, int>/*!*/ valueToPartition;

+    public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;

+

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(cce.NonNullElements(identifierToPartition));

+      Contract.Invariant(partitionToIdentifiers != null);

+      Contract.Invariant(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));

+      Contract.Invariant(partitionToValue != null);

+      Contract.Invariant(valueToPartition != null);

+      Contract.Invariant(cce.NonNullElements(definedFunctions));

+}

+

 

-    public ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions) {

+    public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {

+      Contract.Requires(cce.NonNullElements(identifierToPartition));

+      Contract.Requires(partitionToIdentifiers != null);

+      Contract.Requires(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));

+      Contract.Requires(partitionToValue != null);

+      Contract.Requires(valueToPartition != null);

+      Contract.Requires(cce.NonNullElements(definedFunctions));

       this.identifierToPartition = identifierToPartition;

       this.partitionToIdentifiers = partitionToIdentifiers;

       this.partitionToValue = partitionToValue;

@@ -311,17 +356,18 @@ namespace Microsoft.Boogie
       this.definedFunctions = definedFunctions;

     }

 

-    public virtual void Print(TextWriter! writer) { }

+    public virtual void Print(TextWriter writer) {Contract.Requires(writer != null); }

     

     public int LookupPartitionValue(int partition)

     {

-      BigNum bignum = (BigNum) (!)partitionToValue[partition];

+      BigNum bignum = (BigNum) cce.NonNull(partitionToValue)[partition];

       return bignum.ToInt;

     }

         

     public int LookupControlFlowFunctionAt(int cfc, int id)

     {

-      List<List<int>>! tuples = this.definedFunctions["ControlFlow"];

+      List<List<int>> tuples = this.definedFunctions["ControlFlow"];

+      Contract.Assert(tuples != null);

       foreach (List<int> tuple in tuples)

       {

         if (tuple == null) continue;

@@ -329,49 +375,63 @@ namespace Microsoft.Boogie
         if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id)

           return LookupPartitionValue(tuple[2]);

       }

-      assert false;

+      Contract.Assert(false);throw new cce.UnreachableException();

       return 0;

     }

     

-    private string! LookupSkolemConstant(string! name) {

-      foreach (string! functionName in identifierToPartition.Keys)

+    private string LookupSkolemConstant(string name) {

+      Contract.Requires(name != null);

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

+

+      foreach (string functionName in identifierToPartition.Keys)

       {

+        Contract.Assert(functionName != null);

+

         int index = functionName.LastIndexOf("!");

         if (index == -1) continue;

-        string! newFunctionName = (!)functionName.Remove(index);

+        string newFunctionName = cce.NonNull(functionName.Remove(index));

         if (newFunctionName.Equals(name))

           return functionName;

       }

       return "";

     }

-    private string! LookupSkolemFunction(string! name) {

-      foreach (string! functionName in definedFunctions.Keys)

+    private string LookupSkolemFunction(string name) {

+      Contract.Requires(name != null);

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

+

+      foreach (string functionName in definedFunctions.Keys)

       {

+        Contract.Assert(functionName != null);

         int index = functionName.LastIndexOf("!");

         if (index == -1) continue;

-        string! newFunctionName = (!)functionName.Remove(index);

+        string newFunctionName = cce.NonNull(functionName.Remove(index));

         if (newFunctionName.Equals(name))

           return functionName;

       }

       return "";

     }

-    public int LookupSkolemFunctionAt(string! functionName, List<int>! values)

+    public int LookupSkolemFunctionAt(string functionName, List<int> values)

+      

     {

-      string! actualFunctionName = LookupSkolemFunction(functionName);

+      Contract.Requires(functionName!= null);

+      Contract.Requires(values != null);

+

+      string actualFunctionName = LookupSkolemFunction(functionName);

+      Contract.Assert(actualFunctionName != null);

       if (actualFunctionName.Equals(""))

       {

         // The skolem function is actually a skolem constant

         actualFunctionName = LookupSkolemConstant(functionName);

-        assert !actualFunctionName.Equals("");

+        Contract.Assert( !actualFunctionName.Equals(""));

         return identifierToPartition[actualFunctionName];

       }

-      List<List<int>>! tuples = this.definedFunctions[actualFunctionName];

-      assert tuples.Count > 0;

+      List<List<int>> tuples = this.definedFunctions[actualFunctionName];

+      Contract.Assert( tuples.Count > 0);

       // the last tuple is a dummy tuple

       for (int n = 0; n < tuples.Count - 1; n++)

       {

-        List<int>! tuple = (!)tuples[n];

-        assert tuple.Count - 1 <= values.Count;

+        List<int> tuple = cce.NonNull(tuples[n]);

+        Contract.Assert( tuple.Count - 1 <= values.Count);

         for (int i = 0, j = 0; i < values.Count; i++)

         {

           if (values[i] == tuple[j]) {

@@ -381,33 +441,38 @@ namespace Microsoft.Boogie
           }

         }

       }

-      assert false;

+      Contract.Assert(false);throw new cce.UnreachableException();

       return 0;

     }

     

-    public List<object!>! PartitionsToValues(List<int>! args)

+    public List<object>/*!>!*/ PartitionsToValues(List<int> args)

     {

-      List<object!>! vals = new List<object!>();

+      Contract.Requires(args != null);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<object>>()));

+

+      List<object> vals = new List<object>();

       foreach(int i in args)

       {

-        object! o = (!)partitionToValue[i];

+        object o = cce.NonNull(partitionToValue[i]);

         if (o is bool) {

           vals.Add(o);

         } else if (o is BigNum) {

           vals.Add(o);

-        } else if (o is List<List<int>!>) {

-          List<List<int>!> array = (List<List<int>!>) o;

-          List<List<object!>!> arrayVal = new List<List<object!>!>();

-          foreach (List<int>! tuple in array) {

-            List<object!> tupleVal = new List<object!>();

-            foreach (int i in tuple) {

-              tupleVal.Add((!)partitionToValue[i]);

+        } else if (o is List<List<int>>) {

+          List<List<int>> array = (List<List<int>>) o;

+          List<List<object>> arrayVal = new List<List<object>>();

+          foreach (List<int> tuple in array) {

+            Contract.Assert(Contract.Result<List<int>>() != null);

+

+            List<object> tupleVal = new List<object>();

+            foreach (int j in tuple) {

+              tupleVal.Add(cce.NonNull(partitionToValue[i]));

             }

             arrayVal.Add(tupleVal);

           }

           vals.Add(arrayVal);

         } else {

-          assert false;

+          Contract.Assert(false);throw new cce.UnreachableException();

         }

       }

       return vals;

@@ -417,20 +482,22 @@ namespace Microsoft.Boogie
   public abstract class ProverInterface

   {

     public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined }

-

     public class ErrorHandler

     {

-      public virtual void OnModel(IList<string!>! labels, ErrorModel errModel)

+      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel)

       {

+        Contract.Requires(cce.NonNullElements(labels));

       }

 

-      public virtual void OnResourceExceeded(string! message)

+      public virtual void OnResourceExceeded(string message)

       {

+        Contract.Requires(message!=null);

       }

 

-      public virtual void OnProverWarning(string! message)

-          modifies Console.Out.*, Console.Error.*;

+      public virtual void OnProverWarning(string message)

+          //modifies Console.Out.*, Console.Error.*;

       {

+        Contract.Requires(message != null);

         switch (CommandLineOptions.Clo.PrintProverWarnings) {

           case CommandLineOptions.ProverWarnings.None:

             break;

@@ -441,25 +508,25 @@ namespace Microsoft.Boogie
             Console.Error.WriteLine("Prover warning: " + message);

             break;

           default:

-            assume false;  // unexpected case

+             Contract.Assume( false);throw new cce.UnreachableException();  // unexpected case

         }

       }

 

 

-      public virtual Absy! Label2Absy(string! label)

+      public virtual Absy Label2Absy(string label)

       {

+        Contract.Requires(label != null);

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

+

         throw new System.NotImplementedException();

       }

     }

-  

-    public abstract void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler);

+    public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);

     [NoDefaultContract]

-    public abstract Outcome CheckOutcome(ErrorHandler! handler);

-      throws UnexpectedProverOutputException;

-

-    public virtual void LogComment(string! comment) {

+    public abstract Outcome CheckOutcome(ErrorHandler handler);

+    public virtual void LogComment(string comment) {

+      Contract.Requires(comment != null);

     }

-

     public virtual void Close() {

     }

     

@@ -468,21 +535,39 @@ namespace Microsoft.Boogie
     /// for now it is only implemented by ProcessTheoremProver and still requires some

     /// testing

     /// </summary>    

-    public virtual void PushVCExpression(VCExpr! vc) {}

-    public virtual string! VCExpressionToString(VCExpr! vc) { return ""; }

-    public virtual void Pop() 

-      throws UnexpectedProverOutputException;

-    {}

+    public virtual void PushVCExpression(VCExpr vc) {Contract.Requires(vc != null);}

+    public virtual string VCExpressionToString(VCExpr vc) {Contract.Requires(vc != null);Contract.Ensures(Contract.Result<string>() != null); return ""; }

+    public virtual void Pop()

+    {Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);}

     public virtual int NumAxiomsPushed() 

     { return 0; }

     public virtual int FlushAxiomsToTheoremProver() 

-      throws UnexpectedProverOutputException;

-    { return 0; }

+    { Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);return 0; }

     

         

-    public abstract ProverContext! Context { get; }

-    public abstract VCExpressionGenerator! VCExprGen { get; }

+    public abstract ProverContext Context { get; }

+public abstract VCExpressionGenerator VCExprGen { get; }

   }

+  public class ProverInterfaceContracts:ProverInterface{//TODO Contracts class

+    public override ProverContext Context {

+      get {

+        throw new NotImplementedException();

+      }

+    }

+    public override VCExpressionGenerator VCExprGen {

+      get {

+        throw new NotImplementedException();

+      }

+    }

+    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){Contract.Requires(descriptiveName != null); Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();}

+    [NoDefaultContract]

+    public override Outcome CheckOutcome(ErrorHandler handler){

+    Contract.Requires(handler != null);

+      Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

+    throw new NotImplementedException();}

+  }

+

+    

 

   public class ProverException : Exception 

   {

@@ -490,7 +575,7 @@ namespace Microsoft.Boogie
     {            

     }

   }

-  public class UnexpectedProverOutputException : ProverException, ICheckedException

+  public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException

   {

     public UnexpectedProverOutputException(string s) : base(s)

     {