instconstraintvisitor.java

来自「JAVA的一些源码 JAVA2 STANDARD EDITION DEVELO」· Java 代码 · 共 1,790 行 · 第 1/5 页

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ICMPGT(IF_ICMPGT o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		if (stack().peek(1) != Type.INT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ICMPLE(IF_ICMPLE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		if (stack().peek(1) != Type.INT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ICMPLT(IF_ICMPLT o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		if (stack().peek(1) != Type.INT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ICMPNE(IF_ICMPNE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		if (stack().peek(1) != Type.INT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFEQ(IFEQ o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFGE(IFGE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFGT(IFGT o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFLE(IFLE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFLT(IFLT o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFNE(IFNE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFNONNULL(IFNONNULL o){
		if (!(stack().peek() instanceof ReferenceType)){
			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
		}
		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );	
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIFNULL(IFNULL o){
		if (!(stack().peek() instanceof ReferenceType)){
			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
		}
		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );	
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIINC(IINC o){
		// Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction.
		if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
			constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
		}

		indexOfInt(o, locals().get(o.getIndex()));
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitILOAD(ILOAD o){
		// All done by visitLocalVariableInstruction(), visitLoadInstruction()
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIMPDEP1(IMPDEP1 o){
		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIMPDEP2(IMPDEP2 o){
		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIMUL(IMUL o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		if (stack().peek(1) != Type.INT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitINEG(INEG o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitINSTANCEOF(INSTANCEOF o){
		// The objectref must be of type reference.
		Type objectref = stack().peek(0);
		if (!(objectref instanceof ReferenceType)){
			constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
		}
		else{
			referenceTypeIsInitialized(o, (ReferenceType) objectref);
		}
		// The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
		// current class (&#247;3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
		// pool item at the index must be a symbolic reference to a class, array, or interface type.
		Constant c = cpg.getConstant(o.getIndex());
		if (! (c instanceof ConstantClass)){
			constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitINVOKEINTERFACE(INVOKEINTERFACE o){
		// Method is not native, otherwise pass 3 would not happen.
		
		int count = o.getCount();
		if (count == 0){
			constraintViolated(o, "The 'count' argument must not be 0.");
		}
		// It is a ConstantInterfaceMethodref, Pass 3a made it sure.
		ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex()));
		
		// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

		Type t = o.getType(cpg);
		if (t instanceof ObjectType){
			String name = ((ObjectType)t).getClassName();
			Verifier v = VerifierFactory.getVerifier( name );
			VerificationResult vr = v.doPass2();
			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
			}
		}


		Type[] argtypes = o.getArgumentTypes(cpg);
		int nargs = argtypes.length;
		
		for (int i=nargs-1; i>=0; i--){
			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
			Type fromDesc = argtypes[i];
			if (fromDesc == Type.BOOLEAN ||
					fromDesc == Type.BYTE ||
					fromDesc == Type.CHAR ||
					fromDesc == Type.SHORT){
				fromDesc = Type.INT;
			}
			if (! fromStack.equals(fromDesc)){
				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
					ReferenceType rFromStack = (ReferenceType) fromStack;
					ReferenceType rFromDesc = (ReferenceType) fromDesc;
					// TODO: This can only be checked when using Staerk-et-al's "set of object types"
					// instead of a "wider cast object type" created during verification.
					//if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
					//	constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
					//}
				}
				else{
					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
				}
			}
		}
		
		Type objref = stack().peek(nargs);
		if (objref == Type.NULL){
			return;
		}
		if (! (objref instanceof ReferenceType) ){
			constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'.");
		}
		referenceTypeIsInitialized(o, (ReferenceType) objref);
		if (!(objref instanceof ObjectType)){
			if (!(objref instanceof ArrayType)){
				constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType
			}
			else{
				objref = GENERIC_ARRAY;
			}
		}
		
		String objref_classname = ((ObjectType) objref).getClassName();

		String theInterface = o.getClassName(cpg);
	
		// TODO: This can only be checked if we're using Staerk-et-al's "set of object types"
		//       instead of "wider cast object types" generated during verification.
		//if ( ! Repository.implementationOf(objref_classname, theInterface) ){
		//	constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theInterface+"' as expected.");
		//}	

		int counted_count = 1; // 1 for the objectref
		for (int i=0; i<nargs; i++){
			counted_count += argtypes[i].getSize();
		}
		if (count != counted_count){
			constraintViolated(o, "The 'count' argument should probably read '"+counted_count+"' but is '"+count+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitINVOKESPECIAL(INVOKESPECIAL o){
		// Don't init an object twice.
		if ( (o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME)) && (!(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) ){
			constraintViolated(o, "Possibly initializing object twice. A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable during a backwards branch, or in a local variable in code protected by an exception handler. Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details.");
		}

		// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

		Type t = o.getType(cpg);
		if (t instanceof ObjectType){
			String name = ((ObjectType)t).getClassName();
			Verifier v = VerifierFactory.getVerifier( name );
			VerificationResult vr = v.doPass2();
			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
			}
		}


		Type[] argtypes = o.getArgumentTypes(cpg);
		int nargs = argtypes.length;
		
		for (int i=nargs-1; i>=0; i--){
			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
			Type fromDesc = argtypes[i];
			if (fromDesc == Type.BOOLEAN ||
					fromDesc == Type.BYTE ||
					fromDesc == Type.CHAR ||
					fromDesc == Type.SHORT){
				fromDesc = Type.INT;
			}
			if (! fromStack.equals(fromDesc)){
				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
					ReferenceType rFromStack = (ReferenceType) fromStack;
					ReferenceType rFromDesc = (ReferenceType) fromDesc;
					// TODO: This can only be checked using Staerk-et-al's "set of object types", not
					// using a "wider cast object type".
					//if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
					//	constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
					//}
				}
				else{
					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
				}
			}
		}
		
		Type objref = stack().peek(nargs);
		if (objref == Type.NULL){
			return;
		}
		if (! (objref instanceof ReferenceType) ){
			constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'.");
		}
		String objref_classname = null;
		if ( !(o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME))){
			referenceTypeIsInitialized(o, (ReferenceType) objref);
			if (!(objref instanceof ObjectType)){
				if (!(objref instanceof ArrayType)){
					constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType
				}
				else{
					objref = GENERIC_ARRAY;
				}
			}

			objref_cl