001 // $Id: FlowInsensitiveChecks.java,v 1.92 2006/09/25 15:48:32 chalin Exp $
002 /* Copyright 2000, 2001, Compaq Computer Corporation */
003
004 package escjava.tc;
005
006 import java.util.Enumeration;
007
008 import javafe.ast.*;
009
010 import javafe.tc.Env;
011 import javafe.tc.EnvForLocals;
012 import javafe.tc.EnvForTypeSig;
013 import javafe.tc.LookupException;
014 import javafe.tc.TypeSig;
015
016 import javafe.util.*;
017
018 import escjava.ast.*;
019 import escjava.ast.Modifiers;
020 import escjava.ast.TagConstants;
021 import escjava.tc.Types;
022 import escjava.Main;
023
024 public class FlowInsensitiveChecks extends javafe.tc.FlowInsensitiveChecks
025 {
026 static {
027 inst = new FlowInsensitiveChecks();
028 }
029 static public javafe.tc.FlowInsensitiveChecks inst() { return inst; }
030
031 // Setup for ghost variables
032
033 /**
034 * Are we in the middle of processing an annotation? (Used by {@link GhostEnv}.)
035 */
036 public static boolean inAnnotation = false;
037 public static boolean inModelBody = false;
038 // FIXME - the above two variables are a hack! Note that below we have to save and
039 // restore their values so that the appropriate values are read out of these
040 // global-static variables by GhostEnv. It would be much better to create a sub
041 // Env that understands what to do and pass that along for the checks. -- DRCok
042
043 public escjava.AnnotationHandler annotationHandler =
044 new escjava.AnnotationHandler();
045 /**
046 * Indicates whether <code>LS</code> is allowed in this context. The default is
047 * <code>true</code>. For contexts where <code>LS</code> is not allowed,
048 * <code>isLocksetContext</code> should be set <code>false</code> only temporarily.
049 */
050 protected boolean isLocksetContext = true;
051
052 /**
053 * <code>\result</code> is allowed in this context when <code>isRESContext</code>
054 * is <code>true</code> and <code>returnType != null</code>. The default value
055 * of <code>isRESContext</code> is <code>false</code>. For contexts where
056 * <code>isRESContext</code> should be <code>true</code>,
057 * <code>isRESContext</code> should be set to <code>true</code> only temporarily.
058 */
059 protected boolean isRESContext = false;
060
061 /**
062 * Indicates whether <code>\old</code> and <code>\fresh</code> are allowed in
063 * this context. The default is <code>false</code>. For contexts where these
064 * functions are allowed, <code>isTwoStateContext</code> should be set
065 * <code>true</code> only temporarily.
066 */
067 protected boolean isTwoStateContext = false;
068
069 /**
070 * Indicates whether checking is currently being done inside a <code>PRE</code>.
071 * This is used by the code that disallows nested <code>PRE</code> expressions.
072 * Note: alternatively, one could use <code>isTwoStateContext</code> to implement
073 * this functionality, but by having a separate bit, a more precise error message
074 * can be produced.
075 */
076 protected boolean isInsidePRE = false;
077
078 /**
079 * Indicates whether a quantification or labeled predicate is allowed in this
080 * context. This boolean is used only between one call of <code>checkExpr</code>
081 * to a following recursive call.
082 */
083 protected boolean isPredicateContext = false;
084
085 /**
086 * Indicates whether private field accesses are allowed in the current context.
087 * Private field accesses are allowed everywhere, except in postconditions of
088 * overridable methods.
089 */
090 protected boolean isPrivateFieldAccessAllowed = true;
091
092 protected int accessibilityLowerBound = ACC_LOW_BOUND_Private;
093 // Note, "ACC_LOW_BOUND_Private" would be the same as "no lower bound"
094 protected static final int ACC_LOW_BOUND_Private = 0;
095 protected static final int ACC_LOW_BOUND_Package = 1;
096 protected static final int ACC_LOW_BOUND_Protected = 2;
097 protected static final int ACC_LOW_BOUND_Public = 3;
098
099 /**
100 * If <code>accessibilityLowerBound != ACC_LOW_BOUND_Private</code>, then
101 * <code>accessibilityContext</code> is the field or routine whose modifier
102 * pragma is being type checked.
103 */
104 /*@ invariant accessibilityContext == null ||
105 @ accessibilityContext instanceof FieldDecl ||
106 @ accessibilityContext instanceof RoutineDecl;
107 */
108 //@ readable accessibilityContext if accessibilityLowerBound != ACC_LOW_BOUND_Private;
109 protected ASTNode accessibilityContext;
110
111 /**
112 * Acts as a parameter to <code>checkExpr</code>. Its value is meaningful only
113 * on entry to <code>checkExpr</code>. It indicates whether the expression to be
114 * checked is in a specification designator context. In particular, this
115 * parameter is used to disallow array index wild cards in non-spec designator
116 * contexts.
117 */
118 protected boolean isSpecDesignatorContext = false;
119
120 /**
121 * Contains the loop invariant statement pragmas seen so far and not yet
122 * processed.
123 */
124 protected ExprStmtPragmaVec loopInvariants = ExprStmtPragmaVec.make();
125
126 /**
127 * Contains the loop decreases statement pragmas seen so far and not yet
128 * processed.
129 */
130 protected ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make();
131
132 protected ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make();
133
134 protected LocalVarDeclVec skolemConstants = LocalVarDeclVec.make();
135
136 /**
137 * Indicates whether we are are checking an invariant pragma.
138 */
139 protected boolean invariantContext = false;
140
141 /**
142 * Counts the number of accesses of free variables and fields used for checking
143 * the appropriateness of invariants.
144 */
145 //@ readable countFreeVarsAccesses if invariantContext;
146 protected int countFreeVarsAccesses = 0 ;
147
148 /**
149 * Override so that we use {@link GhostEnv} instead of {@link EnvForTypeSig}.
150 */
151 protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
152 boolean staticContext) {
153 return new GhostEnv(s.getEnclosingEnv(), s, staticContext);
154 }
155
156 public static ASTDecoration envDecoration =
157 new ASTDecoration("env");
158 public static ASTDecoration staticenvDecoration =
159 new ASTDecoration("staticenv");
160
161 public void checkTypeDeclaration(/*@ non_null */ TypeSig s) {
162 super.checkTypeDeclaration(s);
163 TypeDecl td = s.getTypeDecl();
164 envDecoration.set(td,rootIEnv);
165 staticenvDecoration.set(td,rootSEnv);
166 }
167
168 // Extensions to type declaration member checkers.
169
170 protected void checkTypeDeclElem(TypeDeclElem e) {
171 boolean savedInAnnotation = inAnnotation;
172 boolean savedInModelBody = inModelBody;
173 // FIXME - should this use Utils.isModel ???
174 if (e instanceof ConstructorDecl &&
175 null != Utils.findModifierPragma(((ConstructorDecl)e).pmodifiers,TagConstants.MODEL)) {
176 inAnnotation = true;
177 inModelBody = true;
178 }
179 if (e instanceof MethodDecl &&
180 null != Utils.findModifierPragma(((MethodDecl)e).pmodifiers,TagConstants.MODEL)) {
181 inAnnotation = true;
182 inModelBody = true;
183 }
184 try {
185 super.checkTypeDeclElem(e);
186 if (e instanceof RoutineDecl) {
187 // Desugaring presumes that typechecking has already
188 // been performed
189 RoutineDecl m = (RoutineDecl)e;
190 /*
191 if ((m instanceof ConstructorDecl) && m.implicit) {
192 // The desugaring of m can require the desugared
193 // specs of a parent constructor, so we have to be
194 // sure that the parent constructor is typechecked.
195 TypeSig s = TypeSig.getSig(m.parent).superClass();
196 if (s != null) checkTypeDeclElem(s.getTypeDecl());
197 }
198 */
199 /*
200 if (m.originalRaises != null &&
201 m.originalRaises.size() != m.raises.size()) {
202
203 for (int i=m.originalRaises.size()+1; i < m.raises.size(); ++i) {
204
205 TypeSig t = TypeSig.getSig(m.raises.elementAt(i));
206 System.out.println("FOUND " + t);
207 if (!t.isSubtypeOf(Types.javaLangRuntimeException())) {
208 ErrorSet.error(m.raises.elementAt(i).getStartLoc(),
209 "The type " + t + " is not a subtype of " +
210 "RuntimeException and is not declared by the API, and " +
211 "consequently may not be declared in a specification.");
212 System.out.println("BAD");
213 }
214 }
215 }
216 */
217 annotationHandler.desugar(m);
218 }
219 } finally {
220 inAnnotation = savedInAnnotation;
221 inModelBody = savedInModelBody;
222 }
223
224 // Do a separate set of checks - purity checking
225 // FIXME - perhaps these should be moved into this routine
226 annotationHandler.process(e);
227
228 if (e.getTag() == TagConstants.INITBLOCK) {
229 InitBlock ib = (InitBlock)e;
230 if (ib.pmodifiers != null) {
231 checkModifierPragmaVec(ib.pmodifiers,ib,
232 Modifiers.isStatic(ib.modifiers) ? rootSEnv : rootIEnv);
233 /*
234 for (int i = 0; i < ib.pmodifiers.size(); i++) {
235 ModifierPragma mp = (ModifierPragma)ib.pmodifiers.elementAt(i);
236 ErrorSet.error(mp.getStartLoc(),
237 TagConstants.toString(mp.getTag()) +
238 " pragma cannot be applied to initializer block");
239 }
240 */
241 }
242 }
243
244 }
245
246 // Extensions to Expr and Stmt checkers.
247
248 protected Env checkStmt(Env env, Stmt s) {
249 boolean savedTwoStateContext = isTwoStateContext;
250 isTwoStateContext = true;
251 try {
252 int tag = s.getTag();
253
254 // Check for any loop invariants, loop bounds, loop predicates, or skolem
255 // constants in the wrong place
256 if (loopInvariants.size() != 0 ||
257 loopDecreases.size() != 0 ||
258 loopPredicates.size() != 0 ||
259 skolemConstants.size() != 0) {
260 switch (tag) {
261 case TagConstants.DOSTMT:
262 case TagConstants.WHILESTMT:
263 case TagConstants.FORSTMT:
264 case TagConstants.LABELSTMT:
265 case TagConstants.LOOP_INVARIANT:
266 case TagConstants.MAINTAINING:
267 case TagConstants.DECREASES:
268 case TagConstants.DECREASING:
269 case TagConstants.LOOP_PREDICATE:
270 case TagConstants.SKOLEMCONSTANTPRAGMA:
271 break;
272 default:
273 checkLoopInvariants(env, false);
274 checkLoopDecreases(env, false);
275 checkLoopPredicates(env, false);
276 checkSkolemConstants(env, false);
277 break;
278 }
279 }
280
281 switch(tag) {
282 case TagConstants.DOSTMT:
283 case TagConstants.WHILESTMT: {
284 checkLoopInvariants(env, true);
285 checkLoopDecreases(env, true);
286 Env newEnv = checkSkolemConstants(env, true);
287 checkLoopPredicates(newEnv, true);
288 super.checkStmt(env, s);
289 break;
290 }
291 case TagConstants.FORSTMT: {
292 ForStmt f = (ForStmt)s;
293
294 ExprStmtPragmaVec invs = loopInvariants;
295 ExprStmtPragmaVec decrs = loopDecreases;
296 ExprStmtPragmaVec preds = loopPredicates;
297 LocalVarDeclVec skolemConsts = skolemConstants;
298
299 loopInvariants = ExprStmtPragmaVec.make();
300 loopDecreases = ExprStmtPragmaVec.make();
301 loopPredicates = ExprStmtPragmaVec.make();
302 skolemConstants = LocalVarDeclVec.make();
303
304 Env se = checkStmtVec(env, f.forInit);
305
306 Assert.notFalse(loopInvariants.size() == 0);
307 Assert.notFalse(loopDecreases.size() == 0);
308 Assert.notFalse(loopPredicates.size() == 0);
309 Assert.notFalse(skolemConstants.size() == 0);
310
311 loopInvariants = invs;
312 loopDecreases = decrs;
313 loopPredicates = preds;
314 skolemConstants = skolemConsts;
315
316 checkLoopInvariants(se, true);
317 checkLoopDecreases(se, true);
318 Env newEnv = checkSkolemConstants(se, true);
319 checkLoopPredicates(newEnv, true);
320 checkForLoopAfterInit(se, f);
321 break;
322 }
323 case TagConstants.BLOCKSTMT: {
324 env = super.checkStmt(env, s);
325 // Check for any loop_invariant statement pragmas at the end of the
326 // body.
327 checkLoopInvariants(env, false);
328 checkLoopDecreases(env, false);
329 checkLoopPredicates(env, false);
330 checkSkolemConstants(env, false);
331 break;
332 }
333 case TagConstants.VARDECLSTMT: {
334 VarDeclStmt vs = (VarDeclStmt)s;
335 LocalVarDecl x = vs.decl;
336 if (Utils.findModifierPragma(x.pmodifiers,
337 TagConstants.GHOST) != null) {
338 boolean savedInAnnotation = inAnnotation;
339 inAnnotation = true;
340 try {
341 env.resolveType(sig, x.type);
342 checkTypeModifiers(env, x.type);
343 javafe.tc.PrepTypeDeclaration.getInst().
344 checkModifiers(x.modifiers, Modifiers.ACC_FINAL,
345 x.locId, "local ghost variable");
346 checkModifierPragmaVec(x.pmodifiers, x, env);
347
348 Env newEnv = new EnvForGhostLocals(env,x);
349 if (x.init != null)
350 x.init = checkInit(newEnv, x.init, x.type);
351 env = newEnv;
352 } finally {
353 inAnnotation = savedInAnnotation;
354 }
355 break;
356 }
357
358 env = super.checkStmt(env, s);
359 break;
360
361 }
362 case TagConstants.CLASSDECLSTMT: {
363 ClassDeclStmt cds = (ClassDeclStmt)s;
364 ClassDecl cd = cds.decl;
365 (new escjava.AnnotationHandler.NestedPragmaParser()).parseAllRoutineSpecs(cd);
366 env = super.checkStmt(env, s);
367 annotationHandler.desugar(cd);
368 break;
369 }
370 default:
371 env = super.checkStmt(env, s);
372 break;
373 }
374
375 } finally {
376 isTwoStateContext = savedTwoStateContext;
377 }
378 return env;
379 }
380
381 protected void checkLoopInvariants(Env env, boolean allowed) {
382 for (int i = 0; i < loopInvariants.size(); i++) {
383 ExprStmtPragma s = loopInvariants.elementAt(i);
384 Assert.notFalse(s.getTag() == TagConstants.LOOP_INVARIANT
385 || s.getTag() == TagConstants.MAINTAINING);
386 if (allowed) {
387 //Assert.notFalse(!isTwoStateContext);
388 Assert.notFalse(!inAnnotation || inModelBody);
389 boolean savedInAnnotation = inAnnotation;
390 inAnnotation = true;
391 //isTwoStateContext = true;
392 try {
393 s.expr = checkPredicate(env, s.expr);
394 } finally {
395 inAnnotation = savedInAnnotation;
396 //isTwoStateContext = false;
397 }
398 } else {
399 errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_INVARIANT);
400 }
401 }
402 loopInvariants.removeAllElements();
403 }
404
405 protected void checkLoopDecreases(Env env, boolean allowed) {
406 for (int i = 0; i < loopDecreases.size(); i++) {
407 ExprStmtPragma s = loopDecreases.elementAt(i);
408 Assert.notFalse(s.getTag() == TagConstants.DECREASES
409 || s.getTag() == TagConstants.DECREASING);
410 if (allowed) {
411 //Assert.notFalse(!isTwoStateContext);
412 Assert.notFalse(!inAnnotation || inModelBody);
413 boolean savedInAnnotation = inAnnotation;
414 inAnnotation = true;
415 try {
416 s.expr = checkExpr(env, s.expr, Types.bigintType);
417 } finally {
418 inAnnotation = savedInAnnotation;
419 }
420 } else {
421 errorExpectingLoop(s.getStartLoc(), TagConstants.DECREASES);
422 }
423 }
424 loopDecreases.removeAllElements();
425 }
426
427 protected void checkLoopPredicates(Env env, boolean allowed) {
428 for (int i = 0; i < loopPredicates.size(); i++) {
429 ExprStmtPragma s = loopPredicates.elementAt(i);
430 Assert.notFalse(s.getTag() == TagConstants.LOOP_PREDICATE);
431 if (allowed) {
432 //Assert.notFalse(!isTwoStateContext);
433 Assert.notFalse(!inAnnotation || inModelBody);
434 boolean savedInAnnotation = inAnnotation;
435 inAnnotation = true;
436 //isTwoStateContext = true;
437 try {
438 s.expr = checkPredicate(env, s.expr);
439 } finally {
440 inAnnotation = savedInAnnotation;
441 //isTwoStateContext = false;
442 }
443 } else {
444 errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_PREDICATE);
445 }
446 }
447 loopPredicates.removeAllElements();
448 }
449
450 protected Env checkSkolemConstants(Env env, boolean allowed) {
451 for (int i = 0; i < skolemConstants.size(); i++) {
452 LocalVarDecl s = skolemConstants.elementAt(i);
453 if (allowed) {
454 //Assert.notFalse(!isTwoStateContext);
455 Assert.notFalse(!inAnnotation || inModelBody);
456 boolean savedInAnnotation = inAnnotation;
457 inAnnotation = true;
458 //isTwoStateContext = true;
459 try {
460 env.resolveType(sig, s.type);
461 env = new EnvForLocals(env, s);
462 } finally {
463 inAnnotation = savedInAnnotation;
464 //isTwoStateContext = false;
465 }
466 } else {
467 errorExpectingLoop(s.getStartLoc(), TagConstants.SKOLEM_CONSTANT);
468 }
469 }
470 skolemConstants.removeAllElements();
471 return env;
472 }
473
474 private void errorExpectingLoop(int loc, int tag) {
475 ErrorSet.error(loc, "'" + TagConstants.toString(tag) +
476 "' pragmas can occur " +
477 "only immediately prior to a loop statement. Loop " +
478 "statement expected (and not found) here.");
479 }
480
481 protected Expr checkPredicate(Env env, Expr e) {
482 boolean savedPredicateContext = isPredicateContext;
483 isPredicateContext = true;
484 Expr ee = checkExpr(env, e, Types.booleanType);
485 isPredicateContext = savedPredicateContext;
486 return ee;
487 }
488
489 protected Expr checkExpr(/*@non_null*/ Env env, /*@non_null*/ Expr e) {
490 // Anticipate that the next context is probably not one suitable for
491 // quantifications and labels. "isPredicateContext" must revert to its old
492 // value before return.
493 boolean isCurrentlyPredicateContext = isPredicateContext;
494 isPredicateContext = false;
495
496 try {
497
498 if (getTypeOrNull(e) != null )
499 // already done
500 return e;
501
502 // No recursive call to "checkExpr" is a specification designator context, so
503 // set "isSpecDesignatorContext" to "false", keeping the initial value in
504 // local variable "isCurrentlySpecDesignatorContext".
505 boolean isCurrentlySpecDesignatorContext = isSpecDesignatorContext;
506 isSpecDesignatorContext = false;
507
508 int tag = e.getTag();
509 switch(tag) {
510
511 // Handle accesses to ghost fields as well...
512 case TagConstants.FIELDACCESS:
513 {
514 if (!inAnnotation)
515 return super.checkExpr(env, e);
516
517 // a field access is considerded a free variable access in an
518 // invariant.
519 if (invariantContext) countFreeVarsAccesses++;
520
521 // set default result type to errorType, in case there is an error.
522 setType( e, Types.errorType );
523 FieldAccess fa = (FieldAccess)e;
524 Type t = checkObjectDesignator(env, fa.od);
525 if (t==null) {
526 //alx: dw field has not target, take universe of declaration
527 // (when should this happen?)
528 if (useUniverses)
529 copyUniverses(fa,fa.decl);
530 //alx-end
531 return fa;
532 }
533 if (t instanceof TypeName)
534 t = TypeSig.getSig( (TypeName) t );
535
536 if (Types.isErrorType(t)) {
537 setType( fa, Types.errorType );
538 return fa;
539 }
540
541 try {
542 fa.decl = escjava.tc.Types.lookupField( t, fa.id, sig );
543 //alx: dw
544 if (useUniverses)
545 determineUniverseForFieldAccess(fa);
546 //alx-end
547 } catch( LookupException ex) {
548 if (!Types.isErrorType(t))
549 reportLookupException(ex, "field",
550 Types.printName(t), fa.locId);
551 setType( fa, Types.errorType );
552 return fa;
553 }
554 setType( fa, fa.decl.type );
555
556 if (fa.od instanceof TypeObjectDesignator &&
557 !GhostEnv.isStatic(fa.decl)) {
558 // Is fa.decl an instance field of the same class as fa is
559 // part of?
560 boolean thisField = false;
561 if (fa.decl.parent != null)
562 thisField = (env.getEnclosingClass()
563 .isSubtypeOf(TypeSig.getSig(fa.decl.parent)));
564
565 if (thisField ||
566 ((TypeObjectDesignator)fa.od).type instanceof TypeName) {
567
568 ErrorSet.error(fa.locId,
569 "An instance field may be accessed only via "
570 + "an object and/or from a non-static"
571 + " context or an inner class enclosed"
572 + " by a type possessing that field.");
573
574 } else
575 ErrorSet.error(fa.locId,
576 "The instance fields of type "
577 + ((TypeObjectDesignator)fa.od).type
578 + " may not be accessed from type "
579 + sig );
580 }
581
582 /* FIXME -- need to clean up testing of access modifiers and to make them
583 consistent with JML
584 if (!isPrivateFieldAccessAllowed &&
585 Modifiers.isPrivate(fa.decl.modifiers) &&
586 Utils.findModifierPragma(fa.decl,
587 TagConstants.SPEC_PUBLIC) == null &&
588 Utils.findModifierPragma(fa.decl,
589 TagConstants.SPEC_PROTECTED) == null) {
590 ErrorSet.error(fa.locId,
591 "A private field can be used in "+
592 "postconditions of overridable methods only if "+
593 "it is declared spec_public or spec_protected");
594 }
595 */
596
597 // The following code checks that "fa" is at least as
598 // spec-accessible as "accessibilityContext" is Java-accessible.
599 // This is vacuously true if "accessibilityLowerBound" is
600 // private.
601 if (accessibilityLowerBound != ACC_LOW_BOUND_Private) {
602 boolean isAccessibleEnough;
603 if (Modifiers.isPublic(fa.decl.modifiers) ||
604 Utils.findModifierPragma(fa.decl,
605 TagConstants.SPEC_PUBLIC) != null) {
606 // public and spec_public fields are always accessible
607 isAccessibleEnough = true;
608 } else if (Utils.findModifierPragma(fa.decl,
609 TagConstants.SPEC_PROTECTED) != null) {
610
611 // Copied from the protected case down below.
612 isAccessibleEnough = false;
613 if (accessibilityLowerBound == ACC_LOW_BOUND_Package) {
614 isAccessibleEnough = true;
615 } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) {
616 TypeDecl tdContext;
617 if (accessibilityContext instanceof FieldDecl) {
618 tdContext = ((FieldDecl)accessibilityContext).parent;
619 } else {
620 tdContext = ((RoutineDecl)accessibilityContext).parent;
621 }
622 TypeSig tsContext = TypeSig.getSig(tdContext);
623 if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) {
624 isAccessibleEnough = true;
625 }
626 }
627
628 } else if (Modifiers.isPrivate(fa.decl.modifiers)) {
629 // Note: if "fa" type-checked so far, then "fa.decl" and
630 // "accessibilityContext" are declared in the same class.
631 // It would be nice to assert this fact at run-time, but
632 // control may reach this point even if "fa" does not
633 // type-check above.
634
635 // "fa.decl" can be private only if
636 // "accessibilityContext" is private, which was checked
637 // above
638 isAccessibleEnough = false;
639
640 } else if (Modifiers.isPackage(fa.decl.modifiers)) {
641 // Note: if "fa" type-checked so far, then "fa.decl" and
642 // "accessibilityContext" are declared in the same
643 // package. It would be nice to assert this fact at
644 // run-time, but control may reach this point even if
645 // "fa" does not type-check above.
646
647 // "fa.decl" can be package (default) accessible only if
648 // "accessibilityContext" is private (which was checked
649 // above) or package
650 isAccessibleEnough =
651 (accessibilityLowerBound == ACC_LOW_BOUND_Package);
652
653 } else {
654 Assert.notFalse(Modifiers.isProtected(fa.decl.modifiers));
655 // Note: if "fa" type-checked so far, then either
656 // "fa.decl" and "accessibilityContext" are declared in
657 // the same package or the class declaring
658 // "accessibilityContext" is a subtype of the class
659 // declaring "fa.decl". It would be nice to assert this
660 // fact at run-time, but control may reach this point
661 // even if "fa" does not type-check above.
662
663 // "fa.decl" can be protected only if
664 // "accessibilityContext" is private (which was checked
665 // above) or package, or if "accessibilityContext" is
666 // protected and "fa.decl" is declared in a superclass of
667 // the class that declares "accessibilityContext".
668 isAccessibleEnough = false;
669 if (accessibilityLowerBound == ACC_LOW_BOUND_Package) {
670 isAccessibleEnough = true;
671 } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) {
672 TypeDecl tdContext;
673 if (accessibilityContext instanceof FieldDecl) {
674 tdContext = ((FieldDecl)accessibilityContext).parent;
675 } else {
676 tdContext = ((RoutineDecl)accessibilityContext).parent;
677 }
678 TypeSig tsContext = TypeSig.getSig(tdContext);
679 if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) {
680 isAccessibleEnough = true;
681 }
682 }
683 }
684 /* Need to fix the accessibility checking to conform with JML - FIXME
685 if (!isAccessibleEnough) {
686 ErrorSet.error(fa.locId, "Fields mentioned in this modifier "+
687 "pragma must be at least as accessible "+
688 "as the field/method being modified (perhaps "+
689 "try spec_public)");
690 }
691 */
692 }
693
694 return fa;
695 }
696
697 case TagConstants.METHODINVOCATION:
698 {
699 countFreeVarsAccesses++;
700 MethodInvocation mi = (MethodInvocation)e;
701 Type t = checkObjectDesignator(env, mi.od);
702 if (mi.od instanceof ExprObjectDesignator && Types.objectsetType == t) {
703 // FIXME - all reach expressions are true for now
704 Expr ee = LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.TRUE,
705 Location.NULL);
706 setType(ee, Types.booleanType);
707 //alx: dw could be hardcoded
708 if (useUniverses)
709 determineUniverseForMethodInvocation(mi);
710 //alx-end
711
712 return ee;
713 } else {
714 Expr ee = super.checkExpr(env,e);
715 return ee;
716 }
717 }
718
719 case TagConstants.IMPLIES:
720 case TagConstants.EXPLIES:
721 case TagConstants.IFF:
722 case TagConstants.NIFF:
723 {
724 BinaryExpr be = (BinaryExpr)e;
725 // each argument is allowed to contain quantifiers and labels if
726 // this expression is
727 isPredicateContext = isCurrentlyPredicateContext;
728 be.left = checkExpr(env, be.left, Types.booleanType);
729 isPredicateContext = isCurrentlyPredicateContext;
730 be.right = checkExpr(env, be.right, Types.booleanType);
731
732 // check illegal associativity of ==> and <==
733 if ((tag == TagConstants.IMPLIES &&
734 (be.left.getTag() == TagConstants.EXPLIES ||
735 be.right.getTag() == TagConstants.EXPLIES)) ||
736 (tag == TagConstants.EXPLIES &&
737 (be.left.getTag() == TagConstants.IMPLIES ||
738 be.right.getTag() == TagConstants.IMPLIES))) {
739 // unfortunately, we don't have the location of either of the
740 // operators at fault
741 ErrorSet.error(be.getStartLoc(),
742 "Ambiguous association of ==> and <==. " +
743 "Use parentheses to disambiguate.");
744 }
745
746 setType(e, Types.booleanType);
747 return e;
748 }
749
750 case TagConstants.DOTDOT:
751 {
752 BinaryExpr be = (BinaryExpr)e;
753 // each argument is allowed to contain quantifiers and labels if
754 // this expression is
755 isPredicateContext = false;
756 be.left = checkExpr(env, be.left, Types.intType);
757 be.right = checkExpr(env, be.right, Types.intType);
758
759 // FIXME - this really needs to be a range type
760 setType(e, Types.intType);
761 return e;
762 }
763
764 case TagConstants.SUBTYPE:
765 {
766 BinaryExpr be = (BinaryExpr)e;
767 Type expected = Types.booleanType;
768 if (tag == TagConstants.SUBTYPE)
769 expected = Types.typecodeType;
770 be.left = checkExpr(env, be.left, expected);
771 be.right = checkExpr(env, be.right, expected);
772 setType(e, Types.booleanType);
773 return e;
774 }
775
776 case TagConstants.REACH: {
777 // FIXME - just enough to get by for now
778 NaryExpr ne = (NaryExpr)e;
779 Expr nu =
780 checkExpr(env, ne.exprs.elementAt(0));
781 ne.exprs.setElementAt(nu, 0);
782 if (ne.exprs.size() != 1) {
783 ErrorSet.error(ne.sloc,
784 "A \\reach expression expects just one argument");
785 setType(e, Types.errorType);
786 } else if (!Types.isReferenceOrNullType(getType(nu))) {
787 ErrorSet.error(nu.getStartLoc(),
788 "A \\reach expression expects an Object argument");
789 } else {
790 setType(e, Types.objectsetType);
791 }
792 return e;
793 }
794
795 case TagConstants.FRESH:
796 {
797 NaryExpr ne = (NaryExpr)e;
798 if (ne.exprs.size() == 0) {
799 ErrorSet.error(ne.sloc,
800 "The function fresh must have at least one argument");
801 } else if (!isTwoStateContext) {
802 ErrorSet.error(ne.sloc,
803 "The function \\fresh cannot be used in this context");
804 } else if (isInsidePRE) {
805 ErrorSet.error(ne.sloc, "The function \\fresh cannot be used "+
806 "inside a \\old expression");
807 } else {
808 for (int i = 0; i<ne.exprs.size(); ++i) {
809 Expr nu =
810 checkExpr(env, ne.exprs.elementAt(i), Types.javaLangObject());
811 ne.exprs.setElementAt(nu, i);
812 }
813 }
814 setType(e, Types.booleanType);
815 return e;
816 }
817
818 case TagConstants.ELEMSNONNULL:
819 {
820 NaryExpr ne = (NaryExpr)e;
821 if (ne.exprs.size() != 1)
822 ErrorSet.error(ne.sloc,
823 "The function \\nonnullelements takes only one argument");
824 else {
825 Expr nu = checkExpr(env, ne.exprs.elementAt(0),
826 ArrayType.make(Types.javaLangObject(),
827 Location.NULL));
828 ne.exprs.setElementAt(nu, 0);
829 }
830 setType(e, Types.booleanType);
831 return e;
832 }
833
834 case TagConstants.DTTFSA:
835 {
836 NaryExpr ne = (NaryExpr)e;
837 Type resultType = Types.voidType;
838 if (ne.exprs.size() < 2) {
839 Assert.notFalse(1 <= ne.exprs.size());
840 ErrorSet.error(ne.sloc,
841 "The function \\dttfsa requires at least two arguments");
842 } else {
843 // type check each of the arguments
844 for (int i = 0; i < ne.exprs.size(); i++) {
845 Expr nu = checkExpr(env, ne.exprs.elementAt(i));
846 ne.exprs.setElementAt(nu, i);
847 }
848 // the first argument should be a TypeExpr; retrieve the type
849 // it denotes
850 resultType = ((TypeExpr)ne.exprs.elementAt(0)).type;
851 // the second argument should be a String literal
852 Expr arg1 = ne.exprs.elementAt(1);
853 if (arg1.getTag() != TagConstants.STRINGLIT) {
854 ErrorSet.error(arg1.getStartLoc(),
855 "The second argument to \\dttfsa must be a String literal");
856 } else {
857 LiteralExpr lit = (LiteralExpr)arg1;
858 String op = (String)lit.value;
859 if (op.equals("identity") && ne.exprs.size() != 3) {
860 ErrorSet.error(ne.sloc,
861 "The function \\dttfsa requires exactly 3 arguments when the second argument is \"identity\"");
862 }
863 }
864 }
865 setType(e, resultType);
866 return e;
867 }
868
869 case TagConstants.WACK_NOWARN:
870 case TagConstants.NOWARN_OP:
871 case TagConstants.WARN:
872 case TagConstants.WARN_OP:
873 {
874 NaryExpr ne = (NaryExpr)e;
875 Expr nu;
876 if( ne.exprs.size() != 1 ) {
877 ErrorSet.error(ne.sloc,
878 "The function " + TagConstants.toString(tag) +
879 " takes only one argument");
880 setType( e, Types.errorType );
881 } else {
882 // Get rid of this - FIXME - these are an obsolete definition
883 e = checkExpr(env, ne.exprs.elementAt(0));
884 //ne.exprs.setElementAt( nu, 0 );
885 //setType( e, getType(nu) );
886 }
887 return e;
888 }
889
890 case TagConstants.ELEMTYPE:
891 {
892 NaryExpr ne = (NaryExpr)e;
893 if( ne.exprs.size() != 1 )
894 ErrorSet.error(ne.sloc,
895 "The function \\elemtype takes only one argument");
896 else {
897 Expr nu = checkExpr(env, ne.exprs.elementAt(0));
898 ne.exprs.setElementAt( nu, 0 );
899 if (!Types.isTypeType(getType(nu)))
900 ErrorSet.error(nu.getStartLoc(),
901 "The argument must have TYPE type");
902 }
903 setType( e, Types.typecodeType );
904 return e;
905 }
906
907 case TagConstants.WACK_DURATION:
908 case TagConstants.WACK_WORKING_SPACE:
909 case TagConstants.SPACE:
910 {
911 NaryExpr ne = (NaryExpr)e;
912 if( ne.exprs.size() != 1 )
913 ErrorSet.error(ne.sloc,
914 "The function " + TagConstants.toString(tag) +
915 " takes only one argument");
916 else {
917 // Note: the arguments are not evaluated
918 Expr nu = checkExpr(env, ne.exprs.elementAt(0));
919 ne.exprs.setElementAt( nu, 0 );
920 }
921 setType( e, Types.longType );
922 return e;
923 }
924
925 case TagConstants.INVARIANT_FOR:
926 case TagConstants.IS_INITIALIZED:
927 {
928 NaryExpr ne = (NaryExpr)e;
929 // FIXME - Is this a one argument function ?
930 if( ne.exprs.size() != 1 )
931 ErrorSet.error( ne.sloc,
932 "The function takes only one argument");
933 else {
934 Expr nu = checkExpr(env, ne.exprs.elementAt(0));
935 ne.exprs.setElementAt( nu, 0 );
936 }
937 setType( e, Types.booleanType );
938 return e;
939 }
940
941 case TagConstants.NOTMODIFIEDEXPR:
942 {
943 NotModifiedExpr ne = (NotModifiedExpr)e;
944 ne.expr = checkExpr(env, ne.expr);
945 setType( e, Types.booleanType );
946 return e;
947 }
948
949 case TagConstants.MAX:
950 {
951 NaryExpr ne = (NaryExpr)e;
952 if( ne.exprs.size() != 1 )
953 ErrorSet.error( ne.sloc,
954 "The function \\max takes only one argument");
955 else {
956 Expr nu = checkExpr(env, ne.exprs.elementAt(0), Types.locksetType);
957 ne.exprs.setElementAt( nu, 0 );
958 }
959 setType( e, Types.javaLangObject() );
960 return e;
961 }
962
963 case TagConstants.PRE:
964 {
965 NaryExpr ne = (NaryExpr)e;
966 if( ne.exprs.size() != 1 ) {
967 ErrorSet.error( ne.sloc,
968 "The function \\old takes only one argument");
969 setType(e, Types.voidType);
970 } else if (!isTwoStateContext) {
971 ErrorSet.error(ne.sloc,
972 "The function \\old cannot be used in this context");
973 setType(e, Types.voidType);
974 } else if (isInsidePRE) {
975 ErrorSet.error(ne.sloc, "Nested applications of \\old not allowed");
976 setType(e, Types.voidType);
977 } else {
978 isInsidePRE = true;
979 Expr nu = checkExpr(env, ne.exprs.elementAt(0) );
980 Assert.notFalse(isInsidePRE);
981 isInsidePRE = false;
982 ne.exprs.setElementAt( nu, 0 );
983 setType( e, getType( nu ) );
984 }
985 return e;
986 }
987
988 case TagConstants.TYPEOF:
989 {
990 NaryExpr ne = (NaryExpr)e;
991 if( ne.exprs.size() != 1 )
992 ErrorSet.error( ne.sloc,
993 "The function \\typeof takes only one argument");
994 else {
995 Expr ex = ne.exprs.elementAt(0);
996 Expr nu = checkExpr(env, ex );
997 ne.exprs.setElementAt( nu, 0 );
998 Type t = getType(nu);
999 if (t instanceof PrimitiveType) {
1000 e = TypeExpr.make(ex.getStartLoc(),ex.getEndLoc(),t);
1001 }
1002 }
1003 setType( e, Types.typecodeType );
1004 return e;
1005 }
1006
1007 case TagConstants.TYPEEXPR:
1008 {
1009 TypeExpr te = (TypeExpr)e;
1010 env.resolveType( sig, te.type );
1011 setType(e, Types.typecodeType );
1012 return e;
1013 }
1014
1015 case TagConstants.LABELEXPR:
1016 {
1017 LabelExpr le = (LabelExpr)e;
1018 if (!isCurrentlyPredicateContext) {
1019 ErrorSet.error(le.getStartLoc(),
1020 "Labeled predicates are not allowed in this context");
1021 setType(e, Types.booleanType);
1022 } else {
1023 isPredicateContext = true;
1024 le.expr = checkExpr(env, le.expr);
1025 setType(e, getType( le.expr ) );
1026 }
1027 return e;
1028 }
1029
1030 case TagConstants.NUM_OF:
1031 {
1032 NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e;
1033
1034 // if (!isCurrentlyPredicateContext) {
1035 // ErrorSet.error(qe.getStartLoc(),
1036 // "Quantified expressions are not allowed in this context");
1037 // } else
1038 {
1039 Env subenv = env;
1040
1041 for( int i=0; i<qe.vars.size(); i++) {
1042 GenericVarDecl decl = qe.vars.elementAt(i);
1043 env.resolveType( sig, decl.type );
1044
1045 subenv = new EnvForLocals(subenv, decl);
1046 }
1047 isPredicateContext = true;
1048 qe.expr = checkExpr(subenv, qe.expr, Types.booleanType);
1049 }
1050 setType(e, Types.intType);
1051 return e;
1052 }
1053
1054 case TagConstants.SUM:
1055 case TagConstants.PRODUCT:
1056 case TagConstants.MIN:
1057 case TagConstants.MAXQUANT:
1058 {
1059 GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e;
1060
1061 /*
1062 if (!isCurrentlyPredicateContext) {
1063 ErrorSet.error(qe.getStartLoc(),
1064 "Quantified expressions are not allowed in this context");
1065 } else */
1066 {
1067 Env subenv = env;
1068
1069 for( int i=0; i<qe.vars.size(); i++) {
1070 GenericVarDecl decl = qe.vars.elementAt(i);
1071 env.resolveType( sig, decl.type );
1072
1073 subenv = new EnvForLocals(subenv, decl);
1074 }
1075 isPredicateContext = true;
1076 qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType);
1077 qe.expr = checkExpr(subenv, qe.expr, Types.intType);
1078 }
1079 setType(e, Types.intType);
1080 return e;
1081 }
1082
1083 case TagConstants.FORALL:
1084 case TagConstants.EXISTS:
1085 {
1086 QuantifiedExpr qe = (QuantifiedExpr)e;
1087
1088 if (!isCurrentlyPredicateContext) {
1089 ErrorSet.error(qe.getStartLoc(),
1090 "Quantified expressions are not allowed in this context");
1091 } else {
1092 Env subenv = env;
1093
1094 for( int i = 0; i < qe.vars.size(); i++) {
1095 GenericVarDecl decl = qe.vars.elementAt(i);
1096 env.resolveType(sig, decl.type);
1097
1098 subenv = new EnvForLocals(subenv, decl, false);
1099 }
1100 isPredicateContext = true;
1101 if (qe.rangeExpr != null) {
1102 qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType);
1103 }
1104 qe.expr = checkExpr(subenv, qe.expr, Types.booleanType);
1105 }
1106 if (qe.rangeExpr == null) { // skip
1107 } else if (tag == TagConstants.FORALL) {
1108 qe.expr = BinaryExpr.make(TagConstants.IMPLIES,
1109 qe.rangeExpr,qe.expr,Location.NULL);
1110 setType(qe.expr,Types.booleanType);
1111 } else {
1112 qe.expr = BinaryExpr.make(TagConstants.AND,
1113 qe.rangeExpr,qe.expr,Location.NULL);
1114 setType(qe.expr,Types.booleanType);
1115 }
1116 setType(e, Types.booleanType);
1117 return e;
1118 }
1119
1120 case TagConstants.PARENEXPR:
1121 case TagConstants.NOT:
1122 {
1123 // the sub-expression is allowed to contain quantifiers and
1124 // labels if this expression is
1125 isPredicateContext = isCurrentlyPredicateContext;
1126 return super.checkExpr(env, e);
1127 }
1128
1129 case TagConstants.ADD:
1130 {
1131 Expr ee = super.checkExpr(env, e);
1132 if (!Main.options().useOldStringHandling &&
1133 Types.isSameType(getType(ee),Types.javaLangString())) {
1134 boolean savedInAnnotation = inAnnotation;
1135 inAnnotation = true;
1136 BinaryExpr be = (BinaryExpr)ee;
1137 Expr left = be.left;
1138 Expr right = be.right;
1139 if (!Types.isSameType(getType(left),Types.javaLangString())) {
1140 Name nn = Name.make("java.lang.String.valueOf",left.getStartLoc());
1141 ExprVec a = ExprVec.make();
1142 a.addElement(left);
1143 AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make(
1144 nn,null,left.getStartLoc(),a);
1145 MethodInvocation mm = env.disambiguateMethodName(mi);
1146 left = checkExpr(env, mm);
1147 }
1148 if (!Types.isSameType(getType(right),Types.javaLangString())) {
1149 Name nn = Name.make("java.lang.String.valueOf",right.getStartLoc());
1150 ExprVec a = ExprVec.make();
1151 a.addElement(right);
1152 AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make(
1153 nn,null,right.getStartLoc(),a);
1154 MethodInvocation mm = env.disambiguateMethodName(mi);
1155 right = checkExpr(env, mm);
1156 }
1157 int loc = be.locOp;
1158 Name n = Name.make(TagConstants.STRINGCATINFIX,loc);
1159 ExprVec args = ExprVec.make();
1160 args.addElement(left);
1161 args.addElement(right);
1162 AmbiguousMethodInvocation ami = AmbiguousMethodInvocation.make(
1163 n,null,loc,args);
1164 MethodInvocation m = env.disambiguateMethodName(ami);
1165 ee = checkExpr(env, m);
1166 inAnnotation = savedInAnnotation;
1167 }
1168 return ee;
1169 }
1170
1171 case TagConstants.OR:
1172 case TagConstants.AND:
1173 case TagConstants.EQ:
1174 case TagConstants.NE:
1175 {
1176 BinaryExpr be = (BinaryExpr)e;
1177 // each argument is allowed to contain quantifiers and labels if
1178 // this expression is
1179 isPredicateContext = isCurrentlyPredicateContext;
1180 be.left = checkExpr(env, be.left);
1181 isPredicateContext = isCurrentlyPredicateContext;
1182 be.right = checkExpr(env, be.right);
1183 if (false && Types.isTypeType(getType(be.left)) &&
1184 // DO WE NEED TO check the composite expressions ??? FIXME TYPE-EQUIV
1185 Types.isTypeType(getType(be.right))) {
1186 setType( be, Types.booleanType);
1187 } else {
1188 Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
1189 setType( be, t );
1190 }
1191 return be;
1192 }
1193
1194 case TagConstants.WILDREFEXPR:
1195 {
1196 // FIXME - WildRefExpr needs cleanup . In current usage r.od is always null
1197 // on input.
1198 WildRefExpr r = (WildRefExpr)e;
1199 if (!isCurrentlySpecDesignatorContext) {
1200 setType(r, Types.errorType);
1201 ErrorSet.error(r.getStartLoc(),
1202 "Reference wild cards allowed only as "+
1203 "specification designators");
1204 } else {
1205 // Can't set the type, but need to check the type of the od
1206 if (r.od == null) {
1207 if (r.var instanceof AmbiguousVariableAccess) {
1208 AmbiguousVariableAccess a = (AmbiguousVariableAccess)r.var;
1209 Object o = env.disambiguateTypeOrFieldName(a.name);
1210 if (o instanceof TypeSig) {
1211 r.od = TypeObjectDesignator.make(r.var.getStartLoc(),
1212 (TypeSig)o );
1213 } else {
1214 r.var = checkExpr(env,r.var);
1215 // FIXME - really need locDot here
1216 r.od = ExprObjectDesignator.make(
1217 r.var.getEndLoc(),
1218 r.var);
1219 }
1220 r.var = null;
1221 } else {
1222 r.var = checkExpr(env,r.var);
1223 // FIXME - really need locDot here
1224 r.od = ExprObjectDesignator.make(
1225 r.var.getEndLoc(),
1226 r.var);
1227 }
1228 checkObjectDesignator(env,r.od);
1229 } else {
1230 Type t = checkObjectDesignator(env,r.od);
1231 // FIXME
1232 //System.out.println("TYPE " + t);
1233 }
1234 }
1235 return r;
1236 }
1237
1238 case TagConstants.ARRAYREFEXPR:
1239 {
1240 ArrayRefExpr r = (ArrayRefExpr)e;
1241
1242 r.array = checkExpr(env, r.array);
1243 Type arrType = getType( r.array );
1244 r.index = checkExpr(env, r.index);
1245 Type t = getType( r.index );
1246
1247 if( arrType instanceof ArrayType ) {
1248 setType( r, ((ArrayType)arrType).elemType );
1249 Type ndxType =
1250 Types.isNumericType( t ) ? Types.unaryPromote( t ) : t;
1251 if( !Types.isSameType( ndxType, Types.intType ) &&
1252 !Types.isErrorType(ndxType) )
1253 ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
1254
1255 } else if( arrType.getTag() == TagConstants.LOCKSET ) {
1256 setType( r, Types.booleanType );
1257 if( !Types.isReferenceOrNullType( t ) &&
1258 !Types.isErrorType(t) )
1259 ErrorSet.error(r.locOpenBracket,
1260 "Can only index \\lockset with a reference type");
1261 } else {
1262 setType( r, Types.errorType );
1263 if (!Types.isErrorType(arrType) )
1264 ErrorSet.error( r.locOpenBracket,
1265 "Attempt to index a non-array value");
1266 }
1267 //alx: dw set universe modifier for ArrayRefExpr
1268 if (useUniverses)
1269 determineUniverseForArrayRefExpr(r);
1270 //alx-end
1271 return r;
1272 }
1273
1274 case TagConstants.ARRAYRANGEREFEXPR:
1275 {
1276 ArrayRangeRefExpr r = (ArrayRangeRefExpr)e;
1277 if (!isCurrentlySpecDesignatorContext) {
1278 setType(r, Types.errorType);
1279 ErrorSet.error(r.getStartLoc(),
1280 "Array ranges are allowed only as "+
1281 "specification designators");
1282 } else {
1283
1284 r.array = checkExpr(env, r.array);
1285 Type arrType = getType( r.array );
1286 if (r.lowIndex != null) r.lowIndex = checkExpr(env, r.lowIndex);
1287 if (r.highIndex != null) r.highIndex = checkExpr(env, r.highIndex);
1288 Type t = r.lowIndex == null ? null : getType( r.lowIndex );
1289 Type tt = r.highIndex == null ? null : getType( r.highIndex );
1290
1291 if( arrType instanceof ArrayType ) {
1292 setType( r, ((ArrayType)arrType).elemType );
1293 if (t != null) {
1294 Type ndxType =
1295 Types.isNumericType( t ) ? Types.unaryPromote( t ) : t;
1296 if( !Types.isSameType( ndxType, Types.intType ) &&
1297 !Types.isErrorType(ndxType) )
1298 ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
1299 }
1300 if (tt != null) {
1301 Type ndxType =
1302 Types.isNumericType( tt ) ? Types.unaryPromote( tt ) : tt;
1303 if( !Types.isSameType( ndxType, Types.intType ) &&
1304 !Types.isErrorType(ndxType) )
1305 ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
1306 }
1307
1308 } else {
1309 setType( r, Types.errorType );
1310 if (!Types.isErrorType(arrType) )
1311 ErrorSet.error( r.locOpenBracket,
1312 "Attempt to index a non-array value");
1313 }
1314 }
1315
1316 return r;
1317 }
1318 case TagConstants.RESEXPR:
1319 {
1320 if (!isRESContext || returnType == null) {
1321 if (!Types.isErrorType(returnType))
1322 ErrorSet.error(e.getStartLoc(),
1323 "Keyword \\result is not allowed in this context");
1324 setType( e, Types.errorType );
1325 }
1326 else
1327 setType( e, returnType );
1328
1329 return e;
1330 }
1331
1332 case TagConstants.SETCOMPEXPR:
1333 {
1334 SetCompExpr s = (SetCompExpr)e;
1335
1336 env.resolveType(sig, s.type);
1337 env.resolveType(sig, s.fp.type);
1338 Env subenv = new EnvForLocals(env,s.fp,false);
1339 boolean savedPredicateContext = isPredicateContext;
1340 isPredicateContext = true;
1341 s.expr = checkExpr(subenv, s.expr, Types.booleanType);
1342 isPredicateContext = savedPredicateContext;
1343 setType( e, s.type);
1344 // FIXME - CHeck that the type is only JMLObjectSet, JMLValueSet
1345 // Check that the predicate has the correct restricted form
1346 return e;
1347 }
1348
1349 case TagConstants.NOTSPECIFIEDEXPR:
1350 {
1351 setType( e, Types.voidType);
1352 return e;
1353 }
1354 case TagConstants.EVERYTHINGEXPR:
1355 {
1356 if (!isCurrentlySpecDesignatorContext) {
1357 ErrorSet.error(e.getStartLoc(),
1358 "Keyword \\everything is not allowed in this context");
1359 setType( e, Types.errorType);
1360 } else {
1361 setType( e, Types.voidType);
1362 }
1363 return e;
1364 }
1365 case TagConstants.NOTHINGEXPR:
1366 {
1367 if (!isCurrentlySpecDesignatorContext) {
1368 ErrorSet.error(e.getStartLoc(),
1369 "Keyword \\nothing is not allowed in this context");
1370 setType( e, Types.errorType);
1371 } else {
1372 setType( e, Types.voidType);
1373 }
1374 return e;
1375 }
1376 case TagConstants.LOCKSETEXPR:
1377 {
1378 if (! isLocksetContext) {
1379 ErrorSet.error(e.getStartLoc(),
1380 "Keyword \\lockset is not allowed in this context");
1381 }
1382 setType( e, Types.locksetType );
1383 return e;
1384 }
1385
1386 case TagConstants.LE:
1387 case TagConstants.LT:
1388 {
1389 BinaryExpr be = (BinaryExpr)e;
1390 be.left = checkExpr(env, be.left);
1391 be.right = checkExpr(env, be.right);
1392
1393 if( Types.isReferenceOrNullType( getType( be.left ) )
1394 && Types.isReferenceOrNullType( getType( be.right ) ) ) {
1395 // is lock comparison, and is ok
1396 setType( be, Types.booleanType );
1397 return be;
1398 } else {
1399 return super.checkExpr(env, e);
1400 }
1401 }
1402
1403 case TagConstants.NEWINSTANCEEXPR:
1404 case TagConstants.NEWARRAYEXPR:
1405 {
1406 countFreeVarsAccesses++;
1407 /* FIXME - Yes it can, but it must be pure!
1408 if (inAnnotation) {
1409 ErrorSet.error(e.getStartLoc(),
1410 "new cannot be used in specification expressions");
1411 }
1412 */
1413 return super.checkExpr(env, e);
1414 }
1415
1416 case TagConstants.ASSIGN: case TagConstants.ASGMUL:
1417 case TagConstants.ASGDIV: case TagConstants.ASGREM:
1418 case TagConstants.ASGADD: case TagConstants.ASGSUB:
1419 case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
1420 case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
1421 case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR:
1422 {
1423 if (inAnnotation && !inModelBody) {
1424 BinaryExpr be = (BinaryExpr)e;
1425 ErrorSet.error(be.locOp,
1426 "assignments cannot be used in specification expressions");
1427 }
1428 return super.checkExpr(env, e);
1429 }
1430
1431 case TagConstants.INC: case TagConstants.DEC:
1432 case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
1433 {
1434 if (inAnnotation && !inModelBody) {
1435 UnaryExpr ue = (UnaryExpr)e;
1436 ErrorSet.error(ue.locOp,
1437 "assignments cannot be used in specification expressions");
1438 }
1439 return super.checkExpr(env, e);
1440 }
1441
1442 default:
1443 return super.checkExpr(env, e);
1444 }
1445
1446 } finally {
1447
1448 isPredicateContext = isCurrentlyPredicateContext;
1449 }
1450 }
1451
1452 // Pragma checkers
1453
1454 protected void checkTypeDeclElemPragma(TypeDeclElemPragma e) {
1455 int tag = e.getTag();
1456 boolean savedInAnnotation = inAnnotation;
1457 inAnnotation = true; // Must be reset before we exit!
1458 try {
1459
1460 switch(tag) {
1461 case TagConstants.AXIOM:
1462 case TagConstants.INITIALLY:
1463 case TagConstants.INVARIANT:
1464 case TagConstants.CONSTRAINT: // FIXME - do we need to change the logic below to handle constraints?
1465 {
1466 ExprDeclPragma ep = (ExprDeclPragma)e;
1467 Env rootEnv = (tag == TagConstants.AXIOM ||
1468 Modifiers.isStatic(ep.modifiers)) ? rootSEnv : rootIEnv;
1469
1470 invariantContext = (tag == TagConstants.INVARIANT) ||
1471 tag == TagConstants.INITIALLY;
1472 isTwoStateContext = (tag == TagConstants.CONSTRAINT);
1473 boolean oldIsLocksetContext = isLocksetContext;
1474 isLocksetContext = false;
1475 if (invariantContext){
1476 // FIXME Assert.notFalse(countFreeVarsAccesses == 0);
1477 countFreeVarsAccesses = 0;
1478 }
1479
1480 ep.expr = checkPredicate(rootEnv, ep.expr);
1481 isLocksetContext = oldIsLocksetContext;
1482
1483 TypeSig sig = TypeSig.getSig(e.getParent());
1484 if (sig==javafe.tc.Types.javaLangObject() ||
1485 sig==javafe.tc.Types.javaLangCloneable()) {
1486 if (invariantContext) ErrorSet.fatal(e.getStartLoc(),
1487 "java.lang.Object and java.lang.Cloneable may not"
1488 + " contain invariants."); // FIXME - Why?
1489 }
1490 /*
1491 FIXME - see uses of countFreeVarsAccess
1492 if (invariantContext && countFreeVarsAccesses == 0 &&
1493 // Don't print an error if the entire invariant
1494 // is an informal predicate
1495 escjava.parser.EscPragmaParser.
1496 informalPredicateDecoration.get(ep.expr)==null) {
1497 ErrorSet.error(e.getStartLoc(),
1498 "Class invariants must mention program variables"
1499 + " or fields.");
1500 }
1501 */
1502
1503 if (invariantContext) {countFreeVarsAccesses = 0;}
1504 invariantContext = false;
1505 isTwoStateContext = false;
1506 break;
1507 }
1508 case TagConstants.REPRESENTS:
1509 {
1510 NamedExprDeclPragma ep = (NamedExprDeclPragma)e;
1511 boolean stat = Modifiers.isStatic(ep.modifiers);
1512
1513 // What about static model vars?
1514 // Can the represents clause be static ? FIXME
1515 Env rootEnv = stat? rootSEnv : rootIEnv;
1516 ep.target = checkExpr(rootEnv, ep.target);
1517
1518 if (ep.target instanceof FieldAccess) {
1519 invariantContext = false;
1520 isTwoStateContext = false;
1521 boolean oldIsLocksetContext = isLocksetContext;
1522 isLocksetContext = false;
1523 if (invariantContext){
1524 // FIXME Assert.notFalse(countFreeVarsAccesses == 0);
1525 countFreeVarsAccesses = 0;
1526 }
1527
1528 ep.expr = checkPredicate(rootEnv, ep.expr);
1529 isLocksetContext = oldIsLocksetContext;
1530
1531 FieldAccess fa = (FieldAccess)ep.target;
1532 if (!Utils.isModel(fa.decl)) {
1533 ErrorSet.error(fa.getStartLoc(),
1534 "A represents clause must name a model field",
1535 fa.decl.locId);
1536 }
1537 if (stat && !Modifiers.isStatic(fa.decl.modifiers)) {
1538 ErrorSet.error(fa.getStartLoc(),
1539 "A static represents clause must name a static model field");
1540 }
1541 if (!stat && Modifiers.isStatic(fa.decl.modifiers)) {
1542 ErrorSet.error(fa.getStartLoc(),
1543 "A non-static represents clause must name a non-static model field");
1544 }
1545
1546 /* THis is done in type prepping
1547 TypeDecl td = ep.parent;
1548 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(td);
1549 if (tv == null) {
1550 tv = TypeDeclElemVec.make(10);
1551 Utils.representsDecoration.set(td,tv);
1552 }
1553 tv.addElement(ep);
1554 */
1555 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(fa.decl);
1556 if (tv == null) {
1557 tv = TypeDeclElemVec.make(10);
1558 Utils.representsDecoration.set(fa.decl,tv);
1559 }
1560 tv.addElement(ep);
1561 } else if (!(ep.target instanceof AmbiguousVariableAccess)){
1562 // If the type is Ambiguous, then an Undefined variable
1563 // error has already been issued. I'm not actually
1564 // sure that this point is reachable.
1565 ErrorSet.error(ep.target.getStartLoc(),
1566 "Expected a field identifier here");
1567 }
1568 break;
1569 }
1570 case TagConstants.DEPENDS:
1571 {
1572 DependsPragma ep = (DependsPragma)e;
1573 // FIXME - perhaps use rootSEnv if the variable
1574 // being discussed is static ?
1575 Env rootEnv = rootIEnv;
1576
1577 ep.target = checkExpr(rootEnv, ep.target);
1578
1579 ExprVec ev = ep.exprs;
1580 for (int i=0; i<ev.size(); ++i) {
1581 ev.setElementAt(
1582 checkExpr(rootEnv, ev.elementAt(i)), i);
1583 }
1584
1585 // FIXME - Need to check that
1586 // LHS is a simple model variable, a field of
1587 // this or a super class or an interface
1588 // RHS consists of store-refs, no computed expressions
1589 // RHS may have other model variables
1590 // check access ?
1591 break;
1592 }
1593
1594 case TagConstants.MODELCONSTRUCTORDECLPRAGMA: {
1595 ModelConstructorDeclPragma me = (ModelConstructorDeclPragma)e;
1596 ConstructorDecl cd = me.decl;
1597 Env rootEnv = Modifiers.isStatic(cd.modifiers)
1598 ? rootSEnv
1599 : rootIEnv;
1600
1601 // All gets checked since the associated ConstructorDecl is
1602 // part of the type
1603
1604 // FIXME - the body needs to allow ghost/model vars
1605 break;
1606 }
1607
1608
1609 case TagConstants.MODELMETHODDECLPRAGMA: {
1610 MethodDecl decl = ((ModelMethodDeclPragma)e).decl;
1611 Env rootEnv = Modifiers.isStatic(decl.modifiers)
1612 ? rootSEnv
1613 : rootIEnv;
1614
1615 // All gets checked since the associated ConstructorDecl is
1616 // part of the type
1617
1618 // FIXME - the body needs to allow ghost/model vars
1619 break;
1620 }
1621
1622 case TagConstants.MONITORS_FOR: {
1623 IdExprDeclPragma emp = (IdExprDeclPragma)e;
1624 Identifier id = emp.id;
1625 TypeDeclElemVec elems = e.parent.elems;
1626 FieldDecl fd = null;
1627 for (int i=0; i<elems.size(); ++i) {
1628 TypeDeclElem td = elems.elementAt(i);
1629 if (td instanceof FieldDecl &&
1630 ((FieldDecl)td).id == id) {
1631 fd = (FieldDecl)td;
1632 break;
1633 }
1634 }
1635 boolean isStatic = false;
1636 if (fd == null) {
1637 ErrorSet.error(emp.loc,
1638 "Could not find identifier " + id + " in this class");
1639 } else {
1640 isStatic = Modifiers.isStatic(fd.modifiers);
1641 }
1642 if (Modifiers.isStatic(emp.modifiers)) isStatic = true;
1643 Env env = isStatic ? rootSEnv : rootIEnv;
1644 int oldAccessibilityLowerBound = accessibilityLowerBound;
1645 ASTNode oldAccessibilityContext = accessibilityContext;
1646 accessibilityLowerBound = getAccessibility(fd.modifiers);
1647 accessibilityContext = fd;
1648 emp.expr = checkExpr(env, emp.expr, Types.javaLangObject());
1649 accessibilityLowerBound = oldAccessibilityLowerBound;
1650 accessibilityContext = oldAccessibilityContext;
1651 fd.pmodifiers.addElement(
1652 ExprModifierPragma.make(
1653 TagConstants.MONITORED_BY,
1654 emp.expr,
1655 emp.loc
1656 ));
1657 break;
1658 }
1659
1660 case TagConstants.WRITABLE:
1661 case TagConstants.READABLE: {
1662 NamedExprDeclPragma emp = (NamedExprDeclPragma)e;
1663
1664 isSpecDesignatorContext = true;
1665 Env newenv = rootIEnv;
1666 emp.target = checkDesignator(newenv, emp.target);
1667 isSpecDesignatorContext = false;
1668 emp.expr = checkPredicate(newenv, emp.expr);
1669 switch (emp.target.getTag()) {
1670 case TagConstants.FIELDACCESS: {
1671 FieldAccess fa = (FieldAccess)emp.target;
1672 if (fa.decl != null &&
1673 // The array "length" field has already been checked
1674 // insuper.checkDesignator().
1675 fa.decl != Types.lengthFieldDecl) {
1676
1677 if (tag == TagConstants.WRITABLE &&
1678 Modifiers.isFinal(fa.decl.modifiers)) {
1679 // FIXME
1680 }
1681 fa.decl.pmodifiers.addElement(
1682 ExprModifierPragma.make(
1683 emp.tag == TagConstants.READABLE ?
1684 TagConstants.READABLE_IF:
1685 TagConstants.WRITABLE_IF,
1686 emp.expr,
1687 emp.loc
1688 )
1689 );
1690 }
1691 break;
1692 }
1693
1694 case TagConstants.ARRAYREFEXPR:
1695 case TagConstants.ARRAYRANGEREFEXPR:
1696 case TagConstants.WILDREFEXPR:
1697 case TagConstants.EVERYTHINGEXPR:
1698 case TagConstants.NOTHINGEXPR:
1699 case TagConstants.NOTSPECIFIEDEXPR:
1700 // FIXME - not implemented
1701 break;
1702
1703 default:
1704 if (escjava.parser.EscPragmaParser.
1705 informalPredicateDecoration.get(emp.target)==null) {
1706 // The expression is not a designator
1707 // but we allow an informal predicate
1708 if (!Types.isErrorType(getType(emp.target)))
1709 ErrorSet.error(emp.target.getStartLoc(),
1710 "Not a specification designator expression");
1711 } else {
1712 emp.target = null;
1713 }
1714 }
1715 break;
1716 }
1717
1718 case TagConstants.MODELDECLPRAGMA: {
1719 FieldDecl decl = ((ModelDeclPragma)e).decl;
1720 Env rootEnv = Modifiers.isStatic(decl.modifiers)
1721 ? rootSEnv
1722 : rootIEnv;
1723
1724 rootEnv.resolveType( sig, decl.type );
1725 checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv );
1726 checkTypeModifiers(rootEnv, decl.type);
1727
1728 // Check for both static and instance declarations
1729
1730 if (Modifiers.isStatic(decl.modifiers)) {
1731 ModifierPragma inst = Utils.findModifierPragma(decl,
1732 TagConstants.INSTANCE);
1733 if (inst != null) ErrorSet.error(inst.getStartLoc(),
1734 "May not specify both static and instance on a declaration");
1735 }
1736
1737 /*
1738 * Check for other fields with the same name:
1739 */
1740 {
1741 TypeDeclElemVec elems = decl.parent.elems;
1742 FieldDecl fd;
1743 for (int i = 0; i<elems.size(); ++i) {
1744 TypeDeclElem tde = elems.elementAt(i);
1745 if (tde instanceof FieldDecl) {
1746 fd = (FieldDecl)tde;
1747 } else if (tde instanceof GhostDeclPragma) {
1748 fd = ((GhostDeclPragma)tde).decl;
1749 } else if (tde instanceof ModelDeclPragma) {
1750 fd = ((ModelDeclPragma)tde).decl;
1751 } else
1752 continue;
1753 if (fd.id == decl.id && fd != decl)
1754 ErrorSet.error(decl.locId,
1755 "Another field named '"+decl.id.toString()
1756 +"' already exists in this type", fd.locId);
1757 }
1758 }
1759
1760 break;
1761 }
1762
1763 case TagConstants.GHOSTDECLPRAGMA: {
1764 FieldDecl decl = ((GhostDeclPragma)e).decl;
1765 ModifierPragma inst = Utils.findModifierPragma(decl,
1766 TagConstants.INSTANCE);
1767 // Check for both static and instance declarations
1768
1769 if (Modifiers.isStatic(decl.modifiers)) {
1770 if (inst != null) ErrorSet.error(inst.getStartLoc(),
1771 "May not specify both static and instance on a declaration");
1772 }
1773
1774 Env rootEnv = Modifiers.isStatic(decl.modifiers)
1775 ? rootSEnv
1776 : rootIEnv;
1777
1778 rootEnv.resolveType( sig, decl.type );
1779 checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv );
1780 checkTypeModifiers(rootEnv, decl.type);
1781
1782
1783
1784 /*
1785 * Handle initializer:
1786 */
1787
1788 if (decl.init != null) {
1789 leftToRight = true;
1790 allowedExceptions.removeAllElements();
1791 Assert.notFalse( allowedExceptions.size() == 0);
1792 decl.init = checkInit(rootEnv, decl.init, decl.type);
1793 }
1794
1795 /*
1796 * Check for other fields with the same name:
1797 */
1798 {
1799 TypeDeclElemVec elems = decl.parent.elems;
1800 FieldDecl fd;
1801 for (int i = 0; i<elems.size(); ++i) {
1802 TypeDeclElem tde = elems.elementAt(i);
1803 if (tde instanceof FieldDecl) {
1804 fd = (FieldDecl)tde;
1805 } else if (tde instanceof GhostDeclPragma) {
1806 fd = ((GhostDeclPragma)tde).decl;
1807 } else if (tde instanceof ModelDeclPragma) {
1808 fd = ((ModelDeclPragma)tde).decl;
1809 } else
1810 continue;
1811 if (fd.id == decl.id && fd != decl)
1812 ErrorSet.error(decl.locId,
1813 "Another field named '"+decl.id.toString()
1814 +"' already exists in this type", fd.locId);
1815 }
1816 }
1817
1818
1819 break;
1820 }
1821
1822 case TagConstants.STILLDEFERREDDECLPRAGMA: {
1823 StillDeferredDeclPragma sddp = (StillDeferredDeclPragma)e;
1824 if (!sig.hasField(sddp.var)) {
1825 ErrorSet.error(sddp.locId, "No such field");
1826 }
1827
1828 // TBW: To support still_deferred, one also needs to check that
1829 // "sddp.var" is declared as writable-deferred in the direct
1830 // superclass.
1831 break;
1832 }
1833
1834 default:
1835 Assert.fail("Unexpected tag " + tag +
1836 " " + TagConstants.toString(tag));
1837 }
1838 } finally {
1839 inAnnotation = savedInAnnotation;
1840 }
1841 }
1842
1843 protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) {
1844
1845 boolean savedInAnnotation = inAnnotation;
1846 inAnnotation = true; // Must be reset before we exit!
1847 try {
1848 int tag = p.getTag();
1849 switch(tag)
1850 {
1851 case TagConstants.EVERYTHINGEXPR:
1852 case TagConstants.EVERYTHING:
1853 case TagConstants.NOTHING:
1854 case TagConstants.NOT_SPECIFIED:
1855 case TagConstants.NOTHINGEXPR:
1856 case TagConstants.NOTSPECIFIEDEXPR:
1857 // FIXME - check the context???
1858 break;
1859
1860 case TagConstants.UNINITIALIZED:
1861 if( ctxt.getTag() != TagConstants.LOCALVARDECL ) {
1862 int loc;
1863 if (ctxt instanceof GenericVarDecl)
1864 loc = ((GenericVarDecl)ctxt).locId;
1865 else
1866 loc = p.getStartLoc();
1867 ErrorSet.error(loc,
1868 "The uninitialized annotation can occur only on "
1869 +"local variable declarations");
1870 } else if( ((LocalVarDecl)ctxt).init == null ) {
1871 ErrorSet.error(((GenericVarDecl)ctxt).locId,
1872 "The uninitialized annotation can occur only on "
1873 +"local variable declarations "
1874 +"that have an initializer");
1875 }
1876 break;
1877
1878 case TagConstants.MONITORED:
1879 {
1880 if( ctxt.getTag() != TagConstants.FIELDDECL ) {
1881 int loc;
1882 if (ctxt instanceof GenericVarDecl)
1883 loc = ((GenericVarDecl)ctxt).locId;
1884 else
1885 loc = p.getStartLoc();
1886 ErrorSet.error(loc,
1887 "The monitored annotation can occur only on "
1888 +"field declarations");
1889 /* added functionality to have monitors on static fields
1890 } else if (env.isStaticContext()) {
1891 FieldDecl fd = (FieldDecl)ctxt;
1892 ErrorSet.error(fd.locId,
1893 "The monitored annotation can occur only on "+
1894 "instance field declarations");
1895 */
1896 }
1897 break;
1898 }
1899
1900 case TagConstants.NULLABLE:
1901 case TagConstants.NON_NULL:
1902 // NOTE: Part of the NON_NULL check is found in checkTypeDeclElem()
1903 // above, since there's not enough context information here to
1904 // determine whether a formal parameter is declared for a method
1905 // override.
1906 switch (ctxt.getTag()) {
1907 case TagConstants.FORMALPARADECL:
1908 case TagConstants.LOCALVARDECL:
1909 case TagConstants.FIELDDECL: {
1910 GenericVarDecl vd = (GenericVarDecl)ctxt;
1911 if (! Types.isReferenceType(vd.type)) {
1912 ErrorSet.error(vd.locId,
1913 "The " + TagConstants.toString(tag) +
1914 " pragma can be applied only to "+
1915 "variables, fields, and parameters of "+
1916 "reference types");
1917 }
1918 break;
1919 }
1920 case TagConstants.METHODDECL: {
1921 MethodDecl md = (MethodDecl) ctxt;
1922 if (!Types.isReferenceType(md.returnType)) {
1923 ErrorSet.error(md.getStartLoc(),
1924 "'" + TagConstants.toString(tag) +
1925 "' can only be used with methods whose "+
1926 "result type is a reference type");
1927 }
1928 break;
1929 }
1930 default:
1931 ErrorSet.error(p.getStartLoc(),
1932 "The " + TagConstants.toString(tag) + " pragma can be applied only to "+
1933 "variables, fields, parameters, and methods");
1934 break;
1935 }
1936 break;
1937
1938 // FIXME - should have a spec_protected case as well ???
1939 case TagConstants.SPEC_PUBLIC:
1940 case TagConstants.SPEC_PROTECTED:
1941 // JML now allows spec_public and spec_protected on declarations
1942 // of any java accessibiilty
1943 break;
1944
1945 case TagConstants.WRITABLE_DEFERRED:
1946 {
1947 if (ctxt.getTag() != TagConstants.FIELDDECL ||
1948 Modifiers.isStatic(((FieldDecl)ctxt).modifiers)) {
1949 ErrorSet.error(p.getStartLoc(),
1950 "The writable_deferred annotation can occur only on "
1951 +"instance field declarations");
1952 }
1953 break;
1954 }
1955
1956 case TagConstants.INSTANCE:
1957 {
1958 int ctag = ctxt.getTag();
1959
1960 if (!(ctxt instanceof GhostDeclPragma) &&
1961 !(ctxt instanceof ModelDeclPragma)) {
1962
1963 // FIXME - should this use Utils.isModel ???
1964 if (ctxt instanceof FieldDecl &&
1965 (Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.MODEL) != null ||
1966 Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.GHOST) != null )) {
1967 // skip
1968 } else {
1969 ErrorSet.error(p.getStartLoc(),
1970 "An instance modifier may only be applied to ghost and model fields");
1971 }
1972 }
1973
1974 break;
1975 }
1976
1977 case TagConstants.FUNCTION:
1978 // FIXME - do some checking
1979 // must be pure, static, immutable arguments, not void
1980 break;
1981
1982 case TagConstants.PURE:
1983 {
1984 if (ctxt instanceof RoutineDecl) {
1985 } else if (ctxt instanceof TypeDecl) {
1986 } else {
1987 ErrorSet.error(p.getStartLoc(),
1988 "Expected pure to modify a class, interface, constructor or method declaration");
1989 }
1990 break;
1991 }
1992
1993 case TagConstants.HELPER:
1994 switch (ctxt.getTag()) {
1995 case TagConstants.CONSTRUCTORDECL:
1996 ((ConstructorDecl)ctxt).modifiers |= Modifiers.ACC_HELPER;
1997 break;
1998 case TagConstants.METHODDECL:
1999 {
2000 MethodDecl md = (MethodDecl) ctxt;
2001 md.modifiers |= Modifiers.ACC_HELPER;
2002 if (getOverrideStatus(md) != MSTATUS_NEW_ROUTINE) {
2003 ErrorSet.error(p.getStartLoc(),
2004 "The helper pragma cannot be " +
2005 "applied to a method override");
2006 } else if (isOverridable(md)) {
2007 ErrorSet.error(p.getStartLoc(),
2008 "The helper pragma cannot be applied " +
2009 "to method that can be overridden");
2010 } else if (md.body == null) {
2011 ErrorSet.error(p.getStartLoc(),
2012 "The helper pragma cannot be applied " +
2013 "to method without a body");
2014 }
2015 break;
2016 }
2017 default:
2018 ErrorSet.error(p.getStartLoc(),
2019 "The helper pragma can only be applied to "+
2020 "methods and constructors");
2021 break;
2022 }
2023 break;
2024
2025 case TagConstants.IMMUTABLE:
2026 {
2027 if (!(ctxt instanceof TypeDecl)) {
2028 ErrorSet.error(p.getStartLoc(),
2029 "The immutable modifier may be applied only to type declarations");
2030 }
2031 }
2032 break;
2033
2034 case TagConstants.WRITABLE_IF:
2035 case TagConstants.READABLE_IF:
2036 {
2037 ExprModifierPragma emp = (ExprModifierPragma)p;
2038
2039 if( ctxt.getTag() != TagConstants.FIELDDECL
2040 && ctxt.getTag() != TagConstants.LOCALVARDECL ) {
2041 ErrorSet.error(p.getStartLoc(),
2042 "The " + TagConstants.toString(tag)
2043 +" annotation can occur only on "
2044 +"field declarations and "
2045 +"local variable declarations");
2046 }
2047
2048 int oldAccessibilityLowerBound = accessibilityLowerBound;
2049 ASTNode oldAccessibilityContext = accessibilityContext;
2050 if (ctxt.getTag() == TagConstants.FIELDDECL) {
2051 FieldDecl fd = (FieldDecl)ctxt;
2052 accessibilityLowerBound = getAccessibility(fd.modifiers);
2053 accessibilityContext = fd;
2054 }
2055 emp.expr = checkPredicate(env, emp.expr);
2056 accessibilityLowerBound = oldAccessibilityLowerBound;
2057 accessibilityContext = oldAccessibilityContext;
2058 break;
2059 }
2060
2061 case TagConstants.NO_WACK_FORALL:
2062 case TagConstants.OLD:
2063 {
2064 VarDeclModifierPragma vd = (VarDeclModifierPragma)p;
2065 LocalVarDecl x = vd.decl;
2066 env.resolveType( sig, vd.decl.type );
2067 checkTypeModifiers(env, x.type);
2068 javafe.tc.PrepTypeDeclaration.getInst().
2069 checkModifiers(x.modifiers, Modifiers.NONE,
2070 x.locId, "local specification variable");
2071
2072 boolean savedContext = isTwoStateContext;
2073 isTwoStateContext = true;
2074 // The case of x.init==null is illegal and should have
2075 // been caught by the parser.
2076 if (x.init != null) {
2077 //if (x.init instanceof ArrayInit) {
2078 x.init = checkInit(env, x.init, x.type);
2079 //} else {
2080 //checkExpr(newEnv, (Expr)x.init, x.type);
2081 //}
2082 }
2083 isTwoStateContext = savedContext;
2084 // We create the new environment after checking the
2085 // initializer to be sure that the initializer does not
2086 // reference itself.
2087 env = new EnvForGhostLocals(env,x);
2088 break;
2089 }
2090
2091 case TagConstants.ALSO_REQUIRES:
2092 case TagConstants.REQUIRES:
2093 case TagConstants.PRECONDITION:
2094 {
2095 ExprModifierPragma emp = (ExprModifierPragma)p;
2096
2097 if( ctxt instanceof InitBlock ) {
2098 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2099 emp.expr = checkPredicate(env, emp.expr);
2100 } else if( ctxt instanceof RoutineDecl ) {
2101 RoutineDecl rd = (RoutineDecl)ctxt;
2102
2103 int ms = getOverrideStatus(rd);
2104
2105 Env newenv = env;
2106 /* Interpret constructor as acting on an existing object, to initialize it,
2107 so this and fields are in scope.
2108 if (rd instanceof ConstructorDecl) {
2109 newenv = env.asStaticContext();
2110 }
2111 */
2112 int oldAccessibilityLowerBound = accessibilityLowerBound;
2113 ASTNode oldAccessibilityContext = accessibilityContext;
2114 accessibilityLowerBound = getAccessibility(rd.modifiers);
2115 accessibilityContext = rd;
2116 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2117 emp.expr = checkPredicate(newenv, emp.expr);
2118 accessibilityLowerBound = oldAccessibilityLowerBound;
2119 accessibilityContext = oldAccessibilityContext;
2120 } else {
2121 ErrorSet.error(p.getStartLoc(), TagConstants.toString(tag) +
2122 " annotations can occur only on method" +
2123 ((tag == TagConstants.REQUIRES ||
2124 tag == TagConstants.PRECONDITION) ? " and constructor" : "") +
2125 " declarations");
2126 }
2127 break;
2128 }
2129
2130 case TagConstants.MEASURED_BY:
2131 case TagConstants.DURATION:
2132 case TagConstants.WORKING_SPACE:
2133 {
2134 CondExprModifierPragma emp = (CondExprModifierPragma)p;
2135
2136 if( !(ctxt instanceof RoutineDecl ) ) {
2137 ErrorSet.error(p.getStartLoc(),
2138 TagConstants.toString(tag)
2139 +" annotations can occur only on "
2140 +"method and constructor declarations");
2141 } else {
2142 RoutineDecl rd = (RoutineDecl)ctxt;
2143 boolean oldIsRESContext = isRESContext;
2144 boolean oldIsTwoStateContext = isTwoStateContext;
2145 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
2146 isRESContext = true;
2147 isTwoStateContext = true;
2148 // If "rd" is an overridable method, then every private field
2149 // mentioned in "emp.expr" must be spec_public.
2150 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
2151 isPrivateFieldAccessAllowed = false;
2152 }
2153 try {
2154 if (tag == TagConstants.MEASURED_BY) {
2155 // FIXME - what type to use?
2156 emp.expr = checkExpr(env, emp.expr);
2157 } else if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2158 emp.expr = checkExpr(env, emp.expr, Types.longType);
2159 if (emp.cond != null)
2160 emp.cond = checkExpr(env, emp.cond, Types.booleanType);
2161 } finally {
2162 isRESContext = oldIsRESContext;
2163 isTwoStateContext = oldIsTwoStateContext;
2164 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
2165 }
2166 }
2167 break;
2168 }
2169
2170 case TagConstants.DIVERGES:
2171 if (ctxt instanceof RoutineDecl) {
2172 RoutineDecl rd = (RoutineDecl)ctxt;
2173 if (Utils.isPure(rd)) {
2174 ExprModifierPragma emp = (ExprModifierPragma)p;
2175 if (emp.expr instanceof LiteralExpr &&
2176 ((LiteralExpr)emp.expr).value == Boolean.FALSE) {
2177 // OK
2178 } else if (p.getStartLoc() == Location.NULL) {
2179 // Default clause - ignore it and deal with it during desugaring
2180 } else {
2181 int locp = Utils.findPurePragma(rd).getStartLoc();
2182 int loc = p.getStartLoc();
2183 if (loc == Location.NULL) {
2184 ErrorSet.error(locp,
2185 "A lightweight specification case for a pure method must have a 'diverges false' clause");
2186 } else {
2187 ErrorSet.error(loc,
2188 "A pure method may not have a diverges clause",
2189 locp);
2190 }
2191 }
2192 }
2193 }
2194 // fall-through
2195 case TagConstants.ENSURES:
2196 case TagConstants.ALSO_ENSURES:
2197 case TagConstants.POSTCONDITION:
2198 case TagConstants.WHEN:
2199 {
2200 ExprModifierPragma emp = (ExprModifierPragma)p;
2201
2202 if( ctxt instanceof InitBlock ) {
2203 boolean oldIsRESContext = isRESContext;
2204 boolean oldIsTwoStateContext = isTwoStateContext;
2205 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
2206 try {
2207 isRESContext = true;
2208 isTwoStateContext = true;
2209 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2210 emp.expr = checkPredicate(env, emp.expr);
2211 } finally {
2212 isRESContext = oldIsRESContext;
2213 isTwoStateContext = oldIsTwoStateContext;
2214 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
2215 }
2216 } else if( ctxt instanceof RoutineDecl ) {
2217 RoutineDecl rd = (RoutineDecl)ctxt;
2218 escjava.ast.Utils.owningDecl.set(emp,rd);
2219 boolean oldIsRESContext = isRESContext;
2220 boolean oldIsTwoStateContext = isTwoStateContext;
2221 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
2222 isRESContext = true;
2223 isTwoStateContext = true;
2224 // If "rd" is an overridable method, then every private field
2225 // mentioned in "emp.expr" must be spec_public.
2226 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
2227 isPrivateFieldAccessAllowed = false;
2228 }
2229 try {
2230 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2231 emp.expr = checkPredicate(env, emp.expr);
2232 } finally {
2233 isRESContext = oldIsRESContext;
2234 isTwoStateContext = oldIsTwoStateContext;
2235 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
2236 }
2237 } else {
2238 ErrorSet.error(p.getStartLoc(),
2239 TagConstants.toString(tag)
2240 +" annotations can occur only on "
2241 +"initializer, method and constructor declarations");
2242 }
2243 break;
2244 }
2245
2246
2247 case TagConstants.SIGNALS:
2248 {
2249 tag = p.originalTag();
2250 VarExprModifierPragma vemp = (VarExprModifierPragma)p;
2251
2252 if( !(ctxt instanceof RoutineDecl ) ) {
2253 ErrorSet.error(p.getStartLoc(),
2254 TagConstants.toString(tag)
2255 +" annotations can occur only on "
2256 +"method and constructor declarations");
2257 } else {
2258 RoutineDecl rd = (RoutineDecl)ctxt;
2259
2260 // Resolve type and check that it is a subtype of Throwable
2261 // and comparable to some type mentioned in the throws set.
2262 env.resolveType(sig,vemp.arg.type);
2263 //TypeSig top = Main.options().useThrowable ?
2264 // Types.javaLangThrowable() : Types.javaLangException();
2265 TypeSig top = Types.javaLangThrowable();
2266 // FIXME - JML actually requires that the var be a subtype of
2267 // Exception, but the original Esc/Java did not
2268 if (!Types.isSubclassOf(vemp.arg.type,top)) {
2269 ErrorSet.error(vemp.arg.type.getStartLoc(),
2270 "The type of the " +
2271 TagConstants.toString(tag) +
2272 " argument must be a subtype of " +
2273 Types.printName(top));
2274 } else {
2275 // "vemp.arg.type" is a subclass of "Throwable", so it
2276 // must be a "TypeName" or a "TypeSig"
2277 TypeSig ssig;
2278 if (vemp.arg.type instanceof TypeSig) {
2279 ssig = (TypeSig)vemp.arg.type;
2280 } else {
2281 ssig = TypeSig.getSig((TypeName)vemp.arg.type);
2282 }
2283 boolean okay = false;
2284 for (int i = 0; i < rd.raises.size(); i++) {
2285 TypeName tn = rd.raises.elementAt(i);
2286 TypeSig tsig = TypeSig.getSig(tn);
2287 if (Types.isSubclassOf(ssig, tsig) ||
2288 Types.isSubclassOf(tsig, ssig)) {
2289 okay = true;
2290 break;
2291 }
2292 }
2293 /* FIXME - what about Error exceptions, must they be mentioned? */
2294 /* FIXME
2295 if (!okay) {
2296 if (!( (vemp.expr instanceof LiteralExpr) &&
2297 ((LiteralExpr)vemp.expr).value.equals(Boolean.FALSE))) {
2298 ErrorSet.error(vemp.arg.type.getStartLoc(),
2299 "The type of the " +
2300 TagConstants.toString(tag) +
2301 " argument must be comparable to some type"+
2302 " mentioned in the routine's throws set");
2303 }
2304 }
2305 */
2306 }
2307
2308 if (tag == TagConstants.SIGNALS_ONLY) {
2309 // Check that all Exceptions listed are either in the
2310 // throws list or are RuntimeExceptions
2311
2312 // FIXME
2313
2314 }
2315
2316 Env subenv = new EnvForLocals(env, vemp.arg);
2317 // FIXME - below we say that this is a twostate context, in which case we should not set this to static???
2318 /*
2319 if (rd instanceof ConstructorDecl) {
2320 subenv = subenv.asStaticContext();
2321 }
2322 */
2323
2324 // Check the expression to be an appropriate predicate
2325 boolean oldIsTwoStateContext = isTwoStateContext;
2326 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
2327 isTwoStateContext = true;
2328 // If "rd" is an overridable method, then every private field
2329 // mentioned in "emp.expr" must be spec_public.
2330 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
2331 isPrivateFieldAccessAllowed = false;
2332 }
2333 try {
2334 if (vemp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
2335 vemp.expr = checkPredicate(subenv, vemp.expr);
2336 } finally {
2337 isTwoStateContext = oldIsTwoStateContext;
2338 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
2339 }
2340 }
2341 break;
2342 }
2343
2344
2345 case TagConstants.MONITORED_BY: {
2346 ExprModifierPragma emp = (ExprModifierPragma)p;
2347
2348 if (ctxt.getTag() != TagConstants.FIELDDECL) {
2349 ErrorSet.error(emp.loc,
2350 "The monitored_by annotation can occur only on "+
2351 "field declarations");
2352 } else {
2353 FieldDecl fd = (FieldDecl)ctxt;
2354
2355 int oldAccessibilityLowerBound = accessibilityLowerBound;
2356 ASTNode oldAccessibilityContext = accessibilityContext;
2357 accessibilityLowerBound = getAccessibility(fd.modifiers);
2358 accessibilityContext = fd;
2359 emp.expr = checkExpr(env, emp.expr, Types.javaLangObject());
2360 accessibilityLowerBound = oldAccessibilityLowerBound;
2361 accessibilityContext = oldAccessibilityContext;
2362 }
2363 break;
2364 }
2365
2366 case TagConstants.MODIFIESGROUPPRAGMA: {
2367 ModifiesGroupPragma mg = (ModifiesGroupPragma)p;
2368 if (ctxt instanceof InitBlock || ctxt instanceof RoutineDecl) {
2369 CondExprModifierPragmaVec v = mg.items;
2370 for (int i=0; i<v.size(); ++i) {
2371 checkModifierPragma(v.elementAt(i),ctxt,env);
2372 }
2373 if (mg.precondition != null)
2374 mg.precondition = checkPredicate(env,mg.precondition); // FIXME - pre environment ?
2375 } else {
2376 ErrorSet.error(mg.clauseLoc,
2377 "A modifies annotation " +
2378 "can occur only on " +
2379 "method and constructor declarations");
2380 }
2381 break;
2382 }
2383
2384 case TagConstants.MODIFIES:
2385 case TagConstants.ASSIGNABLE:
2386 case TagConstants.MODIFIABLE:
2387 case TagConstants.STILL_DEFERRED: {
2388 CondExprModifierPragma emp = (CondExprModifierPragma)p;
2389
2390 if ((ctxt instanceof RoutineDecl ) ) {
2391 RoutineDecl rd = (RoutineDecl)ctxt;
2392
2393 Assert.notFalse(!isSpecDesignatorContext);
2394 isSpecDesignatorContext = true;
2395 Env newenv = env;
2396 /*
2397 // But we do need to allow the fields of this in the modifies clause, which
2398 // using the static context does not permit.
2399 if (rd instanceof ConstructorDecl) {
2400 // disallow "this" from constructor "modifies" clauses
2401 newenv = env.asStaticContext();
2402 }
2403 */
2404 emp.expr = checkDesignator(newenv, emp.expr);
2405 switch (emp.expr.getTag()) {
2406 case TagConstants.FIELDACCESS: {
2407 FieldAccess fa = (FieldAccess)emp.expr;
2408 if (fa.decl != null &&
2409 (ctxt instanceof MethodDecl) && // FIXME - what about constructors
2410 Modifiers.isFinal(fa.decl.modifiers) &&
2411 // The array "length" field has already been checked
2412 // insuper.checkDesignator().
2413 fa.decl != Types.lengthFieldDecl) {
2414
2415 // java.lang.System has fields in, out, err that are special
2416 // cases. Somehow, Java allows them to be final and yet be
2417 // modified by public routines. Instead of a general
2418 // mechanism, we just do a special case here.
2419 if (fa.decl.parent != Types.javaLangSystem().getTypeDecl())
2420 ErrorSet.caution(fa.locId, "a final field is not allowed as " +
2421 "the designator in a modifies clause");
2422 }
2423 break;
2424 }
2425
2426 case TagConstants.ARRAYREFEXPR:
2427 case TagConstants.ARRAYRANGEREFEXPR:
2428 case TagConstants.WILDREFEXPR:
2429 case TagConstants.EVERYTHINGEXPR:
2430 case TagConstants.NOTHINGEXPR:
2431 case TagConstants.NOTSPECIFIEDEXPR:
2432 break;
2433
2434 default:
2435 if (escjava.parser.EscPragmaParser.
2436 informalPredicateDecoration.get(emp.expr)==null) {
2437 // The expression is not a designator
2438 // but we allow an informal predicate
2439 if (!Types.isErrorType(getType(emp.expr)))
2440 ErrorSet.error(emp.expr.getStartLoc(),
2441 "Not a specification designator expression");
2442 } else {
2443 emp.expr = null;
2444 }
2445 }
2446 if (rd instanceof MethodDecl && Utils.isPure(rd) &&
2447 emp.expr != null && emp.expr.getTag() != TagConstants.NOTHINGEXPR) {
2448 ErrorSet.error(p.getStartLoc(),
2449 "A pure method may not have a modifies clause",
2450 Utils.findPurePragma(rd).getStartLoc());
2451 }
2452 if (rd instanceof ConstructorDecl && Utils.isPure(rd) &&
2453 emp.expr != null &&
2454 !(emp.expr.getTag() == TagConstants.NOTHINGEXPR ||
2455 (emp.expr.getTag() == TagConstants.WILDREFEXPR &&
2456 (((WildRefExpr)emp.expr).var instanceof ThisExpr) &&
2457 ((ThisExpr)((WildRefExpr)emp.expr).var).classPrefix == null)
2458 ||
2459 ((emp.expr instanceof FieldAccess) &&
2460 Types.isSubclassOf(
2461 TypeSig.getSig(rd.parent),
2462 TypeSig.getSig(((FieldAccess)emp.expr).decl.parent)
2463 )
2464 ))
2465 ) {
2466 ErrorSet.error(p.getStartLoc(),
2467 "A pure constructor may not have a modifies clause",
2468 Utils.findPurePragma(rd).getStartLoc());
2469 }
2470 isSpecDesignatorContext = false;
2471 if (emp.cond != null) emp.cond = checkExpr(newenv, emp.cond);
2472 }
2473 break;
2474 }
2475
2476 case TagConstants.ALSO:
2477 case TagConstants.ALSO_REFINE:
2478 case TagConstants.MODEL_PROGRAM:
2479 case TagConstants.CODE_CONTRACT:
2480 case TagConstants.BEHAVIOR:
2481 case TagConstants.CLOSEPRAGMA:
2482 case TagConstants.EXAMPLE:
2483 case TagConstants.EXCEPTIONAL_BEHAVIOR:
2484 case TagConstants.EXCEPTIONAL_EXAMPLE:
2485 case TagConstants.FOR_EXAMPLE:
2486 case TagConstants.IMPLIES_THAT:
2487 case TagConstants.NORMAL_BEHAVIOR:
2488 case TagConstants.NORMAL_EXAMPLE:
2489 case TagConstants.OPENPRAGMA:
2490 // Desugaring happens before type-checking,
2491 // This shouldn't happen.
2492 break;
2493
2494 case TagConstants.GHOST:
2495 case TagConstants.MODEL:
2496 break;
2497
2498 case TagConstants.NESTEDMODIFIERPRAGMA:
2499 {
2500 java.util.ArrayList list = ((NestedModifierPragma)p).list;
2501 java.util.Iterator i = list.iterator();
2502 while (i.hasNext()) {
2503 ModifierPragmaVec mpv = (ModifierPragmaVec)i.next();
2504 checkModifierPragmaVec(mpv,ctxt,env);
2505 }
2506 break;
2507 }
2508
2509 case TagConstants.PARSEDSPECS:
2510 {
2511 escjava.ParsedRoutineSpecs pp = ((ParsedSpecs)p).specs;
2512 java.util.Iterator i = pp.specs.iterator();
2513 while (i.hasNext()) {
2514 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
2515 }
2516 i = pp.impliesThat.iterator();
2517 while (i.hasNext()) {
2518 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
2519 }
2520 i = pp.examples.iterator();
2521 while (i.hasNext()) {
2522 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
2523 }
2524 /* This duplicates stuff
2525 // The last element is the ParsedSpecs containing all the
2526 // clauses etc.
2527 ModifierPragmaVec mpv = pp.modifiers;
2528 ModifierPragma last = mpv.elementAt(mpv.size()-1);
2529 mpv.removeElementAt(mpv.size()-1);
2530 checkModifierPragmaVec(mpv,ctxt,env);
2531 mpv.addElement(last);
2532 */
2533 break;
2534 }
2535
2536 case TagConstants.MAPS: {
2537 Identifier fid = ((FieldDecl)ctxt).id;
2538 MapsExprModifierPragma ep = (MapsExprModifierPragma)p;
2539 //System.out.println("FOUND " + TagConstants.toString(tag) + " for " + fid + " " + ep.id);
2540 if (ep.expr != null) ep.expr = checkExpr(env,ep.expr);
2541 isSpecDesignatorContext = true;
2542 if (ep.mapsexpr != null) ep.mapsexpr = checkDesignator(env,ep.mapsexpr);
2543 isSpecDesignatorContext = false;
2544 Expr e = ep.expr;
2545 if (e == null || TypeCheck.inst.getType(e) == Types.errorType) {
2546 // skip
2547 } else if (e instanceof FieldAccess) {
2548 FieldAccess fe = (FieldAccess)e; // datagroup
2549 FieldDecl fd = (FieldDecl)ctxt; // field with which maps decl is associated
2550 if (Modifiers.isStatic( fe.decl.modifiers)
2551 && !Modifiers.isStatic( fd.modifiers) ){
2552 ErrorSet.error(((FieldDecl)ctxt).getStartLoc(),
2553 "An instance field may not be added to a static datagroup",
2554 fe.decl.getStartLoc());
2555 } else {
2556 Datagroups.add(fd.parent,fe.decl,ep.mapsexpr);
2557 }
2558 } else {
2559 ErrorSet.error(e.getStartLoc(),
2560 "Expected a field reference here, found " +
2561 e.getClass());
2562 }
2563 break;
2564 }
2565
2566 case TagConstants.IN: {
2567 MapsExprModifierPragma ep = (MapsExprModifierPragma)p;
2568 if (ep.expr != null) ep.expr = checkExpr(env,ep.expr);
2569 Expr e = ep.expr;
2570 if (e == null || TypeCheck.inst.getType(e) == Types.errorType) {
2571 } else if (e instanceof FieldAccess) {
2572 FieldAccess fe = (FieldAccess)e; // datagroup
2573 FieldDecl fd = (FieldDecl)ctxt; // field being put in the datagroup
2574 Expr eva = AmbiguousVariableAccess.make(
2575 SimpleName.make(fd.id,fd.getStartLoc()));
2576 eva = checkExpr(env,eva);
2577 if (Modifiers.isStatic( fe.decl.modifiers ) &&
2578 !Modifiers.isStatic(fd.modifiers)) {
2579 ErrorSet.error(fd.getStartLoc(),
2580 "An instance field may not be added to a static datagroup",
2581 fe.decl.getStartLoc());
2582 } else {
2583 Datagroups.add(fd.parent,fe.decl,eva);
2584 }
2585 } else {
2586 ErrorSet.error(e.getStartLoc(),
2587 "Expected a field reference here, found " +
2588 e.getClass());
2589 }
2590 break;
2591 }
2592
2593 //alx: commented out not to interfere with the dw implementation
2594 case TagConstants.READONLY:
2595 case TagConstants.PEER:
2596 case TagConstants.REP:
2597 // FIXME - need to support these
2598 break;
2599 //alx-end
2600
2601 default:
2602 ErrorSet.error(p.getStartLoc(),
2603 "Ignored unexpected " +
2604 TagConstants.toString(tag) +
2605 " tag");
2606 break;
2607 }
2608 } finally {
2609 inAnnotation = savedInAnnotation;
2610 }
2611 return env;
2612 }
2613
2614 /**
2615 * @return whether or not <code>md</code> can be overridden in some possible
2616 * subclass.
2617 */
2618
2619 public static boolean isOverridable(/*@ non_null */ MethodDecl md) {
2620 return !(Modifiers.isPrivate(md.modifiers) ||
2621 Modifiers.isFinal(md.modifiers) ||
2622 Modifiers.isFinal(md.parent.modifiers) ||
2623 Modifiers.isStatic(md.modifiers));
2624 }
2625
2626 /**
2627 * @return a value appropriate for assignment to
2628 * <code>accessibilityLowerBound</code>, given member modifiers.
2629 */
2630
2631 protected int getAccessibility(int modifiers) {
2632 if (Modifiers.isPrivate(modifiers)) {
2633 return ACC_LOW_BOUND_Private;
2634 } else if (Modifiers.isPackage(modifiers)) {
2635 return ACC_LOW_BOUND_Package;
2636 } else if (Modifiers.isProtected(modifiers)) {
2637 return ACC_LOW_BOUND_Protected;
2638 } else {
2639 Assert.notFalse(Modifiers.isPublic(modifiers));
2640 return ACC_LOW_BOUND_Public;
2641 }
2642 }
2643
2644 protected Env checkStmtPragma(Env e, StmtPragma s) {
2645 boolean savedInAnnotation = inAnnotation;
2646 inAnnotation = true; // Must be reset before we exit!
2647 boolean savedTwoStateContext = isTwoStateContext;
2648 isTwoStateContext = true;
2649 try {
2650 int tag = s.getTag();
2651 switch(tag) {
2652 case TagConstants.UNREACHABLE:
2653 break;
2654
2655 case TagConstants.SETSTMTPRAGMA: {
2656 SetStmtPragma set = (SetStmtPragma)s;
2657 set.target = checkExpr(e, set.target);
2658 set.value = checkExpr(e, set.value);
2659 checkBinaryExpr(TagConstants.ASSIGN, set.target,
2660 set.value, set.locOp);
2661 Expr t = set.target;
2662 int nonGhostLoc = isGhost(t);
2663 if (nonGhostLoc != 0) {
2664 ErrorSet.error(s.getStartLoc(),"May use set only with assignment targets that are declared ghost",nonGhostLoc);
2665 }
2666 /*
2667 if (t instanceof FieldAccess &&
2668 ((FieldAccess)t).decl == Types.lengthFieldDecl) {
2669 ErrorSet.error(s.getStartLoc(),"The length field of an array may not be set");
2670 }
2671 */
2672 break;
2673 }
2674
2675 case TagConstants.HENCE_BY:
2676 case TagConstants.ASSUME:
2677 case TagConstants.ASSERT:
2678 {
2679 ExprStmtPragma es = (ExprStmtPragma)s;
2680 es.expr = checkPredicate(e, es.expr);
2681 if (es.label != null)
2682 es.label = checkExpr(e, es.label);
2683 break;
2684 }
2685
2686 case TagConstants.LOOP_INVARIANT:
2687 case TagConstants.MAINTAINING:
2688 {
2689 ExprStmtPragma lis = (ExprStmtPragma)s;
2690 loopInvariants.addElement(lis);
2691 break;
2692 }
2693
2694 case TagConstants.DECREASES:
2695 case TagConstants.DECREASING:
2696 {
2697 ExprStmtPragma lis = (ExprStmtPragma)s;
2698 loopDecreases.addElement(lis);
2699 break;
2700 }
2701
2702 case TagConstants.LOOP_PREDICATE:
2703 {
2704 ExprStmtPragma lis = (ExprStmtPragma)s;
2705 loopPredicates.addElement(lis);
2706 break;
2707 }
2708
2709 case TagConstants.SKOLEMCONSTANTPRAGMA:
2710 {
2711 SkolemConstantPragma p = (SkolemConstantPragma)s;
2712 skolemConstants.append(p.decls);
2713 break;
2714 }
2715
2716 default:
2717 Assert.fail("Unexpected tag " + tag +" "+s +
2718 " " + Location.toString(s.getStartLoc()));
2719 }
2720 } finally {
2721 inAnnotation = savedInAnnotation;
2722 isTwoStateContext = savedTwoStateContext;
2723 }
2724 return e;
2725 }
2726
2727
2728 // Utility routines
2729
2730 /**
2731 * Copy the Type associated with an expression by the typechecking pass to
2732 * another Expr. This is used by Substitute to ensure it returns an Expr of the
2733 * same Type.
2734 */
2735 public static void copyType(VarInit from, VarInit to) {
2736 Type t = getTypeOrNull(from);
2737 if (t != null)
2738 setType(to, t);
2739 }
2740
2741 /**
2742 * @return a set of *all* the methods a given method overrides. This includes
2743 * transitivity.
2744 */
2745 //@ requires md != null;
2746 //@ ensures \result != null;
2747 //@ ensures \result.elementType == \type(MethodDecl);
2748 public static Set getAllOverrides(MethodDecl md) {
2749 Set direct = javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
2750 Set result = new Set();
2751
2752 Enumeration e = direct.elements();
2753 while (e.hasMoreElements()) {
2754 MethodDecl directMD = (MethodDecl)(e.nextElement());
2755 result.add(directMD);
2756 result.addEnumeration(getAllOverrides(directMD).elements());
2757 }
2758
2759 return result;
2760 }
2761
2762 public static javafe.util.Set getDirectOverrides(MethodDecl md) {
2763 return javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
2764 }
2765
2766 /**
2767 * @return If <code>md</code> is a method that overrides a method in a
2768 * superclass, the overridden method is returned. Otherwise, if <code>md</code>
2769 * overrides a method in an interface, such a method is returned. Otherwise,
2770 * <code>null</code> is returned.
2771 */
2772
2773 public static MethodDecl getSuperClassOverride(MethodDecl md) {
2774 MethodDecl classOverride = null;
2775 MethodDecl interfaceOverride = null;
2776 Set direct = javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
2777 Enumeration e = direct.elements();
2778 while (e.hasMoreElements()) {
2779 MethodDecl directMD = (MethodDecl)(e.nextElement());
2780 if (directMD.parent instanceof ClassDecl) {
2781 if (classOverride == null) {
2782 classOverride = directMD;
2783 } else {
2784 Assert.fail("we think this can no longer happen!");
2785 // This suggests that the method is inherited from TWO classes!
2786 // This can actually happen, if the method is one that is
2787 // declared in Object, because every interface has the methods of
2788 // Object. In this case, pick the method override that does not
2789 // reside in Object.
2790 Type javaLangObject = Types.javaLangObject();
2791 Type t0 = TypeSig.getSig(classOverride.parent);
2792 Type t1 = TypeSig.getSig(directMD.parent);
2793 Assert.notFalse(Types.isSameType(t0, javaLangObject) ||
2794 Types.isSameType(t1, javaLangObject));
2795 Assert.notFalse(!Types.isSameType(t0, javaLangObject) ||
2796 !Types.isSameType(t1, javaLangObject));
2797 if (!Types.isSameType(t1, javaLangObject)) {
2798 classOverride = directMD;
2799 }
2800 }
2801 } else {
2802 interfaceOverride = directMD;
2803 }
2804 }
2805 if (classOverride != null) {
2806 return classOverride;
2807 } else {
2808 return interfaceOverride;
2809 }
2810 }
2811
2812 /**
2813 * @return whether or not <code>rd</code> is a method override declaration, that
2814 * is, whether or not <code>rd</code> overrides a method declared in a superclass
2815 * or superinterface.
2816 */
2817
2818 public static boolean isMethodOverride(RoutineDecl rd) {
2819 return getOverrideStatus(rd) != MSTATUS_NEW_ROUTINE;
2820 }
2821
2822 static public final int MSTATUS_NEW_ROUTINE = 0;
2823 static public final int MSTATUS_CLASS_NEW_METHOD = 1;
2824 static public final int MSTATUS_OVERRIDE = 2;
2825
2826 /**
2827 * @return <code>MSTATUS_NEW_ROUTINE</code> if <code>rd</code> is a routine that
2828 * doesn't override any other method. This includes the case where
2829 * <code>rd</code> is a constructor or a static method.
2830 *
2831 * <p> Returns <code>MSTATUS_CLASS_NEW_METHOD</code> if <code>rd</code> is a
2832 * method declared in a class, doesn't override any method in any superclass, but
2833 * overrides a method in an interface.
2834 *
2835 * <p> Otherwise, returns <code>MSTATUS_OVERRIDE</code>.
2836 */
2837
2838 /*@ ensures \result == MSTATUS_NEW_ROUTINE ||
2839 @ \result == MSTATUS_CLASS_NEW_METHOD ||
2840 @ \result == MSTATUS_OVERRIDE;
2841 */
2842 public static int getOverrideStatus(/*@ non_null */ RoutineDecl rd) {
2843 if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) {
2844 return MSTATUS_NEW_ROUTINE;
2845 }
2846 MethodDecl md = (MethodDecl)rd;
2847
2848 Set direct = javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
2849 if (direct.size() == 0) {
2850 return MSTATUS_NEW_ROUTINE;
2851 }
2852 if (!(md.parent instanceof ClassDecl)) {
2853 return MSTATUS_OVERRIDE;
2854 }
2855
2856 Enumeration e = direct.elements();
2857 while (e.hasMoreElements()) {
2858 MethodDecl directMD = (MethodDecl)(e.nextElement());
2859 if (directMD.parent instanceof ClassDecl) {
2860 return MSTATUS_OVERRIDE;
2861 }
2862 }
2863 return MSTATUS_CLASS_NEW_METHOD;
2864 }
2865
2866 /**
2867 * @return null if method md is allowed to declare its jth (counting from 0)
2868 * formal parameter as non_null. That is the case if the method does not
2869 * override anything, or if in everything that it does override that parameter is
2870 * declared non_null. Otherwise returns the MethodDecl corresponding to the
2871 * overridden method with which the argument rd is in conflict.
2872 *
2873 * @todo kiniry - implement nullable versions of this or make two new methods
2874 */
2875 static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j) {
2876 if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) {
2877 return null;
2878 }
2879 MethodDecl md = (MethodDecl)rd;
2880
2881 Set direct = javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
2882 if (direct.size() == 0) {
2883 return null;
2884 }
2885 return getSuperNonNullStatus(rd,j,direct);
2886 }
2887
2888 static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides) {
2889 Enumeration e = directOverrides.elements();
2890 while (e.hasMoreElements()) {
2891 MethodDecl directMD = (MethodDecl)(e.nextElement());
2892 FormalParaDecl f = directMD.args.elementAt(j);
2893 if (Utils.findModifierPragma(f,TagConstants.NON_NULL) == null)
2894 return directMD;
2895 }
2896 return null;
2897 }
2898
2899 /** Returns non-zero if the expression is a ghost expression - that is, it
2900 would not exist if all ghost declarations were removed. Otherwise
2901 returns a Location value of a relevant non-ghost declaration.
2902 */
2903 public int isGhost(Expr t) {
2904 if (t instanceof ArrayRefExpr) {
2905 t = ((ArrayRefExpr)t).array;
2906 }
2907 if (t instanceof FieldAccess) {
2908 FieldAccess fa = (FieldAccess)t;
2909 if (fa.decl == null || GhostEnv.isGhostField(fa.decl))
2910 return 0;
2911 int gl = isGhost(fa.od);
2912 if (gl == 0) return 0;
2913 if (gl == -1) return fa.decl.getStartLoc();
2914 return gl;
2915 } else if (t instanceof VariableAccess) {
2916 VariableAccess va = (VariableAccess)t;
2917 GenericVarDecl gd = va.decl;
2918 if ( Utils.findModifierPragma(
2919 gd.pmodifiers,TagConstants.GHOST) == null)
2920 return gd.getStartLoc();
2921 } else if (t instanceof ParenExpr) {
2922 return isGhost( ((ParenExpr)t).expr );
2923 } else if (t instanceof CastExpr) {
2924 return isGhost( ((CastExpr)t).expr );
2925 }
2926 return 0;
2927 // FIXME - need some test that the expression in advance of
2928 // a . in a field reference or the [] in an array reference
2929 // only designates ghost fields/variables
2930 // e.g. what about method calls, operator expressions?
2931
2932 }
2933
2934 public int isGhost(ObjectDesignator od) {
2935 if (od instanceof ExprObjectDesignator) {
2936 Expr e = ((ExprObjectDesignator)od).expr;
2937 if (e == null || e instanceof ThisExpr) return -1;
2938 return isGhost(e);
2939 }
2940 return -1; // OK for TypeObjectDesignator and SuperObjectDesignator
2941 }
2942
2943 protected boolean assignmentConvertable(Expr e, Type t) {
2944 if (super.assignmentConvertable(e,t)) return true;
2945 return Types.isTypeType(t) && Types.isTypeType(getType(e));
2946 }
2947
2948 //alx: dw overridden, so javafe handels pure methods correctly
2949 //TODO: what other specs?
2950 protected boolean isPure( RoutineDecl rd) {
2951 return Utils.isPure(rd);
2952 }
2953 //alx-end
2954
2955 } // end of class FlowInsensitiveChecks
2956
2957 /*
2958 * Local Variables:
2959 * Mode: Java
2960 * fill-column: 85
2961 * End:
2962 */