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