Skip to content

Commit 43533fd

Browse files
shazqadeershazqadeer
authored
[Civl] Fixes issue 1094 (#1095)
Fixes issue #1094
1 parent 23f70c0 commit 43533fd

File tree

12 files changed

+77
-99
lines changed

12 files changed

+77
-99
lines changed

‎Source/Concurrency/CivlTypeChecker.cs‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
6767
program.AddTopLevelDeclaration(skipImplementation);
6868
}
6969
program.TopLevelDeclarations.OfType<YieldProcedureDecl>()
70-
.Where(decl => !decl.HasMoverType && decl.RefinedAction == null).ForEach(decl =>
70+
.Where(decl => !decl.MoverType.HasValue && decl.RefinedAction == null).ForEach(decl =>
7171
{
7272
decl.RefinedAction = new ActionDeclRef(Token.NoToken, SkipActionDecl.Name)
7373
{
@@ -358,8 +358,7 @@ public IEnumerable<Variable> GlobalVariablesAtLayer(int layerNum)
358358
return GlobalVariables.Where(v => v.LayerRange.LowerLayer <= layerNum && layerNum < v.LayerRange.UpperLayer);
359359
}
360360

361-
public IEnumerable<Action> MoverActions => actionDeclToAction.Keys
362-
.Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]);
361+
public IEnumerable<Action> MoverActions => actionDeclToAction.Keys.Select(actionDecl => actionDeclToAction[actionDecl]);
363362

364363
public IEnumerable<Action> AtomicActions => actionDeclToAction.Values;
365364

‎Source/Concurrency/YieldSufficiencyChecker.cs‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,7 @@ private void AtomicityCheck()
225225
}
226226
}
227227

228-
private bool IsMoverProcedure => yieldingProc.HasMoverType && yieldingProc.Layer == currLayerNum;
228+
private bool IsMoverProcedure => yieldingProc.MoverType.HasValue && yieldingProc.Layer == currLayerNum;
229229

230230
private bool CheckAtomicity(Dictionary<Absy, HashSet<int>> simulationRelation)
231231
{
@@ -331,12 +331,12 @@ private string CallCmdLabel(CallCmd callCmd)
331331
var callee = (YieldProcedureDecl)callCmd.Proc;
332332
if (callCmd.IsAsync)
333333
{
334-
if (callee.HasMoverType && callee.Layer == currLayerNum)
334+
if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
335335
{
336-
return MoverTypeToLabel(callee.MoverType);
336+
return MoverTypeToLabel(callee.MoverType.Value);
337337
}
338338

339-
if (!callee.HasMoverType && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC))
339+
if (!callee.MoverType.HasValue && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC))
340340
{
341341
return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType);
342342
}
@@ -345,12 +345,12 @@ private string CallCmdLabel(CallCmd callCmd)
345345
}
346346
else
347347
{
348-
if (callee.HasMoverType && callee.Layer == currLayerNum)
348+
if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
349349
{
350-
return MoverTypeToLabel(callee.MoverType);
350+
return MoverTypeToLabel(callee.MoverType.Value);
351351
}
352352

353-
if (!callee.HasMoverType && callee.Layer < currLayerNum)
353+
if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
354354
{
355355
return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType);
356356
}
@@ -400,12 +400,12 @@ private string CallCmdLabelAsync(CallCmd callCmd)
400400
var callee = (YieldProcedureDecl)callCmd.Proc;
401401
if (callCmd.IsAsync)
402402
{
403-
if (callee.HasMoverType && callee.Layer == currLayerNum)
403+
if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
404404
{
405405
return ModifiesGlobalLabel(callee.Modifies);
406406
}
407407

408-
if (!callee.HasMoverType && callee.Layer < currLayerNum)
408+
if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
409409
{
410410
if (callCmd.HasAttribute(CivlAttributes.SYNC))
411411
{
@@ -428,12 +428,12 @@ private string CallCmdLabelAsync(CallCmd callCmd)
428428
}
429429
else
430430
{
431-
if (callee.HasMoverType && callee.Layer == currLayerNum)
431+
if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
432432
{
433433
return ModifiesGlobalLabel(callee.Modifies);
434434
}
435435

436-
if (!callee.HasMoverType && callee.Layer < currLayerNum)
436+
if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
437437
{
438438
return ModifiesGlobalLabel(callee.RefinedActionAtLayer(currLayerNum).ModifiedVars);
439439
}

‎Source/Concurrency/YieldingProcChecker.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ public static void AddInvariantCheckers(CivlTypeChecker civlTypeChecker, List<De
3131
{
3232
var yieldProcedureDecl = (YieldProcedureDecl)impl.Proc;
3333
if (yieldProcedureDecl.Layer > layerNum ||
34-
yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.HasMoverType)
34+
yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.MoverType.HasValue)
3535
{
3636
duplicator.VisitImplementation(impl);
3737
}

‎Source/Concurrency/YieldingProcDuplicator.cs‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)
5252
var requires = VisitRequiresSeq(node.Requires);
5353
var preserves = VisitRequiresSeq(node.Preserves);
5454
var ensures = VisitEnsuresSeq(node.Ensures);
55-
if (node.HasMoverType && layerNum == node.Layer && !doRefinementCheck)
55+
if (node.MoverType.HasValue && layerNum == node.Layer && !doRefinementCheck)
5656
{
5757
requires = requires.Select(req => new Requires(req.tok, true, req.Condition, req.Comment, req.Attributes)).ToList();
5858
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)
7070
requires,
7171
[],
7272
ensures,
73-
(node.HasMoverType && node.Layer == layerNum
73+
(node.MoverType.HasValue && node.Layer == layerNum
7474
? node.ModifiedVars.Select(Expr.Ident)
7575
: civlTypeChecker.GlobalVariables.Select(v => Expr.Ident(v))).ToList()
7676
);
@@ -304,7 +304,7 @@ cmd is AssertCmd assertCmd && makeAssume
304304
{
305305
if (yieldingProc.Layer < layerNum)
306306
{
307-
Debug.Assert(!yieldingProc.HasMoverType);
307+
Debug.Assert(!yieldingProc.MoverType.HasValue);
308308
if (newCall.HasAttribute(CivlAttributes.SYNC))
309309
{
310310
// synchronize the called atomic action
@@ -313,14 +313,14 @@ cmd is AssertCmd assertCmd && makeAssume
313313
}
314314
else
315315
{
316-
if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum)
316+
if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum)
317317
{
318318
// synchronize the called mover procedure
319319
AddDuplicateCall(newCall, false);
320320
}
321321
else if (doRefinementCheck)
322322
{
323-
Debug.Assert(!yieldingProc.HasMoverType);
323+
Debug.Assert(!yieldingProc.MoverType.HasValue);
324324
}
325325
else
326326
{
@@ -331,7 +331,7 @@ cmd is AssertCmd assertCmd && makeAssume
331331
}
332332

333333
// handle synchronous calls to yielding procedures
334-
if (yieldingProc.HasMoverType)
334+
if (yieldingProc.MoverType.HasValue)
335335
{
336336
AddDuplicateCall(newCall, yieldingProc.Layer > layerNum);
337337
}
@@ -400,8 +400,8 @@ void ProcessPendingCallCmds()
400400
{
401401
if (callCmd.Proc is YieldProcedureDecl yieldingProc)
402402
{
403-
Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.HasMoverType);
404-
if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.HasMoverType)
403+
Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.MoverType.HasValue);
404+
if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.MoverType.HasValue)
405405
{
406406
ProcessPendingCallCmds();
407407
ProcessCallCmd(callCmd);

‎Source/Concurrency/YieldingProcInstrumentation.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,7 @@ private void TransformImpls(Dictionary<Implementation, List<Cmd>> implToPrecondi
354354
// For mover procedures, simply add disjointness assumptions at the beginning of the first block.
355355
linearPermissionInstrumentation.AddDisjointnessAndWellFormedAssumptions(impl);
356356
var yieldingProc = GetYieldingProc(impl);
357-
if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum)
357+
if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum)
358358
{
359359
impl.Blocks[0].Cmds.InsertRange(0, linearPermissionInstrumentation.DisjointnessAndWellFormedAssumeCmds(impl, true));
360360
}

‎Source/Core/AST/Absy.cs‎

Lines changed: 10 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -2721,7 +2721,7 @@ void TypecheckSpec(List<int> layers, Action<TypecheckingContext> f)
27212721
{
27222722
var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
27232723
if (this is YieldProcedureDecl yieldProcedureDecl &&
2724-
(!yieldProcedureDecl.HasMoverType || layers.Any(layer => layer < yieldProcedureDecl.Layer)))
2724+
(!yieldProcedureDecl.MoverType.HasValue || layers.Any(layer => layer < yieldProcedureDecl.Layer)))
27252725
{
27262726
tc.GlobalAccessOnlyInOld = true;
27272727
}
@@ -2736,9 +2736,9 @@ void TypecheckSpec(List<int> layers, Action<TypecheckingContext> f)
27362736
foreach (Requires e in Preserves)
27372737
{
27382738
if (this is YieldProcedureDecl yieldProcedureDecl &&
2739-
(!yieldProcedureDecl.HasMoverType || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer)))
2739+
(!yieldProcedureDecl.MoverType.HasValue || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer)))
27402740
{
2741-
if (yieldProcedureDecl.HasMoverType)
2741+
if (yieldProcedureDecl.MoverType.HasValue)
27422742
{
27432743
tc.Error(e, $"only layer {yieldProcedureDecl.Layer} allowed for preserves clause");
27442744
}
@@ -2864,7 +2864,6 @@ public enum MoverType
28642864
Right,
28652865
Left,
28662866
Both,
2867-
None
28682867
}
28692868

28702869
public class ActionDecl : Procedure
@@ -2922,14 +2921,6 @@ public override void Resolve(ResolutionContext rc)
29222921
if (RefinedAction != null)
29232922
{
29242923
RefinedAction.Resolve(rc);
2925-
if (!HasMoverType)
2926-
{
2927-
MoverType = MoverType.Atomic;
2928-
}
2929-
if (RefinedAction.ActionDecl is { HasMoverType: false })
2930-
{
2931-
RefinedAction.ActionDecl.MoverType = MoverType.Atomic;
2932-
}
29332924
}
29342925
}
29352926

@@ -3025,8 +3016,6 @@ public IEnumerable<ActionDeclRef> ActionDeclRefs()
30253016

30263017
public bool HasPreconditions => Requires.Count > 0 || YieldRequires.Count > 0;
30273018

3028-
public bool HasMoverType => MoverType != MoverType.None;
3029-
30303019
public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both;
30313020

30323021
public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both;
@@ -3051,7 +3040,7 @@ public YieldingLoop(int layer, List<CallCmd> yieldInvariants)
30513040

30523041
public class YieldProcedureDecl : Procedure
30533042
{
3054-
public MoverType MoverType;
3043+
public MoverType? MoverType;
30553044
public List<CallCmd> YieldRequires;
30563045
public List<CallCmd> YieldPreserves;
30573046
public List<CallCmd> YieldEnsures;
@@ -3061,7 +3050,7 @@ public class YieldProcedureDecl : Procedure
30613050
public HashSet<Variable> VisibleFormals; // set during resolution
30623051
public Dictionary<Block, YieldingLoop> YieldingLoops; // empty initially, filled up during type checking
30633052

3064-
public YieldProcedureDecl(IToken tok, string name, MoverType moverType, List<Variable> inParams,
3053+
public YieldProcedureDecl(IToken tok, string name, MoverType? moverType, List<Variable> inParams,
30653054
List<Variable> outParams,
30663055
List<Requires> requires, List<Requires> preserves, List<Ensures> ensures, List<IdentifierExpr> modifies,
30673056
List<CallCmd> yieldRequires, List<CallCmd> yieldPreserves, List<CallCmd> yieldEnsures,
@@ -3117,7 +3106,7 @@ public override void Resolve(ResolutionContext rc)
31173106
rc.StateMode = oldStateMode;
31183107
rc.Proc = null;
31193108

3120-
if (!HasMoverType)
3109+
if (!MoverType.HasValue)
31213110
{
31223111
VisibleFormals = RefinedAction == null
31233112
? new HashSet<Variable>()
@@ -3128,13 +3117,9 @@ public override void Resolve(ResolutionContext rc)
31283117
if (RefinedAction != null)
31293118
{
31303119
RefinedAction.Resolve(rc);
3131-
if (RefinedAction.ActionDecl is { HasMoverType: false })
3132-
{
3133-
RefinedAction.ActionDecl.MoverType = MoverType.Atomic;
3134-
}
31353120
}
31363121

3137-
if (!HasMoverType)
3122+
if (!MoverType.HasValue)
31383123
{
31393124
if (Modifies.Any())
31403125
{
@@ -3160,7 +3145,7 @@ public override void Typecheck(TypecheckingContext tc)
31603145
}
31613146
}
31623147

3163-
if (HasMoverType)
3148+
if (MoverType.HasValue)
31643149
{
31653150
Modifies.Where(ie => !ie.Decl.LayerRange.Contains(Layer)).ForEach(ie =>
31663151
{
@@ -3219,12 +3204,10 @@ public IEnumerable<CallCmd> CallCmds()
32193204
{
32203205
return YieldEnsures.Union(YieldPreserves).Union(YieldRequires);
32213206
}
3222-
3223-
public bool HasMoverType => MoverType != MoverType.None;
32243207

3225-
public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both;
3208+
public bool IsRightMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Right || MoverType.Value == Boogie.MoverType.Both);
32263209

3227-
public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both;
3210+
public bool IsLeftMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Left || MoverType.Value == Boogie.MoverType.Both);
32283211

32293212
public ActionDecl RefinedActionAtLayer(int layer)
32303213
{

‎Source/Core/AST/Commands/AbsyCmd.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1555,7 +1555,7 @@ public override void Typecheck(TypecheckingContext tc)
15551555
}
15561556

15571557
var callerDecl = (YieldProcedureDecl)tc.Proc;
1558-
if (callerDecl.HasMoverType)
1558+
if (callerDecl.MoverType.HasValue)
15591559
{
15601560
return;
15611561
}

‎Source/Core/AST/Commands/CallCmd.cs‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -312,7 +312,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
312312
tc.Error(this, "layer of callee must not be more than layer of caller");
313313
return;
314314
}
315-
if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null)
315+
if (!calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction == null)
316316
{
317317
return;
318318
}
@@ -323,7 +323,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
323323
return;
324324
}
325325
// call is synchronous or synchronized
326-
if (!calleeDecl.HasMoverType)
326+
if (!calleeDecl.MoverType.HasValue)
327327
{
328328
Debug.Assert(calleeDecl.RefinedAction != null);
329329
if (callerDecl.Layer > calleeDecl.Layer)
@@ -340,7 +340,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
340340
}
341341
else // callerDecl.Layer == calleeDecl.Layer
342342
{
343-
if (callerDecl.HasMoverType)
343+
if (callerDecl.MoverType.HasValue)
344344
{
345345
tc.Error(this, "caller must not be a mover procedure");
346346
}
@@ -350,7 +350,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
350350
}
351351
}
352352
}
353-
else // calleeDecl.HasMoverType
353+
else // calleeDecl.MoverType.HasValue
354354
{
355355
if (callerDecl.Layer > calleeDecl.Layer)
356356
{
@@ -372,7 +372,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
372372
{
373373
tc.Error(this, "layer of callee must not be more than layer of caller");
374374
}
375-
else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.HasMoverType)
375+
else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.MoverType.HasValue)
376376
{
377377
tc.Error(this, "layer of callee must be less than layer of caller");
378378
}
@@ -627,7 +627,7 @@ private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable call
627627
case YieldProcedureDecl yieldProcedureDecl:
628628
{
629629
formalLayerRange = calleeFormal.LayerRange;
630-
if (!yieldProcedureDecl.HasMoverType && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal))
630+
if (!yieldProcedureDecl.MoverType.HasValue && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal))
631631
{
632632
formalLayerRange = new LayerRange(formalLayerRange.LowerLayer, callerDecl.Layer);
633633
}

‎Source/Core/Analysis/ModSetCollector.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ public void CollectModifies(Program program)
2323
{
2424
var implementedProcs = new HashSet<Procedure>(program.Implementations.Where(impl => impl.Proc != null).Select(impl => impl.Proc));
2525
program.Procedures.Where(proc =>
26-
proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.HasMoverType))
26+
proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.MoverType.HasValue))
2727
.ForEach(proc =>
2828
{
2929
modSets.Add(proc, new HashSet<Variable>());
@@ -138,7 +138,7 @@ public override Cmd VisitCallCmd(CallCmd callCmd)
138138
Procedure callee = callCmd.Proc;
139139
Debug.Assert(callee != null);
140140
if (enclosingProc is YieldProcedureDecl callerDecl &&
141-
callee is YieldProcedureDecl calleeDecl && !calleeDecl.HasMoverType && calleeDecl.RefinedAction != null)
141+
callee is YieldProcedureDecl calleeDecl && !calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction != null)
142142
{
143143
callee = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
144144
}

0 commit comments

Comments
 (0)