001    /* Copyright (c) 2005-2008, Torbjorn Ekman
002     *                    2015, Jesper Öqvist <joqvist@google.com>
003     * All rights reserved.
004     *
005     * Redistribution and use in source and binary forms, with or without
006     * modification, are permitted provided that the following conditions are met:
007     *
008     * 1. Redistributions of source code must retain the above copyright notice,
009     * this list of conditions and the following disclaimer.
010     *
011     * 2. Redistributions in binary form must reproduce the above copyright notice,
012     * this list of conditions and the following disclaimer in the documentation
013     * and/or other materials provided with the distribution.
014     *
015     * 3. Neither the name of the copyright holder nor the names of its
016     * contributors may be used to endorse or promote products derived from this
017     * software without specific prior written permission.
018     *
019     * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
020     * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
021     * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
022     * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
023     * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
024     * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
025     * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
026     * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
027     * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
028     * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
029     * POSSIBILITY OF SUCH DAMAGE.
030     */
031    
032    aspect DefiniteAssignment {
033    
034      public void ASTNode.definiteAssignment() {
035      }
036    
037      inh boolean Expr.isDest();
038      eq Program.getChild().isDest() = false;
039      eq AssignSimpleExpr.getDest().isDest() = true;
040      eq AssignExpr.getDest().isDest() = true;
041      eq AssignExpr.getSource().isDest() = false;
042      eq TypeDecl.getChild().isDest() = false;
043      eq AbstractDot.getLeft().isDest() = false;
044    
045      eq ImportDecl.getAccess().isDest() = false;
046    
047      inh boolean Expr.isSource();
048      eq Program.getChild().isSource() = true;
049      eq AssignSimpleExpr.getDest().isSource() = false;
050      eq AssignExpr.getDest().isSource() = true;
051      eq AssignExpr.getSource().isSource() = true;
052      eq TypeDecl.getChild().isSource() = true;
053      eq AbstractDot.getLeft().isSource() = true;
054      eq ImportDecl.getAccess().isSource() = true;
055    
056      eq ArrayAccess.getExpr().isDest() = false;
057      eq ArrayAccess.getExpr().isSource() = true;
058      eq ArrayTypeWithSizeAccess.getExpr().isDest() = false;
059      eq ArrayTypeWithSizeAccess.getExpr().isSource() = true;
060    
061      eq FieldDeclaration.getInit().isSource() = true;
062      eq VariableDeclaration.getInit().isSource() = true;
063      eq VariableDecl.getInit().isSource() = true; // is this needed?
064      eq ArrayInit.getInit().isSource() = true;
065    
066      eq Unary.getOperand().isSource() = true;
067      eq PostfixExpr.getOperand().isDest() = true;
068      eq PreIncExpr.getOperand().isDest() = true;
069      eq PreDecExpr.getOperand().isDest() = true;
070    
071      inh boolean Expr.isIncOrDec();
072      eq Program.getChild().isIncOrDec() = false;
073      eq CompilationUnit.getTypeDecl().isIncOrDec() = false;
074      eq Block.getStmt().isIncOrDec() = false;
075      eq VarDeclStmt.getSingleDecl().isIncOrDec() = false;
076      eq PostfixExpr.getOperand().isIncOrDec() = true;
077      eq PreIncExpr.getOperand().isIncOrDec() = true;
078      eq PreDecExpr.getOperand().isIncOrDec() = true;
079    
080    
081      syn Variable Expr.varDecl() = null;
082      eq AbstractDot.varDecl() = lastAccess().varDecl();
083      eq VarAccess.varDecl() = decl();
084      eq ParExpr.varDecl() = getExpr().varDecl();
085    
086      public void PostfixExpr.definiteAssignment() {
087        if (getOperand().isVariable()) {
088          Variable v = getOperand().varDecl();
089          if (v != null && v.isFinal()) {
090            error("++ and -- can not be applied to final variable " + v);
091          }
092        }
093      }
094    
095      public void PreIncExpr.definiteAssignment() {
096        if (getOperand().isVariable()) {
097          Variable v = getOperand().varDecl();
098          if (v != null && v.isFinal()) {
099            error("++ and -- can not be applied to final variable " + v);
100          }
101        }
102      }
103    
104      public void PreDecExpr.definiteAssignment() {
105        if (getOperand().isVariable()) {
106          Variable v = getOperand().varDecl();
107          if (v != null && v.isFinal()) {
108            error("++ and -- can not be applied to final variable " + v);
109          }
110        }
111      }
112    
113      // final variables with a constant initializer are considered values and not variables
114      syn boolean VariableDeclaration.isBlankFinal() = isFinal() && (!hasInit() || !getInit().isConstant());
115      syn boolean VariableDeclaration.isValue() = isFinal() && hasInit() && getInit().isConstant();
116    
117      public void VarAccess.definiteAssignment() {
118        if (isSource()) {
119          if (decl() instanceof VariableDeclaration) {
120            VariableDeclaration v = (VariableDeclaration) decl();
121            if (v.isValue()) {
122            } else if (v.isBlankFinal()) {
123              if (!isDAbefore(v)) {
124                errorf("Final variable %s is not assigned before used", v.name());
125              }
126            } else {
127              if (!isDAbefore(v)) {
128                errorf("Local variable %s is not assigned before used", v.name());
129              }
130            }
131          } else if (decl() instanceof FieldDeclaration && !isQualified()) {
132            FieldDeclaration f = (FieldDeclaration) decl();
133            if (f.isFinal() && !f.hasInit() && !isDAbefore(f)) {
134              errorf("Final field %s is not assigned before used", f);
135            }
136          }
137    
138        }
139        if (isDest()) {
140          Variable v = decl();
141          // Blank final field
142          if (v.isFinal() && v.isBlank() && !hostType().instanceOf(v.hostType())) {
143            error("The final variable is not a blank final in this context, so it may not be assigned.");
144          } else if (v.isFinal() && isQualified() && (!qualifier().isThisAccess() || ((Access) qualifier()).isQualified())) {
145            errorf("the blank final field %s may only be assigned by simple name", v.name());
146          }
147    
148          // local variable or parameter
149          else if (v instanceof VariableDeclaration) {
150            VariableDeclaration var = (VariableDeclaration) v;
151            //System.out.println("### is variable");
152            if (!var.isValue() && var.getParent().getParent().getParent() instanceof SwitchStmt && var.isFinal()) {
153              if (!isDUbefore(var)) {
154                errorf("Final variable %s may only be assigned once", var.name());
155              }
156            } else if (var.isValue()) {
157              if (var.hasInit() || !isDUbefore(var)) {
158                errorf("Final variable %s may only be assigned once", var.name());
159              }
160            } else if (var.isBlankFinal()) {
161              if (var.hasInit() || !isDUbefore(var)) {
162                errorf("Final variable %s may only be assigned once", var.name());
163              }
164            }
165            if (var.isFinal() && (var.hasInit() || !isDUbefore(var))) {
166            //if (var.isFinal() && ((var.hasInit() && var.getInit().isConstant()) || !isDUbefore(var))) {
167            }
168          }
169          // field
170          else if (v instanceof FieldDeclaration) {
171            FieldDeclaration f = (FieldDeclaration) v;
172            if (f.isFinal()) {
173              if (f.hasInit()) {
174                errorf("already initialized final field %s can not be assigned", f.name());
175              } else {
176                BodyDecl bodyDecl = enclosingBodyDecl();
177                if (!(bodyDecl instanceof ConstructorDecl) && !(bodyDecl instanceof InstanceInitializer) && !(bodyDecl instanceof StaticInitializer) && !(bodyDecl instanceof FieldDeclaration)) {
178                  errorf("final field %s may only be assigned in constructors and initializers", f.name());
179                } else if (!isDUbefore(f)) {
180                  errorf("blank final field %s may only be assigned once", f.name());
181                }
182              }
183            }
184          } else if (v.isParameter()) {
185            // 8.4.1
186            if (v.isFinal()) {
187              errorf("Final parameter %s may not be assigned", v.name());
188            }
189          }
190    
191        }
192      }
193    
194      public void FieldDeclaration.definiteAssignment() {
195        super.definiteAssignment();
196        if (isBlank() && isFinal() && isClassVariable()) {
197          boolean found = false;
198          TypeDecl typeDecl = hostType();
199          for (int i = 0; i < typeDecl.getNumBodyDecl(); i++) {
200            if (typeDecl.getBodyDecl(i) instanceof StaticInitializer) {
201              StaticInitializer s = (StaticInitializer) typeDecl.getBodyDecl(i);
202              if (s.isDAafter(this)) {
203                found = true;
204              }
205            }
206    
207            else if (typeDecl.getBodyDecl(i) instanceof FieldDeclaration) {
208              FieldDeclaration f = (FieldDeclaration) typeDecl.getBodyDecl(i);
209              if (f.isStatic() && f.isDAafter(this)) {
210                found = true;
211              }
212            }
213    
214          }
215          if (!found) {
216            errorf("blank final class variable %s in %s is not definitely assigned in static initializer",
217                name(), hostType().typeName());
218          }
219    
220        }
221        if (isBlank() && isFinal() && isInstanceVariable()) {
222          TypeDecl typeDecl = hostType();
223          boolean found = false;
224          for (int i = 0; !found && i < typeDecl.getNumBodyDecl(); i++) {
225            if (typeDecl.getBodyDecl(i) instanceof FieldDeclaration) {
226              FieldDeclaration f = (FieldDeclaration) typeDecl.getBodyDecl(i);
227              if (!f.isStatic() && f.isDAafter(this)) {
228                found = true;
229              }
230            } else if (typeDecl.getBodyDecl(i) instanceof InstanceInitializer) {
231              InstanceInitializer ii = (InstanceInitializer) typeDecl.getBodyDecl(i);
232              if (ii.getBlock().isDAafter(this)) {
233                found = true;
234              }
235            }
236          }
237          for (Iterator iter = typeDecl.constructors().iterator(); !found && iter.hasNext(); ) {
238            ConstructorDecl c = (ConstructorDecl) iter.next();
239            if (!c.isDAafter(this)) {
240              errorf("blank final instance variable %s in %s is not definitely assigned after %s",
241                  name(), hostType().typeName(), c.signature());
242            }
243          }
244        }
245        if (isBlank() && hostType().isInterfaceDecl()) {
246          errorf("variable  %s in %s which is an interface must have an initializer",
247              name(), hostType().typeName());
248        }
249      }
250    }
251    
252    aspect DA {
253      syn lazy boolean ConditionalExpr.booleanOperator() = getTrueExpr().type().isBoolean() && getFalseExpr().type().isBoolean();
254    
255      inh boolean Stmt.isDAbefore(Variable v);
256      inh boolean VariableDeclaration.isDAbefore(Variable v);
257      syn lazy boolean Stmt.isDAafter(Variable v);
258      inh boolean Expr.isDAbefore(Variable v);
259      syn boolean Expr.isDAafter(Variable v);
260    
261      syn lazy boolean Binary.isDAafter(Variable v);
262      syn lazy boolean AbstractDot.isDAafter(Variable v);
263    
264      inh lazy boolean TypeDecl.isDAbefore(Variable v);
265    
266      syn lazy boolean BodyDecl.isDAafter(Variable v) = true;
267    
268      eq BodyDecl.getChild().isDAbefore(Variable v) = isDAbefore(v, this);
269    
270      syn lazy boolean BodyDecl.isDAbefore(Variable v) = isDAbefore(v, this);
271    
272      inh boolean BodyDecl.isDAbefore(Variable v, BodyDecl b);
273    
274      eq TypeDecl.getChild().isDAbefore(Variable v, BodyDecl b) {
275        //if (b instanceof MethodDecl || b instanceof MemberTypeDecl) {
276        if (!v.isInstanceVariable() && !v.isClassVariable()) {
277          if (v.hostType() != this) {
278            return isDAbefore(v);
279          }
280          return false;
281        }
282        if (b instanceof FieldDeclaration && !((FieldDeclaration) b).isStatic() && v.isClassVariable()) {
283          return true;
284        }
285    
286        if (b instanceof MethodDecl) {
287          return true;
288        }
289        if (b instanceof MemberTypeDecl && v.isBlank() && v.isFinal() && v.hostType() == this) {
290          return true;
291        }
292        if (v.isClassVariable() || v.isInstanceVariable()) {
293          if (v.isFinal() &&  v.hostType() != this && instanceOf(v.hostType())) {
294            return true;
295          }
296    
297          boolean search = true;
298          if (b instanceof ConstructorDecl) {
299            search = false;
300          }
301    
302          for (int i = getNumBodyDecl() - 1; i >= 0; --i) {
303            BodyDecl decl = getBodyDecl(i);
304            if (b == decl) {
305              search = false;
306              continue;
307            }
308            if (search) {
309              continue;
310            }
311            if (decl instanceof FieldDeclaration) {
312              FieldDeclaration f = (FieldDeclaration) decl;
313              if ((v.isClassVariable() && f.isStatic()) || (v.isInstanceVariable() && !f.isStatic())) {
314                boolean c = f.isDAafter(v);
315                //System.err.println("DefiniteAssignment: is " + v.name() + " DA after index " + i + ", " + f + ": " + c);
316                return c;
317                //return f.isDAafter(v);
318              }
319            } else if (decl instanceof StaticInitializer && v.isClassVariable()) {
320              StaticInitializer si = (StaticInitializer) decl;
321              return si.isDAafter(v);
322            } else if (decl instanceof InstanceInitializer && v.isInstanceVariable()) {
323              InstanceInitializer ii = (InstanceInitializer) decl;
324              return ii.isDAafter(v);
325            }
326          }
327        }
328        return isDAbefore(v);
329      }
330    
331      eq InstanceInitializer.isDAafter(Variable v) = getBlock().isDAafter(v);
332      eq StaticInitializer.isDAafter(Variable v) = getBlock().isDAafter(v);
333    
334      eq ConstructorDecl.isDAafter(Variable v) = getBlock().isDAafter(v) && getBlock().checkReturnDA(v);
335      eq ConstructorAccess.isDAafter(Variable v) = decl().isDAafter(v);
336      eq SuperConstructorAccess.isDAafter(Variable v) = isDAbefore(v);
337      eq ConstructorDecl.getBlock().isDAbefore(Variable v) = hasConstructorInvocation() ? getConstructorInvocation().isDAafter(v) : isDAbefore(v);
338    
339      syn lazy boolean Block.checkReturnDA(Variable v) {
340        HashSet set = new HashSet();
341        collectBranches(set);
342        for (Iterator iter = set.iterator(); iter.hasNext(); ) {
343          Object o = iter.next();
344          if (o instanceof ReturnStmt) {
345            ReturnStmt stmt = (ReturnStmt) o;
346            if (!stmt.isDAafterReachedFinallyBlocks(v)) {
347              return false;
348            }
349          }
350        }
351        return true;
352      }
353    
354      eq FieldDeclaration.isDAafter(Variable v) {
355        if (v == this) {
356          return hasInit();
357        }
358        return hasInit() ? getInit().isDAafter(v) : isDAbefore(v);
359      }
360    
361      eq FieldDeclaration.getInit().isDAbefore(Variable v) {
362        return isDAbefore(v);
363      }
364    
365      // missing assignment => not DA
366      eq Program.getChild().isDAbefore(Variable v) = false;
367      eq Stmt.isDAafter(Variable v) = isDAbefore(v);
368      /*eq Stmt.isDAafter(Variable v) {
369        //System.out.println("### isDAafter reached in " + getClass().getName());
370        //throw new NullPointerException();
371        throw new Error("Can not compute isDAafter for " + getClass().getName() + " at " + errorPrefix());
372      }*/
373    
374      syn boolean Expr.isDAafterTrue(Variable v);
375      syn boolean Expr.isDAafterFalse(Variable v);
376    
377      eq AbstractDot.isDAafterTrue(Variable v) = isDAafter(v);
378      eq AbstractDot.isDAafterFalse(Variable v) = isDAafter(v);
379    
380      // JLSv3 16.1.7
381      eq Expr.isDAafterFalse(Variable v) = isTrue() || isDAafter(v);
382      eq Expr.isDAafterTrue(Variable v) = isFalse() || isDAafter(v);
383    
384      eq Expr.isDAafter(Variable v) = isDAbefore(v);
385    
386      eq InstanceOfExpr.isDAafterFalse(Variable v) = isDAafter(v);
387      eq InstanceOfExpr.isDAafterTrue(Variable v) = isDAafter(v);
388    
389      eq ParExpr.isDAafterTrue(Variable v) = isFalse() || getExpr().isDAafterTrue(v);
390      eq ParExpr.isDAafterFalse(Variable v) = isTrue() || getExpr().isDAafterFalse(v);
391    
392      syn lazy boolean VarAccess.isDAafter(Variable v) = isDAbefore(v);
393    
394      eq AbstractDot.getRight().isDAbefore(Variable v) = getLeft().isDAafter(v);
395      eq AbstractDot.isDAafter(Variable v) = lastAccess().isDAafter(v);
396    
397      eq ArrayAccess.isDAafter(Variable v) = getExpr().isDAafter(v);
398      eq ArrayTypeAccess.isDAafter(Variable v) = getAccess().isDAafter(v);
399      eq ArrayTypeWithSizeAccess.isDAafter(Variable v) = getExpr().isDAafter(v);
400      eq ArrayTypeWithSizeAccess.getExpr().isDAbefore(Variable v) = getAccess().isDAafter(v);
401    
402      // 16.1.2 1st bullet
403      eq AndLogicalExpr.isDAafterTrue(Variable v) = isFalse() || getRightOperand().isDAafterTrue(v);
404      // 16.1.2 2nd bullet
405      eq AndLogicalExpr.isDAafterFalse(Variable v) = isTrue() || (getLeftOperand().isDAafterFalse(v) && getRightOperand().isDAafterFalse(v));
406      // 16.1.2 3rd bullet
407      eq AndLogicalExpr.getLeftOperand().isDAbefore(Variable v) = isDAbefore(v);
408      // 16.1.2 4th bullet
409      eq AndLogicalExpr.getRightOperand().isDAbefore(Variable v) = getLeftOperand().isDAafterTrue(v);
410      // 16.1.2 5th bullet
411      eq AndLogicalExpr.isDAafter(Variable v) = isDAafterTrue(v) && isDAafterFalse(v);
412    
413      eq OrLogicalExpr.isDAafterTrue(Variable v) = isFalse() || (getLeftOperand().isDAafterTrue(v) && getRightOperand().isDAafterTrue(v));
414      eq OrLogicalExpr.isDAafterFalse(Variable v) = isTrue() || getRightOperand().isDAafterFalse(v);
415      eq OrLogicalExpr.getLeftOperand().isDAbefore(Variable v) = isDAbefore(v);
416      eq OrLogicalExpr.getRightOperand().isDAbefore(Variable v) = getLeftOperand().isDAafterFalse(v);
417      eq OrLogicalExpr.isDAafter(Variable v) = isDAafterTrue(v) && isDAafterFalse(v);
418    
419      eq LogNotExpr.isDAafterTrue(Variable v) = isFalse() || getOperand().isDAafterFalse(v);
420      eq LogNotExpr.isDAafterFalse(Variable v) = isTrue() || getOperand().isDAafterTrue(v);
421      eq LogNotExpr.getOperand().isDAbefore(Variable v) = isDAbefore(v);
422      eq LogNotExpr.isDAafter(Variable v) = isDAafterTrue(v) && isDAafterFalse(v);
423    
424      eq ConditionalExpr.isDAafterTrue(Variable v) = isFalse() || (getTrueExpr().isDAafterTrue(v) && getFalseExpr().isDAafterTrue(v));
425      eq ConditionalExpr.isDAafterFalse(Variable v) = isTrue() || (getTrueExpr().isDAafterFalse(v) && getFalseExpr().isDAafterFalse(v));
426      eq ConditionalExpr.getCondition().isDAbefore(Variable v) = isDAbefore(v);
427      eq ConditionalExpr.getTrueExpr().isDAbefore(Variable v) = getCondition().isDAafterTrue(v);
428      eq ConditionalExpr.getFalseExpr().isDAbefore(Variable v) = getCondition().isDAafterFalse(v);
429      eq ConditionalExpr.isDAafter(Variable v) = booleanOperator() ? isDAafterTrue(v) && isDAafterFalse(v) : getTrueExpr().isDAafter(v) && getFalseExpr().isDAafter(v);
430    
431      eq AssignExpr.isDAafter(Variable v) = (getDest().isVariable() && getDest().varDecl() == v) || getSource().isDAafter(v);
432      eq AssignExpr.getSource().isDAbefore(Variable v) = getDest().isDAafter(v);
433      eq AssignExpr.getDest().isDAbefore(Variable v) = isDAbefore(v);
434    
435      eq AssignExpr.isDAafterTrue(Variable v) = isFalse() || isDAafter(v);
436      eq AssignExpr.isDAafterFalse(Variable v) = isTrue() || isDAafter(v);
437    
438      eq ParExpr.isDAafter(Variable v) = getExpr().isDAafter(v);
439      eq Unary.isDAafter(Variable v) = getOperand().isDAafter(v);
440      eq CastExpr.isDAafter(Variable v) = getExpr().isDAafter(v);
441    
442      syn lazy boolean Binary.isDAafterTrue(Variable v) = isFalse() || getRightOperand().isDAafter(v);
443      syn lazy boolean Binary.isDAafterFalse(Variable v) = isTrue() || getRightOperand().isDAafter(v);
444    
445      eq Binary.isDAafter(Variable v) = getRightOperand().isDAafter(v);
446      eq Binary.getRightOperand().isDAbefore(Variable v) = getLeftOperand().isDAafter(v);
447    
448      eq InstanceOfExpr.isDAafter(Variable v) = getExpr().isDAafter(v);
449    
450      eq MethodAccess.getArg(int i).isDAbefore(Variable v) = computeDAbefore(i, v);
451      syn lazy boolean MethodAccess.computeDAbefore(int i, Variable v) =
452          i == 0 ? isDAbefore(v) : getArg(i-1).isDAafter(v);
453      eq MethodAccess.isDAafter(Variable v) = getNumArg() == 0 ? isDAbefore(v) : getArg(getNumArg()-1).isDAafter(v);
454      eq MethodAccess.isDAafterTrue(Variable v) = isFalse() || (getNumArg() == 0 ? isDAbefore(v) : getArg(getNumArg()-1).isDAafter(v));
455      eq MethodAccess.isDAafterFalse(Variable v) = isTrue() || (getNumArg() == 0 ? isDAbefore(v) : getArg(getNumArg()-1).isDAafter(v));
456    
457      eq EmptyStmt.isDAafter(Variable v) = isDAbefore(v);
458    
459      eq AssertStmt.isDAafter(Variable v) = getCondition().isDAafter(v);
460      eq AssertStmt.getMessage().isDAbefore(Variable v) = getCondition().isDAafter(v);
461    
462      syn lazy boolean ClassInstanceExpr.isDAafterInstance(Variable v) {
463        if (getNumArg() == 0) {
464          return isDAbefore(v);
465        }
466        return getArg(getNumArg()-1).isDAafter(v);
467      }
468      eq ClassInstanceExpr.isDAafter(Variable v) = isDAafterInstance(v);
469      eq ClassInstanceExpr.getArg(int i).isDAbefore(Variable v) = computeDAbefore(i, v);
470      syn lazy boolean ClassInstanceExpr.computeDAbefore(int i, Variable v) =
471          i == 0 ? isDAbefore(v) : getArg(i-1).isDAafter(v);
472      eq ClassInstanceExpr.getTypeDecl().isDAbefore(Variable v) = isDAafterInstance(v);
473    
474      syn boolean ArrayCreationExpr.isDAafterCreation(Variable v) = getTypeAccess().isDAafter(v);
475      eq ArrayCreationExpr.isDAafter(Variable v) = hasArrayInit() ? getArrayInit().isDAafter(v) : isDAafterCreation(v);
476      eq ArrayCreationExpr.getArrayInit().isDAbefore(Variable v) = isDAafterCreation(v);
477    
478      // 16.2.2 1st bullet
479      eq MethodDecl.getBlock().isDAbefore(Variable v) = v.isFinal() && (v.isClassVariable() || v.isInstanceVariable()) ? true : isDAbefore(v);
480      eq InstanceInitializer.getBlock().isDAbefore(Variable v) = isDAbefore(v);
481      eq StaticInitializer.getBlock().isDAbefore(Variable v) = isDAbefore(v);
482    
483      eq Block.isDAafter(Variable v) = getNumStmt() == 0 ? isDAbefore(v) : getStmt(getNumStmt()-1).isDAafter(v);
484    
485      // 16.2.2 7th bullet
486      eq Block.getStmt(int index).isDAbefore(Variable v) =
487          index == 0 ? isDAbefore(v) : getStmt(index - 1).isDAafter(v);
488      eq VarDeclStmt.getSingleDecl(int index).isDAbefore(Variable v) =
489          index == 0 ? isDAbefore(v) : getSingleDecl(index - 1).isDAafter(v);
490    
491      // 16.2.2 8th, 9th, 10th bullet
492      syn boolean Block.isDUeverywhere(Variable v) = isDUbefore(v) && checkDUeverywhere(v);
493    
494      // 16.2.2 9th, 10th bullet
495      protected boolean ASTNode.checkDUeverywhere(Variable v) {
496        for (int i = 0; i < getNumChild(); i++) {
497          if (!getChild(i).checkDUeverywhere(v)) {
498            return false;
499          }
500        }
501        return true;
502      }
503    
504      protected boolean VarAccess.checkDUeverywhere(Variable v) {
505        if (isDest() && decl() == v) {
506          return false;
507        }
508        return super.checkDUeverywhere(v);
509      }
510      // 16.2.2 9th bullet
511      protected boolean AssignExpr.checkDUeverywhere(Variable v) {
512        if (getDest().isVariable() && getDest().varDecl() == v) {
513          if (!getSource().isDAafter(v)) {
514            return false;
515          }
516        }
517        return super.checkDUeverywhere(v);
518      }
519    
520      // 16.2.2 10th bullet
521      protected boolean PostfixExpr.checkDUeverywhere(Variable v) {
522        if (getOperand().isVariable() && getOperand().varDecl() == v) {
523          if (!isDAbefore(v)) {
524            return false;
525          }
526        }
527        return super.checkDUeverywhere(v);
528      }
529      protected boolean PreIncExpr.checkDUeverywhere(Variable v) {
530        if (getOperand().isVariable() && getOperand().varDecl() == v) {
531          if (!isDAbefore(v)) {
532            return false;
533          }
534        }
535        return super.checkDUeverywhere(v);
536      }
537      protected boolean PreDecExpr.checkDUeverywhere(Variable v) {
538        if (getOperand().isVariable() && getOperand().varDecl() == v) {
539          if (!isDAbefore(v)) {
540            return false;
541          }
542        }
543        return super.checkDUeverywhere(v);
544      }
545    
546      eq LocalClassDeclStmt.isDAafter(Variable v) = isDAbefore(v);
547    
548      eq VarDeclStmt.isDAafter(Variable v) =
549          getSingleDecl(getNumSingleDecl()-1).isDAafter(v);
550    
551      syn lazy boolean VariableDeclaration.isDAafter(Variable v) {
552        if (v == this) {
553          return hasInit();
554        }
555        return hasInit() ? getInit().isDAafter(v) : isDAbefore(v);
556      }
557      eq VariableDeclaration.getInit().isDAbefore(Variable v) = isDAbefore(v);
558    
559      eq ArrayInit.isDAafter(Variable v) = getNumInit() == 0 ? isDAbefore(v) : getInit(getNumInit()-1).isDAafter(v);
560      eq ArrayInit.getInit(int childIndex).isDAbefore(Variable v) = computeDABefore(childIndex, v);
561      // force caching of computation
562      syn lazy boolean ArrayInit.computeDABefore(int childIndex, Variable v) {
563        if (childIndex == 0) {
564          return isDAbefore(v);
565        }
566        int index = childIndex-1;
567        while (index > 0 && getInit(index).isConstant()) {
568          index--;
569        }
570        return getInit(childIndex-1).isDAafter(v);
571      }
572    
573      eq LabeledStmt.getStmt().isDAbefore(Variable v) = isDAbefore(v);
574      eq LabeledStmt.isDAafter(Variable v) {
575        if (!getStmt().isDAafter(v)) {
576          return false;
577        }
578        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
579          BreakStmt stmt = (BreakStmt) iter.next();
580          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
581            return false;
582          }
583        }
584        return true;
585      }
586    
587      eq ExprStmt.isDAafter(Variable v) = getExpr().isDAafter(v);
588      eq ExprStmt.getExpr().isDAbefore(Variable v) = isDAbefore(v);
589    
590      eq IfStmt.isDAafter(Variable v) = hasElse() ? getThen().isDAafter(v) && getElse().isDAafter(v) : getThen().isDAafter(v) && getCondition().isDAafterFalse(v);
591      eq IfStmt.getCondition().isDAbefore(Variable v) = isDAbefore(v);
592      eq IfStmt.getThen().isDAbefore(Variable v) = getCondition().isDAafterTrue(v);
593      eq IfStmt.getElse().isDAbefore(Variable v) = getCondition().isDAafterFalse(v);
594    
595      // 16.2.9 1st bullet
596      eq SwitchStmt.isDAafter(Variable v) {
597        if (!(!noDefaultLabel() || getExpr().isDAafter(v))) {
598          return false;
599        }
600        if (!(!switchLabelEndsBlock() || getExpr().isDAafter(v))) {
601          return false;
602        }
603        if (!assignedAfterLastStmt(v)) {
604          return false;
605        }
606        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
607          BreakStmt stmt = (BreakStmt) iter.next();
608          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
609            return false;
610          }
611        }
612        return true;
613      }
614    
615      syn boolean SwitchStmt.assignedAfterLastStmt(Variable v) =
616          getBlock().isDAafter(v);
617    
618      // 16.2.9 2nd bullet
619      eq SwitchStmt.getExpr().isDAbefore(Variable v) {
620        if (((ASTNode) v).isDescendantTo(this)) {
621          return false;
622        }
623        boolean result = isDAbefore(v);
624        return result;
625      }
626    
627      protected boolean ASTNode.isDescendantTo(ASTNode node) {
628        if (this == node) {
629          return true;
630        }
631        if (getParent() == null) {
632          return false;
633        }
634        return getParent().isDescendantTo(node);
635      }
636    
637      eq SwitchStmt.getBlock().isDAbefore(Variable v) = getExpr().isDAafter(v);
638    
639      syn lazy boolean Case.isDAbefore(Variable v) =
640          getParent().getParent() instanceof Block
641          && ((Block) getParent().getParent()).isDAbefore(v)
642          && super.isDAbefore(v);
643    
644      eq Case.isDAafter(Variable v) = isDAbefore(v);
645    
646      eq WhileStmt.isDAafter(Variable v) {
647        if (!getCondition().isDAafterFalse(v)) {
648          return false;
649        }
650        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
651          BreakStmt stmt = (BreakStmt) iter.next();
652          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
653            return false;
654          }
655        }
656        return true;
657      }
658      eq WhileStmt.getCondition().isDAbefore(Variable v) = isDAbefore(v);
659      eq WhileStmt.getStmt().isDAbefore(Variable v) = getCondition().isDAafterTrue(v);
660    
661      eq DoStmt.isDAafter(Variable v) {
662        if (!getCondition().isDAafterFalse(v)) {
663          return false;
664        }
665        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
666          BreakStmt stmt = (BreakStmt) iter.next();
667          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
668            return false;
669          }
670        }
671        return true;
672      }
673      eq DoStmt.getStmt().isDAbefore(Variable v) = isDAbefore(v);
674      eq DoStmt.getCondition().isDAbefore(Variable v) {
675        if (!getStmt().isDAafter(v)) {
676          return false;
677        }
678        for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
679          ContinueStmt stmt = (ContinueStmt) iter.next();
680          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
681            return false;
682          }
683        }
684        return true;
685      }
686    
687      // 16.2.11 1st bullet
688      eq ForStmt.isDAafter(Variable v) {
689        if (!(!hasCondition() || getCondition().isDAafterFalse(v))) {
690          return false;
691        }
692        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
693          BreakStmt stmt = (BreakStmt) iter.next();
694          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
695            return false;
696          }
697        }
698        return true;
699      }
700      // 16.2.11 2nd bullet
701      eq ForStmt.getInitStmt(int i).isDAbefore(Variable v) = i == 0 ? isDAbefore(v) : getInitStmt(i-1).isDAafter(v);
702      // 16.2.11 3rd bullet
703      syn boolean ForStmt.isDAafterInitialization(Variable v) = getNumInitStmt() == 0 ? isDAbefore(v) : getInitStmt(getNumInitStmt()-1).isDAafter(v);
704      eq ForStmt.getCondition().isDAbefore(Variable v) = isDAafterInitialization(v);
705      // 16.2.11 5th bullet
706      eq ForStmt.getStmt().isDAbefore(Variable v) {
707        if (hasCondition() && getCondition().isDAafterTrue(v)) {
708          return true;
709        }
710        if (!hasCondition() && isDAafterInitialization(v)) {
711          return true;
712        }
713        return false;
714      }
715      // 16.2.11 6th bullet
716      eq ForStmt.getUpdateStmt().isDAbefore(Variable v) {
717        if (!getStmt().isDAafter(v)) {
718          return false;
719        }
720        for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
721          ContinueStmt stmt = (ContinueStmt) iter.next();
722          if (!stmt.isDAafterReachedFinallyBlocks(v)) {
723            return false;
724          }
725        }
726        return true;
727      }
728    
729      eq BreakStmt.isDAafter(Variable v) = true;
730      eq ContinueStmt.isDAafter(Variable v) = true;
731      eq ReturnStmt.isDAafter(Variable v) = true;
732      eq ThrowStmt.isDAafter(Variable v) = true;
733    
734      eq ReturnStmt.getResult().isDAbefore(Variable v) = isDAbefore(v);
735      eq ThrowStmt.getExpr().isDAbefore(Variable v) = isDAbefore(v);
736    
737      eq SynchronizedStmt.isDAafter(Variable v) = getBlock().isDAafter(v);
738      eq SynchronizedStmt.getExpr().isDAbefore(Variable v) = isDAbefore(v);
739      eq SynchronizedStmt.getBlock().isDAbefore(Variable v) = getExpr().isDAafter(v);
740    
741      // 16.2.15 1st bullet
742      eq TryStmt.getBlock().isDAbefore(Variable v) = isDAbefore(v);
743      // 16.2.15 2nd bullet
744      eq TryStmt.getCatchClause().isDAbefore(Variable v) = getBlock().isDAbefore(v);
745    
746      // 16.2.15 6th bullet
747      eq TryStmt.getFinally().isDAbefore(Variable v) = isDAbefore(v);
748      eq TryStmt.isDAafter(Variable v) {
749        // 16.2.15 4th bullet
750        if (!hasNonEmptyFinally()) {
751          if (!getBlock().isDAafter(v)) {
752            return false;
753          }
754          for (int i = 0; i < getNumCatchClause(); i++) {
755            if (!getCatchClause(i).getBlock().isDAafter(v)) {
756              return false;
757            }
758          }
759          return true;
760        } else {
761          // 16.2.15 5th bullet
762          if (getFinally().isDAafter(v)) {
763            return true;
764          }
765          if (!getBlock().isDAafter(v)) {
766            return false;
767          }
768          for (int i = 0; i < getNumCatchClause(); i++) {
769            if (!getCatchClause(i).getBlock().isDAafter(v)) {
770              return false;
771            }
772          }
773          return true;
774        }
775      }
776    }
777    
778    aspect DU {
779      inh boolean Stmt.isDUbefore(Variable v);
780      inh boolean VariableDeclaration.isDUbefore(Variable v);
781      syn lazy boolean Stmt.isDUafter(Variable v);
782      inh boolean Expr.isDUbefore(Variable v);
783      syn boolean Expr.isDUafter(Variable v);
784    
785      inh lazy boolean Binary.isDUbefore(Variable v);
786      inh lazy boolean AbstractDot.isDUbefore(Variable v);
787    
788      syn lazy boolean Binary.isDUafter(Variable v);
789      syn lazy boolean AbstractDot.isDUafter(Variable v);
790    
791      syn boolean Expr.isDUafterTrue(Variable v);
792      syn boolean Expr.isDUafterFalse(Variable v);
793    
794      inh lazy boolean TypeDecl.isDUbefore(Variable v);
795    
796      syn lazy boolean BodyDecl.isDUafter(Variable v) = true;
797    
798      eq Program.getChild().isDUbefore(Variable v) = true;
799    
800      eq BodyDecl.getChild().isDUbefore(Variable v) = isDUbefore(v, this);
801    
802      syn lazy boolean BodyDecl.isDUbefore(Variable v) = isDUbefore(v, this);
803    
804      inh boolean BodyDecl.isDUbefore(Variable v, BodyDecl b);
805    
806      eq TypeDecl.getChild().isDUbefore(Variable v, BodyDecl b) {
807        if (b instanceof MethodDecl || b instanceof MemberTypeDecl) {
808          return false;
809        }
810        if (v.isClassVariable() || v.isInstanceVariable()) {
811          boolean search = true;
812          if (b instanceof ConstructorDecl) {
813            search = false;
814          }
815    
816          for (int i = getNumBodyDecl() - 1; i >= 0; --i) {
817            BodyDecl decl = getBodyDecl(i);
818            if (b == decl) {
819              search = false;
820              continue;
821            }
822            if (search) {
823              continue;
824            }
825            if (decl instanceof FieldDeclaration) {
826              FieldDeclaration f = (FieldDeclaration) decl;
827              //System.err.println("  working on field " + f.name() + " which is child " + i);
828              if (f == v) {
829                return !f.hasInit();
830              }
831              if ((v.isClassVariable() && f.isStatic()) || (v.isInstanceVariable() && !f.isStatic())) {
832                return f.isDUafter(v);
833              }
834              //System.err.println("  field " + f.name() + " can not affect " + v.name());
835            } else if (decl instanceof StaticInitializer && v.isClassVariable()) {
836              StaticInitializer si = (StaticInitializer) decl;
837              //System.err.println("  working on static initializer which is child " + i);
838              return si.isDUafter(v);
839            } else if (decl instanceof InstanceInitializer && v.isInstanceVariable()) {
840              InstanceInitializer ii = (InstanceInitializer) decl;
841              //System.err.println("  working on instance initializer which is child " + i);
842              return ii.isDUafter(v);
843            }
844          }
845        }
846        //System.err.println("Reached TypeDecl when searching for DU for variable");
847        return isDUbefore(v);
848      }
849    
850      eq InstanceInitializer.isDUafter(Variable v) = getBlock().isDUafter(v);
851      eq StaticInitializer.isDUafter(Variable v) = getBlock().isDUafter(v);
852    
853      eq ConstructorDecl.isDUafter(Variable v) = getBlock().isDUafter(v) && getBlock().checkReturnDU(v);
854      eq ConstructorAccess.isDUafter(Variable v) = decl().isDUafter(v);
855      eq SuperConstructorAccess.isDUafter(Variable v) = isDUbefore(v);
856      eq ConstructorDecl.getBlock().isDUbefore(Variable v) = hasConstructorInvocation() ? getConstructorInvocation().isDUafter(v) : isDUbefore(v);
857    
858      syn lazy boolean Block.checkReturnDU(Variable v) {
859        HashSet set = new HashSet();
860        collectBranches(set);
861        for (Iterator iter = set.iterator(); iter.hasNext(); ) {
862          Object o = iter.next();
863          if (o instanceof ReturnStmt) {
864            ReturnStmt stmt = (ReturnStmt) o;
865            if (!stmt.isDUafterReachedFinallyBlocks(v)) {
866              return false;
867            }
868          }
869        }
870        return true;
871      }
872    
873      eq FieldDeclaration.isDUafter(Variable v) {
874        if (v == this) {
875          return !hasInit();
876        }
877        return hasInit() ? getInit().isDUafter(v) : isDUbefore(v);
878      }
879    
880      eq Stmt.isDUafter(Variable v) {
881        throw new Error("isDUafter in " + getClass().getName());
882      }
883    
884      // JLSv3 16.1.7
885      eq Expr.isDUafterFalse(Variable v) = isTrue() || isDUafter(v);
886      eq Expr.isDUafterTrue(Variable v) = isFalse() || isDUafter(v);
887    
888      eq AbstractDot.isDUafterTrue(Variable v) = isDUafter(v);
889      eq AbstractDot.isDUafterFalse(Variable v) = isDUafter(v);
890    
891      //= isTrue() && isDUbefore(v) || isFalse();
892      eq Expr.isDUafter(Variable v) = isDUbefore(v);
893    
894      eq ParExpr.isDUafterTrue(Variable v) = getExpr().isDUafterTrue(v);
895      eq ParExpr.isDUafterFalse(Variable v) = getExpr().isDUafterFalse(v);
896    
897      // JLSv3 16.1.2
898      eq AndLogicalExpr.isDUafterTrue(Variable v) = getRightOperand().isDUafterTrue(v);
899      eq AndLogicalExpr.isDUafterFalse(Variable v) = getLeftOperand().isDUafterFalse(v) && getRightOperand().isDUafterFalse(v);
900      eq AndLogicalExpr.getLeftOperand().isDUbefore(Variable v) = isDUbefore(v);
901      eq AndLogicalExpr.getRightOperand().isDUbefore(Variable v) = getLeftOperand().isDUafterTrue(v);
902      eq AndLogicalExpr.isDUafter(Variable v) = isDUafterTrue(v) && isDUafterFalse(v);
903    
904      eq OrLogicalExpr.isDUafterTrue(Variable v) = getLeftOperand().isDUafterTrue(v) && getRightOperand().isDUafterTrue(v);
905      eq OrLogicalExpr.isDUafterFalse(Variable v) = getRightOperand().isDUafterFalse(v);
906      eq OrLogicalExpr.getLeftOperand().isDUbefore(Variable v) = isDUbefore(v);
907      eq OrLogicalExpr.getRightOperand().isDUbefore(Variable v) = getLeftOperand().isDUafterFalse(v);
908      eq OrLogicalExpr.isDUafter(Variable v) = isDUafterTrue(v) && isDUafterFalse(v);
909    
910      eq LogNotExpr.isDUafterTrue(Variable v) = getOperand().isDUafterFalse(v);
911      eq LogNotExpr.isDUafterFalse(Variable v) = getOperand().isDUafterTrue(v);
912      eq LogNotExpr.getOperand().isDUbefore(Variable v) = isDUbefore(v);
913      eq LogNotExpr.isDUafter(Variable v) = isDUafterTrue(v) && isDUafterFalse(v);
914    
915      eq ConditionalExpr.isDUafterTrue(Variable v) = getTrueExpr().isDUafterTrue(v) && getFalseExpr().isDUafterTrue(v);
916      eq ConditionalExpr.isDUafterFalse(Variable v) = getTrueExpr().isDUafterFalse(v) && getFalseExpr().isDUafterFalse(v);
917      eq ConditionalExpr.getCondition().isDUbefore(Variable v) = isDUbefore(v);
918      eq ConditionalExpr.getTrueExpr().isDUbefore(Variable v) = getCondition().isDUafterTrue(v);
919      eq ConditionalExpr.getFalseExpr().isDUbefore(Variable v) = getCondition().isDUafterFalse(v);
920      eq ConditionalExpr.isDUafter(Variable v) = booleanOperator() ? isDUafterTrue(v) && isDUafterFalse(v) : getTrueExpr().isDUafter(v) && getFalseExpr().isDUafter(v);
921    
922       /**
923       * <a href="http://docs.oracle.com/javase/specs/jls/se7/html/jls-16.html#jls-16.1.8">JLSv7 $16.1.8</a>
924       */
925      eq AssignExpr.isDUafter(Variable v) {
926        if (getDest().isVariable() && getDest().varDecl() == v) {
927          return false;
928        } else {
929          return getSource().isDUafter(v);
930        }
931      }
932      eq AssignExpr.getSource().isDUbefore(Variable v) = getDest().isDUafter(v);
933      eq AssignExpr.getDest().isDUbefore(Variable v) = isDUbefore(v);
934      eq AssignExpr.isDUafterTrue(Variable v) = isDUafter(v);
935      eq AssignExpr.isDUafterFalse(Variable v) = isDUafter(v);
936    
937      syn boolean VarAccess.isDUafter(Variable v) = isDUbefore(v);
938    
939      eq AbstractDot.getRight().isDUbefore(Variable v) = getLeft().isDUafter(v);
940      eq AbstractDot.isDUafter(Variable v) = lastAccess().isDUafter(v);
941      eq ArrayAccess.isDUafter(Variable v) = getExpr().isDUafter(v);
942      eq ArrayTypeAccess.isDUafter(Variable v) = getAccess().isDUafter(v);
943      eq ArrayTypeWithSizeAccess.isDUafter(Variable v) = getExpr().isDUafter(v);
944      eq ArrayTypeWithSizeAccess.getExpr().isDUbefore(Variable v) = getAccess().isDUafter(v);
945    
946      eq ParExpr.isDUafter(Variable v) = getExpr().isDUafter(v);
947      eq Unary.isDUafter(Variable v) = getOperand().isDUafter(v);
948      eq CastExpr.isDUafter(Variable v) = getExpr().isDUafter(v);
949    
950      eq Binary.isDUafter(Variable v) = getRightOperand().isDUafter(v);
951      eq Binary.getRightOperand().isDUbefore(Variable v) = getLeftOperand().isDUafter(v);
952    
953      eq InstanceOfExpr.isDUafter(Variable v) = getExpr().isDUafter(v);
954    
955      /**
956       * <a href="http://docs.oracle.com/javase/specs/jls/se7/html/jls-16.html#jls-16.1.10">JLSv7 $16.1.10</a>
957       */
958      eq MethodAccess.getArg(int i).isDUbefore(Variable v) = computeDUbefore(i, v);
959      syn lazy boolean MethodAccess.computeDUbefore(int i, Variable v) = i == 0 ? isDUbefore(v) : getArg(i-1).isDUafter(v);
960      eq MethodAccess.isDUafter(Variable v) = getNumArg() == 0 ? isDUbefore(v) : getArg(getNumArg()-1).isDUafter(v);
961      eq MethodAccess.isDUafterTrue(Variable v) = isFalse() || (getNumArg() == 0 ? isDUbefore(v) : getArg(getNumArg()-1).isDUafter(v));
962      eq MethodAccess.isDUafterFalse(Variable v) = isTrue() || (getNumArg() == 0 ? isDUbefore(v) : getArg(getNumArg()-1).isDUafter(v));
963    
964      syn boolean ClassInstanceExpr.isDUafterInstance(Variable v) {
965        if (getNumArg() == 0) {
966          return isDUbefore(v);
967        }
968        return getArg(getNumArg()-1).isDUafter(v);
969      }
970      eq ClassInstanceExpr.isDUafter(Variable v) = isDUafterInstance(v);
971      eq ClassInstanceExpr.getArg(int i).isDUbefore(Variable v) = computeDUbefore(i, v);
972      syn lazy boolean ClassInstanceExpr.computeDUbefore(int i, Variable v) =
973          i == 0 ? isDUbefore(v) : getArg(i-1).isDUafter(v);
974    
975      syn boolean ArrayCreationExpr.isDUafterCreation(Variable v) = getTypeAccess().isDUafter(v);
976      eq ArrayCreationExpr.isDUafter(Variable v) = hasArrayInit() ? getArrayInit().isDUafter(v) : isDUafterCreation(v);
977    
978      eq ArrayCreationExpr.getArrayInit().isDUbefore(Variable v) = isDUafterCreation(v);
979    
980      eq EmptyStmt.isDUafter(Variable v) = isDUbefore(v);
981      eq AssertStmt.isDUafter(Variable v) = getCondition().isDUafter(v);
982    
983      eq MethodDecl.getBlock().isDUbefore(Variable v) = v.isFinal() && (v.isClassVariable() || v.isInstanceVariable()) ? false : true;
984    
985      eq Block.isDUafter(Variable v) = getNumStmt() == 0 ? isDUbefore(v) : getStmt(getNumStmt()-1).isDUafter(v);
986      eq Block.getStmt(int index).isDUbefore(Variable v) =
987          index == 0 ? isDUbefore(v) : getStmt(index - 1).isDUafter(v);
988      eq VarDeclStmt.getSingleDecl(int index).isDUbefore(Variable v) =
989          index == 0 ? isDUbefore(v) : getSingleDecl(index - 1).isDUafter(v);
990    
991      eq LocalClassDeclStmt.isDUafter(Variable v) = isDUbefore(v);
992    
993      eq VarDeclStmt.isDUafter(Variable v) =
994          getSingleDecl(getNumSingleDecl()-1).isDUafter(v);
995    
996      syn lazy boolean VariableDeclaration.isDUafter(Variable v) {
997        if (v == this) {
998          return !hasInit();
999        }
1000        return hasInit() ? getInit().isDUafter(v) : isDUbefore(v);
1001      }
1002      eq VariableDeclaration.getInit().isDUbefore(Variable v) = isDUbefore(v);
1003    
1004      eq ArrayInit.isDUafter(Variable v) = getNumInit() == 0 ? isDUbefore(v) : getInit(getNumInit()-1).isDUafter(v);
1005      eq ArrayInit.getInit().isDUbefore(Variable v) = computeDUbefore(childIndex, v);
1006      // force caching of computation
1007      syn lazy boolean ArrayInit.computeDUbefore(int childIndex, Variable v) {
1008        if (childIndex == 0) {
1009          return isDUbefore(v);
1010        }
1011        int index = childIndex-1;
1012        while (index > 0 && getInit(index).isConstant()) {
1013          index--;
1014        }
1015        return getInit(childIndex-1).isDUafter(v);
1016      }
1017    
1018      eq LabeledStmt.getStmt().isDUbefore(Variable v) = isDUbefore(v);
1019      eq LabeledStmt.isDUafter(Variable v) {
1020        if (!getStmt().isDUafter(v)) {
1021          return false;
1022        }
1023        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
1024          BreakStmt stmt = (BreakStmt) iter.next();
1025          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1026            return false;
1027          }
1028        }
1029        return true;
1030      }
1031    
1032      interface FinallyHost {
1033        //public Block getFinally();
1034        public boolean isDUafterFinally(Variable v);
1035        public boolean isDAafterFinally(Variable v);
1036        public FinallyHost enclosingFinally(Stmt branch);
1037        public Block getFinallyBlock();
1038      }
1039      TryStmt implements FinallyHost;
1040      SynchronizedStmt implements FinallyHost;
1041    
1042      public Block TryStmt.getFinallyBlock() {
1043        return getFinally();
1044      }
1045    
1046      public Block SynchronizedStmt.getFinallyBlock() {
1047        return getMonitorExit();
1048      }
1049    
1050      syn boolean TryStmt.isDUafterFinally(Variable v) = getFinally().isDUafter(v);
1051      syn boolean SynchronizedStmt.isDUafterFinally(Variable v) = true;
1052    
1053      syn boolean TryStmt.isDAafterFinally(Variable v) = getFinally().isDAafter(v);
1054      syn boolean SynchronizedStmt.isDAafterFinally(Variable v) = false;
1055    
1056    
1057      syn lazy boolean BreakStmt.isDUafterReachedFinallyBlocks(Variable v) {
1058        Iterator<FinallyHost> iter = finallyIterator();
1059        if (!isDUbefore(v) && !iter.hasNext()) {
1060          return false;
1061        }
1062        while (iter.hasNext()) {
1063          FinallyHost f = iter.next();
1064          if (!f.isDUafterFinally(v)) {
1065            return false;
1066          }
1067        }
1068        return true;
1069      }
1070    
1071      syn lazy boolean ContinueStmt.isDUafterReachedFinallyBlocks(Variable v) {
1072        Iterator<FinallyHost> iter = finallyIterator();
1073        if (!isDUbefore(v) && !iter.hasNext()) {
1074          return false;
1075        }
1076        while (iter.hasNext()) {
1077          FinallyHost f = iter.next();
1078          if (!f.isDUafterFinally(v)) {
1079            return false;
1080          }
1081        }
1082        return true;
1083      }
1084      syn lazy boolean ReturnStmt.isDUafterReachedFinallyBlocks(Variable v) {
1085        Iterator<FinallyHost> iter = finallyIterator();
1086        if (!isDUbefore(v) && !iter.hasNext()) {
1087          return false;
1088        }
1089        while (iter.hasNext()) {
1090          FinallyHost f = iter.next();
1091          if (!f.isDUafterFinally(v)) {
1092            return false;
1093          }
1094        }
1095        return true;
1096      }
1097    
1098      syn lazy boolean BreakStmt.isDAafterReachedFinallyBlocks(Variable v) {
1099        if (isDAbefore(v)) {
1100          return true;
1101        }
1102        Iterator<FinallyHost> iter = finallyIterator();
1103        if (!iter.hasNext()) {
1104          return false;
1105        }
1106        while (iter.hasNext()) {
1107          FinallyHost f = iter.next();
1108          if (!f.isDAafterFinally(v)) {
1109            return false;
1110          }
1111        }
1112        return true;
1113      }
1114    
1115      syn lazy boolean ContinueStmt.isDAafterReachedFinallyBlocks(Variable v) {
1116        if (isDAbefore(v)) {
1117          return true;
1118        }
1119        Iterator<FinallyHost> iter = finallyIterator();
1120        if (!iter.hasNext()) {
1121          return false;
1122        }
1123        while (iter.hasNext()) {
1124          FinallyHost f = iter.next();
1125          if (!f.isDAafterFinally(v)) {
1126            return false;
1127          }
1128        }
1129        return true;
1130      }
1131      syn lazy boolean ReturnStmt.isDAafterReachedFinallyBlocks(Variable v) {
1132        if (hasResult() ? getResult().isDAafter(v) : isDAbefore(v)) {
1133          return true;
1134        }
1135        Iterator<FinallyHost> iter = finallyIterator();
1136        if (!iter.hasNext()) {
1137          return false;
1138        }
1139        while (iter.hasNext()) {
1140          FinallyHost f = iter.next();
1141          if (!f.isDAafterFinally(v)) {
1142            return false;
1143          }
1144        }
1145        return true;
1146      }
1147    
1148      eq ExprStmt.isDUafter(Variable v) = getExpr().isDUafter(v);
1149      eq ExprStmt.getExpr().isDUbefore(Variable v) = isDUbefore(v);
1150    
1151      eq IfStmt.isDUafter(Variable v) = hasElse() ? getThen().isDUafter(v) && getElse().isDUafter(v) : getThen().isDUafter(v) && getCondition().isDUafterFalse(v);
1152      eq IfStmt.getCondition().isDUbefore(Variable v) = isDUbefore(v);
1153      eq IfStmt.getThen().isDUbefore(Variable v) = getCondition().isDUafterTrue(v);
1154      eq IfStmt.getElse().isDUbefore(Variable v) = getCondition().isDUafterFalse(v);
1155    
1156      // 16.2.9 1st bullet
1157      eq SwitchStmt.isDUafter(Variable v) {
1158        if (!(!noDefaultLabel() || getExpr().isDUafter(v))) {
1159          return false;
1160        }
1161        if (!(!switchLabelEndsBlock() || getExpr().isDUafter(v))) {
1162          return false;
1163        }
1164        if (!unassignedAfterLastStmt(v)) {
1165          return false;
1166        }
1167        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
1168          BreakStmt stmt = (BreakStmt) iter.next();
1169          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1170            return false;
1171          }
1172        }
1173        return true;
1174      }
1175    
1176      syn boolean SwitchStmt.unassignedAfterLastStmt(Variable v) =
1177          getBlock().isDUafter(v);
1178    
1179      syn boolean SwitchStmt.switchLabelEndsBlock() =
1180          getBlock().getNumStmt() > 0
1181          && getBlock().getStmt(getBlock().getNumStmt()-1) instanceof ConstCase;
1182    
1183      // 16.2.8 2nd bullet
1184      eq SwitchStmt.getExpr().isDUbefore(Variable v) = isDUbefore(v);
1185      eq SwitchStmt.getBlock().isDUbefore(Variable v) = getExpr().isDUafter(v);
1186    
1187      syn boolean Case.isDUbefore(Variable v) =
1188          getParent().getParent() instanceof Block
1189          && ((Block) getParent().getParent()).isDUbefore(v)
1190          && super.isDUbefore(v);
1191    
1192      eq Case.isDUafter(Variable v) = isDUbefore(v);
1193    
1194      // 16.2.10 1st bullet
1195      eq WhileStmt.isDUafter(Variable v) {
1196        if (!isDUbeforeCondition(v)) {
1197          // start a circular evaluation here
1198          return false;
1199        }
1200        if (!getCondition().isDUafterFalse(v)) {
1201          return false;
1202        }
1203        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
1204          BreakStmt stmt = (BreakStmt) iter.next();
1205          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1206            return false;
1207          }
1208        }
1209        return true;
1210      }
1211    
1212      // 16.2.10 3rd bullet
1213      eq WhileStmt.getCondition().isDUbefore(Variable v) = isDUbeforeCondition(v);
1214    
1215      // 16.2.10 3rd bullet
1216      syn boolean WhileStmt.isDUbeforeCondition(Variable v) circular [true] {
1217        // 1st
1218        if (!isDUbefore(v)) {
1219          return false;
1220        } else if (!getStmt().isDUafter(v)) {
1221          return false;
1222        } else {
1223          for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
1224            ContinueStmt stmt = (ContinueStmt) iter.next();
1225            if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1226              return false;
1227            }
1228          }
1229        }
1230        return true;
1231      }
1232    
1233      // 16.2.10 4th bullet
1234      eq WhileStmt.getStmt().isDUbefore(Variable v) = getCondition().isDUafterTrue(v);
1235    
1236      eq DoStmt.isDUafter(Variable v) {
1237        if (!isDUbeforeCondition(v)) // start a circular evaluation here
1238          return false;
1239        if (!getCondition().isDUafterFalse(v)) {
1240          return false;
1241        }
1242        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
1243          BreakStmt stmt = (BreakStmt) iter.next();
1244          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1245            return false;
1246          }
1247        }
1248        return true;
1249      }
1250      eq DoStmt.getStmt().isDUbefore(Variable v) = isDUbefore(v) && getCondition().isDUafterTrue(v);
1251      eq DoStmt.getCondition().isDUbefore(Variable v) = isDUbeforeCondition(v);
1252      syn boolean DoStmt.isDUbeforeCondition(Variable v) circular [true] {
1253        if (!getStmt().isDUafter(v)) {
1254          return false;
1255        } else {
1256          for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
1257            ContinueStmt stmt = (ContinueStmt) iter.next();
1258            if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1259              return false;
1260            }
1261          }
1262        }
1263        return true;
1264      }
1265    
1266      // 16.2.11 1st bullet
1267      eq ForStmt.isDUafter(Variable v) {
1268        if (!isDUbeforeCondition(v)) {
1269          // start a circular evaluation here
1270          return false;
1271        }
1272        if (!(!hasCondition() || getCondition().isDUafterFalse(v))) {
1273          return false;
1274        }
1275        for (Iterator iter = targetBreaks().iterator(); iter.hasNext(); ) {
1276          BreakStmt stmt = (BreakStmt) iter.next();
1277          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1278            return false;
1279          }
1280        }
1281        return true;
1282      }
1283      // 16.2.11 2nd  bullet
1284      eq ForStmt.getInitStmt().isDUbefore(Variable v) = childIndex == 0 ? isDUbefore(v) : getInitStmt(childIndex-1).isDUafter(v);
1285      // 16.2.11 3rd bullet
1286      eq ForStmt.getCondition().isDUbefore(Variable v) = isDUbeforeCondition(v);
1287      // 16.2.11 3rd bullet
1288      syn boolean ForStmt.isDUafterInit(Variable v) = getNumInitStmt() == 0 ? isDUbefore(v) : getInitStmt(getNumInitStmt()-1).isDUafter(v);
1289      // 16.2.11 4th bullet
1290      syn boolean ForStmt.isDUbeforeCondition(Variable v) circular [true] {
1291        if (!isDUafterInit(v)) {
1292          return false;
1293        } else if (!isDUafterUpdate(v)) {
1294          return false;
1295        }
1296        return true;
1297      }
1298      // 16.2.11 5th bullet
1299      eq ForStmt.getStmt().isDUbefore(Variable v) = isDUbeforeCondition(v) && (hasCondition() ?
1300        getCondition().isDUafterTrue(v) : isDUafterInit(v));
1301    
1302      syn boolean ForStmt.isDUafterUpdate(Variable v) {
1303        if (!isDUbeforeCondition(v)) // start a circular evaluation here
1304          return false;
1305        if (getNumUpdateStmt() > 0) {
1306          return getUpdateStmt(getNumUpdateStmt()-1).isDUafter(v);
1307        }
1308        if (!getStmt().isDUafter(v)) {
1309          return false;
1310        }
1311        for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
1312          ContinueStmt stmt = (ContinueStmt) iter.next();
1313          if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1314            return false;
1315          }
1316        }
1317        return true;
1318      }
1319    
1320      // 16.2.11 6th bullet
1321      eq ForStmt.getUpdateStmt(int i).isDUbefore(Variable v) {
1322        if (!isDUbeforeCondition(v)) // start a circular evaluation here
1323          return false;
1324        if (i == 0) {
1325          if (!getStmt().isDUafter(v)) {
1326            return false;
1327          }
1328          for (Iterator iter = targetContinues().iterator(); iter.hasNext(); ) {
1329            ContinueStmt stmt = (ContinueStmt) iter.next();
1330            if (!stmt.isDUafterReachedFinallyBlocks(v)) {
1331              return false;
1332            }
1333          }
1334          return true;
1335        } else {
1336          return getUpdateStmt(i-1).isDUafter(v);
1337        }
1338      }
1339    
1340      rewrite ForStmt {
1341        when (!hasCondition())
1342        to ForStmt {
1343          setCondition(new BooleanLiteral("true"));
1344          return this;
1345        }
1346      }
1347    
1348      eq BreakStmt.isDUafter(Variable v) = true;
1349      eq ContinueStmt.isDUafter(Variable v) = true;
1350      eq ReturnStmt.isDUafter(Variable v) = true;
1351      eq ThrowStmt.isDUafter(Variable v) = true;
1352    
1353      eq ReturnStmt.getResult().isDUbefore(Variable v) = isDUbefore(v);
1354      eq ThrowStmt.getExpr().isDUbefore(Variable v) = isDUbefore(v);
1355    
1356      eq SynchronizedStmt.isDUafter(Variable v) = getBlock().isDUafter(v);
1357      eq SynchronizedStmt.getExpr().isDUbefore(Variable v) = isDUbefore(v);
1358      eq SynchronizedStmt.getBlock().isDUbefore(Variable v) = getExpr().isDUafter(v);
1359    
1360      // 16.2.15 1st bullet
1361      eq TryStmt.getBlock().isDUbefore(Variable v) = isDUbefore(v);
1362    
1363      syn boolean TryStmt.isDUbefore(Variable v) circular [true] = super.isDUbefore(v);
1364    
1365      // 16.2.15 3rd bullet
1366      eq TryStmt.getCatchClause().isDUbefore(Variable v) {
1367        if (!getBlock().isDUafter(v)) {
1368          return false;
1369        }
1370        if (!getBlock().isDUeverywhere(v)) {
1371          return false;
1372        }
1373        return true;
1374      }
1375    
1376      // 16.2.14 6th bullet
1377      eq TryStmt.getFinally().isDUbefore(Variable v) {
1378        if (!getBlock().isDUeverywhere(v)) {
1379          return false;
1380     }
1381        for (int i = 0; i < getNumCatchClause(); i++) {
1382          if (!getCatchClause(i).getBlock().checkDUeverywhere(v)) {
1383            return false;
1384       }
1385     }
1386        return true;
1387      }
1388    
1389      eq TryStmt.isDUafter(Variable v) {
1390        // 16.2.14 4th bullet
1391        if (!hasNonEmptyFinally()) {
1392          if (!getBlock().isDUafter(v)) {
1393            return false;
1394          }
1395          for (int i = 0; i < getNumCatchClause(); i++) {
1396            if (!getCatchClause(i).getBlock().isDUafter(v)) {
1397              return false;
1398            }
1399          }
1400          return true;
1401        } else {
1402          return getFinally().isDUafter(v);
1403        }
1404      }
1405    }