@@ -175,37 +175,49 @@ predicate excludeNode(Node n) {
175175 excludeNode ( n .getParentNode ( ) )
176176}
177177
178+ private newtype TPos =
179+ PosBefore ( ) or
180+ PosAt ( ) or
181+ PosAfter ( ) or
182+ PosBeforeDestructors ( ) or
183+ PosAfterDestructors ( )
184+
185+ /** A `Pos` without a `bindingset` requirement on the constructor. */
186+ private class AnyPos extends TPos {
187+ string toString ( ) { result = "Pos" }
188+ }
189+
178190/**
179191 * A constant that indicates the type of sub-node in a pair of `(Node, Pos)`.
180192 * See the comment block at the top of this file.
181193 */
182- private class Pos extends int {
194+ private class Pos extends AnyPos {
183195 // This is to make sure we get compile errors in code that forgets to restrict a `Pos`.
184196 bindingset [ this ]
185197 Pos ( ) { any ( ) }
186198
187199 /** Holds if this is the position just _before_ the associated `Node`. */
188- predicate isBefore ( ) { this = - 1 }
200+ predicate isBefore ( ) { this = PosBefore ( ) }
189201
190202 /** Holds if `(n, this)` is the sub-node that represents `n` itself. */
191- predicate isAt ( ) { this = 0 }
203+ predicate isAt ( ) { this = PosAt ( ) }
192204
193205 /** Holds if this is the position just _after_ the associated `Node`. */
194- predicate isAfter ( ) { this = 1 }
206+ predicate isAfter ( ) { this = PosAfter ( ) }
195207
196208 /**
197209 * Holds if `(n, this)` is the virtual sub-node that comes just _before_ any
198210 * implicit destructor calls following `n`. The node `n` will be some node
199211 * that may be followed by local variables going out of scope.
200212 */
201- predicate isBeforeDestructors ( ) { this = 2 }
213+ predicate isBeforeDestructors ( ) { this = PosBeforeDestructors ( ) }
202214
203215 /**
204216 * Holds if `(n, this)` is the virtual sub-node that comes just _after_ any
205217 * implicit destructor calls following `n`. The node `n` will be some node
206218 * that may be followed by local variables going out of scope.
207219 */
208- predicate isAfterDestructors ( ) { this = 3 }
220+ predicate isAfterDestructors ( ) { this = PosAfterDestructors ( ) }
209221
210222 pragma [ inline]
211223 predicate nodeBefore ( Node n , Node nEq ) { this .isBefore ( ) and n = nEq }
@@ -503,26 +515,51 @@ private Node getLastControlOrderChild(Node n) {
503515 result = getControlOrderChildDense ( n , max ( int i | exists ( getControlOrderChildDense ( n , i ) ) ) )
504516}
505517
518+ private newtype TSpec =
519+ SpecPos ( AnyPos p ) or
520+ SpecAround ( ) or
521+ SpecAroundDestructors ( ) or
522+ SpecBarrier ( )
523+
524+ /** A `Spec` without a `bindingset` requirement on the constructor. */
525+ private class AnySpec extends TSpec {
526+ string toString ( ) { result = "Spec" }
527+ }
528+
506529/**
507530 * A constant that represents two positions: one position for when it's used as
508531 * the _source_ of a sub-edge, and another position for when it's used as the
509532 * _target_. Values include all the values of `Pos`, which resolve to
510533 * themselves as both source and target, as well as two _around_ values and a
511534 * _barrier_ value.
512535 */
513- private class Spec extends Pos {
536+ private class Spec extends AnySpec {
514537 bindingset [ this ]
515538 Spec ( ) { any ( ) }
516539
517- // Values -1 .. 3 are used by Pos
540+ /** See Pos.isBefore. */
541+ predicate isBefore ( ) { this = SpecPos ( PosBefore ( ) ) }
542+
543+ /** See Pos.isAt. */
544+ predicate isAt ( ) { this = SpecPos ( PosAt ( ) ) }
545+
546+ /** See Pos.isAfter. */
547+ predicate isAfter ( ) { this = SpecPos ( PosAfter ( ) ) }
548+
549+ /** See Pos.isBeforeDestructors. */
550+ predicate isBeforeDestructors ( ) { this = SpecPos ( PosBeforeDestructors ( ) ) }
551+
552+ /** See Pos.isAfterDestructors. */
553+ predicate isAfterDestructors ( ) { this = SpecPos ( PosAfterDestructors ( ) ) }
554+
518555 /**
519556 * Holds if this spec, when used on a node `n` between `(n1, p1)` and
520557 * `(n2, p2)`, should add the following sub-edges.
521558 *
522559 * (n1, p1) ----> before(n)
523560 * after(n) ----> (n2, p2)
524561 */
525- predicate isAround ( ) { this = 4 }
562+ predicate isAround ( ) { this = SpecAround ( ) }
526563
527564 /**
528565 * Holds if this spec, when used on a node `n` between `(n1, p1)` and
@@ -531,17 +568,16 @@ private class Spec extends Pos {
531568 * (n1, p1) ----> beforeDestructors(n)
532569 * afterDestructors(n) ----> (n2, p2)
533570 */
534- predicate isAroundDestructors ( ) { this = 5 }
571+ predicate isAroundDestructors ( ) { this = SpecAroundDestructors ( ) }
535572
536573 /**
537574 * Holds if this node is a _barrier_. A barrier resolves to no positions and
538575 * can be inserted between nodes that should have no sub-edges between them.
539576 */
540- predicate isBarrier ( ) { this = 6 }
577+ predicate isBarrier ( ) { this = SpecBarrier ( ) }
541578
542579 Pos getSourcePos ( ) {
543- this = [ - 1 .. 3 ] and
544- result = this
580+ this = SpecPos ( result )
545581 or
546582 this .isAround ( ) and
547583 result .isAfter ( )
@@ -551,8 +587,7 @@ private class Spec extends Pos {
551587 }
552588
553589 Pos getTargetPos ( ) {
554- this = [ - 1 .. 3 ] and
555- result = this
590+ this = SpecPos ( result )
556591 or
557592 this .isAround ( ) and
558593 result .isBefore ( )
0 commit comments