Skip to content
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

Jump to bottom

[Civl] Bug fix in anonymous actions #981

Merged
merged 2 commits into from
Nov 10, 2024
Merged

[Civl] Bug fix in anonymous actions #981

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
51ebf35
first commit
shazqadeer Nov 7, 2024
8598dc9
renames
shazqadeer Nov 9, 2024
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
9 changes: 2 additions & 7 deletions Source/Concurrency/LinearRewriter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,9 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker)
this.civlTypeChecker = civlTypeChecker;
}

public static bool IsPrimitive(DeclWithFormals decl)
{
return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
}

public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl)
{
if (IsPrimitive(impl)) {
if (CivlPrimitives.IsPrimitive(impl)) {
return;
}
var linearRewriter = new LinearRewriter(civlTypeChecker);
Expand All @@ -38,7 +33,7 @@ private List<Cmd> RewriteCmdSeq(List<Cmd> cmdSeq)
{
if (cmd is CallCmd callCmd)
{
if (IsPrimitive(callCmd.Proc))
if (CivlPrimitives.IsPrimitive(callCmd.Proc))
{
newCmdSeq.AddRange(RewriteCallCmd(callCmd));
}
Expand Down
10 changes: 5 additions & 5 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
}
else if (cmd is CallCmd callCmd)
{
var isPrimitive = LinearRewriter.IsPrimitive(callCmd.Proc);
var isPrimitive = CivlPrimitives.IsPrimitive(callCmd.Proc);
if (!isPrimitive)
{
linearGlobalVariables.Except(start).ForEach(g =>
Expand Down Expand Up @@ -338,7 +338,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)

public override Implementation VisitImplementation(Implementation node)
{
if (LinearRewriter.IsPrimitive(node))
if (CivlPrimitives.IsPrimitive(node))
{
return node;
}
Expand Down Expand Up @@ -538,7 +538,7 @@ public override Cmd VisitUnpackCmd(UnpackCmd node)

public override Cmd VisitCallCmd(CallCmd node)
{
var isPrimitive = LinearRewriter.IsPrimitive(node.Proc);
var isPrimitive = CivlPrimitives.IsPrimitive(node.Proc);
var inVars = new HashSet<Variable>();
var globalInVars = new HashSet<Variable>();
for (int i = 0; i < node.Proc.InParams.Count; i++)
Expand Down Expand Up @@ -752,7 +752,7 @@ enclosingProc is not YieldProcedureDecl &&

public override Cmd VisitParCallCmd(ParCallCmd node)
{
if (node.CallCmds.Any(callCmd => LinearRewriter.IsPrimitive(callCmd.Proc)))
if (node.CallCmds.Any(callCmd => CivlPrimitives.IsPrimitive(callCmd.Proc)))
{
Error(node, "linear primitives may not be invoked in a parallel call");
return node;
Expand Down Expand Up @@ -831,7 +831,7 @@ private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source
private void CheckLinearStoreAccessInGuards()
{
program.Implementations.ForEach(impl => {
if (LinearRewriter.IsPrimitive(impl))
if (CivlPrimitives.IsPrimitive(impl))
{
return;
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Concurrency/YieldingProcDuplicator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ private void ProcessCallCmd(CallCmd newCall)
InjectGate(pureAction, newCall);
newCmdSeq.Add(newCall);
}
else if (LinearRewriter.IsPrimitive(newCall.Proc))
else if (CivlPrimitives.IsPrimitive(newCall.Proc))
{
newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall));
}
Expand Down
9 changes: 9 additions & 0 deletions Source/Core/Analysis/ModSetCollector.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,6 +194,15 @@ public override Cmd VisitCallCmd(CallCmd callCmd)
}
}

if (CivlPrimitives.IsPrimitive(callCmd.Proc))
{
var modifiedArgument = CivlPrimitives.ModifiedArgument(callCmd)?.Decl;
if (modifiedArgument != null)
{
ProcessVariable(modifiedArgument);
}
}

return ret;
}

Expand Down
8 changes: 5 additions & 3 deletions Source/Core/BoogiePL.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -759,17 +759,19 @@ SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>

SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
=
(. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
(. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
"refines"
{ Attribute<ref kv> }
(
MoverQualifier<ref moverType>
"action" (. tok = t; .)
{ Attribute<ref akv> }
Ident<out unused>
Ident<out m>
ImplBody<out locals, out stmtList>
(.
if (refinedAction == null) {
if (m.val != "_") {
this.SemErr("expected _ for name of anoonymous action");
} else if (refinedAction == null) {
var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
false, new List<ActionDeclRef>(), null, null,
new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
Expand Down
5 changes: 5 additions & 0 deletions Source/Core/CivlAttributes.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,11 @@ public static class CivlPrimitives
"Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put"
};

public static bool IsPrimitive(DeclWithFormals decl)
{
return LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
}

public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
{
if (expr is IdentifierExpr identifierExpr)
Expand Down
8 changes: 5 additions & 3 deletions Source/Core/Parser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1219,7 +1219,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) {
}

void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs) {
IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList;
IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList;
Expect(41);
while (la.kind == 26) {
Attribute(ref kv);
Expand All @@ -1231,9 +1231,11 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken
while (la.kind == 26) {
Attribute(ref akv);
}
Ident(out unused);
Ident(out m);
ImplBody(out locals, out stmtList);
if (refinedAction == null) {
if (m.val != "_") {
this.SemErr("expected _ for name of anoonymous action");
} else if (refinedAction == null) {
var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
false, new List<ActionDeclRef>(), null, null,
new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
Expand Down
Loading
Loading