gov.nasa.jpf.vm.serialize

Class DynamicAbstractionSerializer

java.lang.Object

gov.nasa.jpf.vm.AbstractSerializer

gov.nasa.jpf.vm.serialize.FilteringSerializer

gov.nasa.jpf.vm.serialize.DynamicAbstractionSerializer

All Implemented Interfaces:

Processor<ElementInfo>, KernelState.ChangeListener, ReferenceProcessor, StateSerializer

public class DynamicAbstractionSerializer
extends FilteringSerializer

a serializer that uses Abstraction objects stored as field attributes to obtain the values to hash.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	DynamicAbstractionSerializer.Attributor

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	declaredFieldsOnly
protected StringSetMatcher	excludeClasses
protected StringSetMatcher	excludeMethods
protected StringSetMatcher	includeClasses
protected StringSetMatcher	includeMethods
protected boolean	processAllObjects

Fields inherited from class gov.nasa.jpf.vm.serialize.FilteringSerializer

buf, filter, refQueue

Fields inherited from class gov.nasa.jpf.vm.AbstractSerializer

cached, ks, nativeStateHolders, vm

Constructor Summary

Constructors

Constructor and Description
DynamicAbstractionSerializer(Config conf)

Method Summary

Modifier and Type	Method and Description
void	attach(VM vm)
protected java.util.List<gov.nasa.jpf.vm.serialize.DynamicAbstractionSerializer.FieldAbstraction>	getFieldAbstractions(Config conf)
void	process(ElementInfo ei)
protected void	processArrayFields(ArrayFields fields)
protected void	processField(Fields fields, int[] slotValues, FieldInfo fi, FinalBitSet filtered)
protected void	processNamedFields(ClassInfo ci, Fields fields)
protected void	processNamedInstanceReferenceFields(ClassInfo ci, Fields fields)
protected void	processNamedStaticReferenceFields(ClassInfo ci, Fields fields)
void	processReference(int objref)
protected void	processReferenceArray(ReferenceArrayFields fields)
protected void	serializeClass(StaticElementInfo sei)
protected void	serializeClassLoaders()
protected void	serializeFrame(StackFrame frame) more generic, but less efficient because it can't use block operations protected void _serializeFrame(StackFrame frame){ buf.add(frame.getMethodInfo().getGlobalId()); buf.add(frame.getPC().getInstructionIndex()); int len = frame.getTopPos()+1; buf.add(len); // this looks like something we can push into the frame int[] slots = frame.getSlots(); for (int i = 0; i < len; i++) { if (frame.isReferenceSlot(i)) { processReference(slots[i]); } else { buf.add(slots[i]); } } }
protected void	serializeStatics(Statics statics)

Methods inherited from class gov.nasa.jpf.vm.serialize.FilteringSerializer

computeStoringData, dumpData, getFramePolicy, getInstanceFilterMask, getInstanceRefMask, getSerializedReferenceValue, getStaticFilterMask, getStaticRefMask, initReferenceQueue, processReferenceQueue, serializeLockedObjects, serializeNativeStateHolder, serializeNativeStateHolders, serializeStackFrames, serializeStackFrames, serializeThreadState, serializeThreadStates

Methods inherited from class gov.nasa.jpf.vm.AbstractSerializer

addNativeStateHolder, getCurrentStateVectorLength, getStoringData, kernelStateChanged

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

includeClasses

protected StringSetMatcher includeClasses

excludeClasses

protected StringSetMatcher excludeClasses

includeMethods

protected StringSetMatcher includeMethods

excludeMethods

protected StringSetMatcher excludeMethods

processAllObjects

protected boolean processAllObjects

declaredFieldsOnly

protected boolean declaredFieldsOnly

Constructor Detail

DynamicAbstractionSerializer

public DynamicAbstractionSerializer(Config conf)

Method Detail

getFieldAbstractions

protected java.util.List<gov.nasa.jpf.vm.serialize.DynamicAbstractionSerializer.FieldAbstraction> getFieldAbstractions(Config conf)

attach

public void attach(VM vm)

Specified by:

attach in interface StateSerializer

Overrides:

attach in class FilteringSerializer

processReference

public void processReference(int objref)

Specified by:

processReference in interface ReferenceProcessor

Overrides:

processReference in class FilteringSerializer

processField

protected void processField(Fields fields,
                            int[] slotValues,
                            FieldInfo fi,
                            FinalBitSet filtered)

processArrayFields

protected void processArrayFields(ArrayFields fields)

Overrides:

processArrayFields in class FilteringSerializer

processNamedInstanceReferenceFields

protected void processNamedInstanceReferenceFields(ClassInfo ci,
                                                   Fields fields)

processNamedStaticReferenceFields

protected void processNamedStaticReferenceFields(ClassInfo ci,
                                                 Fields fields)

processReferenceArray

protected void processReferenceArray(ReferenceArrayFields fields)

processNamedFields

protected void processNamedFields(ClassInfo ci,
                                  Fields fields)

Overrides:

processNamedFields in class FilteringSerializer

process

public void process(ElementInfo ei)

Specified by:

process in interface Processor<ElementInfo>

Overrides:

process in class FilteringSerializer

serializeFrame

protected void serializeFrame(StackFrame frame)

Description copied from class: FilteringSerializer

more generic, but less efficient because it can't use block operations protected void _serializeFrame(StackFrame frame){ buf.add(frame.getMethodInfo().getGlobalId()); buf.add(frame.getPC().getInstructionIndex()); int len = frame.getTopPos()+1; buf.add(len); // this looks like something we can push into the frame int[] slots = frame.getSlots(); for (int i = 0; i < len; i++) { if (frame.isReferenceSlot(i)) { processReference(slots[i]); } else { buf.add(slots[i]); } } }

Overrides:

serializeFrame in class FilteringSerializer

serializeClass

protected void serializeClass(StaticElementInfo sei)

Overrides:

serializeClass in class FilteringSerializer

serializeClassLoaders

protected void serializeClassLoaders()

Overrides:

serializeClassLoaders in class FilteringSerializer

serializeStatics

protected void serializeStatics(Statics statics)

Overrides:

serializeStatics in class FilteringSerializer