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

This page was automatically generated by Maven