001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.translate;
004
005 import java.io.ByteArrayOutputStream;
006 import java.util.ArrayList;
007 import java.util.Enumeration;
008 import java.util.HashMap;
009 import java.util.Hashtable;
010 import java.util.Iterator;
011 import java.util.LinkedList;
012 import java.util.Map;
013 import java.util.Vector;
014
015 import javafe.Tool;
016 import javafe.ast.ASTDecoration;
017 import javafe.ast.ASTNode;
018 import javafe.ast.ArrayInit;
019 import javafe.ast.ArrayRefExpr;
020 import javafe.ast.ArrayType;
021 import javafe.ast.AssertStmt;
022 import javafe.ast.BinaryExpr;
023 import javafe.ast.BreakStmt;
024 import javafe.ast.CastExpr;
025 import javafe.ast.CatchClause;
026 import javafe.ast.ClassDecl;
027 import javafe.ast.ClassLiteral;
028 import javafe.ast.CondExpr;
029 import javafe.ast.ConstructorDecl;
030 import javafe.ast.ConstructorInvocation;
031 import javafe.ast.ContinueStmt;
032 import javafe.ast.DoStmt;
033 import javafe.ast.EvalStmt;
034 import javafe.ast.Expr;
035 import javafe.ast.ExprObjectDesignator;
036 import javafe.ast.ExprVec;
037 import javafe.ast.FieldAccess;
038 import javafe.ast.FieldDecl;
039 import javafe.ast.ForStmt;
040 import javafe.ast.FormalParaDecl;
041 import javafe.ast.GenericBlockStmt;
042 import javafe.ast.GenericVarDecl;
043 import javafe.ast.Identifier;
044 import javafe.ast.IfStmt;
045 import javafe.ast.InitBlock;
046 import javafe.ast.InstanceOfExpr;
047 import javafe.ast.LabelStmt;
048 import javafe.ast.LiteralExpr;
049 import javafe.ast.LocalVarDecl;
050 import javafe.ast.MethodDecl;
051 import javafe.ast.MethodInvocation;
052 import javafe.ast.ModifierPragma;
053 import javafe.ast.NewArrayExpr;
054 import javafe.ast.NewInstanceExpr;
055 import javafe.ast.ParenExpr;
056 import javafe.ast.PrettyPrint;
057 import javafe.ast.PrimitiveType;
058 import javafe.ast.ReturnStmt;
059 import javafe.ast.RoutineDecl;
060 import javafe.ast.Stmt;
061 import javafe.ast.SwitchLabel;
062 import javafe.ast.SwitchStmt;
063 import javafe.ast.SynchronizeStmt;
064 import javafe.ast.ThisExpr;
065 import javafe.ast.ThrowStmt;
066 import javafe.ast.TryCatchStmt;
067 import javafe.ast.TryFinallyStmt;
068 import javafe.ast.Type;
069 import javafe.ast.TypeDecl;
070 import javafe.ast.TypeDeclElem;
071 import javafe.ast.TypeName;
072 import javafe.ast.UnaryExpr;
073 import javafe.ast.VarDeclStmt;
074 import javafe.ast.VarInit;
075 import javafe.ast.VariableAccess;
076 import javafe.ast.WhileStmt;
077 import javafe.tc.TypeSig;
078 import javafe.util.Assert;
079 import javafe.util.ErrorSet;
080 import javafe.util.Info;
081 import javafe.util.Location;
082 import javafe.util.Set;
083 import javafe.util.StackVector;
084 import escjava.Main;
085 import escjava.Options;
086 import escjava.ast.ArrayRangeRefExpr;
087 import escjava.ast.Call;
088 import escjava.ast.CmdCmdCmd;
089 import escjava.ast.Condition;
090 import escjava.ast.ConditionVec;
091 import escjava.ast.DecreasesInfo;
092 import escjava.ast.DecreasesInfoVec;
093 import escjava.ast.DerivedMethodDecl;
094 import escjava.ast.DynInstCmd;
095 import escjava.ast.EscPrettyPrint;
096 import escjava.ast.EverythingExpr;
097 import escjava.ast.ExprCmd;
098 import escjava.ast.ExprModifierPragma;
099 import escjava.ast.ExprStmtPragma;
100 import escjava.ast.ExprStmtPragmaVec;
101 import escjava.ast.GenericVarDeclVec;
102 import escjava.ast.GetsCmd;
103 import escjava.ast.GhostDeclPragma;
104 import escjava.ast.GuardedCmd;
105 import escjava.ast.GuardedCmdVec;
106 import escjava.ast.LabelExpr;
107 import escjava.ast.LocalVarDeclVec;
108 import escjava.ast.LoopCmd;
109 import escjava.ast.ModelDeclPragma;
110 import escjava.ast.Modifiers;
111 import escjava.ast.ModifiesGroupPragma;
112 import escjava.ast.ModifiesGroupPragmaVec;
113 import escjava.ast.NaryExpr;
114 import escjava.ast.NothingExpr;
115 import escjava.ast.RestoreFromCmd;
116 import escjava.ast.SeqCmd;
117 import escjava.ast.SetStmtPragma;
118 import escjava.ast.SimpleModifierPragma;
119 import escjava.ast.SkolemConstantPragma;
120 import escjava.ast.Spec;
121 import escjava.ast.SubGetsCmd;
122 import escjava.ast.SubSubGetsCmd;
123 import escjava.ast.TagConstants;
124 import escjava.ast.TypeExpr;
125 import escjava.ast.Utils;
126 import escjava.ast.VarInCmd;
127 import escjava.ast.WildRefExpr;
128 import escjava.backpred.FindContributors;
129 import escjava.tc.FlowInsensitiveChecks;
130 import escjava.tc.TypeCheck;
131 import escjava.tc.Types;
132
133 public final class Translate
134 {
135 Frame frameHandler = null;
136
137 // This Set contains method declarations for which axioms derived from
138 // postconditions need to be added to the assumptions for verifying the body.
139 public static java.util.Set axsToAdd = new java.util.HashSet();
140
141 private Hashtable premap;
142 private Hashtable premapWithArgs;
143
144 /** The type containing the routine whose body is being translated. */
145 private TypeDecl typeDecl;
146
147 /**
148 * Translates the body of a method or constructor, as described in ESCJ 16, section
149 * 8.
150 *
151 * @param predictedSynTargs for correct translation, this must contain an upper
152 * bound for the syntactic targets of the result of this call. A value of null is
153 * taken to represent the set of all variables & is hence always a safe value.
154 *
155 * @note passing a value of <the empty set> for predictedSynTargs will give a
156 * translation missing assert statements for checking call preconditions, but
157 * otherwise correct. The resulting computation runs faster than passing null,
158 * while still having the same set of targets. escjava.Main is currently using
159 * this trick as a kludge to compute the syntactic targets upper bound.
160 */
161 //@ requires rd.body != null;
162 public GuardedCmd trBody(/*@ non_null */ RoutineDecl rd,
163 /*@ non_null */ FindContributors scope,
164 Hashtable premap,
165 Set predictedSynTargs,
166 Translate inlineParent,
167 boolean issueCautions) {
168
169 Hashtable paramMap = GetSpec.makeSubst(rd.args, "pre");
170 premapWithArgs = new Hashtable();
171 premapWithArgs.putAll(paramMap);
172 if (premap != null) premapWithArgs.putAll(premap);
173
174 frameHandler = new Frame(this, issueCautions, rd, premapWithArgs);
175 TrAnExpr.translate = this;
176 this.typeDecl = rd.parent;
177 this.premap = premap;
178 axsToAdd = new java.util.HashSet();
179
180 // Reset the state of the AuxInfo module if this is top-level call to trBody
181 if (inlineParent == null) {
182 AuxInfo.reset();
183 }
184
185 // Reset the internal state of <code>this</code>
186 this.rdCurrent = rd;
187 this.scope = scope;
188 this.predictedSynTargs = predictedSynTargs;
189 this.inlineParent = inlineParent;
190 if (inlineParent == null) {
191 this.inConstructorContext = isStandaloneConstructor(rd);
192 } else {
193 this.inConstructorContext = inlineParent.inConstructorContext &&
194 rdCurrent.parent == inlineParent.rdCurrent.parent;
195 }
196 this.issueCautions = issueCautions;
197 this.modifyEverythingLocations = new ArrayList();
198
199 if (Info.on) {
200 System.out.print("trBody: ");
201 for (Translate ttIR = inlineParent;
202 ttIR != null;
203 ttIR = ttIR.inlineParent) {
204 System.out.print(" ");
205 }
206 System.out.println(TypeCheck.inst.getSig(rd.parent).toString() + "." +
207 TypeCheck.inst.getRoutineName(rd) +
208 TypeCheck.getSignature(rd));
209 System.out.flush();
210 }
211
212 code.clear(); code.push(); // this mark popped by "spill"
213 declaredLocals.clear();
214 temporaries.clear(); temporaries.push(); // this mark popped by "spill"
215 tmpcount = 0;
216
217 GC.thisvar.decl.type = scope.originType;
218
219 code.push(); // this mark popped below
220
221 /*
222 * Translate body:
223 */
224 if (rd.getTag() == TagConstants.METHODDECL) {
225 if (! Modifiers.isSynchronized(rd.modifiers)) {
226 // non-synchronized method
227 trStmt(rd.body,rd.parent);
228 } else if (! Modifiers.isStatic(rd.modifiers)) {
229 // synchronized instance method
230 trSynchronizedBody(GC.thisvar, rd.body, rd.locOpenBrace, typeDecl);
231 } else {
232 // synchronized static method
233 trSynchronizedBody(GC.nary(TagConstants.CLASSLITERALFUNC,
234 getClassObject(rd.parent)),
235 rd.body, rd.locOpenBrace, typeDecl);
236 }
237 } else {
238 Assert.notFalse(rd.getTag() == TagConstants.CONSTRUCTORDECL);
239 trConstructorBody((ConstructorDecl)rd, premap);
240 }
241
242
243 // "code" now contains two marks followed by what ESCJ 16 calls "CS"
244 // (except for the "assume !isAllocated(objectToBeConstructed, alloc)",
245 // which has already been prepended to "code" here)
246 if (Main.options().traceInfo > 0 &&
247 (inlineParent != null || Main.options().traceInfo > 1)) {
248 // add a label to track the implicit return ("falling off the end
249 // of the routine")
250 int loc = rd.getEndLoc();
251 Assert.notFalse(loc != Location.NULL);
252 GuardedCmd g = traceInfoLabelCmd(loc, loc, "ImplicitReturn", loc);
253 code.addElement(g);
254 }
255 code.addElement(GC.gets(GC.ecvar, GC.ec_return));
256 code.addElement(GC.trycmd(GC.seq(GuardedCmdVec.popFromStackVector(code)),
257 GC.skip()));
258 if (rd.getTag() == TagConstants.CONSTRUCTORDECL) {
259 code.addElement(GC.gets(GC.resultvar, GC.thisvar));
260 }
261 GuardedCmd body = spill();
262 // "code" is now empty:
263 Assert.notFalse(code.vectors()==1 && code.size()==0);
264
265 // Finally, if there are any formal parameters, wrap "body" in a
266 // statement that saves and restores the values of the formal parameters
267 GuardedCmd res;
268 if (rd.args.size() == 0) {
269 res = body;
270 }
271 else {
272
273 declaredLocals.push(); // this mark popped by "popDeclBlock"
274 code.push(); // this mark popped by "popDeclBlock"
275
276 VariableAccess[] ppp = new VariableAccess[rd.args.size() * 2];
277 for (int i = 0; i < rd.args.size(); i++) {
278 FormalParaDecl arg = rd.args.elementAt(i);
279 VariableAccess va = (VariableAccess)paramMap.get(arg);
280 declaredLocals.addElement(va.decl);
281 ppp[2*i] = TrAnExpr.makeVarAccess(arg, Location.NULL);
282 ppp[2*i+1] = va;
283 }
284 for (int i = 0; i < ppp.length; i += 2) {
285 code.addElement(GC.gets(ppp[i+1], ppp[i]));
286 }
287 code.addElement(body);
288 for (int i = 0; i < ppp.length; i += 2) {
289 code.addElement(GC.restoreFrom(ppp[i], ppp[i+1]));
290 }
291 res = popDeclBlock();
292 }
293 //TrAnExpr.translate = null;
294 // Don't turn the above off because at present helper methods
295 // are inlined in which case this method is called recursively.
296 return res;
297 }
298
299 /**
300 * @return <code>true</code> when <code>rd</code> is a constructor that does not
301 * call a sibling constructor.
302 */
303 private boolean isStandaloneConstructor(/*@ non_null */ RoutineDecl rd) {
304 if (!(rd instanceof ConstructorDecl)) {
305 return false;
306 }
307 ConstructorDecl cd = (ConstructorDecl)rd;
308 // From here on, return "true" unless there is a call to a sibling
309 // constructor.
310
311 if (cd.body == null || cd.body.getTag() != TagConstants.BLOCKSTMT) {
312 return true;
313 }
314 GenericBlockStmt body = (GenericBlockStmt)cd.body;
315
316 if (body.stmts.size() == 0) {
317 return true;
318 }
319 Stmt s0 = body.stmts.elementAt(0);
320
321 if (s0.getTag() != TagConstants.CONSTRUCTORINVOCATION) {
322 return true;
323 }
324 ConstructorInvocation ccall = (ConstructorInvocation)s0;
325
326 return ccall.decl.parent != cd.parent;
327 }
328
329 /**
330 * Auxiliary routine used by trBody to translate the body of a constructor, as
331 * described in ESCJ 16, section 8.
332 */
333 //@ requires cd.body != null;
334 private void trConstructorBody(/*@ non_null */ ConstructorDecl cd,
335 Hashtable premap) {
336 // assume !isAllocated(objectToBeConstructed, alloc);
337 {
338 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED,
339 GC.objectTBCvar, GC.allocvar);
340 code.addElement(GC.assume(GC.not(isAllocated)));
341 }
342
343
344 if (cd.body == null) return;
345 // FIXME - not entirely sure we should omit everything
346 // from here on if there is no body.
347 /*
348 * Find the call to the superclass or sibling constructor, if
349 * any. In particular, set both "body" and "ccall" to
350 * non-"null" values if "cd.body" starts with a constructor
351 * call. ("ccall" is non-"null" only if "body" is, too.)
352 */
353 GenericBlockStmt body = null;
354 ConstructorInvocation ccall = null;
355 if (cd.body.getTag() == TagConstants.BLOCKSTMT) {
356 body = (GenericBlockStmt)cd.body;
357 if (1 <= body.stmts.size()) {
358 Stmt s0 = body.stmts.elementAt(0);
359 if (s0.getTag() == TagConstants.CONSTRUCTORINVOCATION) {
360 ccall = (ConstructorInvocation)s0;
361 }
362 }
363 }
364
365
366 if (ccall==null) {
367 /*
368 * Here "cd" refers to a constructor of class "Object"
369 * that does not call any sibling constructor.
370 *
371 * The code that used to be here can be found in revision
372 * 1.87 of this file (Translate.java); it is probably
373 * somewhat "rotted", though.
374 */
375 Assert.notFalse(Types.isSameType(TypeSig.getSig(cd.parent),
376 Types.javaLangObject()));
377 Assert.notImplemented("Checking of Object constructor body");
378 }
379
380
381 TypeDecl tdecl = cd.parent;
382 TypeSig type = TypeSig.getSig(tdecl);
383 try {
384 if (!type.isTopLevelType())
385 Inner.firstThis0 = Inner.getEnclosingInstanceArg(cd);
386
387 trConstructorCallStmt(ccall);
388 } finally {
389 Inner.firstThis0 = null;
390 }
391
392
393 // assume typeof(this) <: T
394 TypeExpr texpr = TypeExpr.make(tdecl.getStartLoc(),
395 tdecl.getEndLoc(),
396 type);
397 Expr goodType = GC.nary(TagConstants.TYPELE,
398 GC.nary(TagConstants.TYPEOF, GC.thisvar),
399 texpr);
400 code.addElement(GC.assume(goodType));
401
402 // assume objectToBeConstructed == this;
403 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ,
404 GC.objectTBCvar,
405 GC.thisvar)));
406
407 /*
408 * Insert this.this$0 = this$0arg if we are an inner-class constructor:
409 */
410 {
411 TypeSig T = TypeSig.getSig(cd.parent);
412 if (!T.isTopLevelType()) {
413 FieldDecl this0 = Inner.getEnclosingInstanceField(T);
414 FormalParaDecl this0arg = Inner.getEnclosingInstanceArg(cd);
415
416 code.addElement(GC.subgets(
417 TrAnExpr.makeVarAccess(this0, Location.NULL),
418 GC.thisvar,
419 TrAnExpr.makeVarAccess(this0arg, Location.NULL)));
420 }
421 }
422
423
424 if (ccall.decl.parent != cd.parent) {
425 // superclass (not sibling) constructor call:
426 instanceInitializers(cd.parent);
427 }
428
429 // call "trStmt" on the rest of the body:
430 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock"
431 code.push(); // this mark popped by "wrapUpDeclBlock"
432 for (int i = 1; i < body.stmts.size(); i++) {
433 trStmt(body.stmts.elementAt(i),cd.parent);
434 }
435 wrapUpDeclBlock();
436 }
437
438 private TypeExpr getClassObject(/*@ non_null */ TypeDecl tdClass) {
439 Type type = TypeSig.getSig(tdClass);
440 TypeExpr texpr = TypeExpr.make(tdClass.getStartLoc(), tdClass.getEndLoc(),
441 type);
442 return texpr;
443 }
444
445
446 /**
447 * This method implements "InstanceInitializers", as described in section 8.1 of
448 * ESCJ 16.
449 */
450 private void instanceInitializers(/*@ non_null */ TypeDecl tdecl) {
451 // First, provide zero-equivalent values for fields in first-inherited
452 // interfaces
453 if (tdecl instanceof ClassDecl) {
454 Enumeration interfaces = GetSpec.getFirstInheritedInterfaces((ClassDecl)tdecl);
455 while (interfaces.hasMoreElements()) {
456 TypeDecl tdSuperInterface = (TypeDecl)interfaces.nextElement();
457 instanceInitializeZero(tdSuperInterface);
458 }
459 }
460 // Then, provide zero-equivalent values for fields in "tdecl"
461 instanceInitializeZero(tdecl);
462
463 // Finally, compute the programmer-supplied initial values and assign
464 // the fields appropriately. (Note, first-inherited interfaces don't
465 // have programmer-supplied initial values for instance fields, since
466 // the only instance fields in interfaces are ghost fields and they
467 // don't have initial values.)
468 for (int i = 0; i < tdecl.elems.size(); i++) {
469 TypeDeclElem tde = tdecl.elems.elementAt(i);
470 if (tde instanceof ModelDeclPragma) continue;
471 if (tde instanceof GhostDeclPragma)
472 tde = ((GhostDeclPragma)tde).decl;
473
474 if (tde.getTag() == TagConstants.INITBLOCK) {
475 InitBlock ib = (InitBlock)tde;
476 if (!Modifiers.isStatic(ib.modifiers)) {
477 trStmt(ib.block,tdecl);
478 }
479 } else if (tde.getTag() == TagConstants.FIELDDECL) {
480 FieldDecl fd = (FieldDecl)tde;
481 if (!Modifiers.isStatic(fd.modifiers) && fd.init != null) {
482 Assert.notFalse(fd.locAssignOp != Location.NULL);
483 // e= Expr[[ fd.init ]]
484 Expr e = ptrExpr(fd.init);
485 // WriteCheck[[ f[this], e ]]
486 VariableAccess f = TrAnExpr.makeVarAccess(fd, Location.NULL);
487 Expr lhs = GC.select(f, GC.thisvar);
488 writeCheck(lhs, fd.init, e, fd.locAssignOp, true);
489 // f[this] = e
490 code.addElement(GC.subgets(f, GC.thisvar, e));
491 }
492 }
493 }
494 }
495
496 /**
497 * Called by <code>instanceInitializers</code>.
498 */
499 private void instanceInitializeZero(/*@ non_null */ TypeDecl tdecl) {
500 for (int i = 0; i < tdecl.elems.size(); i++) {
501 TypeDeclElem tde = tdecl.elems.elementAt(i);
502 if (tde instanceof ModelDeclPragma) continue;
503 if (tde instanceof GhostDeclPragma)
504 tde = ((GhostDeclPragma)tde).decl;
505
506 if (tde.getTag() == TagConstants.FIELDDECL) {
507 FieldDecl fd = (FieldDecl)tde;
508 if (!Modifiers.isStatic(fd.modifiers)) {
509 // f[this] = <default value>
510 VariableAccess fdref = TrAnExpr.makeVarAccess(fd, Location.NULL);
511 Expr defaultValue = null;
512 switch (fd.type.getTag()) {
513 case TagConstants.BOOLEANTYPE:
514 defaultValue = GC.falselit;
515 break;
516
517 case TagConstants.BIGINTTYPE:
518 case TagConstants.INTTYPE:
519 case TagConstants.LONGTYPE:
520 case TagConstants.CHARTYPE:
521 case TagConstants.BYTETYPE:
522 case TagConstants.SHORTTYPE:
523 defaultValue = GC.zerolit;
524 break;
525
526 case TagConstants.ARRAYTYPE:
527 case TagConstants.TYPENAME:
528 case TagConstants.TYPESIG:
529 if (GetSpec.NonNullPragma(fd) != null) {
530 defaultValue = temporary(fd.id.toString() + "@zero",
531 fd.getStartLoc());
532 } else {
533 defaultValue = GC.nulllit;
534 }
535 break;
536
537 case TagConstants.DOUBLETYPE:
538 case TagConstants.FLOATTYPE:
539 defaultValue = GC.nary(TagConstants.CAST, GC.zerolit,
540 GC.typeExpr(fd.type));
541 break;
542
543 case TagConstants.TYPECODE:
544 // TYPE fields have no default value:
545 defaultValue = temporary(fd.id.toString() + "@zero",
546 fd.getStartLoc());
547 break;
548
549 case TagConstants.NULLTYPE:
550 default:
551 /*@ unreachable ;*/
552 Assert.fail("Unexpected type tag " + TagConstants.toString(fd.type.getTag()));
553 break;
554 }
555 if (defaultValue != null)
556 code.addElement(GC.subgets(fdref, GC.thisvar, defaultValue));
557 }
558 }
559 }
560 }
561
562 //// Instance variables
563
564 /** References the routine currently being checked by trBody. */
565
566 private RoutineDecl rdCurrent;
567
568 /**
569 * Singly-linked list of the inline parents. Is <code>null</code> if this
570 * translation is not being inlined.
571 */
572 private Translate inlineParent;
573
574 /**
575 * Indicates whether to issue cautions. Value is set from outer call to trBody
576 * and also used by nested/recursive calls.
577 */
578 private boolean issueCautions;
579
580 /**
581 * Indicates whether or not the current routine is in a "constructor context",
582 * meaning that it is a constructor being checked or a method in the same class
583 * that's being inlined into the constructor.
584 */
585 private boolean inConstructorContext;
586
587 /**
588 * Contains the guarded commands generated so far for the current method. As the
589 * translation enters into Java blocks, <code>code</code> gets pushed. As blocks
590 * are left, <code>code</code> is poped into a <code>GuardedCmdVec</code> which
591 * is wrapped inside a BLOCK guarded command that gets appended onto
592 * <code>code</code>.
593 */
594 /*@ spec_public */ private final StackVector code = new StackVector();
595
596 /**
597 * List of loop invariant pragmas seen so far (and not yet used) within the
598 * current method.
599 */
600 private ExprStmtPragmaVec loopinvariants = ExprStmtPragmaVec.make();
601
602 /**
603 * List of loop decreases pragmas seen so far (and not yet used) within the
604 * current method.
605 */
606
607 private /*@ non_null */ ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make();
608
609 private /*@ non_null */ ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make();
610
611 protected /*@ non_null */ LocalVarDeclVec skolemConstants = LocalVarDeclVec.make();
612
613 /**
614 * Contains the local Java variables declared in the current <em>block</em> so
615 * far for the current block and enclosing blocks of the current method. This
616 * variable is maintained parallel to <code>code</code>: Each time a Java block
617 * is entered, <code>declaredLocals</code> gets pushed; when a block is left,
618 * <code>declaredLocals</code> is popped into a <code>GenericVarDeclVec</code>
619 * that gets wrapped inside a BLOCK guarded command.
620 */
621 private final /*@ non_null */ StackVector declaredLocals = new StackVector();
622
623 /**
624 * Contains the temporaries that generated for the current method that haven't
625 * yet been declared in a VARINCMD.
626 */
627 private final /*@ non_null */ StackVector temporaries = new StackVector();
628
629
630 /** Describes the current scope. */
631
632 private FindContributors scope;
633
634 /**
635 * Describes the current predicted set of synTargs.
636 *
637 * <p> If non-null, then represents an <em>*upper*</em> bound on
638 * freeVars of the result of the current trBody(...) call.
639 */
640 private Set predictedSynTargs;
641
642 /**
643 * Describes what aspects of an inlined call to check and what
644 * aspects to either assert or simply ignore. A call
645 * (MethodInvocation, ConstructorInvocation, NewInstanceExpr) may
646 * map to an <code>InlineSettings</code> object in which the
647 * <code>nextInlineCheckDepth</code> and
648 * <code>nextInlineDepthPastCheck</code> fields are unused.
649 *
650 * <p> This variable is used only for some call-site specific
651 * inlining, in particular, currently only to handle the
652 * -inlineConstructors flag. Other reasons for inlining are taken
653 * care of in method <code>computeInlineSettings</code>. </p>
654 */
655 public static final /*@ non_null */ ASTDecoration inlineDecoration =
656 new ASTDecoration("inlineDecoration");
657
658
659 //// Generation of variables to put into guarded commands
660
661 /**
662 * Pops temporaries and code, and makes these into a VARINCMD command that is
663 * returned. If there are no temporaries, only the code is returned.
664 */
665 private GuardedCmd spill() {
666 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
667 GenericVarDeclVec temps = GenericVarDeclVec.popFromStackVector(temporaries);
668 return GC.block(temps, body);
669 }
670
671
672 /**
673 * Make a fresh version of a special variable to save it in.
674 *
675 * (This partially handles ESCJ 23b, case 4.)
676 */
677 //@ requires (* v accesses a special variable. *);
678 private VariableAccess adorn(VariableAccess v) {
679 Assert.precondition(v.decl.locId == UniqName.specialVariable);
680
681 VariableAccess result= GC.makeVar(v.decl.id, v.decl.locId);
682 result.loc= v.getStartLoc();
683
684 temporaries.addElement(result.decl);
685 return result;
686 }
687
688
689 /**
690 * Make a fresh "boolean" variable to hold the initialized status
691 * of a Java variable that is marked as "uninitialized".
692 *
693 * (This partially handles ESCJ 23b, case 13.)
694 */
695 //@ requires (* v accesses a normal Java variable. *);
696 private VariableAccess initadorn(/*@ non_null */ LocalVarDecl d) {
697 Identifier idn = Identifier.intern(d.id + "@init");
698
699 VariableAccess result = GC.makeVar(idn, d.locId);
700 result.loc = Location.NULL;
701
702 return result;
703 }
704
705
706 //// Statement translation
707
708 // Utility routines
709
710 private boolean isRecursiveInvocation(/*@ non_null */ RoutineDecl r) {
711 Translate t = this;
712 while (t != null) {
713 if (t.rdCurrent == r) {
714 return true; // the routine has been visited before
715 }
716 t = t.inlineParent;
717 }
718 return false;
719 }
720
721 /** Reduces number of stack marks by 1. */
722
723 private GuardedCmd opBlockCmd(Expr label) {
724 GuardedCmd g= GC.seq(GuardedCmdVec.popFromStackVector(code));
725 GuardedCmd ifc= GC.ifcmd(GC.nary(TagConstants.ANYEQ, GC.ecvar, label),
726 GC.skip(), GC.raise());
727 return GC.trycmd(g, ifc);
728 }
729
730 private Expr breakLabel(Stmt s) {return GC.symlit(s, "L_");}
731 private Expr continueLabel(Stmt s) {return GC.symlit(s, "C_");}
732
733 /**
734 * Emits the commands <code>EC= label; raise</code> to <code>code</code>.
735 */
736 private void raise(Expr label) {
737 code.addElement(GC.gets(GC.ecvar, label));
738 code.addElement(GC.raise());
739 }
740
741 /**
742 * Computes purity information for Java expression <code>e</code>, translates
743 * <code>e</code> (emitting any code needed to account for impurities or side
744 * effects in the expression), and emits code that performs a <code>RAISE
745 * label</code> command if the expression evaluates to <code>false</code>. As
746 * usual, emitted code is appended to <code>code</code> and temporaries are
747 * appended to <code>temporaries</code>.
748 */
749 private void guard(Expr e, Expr label) {
750 Expr grd = ptrExpr(e);
751 code.push(); // popped off by boxPopFromStackVector
752 code.addElement(GC.assume(grd));
753 code.addElement(GC.skip());
754 code.push(); // popped off by boxPopFromStackVector
755 code.addElement(GC.assumeNegation(grd));
756 raise(label);
757 GuardedCmd ifc= GC.boxPopFromStackVector(code);
758 code.addElement(ifc);
759 }
760
761 /**
762 * Appends to <code>code</code> commands that make up a loop with nominal body
763 * <code>guard;body</code>, where <code>label</code> is raised within
764 * <code>body</code> to terminate the loop. The vector <code>J</code> contains
765 * the user-declared loop invariant pragmas. The vector <code>decreases</code>
766 * contains the user-declared bound function pragmas. The scope of the variables
767 * in <code>tempVars</code> is the nominal body; this method will wrap an
768 * appropriate <code>var .. in .. end</code> command around these.
769 */
770 private void makeLoop(int sLoop, int eLoop, int locHotspot,
771 GenericVarDeclVec tempVars,
772 GuardedCmd guard,
773 GuardedCmd body,
774 /*@ non_null */ ExprStmtPragmaVec J,
775 ExprStmtPragmaVec decreases,
776 LocalVarDeclVec skolemConsts,
777 /*@ non_null */ ExprStmtPragmaVec P,
778 Expr label) {
779
780 code.push(); // this mark popped by "opBlockCmd"
781
782 // construct old variants of the variables that are targets of the loop.
783 code.push();
784 temporaries.push();
785 GuardedCmd S = GC.seq(guard, body);
786 Set normalTargets = Targets.normal(GC.block(tempVars, S));
787 Hashtable h = GetSpec.makeSubst(normalTargets.elements(), "loopold");
788
789 for (Enumeration keys = h.keys(); keys.hasMoreElements(); ) {
790 GenericVarDecl vd = (GenericVarDecl) keys.nextElement();
791 VariableAccess va = (VariableAccess) h.get(vd);
792 temporaries.addElement(va.decl);
793 code.addElement(GC.assume(GC.nary(TagConstants.ANYEQ,
794 VariableAccess.make(vd.id, sLoop, vd), va)));
795 }
796
797
798 ExprVec ev = ExprVec.make(10);
799
800 ConditionVec invs = ConditionVec.make();
801 for (int i = 0; i < J.size(); i++) {
802 TrAnExpr.initForClause();
803 ExprStmtPragma loopinv = J.elementAt(i);
804 Expr pred = TrAnExpr.trSpecExpr(loopinv.expr, null, h); // FIXME - what about formal params in old?
805 Condition cond = GC.condition(TagConstants.CHKLOOPINVARIANT,
806 pred,
807 loopinv.getStartLoc());
808 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
809 invs.addElement(cond);
810 }
811
812 DecreasesInfoVec decs = DecreasesInfoVec.make();
813 for (int i = 0; i < decreases.size(); i++) {
814 ExprStmtPragma d = decreases.elementAt(i);
815 TrAnExpr.initForClause();
816 Expr de = TrAnExpr.trSpecExpr(d.expr); // FIXME - what about old?
817 int startLoc = d.getStartLoc();
818 VariableAccess fOld = temporary("decreases", startLoc, startLoc);
819 DecreasesInfo di = DecreasesInfo.make(startLoc, d.getEndLoc(), de, fOld);
820 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
821 decs.addElement(di);
822 }
823
824 ExprVec preds = ExprVec.make();
825 for (int i = 0; i < P.size(); i++) {
826 ExprStmtPragma looppred = P.elementAt(i);
827 Expr e = TrAnExpr.trSpecExpr(looppred.expr, null, h); // FIXME - what about params?
828 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
829 preds.addElement(e);
830 }
831
832 // If we ever implement the "safe" (as opposed to "fast") version of
833 // loops, then "invs" should be extended with loop object invariant
834 // conditions, and "guard" should be prefixed by a sequence of
835 // TargetTypeCorrect assume commands, per ESCJ 16.
836
837 LoopCmd loop = GC.loop(sLoop, eLoop, locHotspot, h,
838 invs, decs, skolemConsts, preds,
839 tempVars, guard, body);
840 switch (Main.options().loopTranslation) {
841 case Options.LOOP_FAST:
842 case Options.LOOP_FALL_THRU:
843 desugarLoopFast(loop,ev);
844 break;
845
846 case Options.LOOP_SAFE:
847 desugarLoopSafe(loop,ev);
848 break;
849
850 default:
851 Assert.fail("unexpected loop translation scheme: " +
852 Main.options().loopTranslation);
853 }
854
855 code.addElement(loop);
856
857 code.addElement(spill());
858
859 code.addElement(opBlockCmd(label));
860 }
861
862 /**
863 * Desugars <code>loop</code> according to the fast option. In particular, sets
864 * <code>loop.desugared</code> to the desugaring.
865 */
866 private void desugarLoopFast(LoopCmd loop, ExprVec axs) {
867 // A fast-desugared loop has the shape:
868 // var V in J;B;S;J;B;S;J;..;fail end
869 // where "V" is the list of temporary variables used within the
870 // loop, "J" is the command that checks loop invariants, "B" is
871 // the guard command, and "S" is the rest of the body of the
872 // loop.
873 //
874 // The number of repetitions of "J;B;S" is determined by
875 // "Main.loopUnrollCount". After these repetitions is another
876 // "J", and if "Main.loopUnrollHalf" is "true", then there is
877 // then one more "B". As shown above, the sequence ends with
878 // a "fail" command.
879 //
880 // If "Main.traceInfo" is positive, then each "J" is immediately
881 // preceded by a command of the form:
882 // assume (lblpos trace.LoopIter^L#i true)
883 // where "L" is the source location of the loop and "i" is the
884 // iteration count.
885
886 // Build a command that checks loop invariants
887 code.push(); // this mark popped below
888 checkLoopInvariants(loop,axs);
889 GuardedCmd J = GC.seq(GuardedCmdVec.popFromStackVector(code));
890
891 code.push(); // this mark popped below after for loop
892
893 String locString = UniqName.locToSuffix(loop.getStartLoc()) + "#";
894
895 int numOfComponents = 3 * Main.options().loopUnrollCount +
896 (Main.options().loopUnrollHalf ? 2 : 1);
897 int iComp = 0;
898 int i = 0;
899 for ( ; true; i++) {
900 code.push(); // this mark popped below
901
902 // -- J --
903 Assert.notFalse(iComp != numOfComponents);
904 if (Main.options().traceInfo > 0) {
905 String label = locString + i;
906 code.addElement(traceInfoLabelCmd(loop.getStartLoc(),
907 loop.getEndLoc(),
908 "LoopIter", label));
909 }
910 code.addElement(J);
911 iComp++;
912 if (iComp == numOfComponents) {
913 break;
914 }
915 // -- B --
916 addLoopDecreases(loop, 0); // fOld = F;
917 GuardedCmd B = loop.guard;
918 if (Main.options().traceInfo > 0 && 0 < i) {
919 B = cloneGuardedCommand(B);
920 }
921 code.addElement(B);
922 iComp++;
923 if (iComp == numOfComponents) {
924 break;
925 }
926 // -- S --
927 GuardedCmd S = loop.body;
928 if (Main.options().traceInfo > 0 && 0 < i) {
929 S = cloneGuardedCommand(S);
930 }
931 code.addElement(S);
932 addNewAssumptionsNow(axs);
933 addLoopDecreases(loop, 1); // check 0 <= fOld;
934 addLoopDecreases(loop, 2); // check F < fOld;
935 iComp++;
936
937 GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars);
938 code.addElement(iter);
939
940 Assert.notFalse(iComp != numOfComponents);
941 }
942
943 // pop once more to get J or J;B as the case might be
944 GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars);
945 code.addElement(iter);
946
947 // Stop unrolling here
948 if (Main.options().loopTranslation != Options.LOOP_FALL_THRU) {
949 code.addElement(GC.fail());
950 }
951
952 loop.desugared = GC.seq(GuardedCmdVec.popFromStackVector(code));
953 }
954
955 //@ requires 0 <= iteration;
956 private GuardedCmd wrapUpUnrolledIteration(/*@ non_null */ String locString,
957 int iteration,
958 /*@ non_null */ GenericVarDeclVec tempVars) {
959 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
960 body = GC.block(tempVars, body);
961 GuardedCmd iter = DynInstCmd.make(locString + iteration, body);
962 return iter;
963 }
964
965 /**
966 * Adds to <code>code</code> the various pieces of the translation of the
967 * decreases pragma. The pieces are:
968 * <ul>
969 * <li> 0. fOld = F;
970 * <li> 1. check 0 <= fOld;
971 * <li> 2. check F < fOld;
972 * </ul>
973 */
974 //@ requires 0 <= piece && piece < 3;
975 //@ modifies code.elementCount;
976 private void addLoopDecreases(/*@ non_null */ LoopCmd loop,
977 int piece) {
978 for (int i = 0; i < loop.decreases.size(); i++) {
979 DecreasesInfo di = loop.decreases.elementAt(i);
980 switch (piece) {
981 case 0: // fOld = F;
982 code.addElement(GC.gets(di.fOld, di.f));
983 break;
984 case 1: // check 0 <= fOld;
985 addCheck(loop.locHotspot, TagConstants.CHKDECREASES_BOUND,
986 GC.nary(TagConstants.INTEGRALLE, GC.zerolit, di.fOld),
987 di.locStart);
988 break;
989 case 2: // check F < fOld;
990 addCheck(loop.locHotspot, TagConstants.CHKDECREASES_DECR,
991 GC.nary(TagConstants.INTEGRALLT, di.f, di.fOld),
992 di.locStart);
993 break;
994 default:
995 //@ unreachable;
996 Assert.fail("addLoopDecreases: unexpected piece number");
997 break;
998 }
999 }
1000 }
1001
1002
1003 /**
1004 * targets is set of GenericVarDecls. aTargets is set of ATargets.
1005 */
1006 public GuardedCmd modifyATargets(/*@ non_null */ Set aTargets, int loc) {
1007 code.push();
1008 for (Enumeration e = aTargets.elements(); e.hasMoreElements();) {
1009 ATarget at = (ATarget)e.nextElement();
1010 VariableAccess va = VariableAccess.make(at.x.id, loc, at.x);
1011
1012 if (at.indices.length == 0 ||
1013 (at.indices[0] == null &&
1014 (at.indices.length == 1 || at.indices[1] == null))) {
1015 // x, x[*], x[*][*]
1016 // System.out.println("x = " + at.x.id.toString() +
1017 // ", at.indices.length = " + at.indices.length);
1018 code.addElement(modify(va, loc));
1019 } else if (at.indices.length == 1) {
1020 // x[e]
1021 VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1022 code.addElement(GC.subgets(va, at.indices[0], newVal));
1023 } else if (at.indices[0] == null) {
1024 // x[*][e]
1025 VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1026 VariableAccess var1 = GC.makeVar("i", loc);
1027 VariableAccess var2 = GC.makeVar("j", loc);
1028
1029 Expr a = GC.implies(GC.nary(TagConstants.ANYNE, var2, at.indices[1]),
1030 GC.nary(TagConstants.ANYEQ,
1031 GC.select(GC.select(va, var1), var2),
1032 GC.select(GC.select(newVal, var1), var2)));
1033 code.addElement(GC.assume(GC.forall(var1.decl,GC.forall(var2.decl, a ))));
1034 code.addElement(GC.gets(va, newVal));
1035 } else if (at.indices[1] == null) {
1036 // x[e][*]
1037 VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1038 VariableAccess var1 = GC.makeVar("i", loc);
1039 VariableAccess var2 = GC.makeVar("j", loc);
1040
1041 Expr a = GC.implies(GC.and( GC.nary(TagConstants.ANYNE, var1, at.indices[0]),
1042 GC.nary(TagConstants.IS, var2, TrAnExpr.trType(Types.intType))),
1043 GC.nary(TagConstants.ANYEQ,
1044 GC.select(GC.select(va, var1), var2),
1045 GC.select(GC.select(newVal, var1), var2)));
1046 code.addElement(GC.assume(GC.forall(var1.decl, GC.forall(var2.decl, a))));
1047 code.addElement(GC.gets(va, newVal));
1048 } else {
1049 // x[e][e]
1050 VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1051 code.addElement(GC.subsubgets(va, at.indices[0], at.indices[1], newVal));
1052 }
1053 }
1054
1055 return GC.seq(GuardedCmdVec.popFromStackVector(code));
1056 }
1057
1058 public GuardedCmd modify(/*@ non_null */ Set simpleTargets, int loc) {
1059 code.push();
1060 for (Enumeration e = simpleTargets.elements(); e.hasMoreElements();) {
1061 GenericVarDecl at = (GenericVarDecl)e.nextElement();
1062 VariableAccess va = VariableAccess.make(at.id, loc, at);
1063 code.addElement(modify(va, loc));
1064 }
1065
1066 return GC.seq(GuardedCmdVec.popFromStackVector(code));
1067 }
1068
1069 /**
1070 * Desugars <code>loop</code> according to the safe option. In particular, sets
1071 * <code>loop.desugared</code> to the desugaring.
1072 */
1073 public void desugarLoopSafe(LoopCmd loop, ExprVec axs) {
1074 // Build a command that checks loop invariants safely
1075
1076 code.push(); // this mark popped below
1077 checkLoopInvariants(loop,axs);
1078 code.addElement(GC.fail());
1079 GuardedCmd checkInvariantsInitially =
1080 GC.seq(GuardedCmdVec.popFromStackVector(code));
1081
1082 code.push(); // this mark popped shortly
1083 addLoopDecreases(loop, 0); // fOld = F;
1084 code.addElement(loop.guard);
1085 code.addElement(loop.body);
1086 addNewAssumptionsNow(axs);
1087 addLoopDecreases(loop, 1); // check 0 <= fOld;
1088 addLoopDecreases(loop, 2); // check F < fOld;
1089 GuardedCmd S = GC.seq(GuardedCmdVec.popFromStackVector(code));
1090
1091 Set vds = Targets.normal(GC.block(loop.tempVars, S));
1092 GuardedCmd modifyGc = modify(vds, loop.locStart);
1093
1094 if( Main.options().preciseTargets ) {
1095 Set aTargets = ATarget.compute( GC.block(loop.tempVars, loop ));
1096 modifyGc = modifyATargets( aTargets, S.getStartLoc());
1097 }
1098
1099 code.push(); // this mark popped below
1100 code.addElement(modifyGc);
1101
1102 for (Enumeration e = vds.elements(); e.hasMoreElements();) {
1103 GenericVarDecl vd = (GenericVarDecl)e.nextElement();
1104
1105 if (!vd.id.toString().endsWith("@init")) {
1106 code.addElement(GC.assume(TrAnExpr.targetTypeCorrect(vd, loop.oldmap)));
1107 }
1108 }
1109 addNewAssumptionsNow(axs);
1110 for (int i = 0; i < loop.invariants.size(); i++) {
1111 Condition cond = loop.invariants.elementAt(i);
1112 code.addElement(GC.assume(cond.pred));
1113 }
1114
1115 if (Main.options().traceInfo > 0) {
1116 String label = UniqName.locToSuffix(loop.getStartLoc());
1117 code.addElement(traceInfoLabelCmd(loop, "LoopIter"));
1118 }
1119
1120 code.addElement(DynInstCmd.make(UniqName.locToSuffix(loop.getStartLoc()), S));
1121
1122 checkLoopInvariants(loop,axs);
1123 code.addElement(GC.fail());
1124 GuardedCmd checkInvariantsAfterIteration =
1125 GC.seq(GuardedCmdVec.popFromStackVector(code));
1126
1127 loop.desugared = GC.choosecmd(checkInvariantsInitially,
1128 checkInvariantsAfterIteration);
1129 }
1130
1131 /**
1132 * Add to "code" checks for all loop invariants of "loop".
1133 */
1134 private void checkLoopInvariants(/*@ non_null */ LoopCmd loop, ExprVec axs) {
1135 addNewAssumptionsNow(axs);
1136 for (int i = 0; i < loop.invariants.size(); i++) {
1137 Condition cond = loop.invariants.elementAt(i);
1138 addCheck(loop.locHotspot, cond);
1139 }
1140 }
1141
1142 //@ requires Main.options().traceInfo > 0;
1143 private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast,
1144 /*@ non_null */ String traceInfoTag) {
1145 int sloc = ast.getStartLoc();
1146 int eloc = ast.getEndLoc();
1147 return traceInfoLabelCmd(sloc, eloc, traceInfoTag, sloc);
1148 }
1149
1150 //@ requires Main.options().traceInfo > 0;
1151 //@ requires loc != Location.NULL;
1152 private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast,
1153 /*@ non_null */ String traceInfoTag,
1154 int loc) {
1155 return traceInfoLabelCmd(ast.getStartLoc(), ast.getEndLoc(),
1156 traceInfoTag, loc);
1157 }
1158
1159 //@ requires Main.options().traceInfo > 0;
1160 //@ requires loc != Location.NULL;
1161 private GuardedCmd traceInfoLabelCmd(int sloc, int eloc,
1162 /*@ non_null */ String traceInfoTag,
1163 int loc) {
1164 return traceInfoLabelCmd(sloc, eloc, traceInfoTag,
1165 UniqName.locToSuffix(loc));
1166 }
1167
1168
1169 private GuardedCmd traceInfoLabelCmd(int sloc, int eloc,
1170 /*@ non_null */ String traceInfoTag,
1171 String sortSeq) {
1172 Assert.notFalse(Main.options().traceInfo > 0);
1173
1174 String str = "trace." + traceInfoTag + "^" + sortSeq;
1175 Identifier id = Identifier.intern(str);
1176 Expr l = LabelExpr.make(sloc, eloc, true, id, GC.truelit);
1177 return GC.assume(l);
1178 }
1179
1180 /**
1181 * This method returns a guarded command <code>G</code> that is like
1182 * <code>gc</code> except that where <code>gc</code> contains a mutable command,
1183 * <code>G</code> contains a fresh copy of that command. Thus, the resulting
1184 * command is as good as a fresh copy of <code>gc</code>, since all other guarded
1185 * commands are to be read-only after construction.<p>
1186 *
1187 * There is only one mutable command, namely an "assume" command
1188 * of the form:
1189 * <pre>
1190 * assume (lblpos id true)
1191 * </pre>
1192 * where "id" is a trace label. A fresh copy of this command consists of a fresh
1193 * assume command with a fresh labeled expression. However, the "id" reference
1194 * may be shared in the fresh command.
1195 */
1196 private GuardedCmd cloneGuardedCommand(/*@ non_null */ GuardedCmd gc) {
1197 switch (gc.getTag()) {
1198 case TagConstants.SKIPCMD:
1199 case TagConstants.RAISECMD:
1200 case TagConstants.ASSERTCMD:
1201 case TagConstants.GETSCMD:
1202 case TagConstants.SUBGETSCMD:
1203 case TagConstants.SUBSUBGETSCMD:
1204 case TagConstants.RESTOREFROMCMD:
1205 return gc;
1206
1207 case TagConstants.ASSUMECMD: {
1208 ExprCmd ec = (ExprCmd)gc;
1209 if (ec.pred.getTag() == TagConstants.LABELEXPR) {
1210 LabelExpr le = (LabelExpr)ec.pred;
1211 if (le.positive && le.expr == GC.truelit) {
1212 String str = le.label.toString();
1213 if (ErrorMsg.isTraceLabel(str)) {
1214 return GC.assume(LabelExpr.make(le.sloc, le.eloc, true,
1215 le.label, GC.truelit));
1216 }
1217 }
1218 }
1219 return gc;
1220 }
1221
1222 case TagConstants.VARINCMD: {
1223 VarInCmd vc = (VarInCmd)gc;
1224 GuardedCmd body = cloneGuardedCommand(vc.g);
1225 if (body != vc.g) {
1226 return GC.block(vc.v, body);
1227 }
1228 return gc;
1229 }
1230
1231 case TagConstants.DYNINSTCMD: {
1232 DynInstCmd dc = (DynInstCmd)gc;
1233 GuardedCmd body = cloneGuardedCommand(dc.g);
1234 if (body != dc.g) {
1235 return DynInstCmd.make(dc.s, body);
1236 }
1237 return gc;
1238 }
1239
1240 case TagConstants.SEQCMD: {
1241 SeqCmd sc = (SeqCmd)gc;
1242 int len = sc.cmds.size();
1243 GuardedCmd[] cmds = null; // allocate this array lazily
1244 for (int i = 0; i < len; i++) {
1245 GuardedCmd c = sc.cmds.elementAt(i);
1246 GuardedCmd g = cloneGuardedCommand(c);
1247 if (g != c) {
1248 if (cmds == null) {
1249 cmds = new GuardedCmd[len];
1250 // all elements up until now have been the same
1251 for (int j = 0; j < i; j++) {
1252 cmds[j] = sc.cmds.elementAt(j);
1253 }
1254 }
1255 cmds[i] = g;
1256 } else if (cmds != null) {
1257 cmds[i] = g;
1258 }
1259 }
1260 if (cmds != null) {
1261 return GC.seq(GuardedCmdVec.make(cmds));
1262 }
1263 return gc;
1264 }
1265
1266 case TagConstants.CALL: {
1267 Call call = (Call)gc;
1268 GuardedCmd desugared = cloneGuardedCommand(call.desugared);
1269 if (desugared != call.desugared) {
1270 Call newCall = Call.make(call.args, call.scall, call.ecall,
1271 call.inlined);
1272 newCall.rd = call.rd;
1273 newCall.spec = call.spec;
1274 newCall.desugared = desugared;
1275 return newCall;
1276 }
1277 return gc;
1278 }
1279
1280 case TagConstants.TRYCMD: {
1281 CmdCmdCmd tc = (CmdCmdCmd)gc;
1282 GuardedCmd g1 = cloneGuardedCommand(tc.g1);
1283 GuardedCmd g2 = cloneGuardedCommand(tc.g2);
1284 if (g1 != tc.g1 || g2 != tc.g2) {
1285 return GC.trycmd(g1, g2);
1286 }
1287 return gc;
1288 }
1289
1290 case TagConstants.LOOPCMD: {
1291 LoopCmd lp = (LoopCmd)gc;
1292 GuardedCmd guard = cloneGuardedCommand(lp.guard);
1293 GuardedCmd body = cloneGuardedCommand(lp.body);
1294 LoopCmd newLoop = GC.loop(lp.locStart, lp.locEnd, lp.locHotspot, lp.oldmap,
1295 lp.invariants, lp.decreases,
1296 lp.skolemConstants, lp.predicates, lp.tempVars,
1297 guard, body);
1298 newLoop.desugared = cloneGuardedCommand(lp.desugared);
1299 // A desugared loop contains trace info labels, and thus:
1300 Assert.notFalse(newLoop.desugared != lp.desugared);
1301 return newLoop;
1302 }
1303
1304 case TagConstants.CHOOSECMD: {
1305 CmdCmdCmd cc = (CmdCmdCmd)gc;
1306 GuardedCmd g1 = cloneGuardedCommand(cc.g1);
1307 GuardedCmd g2 = cloneGuardedCommand(cc.g2);
1308 if (g1 != cc.g1 || g2 != cc.g2) {
1309 return GC.choosecmd(g1, g2);
1310 }
1311 return gc;
1312 }
1313
1314 default:
1315 //@ unreachable;
1316 Assert.notFalse(false);
1317 return null;
1318 }
1319 }
1320
1321 /**
1322 * Pops <code>declaredLocals</code> and <code>code</code> and then appends
1323 * <code>code</code> with a VARINCMD (if there were any new declared locals) or a
1324 * sequence of commands (otherwise). The new code becomes the body of the
1325 * VARINCMD or the sequence of commands.
1326 */
1327 private void wrapUpDeclBlock() {
1328 if (code.size() == 0) {
1329 declaredLocals.pop();
1330 code.pop();
1331 } else {
1332 if (declaredLocals.size() == 0) {
1333 declaredLocals.pop();
1334 code.merge();
1335 } else {
1336 code.addElement(popDeclBlock());
1337 }
1338 }
1339 }
1340
1341 /**
1342 * Pops the code and declared local variables, makes these into a command
1343 * (usually a VAR .. IN .. END command, but possibly a sequence command if there
1344 * are no declared local variables). The command is then returned.
1345 */
1346 private GuardedCmd popDeclBlock() {
1347 GuardedCmd body= GC.seq(GuardedCmdVec.popFromStackVector(code));
1348 // The following "if" statement seems to be a bug, because it
1349 // fails to pop "declaredLocals". Better would be not to even
1350 // check the "if", but to always pop from the stack vector, and
1351 // then let "GC.block" do the optimization. --KRML, 29 Sep 1999
1352 // Actually, popDeclBlock is not called with declaredLocals.size()==0
1353 if (declaredLocals.size() == 0)
1354 return body;
1355 GenericVarDeclVec locals
1356 = GenericVarDeclVec.popFromStackVector(declaredLocals);
1357 return GC.block(locals, body);
1358 }
1359
1360 /**
1361 * Translate <code>stmt</code> into a sequence of guarded commands
1362 * that are appended to <code>code</code>.
1363 *
1364 * <p> Temporaries generated for expressions in <code>stmt</code>
1365 * are added to <code>temporaries</code>, loop invariant pragmas are
1366 * added to <code>loopinvariants</code>, decreases pragmas are added
1367 * to <code>loopDecreases</code>, loop predicates are added to
1368 * <code>looppredicates<code>, and local skolemized variables are
1369 * added to <code>skolemConstants</code>. </p>
1370 *
1371 * @param stmt the statement that is to be translated.
1372 */
1373 //@ assignable loopinvariants, loopDecreases, skolemConstants, loopPredicates;
1374 private void trStmt(/*@ non_null */ Stmt stmt, TypeDecl decl) {
1375 int tag = stmt.getTag();
1376 switch (tag) {
1377
1378 case TagConstants.RETURNSTMT:
1379 {
1380 ReturnStmt r = (ReturnStmt)stmt;
1381 if (r.expr != null)
1382 code.addElement(GC.gets(GC.resultvar, ptrExpr(r.expr)));
1383 if (Main.options().traceInfo > 0) {
1384 // add a label to track the return
1385 GuardedCmd g = traceInfoLabelCmd(r, "Return", r.loc);
1386 code.addElement(g);
1387 }
1388 raise(GC.ec_return);
1389 return;
1390 }
1391
1392 case TagConstants.THROWSTMT:
1393 {
1394 ThrowStmt t = (ThrowStmt)stmt;
1395 code.addElement(GC.gets(GC.xresultvar, ptrExpr(t.expr)));
1396 nullCheck(t.expr, GC.xresultvar, t.getStartLoc());
1397 if (Main.options().traceInfo > 0) {
1398 // add a label to track the throw
1399 GuardedCmd g = traceInfoLabelCmd(t, "Throw", t.loc);
1400 code.addElement(g);
1401 }
1402 raise(GC.ec_throw);
1403 return;
1404 }
1405
1406 case TagConstants.SWITCHSTMT:
1407 {
1408 SwitchStmt c = (SwitchStmt)stmt;
1409 VariableAccess e = fresh(c.expr, c.expr.getStartLoc(), "switch");
1410 code.addElement( GC.gets( e, ptrExpr( c.expr )));
1411
1412 // we walk thru the switch body, building up the GC
1413 // at each case label, we wrap up the GC generated so far
1414 // on the lhs of a box, and put the new assume on the rhs.
1415
1416 code.push();
1417 code.addElement(GC.assume(GC.falselit));
1418
1419 for(int i=0; i<c.stmts.size(); i++) {
1420 Stmt s = c.stmts.elementAt(i);
1421
1422 if( s.getTag() != TagConstants.SWITCHLABEL ) {
1423 // just a regular statement
1424 trStmt( s , decl);
1425 } else {
1426
1427 SwitchLabel sl = (SwitchLabel)s;
1428
1429 GuardedCmdVec vec = GuardedCmdVec.popFromStackVector(code);
1430 GuardedCmd boxLhs = GC.block(GenericVarDeclVec.make(),
1431 GC.seq(vec));
1432
1433 Expr C;
1434 if( sl.expr != null ) {
1435
1436 C = GC.nary(s.getStartLoc(),s.getEndLoc(),
1437 TagConstants.INTEGRALEQ,
1438 e, TrAnExpr.trSpecExpr(sl.expr)); // FIXME -why a trSpecExpr?
1439 } else {
1440
1441 C = GC.truelit;
1442 for(int j=0; j<c.stmts.size(); j++) {
1443
1444 Stmt s2 = c.stmts.elementAt(j);
1445 if( s2.getTag() == TagConstants.SWITCHLABEL ) {
1446
1447 SwitchLabel sl2 = (SwitchLabel)s2;
1448
1449 if( sl2.expr != null )
1450 C = GC.and(s.getStartLoc(),s.getEndLoc(),
1451 C,
1452 GC.nary(s.getStartLoc(),s.getEndLoc(),
1453 TagConstants.INTEGRALNE,
1454 e, TrAnExpr.trSpecExpr(sl2.expr))); // FIXME - why a specExpr
1455 }
1456 }
1457 }
1458
1459 GuardedCmd boxRhs = GC.assume(C);
1460 if (Main.options().traceInfo > 0) {
1461 // add a label to track the switch branch taken
1462 GuardedCmd g = traceInfoLabelCmd(s, "Switch");
1463 boxRhs = GC.seq(g, boxRhs);
1464 }
1465 GuardedCmd box = GC.choosecmd(boxLhs, boxRhs);
1466
1467 code.push();
1468 code.addElement(box);
1469
1470 }
1471 }
1472
1473 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
1474 GuardedCmd block = GC.blockL(c, body);
1475 code.addElement(block);
1476
1477 return;
1478 }
1479
1480 case TagConstants.BLOCKSTMT:
1481 {
1482 GenericBlockStmt b = (GenericBlockStmt)stmt;
1483 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock"
1484 code.push(); // this mark popped by "wrapUpDeclBlock"
1485
1486 for (int i= 0; i < b.stmts.size(); i++)
1487 trStmt(b.stmts.elementAt(i),decl);
1488
1489 wrapUpDeclBlock();
1490 return;
1491 }
1492
1493 case TagConstants.WHILESTMT:
1494 {
1495 WhileStmt w = (WhileStmt)stmt;
1496 Expr bLabel = breakLabel(w);
1497
1498 temporaries.push(); // this mark popped below
1499
1500 code.push(); // this mark popped below
1501 guard(w.expr, bLabel);
1502 GuardedCmd guardCmd =
1503 GC.seq(GuardedCmdVec.popFromStackVector(code));
1504
1505 ExprStmtPragmaVec invariants = loopinvariants;
1506 loopinvariants = ExprStmtPragmaVec.make();
1507 ExprStmtPragmaVec decreases = loopDecreases;
1508 loopDecreases = ExprStmtPragmaVec.make();
1509 ExprStmtPragmaVec predicates = loopPredicates;
1510 loopPredicates = ExprStmtPragmaVec.make();
1511 LocalVarDeclVec skolemConsts = skolemConstants;
1512 skolemConstants = LocalVarDeclVec.make();
1513
1514 code.push(); // this mark popped by "opBlockCmd"
1515 trStmt(w.stmt,decl);
1516 GuardedCmd bodyCmd = opBlockCmd(continueLabel(w));
1517
1518 makeLoop(w.getStartLoc(), w.getEndLoc(), w.locGuardOpenParen,
1519 GenericVarDeclVec.popFromStackVector(temporaries),
1520 guardCmd, bodyCmd, invariants, decreases,
1521 skolemConsts, predicates, bLabel);
1522
1523 return;
1524 }
1525
1526 case TagConstants.DOSTMT:
1527 {
1528 DoStmt d = (DoStmt)stmt;
1529 Expr bLabel = breakLabel(d);
1530
1531 // the following 3 marks are popped below
1532 temporaries.push();
1533 code.push();
1534
1535 ExprStmtPragmaVec invariants = loopinvariants;
1536 loopinvariants = ExprStmtPragmaVec.make();
1537 ExprStmtPragmaVec decreases = loopDecreases;
1538 loopDecreases = ExprStmtPragmaVec.make();
1539 ExprStmtPragmaVec predicates = loopPredicates;
1540 loopPredicates = ExprStmtPragmaVec.make();
1541 LocalVarDeclVec skolemConsts = skolemConstants;
1542 skolemConstants = LocalVarDeclVec.make();
1543
1544 code.push(); // this mark popped by "opBlockCmd"
1545 trStmt(d.stmt,decl);
1546 code.addElement(opBlockCmd(continueLabel(d)));
1547
1548 guard(d.expr, bLabel);
1549
1550 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
1551
1552 makeLoop(d.getStartLoc(), d.getEndLoc(), d.loc,
1553 GenericVarDeclVec.popFromStackVector(temporaries),
1554 GC.skip(), body, invariants, decreases,
1555 skolemConsts, predicates, bLabel);
1556 return;
1557 }
1558
1559 case TagConstants.FORSTMT:
1560 {
1561 ForStmt x = (ForStmt)stmt;
1562
1563 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock"
1564 code.push(); // this mark popped by "wrapUpDeclBlock"
1565
1566 // initializers
1567 for (int i= 0; i < x.forInit.size(); i++)
1568 trStmt(x.forInit.elementAt(i),decl);
1569
1570 Expr bLabel = breakLabel(x);
1571
1572 temporaries.push(); // this mark popped below
1573
1574 ExprStmtPragmaVec invariants = loopinvariants;
1575 loopinvariants = ExprStmtPragmaVec.make();
1576 ExprStmtPragmaVec decreases = loopDecreases;
1577 loopDecreases = ExprStmtPragmaVec.make();
1578 ExprStmtPragmaVec predicates = loopPredicates;
1579 loopPredicates = ExprStmtPragmaVec.make();
1580 LocalVarDeclVec skolemConsts = skolemConstants;
1581 skolemConstants = LocalVarDeclVec.make();
1582
1583 code.push(); // this mark popped below
1584 guard(x.test, bLabel);
1585 GuardedCmd guardCmd =
1586 GC.seq(GuardedCmdVec.popFromStackVector(code));
1587
1588 code.push(); // this mark popped below
1589
1590 code.push(); // this mark popped by "opBlockCmd"
1591 trStmt(x.body,decl);
1592 code.addElement(opBlockCmd(continueLabel(x)));
1593
1594 for(int i=0; i < x.forUpdate.size(); i++)
1595 ptrExpr(x.forUpdate.elementAt(i));
1596
1597 GuardedCmd bodyCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
1598
1599 makeLoop(x.getStartLoc(), x.getEndLoc(), x.locFirstSemi,
1600 GenericVarDeclVec.popFromStackVector(temporaries),
1601 guardCmd, bodyCmd, invariants, decreases,
1602 skolemConsts, predicates, bLabel);
1603
1604 wrapUpDeclBlock();
1605 return;
1606 }
1607
1608 case TagConstants.IFSTMT:
1609 {
1610 IfStmt i = (IfStmt)stmt;
1611 trIfStmt(i.expr, i.thn, i.els, decl);
1612 return;
1613 }
1614
1615 case TagConstants.BREAKSTMT:
1616 {
1617 BreakStmt b = (BreakStmt)stmt;
1618 Stmt label = TypeCheck.inst.getBranchLabel(b);
1619 if (Main.options().traceInfo > 0) {
1620 // add a label to track the break
1621 GuardedCmd g = traceInfoLabelCmd(b, "Break", b.loc);
1622 code.addElement(g);
1623 }
1624 raise(breakLabel(label));
1625 return;
1626 }
1627
1628 case TagConstants.CONTINUESTMT:
1629 {
1630 ContinueStmt c = (ContinueStmt)stmt;
1631 Stmt label = TypeCheck.inst.getBranchLabel(c);
1632 if (Main.options().traceInfo > 0) {
1633 // add a label to track the continue
1634 GuardedCmd g = traceInfoLabelCmd(c, "Continue", c.loc);
1635 code.addElement(g);
1636 }
1637 raise(continueLabel(label));
1638 return;
1639 }
1640
1641 case TagConstants.SYNCHRONIZESTMT:
1642 {
1643 SynchronizeStmt x = (SynchronizeStmt)stmt;
1644 int xStart = x.getStartLoc();
1645 int xEnd = x.getEndLoc();
1646 VariableAccess mu = fresh(x.expr, x.expr.getStartLoc(),
1647 "synchronized");
1648 Expr e = ptrExpr(x.expr);
1649 code.addElement(GC.gets(mu,e));
1650
1651 nullCheck(x.expr, mu, x.locOpenParen);
1652
1653 trSynchronizedBody(mu, x.stmt, x.locOpenParen, decl);
1654 return;
1655 }
1656
1657
1658 case TagConstants.EVALSTMT:
1659 {
1660 EvalStmt x = (EvalStmt)stmt;
1661 ptrExpr(x.expr);
1662 return;
1663 }
1664
1665 case TagConstants.LABELSTMT:
1666 {
1667 LabelStmt x = (LabelStmt)stmt;
1668 code.push(); // this mark popped by "opBlockCmd"
1669 trStmt(x.stmt,decl);
1670 code.addElement(opBlockCmd(breakLabel(x.stmt)));
1671 return;
1672 }
1673
1674 case TagConstants.SKIPSTMT:
1675 return;
1676
1677 case TagConstants.TRYFINALLYSTMT:
1678 {
1679 TryFinallyStmt x = (TryFinallyStmt)stmt;
1680 int xStart = x.getStartLoc();
1681 int xEnd = x.getEndLoc();
1682 GuardedCmd temp;
1683
1684 code.push();
1685 trStmt(x.tryClause,decl);
1686 GuardedCmd c0 = GC.seq(GuardedCmdVec.popFromStackVector(code));
1687
1688 code.push();
1689 VariableAccess ecSave = adorn(GC.ecvar);
1690 VariableAccess resultSave = adorn(GC.resultvar);
1691 VariableAccess xresultSave = adorn(GC.xresultvar);
1692
1693 if (Main.options().traceInfo > 0) {
1694 // add a label to track that the finally clause is entered because
1695 // an exception was raised
1696 GuardedCmd g = traceInfoLabelCmd(x, "FinallyBegin", x.locFinally);
1697 code.addElement(g);
1698 }
1699 code.addElement(GC.assume(GC.nary(xStart,xEnd,
1700 TagConstants.ANYEQ,
1701 GC.ecvar, ecSave)));
1702 code.addElement(GC.assume(GC.nary(xStart,xEnd,
1703 TagConstants.REFEQ,
1704 GC.resultvar, resultSave)));
1705 code.addElement(GC.assume(GC.nary(xStart,xEnd,
1706 TagConstants.REFEQ,
1707 GC.xresultvar, xresultSave)));
1708
1709 code.push();
1710 trStmt(x.finallyClause,decl);
1711 temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#n",
1712 GC.seq(GuardedCmdVec.popFromStackVector(code)));
1713 code.addElement(temp);
1714
1715 code.addElement(GC.gets(GC.ecvar, ecSave));
1716 code.addElement(GC.gets(GC.resultvar, resultSave));
1717 code.addElement(GC.gets(GC.xresultvar, xresultSave));
1718 if (Main.options().traceInfo > 0) {
1719 // add a label to track that the finally clause is exited when it
1720 // was entered due to that an exception was raised
1721 GuardedCmd g = traceInfoLabelCmd(x, "FinallyEnd", x.getEndLoc());
1722 code.addElement(g);
1723 }
1724 code.addElement(GC.raise());
1725
1726 GuardedCmd c1 = GC.seq(GuardedCmdVec.popFromStackVector(code));
1727
1728 code.addElement(GC.trycmd(c0,c1));
1729
1730 code.push();
1731 trStmt(x.finallyClause,decl);
1732 temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#x",
1733 GC.seq(GuardedCmdVec.popFromStackVector(code)));
1734 code.addElement(temp);
1735
1736 return;
1737 }
1738
1739 case TagConstants.TRYCATCHSTMT:
1740 {
1741 TryCatchStmt x = (TryCatchStmt)stmt;
1742 int xStart = x.getStartLoc();
1743 int xEnd = x.getEndLoc();
1744
1745 code.push();
1746 trStmt(x.tryClause,decl);
1747 GuardedCmd tryGC = GC.seq(GuardedCmdVec.popFromStackVector(code));
1748
1749 GuardedCmd els = GC.raise();
1750
1751 for(int i=x.catchClauses.size()-1; i>=0; i--) {
1752 CatchClause cc = (CatchClause)x.catchClauses.elementAt(i);
1753 int ccStart=cc.getStartLoc();
1754 int ccEnd=cc.getEndLoc();
1755
1756 // tst is typeof(XRES) <: Ti
1757 Expr tst = GC.nary(ccStart,ccEnd,
1758 TagConstants.TYPELE,
1759 GC.nary(ccStart,ccEnd,
1760 TagConstants.TYPEOF,
1761 GC.xresultvar),
1762 TypeExpr.make(ccStart,ccEnd,
1763 cc.arg.type));
1764
1765 if( i==0 ) {
1766 // extend tst with a disjunct XRES==null
1767 tst = GC.or(ccStart,ccEnd,
1768 tst,
1769 GC.nary(ccStart,ccEnd,
1770 TagConstants.REFEQ,
1771 GC.xresultvar,
1772 GC.nulllit));
1773 }
1774
1775
1776 code.push();
1777 declaredLocals.addElement(cc.arg);
1778 VariableAccess arg = VariableAccess.make( cc.arg.id, ccStart,
1779 cc.arg );
1780
1781 code.addElement(GC.assume(GC.nary(ccStart,ccEnd,
1782 TagConstants.ANYEQ,
1783 arg,
1784 GC.xresultvar)));
1785 trStmt(cc.body,decl);
1786 GuardedCmd thn = GC.seq(GuardedCmdVec.popFromStackVector(code));
1787
1788 els = GC.ifcmd(tst, thn, els);
1789 }
1790
1791
1792 GuardedCmd handler =
1793 GC.ifcmd( GC.nary(xStart,xEnd,
1794 TagConstants.ANYNE,
1795 GC.ecvar,
1796 GC.ec_throw),
1797 GC.raise(),
1798 els );
1799
1800 code.addElement(GC.trycmd(tryGC,handler));
1801
1802 return;
1803 }
1804
1805 case TagConstants.VARDECLSTMT:
1806 {
1807 LocalVarDecl vd = ((VarDeclStmt)stmt).decl;
1808 declaredLocals.addElement(vd);
1809 boolean isUninitialized = false;
1810 boolean isGhost = false;
1811 if (vd.pmodifiers != null) {
1812 isGhost = Utils.findModifierPragma(vd.pmodifiers,TagConstants.GHOST) != null;
1813 for (int i= 0; i < vd.pmodifiers.size(); i++) {
1814 ModifierPragma prag= vd.pmodifiers.elementAt(i);
1815 if (prag.getTag() == TagConstants.UNINITIALIZED) {
1816 VariableAccess init = initadorn(vd);
1817 declaredLocals.addElement(init.decl);
1818 setInitVar(vd, init);
1819 isUninitialized = true;
1820 break; // don't look for any further UNINITIALIZED modifiers
1821 }
1822 }
1823 }
1824
1825 if (null != vd.init) {
1826 Assert.notFalse(vd.locAssignOp != Location.NULL);
1827 VariableAccess lhs = TrAnExpr.makeVarAccess(vd, vd.getStartLoc());
1828 TrAnExpr.initForClause();
1829 Expr rval = isGhost ?
1830 TrAnExpr.trSpecExpr((Expr)vd.init,null,premapWithArgs) :
1831 ptrExpr(vd.init);
1832 if (TrAnExpr.extraSpecs) addNewAssumptions();
1833 if (! isUninitialized) {
1834 writeCheck(lhs, vd.init, rval, vd.locAssignOp, false);
1835 }
1836 code.addElement(GC.gets(lhs, rval));
1837 }
1838 return;
1839 }
1840
1841 case TagConstants.CONSTRUCTORINVOCATION:
1842 //@ unreachable;
1843 // If the following assert breaks, there's something wrong in
1844 // "trBody" where the constructor call is split up from the rest of
1845 // the constructor body.
1846 Assert.fail("constructor invocation handled in TrConstructorCallStmt");
1847 return;
1848
1849 case TagConstants.UNREACHABLE:
1850 addCheck(stmt, TagConstants.CHKCODEREACHABILITY, GC.falselit);
1851 return;
1852
1853 case TagConstants.SETSTMTPRAGMA: {
1854 SetStmtPragma s = (SetStmtPragma)stmt;
1855
1856 if (s.target instanceof FieldAccess) {
1857 FieldAccess fa = (FieldAccess)s.target;
1858 TrAnExpr.initForClause();
1859 Expr lhs= trFieldAccess(true, fa); // FIXME - premap?
1860 Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1861 if (TrAnExpr.extraSpecs) addNewAssumptions();
1862 // Add check that the lhs is allowed to be written (writable pragma)
1863 writeCheck(lhs, s.value, rval, s.locOp, false);
1864 // Add checks that the lhs is allowed to be assigned (assignable pragma)
1865 frameHandler.modifiesCheckField(lhs,fa.getStartLoc(),fa.decl);
1866 String name;
1867 if (lhs.getTag() == TagConstants.VARIABLEACCESS) {
1868 VariableAccess valhs = (VariableAccess)lhs;
1869 name = valhs.decl.id.toString();
1870 code.addElement(GC.gets(valhs, rval));
1871 if (Modifiers.isStatic(valhs.decl.modifiers)) {
1872 code.addElement(modify(GC.statevar,s.getStartLoc()));
1873 }
1874 } else {
1875 // Instance field
1876 NaryExpr target = (NaryExpr)lhs;
1877 VariableAccess field = (VariableAccess)target.exprs.elementAt(0);
1878 name = field.decl.id.toString();
1879 Expr obj = target.exprs.elementAt(1);
1880 code.addElement(GC.subgets(field, obj,rval));
1881 code.addElement(modify(GC.statevar,s.getStartLoc()));
1882 }
1883 return;
1884 /*
1885 This was originally here. The if block just above was inserted to
1886 make the correspondence with assignment complete.
1887 Not sure if the protect expressions belong ??? FIXME
1888
1889 VariableAccess field = VariableAccess.make(fa.id, fa.locId, fa.decl);
1890 if (Modifiers.isStatic(fa.decl.modifiers)) {
1891 code.addElement(GC.gets( field,
1892 TrAnExpr.trSpecExpr(s.value)));
1893 } else {
1894 Expr obj = ((ExprObjectDesignator)fa.od).expr;
1895 code.addElement(GC.subgets( field,
1896 TrAnExpr.trSpecExpr(obj),
1897 TrAnExpr.trSpecExpr(s.value) ));
1898 }
1899 */
1900
1901 } else if (s.target instanceof VariableAccess) {
1902 // Assignments to local ghost variables end here
1903 VariableAccess lhs = (VariableAccess)s.target;
1904 TrAnExpr.initForClause();
1905 Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1906 if (TrAnExpr.extraSpecs) addNewAssumptions();
1907 writeCheck(lhs, s.value, rval, s.locOp, false);
1908 code.addElement(GC.gets(lhs,rval));
1909 // A local variable is not part of an assignable frame so there is no
1910 // assignable clause to check
1911 VariableAccess init = getInitVar(lhs.decl);
1912 if (init != null)
1913 code.addElement(GC.gets(init, GC.truelit));
1914 return;
1915 } else if (s.target instanceof ArrayRefExpr) {
1916 ArrayRefExpr lhs= (ArrayRefExpr)s.target;
1917
1918 TrAnExpr.initForClause();
1919 Expr array= TrAnExpr.trSpecExpr(lhs.array,null,premapWithArgs);
1920 Expr index= TrAnExpr.trSpecExpr(lhs.index,null,premapWithArgs);
1921 Expr rval= TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1922 if (TrAnExpr.extraSpecs) addNewAssumptions();
1923 // Add a check that the value of the array index is in bounds
1924 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
1925 // Add a check that the assignment to an array element is allowed
1926 // by the assignable clauses
1927 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
1928 if (! isFinal(TypeCheck.inst.getType(lhs.array))) {
1929 addCheck(s.loc,
1930 TagConstants.CHKARRAYSTORE,
1931 GC.nary(TagConstants.IS, rval,
1932 GC.nary(TagConstants.ELEMTYPE,
1933 GC.nary(TagConstants.TYPEOF, array))),
1934 Location.NULL, lhs.array);
1935 }
1936
1937 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
1938 code.addElement(modify(GC.statevar,lhs.getStartLoc()));
1939 Expr a= GC.select(GC.elemsvar, array);
1940 return;
1941
1942 } else {
1943
1944 ErrorSet.fatal(s.getStartLoc(),
1945 "Unknown construct to translate");
1946 }
1947 break;
1948 }
1949
1950 case TagConstants.HENCE_BY:
1951 // FIXME - ignored - unclear semantics
1952 return;
1953
1954 case TagConstants.ASSUME:
1955 {
1956 ExprStmtPragma x = (ExprStmtPragma)stmt;
1957 TrAnExpr.initForClause();
1958 Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs);
1959 if (TrAnExpr.extraSpecs) addNewAssumptionsNow();
1960 code.addElement(GC.assume(p));
1961 return;
1962 }
1963
1964 case TagConstants.ASSERT: {
1965 ExprStmtPragma x = (ExprStmtPragma)stmt;
1966 TrAnExpr.initForClause();
1967 Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs);
1968 if (TrAnExpr.extraSpecs) addNewAssumptionsNow();
1969 code.addElement(GC.check(x.getStartLoc(), TagConstants.CHKASSERT,
1970 p, Location.NULL));
1971 return;
1972 }
1973
1974 case TagConstants.LOOP_INVARIANT:
1975 case TagConstants.MAINTAINING:
1976 {
1977 ExprStmtPragma x = (ExprStmtPragma)stmt;
1978 loopinvariants.addElement(x);
1979 return;
1980 }
1981
1982 case TagConstants.DECREASES:
1983 case TagConstants.DECREASING:
1984 {
1985 ExprStmtPragma x = (ExprStmtPragma)stmt;
1986 loopDecreases.addElement(x);
1987 return;
1988 }
1989
1990 case TagConstants.LOOP_PREDICATE:
1991 {
1992 ExprStmtPragma x = (ExprStmtPragma)stmt;
1993 loopPredicates.addElement(x);
1994 return;
1995 }
1996
1997 case TagConstants.SKOLEMCONSTANTPRAGMA:
1998 {
1999 SkolemConstantPragma p = (SkolemConstantPragma)stmt;
2000 skolemConstants.append(p.decls);
2001 break;
2002 }
2003
2004 case TagConstants.CLASSDECLSTMT:
2005 if (this.issueCautions && !escjava.Main.options().noNotCheckedWarnings) {
2006 ErrorSet.caution(stmt.getStartLoc(),
2007 "Not checking block-level types");
2008 }
2009 return;
2010
2011 case TagConstants.ASSERTSTMT: {
2012 // Only process if we are supposed to be parsing Java
2013 // 1.4 or later and assertions are enabled.
2014 AssertStmt assertStmt = (AssertStmt)stmt;
2015 if (!Tool.options.assertIsKeyword || !Tool.options.assertionsEnabled) {
2016 // continue - simply skip the assertions
2017 } else if (Main.options().assertionMode ==
2018 Options.JML_ASSERTIONS) {
2019 // Treat a Java assert as a JML assert
2020 // Since it is a Java statement, it can't contain JML constructs
2021 // FIXME - so should it be translated this way?
2022 Expr predicate = TrAnExpr.trSpecExpr(assertStmt.pred);
2023 code.addElement(GC.check(assertStmt.getStartLoc(), TagConstants.CHKASSERT,
2024 predicate, Location.NULL));
2025 } else if (Main.options().assertionMode ==
2026 Options.JAVA_ASSERTIONS) {
2027 // Treat a Java assert as a (conditional) throw
2028 trIfStmt(assertStmt.ifStmt.expr, assertStmt.ifStmt.thn, assertStmt.ifStmt.els,decl);
2029 }
2030 return;
2031 }
2032 default:
2033 //@ unreachable;
2034 Assert.notFalse(false,"Unexpected tag " + TagConstants.toString(tag)
2035 + " " + stmt + " " +
2036 Location.toString(stmt.getStartLoc()));
2037 return;
2038 }
2039 }
2040
2041 /**
2042 * Translate an "if" statement.
2043 *
2044 * @design This method was refactored out to handle Java's "assert" keyword as
2045 * well as normal "if" statements.
2046 */
2047 private void trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl) {
2048 Expr guardExpr = ptrExpr(guard);
2049
2050 code.push();
2051 if (Main.options().traceInfo > 0) {
2052 // add a label to track the if branch taken
2053 GuardedCmd g = traceInfoLabelCmd(thenStmt, "Then");
2054 code.addElement(g);
2055 }
2056 trStmt(thenStmt,decl);
2057 GuardedCmd thenGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
2058
2059 code.push();
2060 if (Main.options().traceInfo > 0) {
2061 // add a label to track the if branch taken
2062 GuardedCmd g = traceInfoLabelCmd(elseStmt, "Else");
2063 code.addElement(g);
2064 }
2065 trStmt(elseStmt,decl);
2066 GuardedCmd elseGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
2067
2068 code.addElement(GC.ifcmd(guardExpr, thenGuardedCmd, elseGuardedCmd));
2069 return;
2070 }
2071
2072 //@ requires loc != Location.NULL;
2073 private void trSynchronizedBody(/*@ non_null */ Expr mu,
2074 /*@ non_null */ Stmt stmt, int loc, TypeDecl decl) {
2075 // check LockingOrderViolation: mutexLE(max(LS),mu) || LS[mu]
2076 addCheck(loc,
2077 TagConstants.CHKLOCKINGORDER,
2078 GC.or(GC.nary(TagConstants.LOCKLE,
2079 GC.nary(TagConstants.MAX, GC.LSvar),
2080 mu),
2081 GC.nary(TagConstants.SELECT, GC.LSvar, mu)));
2082
2083 VariableAccess newLS = adorn(GC.LSvar);
2084
2085 // e1 is ( lockLE(max(LS),mu) && mu == max(newLS) )
2086 Expr e1 = GC.and(
2087 // lockLE(max(LS),mu)
2088 GC.nary(TagConstants.LOCKLE,
2089 GC.nary(TagConstants.MAX, GC.LSvar),
2090 mu),
2091 // mu == max(newLS)
2092 GC.nary(TagConstants.REFEQ,
2093 mu,
2094 GC.nary(TagConstants.MAX, newLS)));
2095
2096 // e2 is ( LS[mu] && newLS == LS )
2097 Expr e2 = GC.and(
2098 // LS[mu]
2099 GC.select(GC.LSvar, mu ),
2100 // newLS == LS
2101 GC.nary(TagConstants.REFEQ, newLS, GC.LSvar));
2102
2103 // assume (e1 || e2)
2104 code.addElement(GC.assume(GC.or(e1, e2)));
2105
2106 // assume newLS == store(LS,mu,boolTrue)
2107 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ?
2108 newLS,
2109 GC.nary(TagConstants.STORE,
2110 GC.LSvar, mu, GC.truelit))));
2111
2112 // assume newLS == asLockSet(newLS)
2113 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ?
2114 newLS,
2115 GC.nary(TagConstants.ASLOCKSET,
2116 newLS))));
2117
2118 // Translate the body, using the new LS
2119 VariableAccess oldLS = GC.LSvar;
2120 GC.LSvar = newLS;
2121 trStmt(stmt,decl);
2122 GC.LSvar = oldLS;
2123 }
2124
2125 /**
2126 * This method implements "TrConstructorCallStmt" as described in section 6 of
2127 * ESCJ 16.
2128 */
2129 private void trConstructorCallStmt(/*@ non_null */ ConstructorInvocation ci) {
2130 // Check if this is a constructor for an inner class; if so, we need to pass
2131 // an enclosing instance as the first argument.
2132 TypeSig resultType = TypeSig.getSig(ci.decl.parent);
2133 boolean inner = !resultType.isTopLevelType();
2134
2135 // translate arguments
2136 int argsSize = ci.args.size() + (inner ? 1 : 0);
2137 ExprVec rawArgs = ci.args.copy();
2138 ExprVec args = ExprVec.make(argsSize);
2139
2140 if (inner) {
2141 Expr rawExpr = ci.enclosingInstance;
2142 Assert.notNull(rawExpr);
2143 rawArgs.insertElementAt(rawExpr, 0);
2144
2145 Purity.decorate(rawExpr);
2146 Expr arg = trExpr(true, rawExpr);
2147 args.addElement(arg);
2148
2149 // do nullCheck here rather than non-null check in call(...):
2150 nullCheck(rawExpr, arg, ci.locDot);
2151 }
2152 for (int i = 0; i < ci.args.size(); i++) {
2153 Expr rawExpr = ci.args.elementAt(i);
2154 Purity.decorate(rawExpr);
2155 // protect all but the last argument
2156 Expr arg = trExpr(i != ci.args.size()-1, rawExpr);
2157 args.addElement(arg);
2158 }
2159
2160 InlineSettings is = (InlineSettings)inlineDecoration.get(ci);
2161 code.addElement(call(ci.decl, rawArgs, args, scope,
2162 ci.getStartLoc(), ci.getEndLoc(),
2163 ci.locOpenParen, true, is, null, false)); // FIXME - set the eod=null to the right value
2164 // this = RES
2165 code.addElement(GC.gets(GC.thisvar, GC.resultvar));
2166
2167 // FIXME - this is for a 'this' or 'super' call within a constructor - need to put in modifies checks
2168 }
2169
2170 //// Expression translation
2171
2172 /**
2173 * Extends the code array with a command that evaluates e and returns an
2174 * expession which denotes this value in the poststate of that command. If
2175 * <code>protect</code> is true, then the expression returned will depend only on
2176 * values of temporary variables (that is, the expression returned will not be
2177 * affected by changes to program variables).<p> If <code>protect</code> is
2178 * <code>true</code>, then the value returned is certain to be of type
2179 * <code>VariableAccess</code>.
2180 */
2181 //@ ensures protect ==> \result instanceof VariableAccess;
2182 private Expr protect(boolean protect, Expr e, int loc) {
2183 if (protect) {
2184 VariableAccess result = fresh(e, loc);
2185 code.addElement(GC.gets(result, e));
2186 return result;
2187 } else return e;
2188 }
2189
2190 //@ ensures protect ==> \result instanceof VariableAccess;
2191 private Expr protect(boolean protect, Expr e, int loc, String suffix) {
2192 if (protect) {
2193 VariableAccess result = fresh(e, loc, suffix);
2194 code.addElement(GC.gets(result, e));
2195 return result;
2196 } else return e;
2197 }
2198
2199 /** Purify and translate expr without protection */
2200 private Expr ptrExpr(VarInit expr) {
2201 Purity.decorate(expr);
2202 return trExpr(false, expr);
2203 }
2204
2205 /**
2206 * Translate <code>expr</code> into a sequence of guarded commands that are
2207 * appended to <code>code</code> and return an expression denoting the value of
2208 * the expression. New temporaries may be generated; these are added to
2209 * <code>temporaries</code>.
2210 *
2211 * @param protect if true, then the expression return will depend only on values
2212 * of temporary variables (that is, the expression returned will not be affected
2213 * by changes in program variables).
2214 */
2215 private Expr trExpr(boolean protect, /*@ non_null */ VarInit expr) {
2216 int tag = expr.getTag();
2217
2218 switch (tag) {
2219 case TagConstants.ARRAYINIT:
2220 {
2221 ArrayInit x = (ArrayInit)expr;
2222 int xStart = x.getStartLoc();
2223 int xEnd = x.getEndLoc();
2224
2225 int len = x.elems.size();
2226 boolean isPure[] = new boolean[len];
2227 Expr[] elems = new Expr[len];
2228
2229 // set isPure[i] to true if {E_{i+1},...,E_n} are all pure
2230 if( len != 0 ) isPure[len-1] = true;
2231 for(int i=len-2; i>=0; i-- ) {
2232 isPure[i] = isPure[i+1] && !Purity.impure(x.elems.elementAt(i+1));
2233 }
2234
2235 for(int i=0; i<len; i++ )
2236 elems[i] = trExpr(isPure[i], x.elems.elementAt(i));
2237
2238 // Construct variables
2239 VariableAccess a = fresh(x, xStart, "arrayinit");
2240 VariableAccess newallocvar = adorn(GC.allocvar);
2241
2242 // assume !isAllocated(a, alloc);
2243 code.addElement(GC.assume(GC.not(xStart, xEnd,
2244 GC.nary(xStart, xEnd,
2245 TagConstants.ISALLOCATED,
2246 a, GC.allocvar))));
2247 // assume isAllocated(a, alloc');
2248 code.addElement(GC.assume(GC.nary(xStart, xEnd,
2249 TagConstants.ISALLOCATED,
2250 a,
2251 newallocvar )));
2252 // assume a != null;
2253 code.addElement(GC.assume(GC.nary(xStart, xEnd,
2254 TagConstants.REFNE,
2255 a,
2256 GC.nulllit )));
2257 // assume typeof(a) == array(T);
2258 Expr typeofa = GC.nary(xStart, xEnd,
2259 TagConstants.TYPEOF, a);
2260 Expr arrayT = TypeExpr.make(xStart, xEnd,
2261 TypeCheck.inst.getType(x));
2262
2263 code.addElement(GC.assume(GC.nary(xStart, xEnd,
2264 TagConstants.TYPEEQ,
2265 typeofa, arrayT )));
2266
2267 // assume arrayLength(a) == n
2268 code.addElement(GC.assume(GC.nary(xStart, xEnd,
2269 TagConstants.INTEGRALEQ,
2270 GC.nary(xStart, xEnd,
2271 TagConstants.ARRAYLENGTH,
2272 a),
2273 LiteralExpr.make(TagConstants.INTLIT,
2274 new Integer(len),
2275 xStart))));
2276
2277 // elems[a][i] = ei
2278 Expr elemsAta = GC.nary(xStart, xEnd,
2279 TagConstants.SELECT,
2280 GC.elemsvar, a);
2281 for(int i=0; i<len; i++ ) {
2282 Expr iLit =
2283 LiteralExpr.make(TagConstants.INTLIT, new Integer(i), xStart);
2284 Expr elemsAtaAti = GC.nary(xStart, xEnd,
2285 TagConstants.SELECT,
2286 elemsAta, iLit);
2287 code.addElement(GC.assume(GC.nary(xStart, xEnd,
2288 TagConstants.REFEQ,
2289 elemsAtaAti, elems[i] )));
2290 }
2291
2292 // assume that everything allocated is an array
2293 code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar,
2294 newallocvar)));
2295 // alloc = alloc'
2296 code.addElement(GC.gets(GC.allocvar, newallocvar));
2297
2298 return a;
2299 }
2300
2301 case TagConstants.THISEXPR: {
2302 ThisExpr t = (ThisExpr)expr;
2303 if (t.classPrefix != null)
2304 return trExpr(protect, Inner.unfoldThis(t));
2305
2306 // We ignore "protect" here, since "this" is (almost) never
2307 // assigned to. (In the one case where "this" is assigned--
2308 // after the super-or-sibling constructor call in a
2309 // constructor--"protect" is not needed.
2310 return GC.thisvar;
2311 }
2312
2313 case TagConstants.SETCOMPEXPR:
2314 ErrorSet.fatal(expr.getStartLoc(), "Set comprehension is not supported");
2315
2316 // Literals
2317 case TagConstants.BOOLEANLIT:
2318 case TagConstants.CHARLIT:
2319 case TagConstants.DOUBLELIT:
2320 case TagConstants.FLOATLIT:
2321 case TagConstants.INTLIT:
2322 case TagConstants.LONGLIT:
2323 case TagConstants.NULLLIT:
2324 return (Expr)expr;
2325
2326 case TagConstants.STRINGLIT:
2327 {
2328 String s = ((LiteralExpr)expr).value.toString();
2329 Expr result = GC.nary(
2330 TagConstants.INTERN,
2331 GC.symlit(Strings.intern(s).toString()),
2332 GC.symlit(Integer.toString(s.length())) );
2333
2334 return result;
2335 }
2336
2337 case TagConstants.ARRAYREFEXPR:
2338 {
2339 ArrayRefExpr x= (ArrayRefExpr)expr;
2340 Expr array= trExpr(Purity.impure(x.index), x.array);
2341 Expr index= trExpr(false, x.index);
2342
2343 arrayAccessCheck(x.array, array, x.index, index, x.locOpenBracket);
2344
2345 Expr a= GC.select(GC.elemsvar, array);
2346 return protect(protect, GC.select(a, index), x.locOpenBracket);
2347 }
2348
2349 case TagConstants.NEWINSTANCEEXPR:
2350 {
2351 NewInstanceExpr ni= (NewInstanceExpr)expr;
2352
2353 ExprVec rawArgs = ni.args.copy();
2354 ExprVec args = ExprVec.make(ni.args.size());
2355
2356 if (ni.anonDecl != null) {
2357 if (this.issueCautions && ! Main.options().noNotCheckedWarnings) {
2358 ErrorSet.caution(ni.anonDecl.loc,
2359 "Not checking body of anonymous class" +
2360 " (subclass of " +
2361 ni.type.name.printName() + ")");
2362 }
2363 }
2364
2365 // translate enclosing instance argument if present:
2366 if (ni.enclosingInstance != null) {
2367 rawArgs.insertElementAt(ni.enclosingInstance, 0);
2368 Expr arg = trExpr(true, ni.enclosingInstance);
2369 args.addElement(arg);
2370
2371 // do nullCheck here rather than non-null check in call(...):
2372 nullCheck(ni.enclosingInstance, arg, ni.locDot);
2373 }
2374
2375 // translate normal arguments
2376 for (int i = 0; i < ni.args.size(); i++) {
2377 // protect all but the last argument
2378 Expr arg = trExpr(i != ni.args.size()-1, ni.args.elementAt(i));
2379 args.addElement(arg);
2380 }
2381
2382 InlineSettings is = (InlineSettings)inlineDecoration.get(ni);
2383 code.addElement(call(ni.decl, rawArgs, args, scope,
2384 ni.loc, ni.getEndLoc(), ni.locOpenParen,
2385 false, is, temporary("RES", ni.loc, ni.loc),
2386 true));
2387
2388 { Expr tType = TypeExpr.make(ni.loc, ni.getEndLoc(), ni.type);
2389 Expr resType = GC.nary(TagConstants.TYPEOF, GC.resultvar);
2390 if (ni.anonDecl != null) {
2391 // assume typeof(RES) != T (for anonymous new)
2392 code.addElement(GC.assume(GC.nary(TagConstants.TYPENE,
2393 resType,
2394 tType)));
2395 } else {
2396 // assume typeof(RES) == T (for ordinary new)
2397 code.addElement(GC.assume(GC.nary(TagConstants.TYPEEQ,
2398 resType,
2399 tType)));
2400 }
2401 }
2402
2403 ByteArrayOutputStream baos = new ByteArrayOutputStream();
2404 PrettyPrint.write(baos, "new!");
2405 PrettyPrint.inst.print(baos, ni.type);
2406 return protect(protect, GC.resultvar, ni.locOpenParen, baos.toString());
2407 }
2408
2409 case TagConstants.NEWARRAYEXPR:
2410 {
2411 NewArrayExpr x= (NewArrayExpr)expr;
2412 int nd= x.dims.size();
2413
2414 if (x.init != null) {
2415 return trExpr(true, x.init);
2416 }
2417
2418 // Construct variables
2419 ByteArrayOutputStream baos = new ByteArrayOutputStream();
2420 PrettyPrint.write(baos, "new!");
2421 PrettyPrint.inst.print(baos, x.type);
2422 for (int i = 0; i < nd; i++) {
2423 PrettyPrint.write(baos, "[]");
2424 }
2425 VariableAccess result= fresh(x, x.loc, baos.toString());
2426 VariableAccess newallocvar= adorn(GC.allocvar);
2427
2428 // Evaluate length in each dimension
2429 Expr[] dims= new Expr[nd];
2430 for (int i= 0; i < nd; i++) {
2431 boolean protectDim= false;
2432 for (int j= i+1; j < nd && ! protectDim; j++)
2433 protectDim= Purity.impure(x.dims.elementAt(j));
2434 dims[i]= trExpr(protectDim, x.dims.elementAt(i));
2435 // "nd" squared iterations, but nd should be small
2436 }
2437
2438 // Check for negative array sizes
2439 for (int i= 0; i < nd; i++) {
2440 Expr nonneg= GC.nary(TagConstants.INTEGRALLE, GC.zerolit, dims[i]);
2441 Condition cond= GC.condition(TagConstants.CHKNEGATIVEARRAYSIZE,
2442 nonneg, Location.NULL);
2443 Expr je= x.dims.elementAt(i);
2444 code.addElement(GC.check(x.locOpenBrackets[i], cond,
2445 trim(x.dims.elementAt(i))));
2446 }
2447
2448 // Construct call to arrayFresh
2449 Expr shape= GC.nary(TagConstants.ARRAYSHAPEONE, dims[nd-1]);
2450 Type type= ArrayType.make(x.type, Location.NULL);
2451 for (int i= nd-2; 0 <= i; i--) {
2452 shape= GC.nary(TagConstants.ARRAYSHAPEMORE, dims[i], shape);
2453 type= ArrayType.make(type, Location.NULL);
2454 }
2455 Expr[] arrayFreshArgs= {
2456 result, GC.allocvar, newallocvar, GC.elemsvar, shape,
2457 GC.typeExpr(type), GC.zeroequiv(x.type)
2458 };
2459 Expr arrayFresh= GC.nary(x.getStartLoc(), x.getEndLoc(),
2460 TagConstants.ARRAYFRESH,
2461 ExprVec.make(arrayFreshArgs));
2462
2463 // Emit the Assume and a Gets commands
2464 code.addElement(GC.assume(arrayFresh));
2465 code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar,
2466 newallocvar)));
2467 Expr ownerNull = predArrayOwnerNull(GC.allocvar, newallocvar,
2468 result);
2469 if (ownerNull != null)
2470 code.addElement(GC.assume(ownerNull));
2471 code.addElement(GC.gets(GC.allocvar, newallocvar));
2472
2473 // Return the variable containing the newly-allocated array
2474 return result;
2475 }
2476
2477 case TagConstants.CONDEXPR:
2478 {
2479 CondExpr x= (CondExpr)expr;
2480 // ifCmd((tr(x.test), tr(x.thn), tr(x.els))
2481 Expr test= trExpr(false, x.test);
2482 VariableAccess result= fresh(x, x.locQuestion, "cond");
2483
2484 code.push();
2485 if (Main.options().traceInfo > 0) {
2486 // add a label to track the if branch taken
2487 GuardedCmd g = traceInfoLabelCmd(x.thn, "Then");
2488 code.addElement(g);
2489 }
2490 Expr thnP= trExpr(false, x.thn);
2491 code.addElement(GC.gets(result, thnP));
2492 GuardedCmd thenbody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2493
2494 code.push();
2495 if (Main.options().traceInfo > 0) {
2496 // add a label to track the if branch taken
2497 GuardedCmd g = traceInfoLabelCmd(x.els, "Else");
2498 code.addElement(g);
2499 }
2500 Expr elsP= trExpr(false, x.els);
2501 code.addElement(GC.gets(result, elsP));
2502 GuardedCmd elsebody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2503
2504 code.addElement(GC.ifcmd(test, thenbody, elsebody));
2505 return result;
2506 }
2507
2508 case TagConstants.INSTANCEOFEXPR:
2509 {
2510 InstanceOfExpr x= (InstanceOfExpr)expr;
2511 Expr obj = trExpr(protect, x.expr);
2512
2513 Expr isOfType = GC.nary(x.getStartLoc(), x.getEndLoc(),
2514 TagConstants.IS, obj,
2515 TypeExpr.make(x.type.getStartLoc(),
2516 x.type.getEndLoc(),
2517 x.type));
2518 Expr notNull = GC.nary(x.getStartLoc(), x.getEndLoc(),
2519 TagConstants.REFNE, obj, GC.nulllit);
2520
2521 return GC.and(x.getStartLoc(), x.getEndLoc(),
2522 isOfType,
2523 notNull);
2524 }
2525
2526 case TagConstants.CASTEXPR:
2527 {
2528 CastExpr x= (CastExpr)expr;
2529 Expr result= trExpr(protect, x.expr);
2530 Expr te = GC.typeExpr(x.type);
2531 if (Types.isReferenceType(x.type)) {
2532 addCheck(expr,
2533 TagConstants.CHKCLASSCAST,
2534 GC.nary(TagConstants.IS, result, te));
2535 }
2536 result = GC.nary(TagConstants.CAST, result, te);
2537 return result;
2538 }
2539
2540 case TagConstants.CLASSLITERAL:
2541 {
2542 ClassLiteral x= (ClassLiteral)expr;
2543 return GC.nary(x.getStartLoc(), x.getEndLoc(),
2544 TagConstants.CLASSLITERALFUNC,
2545 TypeExpr.make(x.type.getStartLoc(),
2546 x.type.getEndLoc(),
2547 x.type));
2548 }
2549
2550 // Binary expressions
2551 case TagConstants.OR: case TagConstants.AND:
2552 {
2553 BinaryExpr x= (BinaryExpr)expr;
2554 VariableAccess result= fresh(x, x.locOp,
2555 (tag == TagConstants.OR ?
2556 "cor" : "cand"));
2557 Expr left= trExpr(false, x.left);
2558
2559 // Create a chunk of code that evaluates the right expr and
2560 // saves its value in "result"
2561 code.push();
2562 Expr right= trExpr(false, x.right);
2563 code.addElement(GC.gets(result, right));
2564 GuardedCmd rightbody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2565
2566 GuardedCmd thn, els;
2567 if (tag == TagConstants.OR) {
2568 thn= GC.gets(result, GC.truelit);
2569 els= rightbody;
2570 } else {
2571 thn= rightbody;
2572 els= GC.gets(result, GC.falselit);
2573 }
2574 if (Main.options().traceInfo > 0) {
2575 // add labels to track which operands are evaluated
2576 GuardedCmd g = traceInfoLabelCmd(x, "FirstOpOnly", x.locOp);
2577 if (tag == TagConstants.OR) {
2578 thn = GC.seq(g, thn);
2579 }
2580 else {
2581 els = GC.seq(g, els);
2582 }
2583 }
2584 code.addElement(GC.ifcmd(left, thn, els));
2585 return result;
2586 }
2587
2588 case TagConstants.BITOR: case TagConstants.BITXOR:
2589 case TagConstants.BITAND: case TagConstants.NE:
2590 case TagConstants.EQ: case TagConstants.GE:
2591 case TagConstants.GT: case TagConstants.LE:
2592 case TagConstants.LT: case TagConstants.LSHIFT:
2593 case TagConstants.RSHIFT: case TagConstants.URSHIFT:
2594 case TagConstants.ADD: case TagConstants.SUB:
2595 case TagConstants.STAR:
2596 case TagConstants.DIV: case TagConstants.MOD:
2597 {
2598 BinaryExpr x= (BinaryExpr)expr;
2599 Expr left= trExpr(Purity.impure(x.right), x.left);
2600 Expr right= trExpr(false, x.right);
2601 if (tag == TagConstants.DIV || tag == TagConstants.MOD) {
2602 if (Types.isIntegralType(TypeCheck.inst.getType(x.right))) {
2603 addCheck(x.locOp, TagConstants.CHKARITHMETIC,
2604 GC.nary(TagConstants.INTEGRALNE, right, GC.zerolit));
2605 }
2606 }
2607 int newtag= TrAnExpr.getGCTagForBinary(x);
2608 if (tag == TagConstants.GT || tag == TagConstants.GE ||
2609 tag == TagConstants.LT || tag == TagConstants.LE) {
2610 // Must be primitive types
2611 int leftTag = ((PrimitiveType)TypeCheck.inst.getType(x.left)).getTag();
2612 int rightTag = ((PrimitiveType)TypeCheck.inst.getType(x.right)).getTag();
2613 if (leftTag == rightTag)
2614 ; // do nothing
2615 else if (leftTag == TagConstants.REALTYPE && rightTag != TagConstants.REALTYPE)
2616 right = GC.cast(right,Types.realType);
2617 else if (leftTag != TagConstants.REALTYPE && rightTag == TagConstants.REALTYPE)
2618 left = GC.cast(left,Types.realType);
2619 else if (leftTag == TagConstants.DOUBLETYPE && rightTag != TagConstants.DOUBLETYPE)
2620 right = GC.cast(right,Types.doubleType);
2621 else if (leftTag != TagConstants.DOUBLETYPE && rightTag == TagConstants.DOUBLETYPE)
2622 left = GC.cast(left,Types.doubleType);
2623 else if (leftTag == TagConstants.FLOATTYPE && rightTag != TagConstants.FLOATTYPE)
2624 right = GC.cast(right,Types.floatType);
2625 else if (leftTag != TagConstants.FLOATTYPE && rightTag == TagConstants.FLOATTYPE)
2626 left = GC.cast(left,Types.floatType);
2627
2628 // FIXME - other promotions ? Also in TrAnExpr.java
2629
2630 }
2631 if (newtag == TagConstants.STRINGCAT) {
2632 return addNewString(x,left,right);
2633
2634 } else {
2635 return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(),
2636 newtag, left, right),
2637 x.locOp);
2638 }
2639 }
2640
2641 case TagConstants.ASSIGN:
2642 {
2643 BinaryExpr x= (BinaryExpr)expr;
2644 Expr right= x.right;
2645 Expr left= x.left;
2646
2647 int ltag = left.getTag();
2648 if (ltag == TagConstants.VARIABLEACCESS) {
2649 VariableAccess lhs= (VariableAccess)left;
2650 Expr rval= trExpr(false, right);
2651 writeCheck(lhs, right, rval, x.locOp, false);
2652 code.addElement(GC.gets(lhs, rval));
2653 VariableAccess init= getInitVar(lhs.decl);
2654 if (init != null)
2655 code.addElement(GC.gets(init, GC.truelit));
2656 if (Modifiers.isStatic(lhs.decl.modifiers)) {
2657 code.addElement(modify(GC.statevar,x.getStartLoc()));
2658 }
2659 return protect(protect, left, x.locOp, lhs.decl.id.toString() + "=");
2660
2661 } else if (ltag == TagConstants.FIELDACCESS) {
2662 Expr lhs= trFieldAccess(true, (FieldAccess)left);
2663 Expr rval= trExpr(false, right);
2664 String name;
2665 writeCheck(lhs, right, rval, x.locOp, false);
2666 // Add a check that the lhs field may be assigned (assignable clause)
2667 frameHandler.modifiesCheckField(lhs,lhs.getStartLoc(),
2668 ((FieldAccess)left).decl);
2669 if (lhs.getTag() == TagConstants.VARIABLEACCESS) {
2670 VariableAccess vaLhs = (VariableAccess)lhs;
2671 name = vaLhs.decl.id.toString();
2672 code.addElement(GC.gets(vaLhs, rval));
2673 } else {
2674 NaryExpr target= (NaryExpr)lhs;
2675 VariableAccess field= (VariableAccess)target.exprs.elementAt(0);
2676 name = field.decl.id.toString();
2677 Expr obj= target.exprs.elementAt(1);
2678 code.addElement(GC.subgets(field, obj, rval));
2679 }
2680 code.addElement(modify(GC.statevar,x.locOp));
2681 return protect(protect, lhs, x.locOp, name + "=");
2682
2683 } else if (ltag == TagConstants.ARRAYREFEXPR) {
2684 ArrayRefExpr lhs= (ArrayRefExpr)left;
2685
2686 Expr array= trExpr(true, lhs.array);
2687 Expr index= trExpr(true, lhs.index);
2688 Expr rval= trExpr(false, right);
2689
2690 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
2691 // Add a check that the array[index] on the lhs is assignable
2692 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
2693 if (! isFinal(TypeCheck.inst.getType(lhs.array))) {
2694 addCheck(x.locOp,
2695 TagConstants.CHKARRAYSTORE,
2696 GC.nary(TagConstants.IS, rval,
2697 GC.nary(TagConstants.ELEMTYPE,
2698 GC.nary(TagConstants.TYPEOF, array))),
2699 Location.NULL, lhs.array);
2700 }
2701
2702 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
2703 code.addElement(modify(GC.statevar,x.locOp));
2704 Expr a= GC.select(GC.elemsvar, array);
2705 return protect(protect, GC.select(a, index), x.locOp);
2706
2707 } else {
2708 Assert.fail("Unexpected tag " + TagConstants.toString(ltag)
2709 + " (" + ltag + ")");
2710 }
2711 }
2712
2713 case TagConstants.INC: case TagConstants.DEC:
2714 case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
2715 case TagConstants.ASGMUL:
2716 case TagConstants.ASGADD: case TagConstants.ASGSUB:
2717 case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
2718 case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
2719 case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR:
2720 case TagConstants.ASGDIV: case TagConstants.ASGREM:
2721 {
2722 Expr right, left;
2723 int op;
2724 int locOp;
2725 Type rType;
2726 if (expr instanceof UnaryExpr) {
2727 UnaryExpr u= (UnaryExpr) expr;
2728 right= GC.onelit;
2729 rType = Types.intType;
2730 left= u.expr;
2731 op= TrAnExpr.getGCTagForUnary(u);
2732 locOp = u.locOp;
2733 } else {
2734 BinaryExpr x= (BinaryExpr)expr;
2735 right= x.right;
2736 rType = TypeCheck.inst.getType(right);
2737 left= x.left;
2738 op= TrAnExpr.getGCTagForBinary(x);
2739 locOp = x.locOp;
2740 }
2741 Type lType = TypeCheck.inst.getType(left);
2742 boolean returnold= (tag == TagConstants.POSTFIXINC
2743 || tag == TagConstants.POSTFIXDEC);
2744
2745 int ltag = left.getTag();
2746 if (ltag == TagConstants.VARIABLEACCESS) {
2747 VariableAccess lhs= (VariableAccess)left;
2748 readCheck(lhs, lhs.getStartLoc());
2749
2750 Expr oldLval= protect(Purity.impure(right) || returnold, lhs,
2751 locOp, "old!" + lhs.decl.id.toString());
2752 Expr rval= trExpr(false, right);
2753
2754 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2755 Assert.notFalse(expr instanceof BinaryExpr);
2756 if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2757 addCheck(locOp, TagConstants.CHKARITHMETIC,
2758 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2759 }
2760 }
2761
2762 if (op == TagConstants.STRINGCAT) {
2763 rval = addNewString(expr,left,rval);
2764
2765 } else {
2766 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(), op, oldLval, rval);
2767 rval= addRelAsgCast(rval, lType, rType);
2768 }
2769
2770 writeCheck(lhs, null, rval, locOp, false);
2771 code.addElement(GC.gets(lhs, rval));
2772 if (returnold) {
2773 return oldLval;
2774 } else {
2775 return protect(protect, lhs, locOp, lhs.decl.id.toString() + "=");
2776 }
2777
2778 } else if (ltag == TagConstants.FIELDACCESS) {
2779 FieldAccess lhs = (FieldAccess)left;
2780 Expr lval= trFieldAccess(true, lhs);
2781 readCheck(lval, lhs.locId);
2782 // Add a check that the lhs is assignable
2783 frameHandler.modifiesCheckField(lval,lhs.getStartLoc(),
2784 ((FieldAccess)left).decl);
2785
2786 String name = lhs.decl.id.toString();
2787 Expr oldLval = protect(Purity.impure(right) || returnold, lval,
2788 locOp, "old!" + name);
2789 Expr rval= trExpr(false, right);
2790 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2791 Assert.notFalse(expr instanceof BinaryExpr);
2792 if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2793 addCheck(locOp, TagConstants.CHKARITHMETIC,
2794 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2795 }
2796 }
2797
2798 if (op == TagConstants.STRINGCAT) {
2799 rval = addNewString(expr,lval,rval);
2800
2801 } else {
2802 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(),
2803 op, oldLval, rval);
2804 rval= addRelAsgCast(rval, lType, rType);
2805 }
2806
2807 writeCheck(lval, null, rval, locOp, false);
2808 if (lval.getTag() == TagConstants.VARIABLEACCESS) {
2809 code.addElement(GC.gets((VariableAccess)lval, rval));
2810 } else {
2811 NaryExpr target= (NaryExpr)lval;
2812 VariableAccess field= (VariableAccess)target.exprs.elementAt(0);
2813 Expr obj= target.exprs.elementAt(1);
2814 code.addElement(GC.subgets(field, obj, rval));
2815 }
2816 code.addElement(modify(GC.statevar,locOp));
2817 if (returnold) {
2818 return oldLval;
2819 } else {
2820 return protect(protect, lval, locOp, name + "=");
2821 }
2822
2823 } else if (ltag == TagConstants.ARRAYREFEXPR) {
2824 ArrayRefExpr lhs= (ArrayRefExpr)left;
2825
2826 Expr array= trExpr(true, lhs.array);
2827 Expr index= trExpr(true, lhs.index);
2828 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
2829 // Add a check that the lhs is assignable
2830 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
2831 Expr oldLval = protect(Purity.impure(right) || returnold,
2832 GC.select(GC.select(GC.elemsvar, array),
2833 index),
2834 locOp, "old");
2835
2836 Expr rval= trExpr(false, right);
2837 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2838 Assert.notFalse(expr instanceof BinaryExpr);
2839 if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2840 addCheck(locOp, TagConstants.CHKARITHMETIC,
2841 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2842 }
2843 }
2844
2845 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(),
2846 op, oldLval, rval);
2847 rval= addRelAsgCast(rval, lType, rType);
2848
2849 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
2850 code.addElement(modify(GC.statevar,locOp));
2851 if (returnold) {
2852 return oldLval;
2853 } else {
2854 Expr a= GC.select(GC.elemsvar, array);
2855 return protect(protect, GC.select(a, index), locOp);
2856 }
2857
2858 } else {
2859 Assert.fail("Unexpected tag " + TagConstants.toString(ltag)
2860 + " (" + ltag + ")");
2861 }
2862 }
2863
2864 // Unary expressions
2865 case TagConstants.UNARYADD:
2866 {
2867 // drop UnaryADD
2868 UnaryExpr x= (UnaryExpr)expr;
2869 return trExpr(protect, x.expr);
2870 }
2871
2872 case TagConstants.UNARYSUB:
2873 case TagConstants.NOT: case TagConstants.BITNOT:
2874 {
2875 UnaryExpr x= (UnaryExpr)expr;
2876 Expr x2= trExpr(false, x.expr);
2877 int newtag= TrAnExpr.getGCTagForUnary(x);
2878 return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(),
2879 newtag, x2),
2880 x.locOp);
2881 }
2882
2883 case TagConstants.PARENEXPR:
2884 {
2885 ParenExpr x= (ParenExpr)expr;
2886 return trExpr(protect, x.expr);
2887 }
2888
2889 case TagConstants.VARIABLEACCESS:
2890 {
2891 VariableAccess x= (VariableAccess)expr;
2892 readCheck(x, x.getStartLoc());
2893 return protect(protect, x, x.getStartLoc(), x.decl.id.toString());
2894 }
2895
2896 case TagConstants.FIELDACCESS:
2897 {
2898 FieldAccess fa = (FieldAccess)expr;
2899 Expr result = trFieldAccess(false, fa);
2900 if (fa.decl != Types.lengthFieldDecl)
2901 readCheck(result, fa.locId);
2902 return protect(protect, result, fa.locId, fa.decl.id.toString());
2903 }
2904
2905 case TagConstants.METHODINVOCATION:
2906 {
2907 return trMethodInvocation(protect, (MethodInvocation)expr);
2908 }
2909
2910 default:
2911 //@ unreachable;
2912 Assert.fail("UnknownTag<" + TagConstants.toString(tag) + ">");
2913 return null;
2914 }
2915 }
2916
2917 private static Expr addRelAsgCast(Expr rval, Type lType, Type rType) {
2918 if (!(lType instanceof PrimitiveType))
2919 return rval;
2920
2921 switch (lType.getTag()) {
2922 case TagConstants.BYTETYPE:
2923 case TagConstants.SHORTTYPE:
2924 case TagConstants.CHARTYPE:
2925 break; // cast needed
2926 case TagConstants.INTTYPE:
2927 if (Types.isLongType(rType) || Types.isFloatingPointType(rType)) {
2928 break; // cast needed
2929 } else {
2930 return rval;
2931 }
2932 case TagConstants.LONGTYPE:
2933 if (Types.isFloatingPointType(rType)) {
2934 break; // cast needed
2935 } else {
2936 return rval;
2937 }
2938 case TagConstants.FLOATTYPE:
2939 case TagConstants.DOUBLETYPE:
2940 return rval;
2941 default:
2942 return rval;
2943 }
2944 return GC.nary(TagConstants.CAST, rval, GC.typeExpr(lType));
2945 }
2946
2947 /**
2948 * Returns the guarded-command expression:
2949 * <pre>
2950 * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
2951 * ==> isNewArray(o))
2952 * </pre>
2953 */
2954 private static Expr predEvathangsAnArray(VariableAccess allocOld,
2955 VariableAccess allocNew) {
2956 LocalVarDecl odecl = UniqName.newBoundVariable('o');
2957 VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL);
2958
2959 Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld));
2960 Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew);
2961 Expr e2 = GC.nary(TagConstants.ISNEWARRAY, o);
2962
2963 Expr body = GC.implies(GC.and(e0, e1), e2);
2964
2965 // TBW: "e2" should be the trigger of the following quantification
2966 return GC.forall(odecl, body);
2967 }
2968
2969
2970 /**
2971 * Returns the guarded-command expression:
2972 * <pre>
2973 * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
2974 * ==> o.owner == null)
2975 * </pre>
2976 */
2977 private static Expr predArrayOwnerNull(VariableAccess allocOld,
2978 VariableAccess allocNew,
2979 VariableAccess arr) {
2980 // get java.lang.Object
2981 TypeSig obj = Types.javaLangObject();
2982
2983 FieldDecl owner = null; // make the compiler happy
2984 boolean notFound = false;
2985 try {
2986 owner = Types.lookupField(obj, Identifier.intern("owner"),
2987 obj);
2988 }
2989 catch (javafe.tc.LookupException e) {
2990 notFound = true;
2991 }
2992 // if we couldn't find the owner ghost field, there's nothing to do
2993 if (notFound)
2994 return null;
2995
2996 VariableAccess ownerVA = TrAnExpr.makeVarAccess(owner, Location.NULL);
2997
2998 LocalVarDecl odecl = UniqName.newBoundVariable('o');
2999 VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL);
3000
3001 Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld));
3002 Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew);
3003 Expr e2 = GC.nary(TagConstants.REFEQ, GC.select(ownerVA, arr),
3004 GC.nulllit);
3005
3006
3007 Expr body = GC.implies(GC.and(e0, e1), e2);
3008
3009 return GC.forall(odecl, body);
3010 }
3011
3012 // @todo Should be moved type javafe.tc.Types
3013
3014 /**
3015 * @return true if there can be no subtypes of <code>t</code>.
3016 * @design The definition of final used by this method is as follows. Reference
3017 * types are "final" if they have the <code>final</code> modifier. Array types
3018 * are "final" if their element types satisfy <code>isFinal</code>. Primitive
3019 * types are "final".
3020 */
3021 public static boolean isFinal(/*@ non_null */ Type t) {
3022 int tag= t.getTag();
3023 switch (tag) {
3024 case TagConstants.BOOLEANTYPE:
3025 case TagConstants.INTTYPE:
3026 case TagConstants.LONGTYPE:
3027 case TagConstants.CHARTYPE:
3028 case TagConstants.FLOATTYPE:
3029 case TagConstants.DOUBLETYPE:
3030 case TagConstants.BYTETYPE:
3031 case TagConstants.SHORTTYPE:
3032 return true;
3033
3034 case TagConstants.ARRAYTYPE:
3035 return isFinal(((ArrayType)t).elemType);
3036
3037 case TagConstants.TYPENAME:
3038 t= TypeCheck.inst.getSig((TypeName)t);
3039 case TagConstants.TYPESIG:
3040 TypeSig ts= (TypeSig)t;
3041 return Modifiers.isFinal(ts.getTypeDecl().modifiers);
3042
3043 default:
3044 //@ unreachable;
3045 Assert.fail("Unexpected tag " + TagConstants.toString(tag) + " ("
3046 + tag + ")");
3047 return false;
3048 }
3049 }
3050
3051 //// Factor processing of FieldAccess nodes
3052
3053 /**
3054 * Returns either a <code>VariableAccess</code> if <code>fa</code> is a class
3055 * variable or a <code>SELECT</code> application if <code>fa</code> is an
3056 * instance variable access, or an <code>ARRAYLENGTH</code> application if
3057 * <code>fa</code> is the final array field <code>length</code>. In the second
3058 * case, will emit code for computing the object designator and also a check to
3059 * ensure that object is not null.
3060 */
3061 private Expr trFieldAccess(boolean protectObject,
3062 /*@ non_null */ FieldAccess fa) {
3063 VariableAccess va;
3064 Iterator iter = modifyEverythingLocations.iterator();
3065 if (iter.hasNext()) {
3066 va = TrAnExpr.makeVarAccess(fa.decl, fa.locId);
3067 EverythingLoc s = (EverythingLoc)iter.next();
3068 s.add(va);
3069
3070 } else {
3071 va = TrAnExpr.makeVarAccess(fa.decl, fa.locId);
3072 }
3073
3074 int tag= fa.od.getTag();
3075 if (Modifiers.isStatic(fa.decl.modifiers)) {
3076 // static field
3077 switch (tag) {
3078 case TagConstants.TYPEOBJECTDESIGNATOR:
3079 case TagConstants.SUPEROBJECTDESIGNATOR:
3080 break;
3081 case TagConstants.EXPROBJECTDESIGNATOR: {
3082 ExprObjectDesignator od= (ExprObjectDesignator)fa.od;
3083 Expr discardResult = trExpr(false, od.expr);
3084 break;
3085 }
3086 default:
3087 //@ unreachable;
3088 Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3089 + " (" + tag + ")");
3090 break;
3091 }
3092 return va;
3093
3094 } else {
3095 // instance variable
3096 Expr obj;
3097 switch (tag) {
3098 case TagConstants.EXPROBJECTDESIGNATOR: {
3099 ExprObjectDesignator od= (ExprObjectDesignator)fa.od;
3100 obj= trExpr(protectObject, od.expr);
3101 nullCheck(od.expr, obj, fa.od.locDot);
3102 break;
3103 }
3104 case TagConstants.SUPEROBJECTDESIGNATOR:
3105 obj= GC.thisvar;
3106 break;
3107 case TagConstants.TYPEOBJECTDESIGNATOR:
3108 // This case is not legal Java and should already have been
3109 // checked by the type checker
3110 //@ unreachable;
3111 Assert.fail("Unexpected tag");
3112 obj= null; // dummy assignment
3113 break;
3114 default:
3115 //@ unreachable;
3116 Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3117 + " (" + tag + ")");
3118 obj= null; // dummy assignment
3119 break;
3120 }
3121
3122 Expr res;
3123 if (fa.decl == Types.lengthFieldDecl) {
3124 return GC.nary(fa.getStartLoc(), fa.getEndLoc(),
3125 TagConstants.ARRAYLENGTH, obj);
3126 } else {
3127 return GC.nary(fa.getStartLoc(), fa.getEndLoc(),
3128 TagConstants.SELECT, va, obj);
3129 }
3130 }
3131 }
3132
3133 /**
3134 * This translation of method invocation follows section 4.1 of ESCJ 16.
3135 */
3136 private Expr trMethodInvocation(boolean protect,
3137 /*@ non_null */ MethodInvocation mi) {
3138 boolean isStatic = Modifiers.isStatic(mi.decl.modifiers);
3139
3140 // for holding the translated arguments
3141 ExprVec args = ExprVec.make(mi.args.size() + 1);
3142 ExprVec argsRaw = ExprVec.make(mi.args.size() + 1);
3143 Expr nullcheckArg = null; // Java expression
3144 /*-@ uninitialized */ int nullcheckLoc = Location.NULL;
3145 // FIXME /*@ readable nullcheckLoc if nullcheckArg != null; */
3146
3147 Expr eod = null;
3148 int tag= mi.od.getTag();
3149 switch (tag) {
3150 case TagConstants.TYPEOBJECTDESIGNATOR: {
3151 Assert.notFalse(isStatic); // non-static is not legal Java
3152 // the arguments are translated below
3153 break;
3154 }
3155 case TagConstants.EXPROBJECTDESIGNATOR: {
3156 ExprObjectDesignator od = (ExprObjectDesignator)mi.od;
3157 if (isStatic) {
3158 Expr discardResult = trExpr(false, od.expr);
3159 } else {
3160 // protect "self" if there are more arguments
3161 Expr self = trExpr(mi.args.size() != 0, od.expr);
3162 args.addElement(self);
3163 argsRaw.addElement(od.expr);
3164 nullcheckArg = od.expr;
3165 nullcheckLoc = od.locDot;
3166 eod = self;
3167 }
3168 // the (rest of) the arguments are translated below
3169 break;
3170 }
3171 case TagConstants.SUPEROBJECTDESIGNATOR: {
3172 if (! isStatic) {
3173 args.addElement(GC.thisvar);
3174 argsRaw.addElement(ThisExpr.make(null, mi.od.getStartLoc()));
3175 eod = GC.thisvar;
3176 }
3177 // the (rest of) the arguments are translated below
3178 break;
3179 }
3180 default:
3181 //@ unreachable;
3182 Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3183 + " (" + tag + ")");
3184 break;
3185 }
3186
3187 // translate remaining arguments
3188 for (int i = 0; i < mi.args.size(); i++) {
3189 // protect all but the last argument
3190 Expr argRaw = mi.args.elementAt(i);
3191 Expr arg = trExpr(i != mi.args.size()-1, argRaw);
3192 args.addElement(arg);
3193 argsRaw.addElement(argRaw);
3194 }
3195
3196 if (nullcheckArg != null) {
3197 nullCheck(nullcheckArg, args.elementAt(0), nullcheckLoc);
3198 }
3199
3200 InlineSettings is = (InlineSettings)inlineDecoration.get(mi);
3201 code.addElement( call( mi.decl, argsRaw, args, scope, mi.locId,
3202 mi.getEndLoc(), mi.locOpenParen, false, is, eod, false));
3203 return protect(protect, GC.resultvar, mi.locOpenParen,
3204 mi.decl.id.toString());
3205 }
3206
3207
3208 //// Helper methods for generating check assertions/assumptions
3209
3210 /**
3211 * Emit a check at location <code>loc</code> that guarded command expression
3212 * <code>e</code>, which was translated from the Java expression <code>E</code>,
3213 * is not <code>null</code>. If <code>E</code> denotes an expression that is
3214 * guaranteed not to be <code>null</code>, no check is emitted.
3215 */
3216 private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc) {
3217 nullCheck(E, e, loc, TagConstants.CHKNULLPOINTER, Location.NULL);
3218 }
3219
3220 private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc,
3221 int errorName, int locPragma) {
3222 // start by peeling off parentheses and casts
3223 E = trim(E);
3224
3225 switch (E.getTag()) {
3226 case TagConstants.THISEXPR:
3227 return;
3228
3229 case TagConstants.VARIABLEACCESS: {
3230 GenericVarDecl d = ((VariableAccess)E).decl;
3231 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d);
3232 if (nonNullPragma != null && !Main.options().guardedVC) {
3233 LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc());
3234 return;
3235 }
3236 break; // perform check
3237 }
3238
3239 case TagConstants.FIELDACCESS: {
3240 FieldDecl fd = ((FieldAccess)E).decl;
3241 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(fd);
3242 if (nonNullPragma != null && !Main.options().guardedVC) {
3243 if (Modifiers.isStatic(fd.modifiers) ||
3244 rdCurrent.getTag() != TagConstants.CONSTRUCTORDECL ||
3245 rdCurrent.parent != fd.parent) {
3246 LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc());
3247 return;
3248 }
3249 }
3250 break; // perform check
3251 }
3252
3253 default:
3254 break; // perform check
3255 }
3256
3257 Expr nullcheck = GC.nary(TagConstants.REFNE, e, GC.nulllit);
3258 addCheck(loc, errorName, nullcheck, locPragma, E);
3259 }
3260
3261 /**
3262 * Peels off parentheses and casts from <code>E</code> and returns the result
3263 */
3264 private VarInit trim(/*@ non_null */ VarInit E) {
3265 while (true) {
3266 if (E.getTag() == TagConstants.PARENEXPR) {
3267 E = ((ParenExpr)E).expr;
3268 } else if (E.getTag() == TagConstants.CASTEXPR) {
3269 E = ((CastExpr)E).expr;
3270 } else {
3271 return E;
3272 }
3273 }
3274 }
3275
3276 /**
3277 * Emit the checks that <code>array</code> is non-null and that
3278 * <code>index</code> is inbounds for <code>array</code>. Implements the
3279 * ArrayAccessCheck function of ESCJ16.
3280 */
3281 private void arrayAccessCheck(/*@ non_null */ Expr Array, /*@ non_null */ Expr array,
3282 /*@ non_null */ Expr Index, /*@ non_null */ Expr index,
3283 int locOpenBracket) {
3284 nullCheck(Array, array, locOpenBracket);
3285
3286 Expr length= GC.nary(TagConstants.ARRAYLENGTH, array);
3287 Expr indexNeg = GC.nary(TagConstants.INTEGRALLE, GC.zerolit, index);
3288 addCheck(locOpenBracket, TagConstants.CHKINDEXNEGATIVE, indexNeg,
3289 Location.NULL, trim(Index));
3290 Expr indexTooBig = GC.nary(TagConstants.INTEGRALLT, index, length);
3291 addCheck(locOpenBracket, TagConstants.CHKINDEXTOOBIG, indexTooBig);
3292 }
3293
3294 /**
3295 * Used by <code>readCheck</code> and <code>writeCheck</code> to accumulate the
3296 * list of mutexes protecting a shared variable. Thus, these methods are not
3297 * thread re-entrant.
3298 */
3299 private /*@ non_null */ ExprVec mutexList = ExprVec.make(5);
3300 private /*@ non_null */ ArrayList locList = new ArrayList(5);
3301
3302 /**
3303 * Insert checks done before reading variables.
3304 *
3305 * <p> This method implements ReadCheck as defined in ESCJ16. Handles reads of
3306 * local, class, and instance variables (ESCJ16 splits these into two ReadCheck
3307 * functions). </p>
3308 *
3309 * @param va is the variable being read; it must be either a
3310 * <code>VariableAccess</code> (in the case of local variables and class fields)
3311 * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance
3312 * fields).
3313 * @param locId is the location of the variable or field being read. It is used
3314 * to determine the location of the "wrong" part of the check's label.
3315 */
3316 private void readCheck(/*@ non_null */ Expr va, int locId) {
3317 Assert.notFalse(locId != Location.NULL);
3318 // "d" is the declaration of the variable being read
3319 GenericVarDecl d;
3320 Expr actualSelf = null;
3321 if (va.getTag() == TagConstants.SELECT) {
3322 NaryExpr sel= (NaryExpr)va;
3323 d= ((VariableAccess)sel.exprs.elementAt(0)).decl;
3324 actualSelf = sel.exprs.elementAt(1);
3325 } else {
3326 d= ((VariableAccess)va).decl;
3327 }
3328
3329 if (d.pmodifiers == null) return;
3330
3331 Hashtable map = null;
3332
3333 mutexList.removeAllElements();
3334 locList.clear();
3335 ModifierPragma firstMonitoredPragma = null;
3336 for (int i= 0; i < d.pmodifiers.size(); i++) {
3337 ModifierPragma prag= d.pmodifiers.elementAt(i);
3338 int tag= prag.getTag();
3339 switch (tag) {
3340 case TagConstants.NON_NULL:
3341 case TagConstants.NULLABLE:
3342 case TagConstants.SPEC_PUBLIC:
3343 case TagConstants.SPEC_PROTECTED:
3344 case TagConstants.WRITABLE_IF:
3345 break;
3346
3347 case TagConstants.UNINITIALIZED:
3348 // "uninitialized" can be used only with local variables
3349 Assert.notFalse(va.getTag() != TagConstants.SELECT);
3350 VariableAccess init= getInitVar((LocalVarDecl) d);
3351 addCheck(locId, TagConstants.CHKINITIALIZATION, init, prag);
3352 break;
3353
3354 case TagConstants.READABLE_IF:
3355 map = initializeRWCheckSubstMap(map, actualSelf, locId);
3356 Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null);
3357 addCheck(locId, TagConstants.CHKDEFINEDNESS, dc, prag);
3358 break;
3359
3360 case TagConstants.MONITORED_BY: {
3361 ExprModifierPragma emp = (ExprModifierPragma)prag;
3362 map = initializeRWCheckSubstMap(map, actualSelf, locId);
3363 mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null));
3364 locList.add(new Integer(emp.expr.getStartLoc()));
3365 if (firstMonitoredPragma == null)
3366 firstMonitoredPragma = prag;
3367 break;
3368 }
3369
3370 case TagConstants.MONITORED:
3371 Assert.notFalse(d instanceof FieldDecl);
3372 if (Modifiers.isStatic(d.modifiers)) {
3373 mutexList.addElement(
3374 GC.nary(TagConstants.CLASSLITERALFUNC,
3375 getClassObject(((FieldDecl)d).parent)));
3376 } else {
3377 mutexList.addElement(actualSelf);
3378 }
3379 locList.add(new Integer(prag.getStartLoc()));
3380 if (firstMonitoredPragma == null)
3381 firstMonitoredPragma = prag;
3382 break;
3383
3384 case TagConstants.INSTANCE:
3385 case TagConstants.IN:
3386 case TagConstants.MAPS:
3387 case TagConstants.GHOST:
3388 case TagConstants.MODEL:
3389 // ignore
3390 break;
3391
3392 default:
3393 Assert.fail("Unexpected tag \"" + TagConstants.toString(tag)
3394 + "\" (" + tag + ")");
3395 }
3396 }
3397
3398 if (mutexList.size() != 0) {
3399 Expr onelocked= GC.falselit;
3400 for (int i= mutexList.size()-1; 0 <= i; i--) {
3401 Expr mu= mutexList.elementAt(i);
3402 onelocked= GC.or(GC.and(GC.nary(TagConstants.REFNE, mu, GC.nulllit),
3403 GC.nary(TagConstants.SELECT, GC.LSvar, mu)),
3404 onelocked);
3405 }
3406 if (rdCurrent instanceof ConstructorDecl && actualSelf != null) {
3407 // In constructors, always allow access to the fields of the object
3408 // being constructed.
3409 // Note: The following could be optimized so that if "actualSelf"
3410 // is ``obviously'' "this", then the check could be omitted altogether.
3411 onelocked = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar),
3412 onelocked);
3413 }
3414 // For a read race, we have a race condition if none of the
3415 // monitors are locked. Since we can't point to all of them
3416 // we point to the beginning of the first monitored declaration,
3417 // rather than to a specific expresssion - will likely be
3418 // confusing to the user anyway.
3419 addCheck(locId, TagConstants.CHKSHARING, onelocked,
3420 firstMonitoredPragma);
3421 }
3422 mutexList.removeAllElements(); // Help the garbage collector...
3423 locList.clear(); // Help the garbage collector...
3424 }
3425
3426 /**
3427 * Insert checks done before writing variables, as prescribed by WriteCheck in
3428 * ESCJ 16. Handles writes of local, class, and instance variables (ESCJ 16
3429 * splits these into two WriteCheck functions).
3430 *
3431 * @param va is the variable being written; it must be either a
3432 * <code>VariableAccess</code> (in the case of local variables and class fields)
3433 * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance
3434 * fields).
3435 * @param rval is the guarded command expression being written into
3436 * <code>va</code>. The argument <code>Rval</code> is either the Java expression
3437 * from which <code>rval</code> was translated, or <code>null</code> if
3438 * <code>rval</code> was somehow synthesized.
3439 * @param locAssignOp is the location of the assignment operator that prescribes
3440 * the write. It is used to determine the location of the "wrong" part of the
3441 * check's label.
3442 * @param inInitializerContext indicates whether or not the expression whose
3443 * write check is to be performed is the initializing expression of a field.
3444 */
3445 private void writeCheck(/*@ non_null */ Expr va,
3446 VarInit Rval, Expr rval, int locAssignOp,
3447 boolean inInitializerContext) {
3448 Assert.notFalse(locAssignOp != Location.NULL);
3449 // "d" is the declaration of the variable being written
3450 GenericVarDecl d;
3451 Expr actualSelf = null;
3452 if (va.getTag() == TagConstants.SELECT) {
3453 NaryExpr sel= (NaryExpr)va;
3454 d= ((VariableAccess)sel.exprs.elementAt(0)).decl;
3455 actualSelf = sel.exprs.elementAt(1);
3456 } else {
3457 d= ((VariableAccess)va).decl;
3458 }
3459
3460 // Handle non_null variables
3461 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d);
3462 if (nonNullPragma != null) {
3463 if (Rval == null) {
3464 Expr nullcheck = GC.nary(TagConstants.REFNE, rval, GC.nulllit);
3465 addCheck(locAssignOp, TagConstants.CHKNONNULL, nullcheck,
3466 nonNullPragma.getStartLoc());
3467 } else if (!Main.options().excuseNullInitializers || !inInitializerContext ||
3468 trim(Rval).getTag() != TagConstants.NULLLIT) {
3469 nullCheck(Rval, rval, locAssignOp, TagConstants.CHKNONNULL,
3470 nonNullPragma.getStartLoc());
3471 }
3472 }
3473
3474 if (d.pmodifiers == null) return;
3475
3476 Hashtable map = null;
3477
3478 mutexList.removeAllElements();
3479 locList.clear();
3480 Expr onenotnull= GC.falselit;
3481 ModifierPragma firstMonitoredPragma = null;
3482 for (int i= 0; i < d.pmodifiers.size(); i++) {
3483 ModifierPragma prag= d.pmodifiers.elementAt(i);
3484 int tag= prag.getTag();
3485 switch (tag) {
3486 case TagConstants.IN:
3487 case TagConstants.MAPS:
3488 case TagConstants.INSTANCE:
3489 case TagConstants.UNINITIALIZED:
3490 case TagConstants.READABLE_IF:
3491 case TagConstants.SPEC_PUBLIC:
3492 case TagConstants.SPEC_PROTECTED:
3493 case TagConstants.GHOST:
3494 case TagConstants.NON_NULL: // handled above
3495 case TagConstants.NULLABLE:
3496 break;
3497
3498 case TagConstants.MODEL:
3499 ErrorSet.error(locAssignOp,"May not assign to a model variable");
3500 break;
3501
3502 case TagConstants.WRITABLE_IF:
3503 map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp);
3504 Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null);
3505 addCheck(locAssignOp, TagConstants.CHKWRITABLE, dc, prag);
3506 break;
3507
3508 case TagConstants.MONITORED_BY: {
3509 ExprModifierPragma emp = (ExprModifierPragma)prag;
3510 map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp);
3511 // We keep a list of locations in locList because the
3512 // translated expr (if it refers to this) may have a
3513 // dummy location and we want to be sure to have any
3514 // Race warning point to the actual object whose monitor
3515 // has not been acquired.
3516 mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null));
3517 locList.add(new Integer(emp.expr.getStartLoc()));
3518 if (firstMonitoredPragma == null)
3519 firstMonitoredPragma = prag;
3520 break;
3521 }
3522
3523 case TagConstants.MONITORED:
3524 Assert.notFalse(d instanceof FieldDecl);
3525 if (Modifiers.isStatic(d.modifiers)) {
3526 mutexList.addElement(GC.nary(
3527 TagConstants.CLASSLITERALFUNC,
3528 getClassObject(((FieldDecl)d).parent)));
3529 } else {
3530 mutexList.addElement(actualSelf);
3531 }
3532 locList.add(new Integer(prag.getStartLoc()));
3533 onenotnull= GC.truelit;
3534 if (firstMonitoredPragma == null)
3535 firstMonitoredPragma = prag;
3536 break;
3537
3538 default:
3539 Assert.fail("Unexpected tag \"" + TagConstants.toString(tag)
3540 + "\" (" + tag + ")");
3541 }
3542 }
3543
3544 if (mutexList.size() != 0) {
3545 Expr allnullorlocked= GC.truelit;
3546 boolean doConst = rdCurrent instanceof ConstructorDecl &&
3547 actualSelf != null;
3548 for (int i= mutexList.size()-1; 0 <= i; i--) {
3549 Expr mu= mutexList.elementAt(i);
3550 onenotnull= GC.or(GC.nary(TagConstants.REFNE, mu, GC.nulllit),
3551 onenotnull);
3552 Expr nullOrLocked =
3553 GC.or(GC.nary(TagConstants.REFEQ, mu, GC.nulllit),
3554 GC.select(GC.LSvar, mu));
3555 if (!doConst) {
3556 int loc = mu.getStartLoc();
3557 if (loc == Location.NULL) loc = ((Integer)locList.get(i)).intValue();
3558 addCheck(locAssignOp, TagConstants.CHKSHARING,
3559 nullOrLocked,loc);
3560 }
3561 allnullorlocked=
3562 GC.and(nullOrLocked, allnullorlocked);
3563 }
3564 Expr p = GC.and(onenotnull, allnullorlocked);
3565 if (doConst) {
3566 // In constructors, always allow access to the fields of the object
3567 // being constructed.
3568 // Note: The following could be optimized so that if "actualSelf"
3569 // is ``obviously'' "this", then the check could be omitted altogether.
3570 p = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar), p);
3571 addCheck(locAssignOp, TagConstants.CHKSHARING, p, firstMonitoredPragma);
3572 } else {
3573 addCheck(locAssignOp, TagConstants.CHKSHARINGALLNULL, onenotnull, firstMonitoredPragma);
3574 }
3575 }
3576 mutexList.removeAllElements(); // Help the garbage collector...
3577 locList.clear(); // Help the garbage collector...
3578 }
3579
3580 /**
3581 * The following method is used in readCheck and writeCheck to lazily construct a
3582 * substitution map (which may also create another temporary variable).
3583 */
3584 private Hashtable initializeRWCheckSubstMap(Hashtable prevMap,
3585 Expr actualSelf,
3586 int loc) {
3587 if (actualSelf == null) {
3588 // no map needed
3589 Assert.notFalse(prevMap == null);
3590 return null;
3591 } else if (prevMap != null) {
3592 return prevMap;
3593 } else {
3594 Hashtable map = new Hashtable();
3595 VariableAccess vaSelf;
3596 if (actualSelf instanceof VariableAccess) {
3597 vaSelf = (VariableAccess)actualSelf;
3598 } else {
3599 vaSelf = (VariableAccess)protect(true, actualSelf, loc, "od");
3600 }
3601 map.put(GC.thisvar.decl, vaSelf);
3602 return map;
3603 }
3604 }
3605
3606 /**
3607 * Calls <code>GC.check</code> to create a check and appends the result to
3608 * <code>code</code>.
3609 */
3610 //@ modifies code.elementCount;
3611 private void addCheck(int locUse, Condition cond) {
3612 code.addElement(GC.check(locUse, cond));
3613 }
3614
3615 /**
3616 * Calls <code>GC.check</code> to create a check and appends the result to
3617 * <code>code</code>.
3618 */
3619 //@ modifies code.elementCount;
3620 void addCheck(int locUse, int errorName, Expr pred) {
3621 addCheck(locUse, errorName, pred, Location.NULL);
3622 }
3623
3624 /**
3625 * Calls <code>GC.check</code> to create a check and appends the result to
3626 * <code>code</code>.
3627 */
3628 //@ modifies code.elementCount;
3629 private void addCheck(/*@ non_null */ ASTNode use, int errorName, Expr pred) {
3630 code.addElement(GC.check(use.getStartLoc(),
3631 errorName, pred,
3632 Location.NULL));
3633 }
3634
3635 /**
3636 * Calls <code>GC.check</code> to create a check and appends the result to
3637 * <code>code</code>.
3638 */
3639 //@ modifies code.elementCount;
3640 private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl) {
3641 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl));
3642 }
3643
3644 void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc) {
3645 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, auxLoc, null));
3646 }
3647
3648 /**
3649 * Calls <code>GC.check</code> to create a check and appends the result to
3650 * <code>code</code>.
3651 */
3652 //@ modifies code.elementCount;
3653 private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl,
3654 Object aux) {
3655 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, aux));
3656 }
3657
3658 /** Calls <code>GC.check</code> to create a check and appends the
3659 result to <code>code</code>. */
3660
3661 //@ modifies code.elementCount;
3662 private void addCheck(int locUse, int errorName, Expr pred,
3663 /*@ non_null */ ASTNode prag) {
3664 code.addElement(GC.check(locUse, errorName, pred, prag.getStartLoc()));
3665 }
3666
3667 private void addAssumption(Expr pred) {
3668 code.addElement(GC.assume(pred));
3669 //code.addElement(GC.check(pred.getStartLoc(),TagConstants.CHKCONSISTENT, pred,
3670 // Location.NULL, null));
3671 }
3672
3673 private void addAssumptions(ExprVec ev) {
3674 if (ev == null) return;
3675 for (int i=0; i<ev.size(); ++i) {
3676 addAssumption(ev.elementAt(i));
3677 }
3678 }
3679
3680 private void addNewAssumptions() {
3681 addNewAssumptionsHelper();
3682 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
3683 TrAnExpr.closeForClause();
3684 }
3685 ExprVec addNewAssumptionsNow() {
3686 addNewAssumptionsHelper();
3687 if (TrAnExpr.trSpecAuxAxiomsNeeded != null)
3688 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
3689 ExprVec ev = ExprVec.make(10);
3690 GetSpec.addAxioms(axsToAdd,ev);
3691 addNewAssumptionsNow(ev);
3692 TrAnExpr.closeForClause();
3693 return ev;
3694 }
3695 private void addNewAssumptionsNow(ExprVec ev) {
3696 //addNewAssumptionsHelper();
3697 for (int i=0; i<ev.size(); ++i) {
3698 addAssumption(ev.elementAt(i));
3699 }
3700 }
3701 private void addNewAssumptionsHelper() {
3702 if (TrAnExpr.trSpecModelVarsUsed != null) {
3703 // These assignments with a null rhs are used to indicate
3704 // that the target has some unknown new value.
3705 Iterator ii = TrAnExpr.trSpecModelVarsUsed.values().iterator();
3706 while (ii.hasNext()) {
3707 VariableAccess d = (VariableAccess)ii.next();
3708 code.addElement(GC.gets(d,null)); // FIXME - what about array model vars, static model vars
3709 }
3710 }
3711 addAssumptions(TrAnExpr.trSpecExprAuxConditions);
3712 addAssumptions(TrAnExpr.trSpecExprAuxAssumptions);
3713 }
3714 /**
3715 * Return the <code>VariableAccesss</code> associated with <code>d</code> by a
3716 * call to <code>setInitVar</code>. If none has been associated with
3717 * <code>d</code>, returns <code>null</code>.
3718 */
3719 private static VariableAccess getInitVar(GenericVarDecl d) {
3720 return (VariableAccess)Purity.translateDecoration.get(d);
3721 }
3722
3723 /**
3724 * Associates <code>init</code> with <code>d</code>; will be returned by a call
3725 * to <code>getInitVar</code>.
3726 */
3727 private static void setInitVar(GenericVarDecl d, VariableAccess init) {
3728 Purity.translateDecoration.set(d, init);
3729 }
3730
3731 /** Modifies a GC designator. GC designator can include SubstExpr. */
3732
3733 private GuardedCmd modify(/*@ non_null */ VariableAccess va, int loc) {
3734 VariableAccess newVal = temporary(va.id.toString(), loc, loc);
3735 return GC.gets(va, newVal);
3736 }
3737
3738 private GuardedCmd modify(/*@ non_null */ Expr e, Hashtable pt, int loc) {
3739 VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(loc),
3740 e.getStartLoc(), e.getStartLoc());
3741
3742 int etag = e.getTag();
3743 if (etag == TagConstants.VARIABLEACCESS) {
3744 // "e" is a single variable
3745 return GC.gets( (VariableAccess)e, newVal );
3746 }
3747
3748 Assert.notFalse(etag == TagConstants.SELECT);
3749 NaryExpr nary = (NaryExpr)e;
3750 e = nary.exprs.elementAt(0);
3751 Expr index = nary.exprs.elementAt(1);
3752 if (pt != null) {
3753 index = GC.subst(Location.NULL, Location.NULL, pt, index);
3754 }
3755 etag = e.getTag();
3756 if (etag == TagConstants.VARIABLEACCESS) {
3757 // The given "e" had the form "f[index]"
3758 return GC.subgets((VariableAccess)e, index, newVal);
3759 }
3760
3761 // The given "e" had the form "elems[array][index]"
3762 //Assert.notFalse(etag == TagConstants.SELECT);
3763 //nary = (NaryExpr)e;
3764 //VariableAccess elems = (VariableAccess)nary.exprs.elementAt(0);
3765 //Expr array = nary.exprs.elementAt(1);
3766 //if (pt != null) {
3767 // array = GC.subst(Location.NULL, Location.NULL, pt, array);
3768 //}
3769 //return GC.subsubgets(elems, array, index, newVal);
3770 return null;
3771 }
3772
3773
3774 // the inlining depth at which to perform checking.
3775 public int inlineCheckDepth = 0;
3776 // the number of levels of inlining after the level that is checked.
3777 public int inlineDepthPastCheck = 0;
3778
3779 /**
3780 * Creates and desugars a call node, extended to allow the possibility of
3781 * inlining a call.
3782 */
3783 private Call call(RoutineDecl rd, ExprVec argsRaw, ExprVec args,
3784 FindContributors scope,
3785 int scall, int ecall, int locOpenParen,
3786 boolean superOrSiblingConstructorCall,
3787 InlineSettings inline, Expr eod, boolean freshResult) {
3788 // save the current status of checking assertions
3789 boolean useGlobalStatus = NoWarn.useGlobalStatus;
3790
3791 // obtain the appropriate inlining flags
3792 inline = computeInlineSettings(rd, argsRaw, inline, scall);
3793
3794 // create call
3795 Call call = Call.make( args, scall, ecall, inline != null);
3796 call.rd = rd;
3797
3798 // now figure out desugared part
3799
3800 String description;
3801 Spec spec;
3802 if (inline != null) {
3803 if (inline.getSpecForInline) {
3804 //System.out.println("GETTING SPEC FOR INLINE");
3805 spec = GetSpec.getSpecForInline(call.rd, scope);
3806 } else {
3807 Set synTargs = predictedSynTargs;
3808 if (synTargs == null)
3809 synTargs = new Set();
3810 //System.out.println("GETTING SPEC FOR BODY");
3811 spec = GetSpec.getSpecForBody(call.rd, scope, synTargs, null);
3812 }
3813 description = "inlined call";
3814 }
3815 else {
3816 //System.out.println("GETTING SPEC FOR CALL " + Location.toString(call.rd.loc) );
3817 spec = GetSpec.getSpecForCall( call.rd, scope, predictedSynTargs );
3818 if (spec.modifiesEverything) {
3819 ErrorSet.caution(scall,
3820 "A method that 'modifies everything' has been called; the verification of a body with such a call is not correct.");
3821 }
3822 description = "call";
3823 }
3824 call.spec = spec;
3825
3826 Assert.notFalse( spec.dmd.args.size() == call.args.size(),
3827 "formal args: " + spec.dmd.args.size()
3828 + " actualargs: " + call.args.size() );
3829
3830
3831 // now start creating code and temporaries
3832 code.push(); // this mark popped by "spill"
3833 temporaries.push(); // this mark popped by "spill"
3834
3835 // create pt = { p* -> p*@L, wt*@pre -> wt*@L }
3836
3837 Vector ptDomain = new Vector();
3838 for(int i=0; i<spec.dmd.args.size(); i++)
3839 ptDomain.addElement( spec.dmd.args.elementAt(i) );
3840
3841 // spec.preVarMap gives the set of locations that are in modifies clauses for the
3842 // called routine
3843 for(Enumeration e = spec.preVarMap.elements(); e.hasMoreElements(); )
3844 ptDomain.addElement( ((VariableAccess)e.nextElement()).decl );
3845 Hashtable pt = GetSpec.makeSubst( ptDomain.elements(),
3846 UniqName.locToSuffix(call.scall) );
3847
3848 /* if the dontCheckPreconditions flag is set, turn off the following
3849 checks for non_null parameters and preconditions */
3850 if (inline != null) {
3851 globallyTurnOffChecks(inline.dontCheckPreconditions);
3852 }
3853
3854 // var p*@L = e* in
3855 Hashtable argsMap = new Hashtable();
3856 VariableAccess[] piLs = new VariableAccess[ call.args.size() ];
3857 for(int i=0; i<spec.dmd.args.size(); i++) {
3858 GenericVarDecl pi = spec.dmd.args.elementAt(i);
3859 piLs[i] = (VariableAccess)pt.get( pi );
3860 temporaries.addElement( piLs[i].decl );
3861 /* non_null pragmas are handled by desugaring now
3862 SimpleModifierPragma nonnull = null; // GetSpec.NonNullPragma(pi);
3863 if (nonnull != null && !pi.id.toString().equals("this$0arg")) {
3864 Expr argRaw = argsRaw.elementAt(i);
3865 nullCheck(argRaw, call.args.elementAt(i),
3866 argRaw.getStartLoc(),
3867 TagConstants.CHKNONNULL, nonnull.getStartLoc());
3868 }
3869 */
3870 argsMap.put(pi,piLs[i]);
3871 code.addElement(GC.gets(piLs[i], call.args.elementAt(i)));
3872 }
3873
3874 if (spec.dmd.isConstructor()) {
3875 code.addElement(GC.gets(GC.resultvar, eod));
3876 }
3877
3878 for (int i=0; i<spec.preAssumptions.size(); ++i) {
3879 addAssumption(spec.preAssumptions.elementAt(i));
3880 }
3881
3882 // check all preconditions
3883 for(int i=0; i<spec.pre.size(); i++) {
3884 Condition cond = spec.pre.elementAt(i);
3885 int label = cond.label;
3886 if (cond.label == TagConstants.CHKEXPRDEFINEDNESS) {
3887 // We do not need to check for definedness of the precondition of a called
3888 // method since such a definedness check will be done when the called
3889 // method spec is checked.
3890 continue;
3891 }
3892 Expr p = cond.pred;
3893 if (cond.label == TagConstants.CHKPRECONDITION) {
3894 p = mapLocation(p,locOpenParen);
3895 label = TagConstants.CHKQUIET;
3896 }
3897 addCheck(locOpenParen,
3898 label,
3899 GC.subst( call.scall, call.ecall, pt, p ),
3900 cond.locPragmaDecl);
3901 }
3902
3903 // Add a check that all the locations that might be assigned by the callee
3904 // are allowed to be assigned by the caller
3905 DerivedMethodDecl calledSpecs = GetSpec.getCombinedMethodDecl(rd);
3906 frameHandler.modifiesCheckMethodI(calledSpecs.modifies,
3907 eod, locOpenParen, pt,freshResult, rd.parent);
3908
3909 if (inline != null && Main.options().traceInfo > 0) {
3910 // add a label to say that a routine is being called
3911 GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall,
3912 "Call", call.scall);
3913 code.addElement(g);
3914 }
3915
3916
3917 // var w*@L = w in
3918 for(Enumeration e = spec.preVarMap.keys(); e.hasMoreElements(); )
3919 {
3920 GenericVarDecl w = (GenericVarDecl)e.nextElement();
3921 VariableAccess wPre = (VariableAccess)spec.preVarMap.get(w);
3922 VariableAccess wL = (VariableAccess)pt.get( wPre.decl );
3923 Assert.notNull( wL );
3924 VariableAccess wAccess = VariableAccess.make( w.id, call.scall, w );
3925
3926 temporaries.addElement( wL.decl );
3927 code.addElement( GC.gets( wL, wAccess ) );
3928 }
3929
3930 // restore original checking of warnings
3931 NoWarn.useGlobalStatus = useGlobalStatus;
3932
3933
3934 if (inline != null) {
3935
3936 // insert the translated body, with appropriate substitutions of
3937 // formals for the new names provided above
3938 Translate trInline = new Translate();
3939 trInline.inlineCheckDepth = inline.nextInlineCheckDepth;
3940 trInline.inlineDepthPastCheck = inline.nextInlineDepthPastCheck;
3941
3942 // turn off body checks if the appropriate flag is set
3943 globallyTurnOffChecks(inline.dontCheckInlinedBody);
3944
3945 GuardedCmd body = trInline.trBody(rd, scope, null, predictedSynTargs,
3946 this, this.issueCautions);
3947 body = substituteGC(pt, body);
3948 code.addElement(body);
3949
3950 for (int i=0; i<spec.postAssumptions.size(); ++i) {
3951 addAssumption(spec.postAssumptions.elementAt(i));
3952 }
3953
3954 // check all postconditions
3955 for(int i=0; i<spec.post.size(); i++) {
3956 Condition cond = spec.post.elementAt(i);
3957 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) continue;
3958 addCheck(rd.getEndLoc(),
3959 cond.label,
3960 GC.subst( call.scall, call.ecall, pt, cond.pred),
3961 cond.locPragmaDecl);
3962 }
3963 if (Main.options().traceInfo > 1) {
3964 // add a label to say that the inlined call has returned
3965 GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall,
3966 "CallReturn", call.scall);
3967 code.addElement(g);
3968 }
3969 // restore original checking of warnings
3970 NoWarn.useGlobalStatus = useGlobalStatus;
3971 }
3972
3973 else {
3974 Type savedType = GC.thisvar.decl.type;
3975
3976 // We need to evaluate all of the expressions in the
3977 // modifies clauses before we set the locations that are
3978 // in the modifies clauses to arbitrary values, since
3979 // some of the expressions might also be modified.
3980 // For example, a clause might be modifies i,a[i];
3981 // We don't try to see what expressions are modified;
3982 // we simply translate all of them, assigning the results
3983 // to some temporary variables. Those temporary variables
3984 // are then used later.
3985
3986 // For each item in the modifies clauses we add 0 or more
3987 // items to the translations and locations lists. Later
3988 // we iterate over the modifies clauses again, in precisely
3989 // the same order - being sure to take off EXACTLY the same
3990 // items as we put on, for each kind of entry in the modifies
3991 // clause.
3992 /* System.out.println("ARGS " );
3993 { java.util.Iterator im = argsMap.keySet().iterator();
3994 while (im.hasNext()) {
3995 Object o = im.next();
3996 System.out.println("ITEM " + o + " ::: " + argsMap.get(o));
3997 }
3998 }*/
3999 Expr thisTrans = eod;
4000 /* System.out.println("THISTRSANS");
4001 if (thisTrans != null) EscPrettyPrint.inst.print(System.out,0,thisTrans);
4002 System.out.println("");*/
4003 LinkedList translations = new LinkedList();
4004 LinkedList locations = new LinkedList();
4005 ModifiesGroupPragmaVec mgpv = calledSpecs.modifies;
4006 for (int i=0; i<mgpv.size(); ++i) {
4007 GC.thisvar.decl.type = TypeSig.getSig(calledSpecs.getContainingClass());
4008 ModifiesGroupPragma mgp = mgpv.elementAt(i);
4009 Expr precondition = mgp.precondition;
4010 precondition = TrAnExpr.trSpecExpr(precondition,argsMap,argsMap,eod);
4011 codevec = GuardedCmdVec.make();
4012 Frame.ModifiesIterator iter = new Frame.ModifiesIterator(
4013 rd.parent,mgp.items,true,true);
4014 while (iter.hasNext()) {
4015 Object o = iter.next();
4016 if (o instanceof FieldAccess) {
4017 FieldAccess fa = (FieldAccess)o;
4018 //System.out.println("FIELD ACCESS " + fa + " " + Location.toString(fa.getStartLoc()) + " " + Location.toString(fa.decl.getStartLoc()));
4019 Expr b = TrAnExpr.trSpecExpr(fa,argsMap,argsMap,eod);
4020 if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.SELECT) {
4021 // instance fields
4022 NaryExpr n = (NaryExpr)b;
4023 translations.add(n.exprs.elementAt(0));
4024 translations.add(cacheValue(n.exprs.elementAt(1)));
4025 locations.add(new Integer(fa.getStartLoc()));
4026 } else if (b instanceof VariableAccess) {
4027 // static fields
4028 translations.add(b);
4029 translations.add(null);
4030 locations.add(new Integer(fa.getStartLoc()));
4031 } else if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.METHODCALL) {
4032 // model variable - skip
4033 translations.add(null);
4034 } else {
4035 translations.add(null);
4036 // FIXME - turn into an internal error
4037 System.out.println("UNSPPORTRED-EB " + b.getClass() + " " + TagConstants.toString(((NaryExpr)b).op));
4038 escjava.ast.EscPrettyPrint.inst.print(System.out,0,b);
4039 System.out.println("");
4040 }
4041 } else if (o instanceof ArrayRefExpr) {
4042 // array elements like a[i]
4043 ArrayRefExpr arr = (ArrayRefExpr)o;
4044 Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans);
4045 Expr index = arr.index == null ? GC.zerolit :
4046 TrAnExpr.trSpecExpr(arr.index,argsMap,argsMap,thisTrans);
4047 translations.add(cacheValue(a));
4048 locations.add(new Integer(arr.getStartLoc()));
4049 translations.add(cacheValue(index));
4050 } else if (o instanceof ArrayRangeRefExpr){
4051 // array ranges like a[i..j] or a[*]
4052 ArrayRangeRefExpr arr = (ArrayRangeRefExpr)o;
4053 Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans);
4054 Expr low = arr.lowIndex == null ? GC.zerolit :
4055 TrAnExpr.trSpecExpr(arr.lowIndex,argsMap,argsMap,thisTrans);
4056 Expr hi = arr.highIndex == null ?
4057 GC.nary(TagConstants.INTEGRALSUB,GC.nary(TagConstants.ARRAYLENGTH,a),GC.onelit) :
4058 TrAnExpr.trSpecExpr(arr.highIndex,argsMap,argsMap,thisTrans);
4059 translations.add(cacheValue(a));
4060 translations.add(cacheValue(low));
4061 translations.add(cacheValue(hi));
4062 } else if (o instanceof NothingExpr) {
4063 // skip
4064 } else if (o instanceof EverythingExpr) {
4065 // skip
4066 } else if (o instanceof WildRefExpr) {
4067 // store refs like a.* or this.* or Type.* or super.*
4068 // skip - the wildref expression is expanded into
4069 // all of the fields by the iterator
4070 } else {
4071 // FIXME - turn into internal error
4072 System.out.println("UNSUPPORTED " + o.getClass());
4073 }
4074 }
4075
4076 GC.thisvar.decl.type = savedType; // FIXME - put in finally clause?
4077
4078 // An assignment generated for each modified target
4079 // of the form i:7.19 = after@16.2:20.19
4080
4081 // Here we handle special variables like alloc and state
4082 for (int ii=0; ii<spec.specialTargets.size(); ii++) {
4083 Expr target = spec.specialTargets.elementAt(ii);
4084 GuardedCmd gc = modify(target, pt, scall);
4085
4086 if (gc != null) codevec.addElement(gc);
4087 }
4088
4089 // Here we set everything in the modifies clauses to
4090 // unspecified values. For instance, for simple variables
4091 // we add the command: i:7.19 = after@16.2:20.19
4092 // There is nothing specified about the after variables.
4093 iter = new Frame.ModifiesIterator(rd.parent,mgp.items,true,true);
4094 while (iter.hasNext()) {
4095 Object o = iter.next();
4096 if (o instanceof FieldAccess) {
4097 VariableAccess a = (VariableAccess)translations.removeFirst();
4098 if (a != null) {
4099 Expr obj = (Expr)translations.removeFirst();
4100 // if obj == null, the variable is static
4101 int loc = ((Integer)(locations.removeFirst())).intValue();
4102 VariableAccess newVal =
4103 temporary("after@" + UniqName.locToSuffix(scall),
4104 loc, loc);
4105 GuardedCmd g = obj != null ?
4106 GC.subgets(a, obj, newVal ) :
4107 GC.gets(a, newVal);
4108 codevec.addElement(g);
4109 }
4110 } else if (o instanceof ArrayRefExpr) {
4111 Expr a = (Expr)translations.removeFirst();
4112 Expr index = (Expr)translations.removeFirst();
4113 int loc = ((Integer)(locations.removeFirst())).intValue();
4114 VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(scall),
4115 loc, loc);
4116 GuardedCmd g = GC.subsubgets(GC.elemsvar, a, index, newVal);
4117 codevec.addElement(g);
4118 } else if (o instanceof ArrayRangeRefExpr){
4119 // This one is slightly different. The array a is
4120 // replaced by a new array unset(a,low,hi).
4121 // In the background predicate, unset(a,i,j) has the
4122 // same array elements as a, except for values between
4123 // i and j, inclusive.
4124 Expr a = (Expr)translations.removeFirst();
4125 Expr low = (Expr)translations.removeFirst();
4126 Expr hi = (Expr)translations.removeFirst();
4127 GuardedCmd g = GC.subgets(GC.elemsvar, a, GC.nary(TagConstants.UNSET, GC.select(GC.elemsvar,a), low, hi));
4128 codevec.addElement(g);
4129 } else if (o instanceof NothingExpr) {
4130 // skip
4131 } else if (o instanceof EverythingExpr) {
4132 // FIXME !!!
4133 } else if (o instanceof WildRefExpr) {
4134 // skip - the wildref expression is expanded into
4135 // all of the fields by the iterator
4136 } else {
4137 // FIXME - turn into an internal error
4138 System.out.println("UNSUPPORTED " + o.getClass());
4139 }
4140 }
4141 GuardedCmd seq = GC.seq(codevec);
4142 GuardedCmd ifcmd = GC.ifcmd(precondition,seq,GC.skip());
4143 code.addElement(ifcmd);
4144 }
4145
4146 if (spec.modifiesEverything) {
4147 EverythingLoc el = new EverythingLoc(scall,pt);
4148 modifyEverythingLocations.add(el);
4149 el.completed.add(GC.ecvar);
4150 el.completed.add(GC.resultvar);
4151 el.completed.add(GC.xresultvar);
4152 code.addElement(el.gcseq);
4153 Iterator iter = spec.postconditionLocations.iterator();
4154 while (iter.hasNext()) {
4155 Object o = iter.next();
4156 if (o instanceof Expr) el.add((Expr)o);
4157 else System.out.println("WHAT? " + o.getClass() + " " + o);
4158 // FIXME
4159 }
4160
4161 }
4162
4163 // modify EC, RES, XRES
4164 code.addElement(modify(GC.ecvar, scall));
4165 if (!spec.dmd.isConstructor()) {
4166 if (freshResult) code.addElement(GC.gets(GC.resultvar, eod));
4167 else {
4168 code.addElement(modify(GC.resultvar, scall));
4169 }
4170 }
4171 code.addElement(modify(GC.xresultvar, scall));
4172
4173 // FIXME - we might be doing statevar twice - once
4174 // up above before the assignments of after values to
4175 // all the items in the modifies clause
4176 if (!Utils.isPure(rd))
4177 code.addElement(modify(GC.statevar, scall));
4178
4179 for (int i=0; i<spec.postAssumptions.size(); ++i) {
4180 addAssumption(spec.postAssumptions.elementAt(i));
4181 }
4182
4183 // FIXME - do we need this - I think we already do it
4184 // FIXME - figure out why this needs Exception instead of Throwable
4185
4186 addAssumption(
4187 GC.or(
4188 GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_return),
4189 GC.and(
4190 GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_throw),
4191 GC.nary(TagConstants.TYPELE,
4192 GC.nary(TagConstants.TYPEOF,GC.xresultvar),
4193 GC.typeExpr(
4194 Main.options().useThrowable ?
4195 Types.javaLangThrowable() : Types.javaLangException() )
4196 )
4197 )
4198 )
4199 );
4200
4201 // assume postconditions
4202 Condition exceptionCondition = null;
4203 for(int i=0; i<spec.post.size(); i++) {
4204 Condition cond = spec.post.elementAt(i);
4205 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION) {
4206 continue;
4207 }
4208 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) {
4209 exceptionCondition = cond;
4210 continue;
4211 }
4212 code.addElement(GC.assumeAnnotation(cond.locPragmaDecl,
4213 GC.subst(call.scall, call.ecall,
4214 pt, cond.pred)));
4215 }
4216 if (exceptionCondition != null &&
4217 NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2) ==
4218 TagConstants.CHK_AS_ASSERT) {
4219 Condition cond = exceptionCondition;
4220 int loc = rd.locThrowsKeyword;
4221 if (loc == Location.NULL) loc = rd.getStartLoc();
4222 addCheck(call.scall,
4223 TagConstants.CHKUNEXPECTEDEXCEPTION2,
4224 GC.subst( call.scall, call.ecall, pt, cond.pred),
4225 loc);
4226 }
4227 }
4228
4229 if( spec.dmd.throwsSet != null && spec.dmd.throwsSet.size() != 0 ) {
4230 // #if (! superOrSiblingConstructorCall)
4231 // assume EC == ec$return [] assume EC == ec$throw; raise
4232 // #else
4233 // assume EC == ec$return []
4234 // assume EC == ec$throw; assume !isAllocated(objectToBeConstructed, alloc); raise
4235 // #end
4236
4237 code.push();
4238 code.addElement( GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return )));
4239
4240 code.push();
4241 if (Main.options().traceInfo > 0) {
4242 // add a label to track whether the method invocation throws an
4243 // exception
4244 GuardedCmd g = traceInfoLabelCmd(scall, ecall,
4245 "RoutineException", scall);
4246 code.addElement(g);
4247 }
4248 GuardedCmd cmd = GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw ));
4249 code.addElement( cmd );
4250
4251 if (superOrSiblingConstructorCall) {
4252 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED,
4253 GC.objectTBCvar, GC.allocvar);
4254 code.addElement(GC.assume(GC.not(isAllocated)));
4255 }
4256 code.addElement( GC.raise() );
4257
4258 code.addElement( GC.boxPopFromStackVector(code) );
4259 }
4260
4261 // extract code and temporaries created, and put into call.desugared
4262
4263 call.desugared = DynInstCmd.make(UniqName.locToSuffix(call.scall), spill());
4264
4265 // all done
4266 return call;
4267 }
4268
4269 /**
4270 * Computes the inlining settings for a given call. A return value of
4271 * <code>null</code> means "don't inline".
4272 */
4273 private InlineSettings computeInlineSettings(/*@ non_null */ RoutineDecl rd,
4274 /*@ non_null */ ExprVec argsRaw,
4275 InlineSettings inline,
4276 int scall) {
4277 // Try to use the given inline settings, but bag out if the routine
4278 // doesn't have a body
4279 if (inline != null) {
4280 if (rd.body == null) {
4281 // if we don't have the routine's body, we can't inline it
4282 // (does this ever happen? --jbs)
4283 if (this.issueCautions) {
4284 ErrorSet.caution(scall, "Couldn't inline call because the routine's body was not found");
4285 }
4286 return null;
4287 }
4288 // TBW: should there be a check for isRecursiveInvocation here?
4289 return new InlineSettings(inline,
4290 inlineCheckDepth, inlineDepthPastCheck);
4291 }
4292
4293 if (rd.body == null) {
4294 return null;
4295 }
4296
4297 // Set the inlining bits appropriately, according to any given "helper"
4298 // pragma, but only if this is a non-recursive call.
4299 if (Helper.isHelper(rd) && !isRecursiveInvocation(rd)) {
4300 return new InlineSettings(false, false, true,
4301 inlineCheckDepth, inlineDepthPastCheck);
4302 }
4303
4304 // Set the inlining bits appropriately, according to the
4305 // flag -inlineFromConstructors.
4306 if (Main.options().inlineFromConstructors && inConstructorContext &&
4307 !isRecursiveInvocation(rd)) {
4308 // inline if "rd" is an instance method in the same class as rdCurrent
4309 if (rd instanceof MethodDecl && !Modifiers.isStatic(rd.modifiers) &&
4310 rd.parent == rdCurrent.parent) {
4311 // ...and the method is not overridable
4312 if (!FlowInsensitiveChecks.isOverridable((MethodDecl)rd)) {
4313 // ...and the method is clearly being invoked on the "this" object
4314 Assert.notFalse(1 <= argsRaw.size()); // it's an instance method!
4315 VarInit e0 = argsRaw.elementAt(0);
4316 e0 = trim(e0);
4317 if (e0.getTag() == TagConstants.THISEXPR &&
4318 ((ThisExpr)e0).classPrefix == null) {
4319 // inline it!
4320 return new InlineSettings(false, false, true,
4321 inlineCheckDepth, inlineDepthPastCheck);
4322 }
4323 }
4324 }
4325 }
4326
4327 // Set the inlining bits appropriately, according to the two
4328 // inlining depth flags.
4329 // Also set the inlining depth flags for the next level appropriately.
4330 // We don't inline constructors because of problems with checking
4331 // the constructor for Object.
4332 if ((inlineCheckDepth > 0 || inlineDepthPastCheck > 0) &&
4333 rd instanceof MethodDecl && rd.body != null) {
4334
4335 InlineSettings is = new InlineSettings(true, true, true,
4336 inlineCheckDepth,
4337 inlineDepthPastCheck);
4338 if (inlineCheckDepth > 1) {
4339 // don't check anything until we've reached the check depth
4340 is.nextInlineCheckDepth--;
4341 } else if (inlineCheckDepth == 1) {
4342 // check the body at the check depth
4343 is.dontCheckInlinedBody = false;
4344 is.getSpecForInline = false;
4345 is.nextInlineCheckDepth--;
4346 } else if (inlineCheckDepth == 0) {
4347 // check the preconditions of calls from the check depth
4348 is.dontCheckPreconditions = false;
4349 is.nextInlineCheckDepth--;
4350 is.nextInlineDepthPastCheck--;
4351 } else {
4352 // don't check anything lower than the check depth
4353 is.nextInlineDepthPastCheck--;
4354 }
4355
4356 return is;
4357 }
4358
4359 // don't inline
4360 return null;
4361 }
4362
4363 /**
4364 * If the flag is true, set all assertion checks to assumes. Otherwise, make
4365 * sure that regular checking of assertions is performed.
4366 */
4367 public static void globallyTurnOffChecks(boolean flag) {
4368 if (flag) {
4369 // turn precondition checks into assumes
4370 NoWarn.useGlobalStatus = true;
4371 NoWarn.globalStatus = TagConstants.CHK_AS_ASSUME;
4372 }
4373 else
4374 NoWarn.useGlobalStatus = false;
4375 }
4376
4377 /**
4378 * When a call is inlined, we need to substitute the new names given to its
4379 * formal parameters for its original names in the inlined body.
4380 */
4381 private static GuardedCmd substituteGC(/*@ non_null */ Hashtable pt,
4382 /*@ non_null */ GuardedCmd gc) {
4383 int tag = gc.getTag();
4384 switch (tag) {
4385 case TagConstants.SKIPCMD:
4386 case TagConstants.RAISECMD:
4387 return gc;
4388 case TagConstants.ASSERTCMD:
4389 case TagConstants.ASSUMECMD:
4390 {
4391 ExprCmd exprcmd = (ExprCmd) gc;
4392 return ExprCmd.make(exprcmd.cmd,
4393 Substitute.doSubst(pt, exprcmd.pred),
4394 exprcmd.loc);
4395 }
4396 case TagConstants.GETSCMD:
4397 {
4398 GetsCmd getscmd = (GetsCmd) gc;
4399 return GetsCmd.make((VariableAccess)
4400 Substitute.doSubst(pt, getscmd.v),
4401 Substitute.doSubst(pt, getscmd.rhs));
4402 }
4403 case TagConstants.SUBGETSCMD:
4404 {
4405 SubGetsCmd sgetscmd = (SubGetsCmd) gc;
4406 return SubGetsCmd.make((VariableAccess)
4407 Substitute.doSubst(pt, sgetscmd.v),
4408 Substitute.doSubst(pt, sgetscmd.rhs),
4409 Substitute.doSubst(pt, sgetscmd.index));
4410 }
4411 case TagConstants.SUBSUBGETSCMD:
4412 {
4413 SubSubGetsCmd ssgetscmd = (SubSubGetsCmd) gc;
4414 return SubSubGetsCmd.make((VariableAccess)
4415 Substitute.doSubst(pt, ssgetscmd.v),
4416 Substitute.doSubst(pt, ssgetscmd.rhs),
4417 Substitute.doSubst(pt, ssgetscmd.index1),
4418 Substitute.doSubst(pt, ssgetscmd.index2));
4419 }
4420 case TagConstants.RESTOREFROMCMD:
4421 {
4422 RestoreFromCmd rfcmd = (RestoreFromCmd) gc;
4423 return RestoreFromCmd.make((VariableAccess)
4424 Substitute.doSubst(pt, rfcmd.v),
4425 Substitute.doSubst(pt, rfcmd.rhs));
4426 }
4427 case TagConstants.SEQCMD:
4428 {
4429 SeqCmd scmd = (SeqCmd) gc;
4430 int size = scmd.cmds.size();
4431 GuardedCmdVec vec = GuardedCmdVec.make(size);
4432 for (int i = 0; i < size; i++)
4433 vec.addElement(substituteGC(pt, scmd.cmds.elementAt(i)));
4434 return SeqCmd.make(vec);
4435 }
4436 case TagConstants.VARINCMD:
4437 {
4438 VarInCmd vicmd = (VarInCmd) gc;
4439 return GC.block(vicmd.v, substituteGC(pt, vicmd.g));
4440 }
4441 case TagConstants.DYNINSTCMD:
4442 {
4443 DynInstCmd dc = (DynInstCmd) gc;
4444 return DynInstCmd.make(dc.s, substituteGC(pt, dc.g));
4445 }
4446 case TagConstants.TRYCMD:
4447 case TagConstants.CHOOSECMD:
4448 {
4449 CmdCmdCmd cccmd = (CmdCmdCmd) gc;
4450 return CmdCmdCmd.make(cccmd.cmd,
4451 substituteGC(pt, cccmd.g1),
4452 substituteGC(pt, cccmd.g2));
4453 }
4454 case TagConstants.CALL:
4455 {
4456 Call call = (Call) gc;
4457 int size = call.args.size();
4458 ExprVec vec = ExprVec.make(size);
4459 for (int i = 0; i < size; i++)
4460 vec.addElement(Substitute.doSubst(pt,
4461 call.args.elementAt(i)));
4462 Call res = Call.make(vec, call.scall, call.ecall,
4463 call.inlined);
4464 res.desugared = substituteGC(pt, call.desugared);
4465 res.rd = call.rd;
4466 res.spec = call.spec;
4467 return res;
4468 }
4469 case TagConstants.LOOPCMD:
4470 {
4471 LoopCmd lcmd = (LoopCmd) gc;
4472 LoopCmd res = GC.loop(lcmd.locStart, lcmd.locEnd, lcmd.locHotspot,
4473 lcmd.oldmap,
4474 lcmd.invariants, lcmd.decreases,
4475 lcmd.skolemConstants, lcmd.predicates,
4476 lcmd.tempVars, lcmd.guard,
4477 lcmd.body);
4478 res.desugared = substituteGC(pt, lcmd.desugared);
4479 return res;
4480 }
4481 default:
4482 //@ unreachable;
4483 Assert.fail("Unknown kind of guarded command encountered");
4484 return null;
4485 }
4486 }
4487
4488 /**
4489 * Destructively change the trace labels in <code>gc</code> to insert sequence
4490 * numbers that are used by the ErrorMsg class in printing trace labels in the
4491 * correct execution order. This method requires that trace labels do not yet
4492 * contain sequence numbers.
4493 */
4494 public static void addTraceLabelSequenceNumbers(/*@ non_null */ GuardedCmd gc) {
4495 // order the body's trace labels by execution order
4496 if (Main.options().traceInfo > 0) {
4497 orderTraceLabels(gc, 0);
4498 }
4499 }
4500
4501 /**
4502 * Walk through the guarded command translation of a method, adding unique number
4503 * to its location sequence, in order to sort trace labels in order of execution.
4504 * This is a destructive operation.
4505 */
4506 private static int orderTraceLabels(/*@ non_null */ GuardedCmd gc, int count) {
4507 int tag = gc.getTag();
4508 switch (tag) {
4509 case TagConstants.SKIPCMD:
4510 case TagConstants.RAISECMD:
4511 case TagConstants.ASSERTCMD:
4512 case TagConstants.GETSCMD:
4513 case TagConstants.SUBGETSCMD:
4514 case TagConstants.SUBSUBGETSCMD:
4515 case TagConstants.RESTOREFROMCMD:
4516 return count;
4517 case TagConstants.ASSUMECMD:
4518 {
4519 Expr pred = ((ExprCmd) gc).pred;
4520 if (pred.getTag() == TagConstants.LABELEXPR) {
4521 LabelExpr le = (LabelExpr) pred;
4522 count = orderTraceLabel(le, count);
4523 }
4524 return count;
4525 }
4526 case TagConstants.SEQCMD:
4527 {
4528 SeqCmd scmd = (SeqCmd) gc;
4529 int size = scmd.cmds.size();
4530 for (int i = 0; i < size; i++)
4531 count = orderTraceLabels(scmd.cmds.elementAt(i), count);
4532 return count;
4533 }
4534 case TagConstants.VARINCMD:
4535 {
4536 VarInCmd vicmd = (VarInCmd) gc;
4537 return orderTraceLabels(vicmd.g, count);
4538 }
4539 case TagConstants.DYNINSTCMD:
4540 {
4541 DynInstCmd dc = (DynInstCmd) gc;
4542 return orderTraceLabels(dc.g, count);
4543 }
4544 case TagConstants.TRYCMD:
4545 case TagConstants.CHOOSECMD:
4546 {
4547 CmdCmdCmd cccmd = (CmdCmdCmd) gc;
4548 count = orderTraceLabels(cccmd.g1, count);
4549 return orderTraceLabels(cccmd.g2, count);
4550 }
4551 case TagConstants.CALL:
4552 {
4553 Call call = (Call) gc;
4554 return orderTraceLabels(call.desugared, count);
4555 }
4556 case TagConstants.LOOPCMD:
4557 {
4558 LoopCmd lcmd = (LoopCmd) gc;
4559 return orderTraceLabels(lcmd.desugared, count);
4560 }
4561 default:
4562 //@ unreachable;
4563 Assert.fail("Unknown kind of guarded command encountered");
4564 return -1;
4565 }
4566 }
4567
4568 /**
4569 * If the given label is a trace label, add the <code>count</code> number to the
4570 * given label expression's label name, so that trace labels will sort correctly.
4571 */
4572 private static int orderTraceLabel(/*@ non_null */ LabelExpr le, int count) {
4573 String name = le.label.toString();
4574 if (ErrorMsg.isTraceLabel(name)) {
4575 // check that we aren't touching a label that has already had a
4576 // number prefixed to it
4577 Assert.notFalse(name.indexOf(",") == -1);
4578 int k = name.indexOf("^");
4579 Assert.notFalse(k != -1);
4580 name = name.substring(0, k+1) + String.valueOf(count) + "," +
4581 name.substring(k+1);
4582 le.label = Identifier.intern(name);
4583 count++;
4584 }
4585
4586 return count;
4587 }
4588
4589
4590 /***************************************************
4591 * *
4592 * Generating temporary variables: *
4593 * *
4594 ***************************************************/
4595
4596 /**
4597 * Countains the number of temporaries generated for the method currently being
4598 * translated.
4599 *
4600 * <p> Reset to 0 on entry to {@link #trExpr(boolean, VarInit)}.
4601 */
4602 private int tmpcount;
4603
4604 /**
4605 * Generate a temporary for the result of a given expression.
4606 *
4607 * <p> This partially implements ESCJ 23b, case 6.
4608 */
4609 private VariableAccess fresh(/*@ non_null */ VarInit e, int loc) {
4610 return fresh(e, loc, null);
4611 }
4612
4613 private VariableAccess fresh(/*@ non_null */ VarInit e, int loc, String suffix) {
4614 String name = "tmp" + tmpcount++;
4615 if (suffix != null) {
4616 name += "!" + suffix;
4617 }
4618 return temporary(name, e.getStartLoc(), loc);
4619 }
4620
4621 /**
4622 * Generate a temporary variable with prefix <code>s</code> and associated
4623 * expression location information <code>locAccess</code>.
4624 */
4625 private VariableAccess temporary(String s, int locAccess) {
4626 return temporary(s, locAccess, Location.NULL);
4627 }
4628
4629 private VariableAccess temporary(String s, int locAccess, int locIdDecl) {
4630 // As per ESCJ 23b, case 6, we do not use locId:
4631 if (locIdDecl == Location.NULL) {
4632 locIdDecl = UniqName.temporaryVariable;
4633 }
4634
4635 Identifier idn = Identifier.intern(s);
4636 VariableAccess result = GC.makeVar(idn, locIdDecl);
4637 temporaries.addElement(result.decl);
4638 result.loc = locAccess;
4639
4640 return result;
4641 }
4642
4643 public static Expr mapLocation(Expr e, int loc) {
4644 int tag = e.getTag();
4645 switch (tag) {
4646 case TagConstants.LABELEXPR:
4647 LabelExpr le = (LabelExpr)e;
4648 String s = le.label.toString();
4649 if (s.indexOf('@') != -1) return e;
4650 return LabelExpr.make(le.sloc,le.eloc,le.positive,
4651 Identifier.intern(
4652 s+"@"+UniqName.locToSuffix(loc)),
4653 le.expr);
4654 case TagConstants.BOOLOR:
4655 case TagConstants.BOOLAND:
4656 case TagConstants.BOOLANDX:
4657 ExprVec ev = ExprVec.make();
4658 NaryExpr ne = (NaryExpr)e;
4659 ExprVec evo = ne.exprs;
4660 for (int k=0; k<evo.size(); ++k) {
4661 Expr ex = evo.elementAt(k);
4662 ex = mapLocation(ex,loc);
4663 ev.addElement(ex);
4664 }
4665 return NaryExpr.make(ne.sloc, ne.eloc, ne.op,
4666 ne.methodName, ev);
4667 default:
4668 return e;
4669 }
4670 }
4671
4672 public ArrayList modifyEverythingLocations = new ArrayList();
4673
4674 public class EverythingLoc {
4675 public int loc;
4676 public Hashtable pt;
4677 public SeqCmd gcseq = SeqCmd.make(GuardedCmdVec.make());
4678 public Set completed = new Set();
4679 public EverythingLoc(int loc, Hashtable pt) {
4680 this.loc = loc;
4681 this.pt = pt;
4682 }
4683 public void add(Expr e) {
4684 if (e instanceof VariableAccess) {
4685 if (completed.contains( ((VariableAccess)e).decl )) return;
4686 completed.add( ((VariableAccess)e).decl );
4687 }
4688 GuardedCmd gc = modify(e, pt, loc);
4689 if (gc != null) gcseq.cmds.addElement(gc);
4690 }
4691 }
4692
4693 public void addMoreLocations(java.util.Set s) {
4694 Iterator ii = modifyEverythingLocations.iterator();
4695 while (ii.hasNext()) {
4696 EverythingLoc ev = (EverythingLoc)ii.next();
4697 Iterator i = s.iterator();
4698 while (i.hasNext()) {
4699 Object o = i.next();
4700 ev.add((Expr)o);
4701 }
4702 }
4703 }
4704
4705 // Changes all BOOLANDX operations to BOOLIMPLIES, in place
4706 static void setop(ASTNode e) {
4707 if (e instanceof NaryExpr) {
4708 NaryExpr ne = (NaryExpr)e;
4709 if (ne.getTag() == TagConstants.BOOLANDX) {
4710 ne.op = TagConstants.BOOLIMPLIES;
4711 }
4712 }
4713 int n = e.childCount();
4714 for (int i = 0; i<n; ++i) {
4715 Object o = e.childAt(i);
4716 if (o != null && o instanceof ASTNode) setop((ASTNode)o);
4717 }
4718 }
4719
4720 public Expr addNewString(VarInit x, Expr left, Expr right) {
4721 // Construct variables
4722 VariableAccess result= fresh(x, x.getStartLoc(), "newString!");
4723 VariableAccess newallocvar= adorn(GC.allocvar);
4724
4725 ExprVec ev = ExprVec.make(5);
4726 ev.addElement(result);
4727 ev.addElement(left);
4728 ev.addElement(right);
4729 ev.addElement(GC.allocvar);
4730 ev.addElement(newallocvar);
4731
4732 Expr newstring = GC.nary(x.getStartLoc(), x.getEndLoc(),
4733 TagConstants.STRINGCATP, ev);
4734
4735 // Emit the Assume and a Gets commands
4736 code.addElement(GC.assume(newstring));
4737 code.addElement(GC.gets(GC.allocvar, newallocvar));
4738
4739 return result; // FIXME - we are omitting the protect, which I don't understand
4740 }
4741
4742 public static class Strings {
4743 static Map map = new HashMap();
4744 static private int count = 0;
4745 static Integer intern(String s) {
4746 Object o = map.get(s);
4747 if (o != null) return ((Integer)o);
4748 Integer i = new Integer(++count);
4749 map.put(s,i);
4750 return i;
4751 }
4752 }
4753
4754 private GuardedCmdVec codevec;
4755 private Identifier cacheVar = Identifier.intern("modCache");
4756
4757 public VariableAccess cacheValue(Expr e) {
4758 VariableAccess va = GC.makeVar(cacheVar, e.getStartLoc());
4759 codevec.addElement(GC.gets(va, e));
4760 return va;
4761 }
4762 } // end of class Translate
4763
4764 // FIXME - translation of model vars is handled for set, assume, assert, ghost decls
4765 // But still need to do so for other types of statement pragmas
4766 // Also need to do so for quantified expresssions.
4767 // What about for old expressions?
4768
4769 /*
4770 * Local Variables:
4771 * Mode: Java
4772 * fill-column: 85
4773 * End:
4774 */