edu.mit.csail.sdg.squander.engine.Heap2Bounds Class Reference
[Engine]

Collaboration diagram for edu.mit.csail.sdg.squander.engine.Heap2Bounds:

Classes
class	Pair
Public Member Functions
	Heap2Bounds (JavaScene javaScene)
int	minBW ()
Map< String, ObjTupleSet >	bounds ()
ObjTupleSet	getBound (ForgeVariable var)
Set< Object >	reachableObjects ()
void	ensureAdequateIntBitWidth (int x)
void	traverse (List< Pair > rootObjects)
Package Functions
void	addBound (String varName, ObjTuple value)
void	addBound (String varName, ObjTupleSet value)
Private Member Functions
void	newObject (Object object, Unary[] actualTypeParams)
void	visitPrimitive (Object obj)
void	ensureAdequateBitWidth (final Object obj)
Private Attributes
final JavaScene	javaScene
final Set< Object >	visited = new IdentityHashSet<Object>()
Map< String, ObjTupleSet >	varName2Const = new HashMap<String, ObjTupleSet>()
int	rbw = GlobalOptions.INSTANCE.min_bitwidth

Detailed Description

Used to convert the heap to bounds for fields, that are going to be used later for solving.

Author:: Aleksandar Milicevic

Definition at line 39 of file Heap2Bounds.java.

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.engine.Heap2Bounds.Heap2Bounds ( JavaScene javaScene )

Definition at line 84 of file Heap2Bounds.java.

Member Function Documentation

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound	(	String	varName,
		ObjTupleSet	value
	)			`[package]`

Definition at line 142 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, and edu.mit.csail.sdg.squander.engine.Heap2Bounds.varName2Const.

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound	(	String	varName,
		ObjTuple	value
	)			`[package]`

Definition at line 136 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), and edu.mit.csail.sdg.squander.absstate.ObjTuple.arity.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), and edu.mit.csail.sdg.squander.engine.Heap2Bounds.traverse().

Map<String, ObjTupleSet> edu.mit.csail.sdg.squander.engine.Heap2Bounds.bounds ( )

Returns the exact bounds for all fields (field names, that is)

Definition at line 91 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.varName2Const.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.printBounds().

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateBitWidth ( final Object obj ) [private]

Definition at line 174 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateIntBitWidth().

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject().

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateIntBitWidth ( int x )

Makes sure that the bitwidth is big enough to represent the given integer value

Definition at line 98 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.rbw.

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateBitWidth(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), and edu.mit.csail.sdg.squander.engine.Heap2Bounds.visitPrimitive().

ObjTupleSet edu.mit.csail.sdg.squander.engine.Heap2Bounds.getBound ( ForgeVariable var )

Returns the exact bounds for the field represented with the given Forge variable

Definition at line 93 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.varName2Const.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitVariable().

int edu.mit.csail.sdg.squander.engine.Heap2Bounds.minBW ( )

Returns min required bit width, based on the content of the heap

Definition at line 89 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.rbw.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt().

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject	(	Object	object,
		Unary[]	actualTypeParams
	)			`[private]`

Definition at line 156 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.addObj2spec(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateBitWidth(), edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.javaScene, and edu.mit.csail.sdg.squander.engine.Heap2Bounds.visitPrimitive().

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.traverse().

Set<Object> edu.mit.csail.sdg.squander.engine.Heap2Bounds.reachableObjects ( )

Returns all reachable objects found on the heap

Definition at line 95 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.visited.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.traverse ( List< Pair > rootObjects )

Traverses the heap starting from the given root objects (rootObjects). It uses IObjSer to serialize objects (i.e. break the apart). During the traversal it collects the bounds for fields.

Definition at line 108 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.serializer.special.IObjSer.absFunc(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound(), edu.mit.csail.sdg.squander.serializer.special.ObjSerFactory.getSerForObj(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.javaScene, edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject(), and edu.mit.csail.sdg.squander.engine.Heap2Bounds.visited.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().

void edu.mit.csail.sdg.squander.engine.Heap2Bounds.visitPrimitive ( Object obj ) [private]

Definition at line 167 of file Heap2Bounds.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateIntBitWidth().

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject().