Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/DefaultBacktracker.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
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 }