001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.backpred; 004 005 import java.util.*; 006 import java.io.*; 007 008 import javafe.ast.*; 009 import javafe.tc.*; 010 import javafe.util.*; 011 012 import escjava.Main; 013 import escjava.ast.TagConstants; 014 import escjava.ast.TypeExpr; 015 import escjava.prover.Atom; 016 import escjava.translate.*; 017 018 /** 019 * Generates the background predicate for a given type. 020 * 021 * <p> The background predicate <I>for</I> a particular class or 022 * interface type T consists of the conjunction of the background 023 * predicates contributions of each contributor class. See 024 * <code>FindContributors</code> for the definition of the 025 * contributors of a class. 026 027 * <p> A type must be typechecked in order to generate its background 028 * predicate. A type need only be prepped in order to generate its 029 * background predicate contribution. 030 */ 031 032 public class BackPred 033 { 034 /** 035 * Returns the universal background predicate as a sequence of 036 * simplify commands. 037 */ 038 039 public static void genUnivBackPred(/*@ non_null */ PrintStream proverStream) { 040 if (escjava.Main.options().univBackPredFile == null) { 041 proverStream.print(DefaultUnivBackPred.s); 042 return; 043 } 044 String filename = escjava.Main.options().univBackPredFile; 045 try { 046 FileInputStream fis = null; 047 try { 048 fis = new FileInputStream(filename); 049 int c; 050 while( (c=fis.read()) != -1 ) proverStream.print((char)c); 051 } finally { 052 if (fis != null) fis.close(); 053 } 054 } catch( IOException e) { 055 ErrorSet.fatal("IOException: "+e); 056 } 057 } 058 059 060 /** 061 * Return the type-specific background predicate as a formula. 062 */ 063 public static void genTypeBackPred(/*@ non_null */ FindContributors scope, 064 /*@ non_null */ PrintStream proverStream) { 065 // set up the background predicate buffer 066 proverStream.print("(AND "); 067 068 // set up the distinct types axiom buffer 069 StringBuffer dta = 070 new StringBuffer("(DISTINCT arrayType |" 071 + UniqName.type(Types.booleanType) + "| |" 072 + UniqName.type(Types.charType) + "| |" 073 + UniqName.type(Types.byteType) + "| |" 074 + UniqName.type(Types.shortType) + "| |" 075 + UniqName.type(Types.intType) + "| |" 076 + UniqName.type(Types.longType) + "| |" 077 + UniqName.type(Types.floatType) + "| |" 078 + UniqName.type(Types.doubleType) + "| |" 079 + UniqName.type(escjava.tc.Types.typecodeType) + "|"); 080 081 082 // Print them out, and add their contribution to the BP. 083 Info.out("[TypeSig contributors for " 084 +Types.printName(scope.originType)+":"); 085 for( Enumeration typeSigs = scope.typeSigs(); 086 typeSigs.hasMoreElements(); ) 087 { 088 TypeSig sig2 = (TypeSig)typeSigs.nextElement(); 089 Info.out(" "+Types.printName( sig2 )); 090 addContribution( sig2.getTypeDecl(), proverStream ); 091 dta.append(" "+simplifyTypeName( sig2 ) ); 092 } 093 Info.out("]"); 094 095 096 // Add the distinct types axiom 097 bg( dta.toString()+")", proverStream ); 098 099 100 // Handle constant fields' contribution: 101 for( Enumeration fields = scope.fields(); 102 fields.hasMoreElements(); ) { 103 FieldDecl fd = (FieldDecl)fields.nextElement(); 104 if (!Modifiers.isFinal(fd.modifiers) || fd.init==null) 105 continue; 106 107 int loc = fd.init.getStartLoc(); 108 VariableAccess f = VariableAccess.make(fd.id, loc, fd); 109 110 if (Modifiers.isStatic(fd.modifiers)) { 111 genFinalInitInfo(fd.init, null, null, f, fd.type, loc, 112 proverStream); 113 } else { 114 LocalVarDecl sDecl = UniqName.newBoundVariable('s'); 115 VariableAccess s = TrAnExpr.makeVarAccess(sDecl, Location.NULL); 116 genFinalInitInfo(fd.init, sDecl, s, GC.select(f, s), fd.type, 117 loc, proverStream); 118 } 119 } 120 121 proverStream.print(")"); 122 } 123 124 //@ requires loc != Location.NULL; 125 //@ requires sDecl != null ==> s != null; 126 private static void genFinalInitInfo(/*@ non_null */ VarInit initExpr, 127 GenericVarDecl sDecl, Expr s, 128 /*@ non_null */ Expr x, 129 /*@ non_null */ Type type, 130 int loc, 131 /*@ non_null */ PrintStream proverStream) { 132 /* The dynamic type of the field is subtype of the static type of the 133 * initializing expression. 134 */ 135 { 136 Type exprType = TypeCheck.inst.getType(initExpr); 137 Expr tExpr = TypeExpr.make(initExpr.getStartLoc(), 138 initExpr.getEndLoc(), 139 exprType); 140 produce(sDecl, s, GC.nary(TagConstants.IS, x, tExpr), proverStream); 141 } 142 143 /* Generate primitive type constant info */ 144 if (type instanceof PrimitiveType) { 145 if (initExpr instanceof Expr) { 146 Expr constant = eval((Expr)initExpr, loc); 147 if (constant != null) { 148 produce(sDecl, s, eq(x, constant, type), proverStream); 149 } 150 } 151 return; 152 } 153 154 /* Peel off parentheses and casts. */ 155 int tag; 156 while (true) { 157 tag = initExpr.getTag(); 158 159 if (tag == TagConstants.PARENEXPR) { 160 initExpr = ((ParenExpr)initExpr).expr; 161 } else if (tag == TagConstants.CASTEXPR) { 162 initExpr = ((CastExpr)initExpr).expr; 163 } else if (tag == TagConstants.NEWARRAYEXPR) { 164 NewArrayExpr nae = (NewArrayExpr)initExpr; 165 if (nae.init != null) { 166 initExpr = nae.init; 167 tag = initExpr.getTag(); 168 } 169 break; 170 } else { 171 break; 172 } 173 } 174 175 /* Generate null related info */ 176 if (isStaticallyNonNull(initExpr)) { 177 produce(sDecl, s, GC.nary(TagConstants.REFNE, x, GC.nulllit), 178 proverStream); 179 } else if (initExpr.getTag() == TagConstants.NULLLIT) { 180 produce(sDecl, s, GC.nary(TagConstants.REFEQ, x, GC.nulllit), 181 proverStream); 182 } 183 184 /* Generate new and array related info */ 185 if (tag == TagConstants.ARRAYINIT) { 186 ArrayInit aInit = (ArrayInit)initExpr; 187 188 // typeof(x) == array(T) 189 Expr typeofx = GC.nary(TagConstants.TYPEOF, x); 190 Expr arrayT = TypeExpr.make(aInit.getStartLoc(), aInit.getEndLoc(), 191 TypeCheck.inst.getType(aInit)); 192 produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, arrayT), 193 proverStream); 194 195 // arrayLength(x) == len 196 int len = aInit.elems.size(); 197 produce(sDecl, s, GC.nary(TagConstants.INTEGRALEQ, 198 GC.nary(TagConstants.ARRAYLENGTH, x), 199 LiteralExpr.make(TagConstants.INTLIT, 200 new Integer(len), loc)), 201 proverStream); 202 203 } else if (tag == TagConstants.NEWARRAYEXPR) { 204 NewArrayExpr nae = (NewArrayExpr)initExpr; 205 Assert.notFalse(nae.dims.size() > 0); // arrayinit is handled above 206 // typeof(x) == array(...(array(T))) 207 Expr typeofx = GC.nary(TagConstants.TYPEOF, x); 208 Expr arrayT = TypeExpr.make(nae.getStartLoc(), nae.getEndLoc(), 209 TypeCheck.inst.getType(nae)); 210 produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, arrayT), 211 proverStream); 212 213 LiteralExpr constant = eval(nae.dims.elementAt(0), loc); 214 if (constant != null) { 215 Assert.notFalse(constant.getTag() == TagConstants.INTLIT); 216 if (0 <= ((Integer)constant.value).intValue()) { 217 // arrayLength(x) == constant 218 produce(sDecl, s, GC.nary(TagConstants.INTEGRALEQ, 219 GC.nary(TagConstants.ARRAYLENGTH, x), 220 constant), 221 proverStream); 222 } 223 } 224 225 } else if (tag == TagConstants.NEWINSTANCEEXPR) { 226 NewInstanceExpr ni = (NewInstanceExpr)initExpr; 227 // typeof(x) == T 228 Expr typeofx = GC.nary(TagConstants.TYPEOF, x); 229 Expr T = TypeExpr.make(ni.getStartLoc(), ni.getEndLoc(), ni.type); 230 produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, T), 231 proverStream); 232 } 233 } 234 235 //@ requires sDecl != null ==> s != null; 236 private static void produce(GenericVarDecl sDecl, Expr s, 237 /*@ non_null */ Expr e, 238 /*@ non_null */ PrintStream proverStream) { 239 if (sDecl != null) { 240 Expr ant = GC.nary(TagConstants.REFNE, s, GC.nulllit); 241 ExprVec nopats = ExprVec.make(1); 242 nopats.addElement(ant); 243 e = GC.forall(sDecl, GC.implies(ant, e), nopats); 244 } 245 proverStream.print("\n"); 246 VcToString.computeTypeSpecific(e, proverStream); 247 } 248 249 /** 250 * Add to b the contribution from a particular TypeDecl, which is 251 * a formula. 252 */ 253 254 static protected void addContribution(/*@ non_null */ TypeDecl d, 255 /*@ non_null */ PrintStream proverStream) { 256 257 TypeSig sig = TypeCheck.inst.getSig(d); 258 259 // === ESCJ 8: Section 1.1 260 261 if( d instanceof ClassDecl ) { 262 ClassDecl cd = (ClassDecl)d; 263 264 if( cd.superClass != null ) { 265 saySubClass( sig, cd.superClass, proverStream ); 266 } 267 268 if( Modifiers.isFinal(cd.modifiers) ) 269 sayIsFinal( sig, proverStream ); 270 271 } else { 272 saySubType( sig, Types.javaLangObject(), proverStream ); 273 } 274 275 for( int i=0; i<d.superInterfaces.size(); i++ ) 276 saySubType( sig, d.superInterfaces.elementAt(i), proverStream ); 277 278 saySuper(d, proverStream); 279 } 280 281 282 /** Record in the background predicate that x is a subclass of y. */ 283 284 private static void saySubClass( Type x, Type y, 285 /*@ non_null */ PrintStream proverStream ) { 286 287 saySubType( x, y, proverStream ); 288 bg("(EQ "+simplifyTypeName(x)+ 289 " (asChild "+simplifyTypeName(x)+" "+simplifyTypeName(y)+"))", 290 proverStream); 291 } 292 293 /** Record in the background predicate that x is a subtype of y. */ 294 295 private static void saySubType( Type x, Type y, 296 /*@ non_null */ PrintStream proverStream ) { 297 298 bg( "(<: "+simplifyTypeName(x)+" "+simplifyTypeName(y)+")" , proverStream); 299 300 } 301 302 private static void saySuper(TypeDecl d, /*@ non_null*/ PrintStream proverStream) { 303 TypeSig sig = TypeCheck.inst.getSig(d); 304 String n = simplifyTypeName(sig); 305 StringBuffer b = new StringBuffer(); 306 b.append( "(FORALL (t) (PATS (<: "+n+" t)) " + 307 "(IFF (<: "+n+" t) (OR (EQ t "+n+") "); 308 if( d instanceof ClassDecl ) { 309 ClassDecl cd = (ClassDecl)d; 310 311 if( cd.superClass != null ) { 312 String sp = simplifyTypeName(cd.superClass); 313 b.append("(<: "+sp+" t) "); 314 } 315 } else { 316 b.append( "(EQ t |T_java.lang.Object|) "); 317 } 318 for( int i=0; i<d.superInterfaces.size(); i++ ) { 319 String tt = simplifyTypeName(d.superInterfaces.elementAt(i)); 320 b.append( "(<: " +tt+" t) "); 321 } 322 b.append(" )))"); 323 324 bg(b.toString(),proverStream); 325 326 } 327 328 /** Record in the background predicate that x is final. */ 329 330 private static void sayIsFinal( Type x, 331 /*@ non_null */ PrintStream proverStream ) { 332 String n = simplifyTypeName(x); 333 bg( "(FORALL (t) (PATS (<: t "+n+")) (IFF (<: t "+n+") (EQ t "+n+")))", 334 proverStream); 335 } 336 337 public static String simplifyTypeName(/*@ non_null */ Type x) { 338 if (x instanceof ArrayType) { 339 ArrayType at = (ArrayType)x; 340 return "(|_array| " + simplifyTypeName(at.elemType) + ")"; 341 } else { 342 return Atom.printableVersion(UniqName.type(x)); 343 } 344 } 345 346 /** 347 * Called with an S-expression that may contain a free variable 348 * "t". Wraps "(FORALL (s) (IMPLIES (NEQ s null) " and "))" 349 * around this expression and adds it to the background predicate. 350 */ 351 352 protected static void bgi(/*@ non_null */ String s, 353 /*@ non_null */ PrintStream proverStream) { 354 proverStream.print("\n(FORALL (s) (IMPLIES (NEQ s null) "); 355 proverStream.print(s); 356 proverStream.print("))"); 357 } 358 359 /** 360 * Called with a simplify command. Adds it to the background 361 * predicate. 362 */ 363 364 protected static void bg(/*@ non_null */ String s, 365 /*@ non_null */ PrintStream proverStream) { 366 proverStream.print('\n'); 367 proverStream.print(s); 368 } 369 370 371 // ====================================================================== 372 373 /** 374 * Do we know statically that an expression always returns a 375 * non-null value? 376 */ 377 protected static boolean isStaticallyNonNull(VarInit e) { 378 int tag = e.getTag(); 379 380 // New expressions are always non-null: 381 if (tag==TagConstants.NEWARRAYEXPR || 382 tag==TagConstants.NEWINSTANCEEXPR) 383 return true; 384 385 // Array initializers are always non-null: 386 if (tag==TagConstants.ARRAYINIT) 387 return true; 388 389 // String constants can be non-null: 390 if (tag==TagConstants.STRINGLIT) { 391 LiteralExpr asLit = (LiteralExpr)e; 392 if (asLit.value != null) 393 return true; 394 } 395 396 if (tag == TagConstants.ADD || tag == TagConstants.ASGADD) { 397 BinaryExpr be = (BinaryExpr)e; 398 Type leftType = TypeCheck.inst.getType( be.left ); 399 Type rightType = TypeCheck.inst.getType( be.right ); 400 if (Types.isReferenceOrNullType(leftType) || 401 Types.isReferenceOrNullType(rightType)) { 402 // The "+" or "+=" operator is String catenation, which always 403 // returns a non-null value. 404 return true; 405 } 406 } 407 408 return false; 409 } 410 411 412 /** 413 * Like ConstantExpr.eval, but returns a LiteralExpr instead of an 414 * Integer/Long/etc. 415 * 416 * <p> Ignores String constants. (Always returns null in that case.) 417 * 418 * <p> If returns a non-null LiteralExpr, sets its loc to 419 * <code>loc</code>. 420 */ 421 //@ requires e!=null && loc!=Location.NULL; 422 protected static LiteralExpr eval(Expr e, int loc) { 423 Object val = ConstantExpr.eval(e); 424 425 if (val instanceof Boolean) 426 return LiteralExpr.make(TagConstants.BOOLEANLIT, val, loc); 427 428 // char, byte, short, int cases: 429 if (val instanceof Integer) 430 return LiteralExpr.make(TagConstants.INTLIT, val, loc); 431 432 if (val instanceof Long) 433 return LiteralExpr.make(TagConstants.LONGLIT, val, loc); 434 435 if (val instanceof Float) 436 return LiteralExpr.make(TagConstants.FLOATLIT, val, loc); 437 if (val instanceof Double) 438 return LiteralExpr.make(TagConstants.DOUBLELIT, val, loc); 439 440 // Ignore String because don't have the right location 441 442 return null; 443 } 444 445 446 /** 447 * Generate the appropriate GC equality e1 == e2 based on type t. 448 */ 449 //@ requires e1 != null && e2!=null && t!=null; 450 //@ ensures \result != null; 451 protected static Expr eq(Expr e1, Expr e2, Type t) { 452 if (!(t instanceof PrimitiveType)) 453 return GC.nary(TagConstants.REFEQ, e1, e2); 454 455 switch (t.getTag()) { 456 case TagConstants.NULLTYPE: 457 return GC.nary(TagConstants.REFEQ, e1, e2); 458 459 case TagConstants.BOOLEANTYPE: 460 return GC.nary(TagConstants.BOOLEQ, e1, e2); 461 462 case TagConstants.CHARTYPE: 463 case TagConstants.BYTETYPE: 464 case TagConstants.SHORTTYPE: 465 case TagConstants.INTTYPE: 466 case TagConstants.LONGTYPE: 467 return GC.nary(TagConstants.INTEGRALEQ, e1, e2); 468 469 case TagConstants.FLOATTYPE: 470 case TagConstants.DOUBLETYPE: 471 return GC.nary(TagConstants.FLOATINGEQ, e1, e2); 472 473 case TagConstants.TYPECODE: 474 return GC.nary(TagConstants.TYPEEQ, e1, e2); 475 476 default: 477 Assert.fail("Bad primitive type passed to BackPred.eq:" 478 + TagConstants.toString(t.getTag())); 479 return null; // keep compiler happy... 480 } 481 } 482 }