|Home >> All >> edu >> ucsb >> ccs >> jcontractor >> [ transformation Javadoc ]|
edu.ucsb.ccs.jcontractor.transformation: Javadoc index of package edu.ucsb.ccs.jcontractor.transformation.
ContractCheckTransformation: A transformation to insert a call to the contract method into a non-contract method. The details of inserting the check are left to descendents (whether to insert the check at the beginning or end of the method, for example). This class defines the buildContractCheck(MethodGen, MethodGen, InstructionList, String, String) method, that creates an instruction list that will call a contract method, and throw an exception if the method returns false. The Assertion Evaluation Rule states that when a function is called while evaluating a contract, the contracts of that function should not be evaluated. ...
PreconditionMethodTransformation: A transformation to prepare precondition methods. For each non-contract method in a class, the transformation searches for a precondition method. The precondition method is modified to call the superclass precondition method before evaluation, and inlined versions of preconditions inherited from interfaces, and the external precondition defined in a contract class are added. The superclass precondition is logical or-ed with the interface conditions, and the subclass precondition. The subclass precondition is constructed by and-ing the in-class precondition with the external precondition. If no ...
ReplaceReturnInstructionsTransformation: A transformation to replace all the return statements in a non-contract methods with a jump to the end of the method, so that exit condition checking code may be appended to the instruction list. The transformation is only neccessary when an exit condition needs to be checked, so it only modifies methods for which either the postcondition or the exit invariant is checkable. The transformation also saves the method's return value to a local variable, and makes the index of this variable available to subsequent transformations (AppendReturnTransformation, in particular, needs it). The index is saved ...
PostconditionMethodTransformation: A transformation to prepare postcondition methods. For each non-contract method in a class, the transformation searches for a postcondition method. The postcondition method is modified to call the superclass postcondition method before evaluation, and inlined versions of postconditions inherited from interfaces, and the external postcondition defined in a contract class are added. All of these are logical and-ed, so that the postcondition may be strengthened, but not weakened. If no postcondition method was found, a default postcondition method is added to the class. The default method just calls ...
AppendReturnTransformation: A transformation to append code to load the method's result from a local variable, and return. This must be done after processing with ReplaceReturnInstructionTransformation. This transformation requires that ReplaceReturnInstructionTransformation has saved the method's return value to a local variable, and placed the index of this variable into the shared data table. This transformation is only required where ReplaceReturnInstructionTransformation is required, so it transforms only methods for which either the postcondition or exit invariant is checkable. Before: After: ----------- -------------- ...
InvariantMethodTransformation: A transformation to prepare invariant methods. For each class, the transformation searches for an invariant method. The invariant method is modified to call the superclass invariant method before evaluation, and inlined version of invariants inherited from interfaces, and the external invariant defined in a contract class are added. All of these are logical and-ed, so that the invariant may be strengthened, but not weakened. If no invariant method was found, a default invariant method is added to the class. The invariant method in its final form looks something like this: return <interface1 ...
PreconditionCheckTransformation: A transformation to insert code to check the precondition of each method by calling method_Precondition . This transformation requires that PreconditionMethodTransformation has already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. One note on constructors: Because call to the super class constructor is required to be the first statement of the constructor, preconditions are checked immediatly after the super class constructor call, not at method entry. This transformation depends on: PreconditionMethodTransformation
LockCloneTransformation: Transformation to disable contract checking while in the clone() method. clone() is used to implement OLD references, and checking contracts on method called from clone() could require more calls to clone() . This leads to infinite recursion, which would be bad. To prevent this scenario, jContractor does not check contracts on any methods called from clone() . Note: Strictly speaking, all that is required is to not check contracts that refer to OLD. However, just supressing all contract checks is much easier to implement.
LoadContractClassTransformation: A transformation that loads the contract class for the transformed class into the Repository so that it will be available to subsequent transformations. The contract class has a "_CONTRACT" suffix (as in "MyClass" and "MyClass_CONTRACT"), and defines contracts for another class. Before inserting code to check the contracts, the contract class needs to be accessible in the Repository. This transformation should be run before transformations requiring access to the contract class. The transformation does not modify the current class or any of it's methods.
InvariantCheckTransformation: A transformation to insert code to check the invariant of each method by calling _Invariant . This transformation requires that InvariantMethodTransformation and ReplaceReturnInstructionsTransformation have already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. In most methods, the invariant is checked at both entry and exit. This transformation depends on: InvariantMethodTransformation ReplaceReturnInstructionsTransformation
PostconditionCheckTransformation: A transformation to insert code to check the postcondition of each method by calling method_Postcondition . This transformation requires that PostconditionMethodTransformation and ReplaceReturnInstructionsTransformation have already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. This transformation depends on: PreconditionMethodTransformation ReplaceReturnInstructionsTransformation
ClassTransformer: A ClassTransformer executes a complex transformation on a JavaClass object. The complex transform is made up of simpler transforms that are carried out in sequence on the class itself and on each method. Transformations are stored as a list, and are executed in the order that they appear. The list may be modified with insert(Transformation) and append(Transformation) . Use the transform(JavaClass) method to apply the transformations to a class.
ContractTransformation: Abstract super class for contract transformations. This class defines methods that determine the names and signatures of contract methods, and defines the rules about which methods may have which sorts of contracts, and when contracts are checked. Logic about the naming conventions used by jContractor, and about the rules of when contracts can be checked is encapsulated in this class. This class also defines several utility methods that are useful for working with InstructionLists.
ContractMethodTransformation: Superclass for transformations that modify contract methods. Contract methods need to be modified to check superclass contracts, external contracts, and contracts inherited from interfaces. This class provides methods to check these contracts, and to combine contract checks by and-ing or or-ing them together. This transformation depends on: LoadContractClassTransformation
ReplaceOldReferencesTransformation: Transformation to replace references to OLD in postconditions. The old state is saved on a stack in jContractorRuntime, so the postcondition needs to pop the saved state, and store it to a local variable (storing to the OLD instance variable wouldn't be thread safe). Each reference to the OLD instance variable needs to be changed to a reference to the local variable.
RemoveContractMethodsTransformation: Transformation to remove the contract methods from a class, to decrease the size of the bytecode. Once contract checks are inserted, the class becomes dependant on its contract methods to run correctly. For this reason it is not safe remove the contract methods from an instrumented class.
Transformation: Abstract description of a transformation that can be applied to a class. Each transformation is attached to a ClassTransformer, which holds data about the class being transformed, and provides a means for different transformations to share information.
InstrumentedFlagTransformation: A transformation to insert a flag constant into the constant pool of a class to mark the class as instrumented. This constant consists of jInstrument.JCONTRACTOR_FLAG_CONSTANT concatenated with the class name.
MarkInstrumentedTransformation: A transformation to insert a flag constant into the constant pool of a class to mark the class as instrumented. This constant consists of jInstrument.JCONTRACTOR_FLAG_CONSTANT concatenated with the class name.
SaveOldStateTransformation: This transformation adds code to postconditions that refer to old to call to clone an object, and push the clone onto the stack of saved instances in jContractorRuntime.
AbortTransformationException: An exception that will be thrown by a Transformation when an error occurs that requires that the ClassTransformer abort all subsequent transformations.
MethodSet: A simple container to hold MethodGen objects. Basically, just a specialized hashtable.