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