@@ -160,17 +160,62 @@ signature module Semantic {
160
160
/** Gets a tiebreaker id in case `getBlockId1` is not unique. */
161
161
default string getBlockId2 ( BasicBlock bb ) { result = "" }
162
162
163
+ /**
164
+ * A guard in the range analysis.
165
+ */
163
166
class Guard {
167
+ /**
168
+ * Gets a string representation of the guard.
169
+ */
164
170
string toString ( ) ;
165
171
172
+ /**
173
+ * Gets the basic block associated with the guard.
174
+ */
166
175
BasicBlock getBasicBlock ( ) ;
167
176
177
+ /**
178
+ * Gets the guard as an expression, if any.
179
+ */
168
180
Expr asExpr ( ) ;
169
181
182
+ /**
183
+ * Holds if the guard directly controls a given basic block. For example in
184
+ * the following code, the guard `(x > y)` directly controls the block
185
+ * beneath it:
186
+ * ```
187
+ * if (x > y)
188
+ * {
189
+ * Console.WriteLine("x is greater than y");
190
+ * }
191
+ * ```
192
+ * `branch` indicates whether the basic block is entered when the guard
193
+ * evaluates to `true` or when it evaluates to `false`.
194
+ */
170
195
predicate directlyControls ( BasicBlock controlled , boolean branch ) ;
171
196
197
+ /**
198
+ * Holds if this guard is an equality test between `e1` and `e2`. If the
199
+ * test is negated, that is `!=`, then `polarity` is false, otherwise
200
+ * `polarity` is true.
201
+ */
172
202
predicate isEquality ( Expr e1 , Expr e2 , boolean polarity ) ;
173
203
204
+ /**
205
+ * Holds if there is a branch edge between two basic blocks. For example
206
+ * in the following C code, there are two branch edges from the basic block
207
+ * containing the condition `(x > y)` to the beginnings of the true and
208
+ * false blocks that follow:
209
+ * ```
210
+ * if (x > y) {
211
+ * printf("x is greater than y\n");
212
+ * } else {
213
+ * printf("x is not greater than y\n");
214
+ * }
215
+ * ```
216
+ * `branch` indicates whether the second basic block is the one entered
217
+ * when the guard evaluates to `true` or when it evaluates to `false`.
218
+ */
174
219
predicate hasBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , boolean branch ) ;
175
220
}
176
221
@@ -194,18 +239,50 @@ signature module Semantic {
194
239
/** Gets the type of an expression. */
195
240
Type getExprType ( Expr e ) ;
196
241
242
+ /**
243
+ * A static single-assignment (SSA) variable.
244
+ */
197
245
class SsaVariable {
246
+ /**
247
+ * Gets an expression reading the value of this SSA variable.
248
+ */
198
249
Expr getAUse ( ) ;
199
250
251
+ /**
252
+ * Gets the basic block where this SSA variable is defined.
253
+ */
200
254
BasicBlock getBasicBlock ( ) ;
201
255
}
202
256
257
+ /**
258
+ * A phi node in the SSA form. A phi node is a kind of node in the SSA form
259
+ * that represents a merge point where multiple control flow paths converge
260
+ * and the value of a variable needs to be selected according to which
261
+ * control flow path was taken. For example, in the following Ruby code:
262
+ * ```rb
263
+ * if b
264
+ * x = 0
265
+ * else
266
+ * x = 1
267
+ * end
268
+ * puts x
269
+ * ```
270
+ * A phi node for `x` is inserted just before the call `puts x`, since the
271
+ * value of `x` may come from either `x = 0` or `x = 1`.
272
+ */
203
273
class SsaPhiNode extends SsaVariable {
204
274
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
205
275
predicate hasInputFromBlock ( SsaVariable inp , BasicBlock bb ) ;
206
276
}
207
277
278
+ /**
279
+ * An SSA variable representing the value of an explicit update of the source variable.
280
+ */
208
281
class SsaExplicitUpdate extends SsaVariable {
282
+ /**
283
+ * Gets the expression that defines the value of the variable in this
284
+ * update.
285
+ */
209
286
Expr getDefiningExpr ( ) ;
210
287
}
211
288
@@ -296,11 +373,32 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
296
373
}
297
374
298
375
signature module BoundSig< LocationSig Location, Semantic Sem, DeltaSig D> {
376
+ /**
377
+ * A bound that the range analysis can infer for a variable. This includes
378
+ * constant bounds represented by the abstract value zero, SSA bounds for when
379
+ * a variable is bounded by the value of a different variable, and possibly
380
+ * other abstract values that may be useful variable bounds. Since all bounds
381
+ * are combined with an integer delta there's no need to represent constant
382
+ * bounds other than zero.
383
+ */
299
384
class SemBound {
385
+ /**
386
+ * Gets a string representation of this bound.
387
+ */
300
388
string toString ( ) ;
301
389
390
+ /**
391
+ * Gets the location of this bound.
392
+ */
302
393
Location getLocation ( ) ;
303
394
395
+ /**
396
+ * Gets an expression that equals this bound plus `delta`.
397
+ *
398
+ * For the zero-bound this gets integer constants equal to `delta`, for any
399
+ * value `delta`. For other bounds this gets expressions equal to the bound
400
+ * and `delta = 0`.
401
+ */
304
402
Sem:: Expr getExpr ( D:: Delta delta ) ;
305
403
}
306
404
0 commit comments