src/main/gov/nasa/jpf/jvm/bytecode/SwitchInstruction.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
  19 package gov.nasa.jpf.jvm.bytecode;
  20
  21 import gov.nasa.jpf.vm.Instruction;
  22 import gov.nasa.jpf.vm.KernelState;
  23 import gov.nasa.jpf.vm.StackFrame;
  24 import gov.nasa.jpf.vm.SystemState;
  25 import gov.nasa.jpf.vm.ThreadInfo;
  26 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  27
  28 /**
  29  * common root class for LOOKUPSWITCH and TABLESWITCH insns
  30  *
  31  * <2do> this is inefficient. First, we should store targets as instruction indexes
  32  * to avoid execution() looping. Second, there are no matches for a TABLESWITCH
  33  */
  34 public abstract class SwitchInstruction extends Instruction implements JVMInstruction {
  35
  36   public static final int DEFAULT = -1;
  37
  38   protected int   target;   // default branch
  39   protected int[] targets;  // explicit value branches
  40   protected int[] matches;  // branch consts
  41
  42   protected int lastIdx;
  43
  44   protected SwitchInstruction (int defaultTarget, int numberOfTargets){
  45     target = defaultTarget;
  46     targets = new int[numberOfTargets];
  47     matches = new int[numberOfTargets];
  48   }
  49
  50   public int getNumberOfEntries() {
  51     return targets.length;
  52   }
  53
  54   protected Instruction executeConditional (ThreadInfo ti){
  55     StackFrame frame = ti.getModifiableTopFrame();
  56
  57     int value = frame.pop();
  58
  59     lastIdx = DEFAULT;
  60
  61     for (int i = 0, l = matches.length; i < l; i++) {
  62       if (value == matches[i]) {
  63         lastIdx = i;
  64         return mi.getInstructionAt(targets[i]);
  65       }
  66     }
  67
  68     return mi.getInstructionAt(target);
  69   }
  70
  71   @Override
  72   public Instruction execute (ThreadInfo ti) {
  73     // this can be overridden by subclasses, so we have to delegate the conditional execution
  74     // to avoid getting recursive in executeAllBranches()
  75     return executeConditional(ti);
  76   }
  77
  78   /** useful for symbolic execution modes */
  79   public Instruction executeAllBranches (SystemState ss, KernelState ks, ThreadInfo ti) {
  80     if (!ti.isFirstStepInsn()) {
  81       IntIntervalGenerator cg = new IntIntervalGenerator("switchAll", 0,matches.length);
  82       if (ss.setNextChoiceGenerator(cg)){
  83         return this;
  84
  85       } else {
  86         // listener did override CG, fall back to conditional execution
  87         return executeConditional(ti);
  88       }
  89
  90     } else {
  91       IntIntervalGenerator cg = ss.getCurrentChoiceGenerator("switchAll", IntIntervalGenerator.class);
  92       assert (cg != null) : "no IntIntervalGenerator";
  93
  94       StackFrame frame = ti.getModifiableTopFrame();
  95       int idx = frame.pop(); // but we are not using it
  96       idx = cg.getNextChoice();
  97
  98       if (idx == matches.length){ // default branch
  99         lastIdx = DEFAULT;
 100         return mi.getInstructionAt(target);
 101       } else {
 102         lastIdx = idx;
 103         return mi.getInstructionAt(targets[idx]);
 104       }
 105     }
 106   }
 107
 108   //--- a little inspection, but only post exec yet
 109
 110   public int getLastTargetIndex () {
 111     return lastIdx;
 112   }
 113
 114   public int getNumberOfTargets () {
 115     return matches.length;
 116   }
 117
 118   public int getMatchConst (int idx){
 119     return matches[idx];
 120   }
 121
 122   @Override
 123   public void accept(JVMInstructionVisitor insVisitor) {
 124           insVisitor.visit(this);
 125   }
 126
 127   public int getTarget() {
 128         return target;
 129   }
 130
 131   public int[] getTargets() {
 132         return targets;
 133   }
 134
 135   public int[] getMatches() {
 136         return matches;
 137   }
 138 }