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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics;
namespace GPUVerify
{
class VariableDualiser : Duplicator
{
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 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 (CommandLineOptions.InterGroupRaceChecking && 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) ||
(CommandLineOptions.InterGroupRaceChecking && 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 (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool") ||
call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool") ||
call.Func.Name.Equals("__all") || call.Func.Name.Equals("__at_most_one"))
{
return node;
}
}
return base.VisitNAryExpr(node);
}
}
}
|
