You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@commons.apache.org by se...@apache.org on 2014/05/31 00:51:30 UTC
svn commit: r1598766 [9/12] - in /commons/proper/bcel/trunk/src:
main/java/org/apache/bcel/ main/java/org/apache/bcel/classfile/
main/java/org/apache/bcel/generic/ main/java/org/apache/bcel/util/
main/java/org/apache/bcel/verifier/exc/ main/java/org/ap...
Modified: commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java
URL: http://svn.apache.org/viewvc/commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java?rev=1598766&r1=1598765&r2=1598766&view=diff
==============================================================================
--- commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java (original)
+++ commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java Fri May 30 22:51:27 2014
@@ -53,1206 +53,1206 @@ import org.apache.bcel.verifier.exc.Stru
*/
public class InstConstraintVisitor extends EmptyVisitor{
- private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance("org.apache.bcel.verifier.structurals.GenericArray");
+ private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance("org.apache.bcel.verifier.structurals.GenericArray");
- /**
- * The constructor. Constructs a new instance of this class.
- */
- public InstConstraintVisitor(){}
-
- /**
- * The Execution Frame we're working on.
- *
- * @see #setFrame(Frame f)
- * @see #locals()
- * @see #stack()
- */
- private Frame frame = null;
-
- /**
- * The ConstantPoolGen we're working on.
- *
- * @see #setConstantPoolGen(ConstantPoolGen cpg)
- */
- private ConstantPoolGen cpg = null;
-
- /**
- * The MethodGen we're working on.
- *
- * @see #setMethodGen(MethodGen mg)
- */
- private MethodGen mg = null;
-
- /**
- * The OperandStack we're working on.
- *
- * @see #setFrame(Frame f)
- */
- private OperandStack stack(){
- return frame.getStack();
- }
-
- /**
- * The LocalVariables we're working on.
- *
- * @see #setFrame(Frame f)
- */
- private LocalVariables locals(){
- return frame.getLocals();
- }
+ /**
+ * The constructor. Constructs a new instance of this class.
+ */
+ public InstConstraintVisitor(){}
+
+ /**
+ * The Execution Frame we're working on.
+ *
+ * @see #setFrame(Frame f)
+ * @see #locals()
+ * @see #stack()
+ */
+ private Frame frame = null;
+
+ /**
+ * The ConstantPoolGen we're working on.
+ *
+ * @see #setConstantPoolGen(ConstantPoolGen cpg)
+ */
+ private ConstantPoolGen cpg = null;
+
+ /**
+ * The MethodGen we're working on.
+ *
+ * @see #setMethodGen(MethodGen mg)
+ */
+ private MethodGen mg = null;
+
+ /**
+ * The OperandStack we're working on.
+ *
+ * @see #setFrame(Frame f)
+ */
+ private OperandStack stack(){
+ return frame.getStack();
+ }
+
+ /**
+ * The LocalVariables we're working on.
+ *
+ * @see #setFrame(Frame f)
+ */
+ private LocalVariables locals(){
+ return frame.getLocals();
+ }
- /**
+ /**
* 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.
* @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException always.
*/
- private void constraintViolated(Instruction violator, String description){
- String fq_classname = violator.getClass().getName();
- throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description);
- }
-
- /**
- * 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.
- *
- * @see #setConstantPoolGen(ConstantPoolGen cpg)
- * @see #setMethodGen(MethodGen mg)
- */
- public void setFrame(Frame f){
- this.frame = f;
- //if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
- }
-
- /**
- * Sets the ConstantPoolGen instance needed for constraint
- * checking prior to execution.
- */
- public void setConstantPoolGen(ConstantPoolGen cpg){
- this.cpg = cpg;
- }
-
- /**
- * Sets the MethodGen instance needed for constraint
- * checking prior to execution.
- */
- public void setMethodGen(MethodGen mg){
- this.mg = mg;
- }
-
- /**
- * Assures index is of type INT.
- * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
- */
- private void indexOfInt(Instruction o, Type index){
- if (! index.equals(Type.INT)) {
+ private void constraintViolated(Instruction violator, String description){
+ String fq_classname = violator.getClass().getName();
+ throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description);
+ }
+
+ /**
+ * 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.
+ *
+ * @see #setConstantPoolGen(ConstantPoolGen cpg)
+ * @see #setMethodGen(MethodGen mg)
+ */
+ public void setFrame(Frame f){
+ this.frame = f;
+ //if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
+ }
+
+ /**
+ * Sets the ConstantPoolGen instance needed for constraint
+ * checking prior to execution.
+ */
+ public void setConstantPoolGen(ConstantPoolGen cpg){
+ this.cpg = cpg;
+ }
+
+ /**
+ * Sets the MethodGen instance needed for constraint
+ * checking prior to execution.
+ */
+ public void setMethodGen(MethodGen mg){
+ this.mg = mg;
+ }
+
+ /**
+ * Assures index is of type INT.
+ * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
+ */
+ private void indexOfInt(Instruction o, Type index){
+ if (! index.equals(Type.INT)) {
constraintViolated(o, "The 'index' is not of type int but of type "+index+".");
}
- }
+ }
- /**
- * Assures the ReferenceType r is initialized (or Type.NULL).
- * Formally, this means (!(r instanceof UninitializedObjectType)), because
- * there are no uninitialized array types.
- * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
- */
- private void referenceTypeIsInitialized(Instruction o, ReferenceType r){
- if (r instanceof UninitializedObjectType){
- constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
- }
- }
-
- /** Assures value is of type INT. */
- private void valueOfInt(Instruction o, Type value){
- if (! value.equals(Type.INT)) {
+ /**
+ * Assures the ReferenceType r is initialized (or Type.NULL).
+ * Formally, this means (!(r instanceof UninitializedObjectType)), because
+ * there are no uninitialized array types.
+ * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
+ */
+ private void referenceTypeIsInitialized(Instruction o, ReferenceType r){
+ if (r instanceof UninitializedObjectType){
+ constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
+ }
+ }
+
+ /** Assures value is of type INT. */
+ private void valueOfInt(Instruction o, Type value){
+ if (! value.equals(Type.INT)) {
constraintViolated(o, "The 'value' is not of type int but of type "+value+".");
}
- }
+ }
- /**
- * Assures arrayref is of ArrayType or NULL;
- * returns true if and only if arrayref is non-NULL.
- * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is violated.
- */
- private boolean arrayrefOfArrayType(Instruction o, Type arrayref){
- if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) ) {
+ /**
+ * Assures arrayref is of ArrayType or NULL;
+ * returns true if and only if arrayref is non-NULL.
+ * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is violated.
+ */
+ private boolean arrayrefOfArrayType(Instruction o, Type arrayref){
+ 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);
- }
+ return (arrayref instanceof ArrayType);
+ }
+
+ /***************************************************************/
+ /* MISC */
+ /***************************************************************/
+ /**
+ * 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.]
+ *
+ * @see #visitStackConsumer(StackConsumer o)
+ * @see #visitStackProducer(StackProducer o)
+ * @see #visitStackInstruction(StackInstruction o)
+ */
+ private void _visitStackAccessor(Instruction o){
+ int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
+ if (consume > stack().slotsUsed()){
+ constraintViolated(o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
+ }
- /***************************************************************/
- /* MISC */
- /***************************************************************/
- /**
- * 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.]
- *
- * @see #visitStackConsumer(StackConsumer o)
- * @see #visitStackProducer(StackProducer o)
- * @see #visitStackInstruction(StackInstruction o)
- */
- private void _visitStackAccessor(Instruction o){
- int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
- if (consume > stack().slotsUsed()){
- constraintViolated(o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
- }
-
- int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
- if ( produce + stack().slotsUsed() > stack().maxStack() ){
- constraintViolated(o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
- }
- }
-
- /***************************************************************/
- /* "generic"visitXXXX methods where XXXX is an interface */
- /* therefore, we don't know the order of visiting; but we know */
- /* these methods are called before the visitYYYY methods below */
- /***************************************************************/
-
- /**
- * Assures the generic preconditions of a LoadClass instance.
- * The referenced class is loaded and pass2-verified.
- */
- @Override
+ int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
+ if ( produce + stack().slotsUsed() > stack().maxStack() ){
+ constraintViolated(o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
+ }
+ }
+
+ /***************************************************************/
+ /* "generic"visitXXXX methods where XXXX is an interface */
+ /* therefore, we don't know the order of visiting; but we know */
+ /* these methods are called before the visitYYYY methods below */
+ /***************************************************************/
+
+ /**
+ * Assures the generic preconditions of a LoadClass instance.
+ * The referenced class is loaded and pass2-verified.
+ */
+ @Override
public void visitLoadClass(LoadClass o){
- 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+"'.");
- }
- }
- }
-
- /**
- * Ensures the general preconditions of a StackConsumer instance.
- */
- @Override
+ 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+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the general preconditions of a StackConsumer instance.
+ */
+ @Override
public void visitStackConsumer(StackConsumer o){
- _visitStackAccessor((Instruction) o);
- }
-
- /**
- * Ensures the general preconditions of a StackProducer instance.
- */
- @Override
+ _visitStackAccessor((Instruction) o);
+ }
+
+ /**
+ * Ensures the general preconditions of a StackProducer instance.
+ */
+ @Override
public void visitStackProducer(StackProducer o){
- _visitStackAccessor((Instruction) o);
- }
+ _visitStackAccessor((Instruction) o);
+ }
- /***************************************************************/
- /* "generic" visitYYYY methods where YYYY is a superclass. */
- /* therefore, we know the order of visiting; we know */
- /* these methods are called after the visitXXXX methods above. */
- /***************************************************************/
- /**
- * Ensures the general preconditions of a CPInstruction instance.
- */
- @Override
+ /***************************************************************/
+ /* "generic" visitYYYY methods where YYYY is a superclass. */
+ /* therefore, we know the order of visiting; we know */
+ /* these methods are called after the visitXXXX methods above. */
+ /***************************************************************/
+ /**
+ * Ensures the general preconditions of a CPInstruction instance.
+ */
+ @Override
public void visitCPInstruction(CPInstruction o){
- 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!");
- }
- }
-
- /**
- * Ensures the general preconditions of a FieldInstruction instance.
- */
- @Override
+ 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!");
+ }
+ }
+
+ /**
+ * Ensures the general preconditions of a FieldInstruction instance.
+ */
+ @Override
public void visitFieldInstruction(FieldInstruction o){
- // 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(o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
- }
- }
- }
-
- /**
- * Ensures the general preconditions of an InvokeInstruction instance.
- */
- @Override
+ // 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(o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the general preconditions of an InvokeInstruction instance.
+ */
+ @Override
public void visitInvokeInstruction(InvokeInstruction o){
- // visitLoadClass(o) has been called before: Every FieldOrMethod
- // implements LoadClass.
- // visitCPInstruction(o) has been called before.
+ // visitLoadClass(o) has been called before: Every FieldOrMethod
+ // implements LoadClass.
+ // visitCPInstruction(o) has been called before.
//TODO
- }
-
- /**
- * Ensures the general preconditions of a StackInstruction instance.
- */
- @Override
+ }
+
+ /**
+ * Ensures the general preconditions of a StackInstruction instance.
+ */
+ @Override
public void visitStackInstruction(StackInstruction o){
- _visitStackAccessor(o);
- }
+ _visitStackAccessor(o);
+ }
- /**
- * Assures the generic preconditions of a LocalVariableInstruction instance.
- * That is, the index of the local variable must be valid.
- */
- @Override
+ /**
+ * Assures the generic preconditions of a LocalVariableInstruction instance.
+ * That is, the index of the local variable must be valid.
+ */
+ @Override
public void visitLocalVariableInstruction(LocalVariableInstruction o){
- if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
- constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
- }
- }
-
- /**
- * Assures the generic preconditions of a LoadInstruction instance.
- */
- @Override
+ if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
+ constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
+ }
+ }
+
+ /**
+ * Assures the generic preconditions of a LoadInstruction instance.
+ */
+ @Override
public void visitLoadInstruction(LoadInstruction o){
- //visitLocalVariableInstruction(o) is called before, because it is more generic.
+ //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 not read Type.UNKNOWN
- if (locals().get(o.getIndex()) == Type.UNKNOWN){
- constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content.");
- }
-
- // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
- // as a symbol for the higher halve at index N+1
- // [suppose some instruction put an int at N+1--- our double at N is defective]
- if (o.getType(cpg).getSize() == 2){
- if (locals().get(o.getIndex()+1) != Type.UNKNOWN){
- constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed.");
- }
- }
-
- // LOAD instructions must read the correct type.
- if (!(o instanceof ALOAD)){
- if (locals().get(o.getIndex()) != o.getType(cpg) ){
- constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
- }
- }
- else{ // we deal with an ALOAD
- if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
- constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
- }
- // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
- //referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
- }
-
- // LOAD instructions must have enough free stack slots.
- if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
- constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
- }
- }
-
- /**
- * Assures the generic preconditions of a StoreInstruction instance.
- */
- @Override
+ // LOAD instructions must read the correct type.
+ if (!(o instanceof ALOAD)){
+ if (locals().get(o.getIndex()) != o.getType(cpg) ){
+ constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
+ }
+ }
+ else{ // we deal with an ALOAD
+ if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
+ constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
+ }
+ // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
+ //referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
+ }
+
+ // LOAD instructions must have enough free stack slots.
+ if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
+ constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
+ }
+ }
+
+ /**
+ * Assures the generic preconditions of a StoreInstruction instance.
+ */
+ @Override
public void visitStoreInstruction(StoreInstruction o){
- //visitLocalVariableInstruction(o) is called before, because it is more generic.
+ //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);
+ //}
+ }
+ }
- if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking.
- constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
- }
-
- if ( (!(o instanceof ASTORE)) ){
- if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL.
- constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'.");
- }
- }
- else{ // we deal with ASTORE
- Type stacktop = stack().peek();
- if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){
- constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType.");
- }
- //if (stacktop instanceof ReferenceType){
- // referenceTypeIsInitialized(o, (ReferenceType) stacktop);
- //}
- }
- }
-
- /**
- * Assures the generic preconditions of a ReturnInstruction instance.
- */
- @Override
+ /**
+ * Assures the generic preconditions of a ReturnInstruction instance.
+ */
+ @Override
public void visitReturnInstruction(ReturnInstruction o){
- 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;
- }
+ 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 (o instanceof RETURN){
if (method_type != Type.VOID){
constraintViolated(o, "RETURN instruction in non-void method.");
}
else{
- 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()+"'.");
+ //}
}
- }
- 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{
- if (! ( method_type.equals( stack().peek() ))){
- constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'.");
- }
- }
- }
-
- /***************************************************************/
- /* "special"visitXXXX methods for one type of instruction each */
- /***************************************************************/
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ }
+ else{
+ if (! ( method_type.equals( stack().peek() ))){
+ constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'.");
+ }
+ }
+ }
+
+ /***************************************************************/
+ /* "special"visitXXXX methods for one type of instruction each */
+ /***************************************************************/
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitAALOAD(AALOAD o){
- Type arrayref = stack().peek(1);
- Type index = stack().peek(0);
-
- indexOfInt(o, index);
- if (arrayrefOfArrayType(o, arrayref)){
- if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
- constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
- }
- //referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ Type arrayref = stack().peek(1);
+ Type index = stack().peek(0);
+
+ indexOfInt(o, index);
+ if (arrayrefOfArrayType(o, arrayref)){
+ if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
+ constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
+ }
+ //referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitAASTORE(AASTORE o){
- try {
- 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(((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()+"')");
- }
- }
- } catch (ClassNotFoundException e) {
- // FIXME: maybe not the best way to handle this
- throw new AssertionViolatedException("Missing class: " + e, e);
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ try {
+ 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(((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()+"')");
+ }
+ }
+ } catch (ClassNotFoundException e) {
+ // FIXME: maybe not the best way to handle this
+ throw new AssertionViolatedException("Missing class: " + e, e);
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitACONST_NULL(ACONST_NULL o){
- // Nothing needs to be done here.
- }
+ // Nothing needs to be done here.
+ }
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitALOAD(ALOAD o){
- //visitLoadInstruction(LoadInstruction) is called before.
-
- // Nothing else needs to be done here.
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ //visitLoadInstruction(LoadInstruction) is called before.
+
+ // Nothing else needs to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitANEWARRAY(ANEWARRAY o){
- if (!stack().peek().equals(Type.INT)) {
+ 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.
+ // The runtime constant pool item at that index must be a symbolic reference to a class,
+ // array, or interface type. See Pass 3a.
}
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitARETURN(ARETURN o){
- if (! (stack().peek() instanceof ReferenceType) ){
- constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
- }
- ReferenceType objectref = (ReferenceType) (stack().peek());
- referenceTypeIsInitialized(o, objectref);
-
- // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
- // It cannot be done using Staerk-et-al's "set of object types" instead of a
- // "wider cast object type", anyway.
- //if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
- // constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
- //}
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (! (stack().peek() instanceof ReferenceType) ){
+ constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
+ }
+ ReferenceType objectref = (ReferenceType) (stack().peek());
+ referenceTypeIsInitialized(o, objectref);
+
+ // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
+ // It cannot be done using Staerk-et-al's "set of object types" instead of a
+ // "wider cast object type", anyway.
+ //if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
+ // constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
+ //}
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitARRAYLENGTH(ARRAYLENGTH o){
- Type arrayref = stack().peek(0);
- arrayrefOfArrayType(o, arrayref);
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ Type arrayref = stack().peek(0);
+ arrayrefOfArrayType(o, arrayref);
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitASTORE(ASTORE o){
- if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
- constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
- }
- //if (stack().peek() instanceof ReferenceType){
- // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
- //}
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
+ constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
+ }
+ //if (stack().peek() instanceof ReferenceType){
+ // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
+ //}
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitATHROW(ATHROW o){
- try {
- // 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)) {
+ try {
+ // 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()+"'.");
- }
- } catch (ClassNotFoundException e) {
- // FIXME: maybe not the best way to handle this
- throw new AssertionViolatedException("Missing class: " + e, e);
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+
+ 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()+"'.");
+ }
+ } catch (ClassNotFoundException e) {
+ // FIXME: maybe not the best way to handle this
+ throw new AssertionViolatedException("Missing class: " + e, e);
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitBALOAD(BALOAD o){
- Type arrayref = stack().peek(1);
- Type index = stack().peek(0);
- indexOfInt(o, index);
- if (arrayrefOfArrayType(o, arrayref)){
- if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
- (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
- constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
- }
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ Type arrayref = stack().peek(1);
+ Type index = stack().peek(0);
+ indexOfInt(o, index);
+ if (arrayrefOfArrayType(o, arrayref)){
+ if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
+ (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
+ constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitBASTORE(BASTORE o){
- Type arrayref = stack().peek(2);
- Type index = stack().peek(1);
- Type value = stack().peek(0);
-
- indexOfInt(o, index);
- valueOfInt(o, value);
- if (arrayrefOfArrayType(o, arrayref)){
- if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
- (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ) {
+ Type arrayref = stack().peek(2);
+ Type index = stack().peek(1);
+ Type value = stack().peek(0);
+
+ indexOfInt(o, index);
+ valueOfInt(o, value);
+ if (arrayrefOfArrayType(o, arrayref)){
+ if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
+ (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ) {
constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
}
- }
- }
+ }
+ }
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitBIPUSH(BIPUSH o){
- // Nothing to do...
- }
+ // Nothing to do...
+ }
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitBREAKPOINT(BREAKPOINT o){
- throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
- }
+ throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
+ }
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitCALOAD(CALOAD o){
- Type arrayref = stack().peek(1);
- Type index = stack().peek(0);
-
- indexOfInt(o, index);
- arrayrefOfArrayType(o, arrayref);
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ Type arrayref = stack().peek(1);
+ Type index = stack().peek(0);
+
+ indexOfInt(o, index);
+ arrayrefOfArrayType(o, arrayref);
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitCASTORE(CASTORE o){
- Type arrayref = stack().peek(2);
- Type index = stack().peek(1);
- Type value = stack().peek(0);
-
- indexOfInt(o, index);
- valueOfInt(o, value);
- if (arrayrefOfArrayType(o, arrayref)){
- if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
- constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
- }
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ Type arrayref = stack().peek(2);
+ Type index = stack().peek(1);
+ Type value = stack().peek(0);
+
+ indexOfInt(o, index);
+ valueOfInt(o, value);
+ if (arrayrefOfArrayType(o, arrayref)){
+ if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
+ constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
+ }
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitCHECKCAST(CHECKCAST o){
- // The objectref must be of type reference.
- Type objectref = stack().peek(0);
- if (!(objectref instanceof ReferenceType)){
- constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
- }
- //else{
- // referenceTypeIsInitialized(o, (ReferenceType) objectref);
- //}
- // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
- // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
- // pool item at the index must be a symbolic reference to a class, array, or interface type.
- Constant c = cpg.getConstant(o.getIndex());
- if (! (c instanceof ConstantClass)){
- constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ // 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+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitD2F(D2F o){
- if (stack().peek() != Type.DOUBLE){
- constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (stack().peek() != Type.DOUBLE){
+ constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitD2I(D2I o){
- if (stack().peek() != Type.DOUBLE){
- constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (stack().peek() != Type.DOUBLE){
+ constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitD2L(D2L o){
- if (stack().peek() != Type.DOUBLE){
- constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (stack().peek() != Type.DOUBLE){
+ constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDADD(DADD o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDALOAD(DALOAD 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 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDASTORE(DASTORE o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDCMPG(DCMPG o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDCMPL(DCMPL o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDCONST(DCONST o){
- // There's nothing to be done here.
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ // There's nothing to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDDIV(DDIV o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDLOAD(DLOAD o){
- //visitLoadInstruction(LoadInstruction) is called before.
-
- // Nothing else needs to be done here.
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ //visitLoadInstruction(LoadInstruction) is called before.
+
+ // Nothing else needs to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDMUL(DMUL o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDNEG(DNEG o){
- if (stack().peek() != Type.DOUBLE){
- constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (stack().peek() != Type.DOUBLE){
+ constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDREM(DREM o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDRETURN(DRETURN o){
- if (stack().peek() != Type.DOUBLE){
- constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ if (stack().peek() != Type.DOUBLE){
+ constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDSTORE(DSTORE o){
- //visitStoreInstruction(StoreInstruction) is called before.
-
- // Nothing else needs to be done here.
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ //visitStoreInstruction(StoreInstruction) is called before.
+
+ // Nothing else needs to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDSUB(DSUB o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP(DUP o){
- 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()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP_X1(DUP_X1 o){
- 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()+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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()+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP_X2(DUP_X2 o){
- 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()+"'.");
- }
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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()+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP2(DUP2 o){
- 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()+"'.");
- }
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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()+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP2_X1(DUP2_X1 o){
- 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()+"'.");
- }
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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()+"'.");
+ }
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitDUP2_X2(DUP2_X2 o){
- 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.");
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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.");
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitF2D(F2D 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitF2I(F2I 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitF2L(F2L 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitFADD(FADD 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitFALOAD(FALOAD 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 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitFASTORE(FASTORE o){
- 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)+"'.");
- }
- }
-
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ 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)+"'.");
+ }
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
public void visitFCMPG(FCMPG 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitFCMPL(FCMPL 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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitFCONST(FCONST o){
- // nothing to do here.
- }
+ // nothing to do here.
+ }
- /**
- * Ensures the specific preconditions of the said instruction.
- */
- @Override
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
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.
- */
- @Override
+ //visitLoadInstruction(LoadInstruction) is called before.
+
+ // Nothing else needs to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
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.
- */
- @Override
+ //visitStoreInstruction(StoreInstruction) is called before.
+
+ // Nothing else needs to be done here.
+ }
+
+ /**
+ * Ensures the specific preconditions of the said instruction.
+ */
+ @Override
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.
- */
- @Override
+ 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.
+ */
+ @Override
public void visitGETFIELD(GETFIELD o){
- try {
- 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 (Field field : fields) {
- if (field.getName().equals(field_name)){
- Type f_type = Type.getType(field.getSignature());
- Type o_type = o.getType(cpg);
- /* TODO: Check if assignment compatibility is sufficient.
- * What does Sun do?
- */
- if (f_type.equals(o_type)){
- f = field;
- break;
- }
- }
- }
-
- if (f == null){
- JavaClass[] superclasses = jc.getSuperClasses();
- outer:
+ try {
+ 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 (Field field : fields) {
+ if (field.getName().equals(field_name)){
+ Type f_type = Type.getType(field.getSignature());
+ Type o_type = o.getType(cpg);
+ /* TODO: Check if assignment compatibility is sufficient.
+ * What does Sun do?
+ */
+ if (f_type.equals(o_type)){
+ f = field;
+ break;
+ }
+ }
+ }
+
+ if (f == null){
+ JavaClass[] superclasses = jc.getSuperClasses();
+ outer:
for (JavaClass superclass : superclasses) {
fields = superclass.getFields();
for (Field field : fields) {
@@ -1269,1616 +1269,1616 @@ public class InstConstraintVisitor exten
}
}
}
- if (f == null) {
+ if (f == null) {
throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
}
- }
+ }
+
+ if (f.isProtected()){
+ ObjectType classtype = o.getClassType(cpg);
+ ObjectType curr = ObjectType.getInstance(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.");
+ }
+ }
+ }
- if (f.isProtected()){
- ObjectType classtype = o.getClassType(cpg);
- ObjectType curr = ObjectType.getInstance(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
[... 3055 lines stripped ...]