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

Collaboration diagram for edu.mit.csail.sdg.squander.engine.ForgeConverter:
Collaboration graph
[legend]

List of all members.

Public Member Functions

 ForgeConverter (SquanderReporter reporter, Object...heapRootObjects)
void setCallContext (Object caller, JMethod m, Object[] methodArgs)
void boundSpecFields (IEvaluator eval)
JavaScene javaScene ()
ForgeScene forgeScene ()
Heap2Bounds heap2Lit ()
ForgeBounds forgeBounds ()
String printBounds ()
ForgeProcedure proc ()
Spec getSpec ()
SolveOptions forgeOptions ()
Iterable< Integer > allInts ()
List< InstanceLiteral > findInstLiteralsForType (ForgeType.Unary colType)
List< ForgeLiteral > findLiteralsForType (ForgeType.Unary colType)
ObjTupleSet extent (ForgeType t)
Object atom2obj (ForgeAtom atom)
Object lit2obj (ForgeLiteral lit)
int minInt ()
int maxInt ()
ForgeConstant conv2fc (ObjTupleSet objTupleSet, ForgeBounds bounds)
ForgeAtom obj2atom (Object obj, ForgeBounds bounds)

Static Public Member Functions

static Object mapToBoolean (final ForgeAtom atom)
static int mapToInt (final ForgeAtom atom)

Private Member Functions

void finish ()
void createFreshObjects (MethodSpec ms)
int getMaxAtomsForType (ForgeType ft)
int maxSize (ForgeDomain d)
String printObjSet (ObjTupleSet objSet)
void initJavaScene ()
void boundOtherStuff ()
ForgeBounds makeForgeBounds (Heap2Bounds heap2lit)
String printUniverseStats ()

Private Attributes

final SquanderReporter reporter
final Heap heap
final JavaScene javaScene
ForgeScene forgeScene
Heap2Bounds heap2lit
ForgeBounds forgeBounds
boolean finished = false
Map< Object, JType.Unary[]> obj2typeparams = new IdentityHashMap<Object, Unary[]>()
Map< ForgeType, Integer > maxAtomsCache = new HashMap<ForgeType, Integer>()
Set< Integer > allInts = null
Map< ForgeType.Unary, List
< InstanceLiteral > > 		instLitsCache = new HashMap<ForgeType.Unary, List<InstanceLiteral>>()
Map< ForgeType.Unary, List
< ForgeLiteral > > 		litsCache = new HashMap<ForgeType.Unary, List<ForgeLiteral>>()

Detailed Description

This class handles conversion of the heap (heap) and specs (embodied inside javaScene) to Forge domains, literals, and bounds (embodied inside forgeScene).

Author:
Aleksandar Milicevic

Definition at line 74 of file ForgeConverter.java.

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.engine.ForgeConverter.ForgeConverter ( SquanderReporter  reporter,
Object...  heapRootObjects 
)
Parameters:
heapRootObjects heap root objects

Definition at line 89 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.heap, and edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene().

Member Function Documentation

Iterable<Integer> edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts (  ) 

Definition at line 302 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.ints, edu.mit.csail.sdg.squander.spec.ForgeScene.isEnsureAllInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt().

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

Object edu.mit.csail.sdg.squander.engine.ForgeConverter.atom2obj ( ForgeAtom  atom  ) 

Converts the given Forge atom back to Java object

Definition at line 383 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.mapToBoolean(), edu.mit.csail.sdg.squander.engine.ForgeConverter.mapToInt(), and edu.mit.csail.sdg.squander.spec.ForgeScene.objForLit().

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertToObjTuple().

void edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff (  )  [private]

Definition at line 489 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound(), edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.spec.JavaScene.caller, edu.mit.csail.sdg.squander.spec.ForgeScene.consts, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.spec.JavaScene.methodArgs, and edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar.

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

void edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields ( IEvaluator  eval  ) 

Call this method after executing the precondition spec and before executing the postcondition spec to bound the values of spec fields in the pre-state.

Definition at line 118 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound(), edu.mit.csail.sdg.squander.engine.ForgeConverter.conv2fc(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), and edu.mit.csail.sdg.squander.spec.JavaScene.specFields().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeMethod().

ForgeConstant edu.mit.csail.sdg.squander.engine.ForgeConverter.conv2fc ( ObjTupleSet  objTupleSet,
ForgeBounds  bounds 
)

Converts a given tuple set to Forge constant

Definition at line 434 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, and edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2atom().

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds().

void edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects ( MethodSpec  ms  )  [private]

Definition at line 190 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.Heap.addObject(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingFreshObjects(), edu.mit.csail.sdg.squander.spec.MethodSpec.freshObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap, edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2typeparams, and edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter.

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

ObjTupleSet edu.mit.csail.sdg.squander.engine.ForgeConverter.extent ( ForgeType  t  ) 

Definition at line 359 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().

List<InstanceLiteral> edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType ( ForgeType.Unary  colType  ) 

Definition at line 320 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.instLitsCache, and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits().

List<ForgeLiteral> edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType ( ForgeType.Unary  colType  ) 

Returns all Forge literals of the given unary Forge type

Definition at line 338 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.litsCache, and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.nextAtomForLiteral(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processFirst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreEmpty(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.sort(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().

void edu.mit.csail.sdg.squander.engine.ForgeConverter.finish (  )  [private]

Definition at line 140 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), edu.mit.csail.sdg.squander.engine.SquanderReporter.end(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.ensureAdequateIntBitWidth(), edu.mit.csail.sdg.squander.annotations.Options.ensureAllInts(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts, edu.mit.csail.sdg.squander.spec.ForgeScene.ensureInt(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.Heap.getHeapObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.getMaxAtomsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap, edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.spec.JavaScene.method, edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec(), edu.mit.csail.sdg.squander.spec.ForgeScene.numTypes, edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2typeparams, edu.mit.csail.sdg.squander.spec.MethodSpec.options, edu.mit.csail.sdg.squander.engine.ForgeConverter.printUniverseStats(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.reachableObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter, edu.mit.csail.sdg.squander.spec.JavaScene.translateSpecs(), edu.mit.csail.sdg.squander.engine.SquanderReporter.translatingSpecs(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.traverse(), and edu.mit.csail.sdg.squander.engine.SquanderReporter.traversingHeap().

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

ForgeBounds edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds (  ) 

Definition at line 133 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, and edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds().

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

SolveOptions edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeOptions (  ) 

Definition at line 292 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, and edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec().

ForgeScene edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene (  ) 

Definition at line 131 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.atom2obj(), edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec(), edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize(), edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2atom(), edu.mit.csail.sdg.squander.engine.ForgeConverter.printObjSet(), edu.mit.csail.sdg.squander.engine.ForgeConverter.printUniverseStats(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

int edu.mit.csail.sdg.squander.engine.ForgeConverter.getMaxAtomsForType ( ForgeType  ft  )  [private]

Definition at line 207 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.maxAtomsCache, and edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize().

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

Spec edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec (  ) 

Definition at line 284 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.spec.Spec.addCase(), edu.mit.csail.sdg.squander.spec.MethodSpec.cases, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.spec.MethodSpec.isHelper(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), and edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.getSpec().

Heap2Bounds edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit (  ) 

Definition at line 132 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, and edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds().

void edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene (  )  [private]

Definition at line 462 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap, edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.engine.SquanderReporter.loadingJavaScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter, and edu.mit.csail.sdg.squander.serializer.AbstractHeap.serialize().

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

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

Definition at line 130 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.ForgeConverter(), edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec(), edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

Object edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj ( ForgeLiteral  lit  ) 

Converts the given Forge literal back to Java object

Definition at line 398 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.objForLit().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.KodkodIntEval.makeConst(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreEmpty(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().

ForgeBounds edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds ( Heap2Bounds  heap2lit  )  [private]

Definition at line 514 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.bounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.conv2fc(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingBounds(), edu.mit.csail.sdg.squander.spec.ForgeScene.domains(), edu.mit.csail.sdg.squander.spec.ForgeScene.findVar(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.minBW(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter.

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

static Object edu.mit.csail.sdg.squander.engine.ForgeConverter.mapToBoolean ( final ForgeAtom  atom  )  [static]

Definition at line 410 of file ForgeConverter.java.

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

static int edu.mit.csail.sdg.squander.engine.ForgeConverter.mapToInt ( final ForgeAtom  atom  )  [static]

Definition at line 414 of file ForgeConverter.java.

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

int edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt (  ) 

Returns the min int within the bounds

Definition at line 425 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, and edu.mit.csail.sdg.squander.engine.Heap2Bounds.minBW().

Referenced by edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound.allInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse().

int edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize ( ForgeDomain  d  )  [private]

Definition at line 225 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.ints, edu.mit.csail.sdg.squander.spec.ForgeScene.isEnsureAllInts(), and edu.mit.csail.sdg.squander.spec.ForgeScene.numLiteralsFor().

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

int edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt (  ) 

Returns the min int within the bounds

Definition at line 419 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, and edu.mit.csail.sdg.squander.engine.Heap2Bounds.minBW().

Referenced by edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound.allInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse().

ForgeAtom edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2atom ( Object  obj,
ForgeBounds  bounds 
)

Returns the Forge atom corresponding to the given Java object

Definition at line 448 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), and edu.mit.csail.sdg.squander.spec.ForgeScene.nullLit.

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

String edu.mit.csail.sdg.squander.engine.ForgeConverter.printBounds (  ) 

Definition at line 239 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.bounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit, and edu.mit.csail.sdg.squander.engine.ForgeConverter.printObjSet().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.checkPre(), and edu.mit.csail.sdg.squander.engine.SquanderImpl.ensurePost().

String edu.mit.csail.sdg.squander.engine.ForgeConverter.printObjSet ( ObjTupleSet  objSet  )  [private]

Definition at line 247 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.forgeLitForObj(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

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

String edu.mit.csail.sdg.squander.engine.ForgeConverter.printUniverseStats (  )  [private]

Definition at line 539 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

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

ForgeProcedure edu.mit.csail.sdg.squander.engine.ForgeConverter.proc (  ) 

Definition at line 267 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.spec.JavaScene.method, edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec(), edu.mit.csail.sdg.squander.spec.JMethod.name(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, and edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec().

void edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext ( Object  caller,
JMethod  m,
Object[]  methodArgs 
)

Use this method to set the specification of a method to be executed

Definition at line 98 of file ForgeConverter.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.spec.JavaScene.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finished, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2typeparams, edu.mit.csail.sdg.squander.spec.JMethod.paramTypes(), edu.mit.csail.sdg.squander.spec.JavaScene.setArgs(), edu.mit.csail.sdg.squander.spec.JavaScene.setCaller(), edu.mit.csail.sdg.squander.spec.JavaScene.setMethod(), and edu.mit.csail.sdg.squander.spec.JMethod.spec.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeMethod().

Member Data Documentation

Set<Integer> edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts = null [private]

Definition at line 301 of file ForgeConverter.java.

boolean edu.mit.csail.sdg.squander.engine.ForgeConverter.finished = false [private]

Definition at line 84 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeOptions(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt(), edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

ForgeBounds edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds [private]

Definition at line 82 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs().

ForgeScene edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene [private]

Definition at line 79 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound.allInts(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getModsForPostState(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue(), edu.mit.csail.sdg.squander.engine.SquanderResult.getSpecField(), edu.mit.csail.sdg.squander.engine.SquanderResult.program(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreEmpty(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreJavaHeap(), edu.mit.csail.sdg.squander.engine.SquanderResult.returnVar(), and edu.mit.csail.sdg.squander.engine.SquanderResult.self().

final Heap edu.mit.csail.sdg.squander.engine.ForgeConverter.heap [private]

Definition at line 77 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.ForgeConverter(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene().

Heap2Bounds edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2lit [private]

Definition at line 81 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt(), edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.printBounds().

Map<ForgeType.Unary, List<InstanceLiteral> > edu.mit.csail.sdg.squander.engine.ForgeConverter.instLitsCache = new HashMap<ForgeType.Unary, List<InstanceLiteral>>() [private]

Definition at line 319 of file ForgeConverter.java.

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

final JavaScene edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene [private]

Definition at line 78 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), and edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue().

Map<ForgeType.Unary, List<ForgeLiteral> > edu.mit.csail.sdg.squander.engine.ForgeConverter.litsCache = new HashMap<ForgeType.Unary, List<ForgeLiteral>>() [private]

Definition at line 336 of file ForgeConverter.java.

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

Map<ForgeType, Integer> edu.mit.csail.sdg.squander.engine.ForgeConverter.maxAtomsCache = new HashMap<ForgeType, Integer>() [private]

Definition at line 205 of file ForgeConverter.java.

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

Map<Object, JType.Unary[]> edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2typeparams = new IdentityHashMap<Object, Unary[]>() [private]

Definition at line 188 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

final SquanderReporter edu.mit.csail.sdg.squander.engine.ForgeConverter.reporter [private]

Definition at line 76 of file ForgeConverter.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeOptions(), edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds().

The documentation for this class was generated from the following file:
Generated by  doxygen 1.6.2-20100208