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