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