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