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