Skip to content

Commit 23f70c0

Browse files
shazqadeershazqadeer
authored
[Civl] Introduction of pure Assert action (#1092)
Call to pure action is treated specially on the disappearing layer of the caller. At lower layers, the gate is asserted during invariant checking. But at the disappearing layer, the gate is assumed during invariant checking and asserted during refinement checking. This PR introduces a special pure action Assert which can be used as an alternative to the assert statement with the behavior explained above. As a result, the semantics of assert statements becomes simple; they are asserted during invariant checking and assumed during refinement checking.
1 parent de65f92 commit 23f70c0

File tree

22 files changed

+160
-163
lines changed

22 files changed

+160
-163
lines changed

‎Source/Concurrency/YieldingProcDuplicator.cs‎

Lines changed: 28 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ public class YieldingProcDuplicator : Duplicator
1919
private Dictionary<Procedure, Procedure> procToDuplicate; /* Original -> Duplicate */
2020
private AbsyMap absyMap; /* Duplicate -> Original */
2121
private Dictionary<string, Procedure> asyncCallPreconditionCheckers;
22+
private Dictionary<string, Procedure> noRequiresPureProcedures;
2223

2324
private LinearRewriter linearRewriter;
2425

@@ -31,6 +32,7 @@ public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, int layerNum, boo
3132
this.procToDuplicate = [];
3233
this.absyMap = new AbsyMap();
3334
this.asyncCallPreconditionCheckers = [];
35+
this.noRequiresPureProcedures = [];
3436
this.linearRewriter = new LinearRewriter(civlTypeChecker);
3537
this.doRefinementCheck = doRefinementCheck;
3638
}
@@ -129,27 +131,21 @@ public override Ensures VisitEnsures(Ensures node)
129131
#region Implementation duplication
130132

131133
private YieldProcedureDecl enclosingYieldingProc;
132-
private Block enclosingBlock;
133-
private bool inPredicatePhase;
134134

135135
private List<Cmd> newCmdSeq;
136136

137-
private Dictionary<CtorType, Variable> returnedPAs;
138-
139137
private Dictionary<string, Variable> addedLocalVariables;
140138

141139
public override Implementation VisitImplementation(Implementation impl)
142140
{
143141
enclosingYieldingProc = (YieldProcedureDecl)impl.Proc;
144142
Debug.Assert(layerNum <= enclosingYieldingProc.Layer);
145143

146-
returnedPAs = new Dictionary<CtorType, Variable>();
147144
addedLocalVariables = new Dictionary<string, Variable>();
148145

149146
Implementation newImpl = base.VisitImplementation(impl);
150147
newImpl.Name = newImpl.Proc.Name;
151148

152-
newImpl.LocVars.AddRange(returnedPAs.Values);
153149
newImpl.LocVars.AddRange(addedLocalVariables.Values);
154150

155151
absyMap[newImpl] = impl;
@@ -158,9 +154,7 @@ public override Implementation VisitImplementation(Implementation impl)
158154

159155
public override Block VisitBlock(Block node)
160156
{
161-
enclosingBlock = node;
162157
var block = base.VisitBlock(node);
163-
enclosingBlock = null;
164158
absyMap[block] = node;
165159
return block;
166160
}
@@ -173,19 +167,7 @@ public override Cmd VisitAssertCmd(AssertCmd node)
173167
assertCmd.Expr = Expr.True;
174168
return assertCmd;
175169
}
176-
if (layerNum != enclosingYieldingProc.Layer)
177-
{
178-
return assertCmd;
179-
}
180-
bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.IsYieldingLoopHeaderAtProcedureLayer(enclosingBlock) && inPredicatePhase;
181-
if (insideLoopInvariantOfYieldingLoop)
182-
{
183-
return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
184-
}
185-
else
186-
{
187-
return doRefinementCheck ? assertCmd : new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
188-
}
170+
return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
189171
}
190172

191173
public override Cmd VisitCallCmd(CallCmd call)
@@ -209,7 +191,6 @@ public override Cmd VisitParCallCmd(ParCallCmd parCall)
209191
public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
210192
{
211193
newCmdSeq = new List<Cmd>();
212-
inPredicatePhase = true;
213194
foreach (var cmd in cmdSeq)
214195
{
215196
Cmd newCmd = (Cmd) Visit(cmd);
@@ -225,7 +206,6 @@ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
225206
{
226207
newCmdSeq.Add(newCmd);
227208
}
228-
inPredicatePhase = inPredicatePhase && (cmd is PredicateCmd || cmd is CallCmd callCmd && callCmd.Proc is YieldInvariantDecl);
229209
}
230210
return newCmdSeq;
231211
}
@@ -302,7 +282,7 @@ cmd is AssertCmd assertCmd && makeAssume
302282
}
303283
else
304284
{
305-
newCmdSeq.Add(newCall);
285+
DesugarPureCall(newCall);
306286
}
307287
}
308288
return;
@@ -553,21 +533,39 @@ private void AddDuplicateCall(CallCmd newCall, bool makeParallel)
553533

554534
private void DesugarAsyncCall(CallCmd newCall)
555535
{
556-
if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name))
536+
if (!asyncCallPreconditionCheckers.TryGetValue(newCall.Proc.Name, out Procedure checker))
557537
{
558-
asyncCallPreconditionCheckers[newCall.Proc.Name] = DeclHelper.Procedure(
538+
checker = DeclHelper.Procedure(
559539
civlTypeChecker.AddNamePrefix($"AsyncCall_{newCall.Proc.Name}_{layerNum}"),
560540
newCall.Proc.InParams, newCall.Proc.OutParams,
561541
procToDuplicate[newCall.Proc].Requires, [], [], []);
542+
asyncCallPreconditionCheckers[newCall.Proc.Name] = checker;
562543
}
563-
564-
var asyncCallPreconditionChecker = asyncCallPreconditionCheckers[newCall.Proc.Name];
565544
newCall.IsAsync = false;
566-
newCall.Proc = asyncCallPreconditionChecker;
545+
newCall.Proc = checker;
567546
newCall.callee = newCall.Proc.Name;
568547
newCmdSeq.Add(newCall);
569548
}
570549

550+
private void DesugarPureCall(CallCmd newCall)
551+
{
552+
if (doRefinementCheck)
553+
{
554+
if (!noRequiresPureProcedures.TryGetValue(newCall.Proc.Name, out Procedure checker))
555+
{
556+
checker = DeclHelper.Procedure(
557+
civlTypeChecker.AddNamePrefix($"NoRequires_{newCall.Proc.Name}_{layerNum}"),
558+
newCall.Proc.InParams, newCall.Proc.OutParams,
559+
[], [], new List<Ensures>(newCall.Proc.Ensures), []);
560+
noRequiresPureProcedures[newCall.Proc.Name] = checker;
561+
}
562+
newCall.IsAsync = false;
563+
newCall.Proc = checker;
564+
newCall.callee = newCall.Proc.Name;
565+
}
566+
newCmdSeq.Add(newCall);
567+
}
568+
571569
#endregion
572570

573571
public List<Declaration> Collect()
@@ -577,6 +575,7 @@ public List<Declaration> Collect()
577575
var newImpls = absyMap.Keys.OfType<Implementation>();
578576
decls.AddRange(newImpls);
579577
decls.AddRange(asyncCallPreconditionCheckers.Values);
578+
decls.AddRange(noRequiresPureProcedures.Values);
580579
decls.AddRange(YieldingProcInstrumentation.TransformImplementations(
581580
civlTypeChecker,
582581
layerNum,

‎Source/Core/AST/Absy.cs‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3301,11 +3301,6 @@ public bool IsYieldingLoopHeader(Block block, int layerNum)
33013301
}
33023302
return layerNum <= YieldingLoops[block].Layer;
33033303
}
3304-
3305-
public bool IsYieldingLoopHeaderAtProcedureLayer(Block block)
3306-
{
3307-
return IsYieldingLoopHeader(block, Layer);
3308-
}
33093304
}
33103305

33113306
public class LoopProcedure : Procedure

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

Lines changed: 52 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -283,55 +283,59 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
283283
return;
284284
}
285285

286+
void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureDecl calleeDecl)
287+
{
288+
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
289+
var calleeRefinedAction = calleeDecl.RefinedAction;
290+
while (calleeRefinedAction != null)
291+
{
292+
var calleeActionDecl = calleeRefinedAction.ActionDecl;
293+
if (!calleeActionDecl.IsLeftMover)
294+
{
295+
tc.Error(this,
296+
$"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
297+
break;
298+
}
299+
if (calleeActionDecl == highestRefinedActionDecl)
300+
{
301+
break;
302+
}
303+
calleeRefinedAction = calleeActionDecl.RefinedAction;
304+
}
305+
}
306+
286307
// check layers
287308
if (Proc is YieldProcedureDecl calleeDecl)
288309
{
289-
var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
290310
if (calleeDecl.Layer > callerDecl.Layer)
291311
{
292312
tc.Error(this, "layer of callee must not be more than layer of caller");
313+
return;
314+
}
315+
if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null)
316+
{
317+
return;
293318
}
294-
else if (!calleeDecl.HasMoverType)
319+
var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
320+
if (IsAsync && !isSynchronized)
295321
{
322+
tc.Error(this, "async call must be synchronized");
323+
return;
324+
}
325+
// call is synchronous or synchronized
326+
if (!calleeDecl.HasMoverType)
327+
{
328+
Debug.Assert(calleeDecl.RefinedAction != null);
296329
if (callerDecl.Layer > calleeDecl.Layer)
297330
{
298-
if (calleeDecl.RefinedAction != null)
331+
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
332+
if (highestRefinedActionDecl == null)
299333
{
300-
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
301-
if (highestRefinedActionDecl == null)
302-
{
303-
tc.Error(this, $"called action is not available at layer {callerDecl.Layer}");
304-
}
305-
else
306-
{
307-
if (IsAsync)
308-
{
309-
if (isSynchronized)
310-
{
311-
// check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
312-
var calleeRefinedAction = calleeDecl.RefinedAction;
313-
while (calleeRefinedAction != null)
314-
{
315-
var calleeActionDecl = calleeRefinedAction.ActionDecl;
316-
if (!calleeActionDecl.IsLeftMover)
317-
{
318-
tc.Error(this,
319-
$"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
320-
break;
321-
}
322-
if (calleeActionDecl == highestRefinedActionDecl)
323-
{
324-
break;
325-
}
326-
calleeRefinedAction = calleeActionDecl.RefinedAction;
327-
}
328-
}
329-
else if (callerDecl.HasMoverType)
330-
{
331-
tc.Error(this, "async call must be synchronized in mover procedure");
332-
}
333-
}
334-
}
334+
tc.Error(this, $"called action is not available at layer {callerDecl.Layer}");
335+
}
336+
else if (IsAsync)
337+
{
338+
CheckRefinedChainIsLeftMover(callerDecl, calleeDecl);
335339
}
336340
}
337341
else // callerDecl.Layer == calleeDecl.Layer
@@ -340,20 +344,9 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
340344
{
341345
tc.Error(this, "caller must not be a mover procedure");
342346
}
343-
else if (IsAsync && calleeDecl.RefinedAction != null)
347+
else if (IsAsync)
344348
{
345-
if (isSynchronized)
346-
{
347-
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
348-
}
349-
else
350-
{
351-
var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
352-
if (highestRefinedAction == null)
353-
{
354-
tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
355-
}
356-
}
349+
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
357350
}
358351
}
359352
}
@@ -363,18 +356,12 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
363356
{
364357
tc.Error(this, "layer of caller must be equal to layer of callee");
365358
}
366-
else
359+
else if (IsAsync)
367360
{
368-
if (IsAsync)
361+
Debug.Assert(isSynchronized);
362+
if (!calleeDecl.IsLeftMover)
369363
{
370-
if (!isSynchronized)
371-
{
372-
tc.Error(this, "async call to mover procedure must be synchronized");
373-
}
374-
else if (!calleeDecl.IsLeftMover)
375-
{
376-
tc.Error(this, "callee in synchronized call must be a left mover");
377-
}
364+
tc.Error(this, "callee in synchronized call must be a left mover");
378365
}
379366
}
380367
}
@@ -402,7 +389,7 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
402389
}
403390
else
404391
{
405-
// Check global outputs only; the checking of local outputs is done later
392+
// Check global outputs only; the checking of local outputs is done separately
406393
var calleeLayer = Layers[0];
407394
var globalOutputs = Outs.Select(ie => ie.Decl).OfType<GlobalVariable>().Cast<Variable>();
408395
if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
@@ -513,7 +500,8 @@ public override void Typecheck(TypecheckingContext tc)
513500
var actual = Outs[i];
514501
if (actual.Decl is GlobalVariable)
515502
{
516-
if (!Proc.IsPure) // global outputs of pure calls already checked
503+
// layer range for global outputs of pure calls checked in TypecheckCallCmdInYieldProcedureDecl
504+
if (!Proc.IsPure)
517505
{
518506
tc.Error(actual, $"global variable directly modified in a yield procedure: {actual.Decl.Name}");
519507
}
@@ -537,7 +525,7 @@ public override void Typecheck(TypecheckingContext tc)
537525
}
538526
else if (modifiedArgument is { Decl: GlobalVariable })
539527
{
540-
// already done in TypecheckCallCmdInYieldProcedureDecl
528+
// checked in TypecheckCallCmdInYieldProcedureDecl
541529
}
542530
else
543531
{

‎Source/Core/base.bpl‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -338,3 +338,8 @@ datatype Unit { Unit() }
338338
function {:inline} UnitSet(): Set Unit {
339339
Set_Add(Set_Empty(), Unit())
340340
}
341+
342+
pure action Assert(b: bool)
343+
{
344+
assert b;
345+
}

‎Test/civl/large-samples/GC.bpl‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -301,7 +301,7 @@ preserves call Yield_Iso();
301301
preserves call Yield_Lock();
302302
requires {:layer 95, 96, 99} tid->i == i;
303303
{
304-
assert {:layer 100} mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]);
304+
call {:layer 100} Assert(mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]));
305305
call WriteBarrier(tid, i, y);
306306
call Yield_Iso() | Yield_WriteField(tid, x, y);
307307
call WriteFieldRaw(tid, x, f, y) | Yield_Lock();
@@ -1936,7 +1936,8 @@ refines AtomicLockAcquire;
19361936
preserves call Yield_Lock();
19371937
{
19381938
var status:bool;
1939-
assert {:layer 95} tid->i != 0;
1939+
1940+
call {:layer 95} Assert(tid->i != 0);
19401941
while (true)
19411942
invariant {:yields} true;
19421943
invariant call Yield_Lock();

‎Test/civl/large-samples/cache-coherence.bpl‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -357,7 +357,7 @@ refines atomic action {:layer 2} _ {
357357
call Set_Put(cachePermissions, drp);
358358
}
359359
{
360-
assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
360+
call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
361361
call cache_evict_resp#0(i, ma);
362362
call {:layer 1} Set_Put(cachePermissions, drp);
363363
}
@@ -397,7 +397,7 @@ refines left action {:layer 2} _ {
397397
call Set_Put(cachePermissions, drp);
398398
}
399399
{
400-
assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
400+
call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
401401
call cache_read_resp#0(i, ma, v, s);
402402
call {:layer 1} Set_Put(cachePermissions, drp);
403403
}
@@ -722,7 +722,7 @@ refines left action {:layer 2} _ {
722722
call Set_Put(dirPermissions, dp);
723723
}
724724
{
725-
assert {:layer 1} dp == WholeDirPermission(ma);
725+
call {:layer 1} Assert(dp == WholeDirPermission(ma));
726726
call dir_req_end#0(ma, dirState);
727727
call {:layer 1} Set_Put(dirPermissions, dp);
728728
}

0 commit comments

Comments
 (0)