    001/*
    002 * Licensed to the Apache Software Foundation (ASF) under one or more
    003 * contributor license agreements.  See the NOTICE file distributed with
    004 * this work for additional information regarding copyright ownership.
    005 * The ASF licenses this file to You under the Apache License, Version 2.0
    006 * (the "License"); you may not use this file except in compliance with
    007 * the License.  You may obtain a copy of the License at
    008 *
    009 *      http://www.apache.org/licenses/LICENSE-2.0
    010 *
    011 *  Unless required by applicable law or agreed to in writing, software
    012 *  distributed under the License is distributed on an "AS IS" BASIS,
    013 *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
    014 *  See the License for the specific language governing permissions and
    015 *  limitations under the License.
    016 *
    017 */
    018package org.apache.bcel.verifier.structurals;
    019
    020import org.apache.bcel.Const;
    021import org.apache.bcel.Repository;
    022import org.apache.bcel.classfile.Constant;
    023import org.apache.bcel.classfile.ConstantClass;
    024import org.apache.bcel.classfile.ConstantDouble;
    025import org.apache.bcel.classfile.ConstantFieldref;
    026import org.apache.bcel.classfile.ConstantFloat;
    027import org.apache.bcel.classfile.ConstantInteger;
    028import org.apache.bcel.classfile.ConstantLong;
    029import org.apache.bcel.classfile.ConstantString;
    030import org.apache.bcel.classfile.Field;
    031import org.apache.bcel.classfile.JavaClass;
    032//CHECKSTYLE:OFF (there are lots of references!)
    033import org.apache.bcel.generic.*;
    034//CHECKSTYLE:ON
    035import org.apache.bcel.verifier.VerificationResult;
    036import org.apache.bcel.verifier.Verifier;
    037import org.apache.bcel.verifier.VerifierFactory;
    038import org.apache.bcel.verifier.exc.AssertionViolatedException;
    039import org.apache.bcel.verifier.exc.StructuralCodeConstraintException;
    040
    041/**
    042 * A Visitor class testing for valid preconditions of JVM instructions. The instance of this class will throw a
    043 * StructuralCodeConstraintException instance if an instruction is visitXXX()ed which has preconditions that are not
    044 * satisfied. TODO: Currently, the JVM's behavior concerning monitors (MONITORENTER, MONITOREXIT) is not modeled in
    045 * JustIce.
    046 *
    047 * @see StructuralCodeConstraintException
    048 */
    049public class InstConstraintVisitor extends EmptyVisitor {
    050
    051    private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance(GenericArray.class.getName());
    052
    053    /**
    054     * The Execution Frame we're working on.
    055     *
    056     * @see #setFrame(Frame f)
    057     * @see #locals()
    058     * @see #stack()
    059     */
    060    private Frame frame;
    061
    062    /**
    063     * The ConstantPoolGen we're working on.
    064     *
    065     * @see #setConstantPoolGen(ConstantPoolGen cpg)
    066     */
    067    private ConstantPoolGen cpg;
    068
    069    /**
    070     * The MethodGen we're working on.
    071     *
    072     * @see #setMethodGen(MethodGen mg)
    073     */
    074    private MethodGen mg;
    075
    076    /**
    077     * The constructor. Constructs a new instance of this class.
    078     */
    079    public InstConstraintVisitor() {
    080    }
    081
    082    /***************************************************************/
    083    /* MISC */
    084    /***************************************************************/
    085    /**
    086     * Ensures the general preconditions of an instruction that accesses the stack. This method is here because BCEL has no
    087     * such superinterface for the stack accessing instructions; and there are funny unexpected exceptions in the semantices
    088     * of the superinterfaces and superclasses provided. E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
    089     * Therefore, this method is called by all StackProducer, StackConsumer, and StackInstruction instances via their
    090     * visitXXX() method. Unfortunately, as the superclasses and superinterfaces overlap, some instructions cause this
    091     * method to be called two or three times. [TODO: Fix this.]
    092     *
    093     * @see #visitStackConsumer(StackConsumer o)
    094     * @see #visitStackProducer(StackProducer o)
    095     * @see #visitStackInstruction(StackInstruction o)
    096     */
    097    private void _visitStackAccessor(final Instruction o) {
    098        final int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
    099        if (consume > stack().slotsUsed()) {
    100            constraintViolated(o, "Cannot consume " + consume + " stack slots: only " + stack().slotsUsed() + " slot(s) left on stack!\nStack:\n" + stack());
    101        }
    102
    103        final int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
    104        if (produce + stack().slotsUsed() > stack().maxStack()) {
    105            constraintViolated(o, "Cannot produce " + produce + " stack slots: only " + (stack().maxStack() - stack().slotsUsed())
    106                + " free stack slot(s) left.\nStack:\n" + stack());
    107        }
    108    }
    109
    110    /**
    111     * Assures arrayref is of ArrayType or NULL; returns true if and only if arrayref is non-NULL.
    112     *
    113     * @throws StructuralCodeConstraintException if the above constraint is violated.
    114     */
    115    private boolean arrayrefOfArrayType(final Instruction o, final Type arrayref) {
    116        if (!(arrayref instanceof ArrayType || arrayref.equals(Type.NULL))) {
    117            constraintViolated(o, "The 'arrayref' does not refer to an array but is of type " + arrayref + ".");
    118        }
    119        return arrayref instanceof ArrayType;
    120    }
    121
    122    /**
    123     * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor that a constraint
    124     * violation has occurred. This is done by throwing an instance of a StructuralCodeConstraintException.
    125     *
    126     * @throws StructuralCodeConstraintException always.
    127     */
    128    private void constraintViolated(final Instruction violator, final String description) {
    129        final String fq_classname = violator.getClass().getName();
    130        throw new StructuralCodeConstraintException(
    131            "Instruction " + fq_classname.substring(fq_classname.lastIndexOf('.') + 1) + " constraint violated: " + description);
    132    }
    133
    134    private ObjectType getObjectType(final FieldInstruction o) {
    135        final ReferenceType rt = o.getReferenceType(cpg);
    136        if (rt instanceof ObjectType) {
    137            return (ObjectType) rt;
    138        }
    139        constraintViolated(o, "expecting ObjectType but got " + rt);
    140        return null;
    141    }
    142
    143    /**
    144     * Assures index is of type INT.
    145     *
    146     * @throws StructuralCodeConstraintException if the above constraint is not satisfied.
    147     */
    148    private void indexOfInt(final Instruction o, final Type index) {
    149        if (!index.equals(Type.INT)) {
    150            constraintViolated(o, "The 'index' is not of type int but of type " + index + ".");
    151        }
    152    }
    153
    154    /**
    155     * The LocalVariables we're working on.
    156     *
    157     * @see #setFrame(Frame f)
    158     */
    159    private LocalVariables locals() {
    160        return frame.getLocals();
    161    }
    162
    163    /**
    164     * Assures the ReferenceType r is initialized (or Type.NULL). Formally, this means (!(r instanceof
    165     * UninitializedObjectType)), because there are no uninitialized array types.
    166     *
    167     * @throws StructuralCodeConstraintException if the above constraint is not satisfied.
    168     */
    169    private void referenceTypeIsInitialized(final Instruction o, final ReferenceType r) {
    170        if (r instanceof UninitializedObjectType) {
    171            constraintViolated(o, "Working on an uninitialized object '" + r + "'.");
    172        }
    173    }
    174
    175    /**
    176     * Sets the ConstantPoolGen instance needed for constraint checking prior to execution.
    177     */
    178    public void setConstantPoolGen(final ConstantPoolGen cpg) { // TODO could be package-protected?
    179        this.cpg = cpg;
    180    }
    181
    182    /**
    183     * This returns the single instance of the InstConstraintVisitor class. To operate correctly, other values must have
    184     * been set before actually using the instance. Use this method for performance reasons.
    185     *
    186     * @see #setConstantPoolGen(ConstantPoolGen cpg)
    187     * @see #setMethodGen(MethodGen mg)
    188     */
    189    public void setFrame(final Frame f) { // TODO could be package-protected?
    190        this.frame = f;
    191        // if (singleInstance.mg == null || singleInstance.cpg == null)
    192        // throw new AssertionViolatedException("Forgot to set important values first.");
    193    }
    194
    195    /**
    196     * Sets the MethodGen instance needed for constraint checking prior to execution.
    197     */
    198    public void setMethodGen(final MethodGen mg) {
    199        this.mg = mg;
    200    }
    201
    202    /**
    203     * The OperandStack we're working on.
    204     *
    205     * @see #setFrame(Frame f)
    206     */
    207    private OperandStack stack() {
    208        return frame.getStack();
    209    }
    210
    211    /***************************************************************/
    212    /* "generic"visitXXXX methods where XXXX is an interface */
    213    /* therefore, we don't know the order of visiting; but we know */
    214    /* these methods are called before the visitYYYY methods below */
    215    /***************************************************************/
    216
    217    /** Assures value is of type INT. */
    218    private void valueOfInt(final Instruction o, final Type value) {
    219        if (!value.equals(Type.INT)) {
    220            constraintViolated(o, "The 'value' is not of type int but of type " + value + ".");
    221        }
    222    }
    223
    224    /**
    225     * Ensures the specific preconditions of the said instruction.
    226     */
    227    @Override
    228    public void visitAALOAD(final AALOAD o) {
    229        final Type arrayref = stack().peek(1);
    230        final Type index = stack().peek(0);
    231
    232        indexOfInt(o, index);
    233        if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
    234            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
    235                + ((ArrayType) arrayref).getElementType() + ".");
    236        }
    237        // referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
    238    }
    239
    240    /**
    241     * Ensures the specific preconditions of the said instruction.
    242     */
    243    @Override
    244    public void visitAASTORE(final AASTORE o) {
    245        final Type arrayref = stack().peek(2);
    246        final Type index = stack().peek(1);
    247        final Type value = stack().peek(0);
    248
    249        indexOfInt(o, index);
    250        if (!(value instanceof ReferenceType)) {
    251            constraintViolated(o, "The 'value' is not of a ReferenceType but of type " + value + ".");
    252        } else {
    253            // referenceTypeIsInitialized(o, (ReferenceType) value);
    254        }
    255        // Don't bother further with "referenceTypeIsInitialized()", there are no arrays
    256        // of an uninitialized object type.
    257        if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
    258            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
    259                + ((ArrayType) arrayref).getElementType() + ".");
    260        }
    261        // No check for array element assignment compatibility. This is done at runtime.
    262    }
    263
    264    /**
    265     * Ensures the specific preconditions of the said instruction.
    266     */
    267    @Override
    268    public void visitACONST_NULL(final ACONST_NULL o) {
    269        // Nothing needs to be done here.
    270    }
    271
    272    /**
    273     * Ensures the specific preconditions of the said instruction.
    274     */
    275    @Override
    276    public void visitALOAD(final ALOAD o) {
    277        // visitLoadInstruction(LoadInstruction) is called before.
    278
    279        // Nothing else needs to be done here.
    280    }
    281
    282    /**
    283     * Ensures the specific preconditions of the said instruction.
    284     */
    285    @Override
    286    public void visitANEWARRAY(final ANEWARRAY o) {
    287        if (!stack().peek().equals(Type.INT)) {
    288            constraintViolated(o, "The 'count' at the stack top is not of type '" + Type.INT + "' but of type '" + stack().peek() + "'.");
    289            // The runtime constant pool item at that index must be a symbolic reference to a class,
    290            // array, or interface type. See Pass 3a.
    291        }
    292    }
    293
    294    /**
    295     * Ensures the specific preconditions of the said instruction.
    296     */
    297    @Override
    298    public void visitARETURN(final ARETURN o) {
    299        if (!(stack().peek() instanceof ReferenceType)) {
    300            constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '" + stack().peek() + "'.");
    301        }
    302        final ReferenceType objectref = (ReferenceType) stack().peek();
    303        referenceTypeIsInitialized(o, objectref);
    304
    305        // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
    306        // It cannot be done using Staerk-et-al's "set of object types" instead of a
    307        // "wider cast object type", anyway.
    308        // if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )) {
    309        // constraintViolated(o, "The 'objectref' type "+objectref+
    310        // " at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
    311        // }
    312    }
    313
    314    /**
    315     * Ensures the specific preconditions of the said instruction.
    316     */
    317    @Override
    318    public void visitARRAYLENGTH(final ARRAYLENGTH o) {
    319        final Type arrayref = stack().peek(0);
    320        arrayrefOfArrayType(o, arrayref);
    321    }
    322
    323    /**
    324     * Ensures the specific preconditions of the said instruction.
    325     */
    326    @Override
    327    public void visitASTORE(final ASTORE o) {
    328        if (!(stack().peek() instanceof ReferenceType || stack().peek() instanceof ReturnaddressType)) {
    329            constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of " + stack().peek() + ".");
    330        }
    331        // if (stack().peek() instanceof ReferenceType) {
    332        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    333        // }
    334    }
    335
    336    /**
    337     * Ensures the specific preconditions of the said instruction.
    338     */
    339    @Override
    340    public void visitATHROW(final ATHROW o) {
    341        try {
    342            // It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
    343            // not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
    344            if (!(stack().peek() instanceof ObjectType || stack().peek().equals(Type.NULL))) {
    345                constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type " + stack().peek() + ".");
    346            }
    347
    348            // NULL is a subclass of every class, so to speak.
    349            if (stack().peek().equals(Type.NULL)) {
    350                return;
    351            }
    352
    353            final ObjectType exc = (ObjectType) stack().peek();
    354            final ObjectType throwable = (ObjectType) Type.getType("Ljava/lang/Throwable;");
    355            if (!exc.subclassOf(throwable) && !exc.equals(throwable)) {
    356                constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '" + stack().peek() + "'.");
    357            }
    358        } catch (final ClassNotFoundException e) {
    359            // FIXME: maybe not the best way to handle this
    360            throw new AssertionViolatedException("Missing class: " + e, e);
    361        }
    362    }
    363
    364    /**
    365     * Ensures the specific preconditions of the said instruction.
    366     */
    367    @Override
    368    public void visitBALOAD(final BALOAD o) {
    369        final Type arrayref = stack().peek(1);
    370        final Type index = stack().peek(0);
    371        indexOfInt(o, index);
    372        if (arrayrefOfArrayType(o, arrayref)
    373            && !(((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN) || ((ArrayType) arrayref).getElementType().equals(Type.BYTE))) {
    374            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
    375                + ((ArrayType) arrayref).getElementType() + "'.");
    376        }
    377    }
    378
    379    /***************************************************************/
    380    /* "special"visitXXXX methods for one type of instruction each */
    381    /***************************************************************/
    382
    383    /**
    384     * Ensures the specific preconditions of the said instruction.
    385     */
    386    @Override
    387    public void visitBASTORE(final BASTORE o) {
    388        final Type arrayref = stack().peek(2);
    389        final Type index = stack().peek(1);
    390        final Type value = stack().peek(0);
    391
    392        indexOfInt(o, index);
    393        valueOfInt(o, value);
    394        if (arrayrefOfArrayType(o, arrayref)
    395            && !(((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN) || ((ArrayType) arrayref).getElementType().equals(Type.BYTE))) {
    396            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
    397                + ((ArrayType) arrayref).getElementType() + "'.");
    398        }
    399    }
    400
    401    /**
    402     * Ensures the specific preconditions of the said instruction.
    403     */
    404    @Override
    405    public void visitBIPUSH(final BIPUSH o) {
    406        // Nothing to do...
    407    }
    408
    409    /**
    410     * Ensures the specific preconditions of the said instruction.
    411     */
    412    @Override
    413    public void visitBREAKPOINT(final BREAKPOINT o) {
    414        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
    415    }
    416
    417    /**
    418     * Ensures the specific preconditions of the said instruction.
    419     */
    420    @Override
    421    public void visitCALOAD(final CALOAD o) {
    422        final Type arrayref = stack().peek(1);
    423        final Type index = stack().peek(0);
    424
    425        indexOfInt(o, index);
    426        arrayrefOfArrayType(o, arrayref);
    427    }
    428
    429    /**
    430     * Ensures the specific preconditions of the said instruction.
    431     */
    432    @Override
    433    public void visitCASTORE(final CASTORE o) {
    434        final Type arrayref = stack().peek(2);
    435        final Type index = stack().peek(1);
    436        final Type value = stack().peek(0);
    437
    438        indexOfInt(o, index);
    439        valueOfInt(o, value);
    440        if (arrayrefOfArrayType(o, arrayref) && !((ArrayType) arrayref).getElementType().equals(Type.CHAR)) {
    441            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "
    442                + ((ArrayType) arrayref).getElementType() + ".");
    443        }
    444    }
    445
    446    /**
    447     * Ensures the specific preconditions of the said instruction.
    448     */
    449    @Override
    450    public void visitCHECKCAST(final CHECKCAST o) {
    451        // The objectref must be of type reference.
    452        final Type objectref = stack().peek(0);
    453        if (!(objectref instanceof ReferenceType)) {
    454            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
    455        }
    456        // else{
    457        // referenceTypeIsInitialized(o, (ReferenceType) objectref);
    458        // }
    459        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
    460        // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
    461        // pool item at the index must be a symbolic reference to a class, array, or interface type.
    462        final Constant c = cpg.getConstant(o.getIndex());
    463        if (!(c instanceof ConstantClass)) {
    464            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
    465        }
    466    }
    467
    468    /***************************************************************/
    469    /* "generic" visitYYYY methods where YYYY is a superclass. */
    470    /* therefore, we know the order of visiting; we know */
    471    /* these methods are called after the visitXXXX methods above. */
    472    /***************************************************************/
    473    /**
    474     * Ensures the general preconditions of a CPInstruction instance.
    475     */
    476    @Override
    477    public void visitCPInstruction(final CPInstruction o) {
    478        final int idx = o.getIndex();
    479        if (idx < 0 || idx >= cpg.getSize()) {
    480            throw new AssertionViolatedException("Huh?! Constant pool index of instruction '" + o + "' illegal? Pass 3a should have checked this!");
    481        }
    482    }
    483
    484    /**
    485     * Ensures the specific preconditions of the said instruction.
    486     */
    487    @Override
    488    public void visitD2F(final D2F o) {
    489        if (stack().peek() != Type.DOUBLE) {
    490            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    491        }
    492    }
    493
    494    /**
    495     * Ensures the specific preconditions of the said instruction.
    496     */
    497    @Override
    498    public void visitD2I(final D2I o) {
    499        if (stack().peek() != Type.DOUBLE) {
    500            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    501        }
    502    }
    503
    504    /**
    505     * Ensures the specific preconditions of the said instruction.
    506     */
    507    @Override
    508    public void visitD2L(final D2L o) {
    509        if (stack().peek() != Type.DOUBLE) {
    510            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    511        }
    512    }
    513
    514    /**
    515     * Ensures the specific preconditions of the said instruction.
    516     */
    517    @Override
    518    public void visitDADD(final DADD o) {
    519        if (stack().peek() != Type.DOUBLE) {
    520            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    521        }
    522        if (stack().peek(1) != Type.DOUBLE) {
    523            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    524        }
    525    }
    526
    527    /**
    528     * Ensures the specific preconditions of the said instruction.
    529     */
    530    @Override
    531    public void visitDALOAD(final DALOAD o) {
    532        indexOfInt(o, stack().peek());
    533        if (stack().peek(1) == Type.NULL) {
    534            return;
    535        }
    536        if (!(stack().peek(1) instanceof ArrayType)) {
    537            constraintViolated(o, "Stack next-to-top must be of type double[] but is '" + stack().peek(1) + "'.");
    538        }
    539        final Type t = ((ArrayType) stack().peek(1)).getBasicType();
    540        if (t != Type.DOUBLE) {
    541            constraintViolated(o, "Stack next-to-top must be of type double[] but is '" + stack().peek(1) + "'.");
    542        }
    543    }
    544
    545    /**
    546     * Ensures the specific preconditions of the said instruction.
    547     */
    548    @Override
    549    public void visitDASTORE(final DASTORE o) {
    550        if (stack().peek() != Type.DOUBLE) {
    551            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    552        }
    553        indexOfInt(o, stack().peek(1));
    554        if (stack().peek(2) == Type.NULL) {
    555            return;
    556        }
    557        if (!(stack().peek(2) instanceof ArrayType)) {
    558            constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '" + stack().peek(2) + "'.");
    559        }
    560        final Type t = ((ArrayType) stack().peek(2)).getBasicType();
    561        if (t != Type.DOUBLE) {
    562            constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '" + stack().peek(2) + "'.");
    563        }
    564    }
    565
    566    /**
    567     * Ensures the specific preconditions of the said instruction.
    568     */
    569    @Override
    570    public void visitDCMPG(final DCMPG o) {
    571        if (stack().peek() != Type.DOUBLE) {
    572            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    573        }
    574        if (stack().peek(1) != Type.DOUBLE) {
    575            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    576        }
    577    }
    578
    579    /**
    580     * Ensures the specific preconditions of the said instruction.
    581     */
    582    @Override
    583    public void visitDCMPL(final DCMPL o) {
    584        if (stack().peek() != Type.DOUBLE) {
    585            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    586        }
    587        if (stack().peek(1) != Type.DOUBLE) {
    588            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    589        }
    590    }
    591
    592    /**
    593     * Ensures the specific preconditions of the said instruction.
    594     */
    595    @Override
    596    public void visitDCONST(final DCONST o) {
    597        // There's nothing to be done here.
    598    }
    599
    600    /**
    601     * Ensures the specific preconditions of the said instruction.
    602     */
    603    @Override
    604    public void visitDDIV(final DDIV o) {
    605        if (stack().peek() != Type.DOUBLE) {
    606            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    607        }
    608        if (stack().peek(1) != Type.DOUBLE) {
    609            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    610        }
    611    }
    612
    613    /**
    614     * Ensures the specific preconditions of the said instruction.
    615     */
    616    @Override
    617    public void visitDLOAD(final DLOAD o) {
    618        // visitLoadInstruction(LoadInstruction) is called before.
    619
    620        // Nothing else needs to be done here.
    621    }
    622
    623    /**
    624     * Ensures the specific preconditions of the said instruction.
    625     */
    626    @Override
    627    public void visitDMUL(final DMUL o) {
    628        if (stack().peek() != Type.DOUBLE) {
    629            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    630        }
    631        if (stack().peek(1) != Type.DOUBLE) {
    632            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    633        }
    634    }
    635
    636    /**
    637     * Ensures the specific preconditions of the said instruction.
    638     */
    639    @Override
    640    public void visitDNEG(final DNEG o) {
    641        if (stack().peek() != Type.DOUBLE) {
    642            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    643        }
    644    }
    645
    646    /**
    647     * Ensures the specific preconditions of the said instruction.
    648     */
    649    @Override
    650    public void visitDREM(final DREM o) {
    651        if (stack().peek() != Type.DOUBLE) {
    652            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    653        }
    654        if (stack().peek(1) != Type.DOUBLE) {
    655            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    656        }
    657    }
    658
    659    /**
    660     * Ensures the specific preconditions of the said instruction.
    661     */
    662    @Override
    663    public void visitDRETURN(final DRETURN o) {
    664        if (stack().peek() != Type.DOUBLE) {
    665            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    666        }
    667    }
    668
    669    /**
    670     * Ensures the specific preconditions of the said instruction.
    671     */
    672    @Override
    673    public void visitDSTORE(final DSTORE o) {
    674        // visitStoreInstruction(StoreInstruction) is called before.
    675
    676        // Nothing else needs to be done here.
    677    }
    678
    679    /**
    680     * Ensures the specific preconditions of the said instruction.
    681     */
    682    @Override
    683    public void visitDSUB(final DSUB o) {
    684        if (stack().peek() != Type.DOUBLE) {
    685            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
    686        }
    687        if (stack().peek(1) != Type.DOUBLE) {
    688            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
    689        }
    690    }
    691
    692    /**
    693     * Ensures the specific preconditions of the said instruction.
    694     */
    695    @Override
    696    public void visitDUP(final DUP o) {
    697        if (stack().peek().getSize() != 1) {
    698            constraintViolated(o,
    699                "Won't DUP type on stack top '" + stack().peek() + "' because it must occupy exactly one slot, not '" + stack().peek().getSize() + "'.");
    700        }
    701    }
    702
    703    /**
    704     * Ensures the specific preconditions of the said instruction.
    705     */
    706    @Override
    707    public void visitDUP_X1(final DUP_X1 o) {
    708        if (stack().peek().getSize() != 1) {
    709            constraintViolated(o, "Type on stack top '" + stack().peek() + "' should occupy exactly one slot, not '" + stack().peek().getSize() + "'.");
    710        }
    711        if (stack().peek(1).getSize() != 1) {
    712            constraintViolated(o,
    713                "Type on stack next-to-top '" + stack().peek(1) + "' should occupy exactly one slot, not '" + stack().peek(1).getSize() + "'.");
    714        }
    715    }
    716
    717    /**
    718     * Ensures the specific preconditions of the said instruction.
    719     */
    720    @Override
    721    public void visitDUP_X2(final DUP_X2 o) {
    722        if (stack().peek().getSize() != 1) {
    723            constraintViolated(o, "Stack top type must be of size 1, but is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
    724        }
    725        if (stack().peek(1).getSize() == 2) {
    726            return; // Form 2, okay.
    727        }
    728        // stack().peek(1).getSize == 1.
    729        if (stack().peek(2).getSize() != 1) {
    730            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: '"
    731                + stack().peek(2) + "' of size '" + stack().peek(2).getSize() + "'.");
    732        }
    733    }
    734
    735    /**
    736     * Ensures the specific preconditions of the said instruction.
    737     */
    738    @Override
    739    public void visitDUP2(final DUP2 o) {
    740        if (stack().peek().getSize() == 2) {
    741            return; // Form 2, okay.
    742        }
    743        // stack().peek().getSize() == 1.
    744        if (stack().peek(1).getSize() != 1) {
    745            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 '"
    746                + stack().peek(1).getSize() + "'.");
    747        }
    748    }
    749
    750    /**
    751     * Ensures the specific preconditions of the said instruction.
    752     */
    753    @Override
    754    public void visitDUP2_X1(final DUP2_X1 o) {
    755        if (stack().peek().getSize() == 2) {
    756            if (stack().peek(1).getSize() != 1) {
    757                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 '"
    758                    + stack().peek(1).getSize() + "'.");
    759            }
    760        } else { // stack top is of size 1
    761            if (stack().peek(1).getSize() != 1) {
    762                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 '"
    763                    + stack().peek(1).getSize() + "'.");
    764            }
    765            if (stack().peek(2).getSize() != 1) {
    766                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)
    767                    + "' of size '" + stack().peek(2).getSize() + "'.");
    768            }
    769        }
    770    }
    771
    772    /**
    773     * Ensures the specific preconditions of the said instruction.
    774     */
    775    @Override
    776    public void visitDUP2_X2(final DUP2_X2 o) {
    777
    778        if (stack().peek(0).getSize() == 2) {
    779            // stack top size is 2, next-to-top's size is 1
    780            if (stack().peek(1).getSize() == 2 || stack().peek(2).getSize() == 1) {
    781                return; // Form 2
    782            }
    783            constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1,"
    784                + " 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() + "'.");
    785        } else if (stack().peek(1).getSize() == 1 && (stack().peek(2).getSize() == 2 || stack().peek(3).getSize() == 1)) {
    786            return; // Form 1
    787        }
    788        constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
    789    }
    790
    791    /**
    792     * Ensures the specific preconditions of the said instruction.
    793     */
    794    @Override
    795    public void visitF2D(final F2D o) {
    796        if (stack().peek() != Type.FLOAT) {
    797            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    798        }
    799    }
    800
    801    /**
    802     * Ensures the specific preconditions of the said instruction.
    803     */
    804    @Override
    805    public void visitF2I(final F2I o) {
    806        if (stack().peek() != Type.FLOAT) {
    807            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    808        }
    809    }
    810
    811    /**
    812     * Ensures the specific preconditions of the said instruction.
    813     */
    814    @Override
    815    public void visitF2L(final F2L o) {
    816        if (stack().peek() != Type.FLOAT) {
    817            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    818        }
    819    }
    820
    821    /**
    822     * Ensures the specific preconditions of the said instruction.
    823     */
    824    @Override
    825    public void visitFADD(final FADD o) {
    826        if (stack().peek() != Type.FLOAT) {
    827            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    828        }
    829        if (stack().peek(1) != Type.FLOAT) {
    830            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    831        }
    832    }
    833
    834    /**
    835     * Ensures the specific preconditions of the said instruction.
    836     */
    837    @Override
    838    public void visitFALOAD(final FALOAD o) {
    839        indexOfInt(o, stack().peek());
    840        if (stack().peek(1) == Type.NULL) {
    841            return;
    842        }
    843        if (!(stack().peek(1) instanceof ArrayType)) {
    844            constraintViolated(o, "Stack next-to-top must be of type float[] but is '" + stack().peek(1) + "'.");
    845        }
    846        final Type t = ((ArrayType) stack().peek(1)).getBasicType();
    847        if (t != Type.FLOAT) {
    848            constraintViolated(o, "Stack next-to-top must be of type float[] but is '" + stack().peek(1) + "'.");
    849        }
    850    }
    851
    852    /**
    853     * Ensures the specific preconditions of the said instruction.
    854     */
    855    @Override
    856    public void visitFASTORE(final FASTORE o) {
    857        if (stack().peek() != Type.FLOAT) {
    858            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    859        }
    860        indexOfInt(o, stack().peek(1));
    861        if (stack().peek(2) == Type.NULL) {
    862            return;
    863        }
    864        if (!(stack().peek(2) instanceof ArrayType)) {
    865            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '" + stack().peek(2) + "'.");
    866        }
    867        final Type t = ((ArrayType) stack().peek(2)).getBasicType();
    868        if (t != Type.FLOAT) {
    869            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '" + stack().peek(2) + "'.");
    870        }
    871    }
    872
    873    /**
    874     * Ensures the specific preconditions of the said instruction.
    875     */
    876    @Override
    877    public void visitFCMPG(final FCMPG o) {
    878        if (stack().peek() != Type.FLOAT) {
    879            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    880        }
    881        if (stack().peek(1) != Type.FLOAT) {
    882            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    883        }
    884    }
    885
    886    /**
    887     * Ensures the specific preconditions of the said instruction.
    888     */
    889    @Override
    890    public void visitFCMPL(final FCMPL o) {
    891        if (stack().peek() != Type.FLOAT) {
    892            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    893        }
    894        if (stack().peek(1) != Type.FLOAT) {
    895            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    896        }
    897    }
    898
    899    /**
    900     * Ensures the specific preconditions of the said instruction.
    901     */
    902    @Override
    903    public void visitFCONST(final FCONST o) {
    904        // nothing to do here.
    905    }
    906
    907    /**
    908     * Ensures the specific preconditions of the said instruction.
    909     */
    910    @Override
    911    public void visitFDIV(final FDIV o) {
    912        if (stack().peek() != Type.FLOAT) {
    913            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    914        }
    915        if (stack().peek(1) != Type.FLOAT) {
    916            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    917        }
    918    }
    919
    920    /**
    921     * Ensures the general preconditions of a FieldInstruction instance.
    922     */
    923    @Override
    924    public void visitFieldInstruction(final FieldInstruction o) {
    925        // visitLoadClass(o) has been called before: Every FieldOrMethod
    926        // implements LoadClass.
    927        // visitCPInstruction(o) has been called before.
    928        // A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC
    929        final Constant c = cpg.getConstant(o.getIndex());
    930        if (!(c instanceof ConstantFieldref)) {
    931            constraintViolated(o, "Index '" + o.getIndex() + "' should refer to a CONSTANT_Fieldref_info structure, but refers to '" + c + "'.");
    932        }
    933        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    934        final Type t = o.getType(cpg);
    935        if (t instanceof ObjectType) {
    936            final String name = ((ObjectType) t).getClassName();
    937            final Verifier v = VerifierFactory.getVerifier(name);
    938            final VerificationResult vr = v.doPass2();
    939            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    940                constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    941            }
    942        }
    943    }
    944
    945    /**
    946     * Ensures the specific preconditions of the said instruction.
    947     */
    948    @Override
    949    public void visitFLOAD(final FLOAD o) {
    950        // visitLoadInstruction(LoadInstruction) is called before.
    951
    952        // Nothing else needs to be done here.
    953    }
    954
    955    /**
    956     * Ensures the specific preconditions of the said instruction.
    957     */
    958    @Override
    959    public void visitFMUL(final FMUL o) {
    960        if (stack().peek() != Type.FLOAT) {
    961            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    962        }
    963        if (stack().peek(1) != Type.FLOAT) {
    964            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    965        }
    966    }
    967
    968    /**
    969     * Ensures the specific preconditions of the said instruction.
    970     */
    971    @Override
    972    public void visitFNEG(final FNEG o) {
    973        if (stack().peek() != Type.FLOAT) {
    974            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    975        }
    976    }
    977
    978    /**
    979     * Ensures the specific preconditions of the said instruction.
    980     */
    981    @Override
    982    public void visitFREM(final FREM o) {
    983        if (stack().peek() != Type.FLOAT) {
    984            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    985        }
    986        if (stack().peek(1) != Type.FLOAT) {
    987            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    988        }
    989    }
    990
    991    /**
    992     * Ensures the specific preconditions of the said instruction.
    993     */
    994    @Override
    995    public void visitFRETURN(final FRETURN o) {
    996        if (stack().peek() != Type.FLOAT) {
    997            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    998        }
    999    }
    1000
    1001    /**
    1002     * Ensures the specific preconditions of the said instruction.
    1003     */
    1004    @Override
    1005    public void visitFSTORE(final FSTORE o) {
    1006        // visitStoreInstruction(StoreInstruction) is called before.
    1007
    1008        // Nothing else needs to be done here.
    1009    }
    1010
    1011    /**
    1012     * Ensures the specific preconditions of the said instruction.
    1013     */
    1014    @Override
    1015    public void visitFSUB(final FSUB o) {
    1016        if (stack().peek() != Type.FLOAT) {
    1017            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
    1018        }
    1019        if (stack().peek(1) != Type.FLOAT) {
    1020            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
    1021        }
    1022    }
    1023
    1024    /**
    1025     * Ensures the specific preconditions of the said instruction.
    1026     */
    1027    @Override
    1028    public void visitGETFIELD(final GETFIELD o) {
    1029        try {
    1030            final Type objectref = stack().peek();
    1031            if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
    1032                constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '" + objectref + "'.");
    1033            }
    1034
    1035            final String field_name = o.getFieldName(cpg);
    1036
    1037            final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
    1038            Field[] fields = jc.getFields();
    1039            Field f = null;
    1040            for (final Field field : fields) {
    1041                if (field.getName().equals(field_name)) {
    1042                    final Type fType = Type.getType(field.getSignature());
    1043                    final Type oType = o.getType(cpg);
    1044                    /*
    1045                     * TODO: Check if assignment compatibility is sufficient. What does Sun do?
    1046                     */
    1047                    if (fType.equals(oType)) {
    1048                        f = field;
    1049                        break;
    1050                    }
    1051                }
    1052            }
    1053
    1054            if (f == null) {
    1055                final JavaClass[] superclasses = jc.getSuperClasses();
    1056                outer: for (final JavaClass superclass : superclasses) {
    1057                    fields = superclass.getFields();
    1058                    for (final Field field : fields) {
    1059                        if (field.getName().equals(field_name)) {
    1060                            final Type fType = Type.getType(field.getSignature());
    1061                            final Type oType = o.getType(cpg);
    1062                            if (fType.equals(oType)) {
    1063                                f = field;
    1064                                if ((f.getAccessFlags() & (Const.ACC_PUBLIC | Const.ACC_PROTECTED)) == 0) {
    1065                                    f = null;
    1066                                }
    1067                                break outer;
    1068                            }
    1069                        }
    1070                    }
    1071                }
    1072                if (f == null) {
    1073                    throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
    1074                }
    1075            }
    1076
    1077            if (f.isProtected()) {
    1078                final ObjectType classtype = getObjectType(o);
    1079                final ObjectType curr = ObjectType.getInstance(mg.getClassName());
    1080
    1081                if (classtype.equals(curr) || curr.subclassOf(classtype)) {
    1082                    final Type t = stack().peek();
    1083                    if (t == Type.NULL) {
    1084                        return;
    1085                    }
    1086                    if (!(t instanceof ObjectType)) {
    1087                        constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + t + "'.");
    1088                    }
    1089                    final ObjectType objreftype = (ObjectType) t;
    1090                    if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
    1091                        // TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
    1092                        // created during the verification.
    1093                        // "Wider" object types don't allow us to check for things like that below.
    1094                        // constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, "+
    1095                        // "and it's a member of the current class or a superclass of the current class."+
    1096                        // " However, the referenced object type '"+stack().peek()+
    1097                        // "' is not the current class or a subclass of the current class.");
    1098                    }
    1099                }
    1100            }
    1101
    1102            // TODO: Could go into Pass 3a.
    1103            if (f.isStatic()) {
    1104                constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
    1105            }
    1106
    1107        } catch (final ClassNotFoundException e) {
    1108            // FIXME: maybe not the best way to handle this
    1109            throw new AssertionViolatedException("Missing class: " + e, e);
    1110        }
    1111    }
    1112
    1113    /**
    1114     * Ensures the specific preconditions of the said instruction.
    1115     */
    1116    @Override
    1117    public void visitGETSTATIC(final GETSTATIC o) {
    1118        // Field must be static: see Pass 3a.
    1119    }
    1120
    1121    /**
    1122     * Ensures the specific preconditions of the said instruction.
    1123     */
    1124    @Override
    1125    public void visitGOTO(final GOTO o) {
    1126        // nothing to do here.
    1127    }
    1128
    1129    /**
    1130     * Ensures the specific preconditions of the said instruction.
    1131     */
    1132    @Override
    1133    public void visitGOTO_W(final GOTO_W o) {
    1134        // nothing to do here.
    1135    }
    1136
    1137    /**
    1138     * Ensures the specific preconditions of the said instruction.
    1139     */
    1140    @Override
    1141    public void visitI2B(final I2B o) {
    1142        if (stack().peek() != Type.INT) {
    1143            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1144        }
    1145    }
    1146
    1147    /**
    1148     * Ensures the specific preconditions of the said instruction.
    1149     */
    1150    @Override
    1151    public void visitI2C(final I2C o) {
    1152        if (stack().peek() != Type.INT) {
    1153            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1154        }
    1155    }
    1156
    1157    /**
    1158     * Ensures the specific preconditions of the said instruction.
    1159     */
    1160    @Override
    1161    public void visitI2D(final I2D o) {
    1162        if (stack().peek() != Type.INT) {
    1163            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1164        }
    1165    }
    1166
    1167    /**
    1168     * Ensures the specific preconditions of the said instruction.
    1169     */
    1170    @Override
    1171    public void visitI2F(final I2F o) {
    1172        if (stack().peek() != Type.INT) {
    1173            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1174        }
    1175    }
    1176
    1177    /**
    1178     * Ensures the specific preconditions of the said instruction.
    1179     */
    1180    @Override
    1181    public void visitI2L(final I2L o) {
    1182        if (stack().peek() != Type.INT) {
    1183            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1184        }
    1185    }
    1186
    1187    /**
    1188     * Ensures the specific preconditions of the said instruction.
    1189     */
    1190    @Override
    1191    public void visitI2S(final I2S o) {
    1192        if (stack().peek() != Type.INT) {
    1193            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1194        }
    1195    }
    1196
    1197    /**
    1198     * Ensures the specific preconditions of the said instruction.
    1199     */
    1200    @Override
    1201    public void visitIADD(final IADD o) {
    1202        if (stack().peek() != Type.INT) {
    1203            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1204        }
    1205        if (stack().peek(1) != Type.INT) {
    1206            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1207        }
    1208    }
    1209
    1210    /**
    1211     * Ensures the specific preconditions of the said instruction.
    1212     */
    1213    @Override
    1214    public void visitIALOAD(final IALOAD o) {
    1215        indexOfInt(o, stack().peek());
    1216        if (stack().peek(1) == Type.NULL) {
    1217            return;
    1218        }
    1219        if (!(stack().peek(1) instanceof ArrayType)) {
    1220            constraintViolated(o, "Stack next-to-top must be of type int[] but is '" + stack().peek(1) + "'.");
    1221        }
    1222        final Type t = ((ArrayType) stack().peek(1)).getBasicType();
    1223        if (t != Type.INT) {
    1224            constraintViolated(o, "Stack next-to-top must be of type int[] but is '" + stack().peek(1) + "'.");
    1225        }
    1226    }
    1227
    1228    /**
    1229     * Ensures the specific preconditions of the said instruction.
    1230     */
    1231    @Override
    1232    public void visitIAND(final IAND o) {
    1233        if (stack().peek() != Type.INT) {
    1234            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1235        }
    1236        if (stack().peek(1) != Type.INT) {
    1237            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1238        }
    1239    }
    1240
    1241    /**
    1242     * Ensures the specific preconditions of the said instruction.
    1243     */
    1244    @Override
    1245    public void visitIASTORE(final IASTORE o) {
    1246        if (stack().peek() != Type.INT) {
    1247            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1248        }
    1249        indexOfInt(o, stack().peek(1));
    1250        if (stack().peek(2) == Type.NULL) {
    1251            return;
    1252        }
    1253        if (!(stack().peek(2) instanceof ArrayType)) {
    1254            constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '" + stack().peek(2) + "'.");
    1255        }
    1256        final Type t = ((ArrayType) stack().peek(2)).getBasicType();
    1257        if (t != Type.INT) {
    1258            constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '" + stack().peek(2) + "'.");
    1259        }
    1260    }
    1261
    1262    /**
    1263     * Ensures the specific preconditions of the said instruction.
    1264     */
    1265    @Override
    1266    public void visitICONST(final ICONST o) {
    1267        // nothing to do here.
    1268    }
    1269
    1270    /**
    1271     * Ensures the specific preconditions of the said instruction.
    1272     */
    1273    @Override
    1274    public void visitIDIV(final IDIV o) {
    1275        if (stack().peek() != Type.INT) {
    1276            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1277        }
    1278        if (stack().peek(1) != Type.INT) {
    1279            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1280        }
    1281    }
    1282
    1283    /**
    1284     * Ensures the specific preconditions of the said instruction.
    1285     */
    1286    @Override
    1287    public void visitIF_ACMPEQ(final IF_ACMPEQ o) {
    1288        if (!(stack().peek() instanceof ReferenceType)) {
    1289            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
    1290        }
    1291        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1292
    1293        if (!(stack().peek(1) instanceof ReferenceType)) {
    1294            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
    1295        }
    1296        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
    1297
    1298    }
    1299
    1300    /**
    1301     * Ensures the specific preconditions of the said instruction.
    1302     */
    1303    @Override
    1304    public void visitIF_ACMPNE(final IF_ACMPNE o) {
    1305        if (!(stack().peek() instanceof ReferenceType)) {
    1306            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
    1307            // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1308        }
    1309        if (!(stack().peek(1) instanceof ReferenceType)) {
    1310            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
    1311            // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
    1312        }
    1313    }
    1314
    1315    /**
    1316     * Ensures the specific preconditions of the said instruction.
    1317     */
    1318    @Override
    1319    public void visitIF_ICMPEQ(final IF_ICMPEQ o) {
    1320        if (stack().peek() != Type.INT) {
    1321            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1322        }
    1323        if (stack().peek(1) != Type.INT) {
    1324            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1325        }
    1326    }
    1327
    1328    /**
    1329     * Ensures the specific preconditions of the said instruction.
    1330     */
    1331    @Override
    1332    public void visitIF_ICMPGE(final IF_ICMPGE o) {
    1333        if (stack().peek() != Type.INT) {
    1334            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1335        }
    1336        if (stack().peek(1) != Type.INT) {
    1337            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1338        }
    1339    }
    1340
    1341    /**
    1342     * Ensures the specific preconditions of the said instruction.
    1343     */
    1344    @Override
    1345    public void visitIF_ICMPGT(final IF_ICMPGT o) {
    1346        if (stack().peek() != Type.INT) {
    1347            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1348        }
    1349        if (stack().peek(1) != Type.INT) {
    1350            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1351        }
    1352    }
    1353
    1354    /**
    1355     * Ensures the specific preconditions of the said instruction.
    1356     */
    1357    @Override
    1358    public void visitIF_ICMPLE(final IF_ICMPLE o) {
    1359        if (stack().peek() != Type.INT) {
    1360            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1361        }
    1362        if (stack().peek(1) != Type.INT) {
    1363            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1364        }
    1365    }
    1366
    1367    /**
    1368     * Ensures the specific preconditions of the said instruction.
    1369     */
    1370    @Override
    1371    public void visitIF_ICMPLT(final IF_ICMPLT o) {
    1372        if (stack().peek() != Type.INT) {
    1373            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1374        }
    1375        if (stack().peek(1) != Type.INT) {
    1376            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1377        }
    1378    }
    1379
    1380    /**
    1381     * Ensures the specific preconditions of the said instruction.
    1382     */
    1383    @Override
    1384    public void visitIF_ICMPNE(final IF_ICMPNE o) {
    1385        if (stack().peek() != Type.INT) {
    1386            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1387        }
    1388        if (stack().peek(1) != Type.INT) {
    1389            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1390        }
    1391    }
    1392
    1393    /**
    1394     * Ensures the specific preconditions of the said instruction.
    1395     */
    1396    @Override
    1397    public void visitIFEQ(final IFEQ o) {
    1398        if (stack().peek() != Type.INT) {
    1399            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1400        }
    1401    }
    1402
    1403    /**
    1404     * Ensures the specific preconditions of the said instruction.
    1405     */
    1406    @Override
    1407    public void visitIFGE(final IFGE o) {
    1408        if (stack().peek() != Type.INT) {
    1409            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1410        }
    1411    }
    1412
    1413    /**
    1414     * Ensures the specific preconditions of the said instruction.
    1415     */
    1416    @Override
    1417    public void visitIFGT(final IFGT o) {
    1418        if (stack().peek() != Type.INT) {
    1419            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1420        }
    1421    }
    1422
    1423    /**
    1424     * Ensures the specific preconditions of the said instruction.
    1425     */
    1426    @Override
    1427    public void visitIFLE(final IFLE o) {
    1428        if (stack().peek() != Type.INT) {
    1429            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1430        }
    1431    }
    1432
    1433    /**
    1434     * Ensures the specific preconditions of the said instruction.
    1435     */
    1436    @Override
    1437    public void visitIFLT(final IFLT o) {
    1438        if (stack().peek() != Type.INT) {
    1439            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1440        }
    1441    }
    1442
    1443    /**
    1444     * Ensures the specific preconditions of the said instruction.
    1445     */
    1446    @Override
    1447    public void visitIFNE(final IFNE o) {
    1448        if (stack().peek() != Type.INT) {
    1449            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1450        }
    1451    }
    1452
    1453    /**
    1454     * Ensures the specific preconditions of the said instruction.
    1455     */
    1456    @Override
    1457    public void visitIFNONNULL(final IFNONNULL o) {
    1458        if (!(stack().peek() instanceof ReferenceType)) {
    1459            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
    1460        }
    1461        referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
    1462    }
    1463
    1464    /**
    1465     * Ensures the specific preconditions of the said instruction.
    1466     */
    1467    @Override
    1468    public void visitIFNULL(final IFNULL o) {
    1469        if (!(stack().peek() instanceof ReferenceType)) {
    1470            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
    1471        }
    1472        referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
    1473    }
    1474
    1475    /**
    1476     * Ensures the specific preconditions of the said instruction.
    1477     */
    1478    @Override
    1479    public void visitIINC(final IINC o) {
    1480        // Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction.
    1481        if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
    1482            constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
    1483        }
    1484
    1485        indexOfInt(o, locals().get(o.getIndex()));
    1486    }
    1487
    1488    /**
    1489     * Ensures the specific preconditions of the said instruction.
    1490     */
    1491    @Override
    1492    public void visitILOAD(final ILOAD o) {
    1493        // All done by visitLocalVariableInstruction(), visitLoadInstruction()
    1494    }
    1495
    1496    /**
    1497     * Ensures the specific preconditions of the said instruction.
    1498     */
    1499    @Override
    1500    public void visitIMPDEP1(final IMPDEP1 o) {
    1501        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
    1502    }
    1503
    1504    /**
    1505     * Ensures the specific preconditions of the said instruction.
    1506     */
    1507    @Override
    1508    public void visitIMPDEP2(final IMPDEP2 o) {
    1509        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
    1510    }
    1511
    1512    /**
    1513     * Ensures the specific preconditions of the said instruction.
    1514     */
    1515    @Override
    1516    public void visitIMUL(final IMUL o) {
    1517        if (stack().peek() != Type.INT) {
    1518            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1519        }
    1520        if (stack().peek(1) != Type.INT) {
    1521            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1522        }
    1523    }
    1524
    1525    /**
    1526     * Ensures the specific preconditions of the said instruction.
    1527     */
    1528    @Override
    1529    public void visitINEG(final INEG o) {
    1530        if (stack().peek() != Type.INT) {
    1531            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1532        }
    1533    }
    1534
    1535    /**
    1536     * Ensures the specific preconditions of the said instruction.
    1537     */
    1538    @Override
    1539    public void visitINSTANCEOF(final INSTANCEOF o) {
    1540        // The objectref must be of type reference.
    1541        final Type objectref = stack().peek(0);
    1542        if (!(objectref instanceof ReferenceType)) {
    1543            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
    1544        }
    1545        // else{
    1546        // referenceTypeIsInitialized(o, (ReferenceType) objectref);
    1547        // }
    1548        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
    1549        // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
    1550        // pool item at the index must be a symbolic reference to a class, array, or interface type.
    1551        final Constant c = cpg.getConstant(o.getIndex());
    1552        if (!(c instanceof ConstantClass)) {
    1553            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
    1554        }
    1555    }
    1556
    1557    /**
    1558     * Ensures the specific preconditions of the said instruction.
    1559     *
    1560     * @since 6.0
    1561     */
    1562    @Override
    1563    public void visitINVOKEDYNAMIC(final INVOKEDYNAMIC o) {
    1564        throw new UnsupportedOperationException("INVOKEDYNAMIC instruction is not supported at this time");
    1565    }
    1566
    1567    /**
    1568     * Ensures the general preconditions of an InvokeInstruction instance.
    1569     */
    1570    @Override
    1571    public void visitInvokeInstruction(final InvokeInstruction o) {
    1572        // visitLoadClass(o) has been called before: Every FieldOrMethod
    1573        // implements LoadClass.
    1574        // visitCPInstruction(o) has been called before.
    1575        // TODO
    1576    }
    1577
    1578    /**
    1579     * Ensures the specific preconditions of the said instruction.
    1580     */
    1581    @Override
    1582    public void visitINVOKEINTERFACE(final INVOKEINTERFACE o) {
    1583        // Method is not native, otherwise pass 3 would not happen.
    1584
    1585        final int count = o.getCount();
    1586        if (count == 0) {
    1587            constraintViolated(o, "The 'count' argument must not be 0.");
    1588        }
    1589        // It is a ConstantInterfaceMethodref, Pass 3a made it sure.
    1590        // TODO: Do we want to do anything with it?
    1591        // ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex()));
    1592
    1593        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1594
    1595        final Type t = o.getType(cpg);
    1596        if (t instanceof ObjectType) {
    1597            final String name = ((ObjectType) t).getClassName();
    1598            final Verifier v = VerifierFactory.getVerifier(name);
    1599            final VerificationResult vr = v.doPass2();
    1600            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    1601                constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    1602            }
    1603        }
    1604
    1605        final Type[] argtypes = o.getArgumentTypes(cpg);
    1606        final int nargs = argtypes.length;
    1607
    1608        for (int i = nargs - 1; i >= 0; i--) {
    1609            final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
    1610            Type fromDesc = argtypes[i];
    1611            if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
    1612                fromDesc = Type.INT;
    1613            }
    1614            if (!fromStack.equals(fromDesc)) {
    1615                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
    1616                    final ReferenceType rFromStack = (ReferenceType) fromStack;
    1617                    // ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1618                    // TODO: This can only be checked when using Staerk-et-al's "set of object types"
    1619                    // instead of a "wider cast object type" created during verification.
    1620                    // if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ) {
    1621                    // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+
    1622                    // "' on the stack (which is not assignment compatible).");
    1623                    // }
    1624                    referenceTypeIsInitialized(o, rFromStack);
    1625                } else {
    1626                    constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
    1627                }
    1628            }
    1629        }
    1630
    1631        Type objref = stack().peek(nargs);
    1632        if (objref == Type.NULL) {
    1633            return;
    1634        }
    1635        if (!(objref instanceof ReferenceType)) {
    1636            constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
    1637        }
    1638        referenceTypeIsInitialized(o, (ReferenceType) objref);
    1639        if (!(objref instanceof ObjectType)) {
    1640            if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
    1641                constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
    1642            } else {
    1643                objref = GENERIC_ARRAY;
    1644            }
    1645        }
    1646
    1647        // String objref_classname = ((ObjectType) objref).getClassName();
    1648        // String theInterface = o.getClassName(cpg);
    1649        // TODO: This can only be checked if we're using Staerk-et-al's "set of object types"
    1650        // instead of "wider cast object types" generated during verification.
    1651        // if ( ! Repository.implementationOf(objref_classname, theInterface) ) {
    1652        // constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theInterface+"' as expected.");
    1653        // }
    1654
    1655        int counted_count = 1; // 1 for the objectref
    1656        for (int i = 0; i < nargs; i++) {
    1657            counted_count += argtypes[i].getSize();
    1658        }
    1659        if (count != counted_count) {
    1660            constraintViolated(o, "The 'count' argument should probably read '" + counted_count + "' but is '" + count + "'.");
    1661        }
    1662    }
    1663
    1664    /**
    1665     * Ensures the specific preconditions of the said instruction.
    1666     */
    1667    @Override
    1668    public void visitINVOKESPECIAL(final INVOKESPECIAL o) {
    1669        try {
    1670            // Don't init an object twice.
    1671            if (o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME) && !(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) {
    1672                constraintViolated(o,
    1673                    "Possibly initializing object twice."
    1674                        + " A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable"
    1675                        + " during a backwards branch, or in a local variable in code protected by an exception handler."
    1676                        + " Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details.");
    1677            }
    1678
    1679            // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1680
    1681            final Type t = o.getType(cpg);
    1682            if (t instanceof ObjectType) {
    1683                final String name = ((ObjectType) t).getClassName();
    1684                final Verifier v = VerifierFactory.getVerifier(name);
    1685                final VerificationResult vr = v.doPass2();
    1686                if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    1687                    constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    1688                }
    1689            }
    1690
    1691            final Type[] argtypes = o.getArgumentTypes(cpg);
    1692            final int nargs = argtypes.length;
    1693
    1694            for (int i = nargs - 1; i >= 0; i--) {
    1695                final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
    1696                Type fromDesc = argtypes[i];
    1697                if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
    1698                    fromDesc = Type.INT;
    1699                }
    1700                if (!fromStack.equals(fromDesc)) {
    1701                    if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
    1702                        final ReferenceType rFromStack = (ReferenceType) fromStack;
    1703                        final ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1704                        // TODO: This can only be checked using Staerk-et-al's "set of object types", not
    1705                        // using a "wider cast object type".
    1706                        if (!rFromStack.isAssignmentCompatibleWith(rFromDesc)) {
    1707                            constraintViolated(o,
    1708                                "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack (which is not assignment compatible).");
    1709                        }
    1710                        referenceTypeIsInitialized(o, rFromStack);
    1711                    } else {
    1712                        constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
    1713                    }
    1714                }
    1715            }
    1716
    1717            Type objref = stack().peek(nargs);
    1718            if (objref == Type.NULL) {
    1719                return;
    1720            }
    1721            if (!(objref instanceof ReferenceType)) {
    1722                constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
    1723            }
    1724            String objref_classname = null;
    1725            if (!o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME)) {
    1726                referenceTypeIsInitialized(o, (ReferenceType) objref);
    1727                if (!(objref instanceof ObjectType)) {
    1728                    if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
    1729                        constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
    1730                    } else {
    1731                        objref = GENERIC_ARRAY;
    1732                    }
    1733                }
    1734
    1735                objref_classname = ((ObjectType) objref).getClassName();
    1736            } else {
    1737                if (!(objref instanceof UninitializedObjectType)) {
    1738                    constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '" + objref
    1739                        + "'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address).");
    1740                }
    1741                objref_classname = ((UninitializedObjectType) objref).getInitialized().getClassName();
    1742            }
    1743
    1744            final String theClass = o.getClassName(cpg);
    1745            if (!Repository.instanceOf(objref_classname, theClass)) {
    1746                constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
    1747            }
    1748
    1749        } catch (final ClassNotFoundException e) {
    1750            // FIXME: maybe not the best way to handle this
    1751            throw new AssertionViolatedException("Missing class: " + e, e);
    1752        }
    1753    }
    1754
    1755    /**
    1756     * Ensures the specific preconditions of the said instruction.
    1757     */
    1758    @Override
    1759    public void visitINVOKESTATIC(final INVOKESTATIC o) {
    1760        try {
    1761            // Method is not native, otherwise pass 3 would not happen.
    1762
    1763            final Type t = o.getType(cpg);
    1764            if (t instanceof ObjectType) {
    1765                final String name = ((ObjectType) t).getClassName();
    1766                final Verifier v = VerifierFactory.getVerifier(name);
    1767                final VerificationResult vr = v.doPass2();
    1768                if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    1769                    constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    1770                }
    1771            }
    1772
    1773            final Type[] argtypes = o.getArgumentTypes(cpg);
    1774            final int nargs = argtypes.length;
    1775
    1776            for (int i = nargs - 1; i >= 0; i--) {
    1777                final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
    1778                Type fromDesc = argtypes[i];
    1779                if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
    1780                    fromDesc = Type.INT;
    1781                }
    1782                if (!fromStack.equals(fromDesc)) {
    1783                    if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
    1784                        final ReferenceType rFromStack = (ReferenceType) fromStack;
    1785                        final ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1786                        // TODO: This check can possibly only be done using Staerk-et-al's "set of object types"
    1787                        // instead of a "wider cast object type" created during verification.
    1788                        if (!rFromStack.isAssignmentCompatibleWith(rFromDesc)) {
    1789                            constraintViolated(o,
    1790                                "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack (which is not assignment compatible).");
    1791                        }
    1792                        referenceTypeIsInitialized(o, rFromStack);
    1793                    } else {
    1794                        constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
    1795                    }
    1796                }
    1797            }
    1798        } catch (final ClassNotFoundException e) {
    1799            // FIXME: maybe not the best way to handle this
    1800            throw new AssertionViolatedException("Missing class: " + e, e);
    1801        }
    1802    }
    1803
    1804    /**
    1805     * Ensures the specific preconditions of the said instruction.
    1806     */
    1807    @Override
    1808    public void visitINVOKEVIRTUAL(final INVOKEVIRTUAL o) {
    1809        try {
    1810            // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1811
    1812            final Type t = o.getType(cpg);
    1813            if (t instanceof ObjectType) {
    1814                final String name = ((ObjectType) t).getClassName();
    1815                final Verifier v = VerifierFactory.getVerifier(name);
    1816                final VerificationResult vr = v.doPass2();
    1817                if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    1818                    constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    1819                }
    1820            }
    1821
    1822            final Type[] argtypes = o.getArgumentTypes(cpg);
    1823            final int nargs = argtypes.length;
    1824
    1825            for (int i = nargs - 1; i >= 0; i--) {
    1826                final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
    1827                Type fromDesc = argtypes[i];
    1828                if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
    1829                    fromDesc = Type.INT;
    1830                }
    1831                if (!fromStack.equals(fromDesc)) {
    1832                    if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
    1833                        final ReferenceType rFromStack = (ReferenceType) fromStack;
    1834                        final ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1835                        // TODO: This can possibly only be checked when using Staerk-et-al's "set of object types" instead
    1836                        // of a single "wider cast object type" created during verification.
    1837                        if (!rFromStack.isAssignmentCompatibleWith(rFromDesc)) {
    1838                            constraintViolated(o,
    1839                                "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack (which is not assignment compatible).");
    1840                        }
    1841                        referenceTypeIsInitialized(o, rFromStack);
    1842                    } else {
    1843                        constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
    1844                    }
    1845                }
    1846            }
    1847
    1848            Type objref = stack().peek(nargs);
    1849            if (objref == Type.NULL) {
    1850                return;
    1851            }
    1852            if (!(objref instanceof ReferenceType)) {
    1853                constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
    1854            }
    1855            referenceTypeIsInitialized(o, (ReferenceType) objref);
    1856            if (!(objref instanceof ObjectType)) {
    1857                if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
    1858                    constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
    1859                } else {
    1860                    objref = GENERIC_ARRAY;
    1861                }
    1862            }
    1863
    1864            final String objref_classname = ((ObjectType) objref).getClassName();
    1865
    1866            final String theClass = o.getClassName(cpg);
    1867
    1868            if (!Repository.instanceOf(objref_classname, theClass)) {
    1869                constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
    1870            }
    1871        } catch (final ClassNotFoundException e) {
    1872            // FIXME: maybe not the best way to handle this
    1873            throw new AssertionViolatedException("Missing class: " + e, e);
    1874        }
    1875    }
    1876
    1877    /**
    1878     * Ensures the specific preconditions of the said instruction.
    1879     */
    1880    @Override
    1881    public void visitIOR(final IOR o) {
    1882        if (stack().peek() != Type.INT) {
    1883            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1884        }
    1885        if (stack().peek(1) != Type.INT) {
    1886            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1887        }
    1888    }
    1889
    1890    /**
    1891     * Ensures the specific preconditions of the said instruction.
    1892     */
    1893    @Override
    1894    public void visitIREM(final IREM o) {
    1895        if (stack().peek() != Type.INT) {
    1896            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1897        }
    1898        if (stack().peek(1) != Type.INT) {
    1899            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1900        }
    1901    }
    1902
    1903    /**
    1904     * Ensures the specific preconditions of the said instruction.
    1905     */
    1906    @Override
    1907    public void visitIRETURN(final IRETURN o) {
    1908        if (stack().peek() != Type.INT) {
    1909            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1910        }
    1911    }
    1912
    1913    /**
    1914     * Ensures the specific preconditions of the said instruction.
    1915     */
    1916    @Override
    1917    public void visitISHL(final ISHL o) {
    1918        if (stack().peek() != Type.INT) {
    1919            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1920        }
    1921        if (stack().peek(1) != Type.INT) {
    1922            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1923        }
    1924    }
    1925
    1926    /**
    1927     * Ensures the specific preconditions of the said instruction.
    1928     */
    1929    @Override
    1930    public void visitISHR(final ISHR o) {
    1931        if (stack().peek() != Type.INT) {
    1932            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1933        }
    1934        if (stack().peek(1) != Type.INT) {
    1935            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1936        }
    1937    }
    1938
    1939    /**
    1940     * Ensures the specific preconditions of the said instruction.
    1941     */
    1942    @Override
    1943    public void visitISTORE(final ISTORE o) {
    1944        // visitStoreInstruction(StoreInstruction) is called before.
    1945
    1946        // Nothing else needs to be done here.
    1947    }
    1948
    1949    /**
    1950     * Ensures the specific preconditions of the said instruction.
    1951     */
    1952    @Override
    1953    public void visitISUB(final ISUB o) {
    1954        if (stack().peek() != Type.INT) {
    1955            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1956        }
    1957        if (stack().peek(1) != Type.INT) {
    1958            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1959        }
    1960    }
    1961
    1962    /**
    1963     * Ensures the specific preconditions of the said instruction.
    1964     */
    1965    @Override
    1966    public void visitIUSHR(final IUSHR o) {
    1967        if (stack().peek() != Type.INT) {
    1968            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1969        }
    1970        if (stack().peek(1) != Type.INT) {
    1971            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1972        }
    1973    }
    1974
    1975    /**
    1976     * Ensures the specific preconditions of the said instruction.
    1977     */
    1978    @Override
    1979    public void visitIXOR(final IXOR o) {
    1980        if (stack().peek() != Type.INT) {
    1981            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    1982        }
    1983        if (stack().peek(1) != Type.INT) {
    1984            constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
    1985        }
    1986    }
    1987
    1988    /**
    1989     * Ensures the specific preconditions of the said instruction.
    1990     */
    1991    @Override
    1992    public void visitJSR(final JSR o) {
    1993        // nothing to do here.
    1994    }
    1995
    1996    /**
    1997     * Ensures the specific preconditions of the said instruction.
    1998     */
    1999    @Override
    2000    public void visitJSR_W(final JSR_W o) {
    2001        // nothing to do here.
    2002    }
    2003
    2004    /**
    2005     * Ensures the specific preconditions of the said instruction.
    2006     */
    2007    @Override
    2008    public void visitL2D(final L2D o) {
    2009        if (stack().peek() != Type.LONG) {
    2010            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2011        }
    2012    }
    2013
    2014    /**
    2015     * Ensures the specific preconditions of the said instruction.
    2016     */
    2017    @Override
    2018    public void visitL2F(final L2F o) {
    2019        if (stack().peek() != Type.LONG) {
    2020            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2021        }
    2022    }
    2023
    2024    /**
    2025     * Ensures the specific preconditions of the said instruction.
    2026     */
    2027    @Override
    2028    public void visitL2I(final L2I o) {
    2029        if (stack().peek() != Type.LONG) {
    2030            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2031        }
    2032    }
    2033
    2034    /**
    2035     * Ensures the specific preconditions of the said instruction.
    2036     */
    2037    @Override
    2038    public void visitLADD(final LADD o) {
    2039        if (stack().peek() != Type.LONG) {
    2040            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2041        }
    2042        if (stack().peek(1) != Type.LONG) {
    2043            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2044        }
    2045    }
    2046
    2047    /**
    2048     * Ensures the specific preconditions of the said instruction.
    2049     */
    2050    @Override
    2051    public void visitLALOAD(final LALOAD o) {
    2052        indexOfInt(o, stack().peek());
    2053        if (stack().peek(1) == Type.NULL) {
    2054            return;
    2055        }
    2056        if (!(stack().peek(1) instanceof ArrayType)) {
    2057            constraintViolated(o, "Stack next-to-top must be of type long[] but is '" + stack().peek(1) + "'.");
    2058        }
    2059        final Type t = ((ArrayType) stack().peek(1)).getBasicType();
    2060        if (t != Type.LONG) {
    2061            constraintViolated(o, "Stack next-to-top must be of type long[] but is '" + stack().peek(1) + "'.");
    2062        }
    2063    }
    2064
    2065    /**
    2066     * Ensures the specific preconditions of the said instruction.
    2067     */
    2068    @Override
    2069    public void visitLAND(final LAND o) {
    2070        if (stack().peek() != Type.LONG) {
    2071            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2072        }
    2073        if (stack().peek(1) != Type.LONG) {
    2074            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2075        }
    2076    }
    2077
    2078    /**
    2079     * Ensures the specific preconditions of the said instruction.
    2080     */
    2081    @Override
    2082    public void visitLASTORE(final LASTORE o) {
    2083        if (stack().peek() != Type.LONG) {
    2084            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2085        }
    2086        indexOfInt(o, stack().peek(1));
    2087        if (stack().peek(2) == Type.NULL) {
    2088            return;
    2089        }
    2090        if (!(stack().peek(2) instanceof ArrayType)) {
    2091            constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '" + stack().peek(2) + "'.");
    2092        }
    2093        final Type t = ((ArrayType) stack().peek(2)).getBasicType();
    2094        if (t != Type.LONG) {
    2095            constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '" + stack().peek(2) + "'.");
    2096        }
    2097    }
    2098
    2099    /**
    2100     * Ensures the specific preconditions of the said instruction.
    2101     */
    2102    @Override
    2103    public void visitLCMP(final LCMP o) {
    2104        if (stack().peek() != Type.LONG) {
    2105            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2106        }
    2107        if (stack().peek(1) != Type.LONG) {
    2108            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2109        }
    2110    }
    2111
    2112    /**
    2113     * Ensures the specific preconditions of the said instruction.
    2114     */
    2115    @Override
    2116    public void visitLCONST(final LCONST o) {
    2117        // Nothing to do here.
    2118    }
    2119
    2120    /**
    2121     * Ensures the specific preconditions of the said instruction.
    2122     */
    2123    @Override
    2124    public void visitLDC(final LDC o) {
    2125        // visitCPInstruction is called first.
    2126
    2127        final Constant c = cpg.getConstant(o.getIndex());
    2128        if (!(c instanceof ConstantInteger || c instanceof ConstantFloat || c instanceof ConstantString || c instanceof ConstantClass)) {
    2129            constraintViolated(o,
    2130                "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String or a CONSTANT_Class, but is '" + c + "'.");
    2131        }
    2132    }
    2133
    2134    /**
    2135     * Ensures the specific preconditions of the said instruction.
    2136     */
    2137    public void visitLDC_W(final LDC_W o) {
    2138        // visitCPInstruction is called first.
    2139
    2140        final Constant c = cpg.getConstant(o.getIndex());
    2141        if (!(c instanceof ConstantInteger || c instanceof ConstantFloat || c instanceof ConstantString || c instanceof ConstantClass)) {
    2142            constraintViolated(o,
    2143                "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String or a CONSTANT_Class, but is '" + c + "'.");
    2144        }
    2145    }
    2146
    2147    /**
    2148     * Ensures the specific preconditions of the said instruction.
    2149     */
    2150    @Override
    2151    public void visitLDC2_W(final LDC2_W o) {
    2152        // visitCPInstruction is called first.
    2153
    2154        final Constant c = cpg.getConstant(o.getIndex());
    2155        if (!(c instanceof ConstantLong || c instanceof ConstantDouble)) {
    2156            constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '" + c + "'.");
    2157        }
    2158    }
    2159
    2160    /**
    2161     * Ensures the specific preconditions of the said instruction.
    2162     */
    2163    @Override
    2164    public void visitLDIV(final LDIV o) {
    2165        if (stack().peek() != Type.LONG) {
    2166            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2167        }
    2168        if (stack().peek(1) != Type.LONG) {
    2169            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2170        }
    2171    }
    2172
    2173    /**
    2174     * Ensures the specific preconditions of the said instruction.
    2175     */
    2176    @Override
    2177    public void visitLLOAD(final LLOAD o) {
    2178        // visitLoadInstruction(LoadInstruction) is called before.
    2179
    2180        // Nothing else needs to be done here.
    2181    }
    2182
    2183    /**
    2184     * Ensures the specific preconditions of the said instruction.
    2185     */
    2186    @Override
    2187    public void visitLMUL(final LMUL o) {
    2188        if (stack().peek() != Type.LONG) {
    2189            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2190        }
    2191        if (stack().peek(1) != Type.LONG) {
    2192            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2193        }
    2194    }
    2195
    2196    /**
    2197     * Ensures the specific preconditions of the said instruction.
    2198     */
    2199    @Override
    2200    public void visitLNEG(final LNEG o) {
    2201        if (stack().peek() != Type.LONG) {
    2202            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2203        }
    2204    }
    2205
    2206    /**
    2207     * Assures the generic preconditions of a LoadClass instance. The referenced class is loaded and pass2-verified.
    2208     */
    2209    @Override
    2210    public void visitLoadClass(final LoadClass o) {
    2211        final ObjectType t = o.getLoadClassType(cpg);
    2212        if (t != null) {// null means "no class is loaded"
    2213            final Verifier v = VerifierFactory.getVerifier(t.getClassName());
    2214            final VerificationResult vr = v.doPass2();
    2215            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
    2216                constraintViolated((Instruction) o,
    2217                    "Class '" + o.getLoadClassType(cpg).getClassName() + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
    2218            }
    2219        }
    2220    }
    2221
    2222    /**
    2223     * Assures the generic preconditions of a LoadInstruction instance.
    2224     */
    2225    @Override
    2226    public void visitLoadInstruction(final LoadInstruction o) {
    2227        // visitLocalVariableInstruction(o) is called before, because it is more generic.
    2228
    2229        // LOAD instructions must not read Type.UNKNOWN
    2230        if (locals().get(o.getIndex()) == Type.UNKNOWN) {
    2231            constraintViolated(o, "Read-Access on local variable " + o.getIndex() + " with unknown content.");
    2232        }
    2233
    2234        // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
    2235        // as a symbol for the higher halve at index N+1
    2236        // [suppose some instruction put an int at N+1--- our double at N is defective]
    2237        if (o.getType(cpg).getSize() == 2 && locals().get(o.getIndex() + 1) != Type.UNKNOWN) {
    2238            constraintViolated(o,
    2239                "Reading a two-locals value from local variables " + o.getIndex() + " and " + (o.getIndex() + 1) + " where the latter one is destroyed.");
    2240        }
    2241
    2242        // LOAD instructions must read the correct type.
    2243        if (!(o instanceof ALOAD)) {
    2244            if (locals().get(o.getIndex()) != o.getType(cpg)) {
    2245                constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
    2246                    + "'; Instruction type: '" + o.getType(cpg) + "'.");
    2247            }
    2248        } else if (!(locals().get(o.getIndex()) instanceof ReferenceType)) {
    2249            constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
    2250                + "'; Instruction expects a ReferenceType.");
    2251        }
    2252        // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
    2253        // referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
    2254
    2255        // LOAD instructions must have enough free stack slots.
    2256        if (stack().maxStack() - stack().slotsUsed() < o.getType(cpg).getSize()) {
    2257            constraintViolated(o, "Not enough free stack slots to load a '" + o.getType(cpg) + "' onto the OperandStack.");
    2258        }
    2259    }
    2260
    2261    /**
    2262     * Assures the generic preconditions of a LocalVariableInstruction instance. That is, the index of the local variable
    2263     * must be valid.
    2264     */
    2265    @Override
    2266    public void visitLocalVariableInstruction(final LocalVariableInstruction o) {
    2267        if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
    2268            constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
    2269        }
    2270    }
    2271
    2272    /**
    2273     * Ensures the specific preconditions of the said instruction.
    2274     */
    2275    @Override
    2276    public void visitLOOKUPSWITCH(final LOOKUPSWITCH o) {
    2277        if (stack().peek() != Type.INT) {
    2278            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2279        }
    2280        // See also pass 3a.
    2281    }
    2282
    2283    /**
    2284     * Ensures the specific preconditions of the said instruction.
    2285     */
    2286    @Override
    2287    public void visitLOR(final LOR o) {
    2288        if (stack().peek() != Type.LONG) {
    2289            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2290        }
    2291        if (stack().peek(1) != Type.LONG) {
    2292            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2293        }
    2294    }
    2295
    2296    /**
    2297     * Ensures the specific preconditions of the said instruction.
    2298     */
    2299    @Override
    2300    public void visitLREM(final LREM o) {
    2301        if (stack().peek() != Type.LONG) {
    2302            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2303        }
    2304        if (stack().peek(1) != Type.LONG) {
    2305            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2306        }
    2307    }
    2308
    2309    /**
    2310     * Ensures the specific preconditions of the said instruction.
    2311     */
    2312    @Override
    2313    public void visitLRETURN(final LRETURN o) {
    2314        if (stack().peek() != Type.LONG) {
    2315            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2316        }
    2317    }
    2318
    2319    /**
    2320     * Ensures the specific preconditions of the said instruction.
    2321     */
    2322    @Override
    2323    public void visitLSHL(final LSHL o) {
    2324        if (stack().peek() != Type.INT) {
    2325            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2326        }
    2327        if (stack().peek(1) != Type.LONG) {
    2328            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2329        }
    2330    }
    2331
    2332    /**
    2333     * Ensures the specific preconditions of the said instruction.
    2334     */
    2335    @Override
    2336    public void visitLSHR(final LSHR o) {
    2337        if (stack().peek() != Type.INT) {
    2338            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2339        }
    2340        if (stack().peek(1) != Type.LONG) {
    2341            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2342        }
    2343    }
    2344
    2345    /**
    2346     * Ensures the specific preconditions of the said instruction.
    2347     */
    2348    @Override
    2349    public void visitLSTORE(final LSTORE o) {
    2350        // visitStoreInstruction(StoreInstruction) is called before.
    2351
    2352        // Nothing else needs to be done here.
    2353    }
    2354
    2355    /**
    2356     * Ensures the specific preconditions of the said instruction.
    2357     */
    2358    @Override
    2359    public void visitLSUB(final LSUB o) {
    2360        if (stack().peek() != Type.LONG) {
    2361            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2362        }
    2363        if (stack().peek(1) != Type.LONG) {
    2364            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2365        }
    2366    }
    2367
    2368    /**
    2369     * Ensures the specific preconditions of the said instruction.
    2370     */
    2371    @Override
    2372    public void visitLUSHR(final LUSHR o) {
    2373        if (stack().peek() != Type.INT) {
    2374            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2375        }
    2376        if (stack().peek(1) != Type.LONG) {
    2377            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2378        }
    2379    }
    2380
    2381    /**
    2382     * Ensures the specific preconditions of the said instruction.
    2383     */
    2384    @Override
    2385    public void visitLXOR(final LXOR o) {
    2386        if (stack().peek() != Type.LONG) {
    2387            constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
    2388        }
    2389        if (stack().peek(1) != Type.LONG) {
    2390            constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
    2391        }
    2392    }
    2393
    2394    /**
    2395     * Ensures the specific preconditions of the said instruction.
    2396     */
    2397    @Override
    2398    public void visitMONITORENTER(final MONITORENTER o) {
    2399        if (!(stack().peek() instanceof ReferenceType)) {
    2400            constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
    2401        }
    2402        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    2403    }
    2404
    2405    /**
    2406     * Ensures the specific preconditions of the said instruction.
    2407     */
    2408    @Override
    2409    public void visitMONITOREXIT(final MONITOREXIT o) {
    2410        if (!(stack().peek() instanceof ReferenceType)) {
    2411            constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
    2412        }
    2413        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    2414    }
    2415
    2416    /**
    2417     * Ensures the specific preconditions of the said instruction.
    2418     */
    2419    @Override
    2420    public void visitMULTIANEWARRAY(final MULTIANEWARRAY o) {
    2421        final int dimensions = o.getDimensions();
    2422        // Dimensions argument is okay: see Pass 3a.
    2423        for (int i = 0; i < dimensions; i++) {
    2424            if (stack().peek(i) != Type.INT) {
    2425                constraintViolated(o, "The '" + dimensions + "' upper stack types should be 'int' but aren't.");
    2426            }
    2427        }
    2428        // The runtime constant pool item at that index must be a symbolic reference to a class,
    2429        // array, or interface type. See Pass 3a.
    2430    }
    2431
    2432    /**
    2433     * Ensures the specific preconditions of the said instruction.
    2434     */
    2435    @Override
    2436    public void visitNEW(final NEW o) {
    2437        // visitCPInstruction(CPInstruction) has been called before.
    2438        // visitLoadClass(LoadClass) has been called before.
    2439
    2440        final Type t = o.getType(cpg);
    2441        if (!(t instanceof ReferenceType)) {
    2442            throw new AssertionViolatedException("NEW.getType() returning a non-reference type?!");
    2443        }
    2444        if (!(t instanceof ObjectType)) {
    2445            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + t + "'.");
    2446        }
    2447        final ObjectType obj = (ObjectType) t;
    2448
    2449        // e.g.: Don't instantiate interfaces
    2450        try {
    2451            if (!obj.referencesClassExact()) {
    2452                constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'.");
    2453            }
    2454        } catch (final ClassNotFoundException e) {
    2455            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'." + " which threw " + e);
    2456        }
    2457    }
    2458
    2459    /**
    2460     * Ensures the specific preconditions of the said instruction.
    2461     */
    2462    @Override
    2463    public void visitNEWARRAY(final NEWARRAY o) {
    2464        if (stack().peek() != Type.INT) {
    2465            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2466        }
    2467    }
    2468
    2469    /**
    2470     * Ensures the specific preconditions of the said instruction.
    2471     */
    2472    @Override
    2473    public void visitNOP(final NOP o) {
    2474        // nothing is to be done here.
    2475    }
    2476
    2477    /**
    2478     * Ensures the specific preconditions of the said instruction.
    2479     */
    2480    @Override
    2481    public void visitPOP(final POP o) {
    2482        if (stack().peek().getSize() != 1) {
    2483            constraintViolated(o, "Stack top size should be 1 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
    2484        }
    2485    }
    2486
    2487    /**
    2488     * Ensures the specific preconditions of the said instruction.
    2489     */
    2490    @Override
    2491    public void visitPOP2(final POP2 o) {
    2492        if (stack().peek().getSize() != 2) {
    2493            constraintViolated(o, "Stack top size should be 2 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
    2494        }
    2495    }
    2496
    2497    /**
    2498     * Ensures the specific preconditions of the said instruction.
    2499     */
    2500    @Override
    2501    public void visitPUTFIELD(final PUTFIELD o) {
    2502        try {
    2503
    2504            final Type objectref = stack().peek(1);
    2505            if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
    2506                constraintViolated(o, "Stack next-to-top should be an object reference that's not an array reference, but is '" + objectref + "'.");
    2507            }
    2508
    2509            final String field_name = o.getFieldName(cpg);
    2510
    2511            final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
    2512            final Field[] fields = jc.getFields();
    2513            Field f = null;
    2514            for (final Field field : fields) {
    2515                if (field.getName().equals(field_name)) {
    2516                    final Type fType = Type.getType(field.getSignature());
    2517                    final Type oType = o.getType(cpg);
    2518                    /*
    2519                     * TODO: Check if assignment compatibility is sufficient. What does Sun do?
    2520                     */
    2521                    if (fType.equals(oType)) {
    2522                        f = field;
    2523                        break;
    2524                    }
    2525                }
    2526            }
    2527            if (f == null) {
    2528                throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
    2529            }
    2530
    2531            final Type value = stack().peek();
    2532            final Type t = Type.getType(f.getSignature());
    2533            Type shouldbe = t;
    2534            if (shouldbe == Type.BOOLEAN || shouldbe == Type.BYTE || shouldbe == Type.CHAR || shouldbe == Type.SHORT) {
    2535                shouldbe = Type.INT;
    2536            }
    2537            if (t instanceof ReferenceType) {
    2538                ReferenceType rvalue = null;
    2539                if (value instanceof ReferenceType) {
    2540                    rvalue = (ReferenceType) value;
    2541                    referenceTypeIsInitialized(o, rvalue);
    2542                } else {
    2543                    constraintViolated(o, "The stack top type '" + value + "' is not of a reference type as expected.");
    2544                }
    2545                // TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
    2546                // using "wider cast object types" created during verification.
    2547                // Comment it out if you encounter problems. See also the analogon at visitPUTSTATIC.
    2548                if (!rvalue.isAssignmentCompatibleWith(shouldbe)) {
    2549                    constraintViolated(o, "The stack top type '" + value + "' is not assignment compatible with '" + shouldbe + "'.");
    2550                }
    2551            } else if (shouldbe != value) {
    2552                constraintViolated(o, "The stack top type '" + value + "' is not of type '" + shouldbe + "' as expected.");
    2553            }
    2554
    2555            if (f.isProtected()) {
    2556                final ObjectType classtype = getObjectType(o);
    2557                final ObjectType curr = ObjectType.getInstance(mg.getClassName());
    2558
    2559                if (classtype.equals(curr) || curr.subclassOf(classtype)) {
    2560                    final Type tp = stack().peek(1);
    2561                    if (tp == Type.NULL) {
    2562                        return;
    2563                    }
    2564                    if (!(tp instanceof ObjectType)) {
    2565                        constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + tp + "'.");
    2566                    }
    2567                    final ObjectType objreftype = (ObjectType) tp;
    2568                    if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
    2569                        constraintViolated(o,
    2570                            "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or"
    2571                                + " a superclass of the current class. However, the referenced object type '" + stack().peek()
    2572                                + "' is not the current class or a subclass of the current class.");
    2573                    }
    2574                }
    2575            }
    2576
    2577            // TODO: Could go into Pass 3a.
    2578            if (f.isStatic()) {
    2579                constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
    2580            }
    2581
    2582        } catch (final ClassNotFoundException e) {
    2583            // FIXME: maybe not the best way to handle this
    2584            throw new AssertionViolatedException("Missing class: " + e, e);
    2585        }
    2586    }
    2587
    2588    /**
    2589     * Ensures the specific preconditions of the said instruction.
    2590     */
    2591    @Override
    2592    public void visitPUTSTATIC(final PUTSTATIC o) {
    2593        try {
    2594            final String field_name = o.getFieldName(cpg);
    2595            final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
    2596            final Field[] fields = jc.getFields();
    2597            Field f = null;
    2598            for (final Field field : fields) {
    2599                if (field.getName().equals(field_name)) {
    2600                    final Type fType = Type.getType(field.getSignature());
    2601                    final Type oType = o.getType(cpg);
    2602                    /*
    2603                     * TODO: Check if assignment compatibility is sufficient. What does Sun do?
    2604                     */
    2605                    if (fType.equals(oType)) {
    2606                        f = field;
    2607                        break;
    2608                    }
    2609                }
    2610            }
    2611            if (f == null) {
    2612                throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
    2613            }
    2614            final Type value = stack().peek();
    2615            final Type t = Type.getType(f.getSignature());
    2616            Type shouldbe = t;
    2617            if (shouldbe == Type.BOOLEAN || shouldbe == Type.BYTE || shouldbe == Type.CHAR || shouldbe == Type.SHORT) {
    2618                shouldbe = Type.INT;
    2619            }
    2620            if (t instanceof ReferenceType) {
    2621                ReferenceType rvalue = null;
    2622                if (value instanceof ReferenceType) {
    2623                    rvalue = (ReferenceType) value;
    2624                    referenceTypeIsInitialized(o, rvalue);
    2625                } else {
    2626                    constraintViolated(o, "The stack top type '" + value + "' is not of a reference type as expected.");
    2627                }
    2628                // TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
    2629                // using "wider cast object types" created during verification.
    2630                // Comment it out if you encounter problems. See also the analogon at visitPUTFIELD.
    2631                if (!rvalue.isAssignmentCompatibleWith(shouldbe)) {
    2632                    constraintViolated(o, "The stack top type '" + value + "' is not assignment compatible with '" + shouldbe + "'.");
    2633                }
    2634            } else if (shouldbe != value) {
    2635                constraintViolated(o, "The stack top type '" + value + "' is not of type '" + shouldbe + "' as expected.");
    2636            }
    2637
    2638        } catch (final ClassNotFoundException e) {
    2639            // FIXME: maybe not the best way to handle this
    2640            throw new AssertionViolatedException("Missing class: " + e, e);
    2641        }
    2642    }
    2643
    2644    /**
    2645     * Ensures the specific preconditions of the said instruction.
    2646     */
    2647    @Override
    2648    public void visitRET(final RET o) {
    2649        if (!(locals().get(o.getIndex()) instanceof ReturnaddressType)) {
    2650            constraintViolated(o, "Expecting a ReturnaddressType in local variable " + o.getIndex() + ".");
    2651        }
    2652        if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET) {
    2653            throw new AssertionViolatedException("RET expecting a target!");
    2654        }
    2655        // Other constraints such as non-allowed overlapping subroutines are enforced
    2656        // while building the Subroutines data structure.
    2657    }
    2658
    2659    /**
    2660     * Ensures the specific preconditions of the said instruction.
    2661     */
    2662    @Override
    2663    public void visitRETURN(final RETURN o) {
    2664        if (mg.getName().equals(Const.CONSTRUCTOR_NAME) && Frame.getThis() != null && !mg.getClassName().equals(Type.OBJECT.getClassName())) {
    2665            constraintViolated(o, "Leaving a constructor that itself did not call a constructor.");
    2666        }
    2667    }
    2668
    2669    /**
    2670     * Assures the generic preconditions of a ReturnInstruction instance.
    2671     */
    2672    @Override
    2673    public void visitReturnInstruction(final ReturnInstruction o) {
    2674        Type methodType = mg.getType();
    2675        if (methodType == Type.BOOLEAN || methodType == Type.BYTE || methodType == Type.SHORT || methodType == Type.CHAR) {
    2676            methodType = Type.INT;
    2677        }
    2678
    2679        if (o instanceof RETURN) {
    2680            if (methodType == Type.VOID) {
    2681                return;
    2682            }
    2683            constraintViolated(o, "RETURN instruction in non-void method.");
    2684        }
    2685        if (o instanceof ARETURN) {
    2686            if (methodType == Type.VOID) {
    2687                constraintViolated(o, "ARETURN instruction in void method.");
    2688            }
    2689            if (stack().peek() == Type.NULL) {
    2690                return;
    2691            }
    2692            if (!(stack().peek() instanceof ReferenceType)) {
    2693                constraintViolated(o, "Reference type expected on top of stack, but is: '" + stack().peek() + "'.");
    2694            }
    2695            referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
    2696            // ReferenceType objectref = (ReferenceType) (stack().peek());
    2697            // TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
    2698            // "wider cast object type" created during verification.
    2699            // if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ) {
    2700            // constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+
    2701            // "' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
    2702            // }
    2703        } else if (!methodType.equals(stack().peek())) {
    2704            constraintViolated(o, "Current method has return type of '" + mg.getType() + "' expecting a '" + methodType
    2705                + "' on top of the stack. But stack top is a '" + stack().peek() + "'.");
    2706        }
    2707    }
    2708
    2709    /**
    2710     * Ensures the specific preconditions of the said instruction.
    2711     */
    2712    @Override
    2713    public void visitSALOAD(final SALOAD o) {
    2714        indexOfInt(o, stack().peek());
    2715        if (stack().peek(1) == Type.NULL) {
    2716            return;
    2717        }
    2718        if (!(stack().peek(1) instanceof ArrayType)) {
    2719            constraintViolated(o, "Stack next-to-top must be of type short[] but is '" + stack().peek(1) + "'.");
    2720        }
    2721        final Type t = ((ArrayType) stack().peek(1)).getBasicType();
    2722        if (t != Type.SHORT) {
    2723            constraintViolated(o, "Stack next-to-top must be of type short[] but is '" + stack().peek(1) + "'.");
    2724        }
    2725    }
    2726
    2727    /**
    2728     * Ensures the specific preconditions of the said instruction.
    2729     */
    2730    @Override
    2731    public void visitSASTORE(final SASTORE o) {
    2732        if (stack().peek() != Type.INT) {
    2733            constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
    2734        }
    2735        indexOfInt(o, stack().peek(1));
    2736        if (stack().peek(2) == Type.NULL) {
    2737            return;
    2738        }
    2739        if (!(stack().peek(2) instanceof ArrayType)) {
    2740            constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '" + stack().peek(2) + "'.");
    2741        }
    2742        final Type t = ((ArrayType) stack().peek(2)).getBasicType();
    2743        if (t != Type.SHORT) {
    2744            constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '" + stack().peek(2) + "'.");
    2745        }
    2746    }
    2747
    2748    /**
    2749     * Ensures the specific preconditions of the said instruction.
    2750     */
    2751    @Override
    2752    public void visitSIPUSH(final SIPUSH o) {
    2753        // nothing to do here. Generic visitXXX() methods did the trick before.
    2754    }
    2755
    2756    /**
    2757     * Ensures the general preconditions of a StackConsumer instance.
    2758     */
    2759    @Override
    2760    public void visitStackConsumer(final StackConsumer o) {
    2761        _visitStackAccessor((Instruction) o);
    2762    }
    2763
    2764    /**
    2765     * Ensures the general preconditions of a StackInstruction instance.
    2766     */
    2767    @Override
    2768    public void visitStackInstruction(final StackInstruction o) {
    2769        _visitStackAccessor(o);
    2770    }
    2771
    2772    /**
    2773     * Ensures the general preconditions of a StackProducer instance.
    2774     */
    2775    @Override
    2776    public void visitStackProducer(final StackProducer o) {
    2777        _visitStackAccessor((Instruction) o);
    2778    }
    2779
    2780    /**
    2781     * Assures the generic preconditions of a StoreInstruction instance.
    2782     */
    2783    @Override
    2784    public void visitStoreInstruction(final StoreInstruction o) {
    2785        // visitLocalVariableInstruction(o) is called before, because it is more generic.
    2786
    2787        if (stack().isEmpty()) { // Don't bother about 1 or 2 stack slots used. This check is implicitly done below while type checking.
    2788            constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
    2789        }
    2790
    2791        if (!(o instanceof ASTORE)) {
    2792            if (!(stack().peek() == o.getType(cpg))) {// the other xSTORE types are singletons in BCEL.
    2793                constraintViolated(o,
    2794                    "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek() + "'; Instruction type: '" + o.getType(cpg) + "'.");
    2795            }
    2796        } else { // we deal with ASTORE
    2797            final Type stacktop = stack().peek();
    2798            if (!(stacktop instanceof ReferenceType) && !(stacktop instanceof ReturnaddressType)) {
    2799                constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek()
    2800                    + "'; Instruction expects a ReferenceType or a ReturnadressType.");
    2801            }
    2802            // if (stacktop instanceof ReferenceType) {
    2803            // referenceTypeIsInitialized(o, (ReferenceType) stacktop);
    2804            // }
    2805        }
    2806    }
    2807
    2808    /**
    2809     * Ensures the specific preconditions of the said instruction.
    2810     */
    2811    @Override
    2812    public void visitSWAP(final SWAP o) {
    2813        if (stack().peek().getSize() != 1) {
    2814            constraintViolated(o, "The value at the stack top is not of size '1', but of size '" + stack().peek().getSize() + "'.");
    2815        }
    2816        if (stack().peek(1).getSize() != 1) {
    2817            constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '" + stack().peek(1).getSize() + "'.");
    2818        }
    2819    }
    2820
    2821    /**
    2822     * Ensures the specific preconditions of the said instruction.
    2823     */
    2824    @Override
    2825    public void visitTABLESWITCH(final TABLESWITCH o) {
    2826        indexOfInt(o, stack().peek());
    2827        // See Pass 3a.
    2828    }
    2829
    2830}