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