more bug fixes

updates to DeviceCache.bpl to make it verify

5 files changed, 142 insertions, 55 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 8869c447..05fac855 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -14,49 +14,85 @@ namespace Microsoft.Boogie
     {

         MoverTypeChecker moverTypeChecker;

         int phaseNum;

+        int enclosingProcPhaseNum;

         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

         public Dictionary<Absy, Absy> absyMap; /* Original -> Duplicate */

         public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)

         {

             this.moverTypeChecker = moverTypeChecker;

             this.phaseNum = phaseNum;

+            this.enclosingProcPhaseNum = int.MaxValue;

             this.procMap = new Dictionary<Procedure, Procedure>();

             this.absyMap = new Dictionary<Absy, Absy>();

         }

 

+        private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)

+        {

+            Procedure originalProc = originalCallCmd.Proc;

+            if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc) && moverTypeChecker.procToActionInfo[originalProc].phaseNum < phaseNum)

+            {

+                List<AssertCmd> gate = moverTypeChecker.procToActionInfo[originalProc].thisGate;

+                Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

+                for (int i = 0; i < originalProc.InParams.Count; i++)

+                {

+                    map[originalProc.InParams[i]] = callCmd.Ins[i];

+                }

+

+                Substitution subst = Substituter.SubstitutionFromHashtable(map);

+                foreach (AssertCmd assertCmd in gate)

+                {

+                    newCmds.Add(Substituter.Apply(subst, assertCmd));

+                }

+            }

+            newCmds.Add(callCmd);

+        }

+

+        private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)

+        {

+            int maxCalleePhaseNum = 0;

+            foreach (CallCmd iter in originalParCallCmd.CallCmds)

+            {

+                int calleePhaseNum = moverTypeChecker.FindPhaseNumber(iter.Proc);

+                if (calleePhaseNum > maxCalleePhaseNum)

+                    maxCalleePhaseNum = calleePhaseNum;

+            }

+            if (phaseNum > maxCalleePhaseNum)

+            {

+                for (int i = 0; i < parCallCmd.CallCmds.Count; i++) 

+                {

+                    ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds);

+                }

+            }

+            else

+            {

+                newCmds.Add(parCallCmd);

+            }

+        }

+

         public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)

         {

             List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);

             List<Cmd> newCmds = new List<Cmd>();

-            for (int i = 0; i < cmds.Count; i++) 

+            for (int i = 0; i < cmds.Count; i++)

             {

-                Cmd cmd = cmds[i];

-                ParCallCmd parCallCmd = cmd as ParCallCmd;

                 Cmd originalCmd = cmdSeq[i];

-                ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;

-                if (originalParCallCmd == null)

+                Cmd cmd = cmds[i];

+

+                CallCmd originalCallCmd = originalCmd as CallCmd;

+                if (originalCallCmd != null)

                 {

-                    newCmds.Add(cmd);

+                    ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds);

                     continue;

                 }

-                int maxCalleePhaseNum = 0;

-                foreach (CallCmd iter in originalParCallCmd.CallCmds)

-                {

-                    int calleePhaseNum = moverTypeChecker.FindPhaseNumber(iter.Proc);

-                    if (calleePhaseNum > maxCalleePhaseNum)

-                        maxCalleePhaseNum = calleePhaseNum;

-                }

-                if (phaseNum > maxCalleePhaseNum)

-                {

-                    foreach (CallCmd callCmd in parCallCmd.CallCmds)

-                    {

-                        newCmds.Add(callCmd);

-                    }

-                }

-                else

+

+                ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;

+                if (originalParCallCmd != null)

                 {

-                    newCmds.Add(parCallCmd);

+                    ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds);

+                    continue;

                 }

+             

+                newCmds.Add(cmd);

             }

             return newCmds;

         }

@@ -116,9 +152,9 @@ namespace Microsoft.Boogie
             }

             return procMap[node];

         }

-

         public override Implementation VisitImplementation(Implementation node)

         {

+            enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc);

             Implementation impl = base.VisitImplementation(node);

             impl.Name = impl.Proc.Name;

             foreach (Block block in impl.Blocks)

@@ -144,7 +180,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);

             if (node.Free)

                 return requires;

-            if (QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue) != phaseNum)

+            if (!OwickiGries.FindPhaseNums(requires.Attributes).Contains(phaseNum))

                 requires.Condition = Expr.True;

             return requires;

         }

@@ -154,7 +190,7 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);

             if (node.Free)

                 return ensures;

-            if (ensures.IsAtomicSpecification || QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue) != phaseNum)

+            if (ensures.IsAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))

             {

                 ensures.Condition = Expr.True;

                 ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

@@ -165,7 +201,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);

-            if (QKeyValue.FindIntAttribute(assertCmd.Attributes, "phase", int.MaxValue) != phaseNum)

+            if (!OwickiGries.FindPhaseNums(assertCmd.Attributes).Contains(phaseNum))

                 assertCmd.Expr = Expr.True;

             return assertCmd;

         }

@@ -861,7 +897,17 @@ namespace Microsoft.Boogie
             decls.Add(yieldImpl);

         }

 

-        private static QKeyValue RemoveYieldsAttribute(QKeyValue iter)

+        public static HashSet<int> FindPhaseNums(QKeyValue kv)

+        {

+            HashSet<int> attrs = QKeyValue.FindIntAttributes(kv, "phase");

+            if (attrs.Count == 0)

+            {

+                attrs.Add(int.MaxValue);

+            }

+            return attrs;

+        }

+

+        public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

             iter.Next = RemoveYieldsAttribute(iter.Next);

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 254f058d..8c738727 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -286,31 +286,37 @@ namespace Microsoft.Boogie
                 inAtomicSpecification = false;

                 return ret;

             }

-            int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue);

-            assertionPhaseNums.Add(phaseNum);

-            if (phaseNum > enclosingProcPhaseNum)

+            foreach (int phaseNum in OwickiGries.FindPhaseNums(ensures.Attributes))

             {

-                Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");

+                assertionPhaseNums.Add(phaseNum);

+                if (phaseNum > enclosingProcPhaseNum)

+                {

+                    Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");

+                }

             }

             return ensures;

         }

         public override Requires VisitRequires(Requires requires)

         {

-            int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue);

-            assertionPhaseNums.Add(phaseNum); 

-            if (phaseNum > enclosingProcPhaseNum)

+            foreach (int phaseNum in OwickiGries.FindPhaseNums(requires.Attributes))

             {

-                Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");

+                assertionPhaseNums.Add(phaseNum);

+                if (phaseNum > enclosingProcPhaseNum)

+                {

+                    Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");

+                }

             }

             return requires;

         }

         public override Cmd VisitAssertCmd(AssertCmd node)

         {

-            int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", int.MaxValue);

-            assertionPhaseNums.Add(phaseNum); 

-            if (phaseNum > enclosingProcPhaseNum)

+            foreach (int phaseNum in OwickiGries.FindPhaseNums(node.Attributes))

             {

-                Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");

+                assertionPhaseNums.Add(phaseNum);

+                if (phaseNum > enclosingProcPhaseNum)

+                {

+                    Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");

+                }

             }

             return node;

         }

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 460e786a..06d72ee9 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -315,6 +315,37 @@ namespace Microsoft.Boogie {
       return defl;

     }

 

+    public static HashSet<Expr> FindExprAttributes(QKeyValue kv, string name)

+    {

+        Contract.Requires(name != null);

+        HashSet<Expr> attrs = new HashSet<Expr>();

+        for (; kv != null; kv = kv.Next)

+        {

+            if (kv.Key == name)

+            {

+                if (kv.Params.Count == 1 && kv.Params[0] is Expr)

+                {

+                    attrs.Add((Expr)kv.Params[0]);

+                }

+            }

+        }

+        return attrs;

+    }

+

+    public static HashSet<int> FindIntAttributes(QKeyValue kv, string name)

+    {

+        Contract.Requires(name != null);

+        HashSet<int> attrs = new HashSet<int>();

+        HashSet<Expr> es = FindExprAttributes(kv, name);

+        foreach (Expr e in es)

+        {

+            LiteralExpr l = e as LiteralExpr;

+            if (l != null && l.isBigNum)

+                attrs.Add(l.asBigNum.ToIntSafe);

+        }

+        return attrs;

+    }

+

     public override Absy Clone() {

       List<object> newParams = new List<object>();

       foreach (object o in Params)

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index c2c04410..18e97ef4 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -12,11 +12,12 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure {:stable} {:yields} YieldToReadCache()

-requires {:phase 1} Inv(ghostLock, currsize, newsize);

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

+procedure {:stable} {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid' != nil;

+ensures {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && tid == tid' && old(currsize) <= currsize;

 ensures {:both 2} |{ A: return true; }|;

 {

+   tid := tid';

 }

 

 procedure {:stable} {:yields} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

@@ -97,16 +98,15 @@ READ_DEVICE:
     call tid := release(tid);

 

 COPY_TO_BUFFER:

-    assert {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize); assume false;

-    par YieldToReadCache();

-    call ReadCache(start, bytesRead);

+    par tid := YieldToReadCache(tid);

+    call tid := ReadCache(tid, start, bytesRead);

 }

 

 procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} ghostLock == tid' && tid' != nil;

 ensures {:phase 1} tid == tid';

-ensures {:phase 1} Inv(ghostLock, currsize, newsize);

+ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

 {

     var j: int;

     tid := tid';

@@ -114,7 +114,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     call tid, j := ReadCurrsize(tid);

     while (j < index)

     invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize);

+    invariant {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

     {

         par tid := YieldToWriteCache(tid);

         call tid := WriteCacheEntry(tid, j);

@@ -122,28 +122,32 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     }

 }

 

-procedure {:yields} ReadCache(start: int, bytesRead: int)

+procedure {:yields} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

+requires {:phase 1} tid' != nil;

 requires {:phase 1} 0 <= start && 0 <= bytesRead;

 requires {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize);

+ensures {:phase 1} tid == tid';

 ensures {:phase 1} Inv(ghostLock, currsize, newsize);

 {

     var j: int;

+    tid := tid';

+

     j := 0;

     while(j < bytesRead)

     invariant {:phase 1} 0 <= j;

     invariant {:phase 1} bytesRead == 0 || start + j <= currsize; 

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize);

+    invariant {:phase 1} Inv(ghostLock, currsize, newsize) && tid == tid';

     {

-	par YieldToReadCache();

+	par tid := YieldToReadCache(tid);

 	assert {:phase 1} start + j < currsize;

-        call ReadCacheEntry(start + j);

+        call tid := ReadCacheEntry(tid, start + j);

         j := j + 1;

     }

 }

 

 procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:both 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

+ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

 

 procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

 ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

@@ -157,8 +161,8 @@ ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock ==
 procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

 ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

 

-procedure {:yields} ReadCacheEntry(index: int);

-ensures {:atomic 0} |{ A: assert 0 <= index && index < currsize; return true; }|;

+procedure {:yields} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic 0} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|;

 

 procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

 ensures {:right 0} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index b628df30..857ca14e 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -108,7 +108,7 @@ ensures {:both 1} |{ A: return true; }|;
 }

 

 procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:both 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

+ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

 procedure {:yields} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

 ensures {:atomic 0} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;