Skip to content

Commit

Permalink
Isolate path refactorings (#969)
Browse files Browse the repository at this point in the history 
Stacks on #968

### Changes
Contains refactoring that were part of
#970

### Testing
No additional tests needed
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Oct 22, 2024
1 parent d59fec7 commit 7e957c1
Show file tree
Hide file tree
Showing 36 changed files with 434 additions and 446 deletions.
17 changes: 8 additions & 9 deletions Source/AbstractInterpretation/NativeLattice.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -185,8 +185,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
// We need to keep track of some information for each(some) block(s). To do that efficiently,
// we number the implementation's blocks sequentially, and then we can use arrays to store
// the additional information.
var pre = new NativeLattice.Element[impl.Blocks
.Count]; // set to null if we never compute a join/widen at this block
var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
? new NativeLattice.Element[impl.Blocks.Count]
: null;
Expand All @@ -195,7 +194,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
int n = 0;
foreach (var block in impl.Blocks)
{
block.aiId = n;
block.AiId = n;
// Note: The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
// Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
// n == 0 || block.widenBlock
Expand All @@ -219,7 +218,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
{
var workItem = workItems.Dequeue();
var b = workItem.Item1;
var id = b.aiId;
var id = b.AiId;
var e = workItem.Item2;
if (pre[id] == null)
{
Expand All @@ -230,7 +229,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
// no change
continue;
}
else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
else if (b.WidenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
{
e = lattice.Widen(pre[id], e);
pre[id] = e;
Expand Down Expand Up @@ -275,8 +274,8 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.

foreach (var b in impl.Blocks)
{
var element = pre[b.aiId];
if (element != null && (b.widenBlock || options.InstrumentInfer ==
var element = pre[b.AiId];
if (element != null && (b.WidenBlock || options.InstrumentInfer ==
CoreOptions.InstrumentationPlaces.Everywhere))
{
List<Cmd> newCommands = new List<Cmd>();
Expand All @@ -294,9 +293,9 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.

newCommands.Add(cmd);
newCommands.AddRange(b.Cmds);
if (post != null && post[b.aiId] != null)
if (post != null && post[b.AiId] != null)
{
inv = post[b.aiId].ToExpr(options);
inv = post[b.AiId].ToExpr(options);
kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
if (options.InstrumentWithAsserts)
{
Expand Down
4 changes: 2 additions & 2 deletions Source/AbstractInterpretation/Traverse.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ static void Visit(Block b)
{
cce.BeginExpose(b);
// we got here through a back-edge
b.widenBlock = true;
b.WidenBlock = true;
cce.EndExpose();
}
else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
Expand Down Expand Up @@ -111,7 +111,7 @@ static void Visit(Block b)
/// </summary>
public static List<Block> ComputeLoopBodyFrom(Block block)
{
Contract.Requires(block.widenBlock);
Contract.Requires(block.WidenBlock);
Contract.Requires(block != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

Expand Down
6 changes: 3 additions & 3 deletions Source/Concurrency/LinearPermissionInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,18 +61,18 @@ public List<Cmd> DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals)
public void AddDisjointnessAndWellFormedAssumptions(Implementation impl)
{
// calls and parallel calls
foreach (var b in impl.Blocks)
foreach (var block in impl.Blocks)
{
var newCmds = new List<Cmd>();
foreach (var cmd in b.Cmds)
foreach (var cmd in block.Cmds)
{
newCmds.Add(cmd);
if (cmd is ParCallCmd)
{
newCmds.AddRange(DisjointnessAndWellFormedAssumeCmds(cmd, true));
}
}
b.Cmds = newCmds;
block.Cmds = newCmds;
}

// loop headers
Expand Down
10 changes: 5 additions & 5 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -852,14 +852,14 @@ void ProcessIfCmd(IfCmd ifCmd)
{
checkingContext.Error(ifCmd.tok, "access to linear store not allowed");
}
stmtLists.Push(ifCmd.thn);
if (ifCmd.elseIf != null)
stmtLists.Push(ifCmd.Thn);
if (ifCmd.ElseIf != null)
{
ProcessIfCmd(ifCmd.elseIf);
ProcessIfCmd(ifCmd.ElseIf);
}
else if (ifCmd.elseBlock != null)
else if (ifCmd.ElseBlock != null)
{
stmtLists.Push(ifCmd.elseBlock);
stmtLists.Push(ifCmd.ElseBlock);
}
}
ProcessIfCmd(ifCmd);
Expand Down
112 changes: 56 additions & 56 deletions Source/Concurrency/YieldingProcInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -474,65 +474,61 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)

// add jumps to noninterferenceChecker, returnChecker, and refinementChecker blocks
var implRefinementCheckingBlocks = new List<Block>();
foreach (var b in impl.Blocks)
{
if (b.TransferCmd is GotoCmd gotoCmd)
{
var targetBlocks = new List<Block>();
var addEdge = false;
foreach (var nextBlock in gotoCmd.LabelTargets)
{
if (nextBlock.cmds.Count > 0)
{
var cmd = nextBlock.cmds[0];
if (cmd is ParCallCmd parCallCmd)
{
foreach (var callCmd in parCallCmd.CallCmds)
{
if (refinementBlocks.ContainsKey(callCmd))
{
var targetBlock = refinementBlocks[callCmd];
FixUpImplRefinementCheckingBlock(targetBlock,
CivlAttributes.IsCallMarked(callCmd)
? returnCheckerBlock
: unchangedCheckerBlock);
targetBlocks.Add(targetBlock);
implRefinementCheckingBlocks.Add(targetBlock);
}
}
addEdge = true;
}
}
foreach (var b in impl.Blocks) {
if (b.TransferCmd is not GotoCmd gotoCmd) {
b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
new List<Block> { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock });
continue;
}

var targetBlocks = new List<Block>();
var addEdge = false;
foreach (var nextBlock in gotoCmd.LabelTargets) {
if (nextBlock.Cmds.Count <= 0) {
continue;
}

gotoCmd.AddTargets(targetBlocks);
if (addEdge)
{
AddEdge(gotoCmd, noninterferenceCheckerBlock);
if (blocksInYieldingLoops.Contains(b))
{
AddEdge(gotoCmd, unchangedCheckerBlock);
}
else
{
b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
AddEdge(gotoCmd, refinementCheckerBlock);
var cmd = nextBlock.Cmds[0];
if (cmd is not ParCallCmd parCallCmd) {
continue;
}

foreach (var callCmd in parCallCmd.CallCmds) {
if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock)) {
continue;
}

FixUpImplRefinementCheckingBlock(targetBlock,
CivlAttributes.IsCallMarked(callCmd)
? returnCheckerBlock
: unchangedCheckerBlock);
targetBlocks.Add(targetBlock);
implRefinementCheckingBlocks.Add(targetBlock);
}

addEdge = true;
}
else
{
b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
new List<Block> {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock});

gotoCmd.AddTargets(targetBlocks);
if (!addEdge) {
continue;
}

AddEdge(gotoCmd, noninterferenceCheckerBlock);
if (blocksInYieldingLoops.Contains(b)) {
AddEdge(gotoCmd, unchangedCheckerBlock);
} else {
b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
AddEdge(gotoCmd, refinementCheckerBlock);
}
}

// desugar ParCallCmd
foreach (Block b in impl.Blocks)
{
if (b.cmds.Count > 0)
if (b.Cmds.Count > 0)
{
var cmd = b.cmds[0];
var cmd = b.Cmds[0];
if (cmd is ParCallCmd)
{
DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b));
Expand All @@ -545,7 +541,9 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
impl.Blocks.Add(unchangedCheckerBlock);
impl.Blocks.Add(returnCheckerBlock);
impl.Blocks.Add(returnBlock);
impl.Blocks.AddRange(implRefinementCheckingBlocks);
foreach (var block in implRefinementCheckingBlocks) {
impl.Blocks.Add(block);
}
impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions));
}

Expand Down Expand Up @@ -578,31 +576,33 @@ private void SplitBlocks(Implementation impl)
{
var currTransferCmd = b.TransferCmd;
int labelCount = 0;
int lastSplitIndex = b.cmds.Count;
for (int i = b.cmds.Count - 1; i >= 0; i--)
int lastSplitIndex = b.Cmds.Count;
for (int i = b.Cmds.Count - 1; i >= 0; i--)
{
var split = false;
var cmd = b.cmds[i];
var cmd = b.Cmds[i];
if (cmd is ParCallCmd)
{
split = true;
}

if (split)
{
var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i),
var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i),
currTransferCmd);
newBlocks.Add(newBlock);
currTransferCmd = new GotoCmd(b.tok, new List<Block> {newBlock});
lastSplitIndex = i;
}
}

b.cmds = b.cmds.GetRange(0, lastSplitIndex);
b.Cmds = b.Cmds.GetRange(0, lastSplitIndex);
b.TransferCmd = currTransferCmd;
}

impl.Blocks.AddRange(newBlocks);
foreach (var newBlock in newBlocks) {
impl.Blocks.Add(newBlock);
}
}

private Block CreateNoninterferenceCheckerBlock()
Expand Down Expand Up @@ -714,8 +714,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
newCmds.AddRange(CreateUpdatesToOldGlobalVars());
newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd));
newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1));
block.cmds = newCmds;
newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1));
block.Cmds = newCmds;
}

private Formal ParCallDesugarFormal(Variable v, int count, bool incoming)
Expand Down
2 changes: 1 addition & 1 deletion Source/Core/AST/Expression/AbsyExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3890,7 +3890,7 @@ public class CodeExpr : Expr
public List<Variable> /*!*/
LocVars;

[Rep] public List<Block /*!*/> /*!*/ Blocks;
[Rep] public IList<Block /*!*/> /*!*/ Blocks;

[ContractInvariantMethod]
void ObjectInvariant()
Expand Down
Loading

0 comments on commit 7e957c1

Please sign in to comment.