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