001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.translate;
004    
005    import java.util.Enumeration;
006    import javafe.util.Assert;
007    import javafe.util.Location;
008    import javafe.util.Set;
009    import javafe.util.Location;
010    
011    import javafe.ast.*;
012    import escjava.ast.*;
013    import escjava.ast.TagConstants;
014    import escjava.ast.Modifiers;
015    import escjava.tc.FlowInsensitiveChecks;
016    import escjava.prover.*;
017    
018    /** This class generates possible ways to annotate a program to eliminate
019      * a given warning.<p>
020      *
021      * NOTE:  The syntax of the strings produced in this class must be kept
022      * in sync with what is expected by the script wizfilter.perl.
023      **/
024    
025    class Suggestion {
026      static /*null*/ String generate(int warningTag, Object auxInfo,
027                             /*@ non_null */ RoutineDecl rd,
028                             /*@ non_null */ Set directTargets,
029                             /*@ non_null */ SList cc, int locDecl) {
030          switch (warningTag) {
031          case TagConstants.CHKNULLPOINTER:
032          case TagConstants.CHKNONNULL:
033              {
034                  VarInit E = (VarInit)auxInfo;
035                  // CF: bug workaround
036                  if (E==null) return null;
037                  Assert.notNull(E);
038                  return gNull(E, rd);
039              }
040              
041          case TagConstants.CHKNONNULLINIT:
042              return "add an initializer or initialize the field in constructor";
043              
044          case TagConstants.CHKINDEXNEGATIVE:
045          case TagConstants.CHKNEGATIVEARRAYSIZE:
046              {
047                  VarInit E = (VarInit)auxInfo;
048                  Assert.notNull(E);
049                  return gNeg(E, rd, directTargets);
050              }
051              
052          case TagConstants.CHKARRAYSTORE:
053              {
054                  VarInit E = (VarInit)auxInfo;
055                  Assert.notNull(E);
056                  return gArrStore(E, rd);
057              }
058          case TagConstants.CHKOBJECTINVARIANT:
059              {
060                  if (auxInfo == null)
061                      return null;
062                  else {
063                      Expr E = (Expr)auxInfo;
064                      return gInvariant(E, rd, cc, locDecl);
065                  }
066              }
067          default:
068              break;
069          }
070          return null;  // no suggestion
071      }
072    
073      //@ ensures \result != null;
074      private static String gNull(/*@ non_null */ VarInit E,
075                                  /*@ non_null */ RoutineDecl rd) {
076        switch (E.getTag()) {
077          case TagConstants.FIELDACCESS:
078            {
079              FieldDecl fd = ((FieldAccess)E).decl;
080              String description;
081              if (Modifiers.isStatic(fd.modifiers)) {
082                description = "static field ";
083              } else {
084                if (rd instanceof ConstructorDecl && fd.parent == rd.parent) {
085                  return "none <instance field in constructor>";
086                }
087                description = "instance field ";
088              }
089              return "perhaps declare " + description + name(fd.id, fd.locId) +
090                " with 'non_null'";
091            }
092    
093          case TagConstants.VARIABLEACCESS:
094            {
095              GenericVarDecl vd = ((VariableAccess)E).decl;
096              if (vd.getTag() == TagConstants.FORMALPARADECL) {
097                if (FlowInsensitiveChecks.isMethodOverride(rd)) {
098                  MethodDecl md = (MethodDecl)rd;
099    
100                  // Find index of parameter in method's signature
101                  int pi = 0;
102                  while (md.args.elementAt(pi) != vd) {
103                    pi++;
104                  }
105                  // Find the corresponding parameter in the original method decl
106                  MethodDecl mdOrig = getOriginalMethod(md);
107                  GenericVarDecl vdSuper = mdOrig.args.elementAt(pi);
108    
109                  String s = "perhaps declare parameter " +
110                    name(vdSuper.id, vdSuper.locId) +
111                    " with 'non_null'";
112                  String n0 = vdSuper.id.toString();
113                  String n1 = vd.id.toString();
114                  if (!n0.equals(n1)) {
115                    s += " (the parameter is known as '" + n1 +
116                      "' in the method override in class " + md.parent.id + ")";
117                  }
118                  return s;
119                } else {
120                  return "perhaps declare parameter " + name(vd.id, vd.locId) +
121                    " with 'non_null'";
122                }
123              } else if (vd.getTag() == TagConstants.LOCALVARDECL) {
124                return "perhaps declare local variable " + name(vd.id, vd.locId) +
125                  " with 'non_null'";
126              } else {
127                return "none <unknown variable>";
128              }
129            }
130    
131          case TagConstants.METHODINVOCATION:
132            {
133              MethodDecl md =((MethodInvocation)E).decl;
134              if (FlowInsensitiveChecks.isMethodOverride(md)) {
135                return "perhaps declare method override " + name(md.id, md.locId) +
136                  " with 'also_ensures \\result != null;' " +
137                  "(or the overridden method with 'ensures \\result != null;')";
138              } else if (md instanceof MethodDecl) {
139                return "perhaps declare method " + name(md.id, md.locId) +
140                  " with 'ensures \\result != null;'";
141              } else {
142                Assert.fail("unexpected routine returns possibly-null value");
143                return null;
144              }
145            }
146    
147          case TagConstants.NULLLIT:
148            return "none <null>";
149    
150          default:
151            return "none <intimidating expression>";
152        }
153      }
154    
155      //@ ensures \result != null;
156      private static String gNeg(/*@ non_null */ VarInit E,
157                                 /*@ non_null */ RoutineDecl rd,
158                                 /*@ non_null */ Set directTargets) {
159        switch (E.getTag()) {
160          case TagConstants.FIELDACCESS:
161            {
162              FieldDecl fd = ((FieldAccess)E).decl;
163              String description;
164              if (Modifiers.isStatic(fd.modifiers)) {
165                description = "static invariant ";
166              } else {
167                description = "instance invariant ";
168              }
169              if (directTargets.contains(fd)) {
170                return "none <" +
171                  (Modifiers.isStatic(fd.modifiers) ? "static" : "instance") +
172                  " field is direct target>";
173              } else {
174                return "perhaps declare " + description + "'invariant 0 <= " +
175                  fd.id + ";' in class " + fd.parent.id +
176                  " (near " + name(fd.id, fd.locId) + ")";
177              }
178            }
179    
180          case TagConstants.VARIABLEACCESS:
181            {
182              GenericVarDecl vd = ((VariableAccess)E).decl;
183              if (vd.getTag() == TagConstants.FORMALPARADECL) {
184                if (directTargets.contains(vd)) {
185                  return "none <parameter is direct target>";
186                } else if (FlowInsensitiveChecks.isMethodOverride(rd)) {
187                  MethodDecl md = (MethodDecl)rd;
188                  MethodDecl mdOrig = getOriginalMethod(md);
189                  return "perhaps declare overridden method " +
190                    name(mdOrig.id, mdOrig.locId) +
191                    " with 'requires 0 <= " + vd.id + ";'";
192                } else if (rd instanceof MethodDecl) {
193                  MethodDecl md = (MethodDecl)rd;
194                  return "perhaps declare method " + name(md.id, md.locId) +
195                    " with 'requires 0 <= " + vd.id + ";'";
196                } else {
197                  return "perhaps declare constructor " +
198                    name(rd.parent.id, rd.locId) +
199                    " with 'requires 0 <= " + vd.id + ";'";
200                }
201              } else if (vd.getTag() == TagConstants.LOCALVARDECL) {
202                return "none <local variable>";
203              } else {
204                return "none <unknown variable type>";
205              }
206            }
207    
208          case TagConstants.METHODINVOCATION:
209            {
210              MethodDecl md =((MethodInvocation)E).decl;
211              if (FlowInsensitiveChecks.isMethodOverride(md)) {
212                return "perhaps declare method override " + name(md.id, md.locId) +
213                  " with 'also_ensures 0 <= \\result;' " +
214                  "(or the overridden method with 'ensures 0 <= \\result;')";
215              } else if (md instanceof MethodDecl) {
216                return "perhaps declare method " + name(md.id, md.locId) +
217                  " with 'ensures 0 <= \\result;'";
218              } else {
219                Assert.fail("unexpected routine returns possibly-negative value");
220                return null;
221              }
222            }
223          
224          default:
225            return "none <big expression>";
226        }
227      }
228    
229    
230      //@ ensures \result != null;
231      private static String gArrStore(/*@ non_null */ VarInit E,
232                                      /*@ non_null */ RoutineDecl rd) {
233          switch (E.getTag()) {
234          case TagConstants.FIELDACCESS:
235              {
236                  FieldDecl fd = ((FieldAccess)E).decl;
237                  String description;
238                  if (Modifiers.isStatic(fd.modifiers)) {
239                      description = "static invariant ";
240                  } else {
241                      description = "instance invariant ";
242                  }
243                  Assert.notFalse(fd.type instanceof ArrayType);
244                  return "perhaps declare " + description + 
245                      "'invariant \\elemtype(\\typeof(" + fd.id + 
246                      ")) == \\type(" + typeName(((ArrayType) fd.type).elemType) 
247                      + ");' in class " + fd.parent.id +
248                      " (near " + name(fd.id, fd.locId) + ")";      
249              }
250              
251          case TagConstants.VARIABLEACCESS:
252              {
253                  GenericVarDecl vd = ((VariableAccess)E).decl;
254                  if (vd.getTag() == TagConstants.FORMALPARADECL) {
255                      MethodDecl md = (MethodDecl)rd;
256                      if (FlowInsensitiveChecks.isMethodOverride(rd)) {
257                          
258                          // Find index of parameter in method's signature
259                          int pi = 0;
260                          while (md.args.elementAt(pi) != vd) {
261                              pi++;
262                          }
263                          /* Find the corresponding parameter in the 
264                             original method decl */
265                          MethodDecl mdOrig = getOriginalMethod(md);
266                          GenericVarDecl vdSuper = mdOrig.args.elementAt(pi);
267    
268                          String n0 = vdSuper.id.toString();
269                          String n1 = vd.id.toString();
270                          
271                          Assert.notFalse(vdSuper.type instanceof ArrayType);
272                          String s = "perhaps declare overridden method " +
273                              name(mdOrig.id, mdOrig.locId) +
274                              " with 'requires \\elemtype(\\typeof(" + n0 +
275                              ")) == \\type(" + 
276                              typeName(((ArrayType) vdSuper.type).elemType) +
277                              ");'";
278                          if (!n0.equals(n1)) {
279                              s += " (the parameter is known as '" + n1 +
280                                  "' in the method override in class " + 
281                                  md.parent.id + ")";
282                          }
283                          return s;
284                      } else {
285                          Assert.notFalse(vd.type instanceof ArrayType);
286                          return "perhaps declare method " + 
287                              name(md.id, md.locId) +
288                              " with 'requires \\elemtype(\\typeof(" + vd.id 
289                              + ")) == \\type(" 
290                              + typeName(((ArrayType) vd.type).elemType)
291                              + ");'";
292                              
293                      }
294                  } else if (vd.getTag() == TagConstants.LOCALVARDECL) {
295                      return "none <local variable>";
296                  } else {
297                      return "none <unknown variable>";
298                  }
299              }
300              
301          case TagConstants.METHODINVOCATION:
302              {
303                  MethodDecl md =((MethodInvocation)E).decl;
304                  if (FlowInsensitiveChecks.isMethodOverride(md)) {
305                      Assert.notFalse(md.returnType instanceof ArrayType);
306                      String returnType = typeName(((ArrayType) md.returnType).elemType);
307                      return "perhaps declare method override " + name(md.id, md.locId) +
308                          " with 'also_ensures \\elemtype(\\typeof(\\result)) == " +
309                          "\\type(" + returnType + ");' " +
310                          "(or the overridden method with " +
311                          "'ensures \\elemtype(\\typeof(\\result)) == \\type(" + 
312                          returnType + ");')";
313                  } else if (md instanceof MethodDecl) {
314                      Assert.notFalse(md.returnType instanceof ArrayType);
315                      return "perhaps declare method " + 
316                          name(md.id, md.locId) +
317                          " with 'ensures \\elemtype(\\typeof(\\result)) == \\type(" +
318                          typeName(((ArrayType) md.returnType).elemType) + 
319                          ");'";
320                  } else {
321                      Assert.fail("unexpected routine returns possibly-null value");
322                      return null;
323                  }
324              }
325              
326          case TagConstants.NULLLIT:
327              return "none <null>";
328              
329          default:
330              return "none <intimidating expression>";
331          } 
332      } 
333    
334    
335      private static String gInvariant(/*@ non_null */ Expr E,
336                                       /*@ non_null */ RoutineDecl rd,
337                                       /*@ non_null */ SList cc,
338                                                       int locDecl) {
339          if (brokenObjIsMadeUp(cc)) {
340              Set inj = possiblyInjectiveFields(E);
341              if (inj == null)
342                  return null;
343              else if (inj.size() != 1)
344                  return null;
345              else {
346                  Enumeration els = inj.elements();
347                  String injField = ((Identifier) els.nextElement()).toString();
348                  return "perhaps declare instance invariant 'invariant this." + 
349                      injField + ".owner == this;' in class " + rd.parent.id + 
350                      " (near associated declaration at " + 
351                      Location.toString(locDecl) + ")";
352              }
353          }
354          else
355              return null;
356      }
357    
358    
359    
360      /** Returns a method that <code>md</code> overrides.  If <code>md</code>
361        * overrides a method in a class, then that method is returned.  Otherwise,
362        * any one of the overrides is returned.
363        **/
364    
365      //@ ensures \result != null;
366      static MethodDecl getOriginalMethod(/*@ non_null */ MethodDecl md) {
367        MethodDecl orig = md;
368        while (true) {
369          MethodDecl mdSuper = FlowInsensitiveChecks.getSuperClassOverride(orig);
370          if (mdSuper == null) {
371            return orig;
372          }
373          orig = mdSuper;
374        }
375      }
376    
377    
378      //@ ensures \result != null;
379      private static String name(/*@ non_null */ Identifier id, int loc) {
380        String s = "'" + id + "'";
381        if (!Location.isWholeFileLoc(loc)) {
382          s += " at " + Location.toLineNumber(loc) + "," + Location.toColumn(loc);
383        }
384        s += " in " + Location.toFileName(loc);
385        return s;
386      }
387    
388    
389      //@ ensures \result != null;
390      private static String typeName(/*@ non_null */ Type type) {
391          String name;
392          if (type instanceof PrimitiveType) {
393              PrimitiveType pt = (PrimitiveType) type;
394              name = javafe.ast.TagConstants.toString(pt.tag);
395              name = name.substring(name.length() - 4).toLowerCase();
396          }
397          else if (type instanceof TypeName) {
398              TypeName tn = (TypeName) type;
399              name = tn.name.printName();
400          }
401          else if (type instanceof ArrayType) {
402              ArrayType at = (ArrayType) type;
403              String elemName = typeName(at.elemType);
404              name = elemName + "[]";
405          }
406          else {
407              javafe.util.Assert.fail("Unknown kind of Type");
408              name = "";
409          }
410          return name;
411      }
412    
413    
414        /* Returns true if the counterexample context does not say that
415           brokenObj is equal to some program variable, and false otherwise.
416           This tells us whether or not Simplify had to dream up the broken
417           object, which is a strong indicator of an injectivity problem.
418        */
419        private static boolean brokenObjIsMadeUp(/*@ non_null */ SList cc) {
420            int n = cc.length();
421            try {
422                for (int i = 0; i < n; i++) {
423                    SExp cur = cc.at(i);
424                    if (cur.isList()) {
425                        SList curL = (SList) cur;
426                        if (curL.length() == 3) {
427                            if (curL.at(0).toString().equals("EQ") &&
428                                (curL.at(1).toString().startsWith("brokenObj") 
429                                 ||
430                                 curL.at(2).toString().startsWith("brokenObj")))
431                                return false;
432                        }
433                    }
434                }
435            }
436            catch (SExpTypeError e) {
437                Assert.fail("Out of bounds SList access");
438            }
439            return true;    
440        }
441    
442        
443        /* Finds fields that potentially need to be declared injective.  This
444           routine simply searches for fields f in an expression of the form
445           brokenObj.f.f' or brokenObj.f[i]. */
446        private static Set possiblyInjectiveFields(/*@ non_null */ Expr e) {
447            if (e instanceof LabelExpr)
448                return possiblyInjectiveFields(((LabelExpr) e).expr);
449            else if (e instanceof QuantifiedExpr)
450                return possiblyInjectiveFields(((QuantifiedExpr) e).expr);
451            else if (e.getTag() == TagConstants.SELECT) {
452                ExprVec exprs = ((NaryExpr) e).exprs;
453                Expr first = exprs.elementAt(0);
454                Expr second = exprs.elementAt(1);
455                // check for brokenObj.f.f' or this.f.f' (in case the brokenObj
456                // substitution hasn't already been performed for some reason)
457                if (first.getTag() == TagConstants.VARIABLEACCESS &&
458                    second.getTag() == TagConstants.SELECT) {
459                    ExprVec sexprs = ((NaryExpr) second).exprs;
460                    Expr sec0 = sexprs.elementAt(0);
461                    Expr sec1 = sexprs.elementAt(1);
462                    if (sec0.getTag() == TagConstants.VARIABLEACCESS &&
463                        sec1.getTag() == TagConstants.VARIABLEACCESS) {
464                        String name = ((VariableAccess)sec1).id.toString();
465                        if (name.startsWith("brokenObj") || name.equals("this")) {
466                            Set set = new Set();
467                            set.add(((VariableAccess)sec0).id);
468                            return set;
469                        }
470                        else
471                            return null;
472                    }
473                    else
474                        return null;
475                }
476                // check for brokenObj.f[i] or this.f[i] (in case the brokenObj
477                // substitution hasn't already been performed for some reason)
478                else if (first.getTag() == TagConstants.SELECT) {
479                    ExprVec fexprs = ((NaryExpr) first).exprs;
480                    Expr fir0 = fexprs.elementAt(0);
481                    Expr fir1 = fexprs.elementAt(1);
482                    Set set = new Set();
483                    if (fir0.getTag() == TagConstants.VARIABLEACCESS &&
484                        fir1.getTag() == TagConstants.SELECT) {
485                        Assert.notFalse(((VariableAccess)fir0).id.toString().equals("elems"));
486                        ExprVec f1exprs = ((NaryExpr) fir1).exprs;
487                        Expr fir10 = f1exprs.elementAt(0);
488                        Expr fir11 = f1exprs.elementAt(1);
489                        if (fir10.getTag() == TagConstants.VARIABLEACCESS 
490                            && fir11.getTag() == TagConstants.VARIABLEACCESS) {
491                            String name = ((VariableAccess)fir11).id.toString();
492                            if (name.startsWith("brokenObj") || name.equals("this")) 
493                                set.add(((VariableAccess) fir10).id);
494                            else
495                                return null;
496                        }
497                        else
498                            return null;
499                    }
500                    else
501                        return null;
502                    Set res = possiblyInjectiveFields(second);
503                    Enumeration els = res.elements();
504                    while (els.hasMoreElements()) {
505                        set.add(els.nextElement());
506                    }
507                    if (set.size() > 1)
508                        return null;
509                    return set;
510                }
511                // neither special case applies, so do regular NaryExpr processing
512                else
513                    return checkNaryExpr((NaryExpr) e);
514            }
515            else if (e instanceof NaryExpr) 
516                return checkNaryExpr((NaryExpr) e);
517            else if (e instanceof TypeExpr || e instanceof VariableAccess ||
518                     e instanceof LiteralExpr)
519                return new Set();
520            else if (e instanceof SubstExpr) {
521                // check that this is a substitution of brokenObj for this
522                SubstExpr s = (SubstExpr) e;
523                Assert.notFalse(s.var.id.toString().equals("this"));
524                Assert.notFalse(s.val instanceof VariableAccess);
525                Assert.notFalse(((VariableAccess) s.val).id.toString().startsWith("brokenObj"));
526                return possiblyInjectiveFields(s.target);
527            }
528            else {
529                Assert.fail("Unexpected Expr encountered");
530                return null;
531            }
532        }
533        
534        /* A helper function for possiblyInjectiveFields that checks for injective
535           fields in NaryExprs. */
536        private static Set checkNaryExpr(/*@ non_null */ NaryExpr e) {
537            ExprVec exprs = e.exprs;
538            int size = exprs.size();
539            Set total = new Set();
540            for (int i = 0; i < size; i++) {
541                Set cur = possiblyInjectiveFields(exprs.elementAt(i));
542                if (cur == null)
543                    return null;
544                Enumeration els = cur.elements();
545                while (els.hasMoreElements()) {
546                    total.add(els.nextElement());
547                }
548                if (total.size() > 1)
549                    return null;
550            }
551            return total;
552        }
553    }