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