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.
19 package gov.nasa.jpf.vm.serialize;
21 import java.util.Iterator;
23 import gov.nasa.jpf.vm.ElementInfo;
24 import gov.nasa.jpf.vm.Instruction;
25 import gov.nasa.jpf.vm.MJIEnv;
26 import gov.nasa.jpf.vm.StackFrame;
27 import gov.nasa.jpf.vm.ThreadInfo;
28 import gov.nasa.jpf.vm.ThreadList;
31 * a FilteringSerializer that performs on-the-fly heap canonicalization to
32 * achieve heap symmetry. It does so by storing the order in which
33 * objects are referenced, not the reference values themselves.
35 * Use this serializer if the Heap implementation does not provide
36 * sufficient symmetry, i.e. reference values depend on the order of
39 * Ad hoc heap symmetry is hard to achieve in the heap because of static initialization.
40 * Each time a thread loads a class all the static init (at least the class object and
41 * its fields) are associated with this thread, hence thread reference
42 * values depend on which classes are already loaded by other threads. Associating
43 * all allocations from inside of clinits to one address range doesn't help either
44 * because then this range will experience scheduling dependent orders. A hybrid
45 * approach in which only this segment is canonicalized might work, but it is
46 * questionable if the overhead is worth the effort.
48 public class CFSerializer extends FilteringSerializer {
50 // we flip this on every serialization, which helps us to avoid passes
51 // over the serialized objects to reset their sids. This works by resetting
52 // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
53 // from -1, but store the absolute value in the serialization stream
59 protected void initReferenceQueue() {
60 super.initReferenceQueue();
71 // might be overriden in subclasses to conditionally queue objects
72 protected void queueReference(ElementInfo ei){
77 public void processReference(int objref) {
78 if (objref == MJIEnv.NULL) {
82 ElementInfo ei = heap.get(objref);
83 int sid = ei.getSid();
85 if (positiveSid){ // count sid upwards from 1
86 if (sid <= 0){ // not seen before in this serialization run
91 } else { // count sid downwards from -1
92 if (sid >= 0){ // not seen before in this serialization run
100 // note that we always add the absolute sid value
106 protected void serializeStackFrames() {
107 ThreadList tl = ks.getThreadList();
109 for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
110 serializeStackFrames(it.next());
115 protected void serializeFrame(StackFrame frame){
116 buf.add(frame.getMethodInfo().getGlobalId());
118 Instruction pc = frame.getPC();
119 buf.add( pc != null ? pc.getInstructionIndex() : -1);
121 int len = frame.getTopPos()+1;
124 // unfortunately we can't do this as a block operation because that
125 // would use concrete reference values as hash data, i.e. break heap symmetry
126 int[] slots = frame.getSlots();
127 for (int i = 0; i < len; i++) {
128 if (frame.isReferenceSlot(i)) {
129 processReference(slots[i]);
137 protected void processReferenceQueue() {
138 refQueue.process(this);
142 protected int getSerializedReferenceValue (ElementInfo ei){
143 return Math.abs(ei.getSid());