blob: 0da75cb435979220d3c0e335789ae9d5d65f6314 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Graphing;
namespace GPUVerify {
class UnstructuredRegion : IRegion {
Graph<Block> blockGraph;
Block header;
Dictionary<Block, HashSet<Block>> loopNodes = new Dictionary<Block, HashSet<Block>>();
Dictionary<Block, Block> innermostHeader = new Dictionary<Block, Block>();
Expr guard;
public UnstructuredRegion(Program p, Implementation impl) {
blockGraph = p.ProcessLoops(impl);
header = null;
foreach (var h in blockGraph.SortHeadersByDominance()) {
var loopNodes = new HashSet<Block>();
foreach (var b in blockGraph.BackEdgeNodes(h))
loopNodes.UnionWith(blockGraph.NaturalLoops(h, b));
this.loopNodes[h] = loopNodes;
foreach (var n in loopNodes)
if (n != h)
innermostHeader[n] = h;
}
guard = null;
}
private UnstructuredRegion(UnstructuredRegion r, Block h) {
blockGraph = r.blockGraph;
header = h;
loopNodes = r.loopNodes;
innermostHeader = r.innermostHeader;
guard = null;
}
public object Identifier() {
return header;
}
private HashSet<Block> SubBlocks() {
if (header != null) {
return loopNodes[header];
} else {
return blockGraph.Nodes;
}
}
public IEnumerable<Cmd> Cmds() {
foreach (var b in SubBlocks())
foreach (Cmd c in b.Cmds)
yield return c;
}
public IEnumerable<object> CmdsChildRegions() {
if (header != null)
foreach (Cmd c in header.Cmds)
yield return c;
foreach (var b in SubBlocks()) {
Block bHeader;
innermostHeader.TryGetValue(b, out bHeader);
if (header == bHeader) {
if (blockGraph.Headers.Contains(b))
yield return new UnstructuredRegion(this, b);
else
foreach (Cmd c in b.Cmds)
yield return c;
}
}
}
public IEnumerable<IRegion> SubRegions() {
return SubBlocks().Intersect(loopNodes.Keys).Select(b => new UnstructuredRegion(this, b));
}
public Expr Guard() {
if (header == null)
return null;
if (guard == null) {
var backedges = blockGraph.BackEdgeNodes(header);
if (backedges.Count() != 1)
return null;
var assumes = backedges.Single().Cmds.Cast<Cmd>().OfType<AssumeCmd>();
if (assumes.Count() != 1)
return null;
guard = assumes.Single().Expr;
}
return guard;
}
public void AddInvariant(PredicateCmd pc) {
header.Cmds = new CmdSeq((new Cmd[] {pc}.Concat(header.Cmds.Cast<Cmd>())).ToArray());
}
}
}
|
