From 0b396a7572daddd3f5dc1873c4507f92c078d6bb Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 24 Dec 2013 20:52:24 -0800 Subject: more bug fixes updates to DeviceCache.bpl to make it verify --- Source/Concurrency/OwickiGries.cs | 100 ++++++++++++++++++++++++++++---------- Source/Concurrency/TypeCheck.cs | 30 +++++++----- Source/Core/AbsyQuant.cs | 31 ++++++++++++ Test/og/DeviceCache.bpl | 34 +++++++------ Test/og/ticket.bpl | 2 +- 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 procMap; /* Original -> Duplicate */ public Dictionary absyMap; /* Original -> Duplicate */ public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum) { this.moverTypeChecker = moverTypeChecker; this.phaseNum = phaseNum; + this.enclosingProcPhaseNum = int.MaxValue; this.procMap = new Dictionary(); this.absyMap = new Dictionary(); } + private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) + { + Procedure originalProc = originalCallCmd.Proc; + if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc) && moverTypeChecker.procToActionInfo[originalProc].phaseNum < phaseNum) + { + List gate = moverTypeChecker.procToActionInfo[originalProc].thisGate; + Dictionary map = new Dictionary(); + 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 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 VisitCmdSeq(List cmdSeq) { List cmds = base.VisitCmdSeq(cmdSeq); List newCmds = new List(); - 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 FindPhaseNums(QKeyValue kv) + { + HashSet 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 FindExprAttributes(QKeyValue kv, string name) + { + Contract.Requires(name != null); + HashSet attrs = new HashSet(); + 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 FindIntAttributes(QKeyValue kv, string name) + { + Contract.Requires(name != null); + HashSet attrs = new HashSet(); + HashSet 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 newParams = new List(); 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; }|; -- cgit v1.2.3