Skip to content

Commit

Permalink
Merge branch 'master' into coverage-with-renamer
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Aug 14, 2023
2 parents 43d90ad + eb7e2e5 commit e575cb1
Show file tree
Hide file tree
Showing 7 changed files with 42 additions and 110 deletions.
138 changes: 35 additions & 103 deletions Source/Concurrency/NoninterferenceChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,19 @@ public static string PermissionCollectorLocalName(LinearDomain domain)
{
return "linear_" + domain.DomainName + "_available";
}
public static List<Declaration> CreateNoninterferenceCheckers(

public static List<Declaration> CreateNoninterferenceCheckerDecls(
CivlTypeChecker civlTypeChecker,
int layerNum,
AbsyMap absyMap,
YieldInvariantDecl yieldInvariantDecl,
List<Variable> declLocalVariables)
{
if (!yieldInvariantDecl.Requires.Any())
{
return new List<Declaration>();
}

var linearTypeChecker = civlTypeChecker.linearTypeChecker;
var domainToHoleVar = new Dictionary<LinearDomain, Variable>();
Dictionary<Variable, Variable> localVarMap = new Dictionary<Variable, Variable>();
Expand All @@ -35,94 +40,74 @@ public static List<Declaration> CreateNoninterferenceCheckers(
domainToHoleVar[domain] = inParam;
}

foreach (Variable local in declLocalVariables.Union(yieldInvariantDecl.InParams).Union(yieldInvariantDecl.OutParams))
foreach (Variable local in declLocalVariables.Union(yieldInvariantDecl.InParams)
.Union(yieldInvariantDecl.OutParams))
{
var copy = CopyLocal(local);
locals.Add(copy);
localVarMap[local] = copy;
map[local] = Expr.Ident(copy);
}

Dictionary<Variable, Expr> oldLocalMap = new Dictionary<Variable, Expr>();
Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
foreach (Variable g in civlTypeChecker.GlobalVariables)
{
var copy = OldGlobalLocal(civlTypeChecker, g);
locals.Add(copy);
oldLocalMap[g] = Expr.Ident(copy);
Formal f = SnapshotGlobalFormal(civlTypeChecker, g);
inputs.Add(f);
assumeMap[g] = Expr.Ident(f);
}

var linearPermissionInstrumentation = new LinearPermissionInstrumentation(civlTypeChecker,
layerNum, absyMap, domainToHoleVar, localVarMap);
var yieldInfos = new List<YieldInfo>();
var noninterferenceCheckerName = $"yield_{yieldInvariantDecl.Name}";
if (yieldInvariantDecl.Requires.Count > 0)
{
var disjointnessCmds = linearPermissionInstrumentation.ProcDisjointnessAndWellFormedAssumeCmds(yieldInvariantDecl, true);
var yieldPredicates = yieldInvariantDecl.Requires.Select(requires =>
requires.Free
? (PredicateCmd)new AssumeCmd(requires.tok, requires.Condition)
: (PredicateCmd)new AssertCmd(requires.tok, requires.Condition)).ToList();
yieldInfos.Add(new YieldInfo(disjointnessCmds, yieldPredicates));
}

var filteredYieldInfos = yieldInfos.Where(info =>
info.invariantCmds.Any(predCmd => new GlobalAccessChecker().AccessesGlobal(predCmd.Expr)));
if (!filteredYieldInfos.Any())
{
return new List<Declaration>();
}
var disjointnessCmds =
linearPermissionInstrumentation.ProcDisjointnessAndWellFormedAssumeCmds(yieldInvariantDecl, true);
var invariantCmds = yieldInvariantDecl.Requires.Select(requires =>
requires.Free
? (PredicateCmd)new AssumeCmd(requires.tok, requires.Condition)
: (PredicateCmd)new AssertCmd(requires.tok, requires.Condition)).ToList();

Substitution assumeSubst = Substituter.SubstitutionFromDictionary(assumeMap);
Substitution oldSubst = Substituter.SubstitutionFromDictionary(oldLocalMap);
Substitution subst = Substituter.SubstitutionFromDictionary(map);
List<Block> noninterferenceCheckerBlocks = new List<Block>();
List<Block> labelTargets = new List<Block>();
Block noninterferenceCheckerBlock = BlockHelper.Block("exit", new List<Cmd>());
labelTargets.Add(noninterferenceCheckerBlock);
noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock);
int yieldCount = 0;
foreach (var kv in filteredYieldInfos)
{
var newCmds = new List<Cmd>(kv.disjointnessCmds);
foreach (var predCmd in kv.invariantCmds)
{
var newExpr = Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr);
newCmds.Add(new AssumeCmd(predCmd.tok, newExpr));
}

foreach (var predCmd in kv.invariantCmds)
var newCmds = new List<Cmd>(disjointnessCmds);
foreach (var predCmd in invariantCmds)
{
var newExpr = Substituter.Apply(assumeSubst, predCmd.Expr);
newCmds.Add(new AssumeCmd(predCmd.tok, newExpr));
}
foreach (var predCmd in invariantCmds)
{
if (predCmd is AssertCmd)
{
if (predCmd is AssertCmd)
{
var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
assertCmd.Description = new FailureOnlyDescription("Non-interference check failed");
newCmds.Add(assertCmd);
}
var newExpr = Substituter.Apply(subst, predCmd.Expr);
AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
assertCmd.Description = new FailureOnlyDescription("Non-interference check failed");
newCmds.Add(assertCmd);
}

newCmds.Add(CmdHelper.AssumeCmd(Expr.False));
noninterferenceCheckerBlock = BlockHelper.Block("L" + yieldCount++, newCmds);
labelTargets.Add(noninterferenceCheckerBlock);
noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock);
}

newCmds.Add(CmdHelper.AssumeCmd(Expr.False));
noninterferenceCheckerBlock = BlockHelper.Block("L", newCmds);
labelTargets.Add(noninterferenceCheckerBlock);
noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock);
noninterferenceCheckerBlocks.Insert(0, BlockHelper.Block("enter", new List<Cmd>(), labelTargets));

// Create the yield checker procedure
noninterferenceCheckerName = civlTypeChecker.AddNamePrefix($"NoninterferenceChecker_{noninterferenceCheckerName}");
noninterferenceCheckerName =
civlTypeChecker.AddNamePrefix($"NoninterferenceChecker_{noninterferenceCheckerName}");
var noninterferenceCheckerProc = DeclHelper.Procedure(noninterferenceCheckerName,
inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
CivlUtil.AddInlineAttribute(noninterferenceCheckerProc);

// Create the yield checker implementation
var noninterferenceCheckerImpl = DeclHelper.Implementation(noninterferenceCheckerProc,
inputs, new List<Variable>(), locals, noninterferenceCheckerBlocks);
return new List<Declaration> {noninterferenceCheckerProc, noninterferenceCheckerImpl};
return new List<Declaration> { noninterferenceCheckerProc, noninterferenceCheckerImpl };
}

private static LocalVariable CopyLocal(Variable v)
Expand All @@ -139,58 +124,5 @@ private static Formal SnapshotGlobalFormal(CivlTypeChecker civlTypeChecker, Vari
{
return civlTypeChecker.Formal($"snapshot_{v.Name}", v.TypedIdent.Type, true);
}

private static LocalVariable OldGlobalLocal(CivlTypeChecker civlTypeChecker, Variable v)
{
return civlTypeChecker.LocalVariable($"old_{v.Name}", v.TypedIdent.Type);
}
}

class YieldInfo
{
public List<Cmd> disjointnessCmds;
public List<PredicateCmd> invariantCmds;

public YieldInfo(List<Cmd> disjointnessCmds, List<PredicateCmd> invariantCmds)
{
this.disjointnessCmds = disjointnessCmds;
this.invariantCmds = invariantCmds;
}
}

class GlobalAccessChecker : ReadOnlyVisitor
{
private bool accessesGlobal;
private int insideOldExpr;

public GlobalAccessChecker()
{
this.accessesGlobal = false;
this.insideOldExpr = 0;
}

public bool AccessesGlobal(Expr expr)
{
Visit(expr);
return accessesGlobal;
}

public override Expr VisitOldExpr(OldExpr node)
{
insideOldExpr++;
base.VisitOldExpr(node);
insideOldExpr--;
return node;
}

public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
if (node.Decl is GlobalVariable && insideOldExpr == 0)
{
accessesGlobal = true;
}

return node;
}
}
}
2 changes: 1 addition & 1 deletion Source/Concurrency/YieldingProcInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ private void AddNoninterferenceCheckers()
if (layerNum == yieldInvariant.Layer)
{
noninterferenceCheckerDecls.AddRange(
NoninterferenceChecker.CreateNoninterferenceCheckers(civlTypeChecker,
NoninterferenceChecker.CreateNoninterferenceCheckerDecls(civlTypeChecker,
layerNum, absyMap, yieldInvariant, new List<Variable>()));
}
}
Expand Down
2 changes: 1 addition & 1 deletion Test/civl/regression-tests/non-interference-1.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed
Execution trace:
non-interference-1.bpl(7,3): anon0
non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L

Boogie program verifier finished with 4 verified, 1 error
4 changes: 2 additions & 2 deletions Test/civl/regression-tests/non-interference-2.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed
Execution trace:
non-interference-2.bpl(7,3): anon0
non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
non-interference-2.bpl(25,1): Error: Non-interference check failed
Execution trace:
non-interference-2.bpl(34,3): anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L

Boogie program verifier finished with 2 verified, 2 errors
2 changes: 1 addition & 1 deletion Test/civl/regression-tests/parallel1.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ parallel1.bpl(25,1): Error: Non-interference check failed
Execution trace:
parallel1.bpl(7,3): anon0
parallel1.bpl(12,5): inline$AtomicIncr$0$anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L

Boogie program verifier finished with 3 verified, 1 error
2 changes: 1 addition & 1 deletion Test/civl/regression-tests/perm4.bpl.expect
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
perm4.bpl(87,1): Error: Non-interference check failed
Execution trace:
perm4.bpl(68,13): anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L

Boogie program verifier finished with 4 verified, 1 error
2 changes: 1 addition & 1 deletion Test/civl/regression-tests/yield-invariant-fails.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed
Execution trace:
yield-invariant-fails.bpl(11,5): anon0
yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0
(0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L0
(0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L

Boogie program verifier finished with 0 verified, 1 error

0 comments on commit e575cb1

Please sign in to comment.