From 8aa34404bb634609719f90b59012771adb7d525d Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 15 Dec 2014 10:23:17 -0800 Subject: systematic renaming of phase to layer --- Source/Concurrency/MoverCheck.cs | 22 ++++---- Source/Concurrency/OwickiGries.cs | 44 ++++++++-------- Source/Concurrency/TypeCheck.cs | 93 +++++++++++++++++----------------- Source/Concurrency/YieldTypeChecker.cs | 22 ++++---- 4 files changed, 90 insertions(+), 91 deletions(-) diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 9a2203c3..1dd350de 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -35,34 +35,34 @@ namespace Microsoft.Boogie { AtomicActionInfo atomicAction = action as AtomicActionInfo; if (atomicAction == null) continue; - foreach (int phaseNum in moverTypeChecker.AllLayerNums) + foreach (int layerNum in moverTypeChecker.AllLayerNums) { - if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoLayerNum) + if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum) { - if (!pools.ContainsKey(phaseNum)) + if (!pools.ContainsKey(layerNum)) { - pools[phaseNum] = new HashSet(); + pools[layerNum] = new HashSet(); } - pools[phaseNum].Add(atomicAction); + pools[layerNum].Add(atomicAction); } } } Program program = moverTypeChecker.program; MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); - foreach (int phaseNum1 in pools.Keys) + foreach (int layerNum1 in pools.Keys) { - foreach (AtomicActionInfo first in pools[phaseNum1]) + foreach (AtomicActionInfo first in pools[layerNum1]) { Debug.Assert(first.moverType != MoverType.Top); if (first.moverType == MoverType.Atomic) continue; - foreach (int phaseNum2 in pools.Keys) + foreach (int layerNum2 in pools.Keys) { - if (phaseNum2 < phaseNum1) continue; - foreach (AtomicActionInfo second in pools[phaseNum2]) + if (layerNum2 < layerNum1) continue; + foreach (AtomicActionInfo second in pools[layerNum2]) { - if (second.phaseNum < phaseNum1) + if (second.createdAtLayerNum < layerNum1) { if (first.IsRightMover) { diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index f656da57..e485e1bc 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -14,7 +14,7 @@ namespace Microsoft.Boogie public class MyDuplicator : Duplicator { MoverTypeChecker moverTypeChecker; - public int phaseNum; + public int layerNum; Procedure enclosingProc; Implementation enclosingImpl; public Dictionary procMap; /* Original -> Duplicate */ @@ -23,10 +23,10 @@ namespace Microsoft.Boogie public HashSet yieldingProcs; public List impls; - public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum) + public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) { this.moverTypeChecker = moverTypeChecker; - this.phaseNum = phaseNum; + this.layerNum = layerNum; this.enclosingProc = null; this.enclosingImpl = null; this.procMap = new Dictionary(); @@ -38,12 +38,12 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) { - int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum; + int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; Procedure originalProc = originalCallCmd.Proc; if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) { AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; - if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcLayerNum) + if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && layerNum == enclosingProcLayerNum) { newCmds.Add(new HavocCmd(Token.NoToken, new List(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); Dictionary map = new Dictionary(); @@ -66,11 +66,11 @@ namespace Microsoft.Boogie int maxCalleeLayerNum = 0; foreach (CallCmd iter in originalParCallCmd.CallCmds) { - int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum; + int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; if (calleeLayerNum > maxCalleeLayerNum) maxCalleeLayerNum = calleeLayerNum; } - if (phaseNum > maxCalleeLayerNum) + if (layerNum > maxCalleeLayerNum) { for (int i = 0; i < parCallCmd.CallCmds.Count; i++) { @@ -150,13 +150,13 @@ namespace Microsoft.Boogie { enclosingProc = node; Procedure proc = (Procedure)node.Clone(); - proc.Name = string.Format("{0}_{1}", node.Name, phaseNum); + proc.Name = string.Format("{0}_{1}", node.Name, layerNum); proc.InParams = this.VisitVariableSeq(node.InParams); proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); proc.OutParams = this.VisitVariableSeq(node.OutParams); ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; - if (actionInfo.phaseNum < phaseNum) + if (actionInfo.createdAtLayerNum < layerNum) { proc.Requires = new List(); proc.Ensures = new List(); @@ -220,7 +220,7 @@ namespace Microsoft.Boogie Requires requires = base.VisitRequires(node); if (node.Free) return requires; - if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum)) + if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) requires.Condition = Expr.True; return requires; } @@ -232,7 +232,7 @@ namespace Microsoft.Boogie return ensures; AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; - if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(phaseNum)) + if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) { ensures.Condition = Expr.True; ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); @@ -243,7 +243,7 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node) { AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); - if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum)) + if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) assertCmd.Expr = Expr.True; return assertCmd; } @@ -256,7 +256,7 @@ namespace Microsoft.Boogie Dictionary absyMap; Dictionary implMap; HashSet yieldingProcs; - int phaseNum; + int layerNum; List globalMods; Dictionary asyncAndParallelCallDesugarings; List yieldCheckerProcs; @@ -274,7 +274,7 @@ namespace Microsoft.Boogie this.linearTypeChecker = linearTypeChecker; this.moverTypeChecker = moverTypeChecker; this.absyMap = duplicator.absyMap; - this.phaseNum = duplicator.phaseNum; + this.layerNum = duplicator.layerNum; this.implMap = duplicator.implMap; this.yieldingProcs = duplicator.yieldingProcs; Program program = linearTypeChecker.program; @@ -319,7 +319,7 @@ namespace Microsoft.Boogie Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); inputs.Add(f); } - yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List(), inputs, new List(), new List(), new List(), new List()); + yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List(), inputs, new List(), new List(), new List(), new List()); yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); } CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); @@ -716,7 +716,7 @@ namespace Microsoft.Boogie Procedure originalProc = implMap[impl].Proc; ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; - if (actionInfo.phaseNum == this.phaseNum) + if (actionInfo.createdAtLayerNum == this.layerNum) { pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); newLocalVars.Add(pc); @@ -742,11 +742,11 @@ namespace Microsoft.Boogie HashSet introducedVars = new HashSet(); foreach (Variable v in program.GlobalVariables) { - if (moverTypeChecker.hideLayerNums[v] <= actionInfo.phaseNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.phaseNum) + if (moverTypeChecker.hideLayerNums[v] <= actionInfo.createdAtLayerNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.createdAtLayerNum) { frame.Remove(v); } - if (moverTypeChecker.introduceLayerNums[v] == actionInfo.phaseNum) + if (moverTypeChecker.introduceLayerNums[v] == actionInfo.createdAtLayerNum) { introducedVars.Add(v); } @@ -1159,11 +1159,11 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int phaseNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 })) + foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 })) { - if (CommandLineOptions.Clo.TrustLayersDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; + if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; - MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum); + MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); foreach (var proc in program.Procedures) { if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; @@ -1174,7 +1174,7 @@ namespace Microsoft.Boogie OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); foreach (var impl in program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum) + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) continue; Implementation duplicateImpl = duplicator.VisitImplementation(impl); ogTransform.TransformImpl(duplicateImpl); diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index be40bbf0..39d75119 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -20,13 +20,13 @@ namespace Microsoft.Boogie public class ActionInfo { public Procedure proc; - public int phaseNum; + public int createdAtLayerNum; public int availableUptoLayerNum; - public ActionInfo(Procedure proc, int phaseNum, int availableUptoLayerNum) + public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum) { this.proc = proc; - this.phaseNum = phaseNum; + this.createdAtLayerNum = createdAtLayerNum; this.availableUptoLayerNum = availableUptoLayerNum; } @@ -77,8 +77,8 @@ namespace Microsoft.Boogie get { return moverType == MoverType.Left || moverType == MoverType.Both; } } - public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoLayerNum) - : base(proc, phaseNum, availableUptoLayerNum) + public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum) + : base(proc, layerNum, availableUptoLayerNum) { CodeExpr codeExpr = ensures.Condition as CodeExpr; this.ensures = ensures; @@ -216,13 +216,12 @@ namespace Microsoft.Boogie public Dictionary> absyToLayerNums; HashSet auxVars; - private static List FindIntAttributes(QKeyValue kv, string name) + private static List FindLayers(QKeyValue kv) { - Contract.Requires(name != null); HashSet attrs = new HashSet(); for (; kv != null; kv = kv.Next) { - if (kv.Key != name) continue; + if (kv.Key != "layer") continue; foreach (var o in kv.Params) { Expr e = o as Expr; @@ -232,9 +231,9 @@ namespace Microsoft.Boogie attrs.Add(l.asBigNum.ToIntSafe); } } - List phases = attrs.ToList(); - phases.Sort(); - return phases; + List layers = attrs.ToList(); + layers.Sort(); + return layers; } private static MoverType GetMoverType(Ensures e) @@ -260,7 +259,7 @@ namespace Microsoft.Boogie allLayerNums = new HashSet(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allLayerNums.Add(actionInfo.phaseNum); + allLayerNums.Add(actionInfo.createdAtLayerNum); } } return allLayerNums; @@ -273,21 +272,21 @@ namespace Microsoft.Boogie { if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; - int phaseNum = int.MaxValue; + int layerNum = int.MaxValue; int availableUptoLayerNum = int.MaxValue; - List attrs = FindIntAttributes(proc.Attributes, "layer"); + List attrs = FindLayers(proc.Attributes); if (attrs.Count == 1) { - phaseNum = attrs[0]; + layerNum = attrs[0]; } else if (attrs.Count == 2) { - phaseNum = attrs[0]; + layerNum = attrs[0]; availableUptoLayerNum = attrs[1]; } else { - Error(proc, "Incorrect number of phases"); + Error(proc, "Incorrect number of layers"); continue; } foreach (Ensures e in proc.Ensures) @@ -313,7 +312,7 @@ namespace Microsoft.Boogie enclosingImpl = null; base.VisitEnsures(e); canAccessSharedVars = false; - if (maxLayerNum <= phaseNum && availableUptoLayerNum <= minLayerNum) + if (maxLayerNum <= layerNum && availableUptoLayerNum <= minLayerNum) { // ok } @@ -322,11 +321,11 @@ namespace Microsoft.Boogie Error(e, "A variable being accessed is hidden before this action becomes unavailable"); } - procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoLayerNum); + procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, layerNum, availableUptoLayerNum); } if (!procToActionInfo.ContainsKey(proc)) { - procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoLayerNum); + procToActionInfo[proc] = new ActionInfo(proc, layerNum, availableUptoLayerNum); } } if (errorCount > 0) return; @@ -353,25 +352,25 @@ namespace Microsoft.Boogie this.maxLayerNum = -1; foreach (var g in program.GlobalVariables) { - List phaseNums = FindIntAttributes(g.Attributes, "layer"); + List layerNums = FindLayers(g.Attributes); this.introduceLayerNums[g] = 0; this.hideLayerNums[g] = int.MaxValue; - if (phaseNums.Count == 0) + if (layerNums.Count == 0) { // ok } - else if (phaseNums.Count == 1) + else if (layerNums.Count == 1) { - this.hideLayerNums[g] = phaseNums[0]; + this.hideLayerNums[g] = layerNums[0]; } - else if (phaseNums.Count == 2) + else if (layerNums.Count == 2) { - this.introduceLayerNums[g] = phaseNums[0]; - this.hideLayerNums[g] = phaseNums[1]; + this.introduceLayerNums[g] = layerNums[0]; + this.hideLayerNums[g] = layerNums[1]; } else { - Error(g, "Too many phase numbers"); + Error(g, "Too many layer numbers"); } } } @@ -408,7 +407,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node) { - int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum; + int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; if (procToActionInfo.ContainsKey(node.Proc)) { ActionInfo actionInfo = procToActionInfo[node.Proc]; @@ -416,11 +415,11 @@ namespace Microsoft.Boogie { Error(node, "Target of async call cannot be an atomic action"); } - int calleeLayerNum = procToActionInfo[node.Proc].phaseNum; + int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum; if (enclosingProcLayerNum < calleeLayerNum || (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo)) { - Error(node, "The phase of the caller procedure must be greater than the phase of the callee"); + Error(node, "The layer of the caller must be greater than the layer of the callee"); } else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0) { @@ -439,7 +438,7 @@ namespace Microsoft.Boogie } if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum) { - Error(node, "The callee is not available in the phase of the caller procedure"); + Error(node, "The callee is not available in the caller procedure"); } } return base.VisitCallCmd(node); @@ -447,7 +446,7 @@ namespace Microsoft.Boogie public override Cmd VisitParCallCmd(ParCallCmd node) { - int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum; + int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; bool isLeftMover = true; bool isRightMover = true; int maxCalleeLayerNum = 0; @@ -457,9 +456,9 @@ namespace Microsoft.Boogie ActionInfo actionInfo = procToActionInfo[iter.Proc]; isLeftMover = isLeftMover && actionInfo.IsLeftMover; isRightMover = isRightMover && actionInfo.IsRightMover; - if (actionInfo.phaseNum > maxCalleeLayerNum) + if (actionInfo.createdAtLayerNum > maxCalleeLayerNum) { - maxCalleeLayerNum = actionInfo.phaseNum; + maxCalleeLayerNum = actionInfo.createdAtLayerNum; } if (actionInfo is AtomicActionInfo) { @@ -472,7 +471,7 @@ namespace Microsoft.Boogie } if (maxCalleeLayerNum == enclosingProcLayerNum && numAtomicActions > 0) { - Error(node, "If some callee in the parallel call has the same phase as the enclosing procedure, then no callee can be an atomic action"); + Error(node, "If some callee in the parallel call has the same layer as the enclosing procedure, then no callee can be an atomic action"); } return base.VisitParCallCmd(node); } @@ -541,7 +540,7 @@ namespace Microsoft.Boogie } else { - CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.phaseNum); + CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); } return ret; } @@ -553,7 +552,7 @@ namespace Microsoft.Boogie canAccessSharedVars = true; Requires ret = base.VisitRequires(requires); canAccessSharedVars = false; - CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum); + CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); return ret; } @@ -568,32 +567,32 @@ namespace Microsoft.Boogie Cmd ret = base.VisitAssertCmd(node); canAccessAuxVars = false; canAccessSharedVars = false; - CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum); + CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum); return ret; } private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum) { - List attrs = FindIntAttributes(attributes, "layer"); + List attrs = FindLayers(attributes); if (attrs.Count == 0) { - Error(node, "phase not present"); + Error(node, "layer not present"); return; } absyToLayerNums[node] = new HashSet(); - foreach (int phaseNum in attrs) + foreach (int layerNum in attrs) { - if (phaseNum > enclosingProcLayerNum) + if (layerNum > enclosingProcLayerNum) { - Error(node, "The phase cannot be greater than the phase of enclosing procedure"); + Error(node, "The layer cannot be greater than the layer of enclosing procedure"); } - else if (maxLayerNum < phaseNum && phaseNum <= minLayerNum) + else if (maxLayerNum < layerNum && layerNum <= minLayerNum) { - absyToLayerNums[node].Add(phaseNum); + absyToLayerNums[node].Add(layerNum); } else { - Error(node, string.Format("A variable being accessed in this specification is unavailable at phase {0}", phaseNum)); + Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum)); } } } diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 345841aa..8e844ede 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -81,7 +81,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at phase {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); + moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); } } @@ -97,7 +97,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at phase {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); + moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); } } @@ -115,7 +115,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at phase {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); + moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); } } @@ -136,15 +136,15 @@ namespace Microsoft.Boogie { foreach (var impl in moverTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue; + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue; impl.PruneUnreachableBlocks(); Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); - int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum; - foreach (int phaseNum in moverTypeChecker.AllLayerNums) + int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; + foreach (int layerNum in moverTypeChecker.AllLayerNums) { - if (phaseNum > specLayerNum) continue; - YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers); + if (layerNum > specLayerNum) continue; + YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); } } } @@ -227,7 +227,7 @@ namespace Microsoft.Boogie if (callCmd.IsAsync) { ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; - if (currLayerNum <= actionInfo.phaseNum) + if (currLayerNum <= actionInfo.createdAtLayerNum) edgeLabels[edge] = 'L'; else edgeLabels[edge] = 'B'; @@ -240,7 +240,7 @@ namespace Microsoft.Boogie { MoverType moverType; ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; - if (actionInfo.phaseNum >= currLayerNum) + if (actionInfo.createdAtLayerNum >= currLayerNum) { moverType = MoverType.Top; } @@ -280,7 +280,7 @@ namespace Microsoft.Boogie bool isLeftMover = true; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currLayerNum) + if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) { isYield = true; } -- cgit v1.2.3