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