Boogie: Committing new source code for VCExpr

1 files changed, 68 insertions, 43 deletions

diff --git a/Source/VCExpr/LetBindingSorter.cs b/Source/VCExpr/LetBindingSorter.cs
index 96eb0af2..97d71e27 100644
--- a/Source/VCExpr/LetBindingSorter.cs
+++ b/Source/VCExpr/LetBindingSorter.cs
@@ -8,124 +8,149 @@ using System.Text;
 using System.IO;

 using System.Collections;

 using System.Collections.Generic;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 

 // Sort the bindings in a let-expression so that terms bound earlier do

 // not contain variables bound later

 

-namespace Microsoft.Boogie.VCExprAST

-{

+namespace Microsoft.Boogie.VCExprAST {

 

   // (argument is not used)

   public class LetBindingSorter : MutatingVCExprVisitor<bool> {

 

-    private readonly FreeVariableCollector! FreeVarCollector =

-      new FreeVariableCollector ();

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(FreeVarCollector != null);

+    }

+

+    private readonly FreeVariableCollector/*!*/ FreeVarCollector =

+      new FreeVariableCollector();

 

-    private List<VCExprVar!>! FreeVarsIn(VCExpr! expr) {

+    private List<VCExprVar/*!*/>/*!*/ FreeVarsIn(VCExpr expr) {

+      Contract.Requires(expr != null);

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

       FreeVarCollector.Collect(expr);

-      List<VCExprVar!>! freeVars = new List<VCExprVar!> (FreeVarCollector.FreeTermVars.Keys);

+      List<VCExprVar/*!*/>/*!*/ freeVars = new List<VCExprVar/*!*/>(FreeVarCollector.FreeTermVars.Keys);

       FreeVarCollector.Reset();

       return freeVars;

     }

 

-    public LetBindingSorter(VCExpressionGenerator! gen) {

-      base(gen);

+    public LetBindingSorter(VCExpressionGenerator gen):base(gen) {

+      Contract.Requires(gen != null);

+

     }

 

-    public override VCExpr! Visit(VCExprLet! node, bool arg) {

-      IDictionary<VCExprVar!, Binding!> boundVars =

-        new Dictionary<VCExprVar!, Binding!> ();

+    public override VCExpr Visit(VCExprLet node, bool arg){

+Contract.Requires(node != null);

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

+      IDictionary<VCExprVar/*!*/, Binding/*!*/> boundVars =

+        new Dictionary<VCExprVar/*!*/, Binding/*!*/> ();

 

       // recurse and collect the free variables in bound terms and formulae

-      foreach (VCExprLetBinding! binding in node) {

-        VCExpr! newE = Mutate(binding.E, arg);

-        Binding! b = new Binding (binding.V, newE, FreeVarsIn(newE));

+      foreach (VCExprLetBinding/*!*/ binding in node) {Contract.Assert(binding != null);

+        VCExpr/*!*/ newE = Mutate(binding.E, arg);

+        Binding/*!*/ b = new Binding (binding.V, newE, FreeVarsIn(newE));

         boundVars.Add(b.V, b);

       }

 

       // generate the occurrence edges

-      foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars) {

-        Binding! b = pair.Value;

-        foreach (VCExprVar! v in b.FreeVars) {

+      foreach (KeyValuePair<VCExprVar/*!*/, Binding/*!*/> pair in boundVars) {Contract.Assert(cce.NonNullElements(pair));

+        Binding/*!*/ b = pair.Value;

+        Contract.Assert(b != null);

+        foreach (VCExprVar/*!*/ v in b.FreeVars) {Contract.Assert(v != null);

           Binding b2;

           if (boundVars.TryGetValue(v, out b2)) {

-            ((!)b2).Occurrences.Add(b);

+            cce.NonNull(b2).Occurrences.Add(b);

             b.InvOccurrencesNum = b.InvOccurrencesNum + 1;

           }

         }

       }

 

       // topological sort

-      Stack<Binding!> rootBindings = new Stack<Binding!> ();

-      foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars)

+      Stack<Binding/*!*/> rootBindings = new Stack<Binding/*!*/> ();

+      foreach (KeyValuePair<VCExprVar/*!*/, Binding/*!*/> pair in boundVars)

+      {Contract.Assert(cce.NonNullElements(pair));

         if (pair.Value.InvOccurrencesNum == 0)

-          rootBindings.Push(pair.Value);

+          rootBindings.Push(pair.Value);}

 

-      List<Binding!>! sortedBindings = new List<Binding!> ();

+      List<Binding/*!*/>/*!*/ sortedBindings = new List<Binding/*!*/> ();

       while (rootBindings.Count > 0) {

-        Binding! b = rootBindings.Pop();

+        Binding/*!*/ b = rootBindings.Pop();

+        Contract.Assert(b != null);

         sortedBindings.Add(b);

-        foreach (Binding! b2 in b.Occurrences) {

+        foreach (Binding/*!*/ b2 in b.Occurrences) {

+          Contract.Assert(b2 != null);

           b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1;

           if (b2.InvOccurrencesNum == 0)

             rootBindings.Push(b2);

         }

       }

 

-      if (exists{KeyValuePair<VCExprVar!, Binding!> pair in boundVars;

-                 pair.Value.InvOccurrencesNum > 0})

+      if (Contract.Exists(boundVars, pair=> pair.Value.InvOccurrencesNum > 0))

         System.Diagnostics.Debug.Fail("Cyclic let-bindings");

 

-      assert node.Length == sortedBindings.Count;

+      Contract.Assert(node.Length == sortedBindings.Count);

 

       // check which of the bindings can be dropped

-      VCExpr! newBody = Mutate(node.Body, arg);

+      VCExpr newBody = Mutate(node.Body, arg);

+      Contract.Assert(newBody != null);

 

-      IDictionary<VCExprVar!, VCExprVar!>! usedVars =

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

-      foreach (VCExprVar! v in FreeVarsIn(newBody))

+      IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ usedVars =

+        new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/> ();

+      foreach (VCExprVar/*!*/ v in FreeVarsIn(newBody)){Contract.Assert(v != null);

         if (!usedVars.ContainsKey(v))

-          usedVars.Add(v, v);

+          usedVars.Add(v, v);}

 

       for (int i = sortedBindings.Count - 1; i >= 0; --i) {

         if (usedVars.ContainsKey(sortedBindings[i].V)) {

-          foreach (VCExprVar! v in sortedBindings[i].FreeVars)

+          foreach (VCExprVar/*!*/ v in sortedBindings[i].FreeVars){

+            Contract.Assert(v != null);

             if (!usedVars.ContainsKey(v))

-              usedVars.Add(v, v);

+              usedVars.Add(v, v);}

         } else {

           sortedBindings.RemoveAt(i);

         }

       }

 

       // assemble the resulting let-expression

-      List<VCExprLetBinding!>! newBindings = new List<VCExprLetBinding!> ();

+      List<VCExprLetBinding/*!*/>/*!*/ newBindings = new List<VCExprLetBinding/*!*/>();

       foreach (Binding b in sortedBindings)

         newBindings.Add(Gen.LetBinding(b.V, b.E));

 

       return Gen.Let(newBindings, newBody);

-    }    

+    }

 

     private class Binding {

-      public readonly VCExprVar! V;

-      public readonly VCExpr! E;

-      public readonly List<VCExprVar!>! FreeVars;

+      public readonly VCExprVar/*!*/ V;

+      public readonly VCExpr/*!*/ E;

+      public readonly List<VCExprVar/*!*/>/*!*/ FreeVars;

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(V != null);

+        Contract.Invariant(E != null);

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

+        Contract.Invariant(Occurrences != null);

+      }

+

 

       // list of all bound expression in which the variable V occurs

       // (outgoing edges)

-      public readonly List<Binding>! Occurrences;

+      public readonly List<Binding>/*!*/ Occurrences;

 

       // number of variables that are bound in this let-expression

       // and that occur in FreeVars

       // (incoming edges)

       public int InvOccurrencesNum;

 

-      public Binding(VCExprVar! v, VCExpr! e, List<VCExprVar!>! freeVars) {

+      public Binding(VCExprVar v, VCExpr e, List<VCExprVar/*!*/>/*!*/ freeVars) {

+        Contract.Requires(e != null);

+        Contract.Requires(v != null);

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

         this.V = v;

         this.E = e;

         this.FreeVars = freeVars;

-        this.Occurrences = new List<Binding> ();

+        this.Occurrences = new List<Binding>();

         this.InvOccurrencesNum = 0;

       }

     }