2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.util.ImmutableList;
22 public class DefaultBacktracker<KState> implements Backtracker {
23 /** where we keep the saved KernelState head */
24 protected ImmutableList<KState> kstack;
26 /** and that adds the SystemState specifics */
27 protected ImmutableList<Object> sstack;
29 protected SystemState ss;
30 protected StateRestorer<KState> restorer;
33 public void attach(VM vm) {
34 ss = vm.getSystemState();
35 restorer = vm.getRestorer();
38 //--- the backtrack support (depth first only)
40 protected void backtrackKernelState() {
41 KState data = kstack.head;
44 restorer.restore(data);
47 protected void backtrackSystemState() {
48 Object o = sstack.head;
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)
62 public boolean backtrack () {
65 backtrackKernelState();
66 backtrackSystemState();
70 // we are back to the top of where we can backtrack to
76 * Saves the state of the system.
79 public void pushKernelState () {
80 kstack = new ImmutableList<KState>(restorer.getRestorableData(),kstack);
84 * Saves the backtracking information.
87 public void pushSystemState () {
88 sstack = new ImmutableList<Object>(ss.getBacktrackData(),sstack);
92 //--- the restore support
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;
102 RestorableStateImpl() {
103 savedKstack = kstack;
104 savedSstack = sstack;
105 kcur = restorer.getRestorableData();
106 scur = ss.getRestoreData();
110 kstack = savedKstack;
111 sstack = savedSstack;
112 restorer.restore(kcur);
118 public void restoreState (RestorableState state) {
119 ((RestorableStateImpl) state).restore();
123 public RestorableState getRestorableState() {
124 return new RestorableStateImpl();