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.StaticElementInfo;
  25 import gov.nasa.jpf.vm.Fields;
  26 import gov.nasa.jpf.util.FinalBitSet;
  27 import gov.nasa.jpf.vm.ClassInfo;
  28 import gov.nasa.jpf.vm.Instruction;
  29 import gov.nasa.jpf.vm.MJIEnv;
  30 import gov.nasa.jpf.vm.StackFrame;
  31 import gov.nasa.jpf.vm.ThreadInfo;
  32 import gov.nasa.jpf.vm.ThreadList;
  33
  34 /**
  35  * a FilteringSerializer that performs on-the-fly heap canonicalization to
  36  * achieve heap symmetry. It does so by storing the order in which
  37  * objects are referenced, not the reference values themselves.
  38  *
  39  * Use this serializer if the Heap implementation does not provide
  40  * sufficient symmetry, i.e. reference values depend on the order of
  41  * thread scheduling.
  42  *
  43  * Ad hoc heap symmetry is hard to achieve in the heap because of static initialization.
  44  * Each time a thread loads a class all the static init (at least the class object and
  45  * its fields) are associated with this thread, hence thread reference
  46  * values depend on which classes are already loaded by other threads. Associating
  47  * all allocations from inside of clinits to one address range doesn't help either
  48  * because then this range will experience scheduling dependent orders. A hybrid
  49  * approach in which only this segment is canonicalized might work, but it is
  50  * questionable if the overhead is worth the effort.
  51  */
  52 public class CFSerializer extends FilteringSerializer {
  53
  54   // we flip this on every serialization, which helps us to avoid passes
  55   // over the serialized objects to reset their sids. This works by resetting
  56   // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
  57   // from -1, but store the absolute value in the serialization stream
  58   boolean positiveSid;
  59
  60   int sidCount;
  61
  62   @Override
  63   protected void initReferenceQueue() {
  64     super.initReferenceQueue();
  65
  66     if (positiveSid){
  67       positiveSid = false;
  68       sidCount = -1;
  69     } else {
  70       positiveSid = true;
  71       sidCount = 1;
  72     }
  73   }
  74
  75   // might be overriden in subclasses to conditionally queue objects
  76   protected void queueReference(ElementInfo ei){
  77     refQueue.add(ei);
  78   }
  79
  80   @Override
  81   public void processReference(int objref) {
  82     if (objref == MJIEnv.NULL) {
  83       buf.add(MJIEnv.NULL);
  84     } else {
  85       ElementInfo ei = heap.get(objref);
  86       ClassInfo ci = ei.getClassInfo();
  87
  88       if (SmartThingsConfig.instance.ignoreClass(ci)) {
  89         ei.setSid(0);
  90         buf.add(0);
  91         return;
  92       }
  93
  94       int sid = ei.getSid();
  95
  96       if (positiveSid){ // count sid upwards from 1
  97         if (sid <= 0){  // not seen before in this serialization run
  98           sid = sidCount++;
  99           ei.setSid(sid);
 100           queueReference(ei);
 101         }
 102       } else { // count sid downwards from -1
 103         if (sid >= 0){ // not seen before in this serialization run
 104           sid = sidCount--;
 105           ei.setSid(sid);
 106           queueReference(ei);
 107         }
 108         sid = -sid;
 109       }
 110
 111       // note that we always add the absolute sid value
 112       buf.add(sid);
 113     }
 114   }
 115
 116
 117   @Override
 118   protected void serializeStackFrames() {
 119     ThreadList tl = ks.getThreadList();
 120     for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
 121       serializeStackFrames(it.next());
 122     }
 123   }
 124
 125   //Don't think we actually have static fields...so this should be safe
 126   @Override
 127   protected void serializeClassLoaders(){
 128   }
 129
 130   protected void serializeClass (StaticElementInfo sei){
 131     // buf.add(sei.getStatus());
 132
 133     Fields fields = sei.getFields();
 134     ClassInfo ci = sei.getClassInfo();
 135     FinalBitSet filtered = getStaticFilterMask(ci);
 136     FinalBitSet refs = getStaticRefMask(ci);
 137     int max = ci.getStaticDataSize();
 138     if (SmartThingsConfig.instance.staticClass(ci))
 139       return;
 140     for (int i = 0; i < max; i++) {
 141       if (!filtered.get(i)) {
 142         int v = fields.getIntValue(i);
 143         if (refs.get(i)) {
 144           processReference(v);
 145         } else {
 146           buf.add(v);
 147         }
 148       }
 149     }
 150   }
 151
 152
 153   @Override
 154   protected void serializeFrame(StackFrame frame){
 155     FramePolicy fp = getFramePolicy(frame.getMethodInfo());
 156     Instruction pc = frame.getPC();
 157     int len = frame.getTopPos()+1;
 158
 159     if (fp == null || fp.includePC) {
 160       buf.add(frame.getMethodInfo().getGlobalId());
 161       buf.add( pc != null ? pc.getInstructionIndex() : -1);
 162     }
 163
 164     if (fp == null || fp.includeLocals) {
 165       buf.add(len);
 166
 167       // unfortunately we can't do this as a block operation because that
 168       // would use concrete reference values as hash data, i.e. break heap symmetry
 169       int thisslot = frame.getThis();
 170       processReference(thisslot);
 171       /*
 172       int[] slots = frame.getSlots();
 173       for (int i = 0; i < len; i++) {
 174         if (frame.isReferenceSlot(i)) {
 175           processReference(slots[i]);
 176         } else {
 177           buf.add(slots[i]);
 178         }
 179       }
 180       */
 181     }
 182   }
 183
 184   @Override
 185   protected void processReferenceQueue() {
 186     refQueue.process(this);
 187   }
 188
 189   @Override
 190   protected int getSerializedReferenceValue (ElementInfo ei){
 191     return Math.abs(ei.getSid());
 192   }
 193 }