diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 2e689d592..be517e253 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -67,7 +67,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program) program.AddTopLevelDeclaration(skipImplementation); } program.TopLevelDeclarations.OfType() - .Where(decl => !decl.HasMoverType && decl.RefinedAction == null).ForEach(decl => + .Where(decl => !decl.MoverType.HasValue && decl.RefinedAction == null).ForEach(decl => { decl.RefinedAction = new ActionDeclRef(Token.NoToken, SkipActionDecl.Name) { @@ -358,8 +358,7 @@ public IEnumerable GlobalVariablesAtLayer(int layerNum) return GlobalVariables.Where(v => v.LayerRange.LowerLayer <= layerNum && layerNum < v.LayerRange.UpperLayer); } - public IEnumerable MoverActions => actionDeclToAction.Keys - .Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]); + public IEnumerable MoverActions => actionDeclToAction.Keys.Select(actionDecl => actionDeclToAction[actionDecl]); public IEnumerable AtomicActions => actionDeclToAction.Values; diff --git a/Source/Concurrency/YieldSufficiencyChecker.cs b/Source/Concurrency/YieldSufficiencyChecker.cs index a52b3d3ef..60038636a 100644 --- a/Source/Concurrency/YieldSufficiencyChecker.cs +++ b/Source/Concurrency/YieldSufficiencyChecker.cs @@ -225,7 +225,7 @@ private void AtomicityCheck() } } - private bool IsMoverProcedure => yieldingProc.HasMoverType && yieldingProc.Layer == currLayerNum; + private bool IsMoverProcedure => yieldingProc.MoverType.HasValue && yieldingProc.Layer == currLayerNum; private bool CheckAtomicity(Dictionary> simulationRelation) { @@ -331,12 +331,12 @@ private string CallCmdLabel(CallCmd callCmd) var callee = (YieldProcedureDecl)callCmd.Proc; if (callCmd.IsAsync) { - if (callee.HasMoverType && callee.Layer == currLayerNum) + if (callee.MoverType.HasValue && callee.Layer == currLayerNum) { - return MoverTypeToLabel(callee.MoverType); + return MoverTypeToLabel(callee.MoverType.Value); } - if (!callee.HasMoverType && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC)) + if (!callee.MoverType.HasValue && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC)) { return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType); } @@ -345,12 +345,12 @@ private string CallCmdLabel(CallCmd callCmd) } else { - if (callee.HasMoverType && callee.Layer == currLayerNum) + if (callee.MoverType.HasValue && callee.Layer == currLayerNum) { - return MoverTypeToLabel(callee.MoverType); + return MoverTypeToLabel(callee.MoverType.Value); } - if (!callee.HasMoverType && callee.Layer < currLayerNum) + if (!callee.MoverType.HasValue && callee.Layer < currLayerNum) { return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType); } @@ -400,12 +400,12 @@ private string CallCmdLabelAsync(CallCmd callCmd) var callee = (YieldProcedureDecl)callCmd.Proc; if (callCmd.IsAsync) { - if (callee.HasMoverType && callee.Layer == currLayerNum) + if (callee.MoverType.HasValue && callee.Layer == currLayerNum) { return ModifiesGlobalLabel(callee.Modifies); } - if (!callee.HasMoverType && callee.Layer < currLayerNum) + if (!callee.MoverType.HasValue && callee.Layer < currLayerNum) { if (callCmd.HasAttribute(CivlAttributes.SYNC)) { @@ -428,12 +428,12 @@ private string CallCmdLabelAsync(CallCmd callCmd) } else { - if (callee.HasMoverType && callee.Layer == currLayerNum) + if (callee.MoverType.HasValue && callee.Layer == currLayerNum) { return ModifiesGlobalLabel(callee.Modifies); } - if (!callee.HasMoverType && callee.Layer < currLayerNum) + if (!callee.MoverType.HasValue && callee.Layer < currLayerNum) { return ModifiesGlobalLabel(callee.RefinedActionAtLayer(currLayerNum).ModifiedVars); } diff --git a/Source/Concurrency/YieldingProcChecker.cs b/Source/Concurrency/YieldingProcChecker.cs index b68ac1fe5..2243d18e4 100644 --- a/Source/Concurrency/YieldingProcChecker.cs +++ b/Source/Concurrency/YieldingProcChecker.cs @@ -31,7 +31,7 @@ public static void AddInvariantCheckers(CivlTypeChecker civlTypeChecker, List layerNum || - yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.HasMoverType) + yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.MoverType.HasValue) { duplicator.VisitImplementation(impl); } diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 03c502191..4f554daef 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -52,7 +52,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) var requires = VisitRequiresSeq(node.Requires); var preserves = VisitRequiresSeq(node.Preserves); var ensures = VisitEnsuresSeq(node.Ensures); - if (node.HasMoverType && layerNum == node.Layer && !doRefinementCheck) + if (node.MoverType.HasValue && layerNum == node.Layer && !doRefinementCheck) { requires = requires.Select(req => new Requires(req.tok, true, req.Condition, req.Comment, req.Attributes)).ToList(); preserves = preserves.Select(req => new Requires(req.tok, true, req.Condition, req.Comment, req.Attributes)).ToList(); @@ -70,7 +70,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) requires, [], ensures, - (node.HasMoverType && node.Layer == layerNum + (node.MoverType.HasValue && node.Layer == layerNum ? node.ModifiedVars.Select(Expr.Ident) : civlTypeChecker.GlobalVariables.Select(v => Expr.Ident(v))).ToList() ); @@ -304,7 +304,7 @@ cmd is AssertCmd assertCmd && makeAssume { if (yieldingProc.Layer < layerNum) { - Debug.Assert(!yieldingProc.HasMoverType); + Debug.Assert(!yieldingProc.MoverType.HasValue); if (newCall.HasAttribute(CivlAttributes.SYNC)) { // synchronize the called atomic action @@ -313,14 +313,14 @@ cmd is AssertCmd assertCmd && makeAssume } else { - if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum) + if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum) { // synchronize the called mover procedure AddDuplicateCall(newCall, false); } else if (doRefinementCheck) { - Debug.Assert(!yieldingProc.HasMoverType); + Debug.Assert(!yieldingProc.MoverType.HasValue); } else { @@ -331,7 +331,7 @@ cmd is AssertCmd assertCmd && makeAssume } // handle synchronous calls to yielding procedures - if (yieldingProc.HasMoverType) + if (yieldingProc.MoverType.HasValue) { AddDuplicateCall(newCall, yieldingProc.Layer > layerNum); } @@ -400,8 +400,8 @@ void ProcessPendingCallCmds() { if (callCmd.Proc is YieldProcedureDecl yieldingProc) { - Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.HasMoverType); - if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.HasMoverType) + Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.MoverType.HasValue); + if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.MoverType.HasValue) { ProcessPendingCallCmds(); ProcessCallCmd(callCmd); diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 13fd559f2..0e67724e4 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -354,7 +354,7 @@ private void TransformImpls(Dictionary> implToPrecondi // For mover procedures, simply add disjointness assumptions at the beginning of the first block. linearPermissionInstrumentation.AddDisjointnessAndWellFormedAssumptions(impl); var yieldingProc = GetYieldingProc(impl); - if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum) + if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum) { impl.Blocks[0].Cmds.InsertRange(0, linearPermissionInstrumentation.DisjointnessAndWellFormedAssumeCmds(impl, true)); } diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 915ce10cf..5cfcf4b67 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2721,7 +2721,7 @@ void TypecheckSpec(List layers, Action f) { var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld; if (this is YieldProcedureDecl yieldProcedureDecl && - (!yieldProcedureDecl.HasMoverType || layers.Any(layer => layer < yieldProcedureDecl.Layer))) + (!yieldProcedureDecl.MoverType.HasValue || layers.Any(layer => layer < yieldProcedureDecl.Layer))) { tc.GlobalAccessOnlyInOld = true; } @@ -2736,9 +2736,9 @@ void TypecheckSpec(List layers, Action f) foreach (Requires e in Preserves) { if (this is YieldProcedureDecl yieldProcedureDecl && - (!yieldProcedureDecl.HasMoverType || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer))) + (!yieldProcedureDecl.MoverType.HasValue || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer))) { - if (yieldProcedureDecl.HasMoverType) + if (yieldProcedureDecl.MoverType.HasValue) { tc.Error(e, $"only layer {yieldProcedureDecl.Layer} allowed for preserves clause"); } @@ -2864,7 +2864,6 @@ public enum MoverType Right, Left, Both, - None } public class ActionDecl : Procedure @@ -2922,14 +2921,6 @@ public override void Resolve(ResolutionContext rc) if (RefinedAction != null) { RefinedAction.Resolve(rc); - if (!HasMoverType) - { - MoverType = MoverType.Atomic; - } - if (RefinedAction.ActionDecl is { HasMoverType: false }) - { - RefinedAction.ActionDecl.MoverType = MoverType.Atomic; - } } } @@ -3025,8 +3016,6 @@ public IEnumerable ActionDeclRefs() public bool HasPreconditions => Requires.Count > 0 || YieldRequires.Count > 0; - public bool HasMoverType => MoverType != MoverType.None; - public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both; public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both; @@ -3051,7 +3040,7 @@ public YieldingLoop(int layer, List yieldInvariants) public class YieldProcedureDecl : Procedure { - public MoverType MoverType; + public MoverType? MoverType; public List YieldRequires; public List YieldPreserves; public List YieldEnsures; @@ -3061,7 +3050,7 @@ public class YieldProcedureDecl : Procedure public HashSet VisibleFormals; // set during resolution public Dictionary YieldingLoops; // empty initially, filled up during type checking - public YieldProcedureDecl(IToken tok, string name, MoverType moverType, List inParams, + public YieldProcedureDecl(IToken tok, string name, MoverType? moverType, List inParams, List outParams, List requires, List preserves, List ensures, List modifies, List yieldRequires, List yieldPreserves, List yieldEnsures, @@ -3117,7 +3106,7 @@ public override void Resolve(ResolutionContext rc) rc.StateMode = oldStateMode; rc.Proc = null; - if (!HasMoverType) + if (!MoverType.HasValue) { VisibleFormals = RefinedAction == null ? new HashSet() @@ -3128,13 +3117,9 @@ public override void Resolve(ResolutionContext rc) if (RefinedAction != null) { RefinedAction.Resolve(rc); - if (RefinedAction.ActionDecl is { HasMoverType: false }) - { - RefinedAction.ActionDecl.MoverType = MoverType.Atomic; - } } - if (!HasMoverType) + if (!MoverType.HasValue) { if (Modifies.Any()) { @@ -3160,7 +3145,7 @@ public override void Typecheck(TypecheckingContext tc) } } - if (HasMoverType) + if (MoverType.HasValue) { Modifies.Where(ie => !ie.Decl.LayerRange.Contains(Layer)).ForEach(ie => { @@ -3219,12 +3204,10 @@ public IEnumerable CallCmds() { return YieldEnsures.Union(YieldPreserves).Union(YieldRequires); } - - public bool HasMoverType => MoverType != MoverType.None; - public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both; + public bool IsRightMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Right || MoverType.Value == Boogie.MoverType.Both); - public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both; + public bool IsLeftMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Left || MoverType.Value == Boogie.MoverType.Both); public ActionDecl RefinedActionAtLayer(int layer) { diff --git a/Source/Core/AST/Commands/AbsyCmd.cs b/Source/Core/AST/Commands/AbsyCmd.cs index 363544467..238620e14 100644 --- a/Source/Core/AST/Commands/AbsyCmd.cs +++ b/Source/Core/AST/Commands/AbsyCmd.cs @@ -1555,7 +1555,7 @@ public override void Typecheck(TypecheckingContext tc) } var callerDecl = (YieldProcedureDecl)tc.Proc; - if (callerDecl.HasMoverType) + if (callerDecl.MoverType.HasValue) { return; } diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs index e3e84687a..b24bfffb1 100644 --- a/Source/Core/AST/Commands/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -312,7 +312,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD tc.Error(this, "layer of callee must not be more than layer of caller"); return; } - if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null) + if (!calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction == null) { return; } @@ -323,7 +323,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD return; } // call is synchronous or synchronized - if (!calleeDecl.HasMoverType) + if (!calleeDecl.MoverType.HasValue) { Debug.Assert(calleeDecl.RefinedAction != null); if (callerDecl.Layer > calleeDecl.Layer) @@ -340,7 +340,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD } else // callerDecl.Layer == calleeDecl.Layer { - if (callerDecl.HasMoverType) + if (callerDecl.MoverType.HasValue) { tc.Error(this, "caller must not be a mover procedure"); } @@ -350,7 +350,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD } } } - else // calleeDecl.HasMoverType + else // calleeDecl.MoverType.HasValue { if (callerDecl.Layer > calleeDecl.Layer) { @@ -372,7 +372,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD { tc.Error(this, "layer of callee must not be more than layer of caller"); } - else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.HasMoverType) + else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.MoverType.HasValue) { tc.Error(this, "layer of callee must be less than layer of caller"); } @@ -627,7 +627,7 @@ private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable call case YieldProcedureDecl yieldProcedureDecl: { formalLayerRange = calleeFormal.LayerRange; - if (!yieldProcedureDecl.HasMoverType && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal)) + if (!yieldProcedureDecl.MoverType.HasValue && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal)) { formalLayerRange = new LayerRange(formalLayerRange.LowerLayer, callerDecl.Layer); } diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs index 344299475..c738023e6 100644 --- a/Source/Core/Analysis/ModSetCollector.cs +++ b/Source/Core/Analysis/ModSetCollector.cs @@ -23,7 +23,7 @@ public void CollectModifies(Program program) { var implementedProcs = new HashSet(program.Implementations.Where(impl => impl.Proc != null).Select(impl => impl.Proc)); program.Procedures.Where(proc => - proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.HasMoverType)) + proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.MoverType.HasValue)) .ForEach(proc => { modSets.Add(proc, new HashSet()); @@ -138,7 +138,7 @@ public override Cmd VisitCallCmd(CallCmd callCmd) Procedure callee = callCmd.Proc; Debug.Assert(callee != null); if (enclosingProc is YieldProcedureDecl callerDecl && - callee is YieldProcedureDecl calleeDecl && !calleeDecl.HasMoverType && calleeDecl.RefinedAction != null) + callee is YieldProcedureDecl calleeDecl && !calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction != null) { callee = calleeDecl.RefinedActionAtLayer(callerDecl.Layer); } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 7b983a22d..075edbfae 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -662,7 +662,7 @@ Pure ActionDecl = (. IToken name = null; - MoverType moverType = MoverType.None; + MoverType? moverType = null; List ins, outs = new List(); List mods = new List(); ActionDeclRef refinedAction = null; @@ -691,17 +691,13 @@ ActionDecl SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List ins, List outs.> = - (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List locals; StmtList stmtList; .) + (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType? moverType = MoverType.Atomic; List locals; StmtList stmtList; .) "refines" { Attribute } ( @@ -739,7 +735,7 @@ SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name inParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); var outParams = new List(outs); outParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); - var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), + var actionDecl = new ActionDecl(tok, actionName, moverType.Value, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), false, null, new List(), new List(), new List(), new List(), akv); Pgm.AddTopLevelDeclaration(actionDecl); @@ -774,7 +770,7 @@ SpecAction<.ref ActionDeclRef refinedAction, List mods, List +MoverQualifier = ( "left" (. moverType = MoverType.Left; .) | "right" (. moverType = MoverType.Right; .) @@ -786,7 +782,7 @@ MoverQualifier YieldProcedureDecl = (. IToken name; List ins, outs = new List(); - MoverType moverType = MoverType.None; + MoverType? moverType = null; ActionDeclRef refinedAction = null; List pre = new List(); List preserves = new List(); @@ -800,7 +796,7 @@ YieldProcedureDecl QKeyValue kv = null; impl = null; .) - [ MoverQualifier ] + [ MoverQualifier ] "procedure" { Attribute } Ident diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 328ac3e47..0ca718690 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -592,7 +592,7 @@ void InvariantDecl(out YieldInvariantDecl yieldInvariant) { void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl) { IToken name; List ins, outs = new List(); - MoverType moverType = MoverType.None; + MoverType? moverType = null; ActionDeclRef refinedAction = null; List pre = new List(); List preserves = new List(); @@ -676,7 +676,7 @@ void Procedure(bool isPure, out Procedure proc, out /*maybe null*/ Implementatio void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl) { IToken name = null; - MoverType moverType = MoverType.None; + MoverType? moverType = null; List ins, outs = new List(); List mods = new List(); ActionDeclRef refinedAction = null; @@ -716,17 +716,13 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone()); } else SynErr(130); - if (isPure) { - if (moverType == MoverType.None) - { - moverType = MoverType.Both; - } - else - { - this.SemErr("mover type unnecessary for pure action since it is a both mover"); - } + if (isPure && moverType.HasValue) { + this.SemErr("mover type unnecessary for pure action since it is a both mover"); + } + if (!moverType.HasValue) { + moverType = isPure ? MoverType.Both : MoverType.Atomic; } - actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, refinedAction, requires, mods, yieldRequires, asserts, kv); + actionDecl = new ActionDecl(name, name.val, moverType.Value, ins, outs, isPure, refinedAction, requires, mods, yieldRequires, asserts, kv); } @@ -1120,7 +1116,7 @@ void Invariant(List invariants) { invariants.Add(new Requires(tok, false, e, null, kv)); } - void MoverQualifier(ref MoverType moverType) { + void MoverQualifier(ref MoverType? moverType) { if (la.kind == 41) { Get(); moverType = MoverType.Left; @@ -1174,7 +1170,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { } void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List ins, List outs) { - IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List locals; StmtList stmtList; + IToken tok, m; QKeyValue kv = null, akv = null; MoverType? moverType = MoverType.Atomic; List locals; StmtList stmtList; Expect(40); while (la.kind == 26) { Attribute(ref kv); @@ -1196,7 +1192,7 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken inParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); var outParams = new List(outs); outParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); - var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), + var actionDecl = new ActionDecl(tok, actionName, moverType.Value, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), false, null, new List(), new List(), new List(), new List(), akv); Pgm.AddTopLevelDeclaration(actionDecl); diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl index accb3ca57..527af3916 100644 --- a/Test/civl/large-samples/cache-coherence.bpl +++ b/Test/civl/large-samples/cache-coherence.bpl @@ -412,7 +412,7 @@ refines left action {:layer 2} _ { assert (forall {:pool "X"} j: CacheId :: {:add_to_pool "X", j} (var line := cache[j][ca]; line->ma == ma ==> line->state == Invalid() || line->state == Shared())); // this assertion accompanies the relaxation in cache_read#1 to allow cache_invalidate_shd#1 to commute to the left of cache_read#1 assert cache[i][ca]->value == absMem[ma]; - call primitive_cache_invalidate_shd(i, ma, s); + call cache := primitive_cache_invalidate_shd(cache, i, ma, s); } { call cache_invalidate_shd#0(i, ma, s); @@ -422,7 +422,7 @@ yield procedure {:layer 1} cache_invalidate_exc#1(i: CacheId, ma: MemAddr, s: St refines atomic action {:layer 2} _ { assert dp == WholeDirPermission(ma); assume {:add_to_pool "DirPermission", One(DirPermission(i0, ma))} true; - call value := primitive_cache_invalidate_exc(i, ma, s); + call cache, value := primitive_cache_invalidate_exc(cache, i, ma, s); } { call value := cache_invalidate_exc#0(i, ma, s); @@ -544,10 +544,11 @@ refines atomic action {:layer 1} _ { yield procedure {:layer 0} cache_invalidate_shd#0(i: CacheId, ma: MemAddr, s: State); refines atomic action {:layer 1} _ { - call primitive_cache_invalidate_shd(i, ma, s); + call cache := primitive_cache_invalidate_shd(cache, i, ma, s); } -action {:layer 1,2} primitive_cache_invalidate_shd(i: CacheId, ma: MemAddr, s: State) +pure action primitive_cache_invalidate_shd(cache: [CacheId][CacheAddr]CacheLine, i: CacheId, ma: MemAddr, s: State) + returns (cache': [CacheId][CacheAddr]CacheLine) { var ca: CacheAddr; var line: CacheLine; @@ -557,15 +558,17 @@ action {:layer 1,2} primitive_cache_invalidate_shd(i: CacheId, ma: MemAddr, s: S line := cache[i][ca]; assert line->state == Shared(); assert line->ma == ma; - cache[i][ca]->state := s; + cache' := cache; + cache'[i][ca]->state := s; } yield procedure {:layer 0} cache_invalidate_exc#0(i: CacheId, ma: MemAddr, s: State) returns (value: Value); refines atomic action {:layer 1} _ { - call value := primitive_cache_invalidate_exc(i, ma, s); + call cache, value := primitive_cache_invalidate_exc(cache, i, ma, s); } -action {:layer 1,2} primitive_cache_invalidate_exc(i: CacheId, ma: MemAddr, s: State) returns (value: Value) +pure action primitive_cache_invalidate_exc(cache: [CacheId][CacheAddr]CacheLine, i: CacheId, ma: MemAddr, s: State) + returns (cache': [CacheId][CacheAddr]CacheLine, value: Value) { var ca: CacheAddr; var line: CacheLine; @@ -576,7 +579,8 @@ action {:layer 1,2} primitive_cache_invalidate_exc(i: CacheId, ma: MemAddr, s: S assert line->state == Exclusive() || line->state == Modified(); assert line->ma == ma; value := line->value; - cache[i][ca]->state := s; + cache' := cache; + cache'[i][ca]->state := s; } /// Directory