InstConstraintVisitor


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