src/main/gov/nasa/jpf/jvm/bytecode/IfInstruction.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.BooleanChoiceGenerator;
  22 import gov.nasa.jpf.vm.KernelState;
  23 import gov.nasa.jpf.vm.MethodInfo;
  24 import gov.nasa.jpf.vm.StackFrame;
  25 import gov.nasa.jpf.vm.SystemState;
  26 import gov.nasa.jpf.vm.ThreadInfo;
  27
  28 /**
  29  * abstraction for all comparison instructions
  30  */
  31 public abstract class IfInstruction extends Instruction implements JVMInstruction {
  32   protected int targetPosition;  // insn position at jump insnIndex
  33   protected Instruction target;  // jump target
  34
  35   protected boolean conditionValue;  /** value of last evaluation of branch condition */
  36
  37   protected IfInstruction(int targetPosition){
  38     this.targetPosition = targetPosition;
  39   }
  40
  41   /**
  42    * return which branch was taken. Only useful after instruction got executed
  43    * WATCH OUT - 'true' means the jump condition is met, which logically is
  44    * the 'false' branch
  45    */
  46   public boolean getConditionValue() {
  47     return conditionValue;
  48   }
  49
  50   /**
  51    *  Added so that SimpleIdleFilter can detect do-while loops when
  52    * the while statement evaluates to true.
  53    */
  54   @Override
  55   public boolean isBackJump () {
  56     return (conditionValue) && (targetPosition <= position);
  57   }
  58
  59   /**
  60    * retrieve value of jump condition from operand stack
  61    * (not ideal to have this public, but some listeners might need it for
  62    * skipping the insn, plus we require it for subclass factorization)
  63    */
  64   public abstract boolean popConditionValue(StackFrame frame);
  65
  66   public Instruction getTarget() {
  67     if (target == null) {
  68       target = mi.getInstructionAt(targetPosition);
  69     }
  70     return target;
  71   }
  72
  73   @Override
  74   public Instruction execute (ThreadInfo ti) {
  75     StackFrame frame = ti.getModifiableTopFrame();
  76
  77     conditionValue = popConditionValue(frame);
  78     if (conditionValue) {
  79       return getTarget();
  80     } else {
  81       return getNext(ti);
  82     }
  83   }
  84
  85   /**
  86    * use this as a delegatee in overridden executes of derived IfInstructions
  87    * (e.g. for symbolic execution)
  88    */
  89   protected Instruction executeBothBranches (SystemState ss, KernelState ks, ThreadInfo ti){
  90     if (!ti.isFirstStepInsn()) {
  91       BooleanChoiceGenerator cg = new BooleanChoiceGenerator(ti.getVM().getConfig(), "ifAll");
  92       if (ss.setNextChoiceGenerator(cg)){
  93         return this;
  94
  95       } else {
  96         StackFrame frame = ti.getModifiableTopFrame();
  97         // some listener did override the CG, fallback to normal operation
  98         conditionValue = popConditionValue(frame);
  99         if (conditionValue) {
 100           return getTarget();
 101         } else {
 102           return getNext(ti);
 103         }
 104       }
 105
 106     } else {
 107       BooleanChoiceGenerator cg = ss.getCurrentChoiceGenerator("ifAll", BooleanChoiceGenerator.class);
 108       assert (cg != null) : "no BooleanChoiceGenerator";
 109
 110       StackFrame frame = ti.getModifiableTopFrame();
 111       popConditionValue(frame); // we are not interested in concrete values
 112
 113       conditionValue = cg.getNextChoice();
 114
 115       if (conditionValue) {
 116         return getTarget();
 117       } else {
 118         return getNext(ti);
 119       }
 120
 121     }
 122   }
 123
 124   @Override
 125   public String toString () {
 126     return getMnemonic() + " " + targetPosition;
 127   }
 128
 129   @Override
 130   public int getLength() {
 131     return 3; // usually opcode, bb1, bb2
 132   }
 133
 134   @Override
 135   public void accept(JVMInstructionVisitor insVisitor) {
 136           insVisitor.visit(this);
 137   }
 138
 139   @Override
 140   public Instruction typeSafeClone(MethodInfo mi) {
 141     IfInstruction clone = null;
 142
 143     try {
 144       clone = (IfInstruction) super.clone();
 145
 146       // reset the method that this insn belongs to
 147       clone.mi = mi;
 148
 149       clone.target = null;
 150     } catch (CloneNotSupportedException e) {
 151       e.printStackTrace();
 152     }
 153
 154     return clone;
 155   }
 156 }