diff options
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 22 | ||||
| -rw-r--r-- | Test/og/Answer | 14 |
2 files changed, 18 insertions, 18 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 5aff9bb7..8869c447 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -28,16 +28,19 @@ namespace Microsoft.Boogie {
List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);
List<Cmd> newCmds = new List<Cmd>();
- foreach (Cmd cmd in cmds)
+ for (int i = 0; i < cmds.Count; i++)
{
+ Cmd cmd = cmds[i];
ParCallCmd parCallCmd = cmd as ParCallCmd;
- if (parCallCmd == null)
+ Cmd originalCmd = cmdSeq[i];
+ ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;
+ if (originalParCallCmd == null)
{
newCmds.Add(cmd);
continue;
}
int maxCalleePhaseNum = 0;
- foreach (CallCmd iter in parCallCmd.CallCmds)
+ foreach (CallCmd iter in originalParCallCmd.CallCmds)
{
int calleePhaseNum = moverTypeChecker.FindPhaseNumber(iter.Proc);
if (calleePhaseNum > maxCalleePhaseNum)
@@ -84,11 +87,6 @@ namespace Microsoft.Boogie public override Cmd VisitParCallCmd(ParCallCmd node)
{
ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- callCmd.Proc = VisitProcedure(callCmd.Proc);
- callCmd.callee = callCmd.Proc.Name;
- }
absyMap[node] = parCallCmd;
return parCallCmd;
}
@@ -358,7 +356,7 @@ namespace Microsoft.Boogie }
count++;
}
- proc = new Procedure(Token.NoToken, string.Format("{0}_{1}", procName, phaseNum), new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
+ proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
asyncAndParallelCallDesugarings[procName] = proc;
}
CallCmd dummyCallCmd = new CallCmd(Token.NoToken, proc.Name, ins, outs);
@@ -453,7 +451,7 @@ namespace Microsoft.Boogie yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
// Create the yield checker procedure
- var yieldCheckerName = string.Format("{0}_YieldChecker_{1}_{2}", decl is Procedure ? "Proc" : "Impl", decl.Name, phaseNum);
+ var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);
var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
yieldCheckerProcs.Add(yieldCheckerProc);
@@ -593,7 +591,7 @@ namespace Microsoft.Boogie {
if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
{
- asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}_{1}", callCmd.Proc.Name, phaseNum), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
+ asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
}
var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
@@ -967,6 +965,8 @@ namespace Microsoft.Boogie procs.Add(duplicateProc);
if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum)
{
+ duplicateProc.Attributes = OwickiGries.RemoveYieldsAttribute(duplicateProc.Attributes);
+ program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(new IdentifierExpr(Token.NoToken, x)));
CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);
Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), action.Blocks);
impl.Proc = duplicateProc;
diff --git a/Test/og/Answer b/Test/og/Answer index 54ceb547..73ec8537 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -3,7 +3,7 @@ foo.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
foo.bpl(6,5): anon0
- (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0
+ (0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
Boogie program verifier finished with 4 verified, 1 error
@@ -11,11 +11,11 @@ Boogie program verifier finished with 4 verified, 1 error bar.bpl(13,3): Error BP5001: This assertion might not hold.
Execution trace:
bar.bpl(6,5): anon0
- (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0
+ (0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
bar.bpl(13,3): Error BP5001: This assertion might not hold.
Execution trace:
bar.bpl(23,5): anon0
- (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0
+ (0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
Boogie program verifier finished with 3 verified, 2 errors
@@ -27,11 +27,11 @@ Boogie program verifier finished with 2 verified, 0 errors parallel1.bpl(10,1): Error BP5001: This assertion might not hold.
Execution trace:
parallel1.bpl(6,5): anon0
- (0,0): inline$Proc_YieldChecker_PC_2147483647_2147483647$0$L0
+ (0,0): inline$Proc_YieldChecker_PC_2147483647$0$L0
parallel1.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
parallel1.bpl(6,5): anon0
- (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0
+ (0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
Boogie program verifier finished with 3 verified, 2 errors
@@ -75,7 +75,7 @@ Boogie program verifier finished with 3 verified, 0 errors t1.bpl(35,5): Error BP5001: This assertion might not hold.
Execution trace:
(0,0): og_init
- (0,0): inline$Impl_YieldChecker_A_2147483647_2147483647$0$L1
+ (0,0): inline$Impl_YieldChecker_A_2147483647$0$L1
Boogie program verifier finished with 2 verified, 1 error
@@ -92,6 +92,6 @@ async.bpl(14,1): Error BP5001: This assertion might not hold. Execution trace:
async.bpl(7,3): anon0
async.bpl(7,3): anon0$1
- (0,0): inline$Proc_YieldChecker_P_2147483647_2147483647$1$L0
+ (0,0): inline$Proc_YieldChecker_P_2147483647$1$L0
Boogie program verifier finished with 1 verified, 1 error
|