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