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 }