instconstraintvisitor.java

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

		if (stack().peek(1) != Type.FLOAT){
			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitFCONST(FCONST o){
		// nothing to do here.
	}

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

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

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

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

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

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

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitFSTORE(FSTORE o){
		//visitStoreInstruction(StoreInstruction) is called before.
		
		// Nothing else needs to be done here.
	}

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

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitGETFIELD(GETFIELD o){
		Type objectref = stack().peek();
		if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
			constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '"+objectref+"'.");
		}
		
		String field_name = o.getFieldName(cpg);
		
		JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
		Field[] fields = jc.getFields();
		Field f = null;
		for (int i=0; i<fields.length; i++){
			if (fields[i].getName().equals(field_name)){
				f = fields[i];
				break;
			}
		}
		if (f == null){
			throw new AssertionViolatedException("Field not found?!?");
		}

		if (f.isProtected()){
			ObjectType classtype = o.getClassType(cpg);
			ObjectType curr = new ObjectType(mg.getClassName());

			if (	classtype.equals(curr) ||
						curr.subclassOf(classtype)	){
				Type t = stack().peek();
				if (t == Type.NULL){
					return;
				}
				if (! (t instanceof ObjectType) ){
					constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+t+"'.");
				}
				ObjectType objreftype = (ObjectType) t;
				if (! ( objreftype.equals(curr) ||
						    objreftype.subclassOf(curr) ) ){
					//TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
					//      created during the verification.
					//      "Wider" object types don't allow us to check for things like that below.
					//constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or a superclass of the current class. However, the referenced object type '"+stack().peek()+"' is not the current class or a subclass of the current class.");
				}
			} 
		}
		
		// TODO: Could go into Pass 3a.
		if (f.isStatic()){
			constraintViolated(o, "Referenced field '"+f+"' is static which it shouldn't be.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitGETSTATIC(GETSTATIC o){
		// Field must be static: see Pass 3a.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitGOTO(GOTO o){
		// nothing to do here.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitGOTO_W(GOTO_W o){
		// nothing to do here.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitI2B(I2B 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 visitI2C(I2C 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 visitI2D(I2D 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 visitI2F(I2F 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 visitI2L(I2L 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 visitI2S(I2S 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 visitIADD(IADD 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 visitIALOAD(IALOAD o){
		indexOfInt(o, stack().peek());
		if (stack().peek(1) == Type.NULL){
			return;
		} 
		if (! (stack().peek(1) instanceof ArrayType)){
			constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'.");
		}
		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
		if (t != Type.INT){
			constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIAND(IAND 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 visitIASTORE(IASTORE o){
		if (stack().peek() != Type.INT){
			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
		}
		indexOfInt(o, stack().peek(1));
		if (stack().peek(2) == Type.NULL){
			return;
		} 
		if (! (stack().peek(2) instanceof ArrayType)){
			constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'.");
		}
		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
		if (t != Type.INT){
			constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'.");
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitICONST(ICONST o){
		//nothing to do here.
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIDIV(IDIV 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_ACMPEQ(IF_ACMPEQ 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()) );
	
		if (!(stack().peek(1) instanceof ReferenceType)){
			constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'.");
		}
		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
		
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ACMPNE(IF_ACMPNE 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()) );
		}
		if (!(stack().peek(1) instanceof ReferenceType)){
			constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'.");
			referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
		}
	}

	/**
	 * Ensures the specific preconditions of the said instruction.
	 */
	public void visitIF_ICMPEQ(IF_ICMPEQ 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_ICMPGE(IF_ICMPGE 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)+"'.");
		}
	}