View Javadoc

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