envgen.codegen
Class JavaDriverGenerator

java.lang.Object
  |
  +--envgen.codegen.AbstractDriverGenerator
        |
        +--envgen.codegen.JavaDriverGenerator

All Implemented Interfaces:

ICodeGenerator

Direct Known Subclasses:

LTLDriverGenerator, REDriverGenerator, UniversalDriverGenerator

public abstract class JavaDriverGenerator

extends AbstractDriverGenerator

Generates java drivers.

Field Summary

(package private) boolean	atomicStepsMode Set to insert atomic steps into the generated environment.
(package private) java.util.List	defaultInstantiations
(package private) java.util.List	defaultPropositions

Fields inherited from class envgen.codegen.AbstractDriverGenerator

debug, envTable, unitInterface, unitTable, userSpec

Constructor Summary

JavaDriverGenerator()

Method Summary

protected JavaStmt	genAssignmentStmt(Assignment a) Constructs a Java statement for a method call, including atomic steps around the call, print out of the action label, and try-catch clause if the method invoked throws exceptions.
protected JavaStmt	genAtomicPropStmt(JavaStmt stmt) Creates a method call statement surrounded by endAtomic/beginAtomic method invocations.
abstract void	genMainFromSpec(soot.util.Chain units)
soot.Body	genMainRunBody()
void	genMainThread() Constructs EnvDriver soot class, the main driver that starts up threads.
protected JavaStmt	genMethodStmt(MethodCall mc) Constructs a Java statement for a method call, including atomic steps around the call, print out of the action label, and try-catch clause if the method invoked throws exceptions.
protected JavaStmt	genPropositionStmt(Proposition prop)
protected soot.SootClass	genThreadBasics(java.lang.String threadName) Creates a soot class threadName with a constructor as a base for synthesized thread construction methods.
soot.Body	genThreadConstructorBody(soot.SootClass driverThread, soot.SootMethod method)
protected JavaStmt	genTryCatchStmt(JavaStmt methodCall) Incloses methodCall by a try-catch clause.

Methods inherited from class envgen.codegen.AbstractDriverGenerator

genCode, genThreads

Methods inherited from class java.lang.Object

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

Field Detail

defaultPropositions

java.util.List defaultPropositions

defaultInstantiations

java.util.List defaultInstantiations

atomicStepsMode

boolean atomicStepsMode

Set to insert atomic steps into the generated environment.

Constructor Detail

JavaDriverGenerator

public JavaDriverGenerator()

Method Detail

genMainThread

public void genMainThread()

Constructs EnvDriver soot class, the main driver that starts up threads.

Specified by:

genMainThread in class AbstractDriverGenerator

genMainRunBody

public soot.Body genMainRunBody()

genMainFromSpec

public abstract void genMainFromSpec(soot.util.Chain units)

genThreadBasics

protected soot.SootClass genThreadBasics(java.lang.String threadName)

Creates a soot class threadName with a constructor as a base for synthesized thread construction methods.

genThreadConstructorBody

public soot.Body genThreadConstructorBody(soot.SootClass driverThread,
                                          soot.SootMethod method)

genPropositionStmt

protected JavaStmt genPropositionStmt(Proposition prop)

genMethodStmt

protected JavaStmt genMethodStmt(MethodCall mc)

Constructs a Java statement for a method call, including atomic steps around the call, print out of the action label, and try-catch clause if the method invoked throws exceptions.

genAssignmentStmt

protected JavaStmt genAssignmentStmt(Assignment a)

Constructs a Java statement for a method call, including atomic steps around the call, print out of the action label, and try-catch clause if the method invoked throws exceptions.

genAtomicPropStmt

protected JavaStmt genAtomicPropStmt(JavaStmt stmt)

Creates a method call statement surrounded by endAtomic/beginAtomic method invocations.

genTryCatchStmt

protected JavaStmt genTryCatchStmt(JavaStmt methodCall)

Incloses methodCall by a try-catch clause.