src/main/gov/nasa/jpf/vm/serialize/CFSerializer.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
  19 package gov.nasa.jpf.vm.serialize;
  20
  21 import java.util.Iterator;
  22
  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;
  29
  30 /**
  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.
  34  *
  35  * Use this serializer if the Heap implementation does not provide
  36  * sufficient symmetry, i.e. reference values depend on the order of
  37  * thread scheduling.
  38  *
  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.
  47  */
  48 public class CFSerializer extends FilteringSerializer {
  49
  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
  54   boolean positiveSid;
  55
  56   int sidCount;
  57
  58   @Override
  59   protected void initReferenceQueue() {
  60     super.initReferenceQueue();
  61
  62     if (positiveSid){
  63       positiveSid = false;
  64       sidCount = -1;
  65     } else {
  66       positiveSid = true;
  67       sidCount = 1;
  68     }
  69   }
  70
  71   // might be overriden in subclasses to conditionally queue objects
  72   protected void queueReference(ElementInfo ei){
  73     refQueue.add(ei);
  74   }
  75
  76   @Override
  77   public void processReference(int objref) {
  78     if (objref == MJIEnv.NULL) {
  79       buf.add(MJIEnv.NULL);
  80     } else {
  81       ElementInfo ei = heap.get(objref);
  82       int sid = ei.getSid();
  83
  84       if (positiveSid){ // count sid upwards from 1
  85         if (sid <= 0){  // not seen before in this serialization run
  86           sid = sidCount++;
  87           ei.setSid(sid);
  88           queueReference(ei);
  89         }
  90       } else { // count sid downwards from -1
  91         if (sid >= 0){ // not seen before in this serialization run
  92           sid = sidCount--;
  93           ei.setSid(sid);
  94           queueReference(ei);
  95         }
  96         sid = -sid;
  97       }
  98
  99       // note that we always add the absolute sid value
 100       buf.add(sid);
 101     }
 102   }
 103
 104
 105   boolean istop;
 106   @Override
 107   protected void serializeStackFrames() {
 108     ThreadList tl = ks.getThreadList();
 109     istop = true;
 110     for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
 111       serializeStackFrames(it.next());
 112       istop = false;
 113     }
 114   }
 115
 116   @Override
 117   protected void serializeFrame(StackFrame frame){
 118     FramePolicy fp = getFramePolicy(frame.getMethodInfo());
 119     Instruction pc = frame.getPC();
 120     int len = frame.getTopPos()+1;
 121
 122     if (fp == null || fp.includePC || istop) {
 123       buf.add(frame.getMethodInfo().getGlobalId());
 124       buf.add( pc != null ? pc.getInstructionIndex() : -1);
 125     }
 126
 127     if (fp == null || fp.includeLocals || istop) {
 128       buf.add(len);
 129
 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]);
 136         } else {
 137           buf.add(slots[i]);
 138         }
 139       }
 140     }
 141   }
 142
 143   @Override
 144   protected void processReferenceQueue() {
 145     refQueue.process(this);
 146   }
 147
 148   @Override
 149   protected int getSerializedReferenceValue (ElementInfo ei){
 150     return Math.abs(ei.getSid());
 151   }
 152 }