envgen.spec
Class TypeChecker

java.lang.Object
  |
  +--envgen.spec.TypeChecker

public class TypeChecker

extends java.lang.Object

Field Summary

(package private) int	debug
(package private) java.util.List	defaultInitPropositions Unit classes used for instantiation in the universal driver as discovered by the DriverGenerator according to unit specification.
(package private) java.util.List	defaultPropositions
(package private) java.util.Hashtable	definitions
(package private) java.util.List	instantiations Unit class instantiations as defined in a specification.
(package private) ThreadSpec	mainThread
(package private) java.util.List	threads List that keeps ltl and reg expression specifications as ParserNodes.

Constructor Summary

TypeChecker(UserSpec ast, UnitInterface unitInterface)

Method Summary

protected boolean	checkArgType(java.lang.String arg, soot.Type type)
void	checkAssignmentProposition(Assignment prop) Checks the proposition used in the specification file, returns true if the proposition corresponds to a method invocation of one of the unit visible methods, returns false otherwise.
void	checkMethodProposition(MethodCall mc) Checks the proposition used in the specification file, returns true if the proposition corresponds to a method invocation of one of the unit visible methods, returns false otherwise.
void	checkProposition(Proposition prop)
java.lang.String	checkTopToken(java.lang.String arg)
protected java.lang.String	getArgs(java.lang.String args, soot.SootMethod sm)
soot.SootClass	getClass(java.lang.String type) Checks the type of the object instantiated in the "instantiations" section of the specification file, returns true if the type is found in the default instance classes, returns false otherwise.
soot.SootMethod	getMethod(java.lang.String name, java.lang.String args)
java.lang.String	getReceiver(soot.SootMethod internalMethod) If receiver is not supplied, figures out the receiver object.
soot.Type	getType(java.lang.String type) Checks the type of the object instantiated in the "instantiations" section of the specification file, returns true if the type is found in the default instance classes, returns false otherwise.
protected boolean	isPrimitiveType(java.lang.String type)
boolean	matchesSignature(java.lang.String methodName, java.lang.String args, soot.SootMethod sm)
void	typeCheck()
java.util.List	updateDefaultMethods(java.util.List defaultPublicMethods) In case of LTL, we need to intersect specification propositions with default propositions, in this case default propositions may need to be updated with label information and specific receiver information.

Methods inherited from class java.lang.Object

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

Field Detail

definitions

java.util.Hashtable definitions

defaultPropositions

java.util.List defaultPropositions

instantiations

java.util.List instantiations

Unit class instantiations as defined in a specification.

defaultInitPropositions

java.util.List defaultInitPropositions

Unit classes used for instantiation in the universal driver as discovered by the DriverGenerator according to unit specification.

threads

java.util.List threads

List that keeps ltl and reg expression specifications as ParserNodes.

mainThread

ThreadSpec mainThread

debug

int debug

Constructor Detail

TypeChecker

public TypeChecker(UserSpec ast,
                   UnitInterface unitInterface)

Method Detail

typeCheck

public void typeCheck()

checkProposition

public void checkProposition(Proposition prop)

checkMethodProposition

public void checkMethodProposition(MethodCall mc)

Checks the proposition used in the specification file, returns true if the proposition corresponds to a method invocation of one of the unit visible methods, returns false otherwise. Records the proposition in the specPropositions vector and as a proposition of the node.

checkAssignmentProposition

public void checkAssignmentProposition(Assignment prop)

Checks the proposition used in the specification file, returns true if the proposition corresponds to a method invocation of one of the unit visible methods, returns false otherwise. Records the proposition in the specPropositions vector and as a proposition of the node.

getType

public soot.Type getType(java.lang.String type)

Checks the type of the object instantiated in the "instantiations" section of the specification file, returns true if the type is found in the default instance classes, returns false otherwise.

getClass

public soot.SootClass getClass(java.lang.String type)

Checks the type of the object instantiated in the "instantiations" section of the specification file, returns true if the type is found in the default instance classes, returns false otherwise.

getMethod

public soot.SootMethod getMethod(java.lang.String name,
                                 java.lang.String args)

getReceiver

public java.lang.String getReceiver(soot.SootMethod internalMethod)

If receiver is not supplied, figures out the receiver object.

getArgs

protected java.lang.String getArgs(java.lang.String args,
                                   soot.SootMethod sm)

matchesSignature

public boolean matchesSignature(java.lang.String methodName,
                                java.lang.String args,
                                soot.SootMethod sm)

checkArgType

protected boolean checkArgType(java.lang.String arg,
                               soot.Type type)

isPrimitiveType

protected boolean isPrimitiveType(java.lang.String type)

checkTopToken

public java.lang.String checkTopToken(java.lang.String arg)

updateDefaultMethods

public java.util.List updateDefaultMethods(java.util.List defaultPublicMethods)

In case of LTL, we need to intersect specification propositions with default propositions, in this case default propositions may need to be updated with label information and specific receiver information.