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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics;
namespace GPUVerify
{
class AccessInvariantProcessor : StandardVisitor
{
private const string NO_READ = "__no_read_";
private const string NO_WRITE = "__no_write_";
private const string READ = "__read_";
private const string WRITE = "__write_";
private const string READ_OFFSET = "__read_offset_";
private const string WRITE_OFFSET = "__write_offset_";
private const string READ_IMPLIES = "__read_implies_";
private const string WRITE_IMPLIES = "__write_implies_";
public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is FunctionCall)
{
FunctionCall call = node.Fun as FunctionCall;
if (MatchesIntrinsic(call.Func, READ_OFFSET))
{
return new IdentifierExpr(node.tok, new GlobalVariable(
node.tok, new TypedIdent(node.tok, "_READ_OFFSET_X_" +
call.Func.Name.Substring(READ_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))
);
}
if (MatchesIntrinsic(call.Func, WRITE_OFFSET))
{
return new IdentifierExpr(node.tok, new GlobalVariable(
node.tok, new TypedIdent(node.tok, "_WRITE_OFFSET_X_" +
call.Func.Name.Substring(WRITE_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))
);
}
if (MatchesIntrinsic(call.Func, READ_IMPLIES))
{
return Expr.Imp(MakeReadHasOccurred(call, READ_IMPLIES), VisitExpr(node.Args[0]));
}
if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))
{
return Expr.Imp(MakeWriteHasOccurred(call, WRITE_IMPLIES), VisitExpr(node.Args[0]));
}
if (MatchesIntrinsic(call.Func, NO_READ))
{
return Expr.Not(
MakeReadHasOccurred(call, NO_READ)
);
}
if (MatchesIntrinsic(call.Func, NO_WRITE))
{
return Expr.Not(
MakeWriteHasOccurred(call, NO_WRITE)
);
}
if (MatchesIntrinsic(call.Func, READ))
{
return MakeReadHasOccurred(call, READ);
}
if (MatchesIntrinsic(call.Func, WRITE))
{
return MakeWriteHasOccurred(call, WRITE);
}
}
return base.VisitNAryExpr(node);
}
private static IdentifierExpr MakeReadHasOccurred(FunctionCall call, string intrinsicPrefix)
{
return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "READ");
}
private static IdentifierExpr MakeWriteHasOccurred(FunctionCall call, string intrinsicPrefix)
{
return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "WRITE");
}
private bool MatchesIntrinsic(Function function, string intrinsicPrefix)
{
return function.Name.Length > intrinsicPrefix.Length &&
function.Name.Substring(0, intrinsicPrefix.Length).Equals(intrinsicPrefix);
}
}
}
|
