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