diff options
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 183 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 253 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 221 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 20 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 24 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 12 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 21 | ||||
| -rw-r--r-- | Test/og/Answer | 12 | ||||
| -rw-r--r-- | Test/og/DeviceCache.bpl | 19 | ||||
| -rw-r--r-- | Test/og/DeviceCacheWithBuffer.bpl | 23 | ||||
| -rw-r--r-- | Test/og/lock.bpl | 2 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/og/ticket.bpl | 35 |
13 files changed, 492 insertions, 337 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 2b6b406a..79f0f519 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -7,136 +7,6 @@ using System.Diagnostics; namespace Microsoft.Boogie
{
- public enum MoverType
- {
- Top,
- Atomic,
- Right,
- Left,
- Both
- }
-
- public class ActionInfo
- {
- public Procedure proc;
- public MoverType moverType;
- public int phaseNum;
- public HashSet<int> callerPhaseNums;
- public List<AssertCmd> thisGate;
- public CodeExpr thisAction;
- public List<Variable> thisInParams;
- public List<Variable> thisOutParams;
- public List<AssertCmd> thatGate;
- public CodeExpr thatAction;
- public List<Variable> thatInParams;
- public List<Variable> thatOutParams;
-
- public bool IsRightMover
- {
- get { return moverType == MoverType.Right || moverType == MoverType.Both; }
- }
-
- public bool IsLeftMover
- {
- get { return moverType == MoverType.Left || moverType == MoverType.Both; }
- }
-
- public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)
- {
- this.proc = proc;
- this.moverType = moverType;
- this.phaseNum = phaseNum;
- this.callerPhaseNums = new HashSet<int>();
- this.thisGate = new List<AssertCmd>();
- this.thisAction = codeExpr;
- this.thisInParams = new List<Variable>();
- this.thisOutParams = new List<Variable>();
- this.thatGate = new List<AssertCmd>();
- this.thatInParams = new List<Variable>();
- this.thatOutParams = new List<Variable>();
-
- var cmds = thisAction.Blocks[0].Cmds;
- for (int i = 0; i < cmds.Count; i++)
- {
- AssertCmd assertCmd = cmds[i] as AssertCmd;
- if (assertCmd == null) break;
- thisGate.Add(assertCmd);
- cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
- }
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable x in proc.InParams)
- {
- this.thisInParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
- this.thatInParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- foreach (Variable x in proc.OutParams)
- {
- this.thisOutParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- this.thatOutParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- List<Variable> otherLocVars = new List<Variable>();
- foreach (Variable x in thisAction.LocVars)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- otherLocVars.Add(y);
- }
- Contract.Assume(proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in thisGate)
- {
- thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
- }
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> otherBlocks = new List<Block>();
- foreach (Block block in thisAction.Blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(Substituter.Apply(subst, cmd));
- }
- Block otherBlock = new Block();
- otherBlock.Cmds = otherCmds;
- otherBlock.Label = "that_" + block.Label;
- block.Label = "this_" + block.Label;
- otherBlocks.Add(otherBlock);
- blockMap[block] = otherBlock;
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- for (int i = 0; i < gotoCmd.labelNames.Count; i++)
- {
- gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
- }
- }
- }
- foreach (Block block in thisAction.Blocks)
- {
- if (block.TransferCmd is ReturnExprCmd)
- {
- blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
- continue;
- }
- List<Block> otherGotoCmdLabelTargets = new List<Block>();
- List<string> otherGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- otherGotoCmdLabelTargets.Add(blockMap[target]);
- otherGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
- }
- this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
- }
- }
-
public class MoverCheck
{
public static MoverType GetMoverType(Ensures e, out int phaseNum)
@@ -232,25 +102,42 @@ namespace Microsoft.Boogie {
if (moverTypeChecker.procToActionInfo.Count == 0)
return;
- Program program = moverTypeChecker.program;
- MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker);
- foreach (ActionInfo first in moverTypeChecker.procToActionInfo.Values)
+
+ Dictionary<int, HashSet<ActionInfo>> pools = new Dictionary<int, HashSet<ActionInfo>>();
+ foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
{
- Debug.Assert(first.moverType != MoverType.Top);
- if (first.moverType == MoverType.Atomic)
- continue;
- foreach (ActionInfo second in moverTypeChecker.procToActionInfo.Values)
+ foreach (int phaseNum in action.callerPhaseNums)
{
- if (first.IsRightMover)
+ if (!pools.ContainsKey(phaseNum))
{
- moverChecking.CreateCommutativityChecker(program, first, second);
- moverChecking.CreateGatePreservationChecker(program, second, first);
+ pools[phaseNum] = new HashSet<ActionInfo>();
}
- if (first.IsLeftMover)
+ pools[phaseNum].Add(action);
+ }
+ }
+
+ Program program = moverTypeChecker.program;
+ MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker);
+ foreach (int phaseNum in pools.Keys)
+ {
+ foreach (ActionInfo first in pools[phaseNum])
+ {
+ Debug.Assert(first.moverType != MoverType.Top);
+ if (first.moverType == MoverType.Atomic)
+ continue;
+ foreach (ActionInfo second in pools[phaseNum])
{
- moverChecking.CreateCommutativityChecker(program, second, first);
- moverChecking.CreateGatePreservationChecker(program, first, second);
- moverChecking.CreateFailurePreservationChecker(program, second, first);
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
+ }
}
}
}
@@ -383,7 +270,7 @@ namespace Microsoft.Boogie private void Search(Block b, bool inFirst)
{
dfsStack.Push(b);
- if (b.TransferCmd is ReturnExprCmd)
+ if (b.TransferCmd is ReturnCmd)
{
if (first == null || inFirst)
{
@@ -425,11 +312,7 @@ namespace Microsoft.Boogie }
foreach (Block block in blocks)
{
- if (block.TransferCmd is ReturnExprCmd)
- {
- blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
- continue;
- }
+ if (block.TransferCmd is ReturnCmd) continue;
List<Block> otherGotoCmdLabelTargets = new List<Block>();
List<string> otherGotoCmdLabelNames = new List<string>();
GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 561d9a53..b16e4978 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -10,20 +10,168 @@ using System.Diagnostics.Contracts; namespace Microsoft.Boogie
{
+ public class MyDuplicator : Duplicator
+ {
+ MoverTypeChecker moverTypeChecker;
+ int phaseNum;
+ 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.procMap = new Dictionary<Procedure, Procedure>();
+ this.absyMap = new Dictionary<Absy, Absy>();
+ }
+
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
+ {
+ List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);
+ List<Cmd> newCmds = new List<Cmd>();
+ foreach (Cmd cmd in cmds)
+ {
+ ParCallCmd parCallCmd = cmd as ParCallCmd;
+ if (parCallCmd == null)
+ {
+ newCmds.Add(cmd);
+ continue;
+ }
+ int maxCalleePhaseNum = 0;
+ foreach (CallCmd iter in parCallCmd.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
+ {
+ newCmds.Add(parCallCmd);
+ }
+ }
+ return newCmds;
+ }
+
+ public override YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ YieldCmd yieldCmd = base.VisitYieldCmd(node);
+ absyMap[node] = yieldCmd;
+ return yieldCmd;
+ }
+
+ public override Block VisitBlock(Block node)
+ {
+ Block block = base.VisitBlock(node);
+ absyMap[node] = block;
+ return block;
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);
+ callCmd.Proc = VisitProcedure(callCmd.Proc);
+ absyMap[node] = callCmd;
+ return callCmd;
+ }
+
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
+ {
+ callCmd.Proc = VisitProcedure(callCmd.Proc);
+ }
+ absyMap[node] = parCallCmd;
+ return parCallCmd;
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))
+ return node;
+ if (!procMap.ContainsKey(node))
+ procMap[node] = base.VisitProcedure(node);
+ return procMap[node];
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ if (moverTypeChecker.procToActionInfo.ContainsKey(node.Proc) && moverTypeChecker.procToActionInfo[node.Proc].phaseNum < phaseNum)
+ {
+ CodeExpr action = (CodeExpr) VisitCodeExpr(moverTypeChecker.procToActionInfo[node.Proc].thisAction);
+ Implementation impl = new Implementation(Token.NoToken, node.Name, node.Proc.TypeParameters, node.Proc.InParams, node.Proc.OutParams, new List<Variable>(), action.Blocks);
+ impl.Proc = VisitProcedure(node.Proc);
+ impl.Proc.AddAttribute("inline", 1);
+ impl.AddAttribute("inline", 1);
+ return impl;
+ }
+ else
+ {
+ Implementation impl = base.VisitImplementation(node);
+ foreach (Block block in impl.Blocks)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd == null) continue;
+ List<Block> labelTargets = new List<Block>();
+ List<string> labelNames = new List<string>();
+ foreach (Block x in gotoCmd.labelTargets)
+ {
+ Block y = (Block)absyMap[x];
+ labelTargets.Add(y);
+ labelNames.Add(y.Label);
+ }
+ gotoCmd.labelTargets = labelTargets;
+ gotoCmd.labelNames = labelNames;
+ }
+ return impl;
+ }
+ }
+
+ public override Requires VisitRequires(Requires node)
+ {
+ Requires requires = base.VisitRequires(node);
+ if (QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue) != phaseNum)
+ requires.Condition = Expr.True;
+ return requires;
+ }
+
+ public override Ensures VisitEnsures(Ensures node)
+ {
+ Ensures ensures = base.VisitEnsures(node);
+ if (ensures.IsAtomicSpecification || QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue) != phaseNum)
+ ensures.Condition = Expr.True;
+ return ensures;
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
+ if (QKeyValue.FindIntAttribute(assertCmd.Attributes, "phase", int.MaxValue) != phaseNum)
+ assertCmd.Expr = Expr.True;
+ return assertCmd;
+ }
+ }
+
public class OwickiGriesTransform
{
List<IdentifierExpr> globalMods;
LinearTypeChecker linearTypeChecker;
- MoverTypeChecker moverTypeChecker;
+ Dictionary<Absy, Absy> absyMap;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGriesTransform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
+ public OwickiGriesTransform(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap)
{
this.linearTypeChecker = linearTypeChecker;
- this.moverTypeChecker = moverTypeChecker;
+ this.absyMap = absyMap;
Program program = linearTypeChecker.program;
globalMods = new List<IdentifierExpr>();
foreach (Variable g in program.GlobalVariables())
@@ -36,6 +184,11 @@ namespace Microsoft.Boogie yieldProc = null;
}
+ private HashSet<Variable> AvailableLinearVars(Absy absy)
+ {
+ return linearTypeChecker.availableLinearVars[absyMap[absy]];
+ }
+
private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
List<Expr> exprSeq = new List<Expr>();
@@ -120,7 +273,7 @@ namespace Microsoft.Boogie {
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[yieldCmd], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
for (int j = 0; j < cmds.Count; j++)
@@ -320,8 +473,6 @@ namespace Microsoft.Boogie {
if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return;
- TransformProc(impl.Proc);
-
// Find the yielding loop headers
impl.PruneUnreachableBlocks();
impl.ComputePredecessorsForBlocks();
@@ -437,7 +588,7 @@ namespace Microsoft.Boogie }
if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
{
- HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypeChecker.availableLinearVars[callCmd]);
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
foreach (IdentifierExpr ie in callCmd.Outs)
{
if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;
@@ -452,7 +603,7 @@ namespace Microsoft.Boogie ParCallCmd parCallCmd = cmd as ParCallCmd;
AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
DesugarParallelCallCmd(newCmds, parCallCmd);
- HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypeChecker.availableLinearVars[parCallCmd]);
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
foreach (IdentifierExpr ie in callCmd.Outs)
@@ -487,7 +638,7 @@ namespace Microsoft.Boogie foreach (Block header in yieldingHeaders)
{
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
@@ -644,7 +795,7 @@ namespace Microsoft.Boogie CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
}
- private void AddYieldProcAndImpl()
+ private void AddYieldProcAndImpl(List<Declaration> decls)
{
if (yieldProc == null) return;
@@ -690,8 +841,8 @@ namespace Microsoft.Boogie var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
yieldImpl.Proc = yieldProc;
yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- program.TopLevelDeclarations.Add(yieldProc);
- program.TopLevelDeclarations.Add(yieldImpl);
+ decls.Add(yieldProc);
+ decls.Add(yieldImpl);
}
private QKeyValue RemoveYieldsAttribute(QKeyValue iter)
@@ -701,50 +852,98 @@ namespace Microsoft.Boogie return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;
}
- public void Transform()
+ public void Transform(List<Implementation> impls, List<Procedure> procs, List<Declaration> decls)
{
- Program program = linearTypeChecker.program;
- foreach (var decl in program.TopLevelDeclarations)
+ foreach (var impl in impls)
{
- Implementation impl = decl as Implementation;
- if (impl == null) continue;
TransformImpl(impl);
}
+ foreach (var proc in procs)
+ {
+ TransformProc(proc);
+ }
foreach (Procedure proc in yieldCheckerProcs)
{
- program.TopLevelDeclarations.Add(proc);
+ decls.Add(proc);
}
foreach (Implementation impl in yieldCheckerImpls)
{
- program.TopLevelDeclarations.Add(impl);
+ decls.Add(impl);
}
foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)
{
- program.TopLevelDeclarations.Add(proc);
+ decls.Add(proc);
}
- AddYieldProcAndImpl();
- foreach (var decl in program.TopLevelDeclarations)
+ AddYieldProcAndImpl(decls);
+ foreach (var proc in procs)
{
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
{
HashSet<Variable> modifiedVars = new HashSet<Variable>();
proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
- foreach (GlobalVariable g in program.GlobalVariables())
+ foreach (GlobalVariable g in linearTypeChecker.program.GlobalVariables())
{
if (modifiedVars.Contains(g)) continue;
proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
}
proc.Attributes = RemoveYieldsAttribute(proc.Attributes);
}
+ decls.Add(proc);
+ }
+ foreach (var impl in impls)
+ {
+ impl.Attributes = RemoveYieldsAttribute(impl.Attributes);
+ decls.Add(impl);
}
+ }
+
+ public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
+ {
+ Program program = linearTypeChecker.program;
+ List<Procedure> originalProcs = new List<Procedure>();
+ List<Implementation> originalImpls = new List<Implementation>();
foreach (var decl in program.TopLevelDeclarations)
{
+ Procedure proc = decl as Procedure;
+ if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+ {
+ originalProcs.Add(proc);
+ continue;
+ }
Implementation impl = decl as Implementation;
- if (impl == null) continue;
- impl.Attributes = RemoveYieldsAttribute(impl.Attributes);
+ if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ {
+ originalImpls.Add(impl);
+ }
+ }
+ List<Declaration> decls = new List<Declaration>();
+ foreach (int phaseNum in moverTypeChecker.assertionPhaseNums)
+ {
+ MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, int.MaxValue);
+ List<Implementation> impls = new List<Implementation>();
+ List<Procedure> procs = new List<Procedure>();
+ foreach (Implementation impl in originalImpls)
+ {
+ Implementation duplicateImpl = duplicator.VisitImplementation(impl);
+ impls.Add(duplicateImpl);
+ procs.Add(duplicateImpl.Proc);
+ }
+ foreach (Procedure proc in originalProcs)
+ {
+ if (duplicator.procMap.ContainsKey(proc)) continue;
+ procs.Add(duplicator.VisitProcedure(proc));
+ }
+ Dictionary<Absy, Absy> reverseAbsyMap = new Dictionary<Absy, Absy>();
+ foreach (Absy key in duplicator.absyMap.Keys)
+ {
+ reverseAbsyMap[duplicator.absyMap[key]] = key;
+ }
+ OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker, reverseAbsyMap);
+ ogTransform.Transform(impls, procs, decls);
}
+ program.TopLevelDeclarations.RemoveAll(x => originalImpls.Contains(x));
+ program.TopLevelDeclarations.RemoveAll(x => originalProcs.Contains(x));
+ program.TopLevelDeclarations.AddRange(decls);
}
}
}
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 41fb9480..0a9e6c48 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -3,9 +3,141 @@ using System.Collections.Generic; using System.Linq;
using System.Text;
using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
namespace Microsoft.Boogie
{
+ public enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ public class ActionInfo
+ {
+ public Procedure proc;
+ public MoverType moverType;
+ public int phaseNum;
+ public HashSet<int> callerPhaseNums;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+
+ public bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)
+ {
+ this.proc = proc;
+ this.moverType = moverType;
+ this.phaseNum = phaseNum;
+ this.callerPhaseNums = new HashSet<int>();
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
+ this.thatInParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ this.thatOutParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ List<Variable> otherLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ otherLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
+ }
+ }
+
public class MoverTypeChecker : StandardVisitor
{
public int FindPhaseNumber(Procedure proc)
@@ -19,11 +151,10 @@ namespace Microsoft.Boogie CheckingContext checkingContext;
public int errorCount;
HashSet<Variable> globalVariables;
- bool globalVarAccessAllowed;
- bool visitingAssertion;
int enclosingProcPhaseNum;
public Dictionary<Procedure, ActionInfo> procToActionInfo;
public Program program;
+ public HashSet<int> assertionPhaseNums;
public void TypeCheck()
{
@@ -58,29 +189,19 @@ namespace Microsoft.Boogie public MoverTypeChecker(Program program)
{
- this.globalVariables = new HashSet<Variable>(program.GlobalVariables());
+ this.globalVariables = new HashSet<Variable>();
+ foreach (var g in program.GlobalVariables())
+ {
+ if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))
+ this.globalVariables.Add(g);
+ }
this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+ this.assertionPhaseNums = new HashSet<int>();
this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
this.program = program;
- this.visitingAssertion = false;
this.enclosingProcPhaseNum = int.MaxValue;
}
- public override Block VisitBlock(Block node)
- {
- globalVarAccessAllowed = false;
- return base.VisitBlock(node);
- }
- public override Cmd VisitHavocCmd(HavocCmd node)
- {
- globalVarAccessAllowed = false;
- return base.VisitHavocCmd(node);
- }
- public override Cmd VisitAssignCmd(AssignCmd node)
- {
- globalVarAccessAllowed = false;
- return base.VisitAssignCmd(node);
- }
public override Implementation VisitImplementation(Implementation node)
{
enclosingProcPhaseNum = FindPhaseNumber(node.Proc);
@@ -93,10 +214,6 @@ namespace Microsoft.Boogie }
public override Cmd VisitCallCmd(CallCmd node)
{
- globalVarAccessAllowed = false;
- if (enclosingProcPhaseNum == int.MaxValue)
- return base.VisitCallCmd(node);
-
if (!node.IsAsync)
{
int calleePhaseNum = FindPhaseNumber(node.Proc);
@@ -104,7 +221,7 @@ namespace Microsoft.Boogie {
procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum);
}
- else
+ else if (enclosingProcPhaseNum < calleePhaseNum || enclosingProcPhaseNum != int.MaxValue)
{
Error(node, "The phase of the caller procedure must be greater than the phase of the callee");
}
@@ -113,20 +230,11 @@ namespace Microsoft.Boogie }
public override Cmd VisitParCallCmd(ParCallCmd node)
{
- globalVarAccessAllowed = false;
- foreach (CallCmd callCmd in node.CallCmds)
- {
- base.VisitCallCmd(callCmd);
- }
-
- if (enclosingProcPhaseNum == int.MaxValue)
- return node;
-
int maxCalleePhaseNum = 0;
foreach (CallCmd iter in node.CallCmds)
{
int calleePhaseNum = FindPhaseNumber(iter.Proc);
- if (calleePhaseNum < maxCalleePhaseNum)
+ if (calleePhaseNum > maxCalleePhaseNum)
maxCalleePhaseNum = calleePhaseNum;
}
@@ -141,21 +249,16 @@ namespace Microsoft.Boogie isRightMover = isRightMover && actionInfo.IsRightMover;
actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum);
}
- if (!isLeftMover && !isRightMover)
+ if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
{
Error(node, "The procedures in the parallel call must be all right mover or all left mover");
}
}
return node;
}
- public override YieldCmd VisitYieldCmd(YieldCmd node)
- {
- globalVarAccessAllowed = true;
- return base.VisitYieldCmd(node);
- }
public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
- if (!visitingAssertion && !globalVarAccessAllowed && globalVariables.Contains(node.Decl))
+ if (globalVariables.Contains(node.Decl))
{
Error(node, "Cannot access global variable");
}
@@ -163,50 +266,36 @@ namespace Microsoft.Boogie }
public override Ensures VisitEnsures(Ensures ensures)
{
- int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", 0);
+ if (ensures.IsAtomicSpecification)
+ return ensures;
+ int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue);
+ assertionPhaseNums.Add(phaseNum);
if (phaseNum > enclosingProcPhaseNum)
{
Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");
}
- this.visitingAssertion = true;
- Ensures ret = base.VisitEnsures(ensures);
- this.visitingAssertion = false;
- return ret;
+ return ensures;
}
public override Requires VisitRequires(Requires requires)
{
- int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", 0);
+ int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue);
+ assertionPhaseNums.Add(phaseNum);
if (phaseNum > enclosingProcPhaseNum)
{
Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");
}
- this.visitingAssertion = true;
- Requires ret = base.VisitRequires(requires);
- this.visitingAssertion = false;
- return ret;
+ return requires;
}
public override Cmd VisitAssertCmd(AssertCmd node)
{
- int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0);
+ int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", int.MaxValue);
+ assertionPhaseNums.Add(phaseNum);
if (phaseNum > enclosingProcPhaseNum)
{
Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");
}
- this.visitingAssertion = true;
- Cmd ret = base.VisitAssertCmd(node);
- this.visitingAssertion = false;
- return ret;
- }
- public override Cmd VisitAssumeCmd(AssumeCmd node)
- {
- int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0);
- if (phaseNum > enclosingProcPhaseNum)
- {
- Error(node, "The phase of assume cannot be greater than the phase of enclosing procedure");
- }
- return base.VisitAssumeCmd(node);
+ return node;
}
-
public void Error(Absy node, string message)
{
checkingContext.Error(node, message);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 6c333143..65de2297 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2351,14 +2351,22 @@ namespace Microsoft.Boogie { this.Condition.Resolve(rc);
}
+ public bool IsAtomicSpecification
+ {
+ get
+ {
+ return
+ QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
+ }
+ }
+
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
- bool isAtomicSpecification =
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
- if (isAtomicSpecification && !tc.Yields)
+
+ if (IsAtomicSpecification && !tc.Yields)
{
tc.Error(this, "atomic specification allowed only in a yielding procedure");
return;
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 056a47f9..0c49867c 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -113,15 +113,6 @@ namespace Microsoft.Boogie { clone.Outs = new List<IdentifierExpr>(clone.Outs);
return base.VisitCallCmd(clone);
}
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- ParCallCmd clone = (ParCallCmd)node.Clone();
- Contract.Assert(clone != null);
- clone.CallCmds = new List<CallCmd>(node.CallCmds);
- return base.VisitParCallCmd(clone);
- }
public override Choice VisitChoice(Choice node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Choice>() != null);
@@ -251,6 +242,15 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Expr>() != null);
return base.VisitOldExpr((OldExpr)node.Clone());
}
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ ParCallCmd clone = (ParCallCmd)node.Clone();
+ Contract.Assert(clone != null);
+ clone.CallCmds = new List<CallCmd>(node.CallCmds);
+ return base.VisitParCallCmd(clone);
+ }
public override Procedure VisitProcedure(Procedure node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Procedure>() != null);
@@ -352,6 +352,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Requires>() != null);
return base.VisitRequires((Requires)node.Clone());
}
+ public override YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Requires>() != null);
+ return base.VisitYieldCmd((YieldCmd)node.Clone());
+ }
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index cd59638b..4605019f 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -468,12 +468,6 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<ReturnCmd>() != null);
return (ReturnCmd)this.VisitTransferCmd(node);
}
- public virtual YieldCmd VisitYieldCmd(YieldCmd node)
- {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<YieldCmd>() != null);
- return node;
- }
public virtual ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);
@@ -588,6 +582,12 @@ namespace Microsoft.Boogie { }
return variableSeq;
}
+ public virtual YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<YieldCmd>() != null);
+ return node;
+ }
public virtual Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e7b55dc4..bed9c6c0 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -485,8 +485,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker, moverTypeChecker);
- ogTransform.Transform();
+ OwickiGriesTransform.Transform(linearTypeChecker, moverTypeChecker);
var eraser = new LinearEraser();
eraser.VisitProgram(program);
if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
@@ -683,6 +682,14 @@ namespace Microsoft.Boogie CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
}
+ moverTypeChecker = new MoverTypeChecker(program);
+ moverTypeChecker.TypeCheck();
+ if (moverTypeChecker.errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
+ return PipelineOutcome.TypeCheckingError;
+ }
+
linearTypeChecker = new LinearTypeChecker(program);
linearTypeChecker.TypeCheck();
if (linearTypeChecker.errorCount == 0)
@@ -695,16 +702,6 @@ namespace Microsoft.Boogie return PipelineOutcome.TypeCheckingError;
}
-#if QED
- moverTypeChecker = new MoverTypeChecker(program);
- moverTypeChecker.TypeCheck();
- if (moverTypeChecker.errorCount != 0)
- {
- Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
- return PipelineOutcome.TypeCheckingError;
- }
-#endif
-
if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
{
// if PrintDesugaring option is engaged, print the file here, after resolution and type checking
diff --git a/Test/og/Answer b/Test/og/Answer index d4111927..8397d051 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -35,10 +35,6 @@ Execution trace: Boogie program verifier finished with 3 verified, 2 errors
--------------------- parallel3.bpl --------------------
-
-Boogie program verifier finished with 3 verified, 0 errors
-
-------------------- linear-set.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
@@ -71,14 +67,6 @@ Boogie program verifier finished with 2 verified, 1 error Boogie program verifier finished with 4 verified, 0 errors
--------------------- parallel6.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- parallel7.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-------------------- akash.bpl --------------------
Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index ede0a31e..c93d5d21 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -1,10 +1,10 @@ type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var ghostLock: X;
-var lock: X;
-var currsize: int;
-var newsize: int;
+var {:qed} ghostLock: X;
+var {:qed} lock: X;
+var {:qed} currsize: int;
+var {:qed} newsize: int;
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
{
@@ -87,7 +87,7 @@ ensures 0 <= bytesRead && bytesRead <= size; }
READ_DEVICE:
- par Skip() | tid := YieldToWriteCache(tid);
+ par tid := YieldToWriteCache(tid);
call tid := WriteCache(tid, start + size);
call tid := acquire(tid);
call tid, tmp := ReadNewsize(tid);
@@ -95,7 +95,7 @@ READ_DEVICE: call tid := release(tid);
COPY_TO_BUFFER:
- par Skip() | YieldToReadCache();
+ par YieldToReadCache();
call ReadCache(start, bytesRead);
}
@@ -107,7 +107,7 @@ ensures {:right 1} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; r call tid, j := ReadCurrsize(tid);
while (j < index)
- invariant ghostLock == tid && currsize <= j && tid == tid';
+ invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
{
call tid := WriteCacheEntry(tid, j);
j := j + 1;
@@ -155,8 +155,3 @@ ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lo procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
-
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ A: return true; }|;
-{
-}
\ No newline at end of file diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index fa2cc611..f1da0ecf 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -1,13 +1,13 @@ type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var ghostLock: X;
-var lock: X;
-var currsize: int;
-var newsize: int;
+var {:qed} ghostLock: X;
+var {:qed} lock: X;
+var {:qed} currsize: int;
+var {:qed} newsize: int;
const device: [int]int;
-var cache: [int]int;
+var {:qed} cache: [int]int;
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int, cache: [int]int) : (bool)
{
@@ -93,7 +93,7 @@ ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+ }
READ_DEVICE:
- par Skip() | tid := YieldToWriteCache(tid);
+ par tid := YieldToWriteCache(tid);
call tid := WriteCache(tid, start + size);
call tid := acquire(tid);
call tid, tmp := ReadNewsize(tid);
@@ -101,7 +101,7 @@ READ_DEVICE: call tid := release(tid);
COPY_TO_BUFFER:
- par Skip() | YieldToReadCache();
+ par YieldToReadCache();
call buffer := ReadCache(start, bytesRead);
}
@@ -113,8 +113,8 @@ ensures {:right 1} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; c call tid, j := ReadCurrsize(tid);
while (j < index)
- invariant ghostLock == tid && currsize <= j && tid == tid';
- invariant cache == (lambda i: int :: if (currsize <= i && i < j) then device[i] else old(cache)[i]);
+ invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
+ invariant {:phase 1} cache == (lambda i: int :: if (currsize <= i && i < j) then device[i] else old(cache)[i]);
{
call tid := WriteCacheEntry(tid, j);
j := j + 1;
@@ -168,8 +168,3 @@ ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lo procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
-
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ A: return true; }|;
-{
-}
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 4e4e6dec..c00560fe 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -1,4 +1,4 @@ -var b: bool;
+var {:qed} b: bool;
procedure {:yields} {:entrypoint} main()
{
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 1325e476..068f361f 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -3,13 +3,13 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (
+for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index d620abf3..9f467229 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -4,10 +4,10 @@ function RightClosed(n: int) : [int]bool; type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var t: int;
-var s: int;
-var cs: X;
-var T: [int]bool;
+var {:qed} t: int;
+var {:qed} s: int;
+var {:qed} cs: X;
+var {:qed} T: [int]bool;
procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures xl != nil;
@@ -50,11 +50,11 @@ requires {:phase 2} tid' != nil && Inv2(T, s, cs); invariant {:phase 1} Inv1(T, t);
invariant {:phase 2} tid != nil && Inv2(T, s, cs);
{
- par Skip() | Yield0() | Yield1() | Yield2();
+ par Yield1() | Yield2() | Yield();
call tid := Enter(tid);
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
call tid := Leave(tid);
- par Skip() | Yield0() | Yield1() | Yield2();
+ par Yield1() | Yield2() | Yield();
}
}
@@ -68,11 +68,11 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil var m: int;
tid := tid';
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
call tid, m := GetTicketAbstract(tid);
- par Skip() | Yield0();
+ par Yield1();
call tid := WaitAndEnter(tid, m);
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
}
procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
@@ -82,34 +82,29 @@ ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; re {
tid := tid';
- par Skip() | Yield0();
+ par Yield1();
call tid, m := GetTicket(tid);
- par Skip() | Yield0();
+ par Yield1();
}
-procedure {:yields} {:stable} Yield2()
+procedure {:yields} {:stable} Yield()
{
}
-procedure {:yields} {:stable} Yield1()
+procedure {:yields} {:stable} Yield2()
requires {:phase 2} Inv2(T, s, cs);
ensures {:phase 2} Inv2(T, s, cs);
ensures {:both 2} |{ A: return true; }|;
{
}
-procedure {:yields} {:stable} Yield0()
+procedure {:yields} {:stable} Yield1()
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T,t);
ensures {:both 1} |{ A: return true; }|;
{
}
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ 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; }|;
|