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