Java API By Example, From Geeks To Geeks.

1 package com.sun.org.apache.bcel.internal.verifier.structurals; 2 3 /* ==================================================================== 4  * The Apache Software License, Version 1.1 5  * 6  * Copyright (c) 2001 The Apache Software Foundation. All rights 7  * reserved. 8  * 9  * Redistribution and use in source and binary forms, with or without 10  * modification, are permitted provided that the following conditions 11  * are met: 12  * 13  * 1. Redistributions of source code must retain the above copyright 14  * notice, this list of conditions and the following disclaimer. 15  * 16  * 2. Redistributions in binary form must reproduce the above copyright 17  * notice, this list of conditions and the following disclaimer in 18  * the documentation and/or other materials provided with the 19  * distribution. 20  * 21  * 3. The end-user documentation included with the redistribution, 22  * if any, must include the following acknowledgment: 23  * "This product includes software developed by the 24  * Apache Software Foundation (http://www.apache.org/)." 25  * Alternately, this acknowledgment may appear in the software itself, 26  * if and wherever such third-party acknowledgments normally appear. 27  * 28  * 4. The names "Apache" and "Apache Software Foundation" and 29  * "Apache BCEL" must not be used to endorse or promote products 30  * derived from this software without prior written permission. For 31  * written permission, please contact apache@apache.org. 32  * 33  * 5. Products derived from this software may not be called "Apache", 34  * "Apache BCEL", nor may "Apache" appear in their name, without 35  * prior written permission of the Apache Software Foundation. 36  * 37  * THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESSED OR IMPLIED 38  * WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES 39  * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE 40  * DISCLAIMED. IN NO EVENT SHALL THE APACHE SOFTWARE FOUNDATION OR 41  * ITS CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 42  * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 43  * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF 44  * USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND 45  * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, 46  * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT 47  * OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF 48  * SUCH DAMAGE. 49  * ==================================================================== 50  * 51  * This software consists of voluntary contributions made by many 52  * individuals on behalf of the Apache Software Foundation. For more 53  * information on the Apache Software Foundation, please see 54  * <http://www.apache.org/>. 55  */ 56 57 import com.sun.org.apache.bcel.internal.Constants; 58 import com.sun.org.apache.bcel.internal.Repository; 59 import com.sun.org.apache.bcel.internal.classfile.Constant; 60 import com.sun.org.apache.bcel.internal.classfile.ConstantClass; 61 import com.sun.org.apache.bcel.internal.classfile.ConstantDouble; 62 import com.sun.org.apache.bcel.internal.classfile.ConstantInteger; 63 import com.sun.org.apache.bcel.internal.classfile.ConstantFieldref; 64 import com.sun.org.apache.bcel.internal.classfile.ConstantFloat; 65 import com.sun.org.apache.bcel.internal.classfile.ConstantInterfaceMethodref; 66 import com.sun.org.apache.bcel.internal.classfile.ConstantLong; 67 import com.sun.org.apache.bcel.internal.classfile.ConstantNameAndType; 68 import com.sun.org.apache.bcel.internal.classfile.ConstantString; 69 import com.sun.org.apache.bcel.internal.classfile.ConstantUtf8; 70 import com.sun.org.apache.bcel.internal.classfile.Field; 71 import com.sun.org.apache.bcel.internal.classfile.JavaClass; 72 import com.sun.org.apache.bcel.internal.generic.*; 73 import com.sun.org.apache.bcel.internal.verifier.*; 74 import com.sun.org.apache.bcel.internal.verifier.exc.*; 75 import java.util.ArrayList ; 76 import java.util.HashMap ; 77 import java.util.Hashtable ; 78 79 /** 80  * A Visitor class testing for valid preconditions of JVM instructions. 81  * The instance of this class will throw a StructuralCodeConstraintException 82  * instance if an instruction is visitXXX()ed which has preconditions that are 83  * not satisfied. 84  * TODO: Currently, the JVM's behaviour concerning monitors (MONITORENTER, 85  * MONITOREXIT) is not modeled in JustIce. 86  * 87  * @version $Id: InstConstraintVisitor.java,v 1.1.1.1 2001/10/29 20:00:41 jvanzyl Exp $ 88  * @author <A HREF="http://www.inf.fu-berlin.de/~ehaase"/>Enver Haase</A> 89  * @see com.sun.org.apache.bcel.internal.verifier.exc.StructuralCodeConstraintException 90  * @see com.sun.org.apache.bcel.internal.verifier.exc.LinkingConstraintException 91  */ 92 public class InstConstraintVisitor extends EmptyVisitor implements com.sun.org.apache.bcel.internal.generic.Visitor{ 93 94     private static ObjectType GENERIC_ARRAY = new ObjectType("com.sun.org.apache.bcel.internal.verifier.structurals.GenericArray"); 95 96     /** 97      * The constructor. Constructs a new instance of this class. 98      */ 99     public InstConstraintVisitor(){} 100 101     /** 102      * The Execution Frame we're working on. 103      * 104      * @see #setFrame(Frame f) 105      * @see #locals() 106      * @see #stack() 107      */ 108     private Frame frame = null; 109 110     /** 111      * The ConstantPoolGen we're working on. 112      * 113      * @see #setConstantPoolGen(ConstantPoolGen cpg) 114      */ 115     private ConstantPoolGen cpg = null; 116 117     /** 118      * The MethodGen we're working on. 119      * 120      * @see #setMethodGen(MethodGen mg) 121      */ 122     private MethodGen mg = null; 123 124     /** 125      * The OperandStack we're working on. 126      * 127      * @see #setFrame(Frame f) 128      */ 129     private OperandStack stack(){ 130         return frame.getStack(); 131     } 132 133     /** 134      * The LocalVariables we're working on. 135      * 136      * @see #setFrame(Frame f) 137      */ 138     private LocalVariables locals(){ 139         return frame.getLocals(); 140     } 141 142     /** 143    * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor 144    * that a constraint violation has occured. This is done by throwing an instance of a 145    * StructuralCodeConstraintException. 146    * @throws com.sun.org.apache.bcel.internal.verifier.exc.StructuralCodeConstraintException always. 147    */ 148     private void constraintViolated(Instruction violator, String description){ 149         String fq_classname = violator.getClass().getName(); 150         throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description); 151     } 152 153     /** 154      * This returns the single instance of the InstConstraintVisitor class. 155      * To operate correctly, other values must have been set before actually 156      * using the instance. 157      * Use this method for performance reasons. 158      * 159      * @see #setConstantPoolGen(ConstantPoolGen cpg) 160      * @see #setMethodGen(MethodGen mg) 161      */ 162     public void setFrame(Frame f){ 163         this.frame = f; 164         //if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first."); 165 } 166 167     /** 168      * Sets the ConstantPoolGen instance needed for constraint 169      * checking prior to execution. 170      */ 171     public void setConstantPoolGen(ConstantPoolGen cpg){ 172         this.cpg = cpg; 173     } 174 175     /** 176      * Sets the MethodGen instance needed for constraint 177      * checking prior to execution. 178      */ 179     public void setMethodGen(MethodGen mg){ 180         this.mg = mg; 181     } 182 183     /** 184      * Assures index is of type INT. 185      * @throws com.sun.org.apache.bcel.internal.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied. 186      */ 187     private void indexOfInt(Instruction o, Type index){ 188         if (! index.equals(Type.INT)) 189                 constraintViolated(o, "The 'index' is not of type int but of type "+index+"."); 190     } 191 192     /** 193      * Assures the ReferenceType r is initialized (or Type.NULL). 194      * Formally, this means (!(r instanceof UninitializedObjectType)), because 195      * there are no uninitialized array types. 196      * @throws com.sun.org.apache.bcel.internal.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied. 197      */ 198     private void referenceTypeIsInitialized(Instruction o, ReferenceType r){ 199         if (r instanceof UninitializedObjectType){ 200             constraintViolated(o, "Working on an uninitialized object '"+r+"'."); 201         } 202     } 203 204     /** Assures value is of type INT. */ 205     private void valueOfInt(Instruction o, Type value){ 206         if (! value.equals(Type.INT)) 207                 constraintViolated(o, "The 'value' is not of type int but of type "+value+"."); 208     } 209 210     /** 211      * Assures arrayref is of ArrayType or NULL; 212      * returns true if and only if arrayref is non-NULL. 213      * @throws com.sun.org.apache.bcel.internal.verifier.exc.StructuralCodeConstraintException if the above constraint is violated. 214      */ 215     private boolean arrayrefOfArrayType(Instruction o, Type arrayref){ 216         if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) ) 217                 constraintViolated(o, "The 'arrayref' does not refer to an array but is of type "+arrayref+"."); 218         return (arrayref instanceof ArrayType); 219     } 220 221     /***************************************************************/ 222     /* MISC */ 223     /***************************************************************/ 224     /** 225      * Ensures the general preconditions of an instruction that accesses the stack. 226      * This method is here because BCEL has no such superinterface for the stack 227      * accessing instructions; and there are funny unexpected exceptions in the 228      * semantices of the superinterfaces and superclasses provided. 229      * E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer. 230      * Therefore, this method is called by all StackProducer, StackConsumer, 231      * and StackInstruction instances via their visitXXX() method. 232      * Unfortunately, as the superclasses and superinterfaces overlap, some instructions 233      * cause this method to be called two or three times. [TODO: Fix this.] 234      * 235      * @see #visitStackConsumer(StackConsumer o) 236      * @see #visitStackProducer(StackProducer o) 237      * @see #visitStackInstruction(StackInstruction o) 238      */ 239     private void _visitStackAccessor(Instruction o){ 240         int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced. 241 if (consume > stack().slotsUsed()){ 242             constraintViolated((Instruction) o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack()); 243         } 244 245         int produce = o.produceStack(cpg) - ((Instruction) o).consumeStack(cpg); // Stack values are always consumed first; then produced. 246 if ( produce + stack().slotsUsed() > stack().maxStack() ){ 247             constraintViolated((Instruction) o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack()); 248         } 249     } 250 251     /***************************************************************/ 252     /* "generic"visitXXXX methods where XXXX is an interface */ 253     /* therefore, we don't know the order of visiting; but we know */ 254     /* these methods are called before the visitYYYY methods below */ 255     /***************************************************************/ 256 257     /** 258      * Assures the generic preconditions of a LoadClass instance. 259      * The referenced class is loaded and pass2-verified. 260      */ 261     public void visitLoadClass(LoadClass o){ 262         ObjectType t = o.getLoadClassType(cpg); 263         if (t != null){// null means "no class is loaded" 264 Verifier v = VerifierFactory.getVerifier(t.getClassName()); 265             VerificationResult vr = v.doPass2(); 266             if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 267                 constraintViolated((Instruction) o, "Class '"+o.getLoadClassType(cpg).getClassName()+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 268             } 269         } 270     } 271 272     /** 273      * Ensures the general preconditions of a StackConsumer instance. 274      */ 275     public void visitStackConsumer(StackConsumer o){ 276         _visitStackAccessor((Instruction) o); 277     } 278      279     /** 280      * Ensures the general preconditions of a StackProducer instance. 281      */ 282     public void visitStackProducer(StackProducer o){ 283         _visitStackAccessor((Instruction) o); 284     } 285 286 287     /***************************************************************/ 288     /* "generic" visitYYYY methods where YYYY is a superclass. */ 289     /* therefore, we know the order of visiting; we know */ 290     /* these methods are called after the visitXXXX methods above. */ 291     /***************************************************************/ 292     /** 293      * Ensures the general preconditions of a CPInstruction instance. 294      */ 295     public void visitCPInstruction(CPInstruction o){ 296         int idx = o.getIndex(); 297         if ((idx < 0) || (idx >= cpg.getSize())){ 298             throw new AssertionViolatedException("Huh?! Constant pool index of instruction '"+o+"' illegal? Pass 3a should have checked this!"); 299         } 300     } 301 302     /** 303      * Ensures the general preconditions of a FieldInstruction instance. 304      */ 305      public void visitFieldInstruction(FieldInstruction o){ 306         // visitLoadClass(o) has been called before: Every FieldOrMethod 307 // implements LoadClass. 308 // visitCPInstruction(o) has been called before. 309 // A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC 310 Constant c = cpg.getConstant(o.getIndex()); 311             if (!(c instanceof ConstantFieldref)){ 312                 constraintViolated(o, "Index '"+o.getIndex()+"' should refer to a CONSTANT_Fieldref_info structure, but refers to '"+c+"'."); 313             } 314             // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o). 315 Type t = o.getType(cpg); 316             if (t instanceof ObjectType){ 317                 String name = ((ObjectType)t).getClassName(); 318                 Verifier v = VerifierFactory.getVerifier( name ); 319                 VerificationResult vr = v.doPass2(); 320                 if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 321                     constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 322                 } 323             } 324      } 325       326     /** 327      * Ensures the general preconditions of an InvokeInstruction instance. 328      */ 329      public void visitInvokeInstruction(InvokeInstruction o){ 330         // visitLoadClass(o) has been called before: Every FieldOrMethod 331 // implements LoadClass. 332 // visitCPInstruction(o) has been called before. 333 //TODO 334 } 335       336     /** 337      * Ensures the general preconditions of a StackInstruction instance. 338      */ 339     public void visitStackInstruction(StackInstruction o){ 340         _visitStackAccessor(o); 341     } 342 343     /** 344      * Assures the generic preconditions of a LocalVariableInstruction instance. 345      * That is, the index of the local variable must be valid. 346      */ 347     public void visitLocalVariableInstruction(LocalVariableInstruction o){ 348         if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){ 349             constraintViolated(o, "The 'index' is not a valid index into the local variable array."); 350         } 351     } 352      353     /** 354      * Assures the generic preconditions of a LoadInstruction instance. 355      */ 356     public void visitLoadInstruction(LoadInstruction o){ 357         //visitLocalVariableInstruction(o) is called before, because it is more generic. 358 359         // LOAD instructions must not read Type.UNKNOWN 360 if (locals().get(o.getIndex()) == Type.UNKNOWN){ 361             constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content."); 362         } 363 364         // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN 365 // as a symbol for the higher halve at index N+1 366 // [suppose some instruction put an int at N+1--- our double at N is defective] 367 if (o.getType(cpg).getSize() == 2){ 368             if (locals().get(o.getIndex()+1) != Type.UNKNOWN){ 369                 constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed."); 370             } 371         } 372 373         // LOAD instructions must read the correct type. 374 if (!(o instanceof ALOAD)){ 375             if (locals().get(o.getIndex()) != o.getType(cpg) ){ 376                 constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'."); 377             } 378         } 379         else{ // we deal with an ALOAD 380 if (!(locals().get(o.getIndex()) instanceof ReferenceType)){ 381                 constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType."); 382             } 383             // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack! 384 //referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex()))); 385 } 386 387         // LOAD instructions must have enough free stack slots. 388 if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){ 389             constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack."); 390         } 391     } 392 393     /** 394      * Assures the generic preconditions of a StoreInstruction instance. 395      */ 396     public void visitStoreInstruction(StoreInstruction o){ 397         //visitLocalVariableInstruction(o) is called before, because it is more generic. 398 399         if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking. 400 constraintViolated(o, "Cannot STORE: Stack to read from is empty."); 401         } 402 403         if ( (!(o instanceof ASTORE)) ){ 404             if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL. 405 constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'."); 406             } 407         } 408         else{ // we deal with ASTORE 409 Type stacktop = stack().peek(); 410             if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){ 411                 constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType."); 412             } 413             if (stacktop instanceof ReferenceType){ 414                 referenceTypeIsInitialized(o, (ReferenceType) stacktop); 415             } 416         } 417     } 418 419     /** 420      * Assures the generic preconditions of a ReturnInstruction instance. 421      */ 422     public void visitReturnInstruction(ReturnInstruction o){ 423         if (o instanceof RETURN){ 424             return; 425         } 426         if (o instanceof ARETURN){ 427             if (stack().peek() == Type.NULL){ 428                 return; 429             } 430             else{ 431                 if (! (stack().peek() instanceof ReferenceType)){ 432                     constraintViolated(o, "Reference type expected on top of stack, but is: '"+stack().peek()+"'."); 433                 } 434                 referenceTypeIsInitialized(o, (ReferenceType) (stack().peek())); 435                 ReferenceType objectref = (ReferenceType) (stack().peek()); 436                 // TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a 437 // "wider cast object type" created during verification. 438 //if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ){ 439 // constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+"' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'."); 440 //} 441 } 442         } 443         else{ 444             Type method_type = mg.getType(); 445             if (method_type == Type.BOOLEAN || 446                     method_type == Type.BYTE || 447                     method_type == Type.SHORT || 448                     method_type == Type.CHAR){ 449                 method_type = Type.INT; 450             } 451             if (! ( method_type.equals( stack().peek() ))){ 452                 constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'."); 453             } 454         } 455     } 456 457     /***************************************************************/ 458     /* "special"visitXXXX methods for one type of instruction each */ 459     /***************************************************************/ 460 461     /** 462      * Ensures the specific preconditions of the said instruction. 463      */ 464     public void visitAALOAD(AALOAD o){ 465         Type arrayref = stack().peek(1); 466         Type index = stack().peek(0); 467          468         indexOfInt(o, index); 469         if (arrayrefOfArrayType(o, arrayref)){ 470             if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){ 471                 constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+"."); 472             } 473             referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType())); 474         } 475     } 476 477     /** 478      * Ensures the specific preconditions of the said instruction. 479      */ 480     public void visitAASTORE(AASTORE o){ 481         Type arrayref = stack().peek(2); 482         Type index = stack().peek(1); 483         Type value = stack().peek(0); 484 485         indexOfInt(o, index); 486         if (!(value instanceof ReferenceType)){ 487             constraintViolated(o, "The 'value' is not of a ReferenceType but of type "+value+"."); 488         }else{ 489             referenceTypeIsInitialized(o, (ReferenceType) value); 490         } 491         // Don't bother further with "referenceTypeIsInitialized()", there are no arrays 492 // of an uninitialized object type. 493 if (arrayrefOfArrayType(o, arrayref)){ 494             if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){ 495                 constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+"."); 496             } 497             if (! ((ReferenceType)value).isAssignmentCompatibleWith((ReferenceType) ((ArrayType) arrayref).getElementType())){ 498                 constraintViolated(o, "The type of 'value' ('"+value+"') is not assignment compatible to the components of the array 'arrayref' refers to. ('"+((ArrayType) arrayref).getElementType()+"')"); 499             } 500         } 501     } 502 503     /** 504      * Ensures the specific preconditions of the said instruction. 505      */ 506     public void visitACONST_NULL(ACONST_NULL o){ 507         // Nothing needs to be done here. 508 } 509 510     /** 511      * Ensures the specific preconditions of the said instruction. 512      */ 513     public void visitALOAD(ALOAD o){ 514         //visitLoadInstruction(LoadInstruction) is called before. 515 516         // Nothing else needs to be done here. 517 } 518 519     /** 520      * Ensures the specific preconditions of the said instruction. 521      */ 522     public void visitANEWARRAY(ANEWARRAY o){ 523         if (!stack().peek().equals(Type.INT)) 524             constraintViolated(o, "The 'count' at the stack top is not of type '"+Type.INT+"' but of type '"+stack().peek()+"'."); 525         // The runtime constant pool item at that index must be a symbolic reference to a class, 526 // array, or interface type. See Pass 3a. 527 } 528      529     /** 530      * Ensures the specific preconditions of the said instruction. 531      */ 532     public void visitARETURN(ARETURN o){ 533         if (! (stack().peek() instanceof ReferenceType) ){ 534             constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'."); 535         } 536         ReferenceType objectref = (ReferenceType) (stack().peek()); 537         referenceTypeIsInitialized(o, objectref); 538          539         // The check below should already done via visitReturnInstruction(ReturnInstruction), see there. 540 // It cannot be done using Staerk-et-al's "set of object types" instead of a 541 // "wider cast object type", anyway. 542 //if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){ 543 // constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method."); 544 //} 545 } 546 547     /** 548      * Ensures the specific preconditions of the said instruction. 549      */ 550     public void visitARRAYLENGTH(ARRAYLENGTH o){ 551         Type arrayref = stack().peek(0); 552         arrayrefOfArrayType(o, arrayref); 553     } 554 555     /** 556      * Ensures the specific preconditions of the said instruction. 557      */ 558     public void visitASTORE(ASTORE o){ 559         if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){ 560             constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+"."); 561         } 562         if (stack().peek() instanceof ReferenceType){ 563             referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 564         } 565     } 566 567     /** 568      * Ensures the specific preconditions of the said instruction. 569      */ 570     public void visitATHROW(ATHROW o){ 571         // It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is 572 // not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL. 573 if (! ((stack().peek() instanceof ObjectType) || (stack().peek().equals(Type.NULL))) ){ 574             constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type "+stack().peek()+"."); 575         } 576          577         // NULL is a subclass of every class, so to speak. 578 if (stack().peek().equals(Type.NULL)) return; 579                  580         ObjectType exc = (ObjectType) (stack().peek()); 581         ObjectType throwable = (ObjectType) (Type.getType("Ljava/lang/Throwable;")); 582         if ( (! (exc.subclassOf(throwable)) ) && (! (exc.equals(throwable))) ){ 583             constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '"+stack().peek()+"'."); 584         } 585     } 586 587     /** 588      * Ensures the specific preconditions of the said instruction. 589      */ 590     public void visitBALOAD(BALOAD o){ 591         Type arrayref = stack().peek(1); 592         Type index = stack().peek(0); 593         indexOfInt(o, index); 594         if (arrayrefOfArrayType(o, arrayref)){ 595             if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) || 596                    (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){ 597                 constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'."); 598             } 599         } 600     } 601 602     /** 603      * Ensures the specific preconditions of the said instruction. 604      */ 605     public void visitBASTORE(BASTORE o){ 606         Type arrayref = stack().peek(2); 607         Type index = stack().peek(1); 608         Type value = stack().peek(0); 609 610         indexOfInt(o, index); 611         valueOfInt(o, index); 612         if (arrayrefOfArrayType(o, arrayref)){ 613             if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) || 614                     (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ) 615                     constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'."); 616         } 617     } 618 619     /** 620      * Ensures the specific preconditions of the said instruction. 621      */ 622     public void visitBIPUSH(BIPUSH o){ 623         // Nothing to do... 624 } 625 626     /** 627      * Ensures the specific preconditions of the said instruction. 628      */ 629     public void visitBREAKPOINT(BREAKPOINT o){ 630         throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT."); 631     } 632 633     /** 634      * Ensures the specific preconditions of the said instruction. 635      */ 636     public void visitCALOAD(CALOAD o){ 637         Type arrayref = stack().peek(1); 638         Type index = stack().peek(0); 639          640         indexOfInt(o, index); 641         arrayrefOfArrayType(o, arrayref); 642     } 643 644     /** 645      * Ensures the specific preconditions of the said instruction. 646      */ 647     public void visitCASTORE(CASTORE o){ 648         Type arrayref = stack().peek(2); 649         Type index = stack().peek(1); 650         Type value = stack().peek(0); 651          652         indexOfInt(o, index); 653         valueOfInt(o, index); 654         if (arrayrefOfArrayType(o, arrayref)){ 655             if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){ 656                 constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+"."); 657             } 658         } 659     } 660 661     /** 662      * Ensures the specific preconditions of the said instruction. 663      */ 664     public void visitCHECKCAST(CHECKCAST o){ 665         // The objectref must be of type reference. 666 Type objectref = stack().peek(0); 667         if (!(objectref instanceof ReferenceType)){ 668             constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+"."); 669         } 670         else{ 671             referenceTypeIsInitialized(o, (ReferenceType) objectref); 672         } 673         // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the 674 // current class (&#247;3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant 675 // pool item at the index must be a symbolic reference to a class, array, or interface type. 676 Constant c = cpg.getConstant(o.getIndex()); 677         if (! (c instanceof ConstantClass)){ 678             constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'."); 679         } 680     } 681 682     /** 683      * Ensures the specific preconditions of the said instruction. 684      */ 685     public void visitD2F(D2F o){ 686         if (stack().peek() != Type.DOUBLE){ 687             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 688         } 689     } 690 691     /** 692      * Ensures the specific preconditions of the said instruction. 693      */ 694     public void visitD2I(D2I o){ 695         if (stack().peek() != Type.DOUBLE){ 696             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 697         } 698     } 699 700     /** 701      * Ensures the specific preconditions of the said instruction. 702      */ 703     public void visitD2L(D2L o){ 704         if (stack().peek() != Type.DOUBLE){ 705             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 706         } 707     } 708 709     /** 710      * Ensures the specific preconditions of the said instruction. 711      */ 712     public void visitDADD(DADD o){ 713         if (stack().peek() != Type.DOUBLE){ 714             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 715         } 716         if (stack().peek(1) != Type.DOUBLE){ 717             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 718         } 719     } 720 721     /** 722      * Ensures the specific preconditions of the said instruction. 723      */ 724     public void visitDALOAD(DALOAD o){ 725         indexOfInt(o, stack().peek()); 726         if (stack().peek(1) == Type.NULL){ 727             return; 728         } 729         if (! (stack().peek(1) instanceof ArrayType)){ 730             constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'."); 731         } 732         Type t = ((ArrayType) (stack().peek(1))).getBasicType(); 733         if (t != Type.DOUBLE){ 734             constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'."); 735         } 736     } 737 738     /** 739      * Ensures the specific preconditions of the said instruction. 740      */ 741     public void visitDASTORE(DASTORE o){ 742         if (stack().peek() != Type.DOUBLE){ 743             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 744         } 745         indexOfInt(o, stack().peek(1)); 746         if (stack().peek(2) == Type.NULL){ 747             return; 748         } 749         if (! (stack().peek(2) instanceof ArrayType)){ 750             constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'."); 751         } 752         Type t = ((ArrayType) (stack().peek(2))).getBasicType(); 753         if (t != Type.DOUBLE){ 754             constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'."); 755         } 756     } 757 758     /** 759      * Ensures the specific preconditions of the said instruction. 760      */ 761     public void visitDCMPG(DCMPG o){ 762         if (stack().peek() != Type.DOUBLE){ 763             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 764         } 765         if (stack().peek(1) != Type.DOUBLE){ 766             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 767         } 768     } 769 770     /** 771      * Ensures the specific preconditions of the said instruction. 772      */ 773     public void visitDCMPL(DCMPL o){ 774         if (stack().peek() != Type.DOUBLE){ 775             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 776         } 777         if (stack().peek(1) != Type.DOUBLE){ 778             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 779         } 780     } 781 782     /** 783      * Ensures the specific preconditions of the said instruction. 784      */ 785     public void visitDCONST(DCONST o){ 786         // There's nothing to be done here. 787 } 788      789     /** 790      * Ensures the specific preconditions of the said instruction. 791      */ 792     public void visitDDIV(DDIV o){ 793         if (stack().peek() != Type.DOUBLE){ 794             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 795         } 796         if (stack().peek(1) != Type.DOUBLE){ 797             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 798         } 799     } 800 801     /** 802      * Ensures the specific preconditions of the said instruction. 803      */ 804     public void visitDLOAD(DLOAD o){ 805         //visitLoadInstruction(LoadInstruction) is called before. 806 807         // Nothing else needs to be done here. 808 } 809 810     /** 811      * Ensures the specific preconditions of the said instruction. 812      */ 813     public void visitDMUL(DMUL o){ 814         if (stack().peek() != Type.DOUBLE){ 815             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 816         } 817         if (stack().peek(1) != Type.DOUBLE){ 818             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 819         } 820     } 821 822     /** 823      * Ensures the specific preconditions of the said instruction. 824      */ 825     public void visitDNEG(DNEG o){ 826         if (stack().peek() != Type.DOUBLE){ 827             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 828         } 829     } 830 831     /** 832      * Ensures the specific preconditions of the said instruction. 833      */ 834     public void visitDREM(DREM o){ 835         if (stack().peek() != Type.DOUBLE){ 836             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 837         } 838         if (stack().peek(1) != Type.DOUBLE){ 839             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 840         } 841     } 842 843     /** 844      * Ensures the specific preconditions of the said instruction. 845      */ 846     public void visitDRETURN(DRETURN o){ 847         if (stack().peek() != Type.DOUBLE){ 848             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 849         } 850     } 851 852     /** 853      * Ensures the specific preconditions of the said instruction. 854      */ 855     public void visitDSTORE(DSTORE o){ 856         //visitStoreInstruction(StoreInstruction) is called before. 857 858         // Nothing else needs to be done here. 859 } 860 861     /** 862      * Ensures the specific preconditions of the said instruction. 863      */ 864     public void visitDSUB(DSUB o){ 865         if (stack().peek() != Type.DOUBLE){ 866             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'."); 867         } 868         if (stack().peek(1) != Type.DOUBLE){ 869             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'."); 870         } 871     } 872 873     /** 874      * Ensures the specific preconditions of the said instruction. 875      */ 876     public void visitDUP(DUP o){ 877         if (stack().peek().getSize() != 1){ 878             constraintViolated(o, "Won't DUP type on stack top '"+stack().peek()+"' because it must occupy exactly one slot, not '"+stack().peek().getSize()+"'."); 879         } 880     } 881 882     /** 883      * Ensures the specific preconditions of the said instruction. 884      */ 885     public void visitDUP_X1(DUP_X1 o){ 886         if (stack().peek().getSize() != 1){ 887             constraintViolated(o, "Type on stack top '"+stack().peek()+"' should occupy exactly one slot, not '"+stack().peek().getSize()+"'."); 888         } 889         if (stack().peek(1).getSize() != 1){ 890             constraintViolated(o, "Type on stack next-to-top '"+stack().peek(1)+"' should occupy exactly one slot, not '"+stack().peek(1).getSize()+"'."); 891         } 892     } 893 894     /** 895      * Ensures the specific preconditions of the said instruction. 896      */ 897     public void visitDUP_X2(DUP_X2 o){ 898         if (stack().peek().getSize() != 1){ 899             constraintViolated(o, "Stack top type must be of size 1, but is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'."); 900         } 901         if (stack().peek(1).getSize() == 2){ 902             return; // Form 2, okay. 903 } 904         else{ //stack().peek(1).getSize == 1. 905 if (stack().peek(2).getSize() != 1){ 906                 constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1, stack next-to-next-to-top's size must also be 1, but is: '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'."); 907             } 908         } 909     } 910 911     /** 912      * Ensures the specific preconditions of the said instruction. 913      */ 914     public void visitDUP2(DUP2 o){ 915         if (stack().peek().getSize() == 2){ 916             return; // Form 2, okay. 917 } 918         else{ //stack().peek().getSize() == 1. 919 if (stack().peek(1).getSize() != 1){ 920                 constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'."); 921             } 922         } 923     } 924 925     /** 926      * Ensures the specific preconditions of the said instruction. 927      */ 928     public void visitDUP2_X1(DUP2_X1 o){ 929         if (stack().peek().getSize() == 2){ 930             if (stack().peek(1).getSize() != 1){ 931                 constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'."); 932             } 933             else{ 934                 return; // Form 2 935 } 936         } 937         else{ // stack top is of size 1 938 if ( stack().peek(1).getSize() != 1 ){ 939                 constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'."); 940             } 941             if ( stack().peek(2).getSize() != 1 ){ 942                 constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'."); 943             } 944         } 945     } 946 947     /** 948      * Ensures the specific preconditions of the said instruction. 949      */ 950     public void visitDUP2_X2(DUP2_X2 o){ 951 952         if (stack().peek(0).getSize() == 2){ 953             if (stack().peek(1).getSize() == 2){ 954                 return; // Form 4 955 } 956             else{// stack top size is 2, next-to-top's size is 1 957 if ( stack().peek(2).getSize() != 1 ){ 958                     constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'."); 959                 } 960                 else{ 961                     return; // Form 2 962 } 963             } 964         } 965         else{// stack top is of size 1 966 if (stack().peek(1).getSize() == 1){ 967                 if ( stack().peek(2).getSize() == 2 ){ 968                     return; // Form 3 969 } 970                 else{ 971                     if ( stack().peek(3).getSize() == 1){ 972                         return; // Form 1 973 } 974                 } 975             } 976         } 977         constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction."); 978     } 979 980     /** 981      * Ensures the specific preconditions of the said instruction. 982      */ 983     public void visitF2D(F2D o){ 984         if (stack().peek() != Type.FLOAT){ 985             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 986         } 987     } 988 989     /** 990      * Ensures the specific preconditions of the said instruction. 991      */ 992     public void visitF2I(F2I o){ 993         if (stack().peek() != Type.FLOAT){ 994             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 995         } 996     } 997 998     /** 999      * Ensures the specific preconditions of the said instruction. 1000     */ 1001    public void visitF2L(F2L o){ 1002        if (stack().peek() != Type.FLOAT){ 1003            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1004        } 1005    } 1006     1007    /** 1008     * Ensures the specific preconditions of the said instruction. 1009     */ 1010    public void visitFADD(FADD o){ 1011        if (stack().peek() != Type.FLOAT){ 1012            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1013        } 1014        if (stack().peek(1) != Type.FLOAT){ 1015            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1016        } 1017    } 1018 1019    /** 1020     * Ensures the specific preconditions of the said instruction. 1021     */ 1022    public void visitFALOAD(FALOAD o){ 1023        indexOfInt(o, stack().peek()); 1024        if (stack().peek(1) == Type.NULL){ 1025            return; 1026        } 1027        if (! (stack().peek(1) instanceof ArrayType)){ 1028            constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'."); 1029        } 1030        Type t = ((ArrayType) (stack().peek(1))).getBasicType(); 1031        if (t != Type.FLOAT){ 1032            constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'."); 1033        } 1034    } 1035 1036    /** 1037     * Ensures the specific preconditions of the said instruction. 1038     */ 1039    public void visitFASTORE(FASTORE o){ 1040        if (stack().peek() != Type.FLOAT){ 1041            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1042        } 1043        indexOfInt(o, stack().peek(1)); 1044        if (stack().peek(2) == Type.NULL){ 1045            return; 1046        } 1047        if (! (stack().peek(2) instanceof ArrayType)){ 1048            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'."); 1049        } 1050        Type t = ((ArrayType) (stack().peek(2))).getBasicType(); 1051        if (t != Type.FLOAT){ 1052            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'."); 1053        } 1054    } 1055 1056    /** 1057     * Ensures the specific preconditions of the said instruction. 1058     */ 1059    public void visitFCMPG(FCMPG o){ 1060        if (stack().peek() != Type.FLOAT){ 1061            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1062        } 1063        if (stack().peek(1) != Type.FLOAT){ 1064            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1065        } 1066    } 1067 1068    /** 1069     * Ensures the specific preconditions of the said instruction. 1070     */ 1071    public void visitFCMPL(FCMPL o){ 1072        if (stack().peek() != Type.FLOAT){ 1073            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1074        } 1075        if (stack().peek(1) != Type.FLOAT){ 1076            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1077        } 1078    } 1079 1080    /** 1081     * Ensures the specific preconditions of the said instruction. 1082     */ 1083    public void visitFCONST(FCONST o){ 1084        // nothing to do here. 1085 } 1086 1087    /** 1088     * Ensures the specific preconditions of the said instruction. 1089     */ 1090    public void visitFDIV(FDIV o){ 1091        if (stack().peek() != Type.FLOAT){ 1092            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1093        } 1094        if (stack().peek(1) != Type.FLOAT){ 1095            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1096        } 1097    } 1098 1099    /** 1100     * Ensures the specific preconditions of the said instruction. 1101     */ 1102    public void visitFLOAD(FLOAD o){ 1103        //visitLoadInstruction(LoadInstruction) is called before. 1104 1105        // Nothing else needs to be done here. 1106 } 1107 1108    /** 1109     * Ensures the specific preconditions of the said instruction. 1110     */ 1111    public void visitFMUL(FMUL o){ 1112        if (stack().peek() != Type.FLOAT){ 1113            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1114        } 1115        if (stack().peek(1) != Type.FLOAT){ 1116            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1117        } 1118    } 1119 1120    /** 1121     * Ensures the specific preconditions of the said instruction. 1122     */ 1123    public void visitFNEG(FNEG o){ 1124        if (stack().peek() != Type.FLOAT){ 1125            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1126        } 1127    } 1128 1129    /** 1130     * Ensures the specific preconditions of the said instruction. 1131     */ 1132    public void visitFREM(FREM o){ 1133        if (stack().peek() != Type.FLOAT){ 1134            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1135        } 1136        if (stack().peek(1) != Type.FLOAT){ 1137            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1138        } 1139    } 1140 1141    /** 1142     * Ensures the specific preconditions of the said instruction. 1143     */ 1144    public void visitFRETURN(FRETURN o){ 1145        if (stack().peek() != Type.FLOAT){ 1146            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1147        } 1148    } 1149 1150    /** 1151     * Ensures the specific preconditions of the said instruction. 1152     */ 1153    public void visitFSTORE(FSTORE o){ 1154        //visitStoreInstruction(StoreInstruction) is called before. 1155 1156        // Nothing else needs to be done here. 1157 } 1158 1159    /** 1160     * Ensures the specific preconditions of the said instruction. 1161     */ 1162    public void visitFSUB(FSUB o){ 1163        if (stack().peek() != Type.FLOAT){ 1164            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'."); 1165        } 1166        if (stack().peek(1) != Type.FLOAT){ 1167            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'."); 1168        } 1169    } 1170 1171    /** 1172     * Ensures the specific preconditions of the said instruction. 1173     */ 1174    public void visitGETFIELD(GETFIELD o){ 1175        Type objectref = stack().peek(); 1176        if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){ 1177            constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '"+objectref+"'."); 1178        } 1179         1180        String field_name = o.getFieldName(cpg); 1181         1182        JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName()); 1183        Field[] fields = jc.getFields(); 1184        Field f = null; 1185        for (int i=0; i<fields.length; i++){ 1186            if (fields[i].getName().equals(field_name)){ 1187                f = fields[i]; 1188                break; 1189            } 1190        } 1191        if (f == null){ 1192            throw new AssertionViolatedException("Field not found?!?"); 1193        } 1194 1195        if (f.isProtected()){ 1196            ObjectType classtype = o.getClassType(cpg); 1197            ObjectType curr = new ObjectType(mg.getClassName()); 1198 1199            if ( classtype.equals(curr) || 1200                        curr.subclassOf(classtype) ){ 1201                Type t = stack().peek(); 1202                if (t == Type.NULL){ 1203                    return; 1204                } 1205                if (! (t instanceof ObjectType) ){ 1206                    constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+t+"'."); 1207                } 1208                ObjectType objreftype = (ObjectType) t; 1209                if (! ( objreftype.equals(curr) || 1210                            objreftype.subclassOf(curr) ) ){ 1211                    //TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types 1212 // created during the verification. 1213 // "Wider" object types don't allow us to check for things like that below. 1214 //constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or a superclass of the current class. However, the referenced object type '"+stack().peek()+"' is not the current class or a subclass of the current class."); 1215 } 1216            } 1217        } 1218         1219        // TODO: Could go into Pass 3a. 1220 if (f.isStatic()){ 1221            constraintViolated(o, "Referenced field '"+f+"' is static which it shouldn't be."); 1222        } 1223    } 1224 1225    /** 1226     * Ensures the specific preconditions of the said instruction. 1227     */ 1228    public void visitGETSTATIC(GETSTATIC o){ 1229        // Field must be static: see Pass 3a. 1230 } 1231 1232    /** 1233     * Ensures the specific preconditions of the said instruction. 1234     */ 1235    public void visitGOTO(GOTO o){ 1236        // nothing to do here. 1237 } 1238 1239    /** 1240     * Ensures the specific preconditions of the said instruction. 1241     */ 1242    public void visitGOTO_W(GOTO_W o){ 1243        // nothing to do here. 1244 } 1245 1246    /** 1247     * Ensures the specific preconditions of the said instruction. 1248     */ 1249    public void visitI2B(I2B o){ 1250        if (stack().peek() != Type.INT){ 1251            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1252        } 1253    } 1254 1255    /** 1256     * Ensures the specific preconditions of the said instruction. 1257     */ 1258    public void visitI2C(I2C o){ 1259        if (stack().peek() != Type.INT){ 1260            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1261        } 1262    } 1263 1264    /** 1265     * Ensures the specific preconditions of the said instruction. 1266     */ 1267    public void visitI2D(I2D o){ 1268        if (stack().peek() != Type.INT){ 1269            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1270        } 1271    } 1272 1273    /** 1274     * Ensures the specific preconditions of the said instruction. 1275     */ 1276    public void visitI2F(I2F o){ 1277        if (stack().peek() != Type.INT){ 1278            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1279        } 1280    } 1281 1282    /** 1283     * Ensures the specific preconditions of the said instruction. 1284     */ 1285    public void visitI2L(I2L o){ 1286        if (stack().peek() != Type.INT){ 1287            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1288        } 1289    } 1290 1291    /** 1292     * Ensures the specific preconditions of the said instruction. 1293     */ 1294    public void visitI2S(I2S o){ 1295        if (stack().peek() != Type.INT){ 1296            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1297        } 1298    } 1299 1300    /** 1301     * Ensures the specific preconditions of the said instruction. 1302     */ 1303    public void visitIADD(IADD o){ 1304        if (stack().peek() != Type.INT){ 1305            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1306        } 1307        if (stack().peek(1) != Type.INT){ 1308            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1309        } 1310    } 1311 1312    /** 1313     * Ensures the specific preconditions of the said instruction. 1314     */ 1315    public void visitIALOAD(IALOAD o){ 1316        indexOfInt(o, stack().peek()); 1317        if (stack().peek(1) == Type.NULL){ 1318            return; 1319        } 1320        if (! (stack().peek(1) instanceof ArrayType)){ 1321            constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'."); 1322        } 1323        Type t = ((ArrayType) (stack().peek(1))).getBasicType(); 1324        if (t != Type.INT){ 1325            constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'."); 1326        } 1327    } 1328 1329    /** 1330     * Ensures the specific preconditions of the said instruction. 1331     */ 1332    public void visitIAND(IAND o){ 1333        if (stack().peek() != Type.INT){ 1334            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1335        } 1336        if (stack().peek(1) != Type.INT){ 1337            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1338        } 1339    } 1340 1341    /** 1342     * Ensures the specific preconditions of the said instruction. 1343     */ 1344    public void visitIASTORE(IASTORE o){ 1345        if (stack().peek() != Type.INT){ 1346            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1347        } 1348        indexOfInt(o, stack().peek(1)); 1349        if (stack().peek(2) == Type.NULL){ 1350            return; 1351        } 1352        if (! (stack().peek(2) instanceof ArrayType)){ 1353            constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'."); 1354        } 1355        Type t = ((ArrayType) (stack().peek(2))).getBasicType(); 1356        if (t != Type.INT){ 1357            constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'."); 1358        } 1359    } 1360 1361    /** 1362     * Ensures the specific preconditions of the said instruction. 1363     */ 1364    public void visitICONST(ICONST o){ 1365        //nothing to do here. 1366 } 1367 1368    /** 1369     * Ensures the specific preconditions of the said instruction. 1370     */ 1371    public void visitIDIV(IDIV o){ 1372        if (stack().peek() != Type.INT){ 1373            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1374        } 1375        if (stack().peek(1) != Type.INT){ 1376            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1377        } 1378    } 1379 1380    /** 1381     * Ensures the specific preconditions of the said instruction. 1382     */ 1383    public void visitIF_ACMPEQ(IF_ACMPEQ o){ 1384        if (!(stack().peek() instanceof ReferenceType)){ 1385            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'."); 1386        } 1387        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 1388     1389        if (!(stack().peek(1) instanceof ReferenceType)){ 1390            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'."); 1391        } 1392        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) ); 1393         1394    } 1395 1396    /** 1397     * Ensures the specific preconditions of the said instruction. 1398     */ 1399    public void visitIF_ACMPNE(IF_ACMPNE o){ 1400        if (!(stack().peek() instanceof ReferenceType)){ 1401            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'."); 1402            referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 1403        } 1404        if (!(stack().peek(1) instanceof ReferenceType)){ 1405            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'."); 1406            referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) ); 1407        } 1408    } 1409 1410    /** 1411     * Ensures the specific preconditions of the said instruction. 1412     */ 1413    public void visitIF_ICMPEQ(IF_ICMPEQ o){ 1414        if (stack().peek() != Type.INT){ 1415            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1416        } 1417        if (stack().peek(1) != Type.INT){ 1418            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1419        } 1420    } 1421 1422    /** 1423     * Ensures the specific preconditions of the said instruction. 1424     */ 1425    public void visitIF_ICMPGE(IF_ICMPGE o){ 1426        if (stack().peek() != Type.INT){ 1427            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1428        } 1429        if (stack().peek(1) != Type.INT){ 1430            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1431        } 1432    } 1433 1434    /** 1435     * Ensures the specific preconditions of the said instruction. 1436     */ 1437    public void visitIF_ICMPGT(IF_ICMPGT o){ 1438        if (stack().peek() != Type.INT){ 1439            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1440        } 1441        if (stack().peek(1) != Type.INT){ 1442            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1443        } 1444    } 1445 1446    /** 1447     * Ensures the specific preconditions of the said instruction. 1448     */ 1449    public void visitIF_ICMPLE(IF_ICMPLE o){ 1450        if (stack().peek() != Type.INT){ 1451            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1452        } 1453        if (stack().peek(1) != Type.INT){ 1454            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1455        } 1456    } 1457 1458    /** 1459     * Ensures the specific preconditions of the said instruction. 1460     */ 1461    public void visitIF_ICMPLT(IF_ICMPLT o){ 1462        if (stack().peek() != Type.INT){ 1463            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1464        } 1465        if (stack().peek(1) != Type.INT){ 1466            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1467        } 1468    } 1469 1470    /** 1471     * Ensures the specific preconditions of the said instruction. 1472     */ 1473    public void visitIF_ICMPNE(IF_ICMPNE o){ 1474        if (stack().peek() != Type.INT){ 1475            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1476        } 1477        if (stack().peek(1) != Type.INT){ 1478            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1479        } 1480    } 1481 1482    /** 1483     * Ensures the specific preconditions of the said instruction. 1484     */ 1485    public void visitIFEQ(IFEQ o){ 1486        if (stack().peek() != Type.INT){ 1487            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1488        } 1489    } 1490 1491    /** 1492     * Ensures the specific preconditions of the said instruction. 1493     */ 1494    public void visitIFGE(IFGE o){ 1495        if (stack().peek() != Type.INT){ 1496            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1497        } 1498    } 1499 1500    /** 1501     * Ensures the specific preconditions of the said instruction. 1502     */ 1503    public void visitIFGT(IFGT o){ 1504        if (stack().peek() != Type.INT){ 1505            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1506        } 1507    } 1508 1509    /** 1510     * Ensures the specific preconditions of the said instruction. 1511     */ 1512    public void visitIFLE(IFLE o){ 1513        if (stack().peek() != Type.INT){ 1514            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1515        } 1516    } 1517 1518    /** 1519     * Ensures the specific preconditions of the said instruction. 1520     */ 1521    public void visitIFLT(IFLT o){ 1522        if (stack().peek() != Type.INT){ 1523            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1524        } 1525    } 1526 1527    /** 1528     * Ensures the specific preconditions of the said instruction. 1529     */ 1530    public void visitIFNE(IFNE o){ 1531        if (stack().peek() != Type.INT){ 1532            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1533        } 1534    } 1535 1536    /** 1537     * Ensures the specific preconditions of the said instruction. 1538     */ 1539    public void visitIFNONNULL(IFNONNULL o){ 1540        if (!(stack().peek() instanceof ReferenceType)){ 1541            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'."); 1542        } 1543        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 1544    } 1545 1546    /** 1547     * Ensures the specific preconditions of the said instruction. 1548     */ 1549    public void visitIFNULL(IFNULL o){ 1550        if (!(stack().peek() instanceof ReferenceType)){ 1551            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'."); 1552        } 1553        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 1554    } 1555 1556    /** 1557     * Ensures the specific preconditions of the said instruction. 1558     */ 1559    public void visitIINC(IINC o){ 1560        // Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction. 1561 if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){ 1562            constraintViolated(o, "The 'index' is not a valid index into the local variable array."); 1563        } 1564 1565        indexOfInt(o, locals().get(o.getIndex())); 1566    } 1567 1568    /** 1569     * Ensures the specific preconditions of the said instruction. 1570     */ 1571    public void visitILOAD(ILOAD o){ 1572        // All done by visitLocalVariableInstruction(), visitLoadInstruction() 1573 } 1574 1575    /** 1576     * Ensures the specific preconditions of the said instruction. 1577     */ 1578    public void visitIMPDEP1(IMPDEP1 o){ 1579        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1."); 1580    } 1581 1582    /** 1583     * Ensures the specific preconditions of the said instruction. 1584     */ 1585    public void visitIMPDEP2(IMPDEP2 o){ 1586        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2."); 1587    } 1588 1589    /** 1590     * Ensures the specific preconditions of the said instruction. 1591     */ 1592    public void visitIMUL(IMUL o){ 1593        if (stack().peek() != Type.INT){ 1594            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1595        } 1596        if (stack().peek(1) != Type.INT){ 1597            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1598        } 1599    } 1600 1601    /** 1602     * Ensures the specific preconditions of the said instruction. 1603     */ 1604    public void visitINEG(INEG o){ 1605        if (stack().peek() != Type.INT){ 1606            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1607        } 1608    } 1609 1610    /** 1611     * Ensures the specific preconditions of the said instruction. 1612     */ 1613    public void visitINSTANCEOF(INSTANCEOF o){ 1614        // The objectref must be of type reference. 1615 Type objectref = stack().peek(0); 1616        if (!(objectref instanceof ReferenceType)){ 1617            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+"."); 1618        } 1619        else{ 1620            referenceTypeIsInitialized(o, (ReferenceType) objectref); 1621        } 1622        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the 1623 // current class (&#247;3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant 1624 // pool item at the index must be a symbolic reference to a class, array, or interface type. 1625 Constant c = cpg.getConstant(o.getIndex()); 1626        if (! (c instanceof ConstantClass)){ 1627            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'."); 1628        } 1629    } 1630 1631    /** 1632     * Ensures the specific preconditions of the said instruction. 1633     */ 1634    public void visitINVOKEINTERFACE(INVOKEINTERFACE o){ 1635        // Method is not native, otherwise pass 3 would not happen. 1636 1637        int count = o.getCount(); 1638        if (count == 0){ 1639            constraintViolated(o, "The 'count' argument must not be 0."); 1640        } 1641        // It is a ConstantInterfaceMethodref, Pass 3a made it sure. 1642 ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex())); 1643         1644        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o). 1645 1646        Type t = o.getType(cpg); 1647        if (t instanceof ObjectType){ 1648            String name = ((ObjectType)t).getClassName(); 1649            Verifier v = VerifierFactory.getVerifier( name ); 1650            VerificationResult vr = v.doPass2(); 1651            if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 1652                constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 1653            } 1654        } 1655 1656 1657        Type[] argtypes = o.getArgumentTypes(cpg); 1658        int nargs = argtypes.length; 1659         1660        for (int i=nargs-1; i>=0; i--){ 1661            Type fromStack = stack().peek( (nargs-1) - i ); // 0 to nargs-1 1662 Type fromDesc = argtypes[i]; 1663            if (fromDesc == Type.BOOLEAN || 1664                    fromDesc == Type.BYTE || 1665                    fromDesc == Type.CHAR || 1666                    fromDesc == Type.SHORT){ 1667                fromDesc = Type.INT; 1668            } 1669            if (! fromStack.equals(fromDesc)){ 1670                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){ 1671                    ReferenceType rFromStack = (ReferenceType) fromStack; 1672                    ReferenceType rFromDesc = (ReferenceType) fromDesc; 1673                    // TODO: This can only be checked when using Staerk-et-al's "set of object types" 1674 // instead of a "wider cast object type" created during verification. 1675 //if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){ 1676 // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible)."); 1677 //} 1678 } 1679                else{ 1680                    constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack."); 1681                } 1682            } 1683        } 1684         1685        Type objref = stack().peek(nargs); 1686        if (objref == Type.NULL){ 1687            return; 1688        } 1689        if (! (objref instanceof ReferenceType) ){ 1690            constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'."); 1691        } 1692        referenceTypeIsInitialized(o, (ReferenceType) objref); 1693        if (!(objref instanceof ObjectType)){ 1694            if (!(objref instanceof ArrayType)){ 1695                constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType 1696 } 1697            else{ 1698                objref = GENERIC_ARRAY; 1699            } 1700        } 1701         1702        String objref_classname = ((ObjectType) objref).getClassName(); 1703 1704        String theInterface = o.getClassName(cpg); 1705     1706        // TODO: This can only be checked if we're using Staerk-et-al's "set of object types" 1707 // instead of "wider cast object types" generated during verification. 1708 //if ( ! Repository.implementationOf(objref_classname, theInterface) ){ 1709 // constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theInterface+"' as expected."); 1710 //} 1711 1712        int counted_count = 1; // 1 for the objectref 1713 for (int i=0; i<nargs; i++){ 1714            counted_count += argtypes[i].getSize(); 1715        } 1716        if (count != counted_count){ 1717            constraintViolated(o, "The 'count' argument should probably read '"+counted_count+"' but is '"+count+"'."); 1718        } 1719    } 1720 1721    /** 1722     * Ensures the specific preconditions of the said instruction. 1723     */ 1724    public void visitINVOKESPECIAL(INVOKESPECIAL o){ 1725        // Don't init an object twice. 1726 if ( (o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME)) && (!(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) ){ 1727            constraintViolated(o, "Possibly initializing object twice. A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable during a backwards branch, or in a local variable in code protected by an exception handler. Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details."); 1728        } 1729 1730        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o). 1731 1732        Type t = o.getType(cpg); 1733        if (t instanceof ObjectType){ 1734            String name = ((ObjectType)t).getClassName(); 1735            Verifier v = VerifierFactory.getVerifier( name ); 1736            VerificationResult vr = v.doPass2(); 1737            if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 1738                constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 1739            } 1740        } 1741 1742 1743        Type[] argtypes = o.getArgumentTypes(cpg); 1744        int nargs = argtypes.length; 1745         1746        for (int i=nargs-1; i>=0; i--){ 1747            Type fromStack = stack().peek( (nargs-1) - i ); // 0 to nargs-1 1748 Type fromDesc = argtypes[i]; 1749            if (fromDesc == Type.BOOLEAN || 1750                    fromDesc == Type.BYTE || 1751                    fromDesc == Type.CHAR || 1752                    fromDesc == Type.SHORT){ 1753                fromDesc = Type.INT; 1754            } 1755            if (! fromStack.equals(fromDesc)){ 1756                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){ 1757                    ReferenceType rFromStack = (ReferenceType) fromStack; 1758                    ReferenceType rFromDesc = (ReferenceType) fromDesc; 1759                    // TODO: This can only be checked using Staerk-et-al's "set of object types", not 1760 // using a "wider cast object type". 1761 //if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){ 1762 // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible)."); 1763 //} 1764 } 1765                else{ 1766                    constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack."); 1767                } 1768            } 1769        } 1770         1771        Type objref = stack().peek(nargs); 1772        if (objref == Type.NULL){ 1773            return; 1774        } 1775        if (! (objref instanceof ReferenceType) ){ 1776            constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'."); 1777        } 1778        String objref_classname = null; 1779        if ( !(o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME))){ 1780            referenceTypeIsInitialized(o, (ReferenceType) objref); 1781            if (!(objref instanceof ObjectType)){ 1782                if (!(objref instanceof ArrayType)){ 1783                    constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType 1784 } 1785                else{ 1786                    objref = GENERIC_ARRAY; 1787                } 1788            } 1789 1790            objref_classname = ((ObjectType) objref).getClassName(); 1791        } 1792        else{ 1793            if (!(objref instanceof UninitializedObjectType)){ 1794                constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '"+objref+"'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address)."); 1795            } 1796            objref_classname = ((UninitializedObjectType) objref).getInitialized().getClassName(); 1797        } 1798         1799 1800        String theClass = o.getClassName(cpg); 1801        if ( ! Repository.instanceOf(objref_classname, theClass) ){ 1802            constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected."); 1803        } 1804         1805    } 1806 1807    /** 1808     * Ensures the specific preconditions of the said instruction. 1809     */ 1810    public void visitINVOKESTATIC(INVOKESTATIC o){ 1811        // Method is not native, otherwise pass 3 would not happen. 1812 1813        Type t = o.getType(cpg); 1814        if (t instanceof ObjectType){ 1815            String name = ((ObjectType)t).getClassName(); 1816            Verifier v = VerifierFactory.getVerifier( name ); 1817            VerificationResult vr = v.doPass2(); 1818            if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 1819                constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 1820            } 1821        } 1822 1823        Type[] argtypes = o.getArgumentTypes(cpg); 1824        int nargs = argtypes.length; 1825         1826        for (int i=nargs-1; i>=0; i--){ 1827            Type fromStack = stack().peek( (nargs-1) - i ); // 0 to nargs-1 1828 Type fromDesc = argtypes[i]; 1829            if (fromDesc == Type.BOOLEAN || 1830                    fromDesc == Type.BYTE || 1831                    fromDesc == Type.CHAR || 1832                    fromDesc == Type.SHORT){ 1833                fromDesc = Type.INT; 1834            } 1835            if (! fromStack.equals(fromDesc)){ 1836                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){ 1837                    ReferenceType rFromStack = (ReferenceType) fromStack; 1838                    ReferenceType rFromDesc = (ReferenceType) fromDesc; 1839                    // TODO: This check can only be done using Staerk-et-al's "set of object types" 1840 // instead of a "wider cast object type" created during verification. 1841 //if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){ 1842 // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible)."); 1843 //} 1844 } 1845                else{ 1846                    constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack."); 1847                } 1848            } 1849        } 1850    } 1851 1852    /** 1853     * Ensures the specific preconditions of the said instruction. 1854     */ 1855    public void visitINVOKEVIRTUAL(INVOKEVIRTUAL o){ 1856        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o). 1857 1858        Type t = o.getType(cpg); 1859        if (t instanceof ObjectType){ 1860            String name = ((ObjectType)t).getClassName(); 1861            Verifier v = VerifierFactory.getVerifier( name ); 1862            VerificationResult vr = v.doPass2(); 1863            if (vr.getStatus() != VerificationResult.VERIFIED_OK){ 1864                constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'."); 1865            } 1866        } 1867 1868 1869        Type[] argtypes = o.getArgumentTypes(cpg); 1870        int nargs = argtypes.length; 1871         1872        for (int i=nargs-1; i>=0; i--){ 1873            Type fromStack = stack().peek( (nargs-1) - i ); // 0 to nargs-1 1874 Type fromDesc = argtypes[i]; 1875            if (fromDesc == Type.BOOLEAN || 1876                    fromDesc == Type.BYTE || 1877                    fromDesc == Type.CHAR || 1878                    fromDesc == Type.SHORT){ 1879                fromDesc = Type.INT; 1880            } 1881            if (! fromStack.equals(fromDesc)){ 1882                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){ 1883                    ReferenceType rFromStack = (ReferenceType) fromStack; 1884                    ReferenceType rFromDesc = (ReferenceType) fromDesc; 1885                    // TODO: This can only be checked when using Staerk-et-al's "set of object types" instead 1886 // of a single "wider cast object type" created during verification. 1887 //if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){ 1888 // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible)."); 1889 //} 1890 } 1891                else{ 1892                    constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack."); 1893                } 1894            } 1895        } 1896         1897        Type objref = stack().peek(nargs); 1898        if (objref == Type.NULL){ 1899            return; 1900        } 1901        if (! (objref instanceof ReferenceType) ){ 1902            constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'."); 1903        } 1904        referenceTypeIsInitialized(o, (ReferenceType) objref); 1905        if (!(objref instanceof ObjectType)){ 1906            if (!(objref instanceof ArrayType)){ 1907                constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType 1908 } 1909            else{ 1910                objref = GENERIC_ARRAY; 1911            } 1912        } 1913         1914        String objref_classname = ((ObjectType) objref).getClassName(); 1915 1916        String theClass = o.getClassName(cpg); 1917     1918        if ( ! Repository.instanceOf(objref_classname, theClass) ){ 1919            constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected."); 1920        } 1921    } 1922 1923    /** 1924     * Ensures the specific preconditions of the said instruction. 1925     */ 1926    public void visitIOR(IOR o){ 1927        if (stack().peek() != Type.INT){ 1928            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1929        } 1930        if (stack().peek(1) != Type.INT){ 1931            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1932        } 1933    } 1934 1935    /** 1936     * Ensures the specific preconditions of the said instruction. 1937     */ 1938    public void visitIREM(IREM o){ 1939        if (stack().peek() != Type.INT){ 1940            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1941        } 1942        if (stack().peek(1) != Type.INT){ 1943            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1944        } 1945    } 1946 1947    /** 1948     * Ensures the specific preconditions of the said instruction. 1949     */ 1950    public void visitIRETURN(IRETURN o){ 1951        if (stack().peek() != Type.INT){ 1952            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1953        } 1954    } 1955 1956    /** 1957     * Ensures the specific preconditions of the said instruction. 1958     */ 1959    public void visitISHL(ISHL o){ 1960        if (stack().peek() != Type.INT){ 1961            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1962        } 1963        if (stack().peek(1) != Type.INT){ 1964            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1965        } 1966    } 1967 1968    /** 1969     * Ensures the specific preconditions of the said instruction. 1970     */ 1971    public void visitISHR(ISHR o){ 1972        if (stack().peek() != Type.INT){ 1973            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1974        } 1975        if (stack().peek(1) != Type.INT){ 1976            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1977        } 1978    } 1979 1980    /** 1981     * Ensures the specific preconditions of the said instruction. 1982     */ 1983    public void visitISTORE(ISTORE o){ 1984        //visitStoreInstruction(StoreInstruction) is called before. 1985 1986        // Nothing else needs to be done here. 1987 } 1988 1989    /** 1990     * Ensures the specific preconditions of the said instruction. 1991     */ 1992    public void visitISUB(ISUB o){ 1993        if (stack().peek() != Type.INT){ 1994            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 1995        } 1996        if (stack().peek(1) != Type.INT){ 1997            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 1998        } 1999    } 2000 2001    /** 2002     * Ensures the specific preconditions of the said instruction. 2003     */ 2004    public void visitIUSHR(IUSHR o){ 2005        if (stack().peek() != Type.INT){ 2006            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2007        } 2008        if (stack().peek(1) != Type.INT){ 2009            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 2010        } 2011    } 2012 2013    /** 2014     * Ensures the specific preconditions of the said instruction. 2015     */ 2016    public void visitIXOR(IXOR o){ 2017        if (stack().peek() != Type.INT){ 2018            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2019        } 2020        if (stack().peek(1) != Type.INT){ 2021            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'."); 2022        } 2023    } 2024 2025    /** 2026     * Ensures the specific preconditions of the said instruction. 2027     */ 2028    public void visitJSR(JSR o){ 2029        // nothing to do here. 2030 } 2031 2032    /** 2033     * Ensures the specific preconditions of the said instruction. 2034     */ 2035    public void visitJSR_W(JSR_W o){ 2036        // nothing to do here. 2037 } 2038 2039    /** 2040     * Ensures the specific preconditions of the said instruction. 2041     */ 2042    public void visitL2D(L2D o){ 2043        if (stack().peek() != Type.LONG){ 2044            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2045        } 2046    } 2047 2048    /** 2049     * Ensures the specific preconditions of the said instruction. 2050     */ 2051    public void visitL2F(L2F o){ 2052        if (stack().peek() != Type.LONG){ 2053            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2054        } 2055    } 2056 2057    /** 2058     * Ensures the specific preconditions of the said instruction. 2059     */ 2060    public void visitL2I(L2I o){ 2061        if (stack().peek() != Type.LONG){ 2062            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2063        } 2064    } 2065 2066    /** 2067     * Ensures the specific preconditions of the said instruction. 2068     */ 2069    public void visitLADD(LADD o){ 2070        if (stack().peek() != Type.LONG){ 2071            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2072        } 2073        if (stack().peek(1) != Type.LONG){ 2074            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2075        } 2076    } 2077 2078    /** 2079     * Ensures the specific preconditions of the said instruction. 2080     */ 2081    public void visitLALOAD(LALOAD o){ 2082        indexOfInt(o, stack().peek()); 2083        if (stack().peek(1) == Type.NULL){ 2084            return; 2085        } 2086        if (! (stack().peek(1) instanceof ArrayType)){ 2087            constraintViolated(o, "Stack next-to-top must be of type long[] but is '"+stack().peek(1)+"'."); 2088        } 2089        Type t = ((ArrayType) (stack().peek(1))).getBasicType(); 2090        if (t != Type.LONG){ 2091            constraintViolated(o, "Stack next-to-top must be of type long[] but is '"+stack().peek(1)+"'."); 2092        } 2093    } 2094 2095    /** 2096     * Ensures the specific preconditions of the said instruction. 2097     */ 2098    public void visitLAND(LAND o){ 2099        if (stack().peek() != Type.LONG){ 2100            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2101        } 2102        if (stack().peek(1) != Type.LONG){ 2103            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2104        } 2105    } 2106 2107    /** 2108     * Ensures the specific preconditions of the said instruction. 2109     */ 2110    public void visitLASTORE(LASTORE o){ 2111        if (stack().peek() != Type.LONG){ 2112            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2113        } 2114        indexOfInt(o, stack().peek(1)); 2115        if (stack().peek(2) == Type.NULL){ 2116            return; 2117        } 2118        if (! (stack().peek(2) instanceof ArrayType)){ 2119            constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '"+stack().peek(2)+"'."); 2120        } 2121        Type t = ((ArrayType) (stack().peek(2))).getBasicType(); 2122        if (t != Type.LONG){ 2123            constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '"+stack().peek(2)+"'."); 2124        } 2125    } 2126 2127    /** 2128     * Ensures the specific preconditions of the said instruction. 2129     */ 2130    public void visitLCMP(LCMP o){ 2131        if (stack().peek() != Type.LONG){ 2132            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2133        } 2134        if (stack().peek(1) != Type.LONG){ 2135            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2136        } 2137    } 2138 2139    /** 2140     * Ensures the specific preconditions of the said instruction. 2141     */ 2142    public void visitLCONST(LCONST o){ 2143        // Nothing to do here. 2144 } 2145 2146    /** 2147     * Ensures the specific preconditions of the said instruction. 2148     */ 2149    public void visitLDC(LDC o){ 2150        // visitCPInstruction is called first. 2151 2152        Constant c = cpg.getConstant(o.getIndex()); 2153        if (! ( ( c instanceof ConstantInteger) || 2154                            ( c instanceof ConstantFloat ) || 2155                            ( c instanceof ConstantString ) ) ){ 2156            constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'."); 2157        } 2158    } 2159 2160    /** 2161     * Ensures the specific preconditions of the said instruction. 2162     */ 2163    public void visitLDC_W(LDC_W o){ 2164        // visitCPInstruction is called first. 2165 2166        Constant c = cpg.getConstant(o.getIndex()); 2167        if (! ( ( c instanceof ConstantInteger) || 2168                            ( c instanceof ConstantFloat ) || 2169                            ( c instanceof ConstantString ) ) ){ 2170            constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'."); 2171        } 2172    } 2173 2174    /** 2175     * Ensures the specific preconditions of the said instruction. 2176     */ 2177    public void visitLDC2_W(LDC2_W o){ 2178        // visitCPInstruction is called first. 2179 2180        Constant c = cpg.getConstant(o.getIndex()); 2181        if (! ( ( c instanceof ConstantLong) || 2182                            ( c instanceof ConstantDouble ) ) ){ 2183            constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'."); 2184        } 2185    } 2186 2187    /** 2188     * Ensures the specific preconditions of the said instruction. 2189     */ 2190    public void visitLDIV(LDIV o){ 2191        if (stack().peek() != Type.LONG){ 2192            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2193        } 2194        if (stack().peek(1) != Type.LONG){ 2195            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2196        } 2197    } 2198 2199    /** 2200     * Ensures the specific preconditions of the said instruction. 2201     */ 2202    public void visitLLOAD(LLOAD o){ 2203        //visitLoadInstruction(LoadInstruction) is called before. 2204 2205        // Nothing else needs to be done here. 2206 } 2207 2208    /** 2209     * Ensures the specific preconditions of the said instruction. 2210     */ 2211    public void visitLMUL(LMUL o){ 2212        if (stack().peek() != Type.LONG){ 2213            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2214        } 2215        if (stack().peek(1) != Type.LONG){ 2216            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2217        } 2218    } 2219 2220    /** 2221     * Ensures the specific preconditions of the said instruction. 2222     */ 2223    public void visitLNEG(LNEG o){ 2224        if (stack().peek() != Type.LONG){ 2225            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2226        } 2227    } 2228     2229    /** 2230     * Ensures the specific preconditions of the said instruction. 2231     */ 2232    public void visitLOOKUPSWITCH(LOOKUPSWITCH o){ 2233        if (stack().peek() != Type.INT){ 2234            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2235        } 2236        // See also pass 3a. 2237 } 2238 2239    /** 2240     * Ensures the specific preconditions of the said instruction. 2241     */ 2242    public void visitLOR(LOR o){ 2243        if (stack().peek() != Type.LONG){ 2244            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2245        } 2246        if (stack().peek(1) != Type.LONG){ 2247            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2248        } 2249    } 2250 2251    /** 2252     * Ensures the specific preconditions of the said instruction. 2253     */ 2254    public void visitLREM(LREM o){ 2255        if (stack().peek() != Type.LONG){ 2256            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2257        } 2258        if (stack().peek(1) != Type.LONG){ 2259            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2260        } 2261    } 2262 2263    /** 2264     * Ensures the specific preconditions of the said instruction. 2265     */ 2266    public void visitLRETURN(LRETURN o){ 2267        if (stack().peek() != Type.LONG){ 2268            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2269        } 2270    } 2271 2272    /** 2273     * Ensures the specific preconditions of the said instruction. 2274     */ 2275    public void visitLSHL(LSHL o){ 2276        if (stack().peek() != Type.INT){ 2277            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2278        } 2279        if (stack().peek(1) != Type.LONG){ 2280            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2281        } 2282    } 2283 2284    /** 2285     * Ensures the specific preconditions of the said instruction. 2286     */ 2287    public void visitLSHR(LSHR o){ 2288        if (stack().peek() != Type.INT){ 2289            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2290        } 2291        if (stack().peek(1) != Type.LONG){ 2292            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2293        } 2294    } 2295 2296    /** 2297     * Ensures the specific preconditions of the said instruction. 2298     */ 2299    public void visitLSTORE(LSTORE o){ 2300        //visitStoreInstruction(StoreInstruction) is called before. 2301 2302        // Nothing else needs to be done here. 2303 } 2304 2305    /** 2306     * Ensures the specific preconditions of the said instruction. 2307     */ 2308    public void visitLSUB(LSUB o){ 2309        if (stack().peek() != Type.LONG){ 2310            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2311        } 2312        if (stack().peek(1) != Type.LONG){ 2313            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2314        } 2315    } 2316 2317    /** 2318     * Ensures the specific preconditions of the said instruction. 2319     */ 2320    public void visitLUSHR(LUSHR o){ 2321        if (stack().peek() != Type.INT){ 2322            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2323        } 2324        if (stack().peek(1) != Type.LONG){ 2325            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2326        } 2327    } 2328 2329    /** 2330     * Ensures the specific preconditions of the said instruction. 2331     */ 2332    public void visitLXOR(LXOR o){ 2333        if (stack().peek() != Type.LONG){ 2334            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'."); 2335        } 2336        if (stack().peek(1) != Type.LONG){ 2337            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'."); 2338        } 2339    } 2340 2341    /** 2342     * Ensures the specific preconditions of the said instruction. 2343     */ 2344    public void visitMONITORENTER(MONITORENTER o){ 2345        if (! ((stack().peek()) instanceof ReferenceType)){ 2346            constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'."); 2347        } 2348        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 2349    } 2350 2351    /** 2352     * Ensures the specific preconditions of the said instruction. 2353     */ 2354    public void visitMONITOREXIT(MONITOREXIT o){ 2355        if (! ((stack().peek()) instanceof ReferenceType)){ 2356            constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'."); 2357        } 2358        referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) ); 2359    } 2360 2361    /** 2362     * Ensures the specific preconditions of the said instruction. 2363     */ 2364    public void visitMULTIANEWARRAY(MULTIANEWARRAY o){ 2365        int dimensions = o.getDimensions(); 2366        // Dimensions argument is okay: see Pass 3a. 2367 for (int i=0; i<dimensions; i++){ 2368            if (stack().peek(i) != Type.INT){ 2369                constraintViolated(o, "The '"+dimensions+"' upper stack types should be 'int' but aren't."); 2370            } 2371        } 2372        // The runtime constant pool item at that index must be a symbolic reference to a class, 2373 // array, or interface type. See Pass 3a. 2374 } 2375 2376    /** 2377     * Ensures the specific preconditions of the said instruction. 2378     */ 2379    public void visitNEW(NEW o){ 2380        //visitCPInstruction(CPInstruction) has been called before. 2381 //visitLoadClass(LoadClass) has been called before. 2382 2383        Type t = o.getType(cpg); 2384        if (! (t instanceof ReferenceType)){ 2385            throw new AssertionViolatedException("NEW.getType() returning a non-reference type?!"); 2386        } 2387        if (! (t instanceof ObjectType)){ 2388            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+t+"'."); 2389        } 2390        ObjectType obj = (ObjectType) t; 2391 2392        //e.g.: Don't instantiate interfaces 2393 if (! obj.referencesClass()){ 2394            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+obj+"'."); 2395        } 2396    } 2397 2398    /** 2399     * Ensures the specific preconditions of the said instruction. 2400     */ 2401    public void visitNEWARRAY(NEWARRAY o){ 2402        if (stack().peek() != Type.INT){ 2403            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2404        } 2405    } 2406 2407    /** 2408     * Ensures the specific preconditions of the said instruction. 2409     */ 2410    public void visitNOP(NOP o){ 2411        // nothing is to be done here. 2412 } 2413 2414    /** 2415     * Ensures the specific preconditions of the said instruction. 2416     */ 2417    public void visitPOP(POP o){ 2418        if (stack().peek().getSize() != 1){ 2419            constraintViolated(o, "Stack top size should be 1 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'."); 2420        } 2421    } 2422 2423    /** 2424     * Ensures the specific preconditions of the said instruction. 2425     */ 2426    public void visitPOP2(POP2 o){ 2427        if (stack().peek().getSize() != 2){ 2428            constraintViolated(o, "Stack top size should be 2 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'."); 2429        } 2430    } 2431 2432    /** 2433     * Ensures the specific preconditions of the said instruction. 2434     */ 2435    public void visitPUTFIELD(PUTFIELD o){ 2436 2437        Type objectref = stack().peek(1); 2438        if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){ 2439            constraintViolated(o, "Stack next-to-top should be an object reference that's not an array reference, but is '"+objectref+"'."); 2440        } 2441         2442        String field_name = o.getFieldName(cpg); 2443         2444        JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName()); 2445        Field[] fields = jc.getFields(); 2446        Field f = null; 2447        for (int i=0; i<fields.length; i++){ 2448            if (fields[i].getName().equals(field_name)){ 2449                f = fields[i]; 2450                break; 2451            } 2452        } 2453        if (f == null){ 2454            throw new AssertionViolatedException("Field not found?!?"); 2455        } 2456 2457        Type value = stack().peek(); 2458        Type t = Type.getType(f.getSignature()); 2459        Type shouldbe = t; 2460        if (shouldbe == Type.BOOLEAN || 2461                shouldbe == Type.BYTE || 2462                shouldbe == Type.CHAR || 2463                shouldbe == Type.SHORT){ 2464            shouldbe = Type.INT; 2465        } 2466        if (t instanceof ReferenceType){ 2467            ReferenceType rvalue = null; 2468            if (value instanceof ReferenceType){ 2469                rvalue = (ReferenceType) value; 2470                referenceTypeIsInitialized(o, rvalue); 2471            } 2472            else{ 2473                constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected."); 2474            } 2475            // TODO: This can only be checked using Staerk-et-al's "set-of-object types", not 2476 // using "wider cast object types" created during verification. 2477 //if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){ 2478 // constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'."); 2479 //} 2480 } 2481        else{ 2482            if (shouldbe != value){ 2483                constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected."); 2484            } 2485        } 2486         2487        if (f.isProtected()){ 2488            ObjectType classtype = o.getClassType(cpg); 2489            ObjectType curr = new ObjectType(mg.getClassName()); 2490 2491            if ( classtype.equals(curr) || 2492                        curr.subclassOf(classtype) ){ 2493                Type tp = stack().peek(1); 2494                if (tp == Type.NULL){ 2495                    return; 2496                } 2497                if (! (tp instanceof ObjectType) ){ 2498                    constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+tp+"'."); 2499                } 2500                ObjectType objreftype = (ObjectType) tp; 2501                if (! ( objreftype.equals(curr) || 2502                            objreftype.subclassOf(curr) ) ){ 2503                    constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or a superclass of the current class. However, the referenced object type '"+stack().peek()+"' is not the current class or a subclass of the current class."); 2504                } 2505            } 2506        } 2507 2508        // TODO: Could go into Pass 3a. 2509 if (f.isStatic()){ 2510            constraintViolated(o, "Referenced field '"+f+"' is static which it shouldn't be."); 2511        } 2512    } 2513 2514    /** 2515     * Ensures the specific preconditions of the said instruction. 2516     */ 2517    public void visitPUTSTATIC(PUTSTATIC o){ 2518        String field_name = o.getFieldName(cpg); 2519        JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName()); 2520        Field[] fields = jc.getFields(); 2521        Field f = null; 2522        for (int i=0; i<fields.length; i++){ 2523            if (fields[i].getName().equals(field_name)){ 2524                f = fields[i]; 2525                break; 2526            } 2527        } 2528        if (f == null){ 2529            throw new AssertionViolatedException("Field not found?!?"); 2530        } 2531        Type value = stack().peek(); 2532        Type t = Type.getType(f.getSignature()); 2533        Type shouldbe = t; 2534        if (shouldbe == Type.BOOLEAN || 2535                shouldbe == Type.BYTE || 2536                shouldbe == Type.CHAR || 2537                shouldbe == Type.SHORT){ 2538            shouldbe = Type.INT; 2539        } 2540        if (t instanceof ReferenceType){ 2541            ReferenceType rvalue = null; 2542            if (value instanceof ReferenceType){ 2543                rvalue = (ReferenceType) value; 2544                referenceTypeIsInitialized(o, rvalue); 2545            } 2546            else{ 2547                constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected."); 2548            } 2549            if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){ 2550                constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'."); 2551            } 2552        } 2553        else{ 2554            if (shouldbe != value){ 2555                constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected."); 2556            } 2557        } 2558        // TODO: Interface fields may be assigned to only once. (Hard to implement in 2559 // JustIce's execution model). This may only happen in <clinit>, see Pass 3a. 2560 } 2561 2562    /** 2563     * Ensures the specific preconditions of the said instruction. 2564     */ 2565    public void visitRET(RET o){ 2566        if (! (locals().get(o.getIndex()) instanceof ReturnaddressType)){ 2567            constraintViolated(o, "Expecting a ReturnaddressType in local variable "+o.getIndex()+"."); 2568        } 2569        if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET){ 2570            throw new AssertionViolatedException("Oops: RET expecting a target!"); 2571        } 2572        // Other constraints such as non-allowed overlapping subroutines are enforced 2573 // while building the Subroutines data structure. 2574 } 2575 2576    /** 2577     * Ensures the specific preconditions of the said instruction. 2578     */ 2579    public void visitRETURN(RETURN o){ 2580        if (mg.getName().equals(Constants.CONSTRUCTOR_NAME)){// If we leave an <init> method 2581 if ((frame._this != null) && (!(mg.getClassName().equals(Type.OBJECT.getClassName()))) ) { 2582                constraintViolated(o, "Leaving a constructor that itself did not call a constructor."); 2583            } 2584        } 2585    } 2586 2587    /** 2588     * Ensures the specific preconditions of the said instruction. 2589     */ 2590    public void visitSALOAD(SALOAD o){ 2591        indexOfInt(o, stack().peek()); 2592        if (stack().peek(1) == Type.NULL){ 2593            return; 2594        } 2595        if (! (stack().peek(1) instanceof ArrayType)){ 2596            constraintViolated(o, "Stack next-to-top must be of type short[] but is '"+stack().peek(1)+"'."); 2597        } 2598        Type t = ((ArrayType) (stack().peek(1))).getBasicType(); 2599        if (t != Type.SHORT){ 2600            constraintViolated(o, "Stack next-to-top must be of type short[] but is '"+stack().peek(1)+"'."); 2601        } 2602    } 2603 2604    /** 2605     * Ensures the specific preconditions of the said instruction. 2606     */ 2607    public void visitSASTORE(SASTORE o){ 2608        if (stack().peek() != Type.INT){ 2609            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'."); 2610        } 2611        indexOfInt(o, stack().peek(1)); 2612        if (stack().peek(2) == Type.NULL){ 2613            return; 2614        } 2615        if (! (stack().peek(2) instanceof ArrayType)){ 2616            constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '"+stack().peek(2)+"'."); 2617        } 2618        Type t = ((ArrayType) (stack().peek(2))).getBasicType(); 2619        if (t != Type.SHORT){ 2620            constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '"+stack().peek(2)+"'."); 2621        } 2622    } 2623 2624    /** 2625     * Ensures the specific preconditions of the said instruction. 2626     */ 2627    public void visitSIPUSH(SIPUSH o){ 2628        // nothing to do here. Generic visitXXX() methods did the trick before. 2629 } 2630 2631    /** 2632     * Ensures the specific preconditions of the said instruction. 2633     */ 2634    public void visitSWAP(SWAP o){ 2635        if (stack().peek().getSize() != 1){ 2636            constraintViolated(o, "The value at the stack top is not of size '1', but of size '"+stack().peek().getSize()+"'."); 2637        } 2638        if (stack().peek(1).getSize() != 1){ 2639            constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '"+stack().peek(1).getSize()+"'."); 2640        } 2641    } 2642 2643    /** 2644     * Ensures the specific preconditions of the said instruction. 2645     */ 2646    public void visitTABLESWITCH(TABLESWITCH o){ 2647        indexOfInt(o, stack().peek()); 2648        // See Pass 3a. 2649 } 2650 2651} 2652 2653

A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame Popular Tags