src/main/gov/nasa/jpf/vm/DefaultBacktracker.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.vm;
  19
  20 import gov.nasa.jpf.util.ImmutableList;
  21
  22 public class DefaultBacktracker<KState> implements Backtracker {
  23   /** where we keep the saved KernelState head */
  24   protected ImmutableList<KState> kstack;
  25
  26   /** and that adds the SystemState specifics */
  27   protected ImmutableList<Object> sstack;
  28
  29   protected SystemState ss;
  30   protected StateRestorer<KState> restorer;
  31
  32   @Override
  33   public void attach(VM vm) {
  34     ss = vm.getSystemState();
  35     restorer = vm.getRestorer();
  36   }
  37
  38   //--- the backtrack support (depth first only)
  39
  40   protected void backtrackKernelState() {
  41     KState data = kstack.head;
  42     kstack = kstack.tail;
  43
  44     restorer.restore(data);
  45   }
  46
  47   protected void backtrackSystemState() {
  48     Object o = sstack.head;
  49     sstack = sstack.tail;
  50     ss.backtrackTo(o);
  51   }
  52
  53
  54   /**
  55    * Moves one step backward. This method and forward() are the main methods
  56    * used by the search object.
  57    * Note this is called with the state that caused the backtrack still being on
  58    * the stack, so we have to remove that one first (i.e. popping two states
  59    * and restoring the second one)
  60    */
  61   @Override
  62   public boolean backtrack () {
  63     if (sstack != null) {
  64
  65       backtrackKernelState();
  66       backtrackSystemState();
  67
  68       return true;
  69     } else {
  70       // we are back to the top of where we can backtrack to
  71       return false;
  72     }
  73   }
  74
  75   /**
  76    * Saves the state of the system.
  77    */
  78   @Override
  79   public void pushKernelState () {
  80     kstack = new ImmutableList<KState>(restorer.getRestorableData(),kstack);
  81   }
  82
  83   /**
  84    * Saves the backtracking information.
  85    */
  86   @Override
  87   public void pushSystemState () {
  88     sstack = new ImmutableList<Object>(ss.getBacktrackData(),sstack);
  89   }
  90
  91
  92   //--- the restore support
  93
  94   // <2do> this saves both the backtrack and the restore data - too redundant
  95   class RestorableStateImpl implements RestorableState {
  96     final ImmutableList<KState> savedKstack;
  97     final ImmutableList<Object> savedSstack;
  98
  99     final KState kcur;
 100     final Object scur;
 101
 102     RestorableStateImpl() {
 103       savedKstack = kstack;
 104       savedSstack = sstack;
 105       kcur = restorer.getRestorableData();
 106       scur = ss.getRestoreData();
 107     }
 108
 109     void restore() {
 110       kstack = savedKstack;
 111       sstack = savedSstack;
 112       restorer.restore(kcur);
 113       ss.restoreTo(scur);
 114     }
 115   }
 116
 117   @Override
 118   public void restoreState (RestorableState state) {
 119     ((RestorableStateImpl) state).restore();
 120   }
 121
 122   @Override
 123   public RestorableState getRestorableState() {
 124     return new RestorableStateImpl();
 125   }
 126 }