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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
using Microsoft.Boogie;
using System;
using System.Collections.Generic;
using System.Linq;
namespace GPUVerify {
class ReducedStrengthAnalysis {
GPUVerifier verifier;
Implementation impl;
VariableDefinitionAnalysis varDefs;
Dictionary<Variable, List<Tuple<object, Expr>>> multiDefMap = new Dictionary<Variable, List<Tuple<object, Expr>>>();
Dictionary<string, ModStrideConstraint> strideConstraintMap = new Dictionary<string, ModStrideConstraint>();
Dictionary<object, List<string>> loopCounterMap = new Dictionary<object, List<string>>();
ReducedStrengthAnalysis(GPUVerifier v, Implementation i) {
verifier = v;
impl = i;
varDefs = verifier.varDefAnalyses[impl];
}
void AddAssignment(object regionId, AssignLhs lhs, Expr rhs) {
if (lhs is SimpleAssignLhs) {
var sLhs = (SimpleAssignLhs)lhs;
var theVar = sLhs.DeepAssignedVariable;
List<Tuple<object, Expr>> defs;
if (multiDefMap.ContainsKey(theVar))
defs = multiDefMap[theVar];
else
defs = multiDefMap[theVar] = new List<Tuple<object, Expr>>();
defs.Add(new Tuple<object, Expr>(regionId, rhs));
}
}
void AnalyseRegion(IRegion region) {
foreach (var c in region.CmdsChildRegions()) {
var ac = c as AssignCmd;
if (ac != null) {
foreach (var a in ac.Lhss.Zip(ac.Rhss)) {
AddAssignment(region.Identifier(), a.Item1, a.Item2);
}
}
var child = c as IRegion;
if (child != null)
AnalyseRegion(child);
}
}
void Analyse() {
AnalyseRegion(verifier.RootRegion(impl));
foreach (var v in multiDefMap.Keys) {
var defs = multiDefMap[v];
if (defs.Count != 2)
continue;
bool def0IsConst, def1IsConst;
var def0 = varDefs.SubstDefinitions(defs[0].Item2, impl.Name, out def0IsConst);
var def1 = varDefs.SubstDefinitions(defs[1].Item2, impl.Name, out def1IsConst);
if (def0IsConst && !def1IsConst) {
AddDefinitionPair(v, def0, def1, defs[1].Item1);
} else if (!def0IsConst && def1IsConst) {
AddDefinitionPair(v, def1, def0, defs[0].Item1);
}
}
multiDefMap = null;
}
private class StrideForm {
public StrideForm(Kind kind) { this.kind = kind; this.op = null; }
public StrideForm(Kind kind, Expr op) { this.kind = kind; this.op = op; }
public enum Kind { Bottom, Identity, Constant, Product, PowerMul, PowerDiv };
public Kind kind;
public Expr op;
}
private StrideForm ComputeStrideForm(Variable v, Expr e) {
Expr lhs, rhs;
if (e is LiteralExpr)
return new StrideForm(StrideForm.Kind.Constant, e);
var ie = e as IdentifierExpr;
if (ie != null) {
if (ie.Decl is Constant)
return new StrideForm(StrideForm.Kind.Constant, e);
if (ie.Decl == v)
return new StrideForm(StrideForm.Kind.Identity, e);
}
if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
var lhssf = ComputeStrideForm(v, lhs);
var rhssf = ComputeStrideForm(v, rhs);
if (lhssf.kind == StrideForm.Kind.Constant &&
rhssf.kind == StrideForm.Kind.Constant)
return new StrideForm(StrideForm.Kind.Constant, e);
else if (lhssf.kind == StrideForm.Kind.Constant &&
rhssf.kind == StrideForm.Kind.Identity)
return new StrideForm(StrideForm.Kind.Product, lhs);
else if (lhssf.kind == StrideForm.Kind.Identity &&
rhssf.kind == StrideForm.Kind.Constant)
return new StrideForm(StrideForm.Kind.Product, rhs);
else if (lhssf.kind == StrideForm.Kind.Constant &&
rhssf.kind == StrideForm.Kind.Product)
return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhs, rhssf.op));
else if (lhssf.kind == StrideForm.Kind.Product &&
rhssf.kind == StrideForm.Kind.Constant)
return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhssf.op, rhs));
else
return new StrideForm(StrideForm.Kind.Bottom);
}
var ne = e as NAryExpr;
if (ne != null) {
foreach (Expr op in ne.Args)
if (ComputeStrideForm(v, op).kind != StrideForm.Kind.Constant)
return new StrideForm(StrideForm.Kind.Bottom);
return new StrideForm(StrideForm.Kind.Constant, e);
}
return new StrideForm(StrideForm.Kind.Bottom);
}
private void AddDefinitionPair(Variable v, Expr constDef, Expr nonConstDef, object nonConstId) {
var sf = ComputeStrideForm(v, nonConstDef);
if (sf.kind == StrideForm.Kind.Product) {
var sc = new ModStrideConstraint(sf.op, constDef);
if (!sc.IsBottom()) {
strideConstraintMap[v.Name] = sc;
List<string> lcs;
if (loopCounterMap.ContainsKey(nonConstId))
lcs = loopCounterMap[nonConstId];
else
lcs = loopCounterMap[nonConstId] = new List<string>();
lcs.Add(v.Name);
}
}
}
public StrideConstraint GetStrideConstraint(string varName) {
int id;
var strippedVarName = GPUVerifier.StripThreadIdentifier(varName, out id);
if (!strideConstraintMap.ContainsKey(strippedVarName))
return null;
var msc = strideConstraintMap[strippedVarName];
if (id == 0)
return msc;
return new ModStrideConstraint(verifier.MaybeDualise(msc.mod, id, impl.Name),
verifier.MaybeDualise(msc.modEq, id, impl.Name));
}
public IEnumerable<string> StridedLoopCounters(object loopId) {
if (!loopCounterMap.ContainsKey(loopId))
return Enumerable.Empty<string>();
return loopCounterMap[loopId];
}
public static ReducedStrengthAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
var a = new ReducedStrengthAnalysis(verifier, impl);
a.Analyse();
return a;
}
}
}
|
