java.lang.Object
edu.ucsb.ccs.jcontractor.transformation.Transformation
edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation
- Direct Known Subclasses:
- InvariantCheckTransformation, PostconditionCheckTransformation, PreconditionCheckTransformation
- public abstract class ContractCheckTransformation
- extends ContractTransformation
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. This avoids infinite recursion of
contract checks, among other things. The before calling a
contract, the jContractorRuntime is consulted to see if the
current thread is already evaluating something. If so, the
contract is ignored. If not, the assertion check status is locked
in the jContractorRuntime, the contract is checked, and the
check status is unlocked.
It should be possible to create contract checking code with no
further knowledge of the inner workings of this class, but for the
curious, and those poor souls who have to maintain this code, here's
an example of some contract checking code. Consider the everyone's
favorite hypothetical method:
public void foo (int arg1, int arg2) { ... }
Here's what a precondition check would look like in high level
code:
try {
if (jContractorRuntime.canCheckAssertion()) {
jContractorRuntime.lockAssertionCheck();
if (!foo_Precondition(arg1, arg2)) {
throw new PreconditionViolationError("Precondition Violated"
+ " when foo(" + arg1 + ", "
+ arg2 + ")");
}
}
} catch (Throwable t) {
jContractorRuntime.releaseAssertionCheck();
}
In bytecode, we get something like this:
63: invokestatic edu.ucsb.ccs.jcontractor.jContractorRuntime.releaseAssertionCheck ()V (49)
69: invokestatic edu.ucsb.ccs.jcontractor.jContractorRuntime.canCheckAssertion ()Z (42)
72: ifeq #134
78: invokestatic edu.ucsb.ccs.jcontractor.jContractorRuntime.lockAssertionCheck ()V (46)
81: aload_0
82: iload_1
83: iload_2
84: invokevirtual Test.foo_Precondition (II)Z (36)
87: ifne #128
90: new (57)
93: dup
94: new (59)
97: dup
98: ldc "jContractor Exception: Precondition Violated\nwhen: foo(" (77)
100: invokespecial java.lang.StringBuffer. (Ljava/lang/String;)V (64)
103: iload_1
104: invokevirtual java.lang.StringBuffer.append (I)Ljava/lang/StringBuffer; (80)
107: ldc ", " (82)
109: invokevirtual java.lang.StringBuffer.append (Ljava/lang/String;)Ljava/lang/StringBuffer; (70)
112: iload_2
113: invokevirtual java.lang.StringBuffer.append (I)Ljava/lang/StringBuffer; (80)
116: ldc ")" (66)
118: invokevirtual java.lang.StringBuffer.append (Ljava/lang/String;)Ljava/lang/StringBuffer; (70)
121: invokevirtual java.lang.StringBuffer.toString ()Ljava/lang/String; (74)
124: invokespecial edu.ucsb.ccs.jcontractor.PreconditionViolationError. (Ljava/lang/String;)V
(75)
127: athrow
- Version:
- $Id: ContractCheckTransformation.java,v 1.12 2002/07/14 07:40:59 parkera Exp $
Method Summary |
boolean |
acceptClass()
Determine if a class should be processed. |
protected boolean |
buildContractCheck_Precondition(org.apache.bcel.generic.MethodGen noncontractMethod,
org.apache.bcel.generic.MethodGen contractMethod,
org.apache.bcel.generic.InstructionList loadArgs,
java.lang.String exceptionClassName,
java.lang.String exceptionMessage)
|
protected org.apache.bcel.generic.InstructionList |
buildContractCheck(org.apache.bcel.generic.MethodGen noncontractMethod,
org.apache.bcel.generic.MethodGen contractMethod,
org.apache.bcel.generic.InstructionList loadArgs,
java.lang.String exceptionClassName,
java.lang.String exceptionMessage)
Build an instruction list to check the contract and throw an
exception if it fails. |
protected boolean |
createPushExceptionMessage_Precondition(org.apache.bcel.generic.MethodGen method,
java.lang.String errorMessage)
|
org.apache.bcel.generic.InstructionList |
createPushExceptionMessage(org.apache.bcel.generic.MethodGen mg,
java.lang.String errorMsg)
Build an exception message string, and push it onto the stack. |
void |
transformClass()
Does nothing. |
Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation |
append, canCheckEntryInvariant, canCheckExitInvariant_Precondition, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInheritedContract_Precondition, canHaveInheritedContract, canHaveInvariant_Precondition, canHaveInvariant, canHavePostcondition_Precondition, canHavePostcondition, canHavePrecondition_Precondition, canHavePrecondition, canReferenceOld_Precondition, canReferenceOld, contractsCheckable_Precondition, contractsCheckable, createLoadArguments_Postcondition, createLoadArguments_Precondition, createLoadArguments, entryInvariantCheckable_Precondition, findMethod, findMethod, findMethodIndex, getContractClassName_Postcondition, getContractClassName_Postcondition, getContractClassName_Precondition, getContractClassName_Precondition, getContractClassName, getContractClassName, getInvariantMethodName_Postcondition, getInvariantMethodName_Precondition, getInvariantMethodName, getInvariantMethodSignature_Postcondition, getInvariantMethodSignature_Precondition, getInvariantMethodSignature, getPostconditionMethodName_Postcondition, getPostconditionMethodName_Precondition, getPostconditionMethodName, getPostconditionMethodSignature_Postcondition, getPostconditionMethodSignature_Precondition, getPostconditionMethodSignature, getPreconditionMethodName_Postcondition, getPreconditionMethodName_Precondition, getPreconditionMethodName, getPreconditionMethodSignature_Postcondition, getPreconditionMethodSignature_Precondition, getPreconditionMethodSignature, hasExternalContract, hasInterfaceContract, hasSuperClassContract, isContractClass_Postcondition, isContractClass_Precondition, isContractClass, isContractMethod_Postcondition, isContractMethod_Precondition, isContractMethod, isInvariantMethod_Precondition, isInvariantMethod, isPostconditionMethod_Postcondition, isPostconditionMethod, isPreconditionMethod_Precondition, isPreconditionMethod, postconditionCheckable_Precondition, preconditionCheckable_Precondition, prepend, prependToConstructor_Precondition, prependToConstructor, replaceInstruction, replaceInstruction, replaceReturnInstructions_Precondition, replaceReturnInstructions |
Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation |
acceptClass_Precondition, getTransformer_Postcondition, getTransformer, setTransformer_Postcondition, setTransformer_Precondition, setTransformer, transform_Precondition, transform, transformClass_Precondition, transformMethod_Precondition, transformMethod |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
ContractCheckTransformation
public ContractCheckTransformation()
acceptClass
public boolean acceptClass()
- Determine if a class should be processed. All classes in which
contracts are checkable are processed.
- Specified by:
acceptClass
in class Transformation
buildContractCheck
protected org.apache.bcel.generic.InstructionList buildContractCheck(org.apache.bcel.generic.MethodGen noncontractMethod,
org.apache.bcel.generic.MethodGen contractMethod,
org.apache.bcel.generic.InstructionList loadArgs,
java.lang.String exceptionClassName,
java.lang.String exceptionMessage)
- Build an instruction list to check the contract and throw an
exception if it fails. The exception is created with an
informative message telling what what went wrong, what function
was executing, and what the arguments to that function were. The
contract is inserted into method's instruction list; that task is
left to the descendents of this class.
buildContractCheck_Precondition
protected boolean buildContractCheck_Precondition(org.apache.bcel.generic.MethodGen noncontractMethod,
org.apache.bcel.generic.MethodGen contractMethod,
org.apache.bcel.generic.InstructionList loadArgs,
java.lang.String exceptionClassName,
java.lang.String exceptionMessage)
createPushExceptionMessage
public org.apache.bcel.generic.InstructionList createPushExceptionMessage(org.apache.bcel.generic.MethodGen mg,
java.lang.String errorMsg)
- Build an exception message string, and push it onto the stack.
The message includes the name of the method in which the contract
was violated, and the values of the methods arguments.
createPushExceptionMessage_Precondition
protected boolean createPushExceptionMessage_Precondition(org.apache.bcel.generic.MethodGen method,
java.lang.String errorMessage)
transformClass
public void transformClass()
- Does nothing. This transformation operates only on methods.
- Specified by:
transformClass
in class Transformation