blob: 281620c5c8b55a71ba303ec25c4818959c18de6a (
plain)
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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Basetypes;
using System.Diagnostics;
namespace GPUVerify
{
class ReadCollector : AccessCollector
{
public List<AccessRecord> accesses = new List<AccessRecord>();
public ReadCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
: base(GlobalVariables, TileStaticVariables)
{
}
public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
{
return node;
}
public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is MapSelect)
{
if ((node.Fun as MapSelect).Arity > 1)
{
MultiDimensionalMapError();
}
Variable ReadVariable = null;
Expr IndexX = node.Args[1];
Expr IndexY = null;
Expr IndexZ = null;
if (node.Args[0] is NAryExpr)
{
NAryExpr nestedMap = node.Args[0] as NAryExpr;
Debug.Assert(nestedMap.Fun is MapSelect);
if ((nestedMap.Fun as MapSelect).Arity > 1)
{
MultiDimensionalMapError();
}
IndexY = nestedMap.Args[1];
if (nestedMap.Args[0] is NAryExpr)
{
NAryExpr nestedNestedMap = nestedMap.Args[0] as NAryExpr;
Debug.Assert(nestedNestedMap.Fun is MapSelect);
if ((nestedNestedMap.Fun as MapSelect).Arity > 1)
{
MultiDimensionalMapError();
}
IndexZ = nestedMap.Args[1];
if (!(nestedNestedMap.Args[0] is IdentifierExpr))
{
Console.WriteLine("*** Error - maps with more than three levels of nesting are not supported");
Environment.Exit(1);
}
ReadVariable = (nestedNestedMap.Args[0] as IdentifierExpr).Decl;
this.VisitExpr(nestedNestedMap.Args[1]);
}
else
{
Debug.Assert(nestedMap.Args[0] is IdentifierExpr);
ReadVariable = (nestedMap.Args[0] as IdentifierExpr).Decl;
}
this.VisitExpr(nestedMap.Args[1]);
}
else
{
Debug.Assert(node.Args[0] is IdentifierExpr);
ReadVariable = (node.Args[0] as IdentifierExpr).Decl;
}
this.VisitExpr(node.Args[1]);
if (GlobalVariables.Contains(ReadVariable) || TileStaticVariables.Contains(ReadVariable))
{
accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));
}
return node;
}
else
{
return base.VisitNAryExpr(node);
}
}
public override Variable VisitVariable(Variable node)
{
if (!(GlobalVariables.Contains(node) || TileStaticVariables.Contains(node)))
{
return node;
}
accesses.Add(new AccessRecord(node, null, null, null));
return node;
}
}
}
|
