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