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