001/*
002 * Licensed to the Apache Software Foundation (ASF) under one
003 * or more contributor license agreements.  See the NOTICE file
004 * distributed with this work for additional information
005 * regarding copyright ownership.  The ASF licenses this file
006 * to you under the Apache License, Version 2.0 (the
007 * "License"); you may not use this file except in compliance
008 * with the License.  You may obtain a copy of the License at
009 *
010 *   https://www.apache.org/licenses/LICENSE-2.0
011 *
012 * Unless required by applicable law or agreed to in writing,
013 * software distributed under the License is distributed on an
014 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
015 * KIND, either express or implied.  See the License for the
016 * specific language governing permissions and limitations
017 * under the License.
018 */
019package org.apache.bcel.verifier.structurals;
020
021import org.apache.bcel.Const;
022import org.apache.bcel.classfile.Constant;
023import org.apache.bcel.classfile.ConstantClass;
024import org.apache.bcel.classfile.ConstantDouble;
025import org.apache.bcel.classfile.ConstantDynamic;
026import org.apache.bcel.classfile.ConstantFloat;
027import org.apache.bcel.classfile.ConstantInteger;
028import org.apache.bcel.classfile.ConstantLong;
029import org.apache.bcel.classfile.ConstantString;
030import org.apache.bcel.generic.AALOAD;
031import org.apache.bcel.generic.AASTORE;
032import org.apache.bcel.generic.ACONST_NULL;
033import org.apache.bcel.generic.ALOAD;
034import org.apache.bcel.generic.ANEWARRAY;
035import org.apache.bcel.generic.ARETURN;
036import org.apache.bcel.generic.ARRAYLENGTH;
037import org.apache.bcel.generic.ASTORE;
038import org.apache.bcel.generic.ATHROW;
039import org.apache.bcel.generic.ArrayType;
040import org.apache.bcel.generic.BALOAD;
041import org.apache.bcel.generic.BASTORE;
042import org.apache.bcel.generic.BIPUSH;
043import org.apache.bcel.generic.CALOAD;
044import org.apache.bcel.generic.CASTORE;
045import org.apache.bcel.generic.CHECKCAST;
046import org.apache.bcel.generic.ConstantPoolGen;
047import org.apache.bcel.generic.D2F;
048import org.apache.bcel.generic.D2I;
049import org.apache.bcel.generic.D2L;
050import org.apache.bcel.generic.DADD;
051import org.apache.bcel.generic.DALOAD;
052import org.apache.bcel.generic.DASTORE;
053import org.apache.bcel.generic.DCMPG;
054import org.apache.bcel.generic.DCMPL;
055import org.apache.bcel.generic.DCONST;
056import org.apache.bcel.generic.DDIV;
057import org.apache.bcel.generic.DLOAD;
058import org.apache.bcel.generic.DMUL;
059import org.apache.bcel.generic.DNEG;
060import org.apache.bcel.generic.DREM;
061import org.apache.bcel.generic.DRETURN;
062import org.apache.bcel.generic.DSTORE;
063import org.apache.bcel.generic.DSUB;
064import org.apache.bcel.generic.DUP;
065import org.apache.bcel.generic.DUP2;
066import org.apache.bcel.generic.DUP2_X1;
067import org.apache.bcel.generic.DUP2_X2;
068import org.apache.bcel.generic.DUP_X1;
069import org.apache.bcel.generic.DUP_X2;
070import org.apache.bcel.generic.EmptyVisitor;
071import org.apache.bcel.generic.F2D;
072import org.apache.bcel.generic.F2I;
073import org.apache.bcel.generic.F2L;
074import org.apache.bcel.generic.FADD;
075import org.apache.bcel.generic.FALOAD;
076import org.apache.bcel.generic.FASTORE;
077import org.apache.bcel.generic.FCMPG;
078import org.apache.bcel.generic.FCMPL;
079import org.apache.bcel.generic.FCONST;
080import org.apache.bcel.generic.FDIV;
081import org.apache.bcel.generic.FLOAD;
082import org.apache.bcel.generic.FMUL;
083import org.apache.bcel.generic.FNEG;
084import org.apache.bcel.generic.FREM;
085import org.apache.bcel.generic.FRETURN;
086import org.apache.bcel.generic.FSTORE;
087import org.apache.bcel.generic.FSUB;
088import org.apache.bcel.generic.GETFIELD;
089import org.apache.bcel.generic.GETSTATIC;
090import org.apache.bcel.generic.GOTO;
091import org.apache.bcel.generic.GOTO_W;
092import org.apache.bcel.generic.I2B;
093import org.apache.bcel.generic.I2C;
094import org.apache.bcel.generic.I2D;
095import org.apache.bcel.generic.I2F;
096import org.apache.bcel.generic.I2L;
097import org.apache.bcel.generic.I2S;
098import org.apache.bcel.generic.IADD;
099import org.apache.bcel.generic.IALOAD;
100import org.apache.bcel.generic.IAND;
101import org.apache.bcel.generic.IASTORE;
102import org.apache.bcel.generic.ICONST;
103import org.apache.bcel.generic.IDIV;
104import org.apache.bcel.generic.IFEQ;
105import org.apache.bcel.generic.IFGE;
106import org.apache.bcel.generic.IFGT;
107import org.apache.bcel.generic.IFLE;
108import org.apache.bcel.generic.IFLT;
109import org.apache.bcel.generic.IFNE;
110import org.apache.bcel.generic.IFNONNULL;
111import org.apache.bcel.generic.IFNULL;
112import org.apache.bcel.generic.IF_ACMPEQ;
113import org.apache.bcel.generic.IF_ACMPNE;
114import org.apache.bcel.generic.IF_ICMPEQ;
115import org.apache.bcel.generic.IF_ICMPGE;
116import org.apache.bcel.generic.IF_ICMPGT;
117import org.apache.bcel.generic.IF_ICMPLE;
118import org.apache.bcel.generic.IF_ICMPLT;
119import org.apache.bcel.generic.IF_ICMPNE;
120import org.apache.bcel.generic.IINC;
121import org.apache.bcel.generic.ILOAD;
122import org.apache.bcel.generic.IMUL;
123import org.apache.bcel.generic.INEG;
124import org.apache.bcel.generic.INSTANCEOF;
125import org.apache.bcel.generic.INVOKEDYNAMIC;
126import org.apache.bcel.generic.INVOKEINTERFACE;
127import org.apache.bcel.generic.INVOKESPECIAL;
128import org.apache.bcel.generic.INVOKESTATIC;
129import org.apache.bcel.generic.INVOKEVIRTUAL;
130import org.apache.bcel.generic.IOR;
131import org.apache.bcel.generic.IREM;
132import org.apache.bcel.generic.IRETURN;
133import org.apache.bcel.generic.ISHL;
134import org.apache.bcel.generic.ISHR;
135import org.apache.bcel.generic.ISTORE;
136import org.apache.bcel.generic.ISUB;
137import org.apache.bcel.generic.IUSHR;
138import org.apache.bcel.generic.IXOR;
139import org.apache.bcel.generic.InvokeInstruction;
140import org.apache.bcel.generic.JSR;
141import org.apache.bcel.generic.JSR_W;
142import org.apache.bcel.generic.L2D;
143import org.apache.bcel.generic.L2F;
144import org.apache.bcel.generic.L2I;
145import org.apache.bcel.generic.LADD;
146import org.apache.bcel.generic.LALOAD;
147import org.apache.bcel.generic.LAND;
148import org.apache.bcel.generic.LASTORE;
149import org.apache.bcel.generic.LCMP;
150import org.apache.bcel.generic.LCONST;
151import org.apache.bcel.generic.LDC;
152import org.apache.bcel.generic.LDC2_W;
153import org.apache.bcel.generic.LDC_W;
154import org.apache.bcel.generic.LDIV;
155import org.apache.bcel.generic.LLOAD;
156import org.apache.bcel.generic.LMUL;
157import org.apache.bcel.generic.LNEG;
158import org.apache.bcel.generic.LOOKUPSWITCH;
159import org.apache.bcel.generic.LOR;
160import org.apache.bcel.generic.LREM;
161import org.apache.bcel.generic.LRETURN;
162import org.apache.bcel.generic.LSHL;
163import org.apache.bcel.generic.LSHR;
164import org.apache.bcel.generic.LSTORE;
165import org.apache.bcel.generic.LSUB;
166import org.apache.bcel.generic.LUSHR;
167import org.apache.bcel.generic.LXOR;
168import org.apache.bcel.generic.MONITORENTER;
169import org.apache.bcel.generic.MONITOREXIT;
170import org.apache.bcel.generic.MULTIANEWARRAY;
171import org.apache.bcel.generic.NEW;
172import org.apache.bcel.generic.NEWARRAY;
173import org.apache.bcel.generic.NOP;
174import org.apache.bcel.generic.ObjectType;
175import org.apache.bcel.generic.POP;
176import org.apache.bcel.generic.POP2;
177import org.apache.bcel.generic.PUTFIELD;
178import org.apache.bcel.generic.PUTSTATIC;
179import org.apache.bcel.generic.RET;
180import org.apache.bcel.generic.RETURN;
181import org.apache.bcel.generic.ReturnaddressType;
182import org.apache.bcel.generic.SALOAD;
183import org.apache.bcel.generic.SASTORE;
184import org.apache.bcel.generic.SIPUSH;
185import org.apache.bcel.generic.SWAP;
186import org.apache.bcel.generic.TABLESWITCH;
187import org.apache.bcel.generic.Type;
188
189/**
190 * This Visitor class may be used for a type-based Java Virtual Machine simulation.
191 *
192 * <p>
193 * It does not check for correct types on the OperandStack or in the LocalVariables; nor does it check their sizes are
194 * sufficiently big. Thus, to use this Visitor for bytecode verifying, you have to make sure externally that the type
195 * constraints of the Java Virtual Machine instructions are satisfied. An InstConstraintVisitor may be used for this.
196 * Anyway, this Visitor does not mandate it. For example, when you visitIADD(IADD o), then there are two stack slots
197 * popped and one stack slot containing a Type.INT is pushed (where you could also pop only one slot if you know there
198 * are two Type.INT on top of the stack). Monitor-specific behavior is not simulated.
199 * </p>
200 *
201 * <strong>Conventions:</strong>
202 *
203 * <p>
204 * Type.VOID will never be pushed onto the stack. Type.DOUBLE and Type.LONG that would normally take up two stack slots
205 * (like Double_HIGH and Double_LOW) are represented by a simple single Type.DOUBLE or Type.LONG object on the stack
206 * here.
207 * </p>
208 *
209 * <p>
210 * If a two-slot type is stored into a local variable, the next variable is given the type Type.UNKNOWN.
211 * </p>
212 *
213 * @see #visitDSTORE(DSTORE o)
214 * @see InstConstraintVisitor
215 */
216public class ExecutionVisitor extends EmptyVisitor {
217
218    /**
219     * The executionframe we're operating on.
220     */
221    private Frame frame;
222
223    /**
224     * The ConstantPoolGen we're working with.
225     *
226     * @see #setConstantPoolGen(ConstantPoolGen)
227     */
228    private ConstantPoolGen cpg;
229
230    /**
231     * Constructs a new instance of this class.
232     */
233    public ExecutionVisitor() {
234    }
235
236    /**
237     * The LocalVariables from the current Frame we're operating on.
238     *
239     * @see #setFrame(Frame)
240     */
241    private LocalVariables locals() {
242        return frame.getLocals();
243    }
244
245    /**
246     * Sets the ConstantPoolGen needed for symbolic execution.
247     *
248     * @param cpg The constant pool generator.
249     */
250    public void setConstantPoolGen(final ConstantPoolGen cpg) { // TODO could be package-protected?
251        this.cpg = cpg;
252    }
253
254    /**
255     * Sets the execution frame. Configure the constant pool before using this visitor.
256     *
257     * @param f The frame.
258     * @see #setConstantPoolGen(ConstantPoolGen)
259     */
260    public void setFrame(final Frame f) { // TODO could be package-protected?
261        this.frame = f;
262    }
263
264    /**
265     * The OperandStack from the current Frame we're operating on.
266     *
267     * @see #setFrame(Frame)
268     */
269    private OperandStack stack() {
270        return frame.getStack();
271    }
272
273    /// ** Symbolically executes the corresponding Java Virtual Machine instruction. */
274    // public void visitWIDE(WIDE o) {
275    // The WIDE instruction is modeled as a flag
276    // of the embedded instructions in BCEL.
277    // Therefore BCEL checks for possible errors
278    // when parsing in the .class file: We don't
279    // have even the possibility to care for WIDE
280    // here.
281    // }
282
283    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
284    @Override
285    public void visitAALOAD(final AALOAD o) {
286        stack().pop(); // pop the index int
287        // System.out.print(stack().peek());
288        final Type t = stack().pop(); // Pop Array type
289        if (t == Type.NULL) {
290            stack().push(Type.NULL);
291        } else {
292            final ArrayType at = (ArrayType) t;
293            stack().push(at.getElementType());
294        }
295    }
296
297    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
298    @Override
299    public void visitAASTORE(final AASTORE o) {
300        stack().pop(3);
301    }
302
303    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
304    @Override
305    public void visitACONST_NULL(final ACONST_NULL o) {
306        stack().push(Type.NULL);
307    }
308
309    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
310    @Override
311    public void visitALOAD(final ALOAD o) {
312        stack().push(locals().get(o.getIndex()));
313    }
314
315    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
316    @Override
317    public void visitANEWARRAY(final ANEWARRAY o) {
318        stack().pop(); // count
319        stack().push(new ArrayType(o.getType(cpg), 1));
320    }
321
322    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
323    @Override
324    public void visitARETURN(final ARETURN o) {
325        stack().pop();
326    }
327
328    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
329    @Override
330    public void visitARRAYLENGTH(final ARRAYLENGTH o) {
331        stack().pop();
332        stack().push(Type.INT);
333    }
334
335    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
336    @Override
337    public void visitASTORE(final ASTORE o) {
338        locals().set(o.getIndex(), stack().pop());
339        // System.err.println("TODO-DEBUG: set LV '"+o.getIndex()+"' to '"+locals().get(o.getIndex())+"'.");
340    }
341
342    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
343    @Override
344    public void visitATHROW(final ATHROW o) {
345        final Type t = stack().pop();
346        stack().clear();
347        if (t.equals(Type.NULL)) {
348            stack().push(Type.getType("Ljava/lang/NullPointerException;"));
349        } else {
350            stack().push(t);
351        }
352    }
353
354    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
355    @Override
356    public void visitBALOAD(final BALOAD o) {
357        stack().pop(2);
358        stack().push(Type.INT);
359    }
360
361    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
362    @Override
363    public void visitBASTORE(final BASTORE o) {
364        stack().pop(3);
365    }
366
367    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
368    @Override
369    public void visitBIPUSH(final BIPUSH o) {
370        stack().push(Type.INT);
371    }
372
373    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
374    @Override
375    public void visitCALOAD(final CALOAD o) {
376        stack().pop(2);
377        stack().push(Type.INT);
378    }
379
380    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
381    @Override
382    public void visitCASTORE(final CASTORE o) {
383        stack().pop(3);
384    }
385
386    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
387    @Override
388    public void visitCHECKCAST(final CHECKCAST o) {
389        // It's possibly wrong to do so, but SUN's
390        // ByteCode verifier seems to do (only) this, too.
391        // TODO: One could use a sophisticated analysis here to check
392        // if a type cannot possibly be cated to another and by
393        // so doing predict the ClassCastException at run-time.
394        stack().pop();
395        stack().push(o.getType(cpg));
396    }
397
398    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
399    @Override
400    public void visitD2F(final D2F o) {
401        stack().pop();
402        stack().push(Type.FLOAT);
403    }
404
405    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
406    @Override
407    public void visitD2I(final D2I o) {
408        stack().pop();
409        stack().push(Type.INT);
410    }
411
412    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
413    @Override
414    public void visitD2L(final D2L o) {
415        stack().pop();
416        stack().push(Type.LONG);
417    }
418
419    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
420    @Override
421    public void visitDADD(final DADD o) {
422        stack().pop(2);
423        stack().push(Type.DOUBLE);
424    }
425
426    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
427    @Override
428    public void visitDALOAD(final DALOAD o) {
429        stack().pop(2);
430        stack().push(Type.DOUBLE);
431    }
432
433    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
434    @Override
435    public void visitDASTORE(final DASTORE o) {
436        stack().pop(3);
437    }
438
439    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
440    @Override
441    public void visitDCMPG(final DCMPG o) {
442        stack().pop(2);
443        stack().push(Type.INT);
444    }
445
446    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
447    @Override
448    public void visitDCMPL(final DCMPL o) {
449        stack().pop(2);
450        stack().push(Type.INT);
451    }
452
453    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
454    @Override
455    public void visitDCONST(final DCONST o) {
456        stack().push(Type.DOUBLE);
457    }
458
459    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
460    @Override
461    public void visitDDIV(final DDIV o) {
462        stack().pop(2);
463        stack().push(Type.DOUBLE);
464    }
465
466    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
467    @Override
468    public void visitDLOAD(final DLOAD o) {
469        stack().push(Type.DOUBLE);
470    }
471
472    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
473    @Override
474    public void visitDMUL(final DMUL o) {
475        stack().pop(2);
476        stack().push(Type.DOUBLE);
477    }
478
479    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
480    @Override
481    public void visitDNEG(final DNEG o) {
482        stack().pop();
483        stack().push(Type.DOUBLE);
484    }
485
486    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
487    @Override
488    public void visitDREM(final DREM o) {
489        stack().pop(2);
490        stack().push(Type.DOUBLE);
491    }
492
493    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
494    @Override
495    public void visitDRETURN(final DRETURN o) {
496        stack().pop();
497    }
498
499    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
500    @Override
501    public void visitDSTORE(final DSTORE o) {
502        locals().set(o.getIndex(), stack().pop());
503        locals().set(o.getIndex() + 1, Type.UNKNOWN);
504    }
505
506    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
507    @Override
508    public void visitDSUB(final DSUB o) {
509        stack().pop(2);
510        stack().push(Type.DOUBLE);
511    }
512
513    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
514    @Override
515    public void visitDUP(final DUP o) {
516        final Type t = stack().pop();
517        stack().push(t);
518        stack().push(t);
519    }
520
521    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
522    @Override
523    public void visitDUP_X1(final DUP_X1 o) {
524        final Type w1 = stack().pop();
525        final Type w2 = stack().pop();
526        stack().push(w1);
527        stack().push(w2);
528        stack().push(w1);
529    }
530
531    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
532    @Override
533    public void visitDUP_X2(final DUP_X2 o) {
534        final Type w1 = stack().pop();
535        final Type w2 = stack().pop();
536        if (w2.getSize() == 2) {
537            stack().push(w1);
538        } else {
539            final Type w3 = stack().pop();
540            stack().push(w1);
541            stack().push(w3);
542        }
543        stack().push(w2);
544        stack().push(w1);
545    }
546
547    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
548    @Override
549    public void visitDUP2(final DUP2 o) {
550        final Type t = stack().pop();
551        if (t.getSize() == 2) {
552            stack().push(t);
553        } else { // t.getSize() is 1
554            final Type u = stack().pop();
555            stack().push(u);
556            stack().push(t);
557            stack().push(u);
558        }
559        stack().push(t);
560    }
561
562    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
563    @Override
564    public void visitDUP2_X1(final DUP2_X1 o) {
565        final Type t = stack().pop();
566        if (t.getSize() == 2) {
567            final Type u = stack().pop();
568            stack().push(t);
569            stack().push(u);
570        } else { // t.getSize() is1
571            final Type u = stack().pop();
572            final Type v = stack().pop();
573            stack().push(u);
574            stack().push(t);
575            stack().push(v);
576            stack().push(u);
577        }
578        stack().push(t);
579    }
580
581    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
582    @Override
583    public void visitDUP2_X2(final DUP2_X2 o) {
584        final Type t = stack().pop();
585        if (t.getSize() == 2) {
586            final Type u = stack().pop();
587            if (u.getSize() == 2) {
588                stack().push(t);
589            } else {
590                final Type v = stack().pop();
591                stack().push(t);
592                stack().push(v);
593            }
594            stack().push(u);
595        } else { // t.getSize() is 1
596            final Type u = stack().pop();
597            final Type v = stack().pop();
598            if (v.getSize() == 2) {
599                stack().push(u);
600                stack().push(t);
601            } else {
602                final Type w = stack().pop();
603                stack().push(u);
604                stack().push(t);
605                stack().push(w);
606            }
607            stack().push(v);
608            stack().push(u);
609        }
610        stack().push(t);
611    }
612
613    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
614    @Override
615    public void visitF2D(final F2D o) {
616        stack().pop();
617        stack().push(Type.DOUBLE);
618    }
619
620    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
621    @Override
622    public void visitF2I(final F2I o) {
623        stack().pop();
624        stack().push(Type.INT);
625    }
626
627    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
628    @Override
629    public void visitF2L(final F2L o) {
630        stack().pop();
631        stack().push(Type.LONG);
632    }
633
634    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
635    @Override
636    public void visitFADD(final FADD o) {
637        stack().pop(2);
638        stack().push(Type.FLOAT);
639    }
640
641    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
642    @Override
643    public void visitFALOAD(final FALOAD o) {
644        stack().pop(2);
645        stack().push(Type.FLOAT);
646    }
647
648    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
649    @Override
650    public void visitFASTORE(final FASTORE o) {
651        stack().pop(3);
652    }
653
654    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
655    @Override
656    public void visitFCMPG(final FCMPG o) {
657        stack().pop(2);
658        stack().push(Type.INT);
659    }
660
661    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
662    @Override
663    public void visitFCMPL(final FCMPL o) {
664        stack().pop(2);
665        stack().push(Type.INT);
666    }
667
668    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
669    @Override
670    public void visitFCONST(final FCONST o) {
671        stack().push(Type.FLOAT);
672    }
673
674    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
675    @Override
676    public void visitFDIV(final FDIV o) {
677        stack().pop(2);
678        stack().push(Type.FLOAT);
679    }
680
681    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
682    @Override
683    public void visitFLOAD(final FLOAD o) {
684        stack().push(Type.FLOAT);
685    }
686
687    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
688    @Override
689    public void visitFMUL(final FMUL o) {
690        stack().pop(2);
691        stack().push(Type.FLOAT);
692    }
693
694    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
695    @Override
696    public void visitFNEG(final FNEG o) {
697        stack().pop();
698        stack().push(Type.FLOAT);
699    }
700
701    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
702    @Override
703    public void visitFREM(final FREM o) {
704        stack().pop(2);
705        stack().push(Type.FLOAT);
706    }
707
708    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
709    @Override
710    public void visitFRETURN(final FRETURN o) {
711        stack().pop();
712    }
713
714    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
715    @Override
716    public void visitFSTORE(final FSTORE o) {
717        locals().set(o.getIndex(), stack().pop());
718    }
719
720    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
721    @Override
722    public void visitFSUB(final FSUB o) {
723        stack().pop(2);
724        stack().push(Type.FLOAT);
725    }
726
727    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
728    @Override
729    public void visitGETFIELD(final GETFIELD o) {
730        stack().pop();
731        Type t = o.getFieldType(cpg);
732        if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
733            t = Type.INT;
734        }
735        stack().push(t);
736    }
737
738    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
739    @Override
740    public void visitGETSTATIC(final GETSTATIC o) {
741        Type t = o.getFieldType(cpg);
742        if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
743            t = Type.INT;
744        }
745        stack().push(t);
746    }
747
748    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
749    @Override
750    public void visitGOTO(final GOTO o) {
751        // no stack changes.
752    }
753
754    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
755    @Override
756    public void visitGOTO_W(final GOTO_W o) {
757        // no stack changes.
758    }
759
760    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
761    @Override
762    public void visitI2B(final I2B o) {
763        stack().pop();
764        stack().push(Type.INT);
765    }
766
767    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
768    @Override
769    public void visitI2C(final I2C o) {
770        stack().pop();
771        stack().push(Type.INT);
772    }
773
774    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
775    @Override
776    public void visitI2D(final I2D o) {
777        stack().pop();
778        stack().push(Type.DOUBLE);
779    }
780
781    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
782    @Override
783    public void visitI2F(final I2F o) {
784        stack().pop();
785        stack().push(Type.FLOAT);
786    }
787
788    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
789    @Override
790    public void visitI2L(final I2L o) {
791        stack().pop();
792        stack().push(Type.LONG);
793    }
794
795    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
796    @Override
797    public void visitI2S(final I2S o) {
798        stack().pop();
799        stack().push(Type.INT);
800    }
801
802    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
803    @Override
804    public void visitIADD(final IADD o) {
805        stack().pop(2);
806        stack().push(Type.INT);
807    }
808
809    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
810    @Override
811    public void visitIALOAD(final IALOAD o) {
812        stack().pop(2);
813        stack().push(Type.INT);
814    }
815
816    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
817    @Override
818    public void visitIAND(final IAND o) {
819        stack().pop(2);
820        stack().push(Type.INT);
821    }
822
823    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
824    @Override
825    public void visitIASTORE(final IASTORE o) {
826        stack().pop(3);
827    }
828
829    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
830    @Override
831    public void visitICONST(final ICONST o) {
832        stack().push(Type.INT);
833    }
834
835    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
836    @Override
837    public void visitIDIV(final IDIV o) {
838        stack().pop(2);
839        stack().push(Type.INT);
840    }
841
842    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
843    @Override
844    public void visitIF_ACMPEQ(final IF_ACMPEQ o) {
845        stack().pop(2);
846    }
847
848    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
849    @Override
850    public void visitIF_ACMPNE(final IF_ACMPNE o) {
851        stack().pop(2);
852    }
853
854    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
855    @Override
856    public void visitIF_ICMPEQ(final IF_ICMPEQ o) {
857        stack().pop(2);
858    }
859
860    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
861    @Override
862    public void visitIF_ICMPGE(final IF_ICMPGE o) {
863        stack().pop(2);
864    }
865
866    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
867    @Override
868    public void visitIF_ICMPGT(final IF_ICMPGT o) {
869        stack().pop(2);
870    }
871
872    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
873    @Override
874    public void visitIF_ICMPLE(final IF_ICMPLE o) {
875        stack().pop(2);
876    }
877
878    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
879    @Override
880    public void visitIF_ICMPLT(final IF_ICMPLT o) {
881        stack().pop(2);
882    }
883
884    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
885    @Override
886    public void visitIF_ICMPNE(final IF_ICMPNE o) {
887        stack().pop(2);
888    }
889
890    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
891    @Override
892    public void visitIFEQ(final IFEQ o) {
893        stack().pop();
894    }
895
896    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
897    @Override
898    public void visitIFGE(final IFGE o) {
899        stack().pop();
900    }
901
902    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
903    @Override
904    public void visitIFGT(final IFGT o) {
905        stack().pop();
906    }
907
908    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
909    @Override
910    public void visitIFLE(final IFLE o) {
911        stack().pop();
912    }
913
914    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
915    @Override
916    public void visitIFLT(final IFLT o) {
917        stack().pop();
918    }
919
920    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
921    @Override
922    public void visitIFNE(final IFNE o) {
923        stack().pop();
924    }
925
926    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
927    @Override
928    public void visitIFNONNULL(final IFNONNULL o) {
929        stack().pop();
930    }
931
932    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
933    @Override
934    public void visitIFNULL(final IFNULL o) {
935        stack().pop();
936    }
937
938    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
939    @Override
940    public void visitIINC(final IINC o) {
941        // stack is not changed.
942    }
943
944    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
945    @Override
946    public void visitILOAD(final ILOAD o) {
947        stack().push(Type.INT);
948    }
949
950    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
951    @Override
952    public void visitIMUL(final IMUL o) {
953        stack().pop(2);
954        stack().push(Type.INT);
955    }
956
957    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
958    @Override
959    public void visitINEG(final INEG o) {
960        stack().pop();
961        stack().push(Type.INT);
962    }
963
964    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
965    @Override
966    public void visitINSTANCEOF(final INSTANCEOF o) {
967        stack().pop();
968        stack().push(Type.INT);
969    }
970
971    private void visitInvokedInternals(final InvokeInstruction o) {
972        stack().pop(o.getArgumentTypes(cpg).length);
973        // We are sure the invoked method will xRETURN eventually
974        // We simulate xRETURNs functionality here because we
975        // don't really "jump into" and simulate the invoked
976        // method.
977        if (o.getReturnType(cpg) != Type.VOID) {
978            Type t = o.getReturnType(cpg);
979            if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
980                t = Type.INT;
981            }
982            stack().push(t);
983        }
984    }
985
986    /**
987     * Symbolically executes the corresponding Java Virtual Machine instruction.
988     *
989     * @since 6.0
990     */
991    @Override
992    public void visitINVOKEDYNAMIC(final INVOKEDYNAMIC o) {
993        visitInvokedInternals(o);
994    }
995
996    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
997    @Override
998    public void visitINVOKEINTERFACE(final INVOKEINTERFACE o) {
999        stack().pop(); // objectref
1000        stack().pop(o.getArgumentTypes(cpg).length);
1001        // We are sure the invoked method will xRETURN eventually
1002        // We simulate xRETURNs functionality here because we
1003        // don't really "jump into" and simulate the invoked
1004        // method.
1005        if (o.getReturnType(cpg) != Type.VOID) {
1006            Type t = o.getReturnType(cpg);
1007            if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
1008                t = Type.INT;
1009            }
1010            stack().push(t);
1011        }
1012    }
1013
1014    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1015    @Override
1016    public void visitINVOKESPECIAL(final INVOKESPECIAL o) {
1017        if (o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME)) {
1018            final UninitializedObjectType t = (UninitializedObjectType) stack().peek(o.getArgumentTypes(cpg).length);
1019            if (t == Frame.getThis()) {
1020                Frame.setThis(null);
1021            }
1022            stack().initializeObject(t);
1023            locals().initializeObject(t);
1024        }
1025        stack().pop(); // objectref
1026        stack().pop(o.getArgumentTypes(cpg).length);
1027        // We are sure the invoked method will xRETURN eventually
1028        // We simulate xRETURNs functionality here because we
1029        // don't really "jump into" and simulate the invoked
1030        // method.
1031        if (o.getReturnType(cpg) != Type.VOID) {
1032            Type t = o.getReturnType(cpg);
1033            if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
1034                t = Type.INT;
1035            }
1036            stack().push(t);
1037        }
1038    }
1039
1040    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1041    @Override
1042    public void visitINVOKESTATIC(final INVOKESTATIC o) {
1043        visitInvokedInternals(o);
1044    }
1045
1046    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1047    @Override
1048    public void visitINVOKEVIRTUAL(final INVOKEVIRTUAL o) {
1049        stack().pop(); // objectref
1050        stack().pop(o.getArgumentTypes(cpg).length);
1051        // We are sure the invoked method will xRETURN eventually
1052        // We simulate xRETURNs functionality here because we
1053        // don't really "jump into" and simulate the invoked
1054        // method.
1055        if (o.getReturnType(cpg) != Type.VOID) {
1056            Type t = o.getReturnType(cpg);
1057            if (t.equals(Type.BOOLEAN) || t.equals(Type.CHAR) || t.equals(Type.BYTE) || t.equals(Type.SHORT)) {
1058                t = Type.INT;
1059            }
1060            stack().push(t);
1061        }
1062    }
1063
1064    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1065    @Override
1066    public void visitIOR(final IOR o) {
1067        stack().pop(2);
1068        stack().push(Type.INT);
1069    }
1070
1071    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1072    @Override
1073    public void visitIREM(final IREM o) {
1074        stack().pop(2);
1075        stack().push(Type.INT);
1076    }
1077
1078    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1079    @Override
1080    public void visitIRETURN(final IRETURN o) {
1081        stack().pop();
1082    }
1083
1084    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1085    @Override
1086    public void visitISHL(final ISHL o) {
1087        stack().pop(2);
1088        stack().push(Type.INT);
1089    }
1090
1091    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1092    @Override
1093    public void visitISHR(final ISHR o) {
1094        stack().pop(2);
1095        stack().push(Type.INT);
1096    }
1097
1098    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1099    @Override
1100    public void visitISTORE(final ISTORE o) {
1101        locals().set(o.getIndex(), stack().pop());
1102    }
1103
1104    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1105    @Override
1106    public void visitISUB(final ISUB o) {
1107        stack().pop(2);
1108        stack().push(Type.INT);
1109    }
1110
1111    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1112    @Override
1113    public void visitIUSHR(final IUSHR o) {
1114        stack().pop(2);
1115        stack().push(Type.INT);
1116    }
1117
1118    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1119    @Override
1120    public void visitIXOR(final IXOR o) {
1121        stack().pop(2);
1122        stack().push(Type.INT);
1123    }
1124
1125    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1126    @Override
1127    public void visitJSR(final JSR o) {
1128        stack().push(new ReturnaddressType(o.physicalSuccessor()));
1129//System.err.println("TODO-----------:"+o.physicalSuccessor());
1130    }
1131
1132    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1133    @Override
1134    public void visitJSR_W(final JSR_W o) {
1135        stack().push(new ReturnaddressType(o.physicalSuccessor()));
1136    }
1137
1138    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1139    @Override
1140    public void visitL2D(final L2D o) {
1141        stack().pop();
1142        stack().push(Type.DOUBLE);
1143    }
1144
1145    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1146    @Override
1147    public void visitL2F(final L2F o) {
1148        stack().pop();
1149        stack().push(Type.FLOAT);
1150    }
1151
1152    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1153    @Override
1154    public void visitL2I(final L2I o) {
1155        stack().pop();
1156        stack().push(Type.INT);
1157    }
1158
1159    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1160    @Override
1161    public void visitLADD(final LADD o) {
1162        stack().pop(2);
1163        stack().push(Type.LONG);
1164    }
1165
1166    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1167    @Override
1168    public void visitLALOAD(final LALOAD o) {
1169        stack().pop(2);
1170        stack().push(Type.LONG);
1171    }
1172
1173    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1174    @Override
1175    public void visitLAND(final LAND o) {
1176        stack().pop(2);
1177        stack().push(Type.LONG);
1178    }
1179
1180    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1181    @Override
1182    public void visitLASTORE(final LASTORE o) {
1183        stack().pop(3);
1184    }
1185
1186    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1187    @Override
1188    public void visitLCMP(final LCMP o) {
1189        stack().pop(2);
1190        stack().push(Type.INT);
1191    }
1192
1193    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1194    @Override
1195    public void visitLCONST(final LCONST o) {
1196        stack().push(Type.LONG);
1197    }
1198
1199    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1200    @Override
1201    public void visitLDC(final LDC o) {
1202        final Constant c = cpg.getConstant(o.getIndex());
1203        if (c instanceof ConstantInteger) {
1204            stack().push(Type.INT);
1205        }
1206        if (c instanceof ConstantFloat) {
1207            stack().push(Type.FLOAT);
1208        }
1209        if (c instanceof ConstantString) {
1210            stack().push(Type.STRING);
1211        }
1212        if (c instanceof ConstantClass) {
1213            stack().push(Type.CLASS);
1214        }
1215        if (c instanceof ConstantDynamic) {
1216            stack().push(Type.OBJECT);
1217        }
1218    }
1219
1220    /**
1221     * Symbolically executes the corresponding Java Virtual Machine instruction.
1222     *
1223     * @param o The instruction.
1224     */
1225    public void visitLDC_W(final LDC_W o) {
1226        final Constant c = cpg.getConstant(o.getIndex());
1227        if (c instanceof ConstantInteger) {
1228            stack().push(Type.INT);
1229        }
1230        if (c instanceof ConstantFloat) {
1231            stack().push(Type.FLOAT);
1232        }
1233        if (c instanceof ConstantString) {
1234            stack().push(Type.STRING);
1235        }
1236        if (c instanceof ConstantClass) {
1237            stack().push(Type.CLASS);
1238        }
1239    }
1240
1241    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1242    @Override
1243    public void visitLDC2_W(final LDC2_W o) {
1244        final Constant c = cpg.getConstant(o.getIndex());
1245        if (c instanceof ConstantLong) {
1246            stack().push(Type.LONG);
1247        }
1248        if (c instanceof ConstantDouble) {
1249            stack().push(Type.DOUBLE);
1250        }
1251    }
1252
1253    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1254    @Override
1255    public void visitLDIV(final LDIV o) {
1256        stack().pop(2);
1257        stack().push(Type.LONG);
1258    }
1259
1260    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1261    @Override
1262    public void visitLLOAD(final LLOAD o) {
1263        stack().push(locals().get(o.getIndex()));
1264    }
1265
1266    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1267    @Override
1268    public void visitLMUL(final LMUL o) {
1269        stack().pop(2);
1270        stack().push(Type.LONG);
1271    }
1272
1273    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1274    @Override
1275    public void visitLNEG(final LNEG o) {
1276        stack().pop();
1277        stack().push(Type.LONG);
1278    }
1279
1280    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1281    @Override
1282    public void visitLOOKUPSWITCH(final LOOKUPSWITCH o) {
1283        stack().pop(); // key
1284    }
1285
1286    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1287    @Override
1288    public void visitLOR(final LOR o) {
1289        stack().pop(2);
1290        stack().push(Type.LONG);
1291    }
1292
1293    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1294    @Override
1295    public void visitLREM(final LREM o) {
1296        stack().pop(2);
1297        stack().push(Type.LONG);
1298    }
1299
1300    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1301    @Override
1302    public void visitLRETURN(final LRETURN o) {
1303        stack().pop();
1304    }
1305
1306    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1307    @Override
1308    public void visitLSHL(final LSHL o) {
1309        stack().pop(2);
1310        stack().push(Type.LONG);
1311    }
1312
1313    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1314    @Override
1315    public void visitLSHR(final LSHR o) {
1316        stack().pop(2);
1317        stack().push(Type.LONG);
1318    }
1319
1320    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1321    @Override
1322    public void visitLSTORE(final LSTORE o) {
1323        locals().set(o.getIndex(), stack().pop());
1324        locals().set(o.getIndex() + 1, Type.UNKNOWN);
1325    }
1326
1327    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1328    @Override
1329    public void visitLSUB(final LSUB o) {
1330        stack().pop(2);
1331        stack().push(Type.LONG);
1332    }
1333
1334    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1335    @Override
1336    public void visitLUSHR(final LUSHR o) {
1337        stack().pop(2);
1338        stack().push(Type.LONG);
1339    }
1340
1341    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1342    @Override
1343    public void visitLXOR(final LXOR o) {
1344        stack().pop(2);
1345        stack().push(Type.LONG);
1346    }
1347
1348    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1349    @Override
1350    public void visitMONITORENTER(final MONITORENTER o) {
1351        stack().pop();
1352    }
1353
1354    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1355    @Override
1356    public void visitMONITOREXIT(final MONITOREXIT o) {
1357        stack().pop();
1358    }
1359
1360    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1361    @Override
1362    public void visitMULTIANEWARRAY(final MULTIANEWARRAY o) {
1363        stack().pop(o.getDimensions());
1364        stack().push(o.getType(cpg));
1365    }
1366
1367    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1368    @Override
1369    public void visitNEW(final NEW o) {
1370        stack().push(new UninitializedObjectType((ObjectType) o.getType(cpg)));
1371    }
1372
1373    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1374    @Override
1375    public void visitNEWARRAY(final NEWARRAY o) {
1376        stack().pop();
1377        stack().push(o.getType());
1378    }
1379
1380    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1381    @Override
1382    public void visitNOP(final NOP o) {
1383    }
1384
1385    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1386    @Override
1387    public void visitPOP(final POP o) {
1388        stack().pop();
1389    }
1390
1391    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1392    @Override
1393    public void visitPOP2(final POP2 o) {
1394        final Type t = stack().pop();
1395        if (t.getSize() == 1) {
1396            stack().pop();
1397        }
1398    }
1399
1400    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1401    @Override
1402    public void visitPUTFIELD(final PUTFIELD o) {
1403        stack().pop(2);
1404    }
1405
1406    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1407    @Override
1408    public void visitPUTSTATIC(final PUTSTATIC o) {
1409        stack().pop();
1410    }
1411
1412    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1413    @Override
1414    public void visitRET(final RET o) {
1415        // do nothing, return address
1416        // is in the local variables.
1417    }
1418
1419    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1420    @Override
1421    public void visitRETURN(final RETURN o) {
1422        // do nothing.
1423    }
1424
1425    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1426    @Override
1427    public void visitSALOAD(final SALOAD o) {
1428        stack().pop(2);
1429        stack().push(Type.INT);
1430    }
1431
1432    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1433    @Override
1434    public void visitSASTORE(final SASTORE o) {
1435        stack().pop(3);
1436    }
1437
1438    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1439    @Override
1440    public void visitSIPUSH(final SIPUSH o) {
1441        stack().push(Type.INT);
1442    }
1443
1444    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1445    @Override
1446    public void visitSWAP(final SWAP o) {
1447        final Type t = stack().pop();
1448        final Type u = stack().pop();
1449        stack().push(t);
1450        stack().push(u);
1451    }
1452
1453    /** Symbolically executes the corresponding Java Virtual Machine instruction. */
1454    @Override
1455    public void visitTABLESWITCH(final TABLESWITCH o) {
1456        stack().pop();
1457    }
1458}