@@ -123,18 +123,18 @@ module Make<LocationSig Location, InputSig<Location> Input> {
123
123
* (certain or uncertain) writes.
124
124
*/
125
125
private newtype TRefKind =
126
- Read ( boolean certain ) { certain in [ false , true ] } or
126
+ Read ( ) or
127
127
Write ( boolean certain ) { certain in [ false , true ] }
128
128
129
129
private class RefKind extends TRefKind {
130
130
string toString ( ) {
131
- exists ( boolean certain | this = Read ( certain ) and result = "read (" + certain + ")" )
131
+ this = Read ( ) and result = "read"
132
132
or
133
133
exists ( boolean certain | this = Write ( certain ) and result = "write (" + certain + ")" )
134
134
}
135
135
136
136
int getOrder ( ) {
137
- this = Read ( _ ) and
137
+ this = Read ( ) and
138
138
result = 0
139
139
or
140
140
this = Write ( _) and
@@ -146,7 +146,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
146
146
* Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
147
147
*/
148
148
predicate ref ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
149
- exists ( boolean certain | variableRead ( bb , i , v , certain ) | k = Read ( certain ) )
149
+ variableRead ( bb , i , v , _ ) and k = Read ( )
150
150
or
151
151
exists ( boolean certain | variableWrite ( bb , i , v , certain ) | k = Write ( certain ) )
152
152
}
@@ -183,7 +183,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
183
183
}
184
184
185
185
predicate lastRefIsRead ( BasicBlock bb , SourceVariable v ) {
186
- maxRefRank ( bb , v ) = refRank ( bb , _, v , Read ( _ ) )
186
+ maxRefRank ( bb , v ) = refRank ( bb , _, v , Read ( ) )
187
187
}
188
188
189
189
/**
@@ -213,7 +213,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
213
213
*/
214
214
predicate liveAtEntry ( BasicBlock bb , SourceVariable v ) {
215
215
// The first read or certain write to `v` inside `bb` is a read
216
- refRank ( bb , _, v , Read ( _ ) ) = firstReadOrCertainWrite ( bb , v )
216
+ refRank ( bb , _, v , Read ( ) ) = firstReadOrCertainWrite ( bb , v )
217
217
or
218
218
// There is no certain write to `v` inside `bb`, but `v` is live at entry
219
219
// to a successor basic block of `bb`
@@ -237,7 +237,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
237
237
rnk = maxRefRank ( bb , v ) and
238
238
liveAtExit ( bb , v )
239
239
or
240
- kind = Read ( _ )
240
+ kind = Read ( )
241
241
or
242
242
exists ( RefKind nextKind |
243
243
liveAtRank ( bb , _, v , rnk + 1 ) and
0 commit comments