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
|
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 (uniformityAnalyser == null || !uniformityAnalyser.IsUniform(procName, v.Name))
{
return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
}
return new TypedIdent(v.tok, v.Name, 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)
{
// The point of this override is to avoid dualisation of certain special
// intrinsics 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);
}
}
}
|
