From cb0b9f5a55296ab504cb5c5d6ce863a9def7f705 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 22 Dec 2013 14:11:24 -0800 Subject: more bug fixes --- Source/Concurrency/OwickiGries.cs | 22 +++++++++++----------- 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 cmds = base.VisitCmdSeq(cmdSeq); List newCmds = new List(); - 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(), inParams, outParams, requiresSeq, new List(), ensuresSeq); + proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), 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(), 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(), new List(), new List(), new List()); 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(), new List()); + 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(), new List()); } 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(), 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 -- cgit v1.2.3