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
|
using System;
using Microsoft.Boogie;
using System.Collections.Generic;
using System.Linq;
namespace GPUVerify {
class VariableDefinitionAnalysis {
GPUVerifier verifier;
Implementation impl;
Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();
Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();
bool changed;
VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {
verifier = v;
impl = i;
}
private class IsConstantVisitor : StandardVisitor {
private VariableDefinitionAnalysis analysis;
public bool isConstant = true;
public IsConstantVisitor(VariableDefinitionAnalysis a) {
analysis = a;
}
public override Expr VisitNAryExpr(NAryExpr expr) {
if (expr.Fun is MapSelect) {
isConstant = false;
return expr;
} else
return base.VisitNAryExpr(expr);
}
public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
return expr;
if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)
isConstant = false;
return expr;
}
};
bool IsConstant(Expr e) {
var v = new IsConstantVisitor(this);
v.Visit(e);
return v.isConstant;
}
void UpdateDefMap(Variable v, Expr def) {
if (!defMap.ContainsKey(v) || defMap[v] != def) {
changed = true;
defMap[v] = def;
}
}
void AddAssignment(AssignLhs lhs, Expr rhs) {
if (lhs is SimpleAssignLhs) {
var sLhs = (SimpleAssignLhs)lhs;
var theVar = sLhs.DeepAssignedVariable;
if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {
UpdateDefMap(theVar, null);
} else {
UpdateDefMap(theVar, rhs);
}
}
}
void Analyse() {
do {
changed = false;
foreach (var c in verifier.RootRegion(impl).Cmds()) {
if (c is AssignCmd) {
var aCmd = (AssignCmd)c;
foreach (var a in aCmd.Lhss.Zip(aCmd.Rhss)) {
AddAssignment(a.Item1, a.Item2);
}
}
}
} while (changed);
}
private class BuildNamedDefVisitor : StandardVisitor {
private VariableDefinitionAnalysis analysis;
public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {
analysis = a;
}
public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
return expr;
return analysis.BuildNamedDefFor(expr.Decl);
}
}
Expr BuildNamedDefFor(Variable v) {
Expr def;
if (namedDefMap.TryGetValue(v.Name, out def))
return def;
def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());
namedDefMap[v.Name] = def;
return def;
}
void BuildNamedDefMap() {
foreach (var v in defMap.Keys)
if (defMap[v] != null)
BuildNamedDefFor(v);
}
private class SubstDualisedDefVisitor : StandardVisitor {
private VariableDefinitionAnalysis analysis;
private VariableDualiser dualiser;
public bool isSubstitutable = true;
public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {
analysis = a;
dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);
}
public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
return dualiser.VisitIdentifierExpr(expr);
var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);
Expr def;
if (!analysis.namedDefMap.TryGetValue(varName, out def)) {
isSubstitutable = false;
return null;
}
return (Expr)dualiser.Visit(def.Clone());
}
}
public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {
var v = new SubstDualisedDefVisitor(this, id, procName);
Expr result = (Expr)v.Visit(e.Clone());
if (!v.isSubstitutable)
return null;
return result;
}
public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
var a = new VariableDefinitionAnalysis(verifier, impl);
a.Analyse();
a.BuildNamedDefMap();
a.defMap = null;
return a;
}
}
}
|
