Skip to content

[Civl] Introduction of pure Assert action #1092

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
shazqadeer merged 8 commits into from
Jan 21, 2026
Merged

[Civl] Introduction of pure Assert action #1092

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
8fa70b1
converted a few uses of pure procedure to pure action
shazqadeer Jan 18, 2026
a6cbd14
simplified assert translation by adding pure action Assert
shazqadeer Jan 19, 2026
1d08a4a
removed some dead code
shazqadeer Jan 20, 2026
b2b9692
added comment
shazqadeer Jan 20, 2026
4bb001a
small refactor
shazqadeer Jan 20, 2026
a59a0d3
refactored type checking of calls
shazqadeer Jan 20, 2026
8c784b7
fixed calls to pure procedures and added a test
shazqadeer Jan 21, 2026
312b39d
simplification
shazqadeer Jan 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 28 additions & 29 deletions Source/Concurrency/YieldingProcDuplicator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ public class YieldingProcDuplicator : Duplicator
private Dictionary<Procedure, Procedure> procToDuplicate; /* Original -> Duplicate */
private AbsyMap absyMap; /* Duplicate -> Original */
private Dictionary<string, Procedure> asyncCallPreconditionCheckers;
private Dictionary<string, Procedure> noRequiresPureProcedures;

private LinearRewriter linearRewriter;

Expand All @@ -31,6 +32,7 @@ public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, int layerNum, boo
this.procToDuplicate = [];
this.absyMap = new AbsyMap();
this.asyncCallPreconditionCheckers = [];
this.noRequiresPureProcedures = [];
this.linearRewriter = new LinearRewriter(civlTypeChecker);
this.doRefinementCheck = doRefinementCheck;
}
Expand Down Expand Up @@ -129,27 +131,21 @@ public override Ensures VisitEnsures(Ensures node)
#region Implementation duplication

private YieldProcedureDecl enclosingYieldingProc;
private Block enclosingBlock;
private bool inPredicatePhase;

private List<Cmd> newCmdSeq;

private Dictionary<CtorType, Variable> returnedPAs;

private Dictionary<string, Variable> addedLocalVariables;

public override Implementation VisitImplementation(Implementation impl)
{
enclosingYieldingProc = (YieldProcedureDecl)impl.Proc;
Debug.Assert(layerNum <= enclosingYieldingProc.Layer);

returnedPAs = new Dictionary<CtorType, Variable>();
addedLocalVariables = new Dictionary<string, Variable>();

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

newImpl.LocVars.AddRange(returnedPAs.Values);
newImpl.LocVars.AddRange(addedLocalVariables.Values);

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

public override Block VisitBlock(Block node)
{
enclosingBlock = node;
var block = base.VisitBlock(node);
enclosingBlock = null;
absyMap[block] = node;
return block;
}
Expand All @@ -173,19 +167,7 @@ public override Cmd VisitAssertCmd(AssertCmd node)
assertCmd.Expr = Expr.True;
return assertCmd;
}
if (layerNum != enclosingYieldingProc.Layer)
{
return assertCmd;
}
bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.IsYieldingLoopHeaderAtProcedureLayer(enclosingBlock) && inPredicatePhase;
if (insideLoopInvariantOfYieldingLoop)
{
return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
}
else
{
return doRefinementCheck ? assertCmd : new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
}
return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
}

public override Cmd VisitCallCmd(CallCmd call)
Expand All @@ -209,7 +191,6 @@ public override Cmd VisitParCallCmd(ParCallCmd parCall)
public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
{
newCmdSeq = new List<Cmd>();
inPredicatePhase = true;
foreach (var cmd in cmdSeq)
{
Cmd newCmd = (Cmd) Visit(cmd);
Expand All @@ -225,7 +206,6 @@ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
{
newCmdSeq.Add(newCmd);
}
inPredicatePhase = inPredicatePhase && (cmd is PredicateCmd || cmd is CallCmd callCmd && callCmd.Proc is YieldInvariantDecl);
}
return newCmdSeq;
}
Expand Down Expand Up @@ -302,7 +282,7 @@ cmd is AssertCmd assertCmd && makeAssume
}
else
{
newCmdSeq.Add(newCall);
DesugarPureCall(newCall);
}
}
return;
Expand Down Expand Up @@ -553,21 +533,39 @@ private void AddDuplicateCall(CallCmd newCall, bool makeParallel)

private void DesugarAsyncCall(CallCmd newCall)
{
if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name))
if (!asyncCallPreconditionCheckers.TryGetValue(newCall.Proc.Name, out Procedure checker))
{
asyncCallPreconditionCheckers[newCall.Proc.Name] = DeclHelper.Procedure(
checker = DeclHelper.Procedure(
civlTypeChecker.AddNamePrefix($"AsyncCall_{newCall.Proc.Name}_{layerNum}"),
newCall.Proc.InParams, newCall.Proc.OutParams,
procToDuplicate[newCall.Proc].Requires, [], [], []);
asyncCallPreconditionCheckers[newCall.Proc.Name] = checker;
}

var asyncCallPreconditionChecker = asyncCallPreconditionCheckers[newCall.Proc.Name];
newCall.IsAsync = false;
newCall.Proc = asyncCallPreconditionChecker;
newCall.Proc = checker;
newCall.callee = newCall.Proc.Name;
newCmdSeq.Add(newCall);
}

private void DesugarPureCall(CallCmd newCall)
{
if (doRefinementCheck)
{
if (!noRequiresPureProcedures.TryGetValue(newCall.Proc.Name, out Procedure checker))
{
checker = DeclHelper.Procedure(
civlTypeChecker.AddNamePrefix($"NoRequires_{newCall.Proc.Name}_{layerNum}"),
newCall.Proc.InParams, newCall.Proc.OutParams,
[], [], new List<Ensures>(newCall.Proc.Ensures), []);
noRequiresPureProcedures[newCall.Proc.Name] = checker;
}
newCall.IsAsync = false;
newCall.Proc = checker;
newCall.callee = newCall.Proc.Name;
}
newCmdSeq.Add(newCall);
}

#endregion

public List<Declaration> Collect()
Expand All @@ -577,6 +575,7 @@ public List<Declaration> Collect()
var newImpls = absyMap.Keys.OfType<Implementation>();
decls.AddRange(newImpls);
decls.AddRange(asyncCallPreconditionCheckers.Values);
decls.AddRange(noRequiresPureProcedures.Values);
decls.AddRange(YieldingProcInstrumentation.TransformImplementations(
civlTypeChecker,
layerNum,
Expand Down
5 changes: 0 additions & 5 deletions Source/Core/AST/Absy.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3301,11 +3301,6 @@ public bool IsYieldingLoopHeader(Block block, int layerNum)
}
return layerNum <= YieldingLoops[block].Layer;
}

public bool IsYieldingLoopHeaderAtProcedureLayer(Block block)
{
return IsYieldingLoopHeader(block, Layer);
}
}

public class LoopProcedure : Procedure
Expand Down
116 changes: 52 additions & 64 deletions Source/Core/AST/Commands/CallCmd.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -283,55 +283,59 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
return;
}

void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureDecl calleeDecl)
{
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
var calleeRefinedAction = calleeDecl.RefinedAction;
while (calleeRefinedAction != null)
{
var calleeActionDecl = calleeRefinedAction.ActionDecl;
if (!calleeActionDecl.IsLeftMover)
{
tc.Error(this,
$"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
break;
}
if (calleeActionDecl == highestRefinedActionDecl)
{
break;
}
calleeRefinedAction = calleeActionDecl.RefinedAction;
}
}

// check layers
if (Proc is YieldProcedureDecl calleeDecl)
{
var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
if (calleeDecl.Layer > callerDecl.Layer)
{
tc.Error(this, "layer of callee must not be more than layer of caller");
return;
}
if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null)
{
return;
}
else if (!calleeDecl.HasMoverType)
var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
if (IsAsync && !isSynchronized)
{
tc.Error(this, "async call must be synchronized");
return;
}
// call is synchronous or synchronized
if (!calleeDecl.HasMoverType)
{
Debug.Assert(calleeDecl.RefinedAction != null);
if (callerDecl.Layer > calleeDecl.Layer)
{
if (calleeDecl.RefinedAction != null)
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
if (highestRefinedActionDecl == null)
{
var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
if (highestRefinedActionDecl == null)
{
tc.Error(this, $"called action is not available at layer {callerDecl.Layer}");
}
else
{
if (IsAsync)
{
if (isSynchronized)
{
// check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
var calleeRefinedAction = calleeDecl.RefinedAction;
while (calleeRefinedAction != null)
{
var calleeActionDecl = calleeRefinedAction.ActionDecl;
if (!calleeActionDecl.IsLeftMover)
{
tc.Error(this,
$"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
break;
}
if (calleeActionDecl == highestRefinedActionDecl)
{
break;
}
calleeRefinedAction = calleeActionDecl.RefinedAction;
}
}
else if (callerDecl.HasMoverType)
{
tc.Error(this, "async call must be synchronized in mover procedure");
}
}
}
tc.Error(this, $"called action is not available at layer {callerDecl.Layer}");
}
else if (IsAsync)
{
CheckRefinedChainIsLeftMover(callerDecl, calleeDecl);
}
}
else // callerDecl.Layer == calleeDecl.Layer
Expand All @@ -340,20 +344,9 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
{
tc.Error(this, "caller must not be a mover procedure");
}
else if (IsAsync && calleeDecl.RefinedAction != null)
else if (IsAsync)
{
if (isSynchronized)
{
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
}
else
{
var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
if (highestRefinedAction == null)
{
tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
}
}
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
}
}
}
Expand All @@ -363,18 +356,12 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
{
tc.Error(this, "layer of caller must be equal to layer of callee");
}
else
else if (IsAsync)
{
if (IsAsync)
Debug.Assert(isSynchronized);
if (!calleeDecl.IsLeftMover)
{
if (!isSynchronized)
{
tc.Error(this, "async call to mover procedure must be synchronized");
}
else if (!calleeDecl.IsLeftMover)
{
tc.Error(this, "callee in synchronized call must be a left mover");
}
tc.Error(this, "callee in synchronized call must be a left mover");
}
}
}
Expand Down Expand Up @@ -402,7 +389,7 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc)
}
else
{
// Check global outputs only; the checking of local outputs is done later
// Check global outputs only; the checking of local outputs is done separately
var calleeLayer = Layers[0];
var globalOutputs = Outs.Select(ie => ie.Decl).OfType<GlobalVariable>().Cast<Variable>();
if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
Expand Down Expand Up @@ -513,7 +500,8 @@ public override void Typecheck(TypecheckingContext tc)
var actual = Outs[i];
if (actual.Decl is GlobalVariable)
{
if (!Proc.IsPure) // global outputs of pure calls already checked
// layer range for global outputs of pure calls checked in TypecheckCallCmdInYieldProcedureDecl
if (!Proc.IsPure)
{
tc.Error(actual, $"global variable directly modified in a yield procedure: {actual.Decl.Name}");
}
Expand All @@ -537,7 +525,7 @@ public override void Typecheck(TypecheckingContext tc)
}
else if (modifiedArgument is { Decl: GlobalVariable })
{
// already done in TypecheckCallCmdInYieldProcedureDecl
// checked in TypecheckCallCmdInYieldProcedureDecl
}
else
{
Expand Down
5 changes: 5 additions & 0 deletions Source/Core/base.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -338,3 +338,8 @@ datatype Unit { Unit() }
function {:inline} UnitSet(): Set Unit {
Set_Add(Set_Empty(), Unit())
}

pure action Assert(b: bool)
{
assert b;
}
5 changes: 3 additions & 2 deletions Test/civl/large-samples/GC.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,7 @@ preserves call Yield_Iso();
preserves call Yield_Lock();
requires {:layer 95, 96, 99} tid->i == i;
{
assert {:layer 100} mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]);
call {:layer 100} Assert(mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]));
call WriteBarrier(tid, i, y);
call Yield_Iso() | Yield_WriteField(tid, x, y);
call WriteFieldRaw(tid, x, f, y) | Yield_Lock();
Expand Down Expand Up @@ -1936,7 +1936,8 @@ refines AtomicLockAcquire;
preserves call Yield_Lock();
{
var status:bool;
assert {:layer 95} tid->i != 0;

call {:layer 95} Assert(tid->i != 0);
while (true)
invariant {:yields} true;
invariant call Yield_Lock();
Expand Down
6 changes: 3 additions & 3 deletions Test/civl/large-samples/cache-coherence.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,7 @@ refines atomic action {:layer 2} _ {
call Set_Put(cachePermissions, drp);
}
{
assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
call cache_evict_resp#0(i, ma);
call {:layer 1} Set_Put(cachePermissions, drp);
}
Expand Down Expand Up @@ -397,7 +397,7 @@ refines left action {:layer 2} _ {
call Set_Put(cachePermissions, drp);
}
{
assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
call cache_read_resp#0(i, ma, v, s);
call {:layer 1} Set_Put(cachePermissions, drp);
}
Expand Down Expand Up @@ -722,7 +722,7 @@ refines left action {:layer 2} _ {
call Set_Put(dirPermissions, dp);
}
{
assert {:layer 1} dp == WholeDirPermission(ma);
call {:layer 1} Assert(dp == WholeDirPermission(ma));
call dir_req_end#0(ma, dirState);
call {:layer 1} Set_Put(dirPermissions, dp);
}
Expand Down
Loading
Loading