Skip to content

Commit 68de624

Browse files
shazqadeershazqadeer
committed
second commit
1 parent caa8c0c commit 68de624

File tree

3 files changed

+27
-30
lines changed

3 files changed

+27
-30
lines changed

‎Source/Concurrency/YieldingProcChecker.cs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,6 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration
7070
}
7171
decls.AddRange(duplicator.Collect());
7272
}
73-
7473
}
7574
}
7675
}

‎Source/Concurrency/YieldingProcDuplicator.cs‎

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,13 @@ public class YieldingProcDuplicator : Duplicator
2323

2424
private LinearRewriter linearRewriter;
2525

26-
private ConcurrencyOptions Options => civlTypeChecker.Options;
26+
private bool doRefinementCheck;
2727

28-
private bool forRefinementCheck;
29-
30-
public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, int layerNum, bool forRefinementCheck)
28+
public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, int layerNum, bool doRefinementCheck)
3129
{
3230
this.civlTypeChecker = civlTypeChecker;
3331
this.layerNum = layerNum;
34-
this.forRefinementCheck = forRefinementCheck;
32+
this.doRefinementCheck = doRefinementCheck;
3533
this.procToDuplicate = new Dictionary<Procedure, Procedure>();
3634
this.absyMap = new AbsyMap();
3735
this.asyncCallPreconditionCheckers = new Dictionary<string, Procedure>();
@@ -46,7 +44,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)
4644
{
4745
Debug.Assert(layerNum <= node.Layer);
4846
var procName = civlTypeChecker.AddNamePrefix($"{node.Name}_{layerNum}");
49-
if (forRefinementCheck)
47+
if (doRefinementCheck)
5048
{
5149
procName = civlTypeChecker.AddNamePrefix($"{node.Name}_Refine_{layerNum}");
5250
}
@@ -162,7 +160,7 @@ public override Implementation VisitImplementation(Implementation impl)
162160

163161
newImpl.LocVars.AddRange(returnedPAs.Values);
164162

165-
if (!enclosingYieldingProc.HasMoverType && RefinedAction.HasPendingAsyncs && forRefinementCheck)
163+
if (!enclosingYieldingProc.HasMoverType && RefinedAction.HasPendingAsyncs && doRefinementCheck)
166164
{
167165
var assumeExpr = EmptyPendingAsyncMultisetExpr(CollectedPAs, RefinedAction.PendingAsyncs);
168166
newImpl.LocVars.AddRange(civlTypeChecker.PendingAsyncCollectors(impl).Values.Except(impl.LocVars));
@@ -183,7 +181,7 @@ public override Block VisitBlock(Block node)
183181
public override Cmd VisitAssertCmd(AssertCmd node)
184182
{
185183
var assertCmd = (AssertCmd)base.VisitAssertCmd(node);
186-
if (forRefinementCheck && node.Layers.Contains(layerNum))
184+
if (doRefinementCheck && node.Layers.Contains(layerNum))
187185
{
188186
return new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
189187
}
@@ -286,7 +284,7 @@ private void ProcessCallCmd(CallCmd newCall)
286284
// synchronize the called atomic action
287285
AddActionCall(newCall, yieldingProc);
288286
}
289-
else if (forRefinementCheck)
287+
else if (doRefinementCheck)
290288
{
291289
AddPendingAsync(newCall, yieldingProc);
292290
}
@@ -298,7 +296,7 @@ private void ProcessCallCmd(CallCmd newCall)
298296
// synchronize the called mover procedure
299297
AddDuplicateCall(newCall, false);
300298
}
301-
else if (forRefinementCheck)
299+
else if (doRefinementCheck)
302300
{
303301
Debug.Assert(!yieldingProc.HasMoverType);
304302
AddPendingAsync(newCall, yieldingProc);
@@ -324,7 +322,7 @@ private void ProcessCallCmd(CallCmd newCall)
324322
}
325323
else
326324
{
327-
if (forRefinementCheck && yieldingProc.RefinedAction.ActionDecl != civlTypeChecker.SkipActionDecl)
325+
if (doRefinementCheck && yieldingProc.RefinedAction.ActionDecl != civlTypeChecker.SkipActionDecl)
328326
{
329327
var parCallCmdBefore = new ParCallCmd(newCall.tok, new List<CallCmd> { });
330328
absyMap[parCallCmdBefore] = absyMap[newCall];
@@ -361,7 +359,7 @@ void ProcessPendingCallCmds()
361359
return;
362360
}
363361
var callCmd = callCmds.Find(cmd => cmd.Proc is YieldProcedureDecl yieldingProc && layerNum == yieldingProc.Layer);
364-
if (forRefinementCheck && callCmd != null)
362+
if (doRefinementCheck && callCmd != null)
365363
{
366364
callCmds.Remove(callCmd);
367365
AddParallelCall();
@@ -441,7 +439,7 @@ private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
441439
{
442440
var calleeRefinedAction = PrepareNewCall(newCall, calleeActionProc);
443441
InjectPreconditions(calleeRefinedAction, newCall);
444-
InjectGate(calleeRefinedAction, newCall, !forRefinementCheck);
442+
InjectGate(calleeRefinedAction, newCall, !doRefinementCheck);
445443
newCmdSeq.Add(newCall);
446444

447445
if (calleeRefinedAction.HasPendingAsyncs)
@@ -506,7 +504,7 @@ private void CollectReturnedPendingAsyncs(CallCmd newCall, Action calleeRefinedA
506504
{
507505
// Inject pending async collection
508506
newCall.Outs.AddRange(calleeRefinedAction.PendingAsyncs.Select(decl => Expr.Ident(ReturnedPAs(decl.PendingAsyncType))));
509-
if (!forRefinementCheck)
507+
if (!doRefinementCheck)
510508
{
511509
return;
512510
}
@@ -617,7 +615,7 @@ public List<Declaration> Collect()
617615
civlTypeChecker,
618616
layerNum,
619617
absyMap,
620-
forRefinementCheck));
618+
doRefinementCheck));
621619
return decls;
622620
}
623621
}

‎Source/Concurrency/YieldingProcInstrumentation.cs‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ public static List<Declaration> TransformImplementations(
1212
CivlTypeChecker civlTypeChecker,
1313
int layerNum,
1414
AbsyMap absyMap,
15-
bool forRefinementCheck)
15+
bool doRefinementCheck)
1616
{
1717
var linearPermissionInstrumentation =
1818
new LinearPermissionInstrumentation(civlTypeChecker, layerNum, absyMap);
@@ -21,7 +21,7 @@ public static List<Declaration> TransformImplementations(
2121
linearPermissionInstrumentation,
2222
layerNum,
2323
absyMap,
24-
forRefinementCheck);
24+
doRefinementCheck);
2525
yieldingProcInstrumentation.AddNoninterferenceCheckers();
2626
var implToPreconditions = yieldingProcInstrumentation.CreatePreconditions(linearPermissionInstrumentation);
2727
yieldingProcInstrumentation
@@ -75,7 +75,7 @@ public static List<Declaration> TransformImplementations(
7575
private RefinementInstrumentation refinementInstrumentation;
7676
private LinearPermissionInstrumentation linearPermissionInstrumentation;
7777

78-
private bool forRefinementCheck;
78+
private bool doRefinementCheck;
7979

8080
private Dictionary<LinearDomain, Variable> localPermissionCollectors;
8181
private Dictionary<Variable, Variable> oldGlobalMap;
@@ -86,13 +86,13 @@ private YieldingProcInstrumentation(
8686
LinearPermissionInstrumentation linearPermissionInstrumentation,
8787
int layerNum,
8888
AbsyMap absyMap,
89-
bool forRefinementCheck)
89+
bool doRefinementCheck)
9090
{
9191
this.civlTypeChecker = civlTypeChecker;
9292
this.layerNum = layerNum;
9393
this.absyMap = absyMap;
9494
this.linearPermissionInstrumentation = linearPermissionInstrumentation;
95-
this.forRefinementCheck = forRefinementCheck;
95+
this.doRefinementCheck = doRefinementCheck;
9696
parallelCallAggregators = new Dictionary<string, Procedure>();
9797
noninterferenceCheckerProcs = new Dictionary<YieldInvariantDecl, Procedure>();
9898
noninterferenceCheckerImpls = new Dictionary<YieldInvariantDecl, Implementation>();
@@ -121,7 +121,7 @@ private YieldingProcInstrumentation(
121121
}
122122

123123
var wrapperYieldToYieldNoninterferenceCheckerProcName =
124-
forRefinementCheck
124+
doRefinementCheck
125125
? $"Wrapper_YieldToYield_NoninterferenceChecker_Refine_{layerNum}"
126126
: $"Wrapper_YieldToYield_NoninterferenceChecker_{layerNum}";
127127
wrapperYieldToYieldNoninterferenceCheckerProc = DeclHelper.Procedure(
@@ -130,7 +130,7 @@ private YieldingProcInstrumentation(
130130
CivlUtil.AddInlineAttribute(wrapperYieldToYieldNoninterferenceCheckerProc);
131131

132132
var wrapperGlobalNoninterferenceCheckerProcName =
133-
forRefinementCheck
133+
doRefinementCheck
134134
? $"Wrapper_Global_NoninterferenceChecker_Refine_{layerNum}"
135135
: $"Wrapper_Global_NoninterferenceChecker_{layerNum}";
136136
wrapperGlobalNoninterferenceCheckerProc = DeclHelper.Procedure(
@@ -235,7 +235,7 @@ private Formal OldGlobalFormal(Variable v)
235235

236236
private void AddNoninterferenceCheckers()
237237
{
238-
if (civlTypeChecker.Options.TrustNoninterference || forRefinementCheck)
238+
if (civlTypeChecker.Options.TrustNoninterference || doRefinementCheck)
239239
{
240240
return;
241241
}
@@ -280,7 +280,7 @@ private List<Cmd> InlineYieldLoopInvariants(List<CallCmd> yieldInvariants)
280280
foreach (Requires req in yieldInvariant.Preserves)
281281
{
282282
var newExpr = Substituter.Apply(subst, req.Condition);
283-
if (req.Free || forRefinementCheck)
283+
if (req.Free || doRefinementCheck)
284284
{
285285
inlinedYieldInvariants.Add(new AssumeCmd(req.tok, newExpr, req.Attributes));
286286
}
@@ -369,7 +369,7 @@ private void InlineYieldRequiresAndEnsures()
369369
Substitution subst = Substituter.SubstitutionFromDictionary(map);
370370
foreach (Requires req in yieldInvariant.Preserves)
371371
{
372-
impl.Proc.Ensures.Add(new Ensures(req.tok, req.Free || forRefinementCheck, Substituter.Apply(subst, req.Condition),
372+
impl.Proc.Ensures.Add(new Ensures(req.tok, req.Free || doRefinementCheck, Substituter.Apply(subst, req.Condition),
373373
null,
374374
req.Attributes));
375375
}
@@ -405,7 +405,7 @@ private void TransformImpl(Implementation impl, List<Cmd> preconditions)
405405
{
406406
// initialize refinementInstrumentation
407407
var yieldingProc = GetYieldingProc(impl);
408-
if (forRefinementCheck)
408+
if (doRefinementCheck)
409409
{
410410
Debug.Assert(yieldingProc.Layer == layerNum);
411411
refinementInstrumentation = new ActionRefinementInstrumentation(
@@ -663,7 +663,7 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
663663
ins.AddRange(callCmd.Ins);
664664
outs.AddRange(callCmd.Outs);
665665
}
666-
if (forRefinementCheck)
666+
if (doRefinementCheck)
667667
{
668668
procName = procName + "_Refine";
669669
}
@@ -719,7 +719,7 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
719719
}
720720

721721
parallelCallAggregators[procName] = DeclHelper.Procedure(
722-
procName, inParams, outParams, forRefinementCheck ? new List<Requires>() : requiresSeq, new List<Requires>(),
722+
procName, inParams, outParams, doRefinementCheck ? new List<Requires>() : requiresSeq, new List<Requires>(),
723723
civlTypeChecker.GlobalVariables.Select(v => Expr.Ident(v)).ToList(), ensuresSeq);
724724
}
725725

@@ -767,7 +767,7 @@ private void SplitCmds(List<Cmd> cmds, out List<Cmd> firstCmds, out List<Cmd> se
767767

768768
private IEnumerable<Declaration> ActionNoninterferenceCheckers(IEnumerable<Action> actions, bool isGlobal)
769769
{
770-
if (civlTypeChecker.Options.TrustNoninterference || forRefinementCheck)
770+
if (civlTypeChecker.Options.TrustNoninterference || doRefinementCheck)
771771
{
772772
yield break;
773773
}

0 commit comments

Comments
 (0)