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