src/main/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.jvm.bytecode;
  19
  20 import gov.nasa.jpf.vm.Instruction;
  21 import gov.nasa.jpf.vm.ClassInfo;
  22 import gov.nasa.jpf.vm.ElementInfo;
  23 import gov.nasa.jpf.vm.LoadOnJPFRequired;
  24 import gov.nasa.jpf.vm.MJIEnv;
  25 import gov.nasa.jpf.vm.StackFrame;
  26 import gov.nasa.jpf.vm.ThreadInfo;
  27 import gov.nasa.jpf.vm.Types;
  28
  29
  30 /**
  31  * Check whether object is of given type
  32  * ..., objectref => ..., objectref
  33  */
  34 public class CHECKCAST extends Instruction implements JVMInstruction {
  35   String type;
  36
  37   public CHECKCAST() {} // this is going away
  38
  39   public CHECKCAST(String typeName){
  40     type = Types.getClassNameFromTypeName(typeName);
  41   }
  42
  43   public String getTypeName() {
  44     return type;
  45   }
  46
  47   @Override
  48   public Instruction execute (ThreadInfo ti) {
  49     StackFrame frame = ti.getTopFrame();
  50     int objref = frame.peek();
  51
  52     if (objref == MJIEnv.NULL) {
  53        // we can cast 'null' to anything
  54
  55     } else {
  56       boolean isValid = false;
  57
  58       if(Types.isReferenceSignature(type)) {
  59         String t;
  60         if(Types.isArray(type)) {
  61           // retrieve the component terminal
  62           t = Types.getComponentTerminal(type);
  63         } else {
  64           t = type;
  65         }
  66
  67         // resolve the referenced class
  68         try {
  69           ti.resolveReferencedClass(t);
  70         } catch(LoadOnJPFRequired lre) {
  71           return ti.getPC();
  72         }
  73       }
  74
  75       ElementInfo e = ti.getElementInfo(objref);
  76       ClassInfo eci = e.getClassInfo();
  77
  78       if (type.charAt(0) == '['){  // cast between array types
  79         if (eci.isArray()) {
  80           // check if the element types are compatible
  81           ClassInfo cci = eci.getComponentClassInfo();
  82           isValid = cci.isInstanceOf(type.substring(1));
  83         }
  84
  85       } else { // non-array types
  86         isValid = e.getClassInfo().isInstanceOf(type);
  87       }
  88
  89       if (!isValid) {
  90         return ti.createAndThrowException("java.lang.ClassCastException",
  91                 e.getClassInfo().getName() + " cannot be cast to " + type);
  92       }
  93     }
  94
  95     return getNext(ti);
  96   }
  97
  98
  99   @Override
 100   public int getLength() {
 101     return 3; // opcode, index1, index2
 102   }
 103
 104   @Override
 105   public int getByteCode () {
 106     return 0xC0;
 107   }
 108
 109   @Override
 110   public void accept(JVMInstructionVisitor insVisitor) {
 111           insVisitor.visit(this);
 112   }
 113 }