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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics;
namespace GPUVerify
{
class VariableDualiser : Duplicator
{
static HashSet<string> otherFunctionNames =
new HashSet<string>(new string[] { "__other_bool", "__other_bv32", "__other_arrayId" });
private int id;
private UniformityAnalyser uniformityAnalyser;
private string procName;
public VariableDualiser(int id, UniformityAnalyser uniformityAnalyser, string procName)
{
Debug.Assert((uniformityAnalyser == null && procName == null)
|| (uniformityAnalyser != null && procName != null));
this.id = id;
this.uniformityAnalyser = uniformityAnalyser;
this.procName = procName;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
if (node.Decl is Formal) {
return new IdentifierExpr(node.tok, new Formal(node.tok, DualiseTypedIdent(node.Decl),
(node.Decl as Formal).InComing));
}
if (!(node.Decl is Constant))
{
return new IdentifierExpr(node.tok, new LocalVariable(node.tok, DualiseTypedIdent(node.Decl)));
}
if (GPUVerifier.IsThreadLocalIdConstant(node.Decl))
{
return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));
}
if (GPUVerifier.IsGroupIdConstant(node.Decl))
{
return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));
}
return node;
}
private TypedIdent DualiseTypedIdent(Variable v)
{
if (QKeyValue.FindBoolAttribute(v.Attributes, "global") ||
QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
}
if (uniformityAnalyser != null && uniformityAnalyser.IsUniform(procName, v.Name))
{
return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
}
return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
}
public override Variable VisitVariable(Variable node)
{
if (!(node is Constant) || GPUVerifier.IsThreadLocalIdConstant(node) ||
GPUVerifier.IsGroupIdConstant(node))
{
node.TypedIdent = DualiseTypedIdent(node);
node.Name = node.Name + "$" + id;
return node;
}
return base.VisitVariable(node);
}
public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is MapSelect) {
Debug.Assert((node.Fun as MapSelect).Arity == 1);
Debug.Assert(node.Args[0] is IdentifierExpr);
var v = (node.Args[0] as IdentifierExpr).Decl;
if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
new ExprSeq(new Expr[] { node.Args[0], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));
}
}
// Avoid dualisation of certain special builtin functions that are cross-thread
if (node.Fun is FunctionCall)
{
FunctionCall call = node.Fun as FunctionCall;
if (otherFunctionNames.Contains(call.Func.Name))
{
Debug.Assert(id == 1 || id == 2);
int otherId = id == 1 ? 2 : 1;
return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
node.Args[0]);
}
}
return base.VisitNAryExpr(node);
}
public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
var v = node.DeepAssignedVariable;
if(QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,
new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
}
return base.VisitMapAssignLhs(node);
}
private Expr GroupSharedIndexingExpr() {
return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();
}
}
}
|
