instconstraintvisitor.java

该开源工具主要用于class文件的操作

	 */
	public void visitStackInstruction(StackInstruction o){
		_visitStackAccessor(o);
	}

	/**
	 * Assures the generic preconditions of a LocalVariableInstruction instance.
	 * That is, the index of the local variable must be valid.
	 */
	public void visitLocalVariableInstruction(LocalVariableInstruction o){
		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.");
		}
	}
	
	/**
	 * Assures the generic preconditions of a LoadInstruction instance.
	 */
	public void visitLoadInstruction(LoadInstruction o){
		//visitLocalVariableInstruction(o) is called before, because it is more generic.

		// LOAD instructions must not read Type.UNKNOWN
		if (locals().get(o.getIndex()) == Type.UNKNOWN){
			constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content.");
		}

		// LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
		// as a symbol for the higher halve at index N+1
		// [suppose some instruction put an int at N+1--- our double at N is defective]
		if (o.getType(cpg).getSize() == 2){
			if (locals().get(o.getIndex()+1) != Type.UNKNOWN){
				constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed.");
			}
		}

		// LOAD instructions must read the correct type.
		if (!(o instanceof ALOAD)){
			if (locals().get(o.getIndex()) != o.getType(cpg) ){
				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
			}
		}
		else{ // we deal with an ALOAD
			if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
			}
			// ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
			//referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
		}

		// LOAD instructions must have enough free stack slots.
		if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
			constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
		}
	}

	/**
	 * Assures the generic preconditions of a StoreInstruction instance.
	 */
	public void visitStoreInstruction(StoreInstruction o){
		//visitLocalVariableInstruction(o) is called before, because it is more generic.

		if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking.
			constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
		}

		if ( (!(o instanceof ASTORE)) ){
			if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL.
				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'.");
			}
		}
		else{ // we deal with ASTORE
			Type stacktop = stack().peek();
			if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){
				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType.");
			}
			if (stacktop instanceof ReferenceType){
				referenceTypeIsInitialized(o, (ReferenceType) stacktop);
			}
		}
	}

	/**
	 * Assures the generic preconditions of a ReturnInstruction instance.
	 */
	public void visitReturnInstruction(ReturnInstruction o){
		if (o instanceof RETURN){
			return;
		}
		if (o instanceof ARETURN){
			if (stack().peek() == Type.NULL){
				return;
			}
			else{
				if (! (stack().peek() instanceof ReferenceType)){
					constraintViolated(o, "Reference type expected on top of stack, but is: '"+stack().peek()+"'.");
				}
				referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()));
				ReferenceType objectref = (ReferenceType) (stack().peek());
				// TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
				// "wider cast object type" created during verification.
				//if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ){
				//	constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+"' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
				//}
			}
		}
		else{
			Type method_type = mg.getType();
			if (method_type == Type.BOOLEAN ||
					method_type == Type.BYTE ||
					method_type == Type.SHORT ||
					method_type == Type.CHAR){
				method_type = Type.INT;
			}
			if (! ( method_type.equals( stack().peek() ))){
				constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'.");
			}
		}
	}

	/***************************************************************/
	/* "special"visitXXXX methods for one type of instruction each */
	/***************************************************************/

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitAALOAD(AALOAD o){
		Type arrayref = stack().peek(1);
		Type index    = stack().peek(0);
		
		indexOfInt(o, index);
		if (arrayrefOfArrayType(o, arrayref)){
			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
			}	
			referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitAASTORE(AASTORE o){
		Type arrayref = stack().peek(2);
		Type index    = stack().peek(1);
		Type value    = stack().peek(0);

		indexOfInt(o, index);
		if (!(value instanceof ReferenceType)){
			constraintViolated(o, "The 'value' is not of a ReferenceType but of type "+value+".");
		}else{
			referenceTypeIsInitialized(o, (ReferenceType) value);
		}
		// Don't bother further with "referenceTypeIsInitialized()", there are no arrays
		// of an uninitialized object type. 
		if (arrayrefOfArrayType(o, arrayref)){
			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
			}
			if (! ((ReferenceType)value).isAssignmentCompatibleWith((ReferenceType) ((ArrayType) arrayref).getElementType())){
				constraintViolated(o, "The type of 'value' ('"+value+"') is not assignment compatible to the components of the array 'arrayref' refers to. ('"+((ArrayType) arrayref).getElementType()+"')");
			}
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitACONST_NULL(ACONST_NULL o){
		// Nothing needs to be done here.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitALOAD(ALOAD o){
		//visitLoadInstruction(LoadInstruction) is called before.
		
		// Nothing else needs to be done here.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitANEWARRAY(ANEWARRAY o){
		if (!stack().peek().equals(Type.INT))
			constraintViolated(o, "The 'count' at the stack top is not of type '"+Type.INT+"' but of type '"+stack().peek()+"'.");
		// The runtime constant pool item at that index must be a symbolic reference to a class,
		// array, or interface type. See Pass 3a.
	}
	
	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitARETURN(ARETURN o){
		if (! (stack().peek() instanceof ReferenceType) ){
			constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
		}
		ReferenceType objectref = (ReferenceType) (stack().peek());
		referenceTypeIsInitialized(o, objectref);
		
		// The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
		// It cannot be done using Staerk-et-al's "set of object types" instead of a
		// "wider cast object type", anyway.
		//if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
		//	constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
		//}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitARRAYLENGTH(ARRAYLENGTH o){
		Type arrayref = stack().peek(0);
		arrayrefOfArrayType(o, arrayref);
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitASTORE(ASTORE o){
		if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
			constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
		}
		if (stack().peek() instanceof ReferenceType){
			referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitATHROW(ATHROW o){
		// It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
		// not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
		if (! ((stack().peek() instanceof ObjectType) || (stack().peek().equals(Type.NULL))) ){
			constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type "+stack().peek()+".");
		}
		
		// NULL is a subclass of every class, so to speak.
		if (stack().peek().equals(Type.NULL)) return;
				
		ObjectType exc = (ObjectType) (stack().peek());
		ObjectType throwable = (ObjectType) (Type.getType("Ljava/lang/Throwable;"));
		if ( (! (exc.subclassOf(throwable)) ) && (! (exc.equals(throwable))) ){
			constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '"+stack().peek()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitBALOAD(BALOAD o){
		Type arrayref = stack().peek(1);
		Type index    = stack().peek(0);
		indexOfInt(o, index);
		if (arrayrefOfArrayType(o, arrayref)){
			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
		 	       (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
			}
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitBASTORE(BASTORE o){
		Type arrayref = stack().peek(2);
		Type index    = stack().peek(1);
		Type value    = stack().peek(0);

		indexOfInt(o, index);
		valueOfInt(o, index);
		if (arrayrefOfArrayType(o, arrayref)){
			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
			        (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) )
					constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitBIPUSH(BIPUSH o){
		// Nothing to do...
	}

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

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitCALOAD(CALOAD o){
		Type arrayref = stack().peek(1);
		Type index = stack().peek(0);
		
		indexOfInt(o, index);
		arrayrefOfArrayType(o, arrayref);
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitCASTORE(CASTORE o){
		Type arrayref = stack().peek(2);
		Type index = stack().peek(1);
		Type value = stack().peek(0);
		
		indexOfInt(o, index);
		valueOfInt(o, index);
		if (arrayrefOfArrayType(o, arrayref)){
			if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
			}
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitCHECKCAST(CHECKCAST 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 (