edu.ucsb.ccs.jcontractor.transformation
Class ContractCheckTransformation

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 $

Author:

Parker Abercrombie

See Also:

jContractorRuntime

Constructor Summary

ContractCheckTransformation()

Method Summary

boolean	acceptClass() Determine if a class should be processed.
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

canCheckEntryInvariant, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInvariant, canHavePostcondition, canHavePrecondition, canReferenceOld, contractsCheckable, getContractClassName, getContractClassName, getInvariantMethodName, getInvariantMethodSignature, getPostconditionMethodName, getPostconditionMethodSignature, getPreconditionMethodName, getPreconditionMethodSignature, isContractClass, isContractMethod, isInvariantMethod, isPostconditionMethod, isPreconditionMethod

Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation

getTransformer, setTransformer, transform

Methods inherited from class java.lang.Object

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

Constructor Detail

ContractCheckTransformation

public ContractCheckTransformation()

Method Detail

acceptClass

public boolean acceptClass()

Determine if a class should be processed. All classes in which contracts are checkable are processed.

Overrides:

acceptClass in class Transformation

Returns:

true if contracts are checkable in javaclass.

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.

Parameters:

mg - the method being instrumented. The value of this method's arguments at the time of failure will be included in the exception message.

errorMsg - a specialized message to include in the exception message.

Returns:

an InstructionList to push an informative exception message onto the stack. This list should be inserted before the code to call the exception's constructor.

transformClass

public void transformClass()

Does nothing. This transformation operates only on methods.

Overrides:

transformClass in class Transformation