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