Boogie: I have successfully ported the AbsInt project. It passes all regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL.

Address any error complaints to t-abarbe@microsoft.com

1 files changed, 109 insertions, 119 deletions

diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index 694811da..2890730b 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -3,12 +3,12 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

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

-namespace Microsoft.Boogie

-{

+namespace Microsoft.Boogie {

   using System;

   using System.Collections.Generic;

-  using Microsoft.Contracts;

+  using System.Diagnostics.Contracts;

 

+  

   /// <summary>

   /// This class provides the functionality of traversing a program to determine which

   /// blocks are blocks where the widening operator may need to be applied.  Assumes

@@ -16,95 +16,82 @@ namespace Microsoft.Boogie
   /// the end.  Assumes the 'widenBlock' bits are initially false, and sets them

   /// appropriately.

   /// </summary>

-  public class WidenPoints 

-  {

+  public class WidenPoints {

     /// <summary>

     /// Compute the widen points of a program

     /// </summary>

-    public static void Compute(Program! program) 

-    {

-      expose (program)

-      {

-        foreach (Declaration m in program.TopLevelDeclarations) 

-        {

-          Implementation impl = m as Implementation;

-          if (impl != null) 

-          {

-            if (impl.Blocks != null && impl.Blocks.Count > 0) 

-            {

-              assume impl.IsConsistent;

-              expose (impl) {

-                Block start = impl.Blocks[0];

-                assume start != null;

-                assume start.IsConsistent;

-                Visit(start);

-          

-                // We reset the state...

-                foreach(Block b in impl.Blocks) {

-                  expose (b) {

-                    b.TraversingStatus = Block.VisitState.ToVisit;

-                  }

-                }

-              }

+    public static void Compute(Program program) {

+      Contract.Requires(program != null);

+      cce.BeginExpose(program);

+

+      foreach (Declaration m in program.TopLevelDeclarations) {

+        Implementation impl = m as Implementation;

+        if (impl != null) {

+          if (impl.Blocks != null && impl.Blocks.Count > 0) {

+            Contract.Assume(cce.IsConsistent(impl));

+            cce.BeginExpose(impl);

+            Block start = impl.Blocks[0];

+            Contract.Assume(start != null);

+            Contract.Assume(cce.IsConsistent(start));

+            Visit(start);

+

+            // We reset the state...

+            foreach (Block b in impl.Blocks) {

+              cce.BeginExpose(b);

+              b.TraversingStatus = Block.VisitState.ToVisit;

+              cce.EndExpose();

             }

+            cce.EndExpose();

           }

         }

       }

+      cce.EndExpose();

     }

 

-    static void Visit(Block! b) 

-    {

-      assume b.IsExposable;

-      if (b.TraversingStatus == Block.VisitState.BeingVisited) 

-      {

-        expose (b)

-        {

-          // we got here through a back-edge

-          b.widenBlock = true;

-        }

-      } 

-      else if(b.TraversingStatus == Block.VisitState.AlreadyVisited)

-      {

+    static void Visit(Block b) {

+      Contract.Requires(b != null);

+      Contract.Assume(cce.IsExposable(b));

+      if (b.TraversingStatus == Block.VisitState.BeingVisited) {

+        cce.BeginExpose(b);

+        // we got here through a back-edge

+        b.widenBlock = true;

+        cce.EndExpose();

+      } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {

         // do nothing... we already saw this node

-      }

-      else if (b.TransferCmd is GotoCmd) 

-      {

-        assert b.TraversingStatus == Block.VisitState.ToVisit;    

-    

+      } else if (b.TransferCmd is GotoCmd) {

+        Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

+

         GotoCmd g = (GotoCmd)b.TransferCmd;

-        expose (b)

-        {

-          expose (g) {  //PM: required for the subsequent expose (g.labelTargets)

-            b.TraversingStatus = Block.VisitState.BeingVisited;

-           

-            // labelTargets is made non-null by Resolve, which we assume

-            // has already called in a prior pass.

-            assume g.labelTargets != null;

-            expose (g.labelTargets) {

-              foreach (Block succ in g.labelTargets) 

-//              invariant b.currentlyTraversed; 

-                //PM: The following loop invariant will work once properties are axiomatized

-                //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

+        cce.BeginExpose(b);

+

+        cce.BeginExpose(g);   //PM: required for the subsequent expose (g.labelTargets)

+        b.TraversingStatus = Block.VisitState.BeingVisited;

+

+        // labelTargets is made non-null by Resolve, which we assume

+        // has already called in a prior pass.

+        Contract.Assume(g.labelTargets != null);

+        cce.BeginExpose(g.labelTargets);

+        foreach (Block succ in g.labelTargets)

+        //              invariant b.currentlyTraversed; 

+        //PM: The following loop invariant will work once properties are axiomatized

+        //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

               {

-                assert succ != null;

-                Visit(succ);

-              }

-            }

+          Contract.Assert(succ != null);

+          Visit(succ);

+        }

+        cce.EndExpose();

 

-            assert b.TraversingStatus == Block.VisitState.BeingVisited;

-//            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

+        Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);

+        //            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

 

-            b.TraversingStatus = Block.VisitState.AlreadyVisited;

+        b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

-            //PM: The folowing assumption is needed because we cannot prove that a simple field update

-            //PM: leaves the value of a property unchanged.

-            assume (g.labelNames != null ==> g.labelNames.Length == g.labelTargets.Length);

-          }

-        }

-      }

-      else 

-      {

-        assert b.TransferCmd == null || b.TransferCmd is ReturnCmd;        // It must be a returnCmd;

+        //PM: The folowing assumption is needed because we cannot prove that a simple field update

+        //PM: leaves the value of a property unchanged.

+        Contract.Assume(g.labelNames == null || g.labelNames.Length == g.labelTargets.Length);

+        cce.EndExpose();

+      } else {

+        Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd);        // It must be a returnCmd;

       }

     }

 

@@ -115,21 +102,23 @@ namespace Microsoft.Boogie
     /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>

     /// <return> The blocks that are in the loop from block </return>

     /// </summary>

-    public static List<Block!> ComputeLoopBodyFrom(Block! block)

-      requires block.widenBlock;

-    {

-      assert rootBlock == null;

+    public static List<Block> ComputeLoopBodyFrom(Block block) {

+      Contract.Requires(block.widenBlock);

+      Contract.Requires(block != null);

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

+

+      Contract.Assert(rootBlock == null);

       rootBlock = block;

 

-      List<Block!> blocksInLoop = new List<Block!>();         // We use a list just because .net does not define a set      

-      List<Block!> visitingPath = new List<Block!>();         // The order is important, as we want paths

-             

-      blocksInLoop.Add(block);      

-              

+      List<Block/*!*/> blocksInLoop = new List<Block/*!*/>();         // We use a list just because .net does not define a set

+      List<Block/*!*/> visitingPath = new List<Block/*!*/>();         // The order is important, as we want paths

+

+      blocksInLoop.Add(block);

+

       DoDFSVisit(block, visitingPath, blocksInLoop);

-      

+

       visitingPath.Add(block);

-      

+

 

       rootBlock = null;   // We reset the invariant

 

@@ -141,42 +130,43 @@ namespace Microsoft.Boogie
     /// <param name = "block"> The block to visit </param>

     /// <param name = "path"> The path we are visiting so far </param>

     /// </summary>

-    private static void DoDFSVisit(Block! block, List<Block!>! path, List<Block!>! blocksInPath)

-    {

-        #region case 1. We visit the root => We are done, "path" is a path inside the loop

-        if(block == rootBlock && path.Count > 1)

-        {

-          blocksInPath.AddRange(path);      // Add all the blocks in this path 

-        }

+    private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath) {

+      Contract.Requires(block != null);

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

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

+      #region case 1. We visit the root => We are done, "path" is a path inside the loop

+      if (block == rootBlock && path.Count > 1) {

+        blocksInPath.AddRange(path);      // Add all the blocks in this path 

+      }

 

-        #endregion

-        #region case 2. We visit a node that ends with a return => "path" is not inside the loop

-        if(block.TransferCmd is ReturnCmd)

-        {

-          return;

-        }

-        #endregion

-        #region case 3. We visit a node with successors => continue the exploration of its successors

-        {

-          assert block.TransferCmd is GotoCmd;

-          GotoCmd! successors = (GotoCmd) block.TransferCmd;

-          

-          if (successors.labelTargets != null)

-          foreach (Block! nextBlock in successors.labelTargets)

-          {

-            if(path.Contains(nextBlock))      // If the current path has already seen the block, just skip it 

+      #endregion

+      #region case 2. We visit a node that ends with a return => "path" is not inside the loop

+      if (block.TransferCmd is ReturnCmd) {

+        return;

+      }

+      #endregion

+      #region case 3. We visit a node with successors => continue the exploration of its successors

+      {

+        Contract.Assert(block.TransferCmd is GotoCmd);

+        GotoCmd successors = (GotoCmd)block.TransferCmd;

+        Contract.Assert(successors != null);

+

+        if (successors.labelTargets != null)

+          foreach (Block nextBlock in successors.labelTargets) {

+            Contract.Assert(nextBlock != null);

+            if (path.Contains(nextBlock))      // If the current path has already seen the block, just skip it 

               continue;

-                                              // Otherwise we perform the DFS visit

+            // Otherwise we perform the DFS visit

             path.Add(nextBlock);

             DoDFSVisit(nextBlock, path, blocksInPath);

-            

-            assert nextBlock == path[path.Count-1];

-            path.RemoveAt(path.Count-1);

+

+            Contract.Assert(nextBlock == path[path.Count - 1]);

+            path.RemoveAt(path.Count - 1);

           }

 

-        }

+      }

 

-        #endregion

-    }      

- }   

+      #endregion

+    }

+  }

 }