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