| Methods Summary |
|---|
| private void | _visitStackAccessor(com.sun.org.apache.bcel.internal.generic.Instruction o)/
/**
Ensures the general preconditions of an instruction that accesses the stack.
This method is here because BCEL has no such superinterface for the stack
accessing instructions; and there are funny unexpected exceptions in the
semantices of the superinterfaces and superclasses provided.
E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
Therefore, this method is called by all StackProducer, StackConsumer,
and StackInstruction instances via their visitXXX() method.
Unfortunately, as the superclasses and superinterfaces overlap, some instructions
cause this method to be called two or three times. [TODO: Fix this.]
int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
if (consume > stack().slotsUsed()){
constraintViolated((Instruction) o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
}
int produce = o.produceStack(cpg) - ((Instruction) o).consumeStack(cpg); // Stack values are always consumed first; then produced.
if ( produce + stack().slotsUsed() > stack().maxStack() ){
constraintViolated((Instruction) o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
}
|
| private boolean | arrayrefOfArrayType(com.sun.org.apache.bcel.internal.generic.Instruction o, com.sun.org.apache.bcel.internal.generic.Type arrayref)Assures arrayref is of ArrayType or NULL;
returns true if and only if arrayref is non-NULL.
if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) )
constraintViolated(o, "The 'arrayref' does not refer to an array but is of type "+arrayref+".");
return (arrayref instanceof ArrayType);
|
| private void | constraintViolated(com.sun.org.apache.bcel.internal.generic.Instruction violator, java.lang.String description)This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor
that a constraint violation has occured. This is done by throwing an instance of a
StructuralCodeConstraintException.
String fq_classname = violator.getClass().getName();
throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.")+1) +" constraint violated: " + description);
|
| private void | indexOfInt(com.sun.org.apache.bcel.internal.generic.Instruction o, com.sun.org.apache.bcel.internal.generic.Type index)Assures index is of type INT.
if (! index.equals(Type.INT))
constraintViolated(o, "The 'index' is not of type int but of type "+index+".");
|
| private LocalVariables | locals()The LocalVariables we're working on.
return frame.getLocals();
|
| private void | referenceTypeIsInitialized(com.sun.org.apache.bcel.internal.generic.Instruction o, com.sun.org.apache.bcel.internal.generic.ReferenceType r)Assures the ReferenceType r is initialized (or Type.NULL).
Formally, this means (!(r instanceof UninitializedObjectType)), because
there are no uninitialized array types.
if (r instanceof UninitializedObjectType){
constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
}
|
| public void | setConstantPoolGen(com.sun.org.apache.bcel.internal.generic.ConstantPoolGen cpg)Sets the ConstantPoolGen instance needed for constraint
checking prior to execution.
this.cpg = cpg;
|
| public void | setFrame(Frame f)This returns the single instance of the InstConstraintVisitor class.
To operate correctly, other values must have been set before actually
using the instance.
Use this method for performance reasons.
this.frame = f;
//if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
|
| public void | setMethodGen(com.sun.org.apache.bcel.internal.generic.MethodGen mg)Sets the MethodGen instance needed for constraint
checking prior to execution.
this.mg = mg;
|
| private OperandStack | stack()The OperandStack we're working on.
return frame.getStack();
|
| private void | valueOfInt(com.sun.org.apache.bcel.internal.generic.Instruction o, com.sun.org.apache.bcel.internal.generic.Type value)Assures value is of type INT.
if (! value.equals(Type.INT))
constraintViolated(o, "The 'value' is not of type int but of type "+value+".");
|
| public void | visitAALOAD(com.sun.org.apache.bcel.internal.generic.AALOAD o)/
/**
Ensures the specific preconditions of the said instruction.
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()));
}
|
| public void | visitAASTORE(com.sun.org.apache.bcel.internal.generic.AASTORE o)Ensures the specific preconditions of the said instruction.
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()+"')");
}
}
|
| public void | visitACONST_NULL(com.sun.org.apache.bcel.internal.generic.ACONST_NULL o)Ensures the specific preconditions of the said instruction.
// Nothing needs to be done here.
|
| public void | visitALOAD(com.sun.org.apache.bcel.internal.generic.ALOAD o)Ensures the specific preconditions of the said instruction.
//visitLoadInstruction(LoadInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitANEWARRAY(com.sun.org.apache.bcel.internal.generic.ANEWARRAY o)Ensures the specific preconditions of the said instruction.
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.
|
| public void | visitARETURN(com.sun.org.apache.bcel.internal.generic.ARETURN o)Ensures the specific preconditions of the said instruction.
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.");
//}
|
| public void | visitARRAYLENGTH(com.sun.org.apache.bcel.internal.generic.ARRAYLENGTH o)Ensures the specific preconditions of the said instruction.
Type arrayref = stack().peek(0);
arrayrefOfArrayType(o, arrayref);
|
| public void | visitASTORE(com.sun.org.apache.bcel.internal.generic.ASTORE o)Ensures the specific preconditions of the said instruction.
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()) );
}
|
| public void | visitATHROW(com.sun.org.apache.bcel.internal.generic.ATHROW o)Ensures the specific preconditions of the said instruction.
// 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()+"'.");
}
|
| public void | visitBALOAD(com.sun.org.apache.bcel.internal.generic.BALOAD o)Ensures the specific preconditions of the said instruction.
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()+"'.");
}
}
|
| public void | visitBASTORE(com.sun.org.apache.bcel.internal.generic.BASTORE o)Ensures the specific preconditions of the said instruction.
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()+"'.");
}
|
| public void | visitBIPUSH(com.sun.org.apache.bcel.internal.generic.BIPUSH o)Ensures the specific preconditions of the said instruction.
// Nothing to do...
|
| public void | visitBREAKPOINT(com.sun.org.apache.bcel.internal.generic.BREAKPOINT o)Ensures the specific preconditions of the said instruction.
throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
|
| public void | visitCALOAD(com.sun.org.apache.bcel.internal.generic.CALOAD o)Ensures the specific preconditions of the said instruction.
Type arrayref = stack().peek(1);
Type index = stack().peek(0);
indexOfInt(o, index);
arrayrefOfArrayType(o, arrayref);
|
| public void | visitCASTORE(com.sun.org.apache.bcel.internal.generic.CASTORE o)Ensures the specific preconditions of the said instruction.
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()+".");
}
}
|
| public void | visitCHECKCAST(com.sun.org.apache.bcel.internal.generic.CHECKCAST o)Ensures the specific preconditions of the said instruction.
// 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 (÷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+"'.");
}
|
| public void | visitCPInstruction(com.sun.org.apache.bcel.internal.generic.CPInstruction o)/
/**
Ensures the general preconditions of a CPInstruction instance.
int idx = o.getIndex();
if ((idx < 0) || (idx >= cpg.getSize())){
throw new AssertionViolatedException("Huh?! Constant pool index of instruction '"+o+"' illegal? Pass 3a should have checked this!");
}
|
| public void | visitD2F(com.sun.org.apache.bcel.internal.generic.D2F o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
|
| public void | visitD2I(com.sun.org.apache.bcel.internal.generic.D2I o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
|
| public void | visitD2L(com.sun.org.apache.bcel.internal.generic.D2L o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
|
| public void | visitDADD(com.sun.org.apache.bcel.internal.generic.DADD o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDALOAD(com.sun.org.apache.bcel.internal.generic.DALOAD o)Ensures the specific preconditions of the said instruction.
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 double[] but is '"+stack().peek(1)+"'.");
}
Type t = ((ArrayType) (stack().peek(1))).getBasicType();
if (t != Type.DOUBLE){
constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
}
|
| public void | visitDASTORE(com.sun.org.apache.bcel.internal.generic.DASTORE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', 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 double[] but is '"+stack().peek(2)+"'.");
}
Type t = ((ArrayType) (stack().peek(2))).getBasicType();
if (t != Type.DOUBLE){
constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
}
|
| public void | visitDCMPG(com.sun.org.apache.bcel.internal.generic.DCMPG o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDCMPL(com.sun.org.apache.bcel.internal.generic.DCMPL o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDCONST(com.sun.org.apache.bcel.internal.generic.DCONST o)Ensures the specific preconditions of the said instruction.
// There's nothing to be done here.
|
| public void | visitDDIV(com.sun.org.apache.bcel.internal.generic.DDIV o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDLOAD(com.sun.org.apache.bcel.internal.generic.DLOAD o)Ensures the specific preconditions of the said instruction.
//visitLoadInstruction(LoadInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitDMUL(com.sun.org.apache.bcel.internal.generic.DMUL o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDNEG(com.sun.org.apache.bcel.internal.generic.DNEG o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
|
| public void | visitDREM(com.sun.org.apache.bcel.internal.generic.DREM o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDRETURN(com.sun.org.apache.bcel.internal.generic.DRETURN o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
|
| public void | visitDSTORE(com.sun.org.apache.bcel.internal.generic.DSTORE o)Ensures the specific preconditions of the said instruction.
//visitStoreInstruction(StoreInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitDSUB(com.sun.org.apache.bcel.internal.generic.DSUB o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.DOUBLE){
constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.DOUBLE){
constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitDUP(com.sun.org.apache.bcel.internal.generic.DUP o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 1){
constraintViolated(o, "Won't DUP type on stack top '"+stack().peek()+"' because it must occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
}
|
| public void | visitDUP2(com.sun.org.apache.bcel.internal.generic.DUP2 o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() == 2){
return; // Form 2, okay.
}
else{ //stack().peek().getSize() == 1.
if (stack().peek(1).getSize() != 1){
constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
}
}
|
| public void | visitDUP2_X1(com.sun.org.apache.bcel.internal.generic.DUP2_X1 o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() == 2){
if (stack().peek(1).getSize() != 1){
constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
}
else{
return; // Form 2
}
}
else{ // stack top is of size 1
if ( stack().peek(1).getSize() != 1 ){
constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
}
if ( stack().peek(2).getSize() != 1 ){
constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
}
}
|
| public void | visitDUP2_X2(com.sun.org.apache.bcel.internal.generic.DUP2_X2 o)Ensures the specific preconditions of the said instruction.
if (stack().peek(0).getSize() == 2){
if (stack().peek(1).getSize() == 2){
return; // Form 4
}
else{// stack top size is 2, next-to-top's size is 1
if ( stack().peek(2).getSize() != 1 ){
constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
}
else{
return; // Form 2
}
}
}
else{// stack top is of size 1
if (stack().peek(1).getSize() == 1){
if ( stack().peek(2).getSize() == 2 ){
return; // Form 3
}
else{
if ( stack().peek(3).getSize() == 1){
return; // Form 1
}
}
}
}
constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
|
| public void | visitDUP_X1(com.sun.org.apache.bcel.internal.generic.DUP_X1 o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 1){
constraintViolated(o, "Type on stack top '"+stack().peek()+"' should occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
}
if (stack().peek(1).getSize() != 1){
constraintViolated(o, "Type on stack next-to-top '"+stack().peek(1)+"' should occupy exactly one slot, not '"+stack().peek(1).getSize()+"'.");
}
|
| public void | visitDUP_X2(com.sun.org.apache.bcel.internal.generic.DUP_X2 o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 1){
constraintViolated(o, "Stack top type must be of size 1, but is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
}
if (stack().peek(1).getSize() == 2){
return; // Form 2, okay.
}
else{ //stack().peek(1).getSize == 1.
if (stack().peek(2).getSize() != 1){
constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1, stack next-to-next-to-top's size must also be 1, but is: '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
}
}
|
| public void | visitF2D(com.sun.org.apache.bcel.internal.generic.F2D o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
}
|
| public void | visitF2I(com.sun.org.apache.bcel.internal.generic.F2I o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
}
|
| public void | visitF2L(com.sun.org.apache.bcel.internal.generic.F2L o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
}
|
| public void | visitFADD(com.sun.org.apache.bcel.internal.generic.FADD o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFALOAD(com.sun.org.apache.bcel.internal.generic.FALOAD o)Ensures the specific preconditions of the said instruction.
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 float[] but is '"+stack().peek(1)+"'.");
}
Type t = ((ArrayType) (stack().peek(1))).getBasicType();
if (t != Type.FLOAT){
constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
}
|
| public void | visitFASTORE(com.sun.org.apache.bcel.internal.generic.FASTORE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', 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 float[] but is '"+stack().peek(2)+"'.");
}
Type t = ((ArrayType) (stack().peek(2))).getBasicType();
if (t != Type.FLOAT){
constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
}
|
| public void | visitFCMPG(com.sun.org.apache.bcel.internal.generic.FCMPG o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFCMPL(com.sun.org.apache.bcel.internal.generic.FCMPL o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFCONST(com.sun.org.apache.bcel.internal.generic.FCONST o)Ensures the specific preconditions of the said instruction.
// nothing to do here.
|
| public void | visitFDIV(com.sun.org.apache.bcel.internal.generic.FDIV o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFLOAD(com.sun.org.apache.bcel.internal.generic.FLOAD o)Ensures the specific preconditions of the said instruction.
//visitLoadInstruction(LoadInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitFMUL(com.sun.org.apache.bcel.internal.generic.FMUL o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFNEG(com.sun.org.apache.bcel.internal.generic.FNEG o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
}
|
| public void | visitFREM(com.sun.org.apache.bcel.internal.generic.FREM o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFRETURN(com.sun.org.apache.bcel.internal.generic.FRETURN o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.FLOAT){
constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
}
|
| public void | visitFSTORE(com.sun.org.apache.bcel.internal.generic.FSTORE o)Ensures the specific preconditions of the said instruction.
//visitStoreInstruction(StoreInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitFSUB(com.sun.org.apache.bcel.internal.generic.FSUB o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitFieldInstruction(com.sun.org.apache.bcel.internal.generic.FieldInstruction o)Ensures the general preconditions of a FieldInstruction instance.
// visitLoadClass(o) has been called before: Every FieldOrMethod
// implements LoadClass.
// visitCPInstruction(o) has been called before.
// A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC
Constant c = cpg.getConstant(o.getIndex());
if (!(c instanceof ConstantFieldref)){
constraintViolated(o, "Index '"+o.getIndex()+"' should refer to a CONSTANT_Fieldref_info structure, but refers to '"+c+"'.");
}
// 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+"'.");
}
}
|
| public void | visitGETFIELD(com.sun.org.apache.bcel.internal.generic.GETFIELD o)Ensures the specific preconditions of the said instruction.
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.");
}
|
| public void | visitGETSTATIC(com.sun.org.apache.bcel.internal.generic.GETSTATIC o)Ensures the specific preconditions of the said instruction.
// Field must be static: see Pass 3a.
|
| public void | visitGOTO(com.sun.org.apache.bcel.internal.generic.GOTO o)Ensures the specific preconditions of the said instruction.
// nothing to do here.
|
| public void | visitGOTO_W(com.sun.org.apache.bcel.internal.generic.GOTO_W o)Ensures the specific preconditions of the said instruction.
// nothing to do here.
|
| public void | visitI2B(com.sun.org.apache.bcel.internal.generic.I2B o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitI2C(com.sun.org.apache.bcel.internal.generic.I2C o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitI2D(com.sun.org.apache.bcel.internal.generic.I2D o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitI2F(com.sun.org.apache.bcel.internal.generic.I2F o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitI2L(com.sun.org.apache.bcel.internal.generic.I2L o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitI2S(com.sun.org.apache.bcel.internal.generic.I2S o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIADD(com.sun.org.apache.bcel.internal.generic.IADD o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIALOAD(com.sun.org.apache.bcel.internal.generic.IALOAD o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIAND(com.sun.org.apache.bcel.internal.generic.IAND o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIASTORE(com.sun.org.apache.bcel.internal.generic.IASTORE o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitICONST(com.sun.org.apache.bcel.internal.generic.ICONST o)Ensures the specific preconditions of the said instruction.
//nothing to do here.
|
| public void | visitIDIV(com.sun.org.apache.bcel.internal.generic.IDIV o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIFEQ(com.sun.org.apache.bcel.internal.generic.IFEQ o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFGE(com.sun.org.apache.bcel.internal.generic.IFGE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFGT(com.sun.org.apache.bcel.internal.generic.IFGT o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFLE(com.sun.org.apache.bcel.internal.generic.IFLE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFLT(com.sun.org.apache.bcel.internal.generic.IFLT o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFNE(com.sun.org.apache.bcel.internal.generic.IFNE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitIFNONNULL(com.sun.org.apache.bcel.internal.generic.IFNONNULL o)Ensures the specific preconditions of the said instruction.
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()) );
|
| public void | visitIFNULL(com.sun.org.apache.bcel.internal.generic.IFNULL o)Ensures the specific preconditions of the said instruction.
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()) );
|
| public void | visitIF_ACMPEQ(com.sun.org.apache.bcel.internal.generic.IF_ACMPEQ o)Ensures the specific preconditions of the said instruction.
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)) );
|
| public void | visitIF_ACMPNE(com.sun.org.apache.bcel.internal.generic.IF_ACMPNE o)Ensures the specific preconditions of the said instruction.
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)) );
}
|
| public void | visitIF_ICMPEQ(com.sun.org.apache.bcel.internal.generic.IF_ICMPEQ o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIF_ICMPGE(com.sun.org.apache.bcel.internal.generic.IF_ICMPGE o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIF_ICMPGT(com.sun.org.apache.bcel.internal.generic.IF_ICMPGT o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIF_ICMPLE(com.sun.org.apache.bcel.internal.generic.IF_ICMPLE o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIF_ICMPLT(com.sun.org.apache.bcel.internal.generic.IF_ICMPLT o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIF_ICMPNE(com.sun.org.apache.bcel.internal.generic.IF_ICMPNE o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIINC(com.sun.org.apache.bcel.internal.generic.IINC o)Ensures the specific preconditions of the said instruction.
// 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()));
|
| public void | visitILOAD(com.sun.org.apache.bcel.internal.generic.ILOAD o)Ensures the specific preconditions of the said instruction.
// All done by visitLocalVariableInstruction(), visitLoadInstruction()
|
| public void | visitIMPDEP1(com.sun.org.apache.bcel.internal.generic.IMPDEP1 o)Ensures the specific preconditions of the said instruction.
throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
|
| public void | visitIMPDEP2(com.sun.org.apache.bcel.internal.generic.IMPDEP2 o)Ensures the specific preconditions of the said instruction.
throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
|
| public void | visitIMUL(com.sun.org.apache.bcel.internal.generic.IMUL o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitINEG(com.sun.org.apache.bcel.internal.generic.INEG o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitINSTANCEOF(com.sun.org.apache.bcel.internal.generic.INSTANCEOF o)Ensures the specific preconditions of the said instruction.
// 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 (÷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+"'.");
}
|
| public void | visitINVOKEINTERFACE(com.sun.org.apache.bcel.internal.generic.INVOKEINTERFACE o)Ensures the specific preconditions of the said instruction.
// 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+"'.");
}
|
| public void | visitINVOKESPECIAL(com.sun.org.apache.bcel.internal.generic.INVOKESPECIAL o)Ensures the specific preconditions of the said instruction.
// 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_classname = ((ObjectType) objref).getClassName();
}
else{
if (!(objref instanceof UninitializedObjectType)){
constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '"+objref+"'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address).");
}
objref_classname = ((UninitializedObjectType) objref).getInitialized().getClassName();
}
String theClass = o.getClassName(cpg);
if ( ! Repository.instanceOf(objref_classname, theClass) ){
constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected.");
}
|
| public void | visitINVOKESTATIC(com.sun.org.apache.bcel.internal.generic.INVOKESTATIC o)Ensures the specific preconditions of the said instruction.
// Method is not native, otherwise pass 3 would not happen.
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 check can only be done 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.");
}
}
}
|
| public void | visitINVOKEVIRTUAL(com.sun.org.apache.bcel.internal.generic.INVOKEVIRTUAL o)Ensures the specific preconditions of the said instruction.
// 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 single "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 theClass = o.getClassName(cpg);
if ( ! Repository.instanceOf(objref_classname, theClass) ){
constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected.");
}
|
| public void | visitIOR(com.sun.org.apache.bcel.internal.generic.IOR o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIREM(com.sun.org.apache.bcel.internal.generic.IREM o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIRETURN(com.sun.org.apache.bcel.internal.generic.IRETURN o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitISHL(com.sun.org.apache.bcel.internal.generic.ISHL o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitISHR(com.sun.org.apache.bcel.internal.generic.ISHR o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitISTORE(com.sun.org.apache.bcel.internal.generic.ISTORE o)Ensures the specific preconditions of the said instruction.
//visitStoreInstruction(StoreInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitISUB(com.sun.org.apache.bcel.internal.generic.ISUB o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIUSHR(com.sun.org.apache.bcel.internal.generic.IUSHR o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitIXOR(com.sun.org.apache.bcel.internal.generic.IXOR o)Ensures the specific preconditions of the said instruction.
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)+"'.");
}
|
| public void | visitInvokeInstruction(com.sun.org.apache.bcel.internal.generic.InvokeInstruction o)Ensures the general preconditions of an InvokeInstruction instance.
// visitLoadClass(o) has been called before: Every FieldOrMethod
// implements LoadClass.
// visitCPInstruction(o) has been called before.
//TODO
|
| public void | visitJSR(com.sun.org.apache.bcel.internal.generic.JSR o)Ensures the specific preconditions of the said instruction.
// nothing to do here.
|
| public void | visitJSR_W(com.sun.org.apache.bcel.internal.generic.JSR_W o)Ensures the specific preconditions of the said instruction.
// nothing to do here.
|
| public void | visitL2D(com.sun.org.apache.bcel.internal.generic.L2D o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
|
| public void | visitL2F(com.sun.org.apache.bcel.internal.generic.L2F o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
|
| public void | visitL2I(com.sun.org.apache.bcel.internal.generic.L2I o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
|
| public void | visitLADD(com.sun.org.apache.bcel.internal.generic.LADD o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLALOAD(com.sun.org.apache.bcel.internal.generic.LALOAD o)Ensures the specific preconditions of the said instruction.
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 long[] but is '"+stack().peek(1)+"'.");
}
Type t = ((ArrayType) (stack().peek(1))).getBasicType();
if (t != Type.LONG){
constraintViolated(o, "Stack next-to-top must be of type long[] but is '"+stack().peek(1)+"'.");
}
|
| public void | visitLAND(com.sun.org.apache.bcel.internal.generic.LAND o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLASTORE(com.sun.org.apache.bcel.internal.generic.LASTORE o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', 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 long[] but is '"+stack().peek(2)+"'.");
}
Type t = ((ArrayType) (stack().peek(2))).getBasicType();
if (t != Type.LONG){
constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '"+stack().peek(2)+"'.");
}
|
| public void | visitLCMP(com.sun.org.apache.bcel.internal.generic.LCMP o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLCONST(com.sun.org.apache.bcel.internal.generic.LCONST o)Ensures the specific preconditions of the said instruction.
// Nothing to do here.
|
| public void | visitLDC(com.sun.org.apache.bcel.internal.generic.LDC o)Ensures the specific preconditions of the said instruction.
// visitCPInstruction is called first.
Constant c = cpg.getConstant(o.getIndex());
if (! ( ( c instanceof ConstantInteger) ||
( c instanceof ConstantFloat ) ||
( c instanceof ConstantString ) ) ){
constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
}
|
| public void | visitLDC2_W(com.sun.org.apache.bcel.internal.generic.LDC2_W o)Ensures the specific preconditions of the said instruction.
// visitCPInstruction is called first.
Constant c = cpg.getConstant(o.getIndex());
if (! ( ( c instanceof ConstantLong) ||
( c instanceof ConstantDouble ) ) ){
constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
}
|
| public void | visitLDC_W(com.sun.org.apache.bcel.internal.generic.LDC_W o)Ensures the specific preconditions of the said instruction.
// visitCPInstruction is called first.
Constant c = cpg.getConstant(o.getIndex());
if (! ( ( c instanceof ConstantInteger) ||
( c instanceof ConstantFloat ) ||
( c instanceof ConstantString ) ) ){
constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
}
|
| public void | visitLDIV(com.sun.org.apache.bcel.internal.generic.LDIV o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLLOAD(com.sun.org.apache.bcel.internal.generic.LLOAD o)Ensures the specific preconditions of the said instruction.
//visitLoadInstruction(LoadInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitLMUL(com.sun.org.apache.bcel.internal.generic.LMUL o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLNEG(com.sun.org.apache.bcel.internal.generic.LNEG o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
|
| public void | visitLOOKUPSWITCH(com.sun.org.apache.bcel.internal.generic.LOOKUPSWITCH o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
// See also pass 3a.
|
| public void | visitLOR(com.sun.org.apache.bcel.internal.generic.LOR o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLREM(com.sun.org.apache.bcel.internal.generic.LREM o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLRETURN(com.sun.org.apache.bcel.internal.generic.LRETURN o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
|
| public void | visitLSHL(com.sun.org.apache.bcel.internal.generic.LSHL o)Ensures the specific preconditions of the said instruction.
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.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLSHR(com.sun.org.apache.bcel.internal.generic.LSHR o)Ensures the specific preconditions of the said instruction.
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.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLSTORE(com.sun.org.apache.bcel.internal.generic.LSTORE o)Ensures the specific preconditions of the said instruction.
//visitStoreInstruction(StoreInstruction) is called before.
// Nothing else needs to be done here.
|
| public void | visitLSUB(com.sun.org.apache.bcel.internal.generic.LSUB o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLUSHR(com.sun.org.apache.bcel.internal.generic.LUSHR o)Ensures the specific preconditions of the said instruction.
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.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLXOR(com.sun.org.apache.bcel.internal.generic.LXOR o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.LONG){
constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
}
if (stack().peek(1) != Type.LONG){
constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
}
|
| public void | visitLoadClass(com.sun.org.apache.bcel.internal.generic.LoadClass o)/
/**
Assures the generic preconditions of a LoadClass instance.
The referenced class is loaded and pass2-verified.
ObjectType t = o.getLoadClassType(cpg);
if (t != null){// null means "no class is loaded"
Verifier v = VerifierFactory.getVerifier(t.getClassName());
VerificationResult vr = v.doPass2();
if (vr.getStatus() != VerificationResult.VERIFIED_OK){
constraintViolated((Instruction) o, "Class '"+o.getLoadClassType(cpg).getClassName()+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
}
}
|
| public void | visitLoadInstruction(com.sun.org.apache.bcel.internal.generic.LoadInstruction o)Assures the generic preconditions of a LoadInstruction instance.
//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.");
}
|
| public void | visitLocalVariableInstruction(com.sun.org.apache.bcel.internal.generic.LocalVariableInstruction o)Assures the generic preconditions of a LocalVariableInstruction instance.
That is, the index of the local variable must be valid.
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.");
}
|
| public void | visitMONITORENTER(com.sun.org.apache.bcel.internal.generic.MONITORENTER o)Ensures the specific preconditions of the said instruction.
if (! ((stack().peek()) instanceof ReferenceType)){
constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'.");
}
referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
|
| public void | visitMONITOREXIT(com.sun.org.apache.bcel.internal.generic.MONITOREXIT o)Ensures the specific preconditions of the said instruction.
if (! ((stack().peek()) instanceof ReferenceType)){
constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'.");
}
referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
|
| public void | visitMULTIANEWARRAY(com.sun.org.apache.bcel.internal.generic.MULTIANEWARRAY o)Ensures the specific preconditions of the said instruction.
int dimensions = o.getDimensions();
// Dimensions argument is okay: see Pass 3a.
for (int i=0; i<dimensions; i++){
if (stack().peek(i) != Type.INT){
constraintViolated(o, "The '"+dimensions+"' upper stack types should be 'int' but aren't.");
}
}
// The runtime constant pool item at that index must be a symbolic reference to a class,
// array, or interface type. See Pass 3a.
|
| public void | visitNEW(com.sun.org.apache.bcel.internal.generic.NEW o)Ensures the specific preconditions of the said instruction.
//visitCPInstruction(CPInstruction) has been called before.
//visitLoadClass(LoadClass) has been called before.
Type t = o.getType(cpg);
if (! (t instanceof ReferenceType)){
throw new AssertionViolatedException("NEW.getType() returning a non-reference type?!");
}
if (! (t instanceof ObjectType)){
constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+t+"'.");
}
ObjectType obj = (ObjectType) t;
//e.g.: Don't instantiate interfaces
if (! obj.referencesClass()){
constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+obj+"'.");
}
|
| public void | visitNEWARRAY(com.sun.org.apache.bcel.internal.generic.NEWARRAY o)Ensures the specific preconditions of the said instruction.
if (stack().peek() != Type.INT){
constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
}
|
| public void | visitNOP(com.sun.org.apache.bcel.internal.generic.NOP o)Ensures the specific preconditions of the said instruction.
// nothing is to be done here.
|
| public void | visitPOP(com.sun.org.apache.bcel.internal.generic.POP o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 1){
constraintViolated(o, "Stack top size should be 1 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
}
|
| public void | visitPOP2(com.sun.org.apache.bcel.internal.generic.POP2 o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 2){
constraintViolated(o, "Stack top size should be 2 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
}
|
| public void | visitPUTFIELD(com.sun.org.apache.bcel.internal.generic.PUTFIELD o)Ensures the specific preconditions of the said instruction.
Type objectref = stack().peek(1);
if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
constraintViolated(o, "Stack next-to-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?!?");
}
Type value = stack().peek();
Type t = Type.getType(f.getSignature());
Type shouldbe = t;
if (shouldbe == Type.BOOLEAN ||
shouldbe == Type.BYTE ||
shouldbe == Type.CHAR ||
shouldbe == Type.SHORT){
shouldbe = Type.INT;
}
if (t instanceof ReferenceType){
ReferenceType rvalue = null;
if (value instanceof ReferenceType){
rvalue = (ReferenceType) value;
referenceTypeIsInitialized(o, rvalue);
}
else{
constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected.");
}
// TODO: This can only be checked using Staerk-et-al's "set-of-object types", not
// using "wider cast object types" created during verification.
//if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){
// constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'.");
//}
}
else{
if (shouldbe != value){
constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected.");
}
}
if (f.isProtected()){
ObjectType classtype = o.getClassType(cpg);
ObjectType curr = new ObjectType(mg.getClassName());
if ( classtype.equals(curr) ||
curr.subclassOf(classtype) ){
Type tp = stack().peek(1);
if (tp == Type.NULL){
return;
}
if (! (tp instanceof ObjectType) ){
constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+tp+"'.");
}
ObjectType objreftype = (ObjectType) tp;
if (! ( objreftype.equals(curr) ||
objreftype.subclassOf(curr) ) ){
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.");
}
|
| public void | visitPUTSTATIC(com.sun.org.apache.bcel.internal.generic.PUTSTATIC o)Ensures the specific preconditions of the said instruction.
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?!?");
}
Type value = stack().peek();
Type t = Type.getType(f.getSignature());
Type shouldbe = t;
if (shouldbe == Type.BOOLEAN ||
shouldbe == Type.BYTE ||
shouldbe == Type.CHAR ||
shouldbe == Type.SHORT){
shouldbe = Type.INT;
}
if (t instanceof ReferenceType){
ReferenceType rvalue = null;
if (value instanceof ReferenceType){
rvalue = (ReferenceType) value;
referenceTypeIsInitialized(o, rvalue);
}
else{
constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected.");
}
if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){
constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'.");
}
}
else{
if (shouldbe != value){
constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected.");
}
}
// TODO: Interface fields may be assigned to only once. (Hard to implement in
// JustIce's execution model). This may only happen in <clinit>, see Pass 3a.
|
| public void | visitRET(com.sun.org.apache.bcel.internal.generic.RET o)Ensures the specific preconditions of the said instruction.
if (! (locals().get(o.getIndex()) instanceof ReturnaddressType)){
constraintViolated(o, "Expecting a ReturnaddressType in local variable "+o.getIndex()+".");
}
if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET){
throw new AssertionViolatedException("Oops: RET expecting a target!");
}
// Other constraints such as non-allowed overlapping subroutines are enforced
// while building the Subroutines data structure.
|
| public void | visitRETURN(com.sun.org.apache.bcel.internal.generic.RETURN o)Ensures the specific preconditions of the said instruction.
if (mg.getName().equals(Constants.CONSTRUCTOR_NAME)){// If we leave an <init> method
if ((frame._this != null) && (!(mg.getClassName().equals(Type.OBJECT.getClassName()))) ) {
constraintViolated(o, "Leaving a constructor that itself did not call a constructor.");
}
}
|
| public void | visitReturnInstruction(com.sun.org.apache.bcel.internal.generic.ReturnInstruction o)Assures the generic preconditions of a ReturnInstruction instance.
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()+"'.");
}
}
|
| public void | visitSALOAD(com.sun.org.apache.bcel.internal.generic.SALOAD o)Ensures the specific preconditions of the said instruction.
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 short[] but is '"+stack().peek(1)+"'.");
}
Type t = ((ArrayType) (stack().peek(1))).getBasicType();
if (t != Type.SHORT){
constraintViolated(o, "Stack next-to-top must be of type short[] but is '"+stack().peek(1)+"'.");
}
|
| public void | visitSASTORE(com.sun.org.apache.bcel.internal.generic.SASTORE o)Ensures the specific preconditions of the said instruction.
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 short[] but is '"+stack().peek(2)+"'.");
}
Type t = ((ArrayType) (stack().peek(2))).getBasicType();
if (t != Type.SHORT){
constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '"+stack().peek(2)+"'.");
}
|
| public void | visitSIPUSH(com.sun.org.apache.bcel.internal.generic.SIPUSH o)Ensures the specific preconditions of the said instruction.
// nothing to do here. Generic visitXXX() methods did the trick before.
|
| public void | visitSWAP(com.sun.org.apache.bcel.internal.generic.SWAP o)Ensures the specific preconditions of the said instruction.
if (stack().peek().getSize() != 1){
constraintViolated(o, "The value at the stack top is not of size '1', but of size '"+stack().peek().getSize()+"'.");
}
if (stack().peek(1).getSize() != 1){
constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '"+stack().peek(1).getSize()+"'.");
}
|
| public void | visitStackConsumer(com.sun.org.apache.bcel.internal.generic.StackConsumer o)Ensures the general preconditions of a StackConsumer instance.
_visitStackAccessor((Instruction) o);
|
| public void | visitStackInstruction(com.sun.org.apache.bcel.internal.generic.StackInstruction o)Ensures the general preconditions of a StackInstruction instance.
_visitStackAccessor(o);
|
| public void | visitStackProducer(com.sun.org.apache.bcel.internal.generic.StackProducer o)Ensures the general preconditions of a StackProducer instance.
_visitStackAccessor((Instruction) o);
|
| public void | visitStoreInstruction(com.sun.org.apache.bcel.internal.generic.StoreInstruction o)Assures the generic preconditions of a StoreInstruction instance.
//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);
}
}
|
| public void | visitTABLESWITCH(com.sun.org.apache.bcel.internal.generic.TABLESWITCH o)Ensures the specific preconditions of the said instruction.
indexOfInt(o, stack().peek());
// See Pass 3a.
|
