Merge

6 files changed, 57 insertions, 38 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 1367a08d..c6b66585 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -502,8 +502,13 @@ namespace Microsoft.Boogie {
           CmdSeq ssBody = new CmdSeq();

           CmdSeq ssDone = new CmdSeq();

           if (wcmd.Guard != null) {

-            ssBody.Add(new AssumeCmd(wcmd.tok, wcmd.Guard));

-            ssDone.Add(new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)));

+            var ac = new AssumeCmd(wcmd.tok, wcmd.Guard);

+            ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);

+            ssBody.Add(ac);

+

+            ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard));

+            ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);

+            ssDone.Add(ac);

           }

 

           // Try to squeeze in ssBody into the first block of wcmd.Body

@@ -556,8 +561,13 @@ namespace Microsoft.Boogie {
             CmdSeq ssThen = new CmdSeq();

             CmdSeq ssElse = new CmdSeq();

             if (ifcmd.Guard != null) {

-              ssThen.Add(new AssumeCmd(ifcmd.tok, ifcmd.Guard));

-              ssElse.Add(new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)));

+              var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard);

+              ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);

+              ssThen.Add(ac);

+

+              ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));

+              ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);

+              ssElse.Add(ac);

             }

 

             // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock

@@ -597,7 +607,9 @@ namespace Microsoft.Boogie {
               predLabel = elseLabel;

               predCmds = new CmdSeq();

               if (ifcmd.Guard != null) {

-                predCmds.Add(new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)));

+                var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));

+                ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);

+                predCmds.Add(ac);

               }

 

             } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 118e540f..17f35b1e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4719,7 +4719,6 @@ namespace Microsoft.Dafny
       //  - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)

       //       (if two imported types have the same name, an error message is produced here)

       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

-      //  - imported module name

       //  - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

       //  - static function or method in the enclosing module, or its imports.

 

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index e728c56d..5c746f7e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -2041,7 +2041,7 @@ namespace GPUVerify
             {

                 if (CommandLineOptions.SmartPredication)

                 {

-                    SmartBlockPredicator.Predicate(Program, /*createCandidateInvariants=*/CommandLineOptions.Inference);

+                    SmartBlockPredicator.Predicate(Program);

                 }

                 else

                 {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index ab2fa74f..526302db 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -485,14 +485,18 @@ namespace Microsoft.Boogie.Houdini {
 

     public bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) {

       candidateConstant = null;

-      IExpr antecedent;

+      IExpr antecedent, consequent;

       IExpr expr = boogieExpr as IExpr;

-      if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {

+      if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent, out consequent)) {

         IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

         if (constantFunApp != null && houdiniConstants.Contains(constantFunApp.IdentifierExpr.Decl)) {

           candidateConstant = constantFunApp.IdentifierExpr.Decl;

           return true;

         }

+

+        var e = consequent as Expr;

+        if (e != null && MatchCandidate(e, out candidateConstant))

+          return true;

       }

       return false;

     }

diff --git a/Source/VCGeneration/SmartBlockPredicator.cs b/Source/VCGeneration/SmartBlockPredicator.cs
index 15f19ce5..f769822c 100644
--- a/Source/VCGeneration/SmartBlockPredicator.cs
+++ b/Source/VCGeneration/SmartBlockPredicator.cs
@@ -14,11 +14,11 @@ public class SmartBlockPredicator {
   Graph<Block> blockGraph;

   List<Tuple<Block, bool>> sortedBlocks;

 

-  bool createCandidateInvariants = true;

   bool useProcedurePredicates = true;

 

   Dictionary<Block, Variable> predMap, defMap;

   Dictionary<Block, HashSet<Variable>> ownedMap;

+  Dictionary<Block, Block> parentMap;

   Dictionary<Block, PartInfo> partInfo;

 

   IdentifierExpr fp;

@@ -27,10 +27,9 @@ public class SmartBlockPredicator {
   Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();

   HashSet<Block> doneBlocks = new HashSet<Block>();

 

-  SmartBlockPredicator(Program p, Implementation i, bool cci, bool upp) {

+  SmartBlockPredicator(Program p, Implementation i, bool upp) {

     prog = p;

     impl = i;

-    createCandidateInvariants = cci;

     useProcedurePredicates = upp;

   }

 

@@ -186,10 +185,7 @@ public class SmartBlockPredicator {
                         DomRelation<Block> pdom,

                         IEnumerator<Tuple<Block, bool>> i,

                         Variable headPredicate,

-                        ref int predCount,

-                        Dictionary<Block, Variable> predMap,

-                        Dictionary<Block, Variable> defMap,

-                        Dictionary<Block, HashSet<Variable>> ownedMap) {

+                        ref int predCount) {

     var header = i.Current.Item1;

     var regionPreds = new List<Tuple<Block, Variable>>();

     var ownedPreds = new HashSet<Variable>();

@@ -198,20 +194,18 @@ public class SmartBlockPredicator {
     predMap[header] = headPredicate;

     defMap[header] = headPredicate;

     regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));

-    if (!i.MoveNext())

-      return;

 

-    do {

+    while (i.MoveNext()) {

       var block = i.Current;

       if (block.Item2) {

         if (block.Item1 == header)

           return;

       } else {

         if (blockGraph.Headers.Contains(block.Item1)) {

+          parentMap[block.Item1] = header;

           var loopPred = FreshPredicate(ref predCount);

           ownedPreds.Add(loopPred);

-          AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount,

-                           predMap, defMap, ownedMap);

+          AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);

         } else {

           bool foundExisting = false;

           foreach (var regionPred in regionPreds) {

@@ -231,12 +225,10 @@ public class SmartBlockPredicator {
           }

         }

       }

-    } while (i.MoveNext());

+    }

   }

 

-  void AssignPredicates(out Dictionary<Block, Variable> predMap,

-                        out Dictionary<Block, Variable> defMap,

-                        out Dictionary<Block, HashSet<Variable>> ownedMap) {

+  void AssignPredicates() {

     DomRelation<Block> dom = blockGraph.DominatorMap;

 

     Graph<Block> dualGraph = blockGraph.Dual(new Block());

@@ -253,9 +245,10 @@ public class SmartBlockPredicator {
     predMap = new Dictionary<Block, Variable>();

     defMap = new Dictionary<Block, Variable>();

     ownedMap = new Dictionary<Block, HashSet<Variable>>();

+    parentMap = new Dictionary<Block, Block>();

     AssignPredicates(blockGraph, dom, pdom, iter,

                      useProcedurePredicates ? impl.InParams[0] : null,

-                     ref predCount, predMap, defMap, ownedMap);

+                     ref predCount);

   }

 

   IEnumerable<Block> LoopsExited(Block src, Block dest) {

@@ -339,7 +332,7 @@ public class SmartBlockPredicator {
     blockGraph = prog.ProcessLoops(impl);

     sortedBlocks = blockGraph.LoopyTopSort();

 

-    AssignPredicates(out predMap, out defMap, out ownedMap);

+    AssignPredicates();

     partInfo = BuildPartitionInfo();

 

     if (useProcedurePredicates)

@@ -381,6 +374,17 @@ public class SmartBlockPredicator {
           prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

                                               new BlockSeq(runBlock));

 

+        if (parentMap.ContainsKey(runBlock)) {

+          var parent = parentMap[runBlock];

+          if (predMap.ContainsKey(parent)) {

+            var parentPred = predMap[parent];

+            if (parentPred != null) {

+              runBlock.Cmds.Add(new AssertCmd(Token.NoToken,

+                                              Expr.Imp(pExpr, Expr.Ident(parentPred))));

+            }

+          }

+        }

+

         var transferCmd = runBlock.TransferCmd;

         foreach (Cmd cmd in oldCmdSeq)

           PredicateCmd(pExpr, newBlocks, runBlock, cmd, out runBlock);

@@ -413,7 +417,6 @@ public class SmartBlockPredicator {
   }

 

   public static void Predicate(Program p,

-                               bool createCandidateInvariants = true,

                                bool useProcedurePredicates = true) {

     foreach (var decl in p.TopLevelDeclarations.ToList()) {

       if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {

@@ -448,7 +451,7 @@ public class SmartBlockPredicator {
       try {

         var impl = decl as Implementation;

         if (impl != null)

-          new SmartBlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();

+          new SmartBlockPredicator(p, impl, useProcedurePredicates).PredicateImplementation();

       }

       catch (Program.IrreducibleLoopException) { }

     }

@@ -456,7 +459,7 @@ public class SmartBlockPredicator {
 

   public static void Predicate(Program p, Implementation impl) {

     try {

-      new SmartBlockPredicator(p, impl, false, false).PredicateImplementation();

+      new SmartBlockPredicator(p, impl, false).PredicateImplementation();

     }

     catch (Program.IrreducibleLoopException) { }

   }

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 1613a4aa..b78aada0 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,15 +1,15 @@
-# Aste started: 2012-07-10 07:00:02

+# Aste started: 2012-08-04 07:00:02

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2012-07-10 07:01:07] SpecSharp revision: d78c1f490bc8

-# [2012-07-10 07:01:07] SscBoogie revision: d78c1f490bc8

-# [2012-07-10 07:02:08] Boogie revision: 2a3fa56ccdb4

-[2012-07-10 07:03:28] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2012-08-04 07:02:57] SpecSharp revision: 16a7afdeb53f

+# [2012-08-04 07:02:57] SscBoogie revision: 16a7afdeb53f

+# [2012-08-04 07:05:08] Boogie revision: f0c8bc16dff7

+[2012-08-04 07:06:37] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


-[2012-07-10 07:04:57] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+[2012-08-04 07:08:06] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -41,5 +41,6 @@
     warning CS0162: Unreachable code detected


     warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


-[2012-07-10 07:57:25] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2012-07-10 07:58:07] Released nightly of Boogie

+[2012-08-04 08:01:24] 3 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+['inline', 'test15', 'smoke']

+# [2012-08-04 08:02:07] Released nightly of Boogie