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