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) {
81 ElementInfo ei = heap.get(objref);
82 int sid = ei.getSid();
84 if (positiveSid){ // count sid upwards from 1
85 if (sid <= 0){ // not seen before in this serialization run
90 } else { // count sid downwards from -1
91 if (sid >= 0){ // not seen before in this serialization run
99 // note that we always add the absolute sid value
107 protected void serializeStackFrames() {
108 ThreadList tl = ks.getThreadList();
110 for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
111 serializeStackFrames(it.next());
117 protected void serializeFrame(StackFrame frame){
118 FramePolicy fp = getFramePolicy(frame.getMethodInfo());
119 Instruction pc = frame.getPC();
120 int len = frame.getTopPos()+1;
122 if (fp == null || fp.includePC || istop) {
123 buf.add(frame.getMethodInfo().getGlobalId());
124 buf.add( pc != null ? pc.getInstructionIndex() : -1);
127 if (fp == null || fp.includeLocals || istop) {
130 // unfortunately we can't do this as a block operation because that
131 // would use concrete reference values as hash data, i.e. break heap symmetry
132 int[] slots = frame.getSlots();
133 for (int i = 0; i < len; i++) {
134 if (frame.isReferenceSlot(i)) {
135 processReference(slots[i]);
144 protected void processReferenceQueue() {
145 refQueue.process(this);
149 protected int getSerializedReferenceValue (ElementInfo ei){
150 return Math.abs(ei.getSid());