@@ -160,17 +160,62 @@ signature module Semantic {
160160 /** Gets a tiebreaker id in case `getBlockId1` is not unique. */
161161 default string getBlockId2 ( BasicBlock bb ) { result = "" }
162162
163+ /**
164+ * A guard in the range analysis.
165+ */
163166 class Guard {
167+ /**
168+ * Gets a string representation of the guard.
169+ */
164170 string toString ( ) ;
165171
172+ /**
173+ * Gets the basic block associated with the guard.
174+ */
166175 BasicBlock getBasicBlock ( ) ;
167176
177+ /**
178+ * Gets the guard as an expression, if any.
179+ */
168180 Expr asExpr ( ) ;
169181
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+ */
170195 predicate directlyControls ( BasicBlock controlled , boolean branch ) ;
171196
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+ */
172202 predicate isEquality ( Expr e1 , Expr e2 , boolean polarity ) ;
173203
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+ */
174219 predicate hasBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , boolean branch ) ;
175220 }
176221
@@ -194,18 +239,50 @@ signature module Semantic {
194239 /** Gets the type of an expression. */
195240 Type getExprType ( Expr e ) ;
196241
242+ /**
243+ * A static single-assignment (SSA) variable.
244+ */
197245 class SsaVariable {
246+ /**
247+ * Gets an expression reading the value of this SSA variable.
248+ */
198249 Expr getAUse ( ) ;
199250
251+ /**
252+ * Gets the basic block where this SSA variable is defined.
253+ */
200254 BasicBlock getBasicBlock ( ) ;
201255 }
202256
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+ */
203273 class SsaPhiNode extends SsaVariable {
204274 /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
205275 predicate hasInputFromBlock ( SsaVariable inp , BasicBlock bb ) ;
206276 }
207277
278+ /**
279+ * An SSA variable representing the value of an explicit update of the source variable.
280+ */
208281 class SsaExplicitUpdate extends SsaVariable {
282+ /**
283+ * Gets the expression that defines the value of the variable in this
284+ * update.
285+ */
209286 Expr getDefiningExpr ( ) ;
210287 }
211288
@@ -296,11 +373,32 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
296373}
297374
298375signature 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+ */
299384 class SemBound {
385+ /**
386+ * Gets a string representation of this bound.
387+ */
300388 string toString ( ) ;
301389
390+ /**
391+ * Gets the location of this bound.
392+ */
302393 Location getLocation ( ) ;
303394
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+ */
304402 Sem:: Expr getExpr ( D:: Delta delta ) ;
305403 }
306404
0 commit comments