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