JML

org.jmlspecs.jmlrac
Class ConstructorWrapper

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.WrapperMethod
              extended byorg.jmlspecs.jmlrac.ConstructorWrapper
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants

public class ConstructorWrapper
extends WrapperMethod

A class for generating constructor wrappers. A constructor wrapper is a constructor that wraps a constructor with assertion check methods such as pre and postcondition check methods. The constructor under wrapping becomes a private method and called by the wrapper.

Version:
$Revision: 1.24 $
Author:
Yoonsik Cheon
See Also:
TransConstructor

Field Summary
 
Fields inherited from class org.jmlspecs.jmlrac.WrapperMethod
args, ident, isHelper, isStatic, methodDecl, postArgs, returnType, typeName, xpostArgs
 
Fields inherited from class org.jmlspecs.jmlrac.TransUtils
typeDecl
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Fields inherited from interface org.jmlspecs.jmlrac.RacConstants
MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT
 
Fields inherited from interface org.jmlspecs.checker.Constants
ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
ConstructorWrapper(String typeName, JmlConstructorDeclaration mdecl)
          Construct a new instance.
 
Method Summary
private  JBlock buildWrapperBody(JExpression explicitSuper)
          Returns a body for the constructor wrapper being built.
protected  String callOriginalMethod()
          Returns code for invoking the now-renamed original constructor.
protected  String checkConstraint()
          Returns code for checking history constraints.
protected  String checkPostcondition()
          Returns code for checking normal postcondition.
protected  String checkPostInstanceInvariant()
          Returns code for checking instance invariant in the post-state.
protected  String checkPostInvariant()
          Returns code for checking invariant in the post-state.
protected  String checkPostStaticInvariant()
          Returns code for checking static invariant in the post-state.
protected  String checkPrecondition()
          Returns code for checking precondition.
protected  String checkPreInvariant()
          Returns code for checking invariant in the pre-state.
protected  String checkXPostcondition()
          Returns code for checking exceptional postcondition.
protected  String evalOldInConstraint()
          Returns code for evaluating old expressions in static constraint.
 JMethodDeclarationType generate()
          Returns a constructor wrapper for the given constructor declaration.
protected  String identification(String state)
          Returns a string that identifies the method being translated.
protected  String isActive(String type)
          Returns a string representation of the condition that tests if the given type of assertion is active.
protected  String nocheckDuringInit()
          Returns code for bypassing assertion checks during the class and instance initialization.
 
Methods inherited from class org.jmlspecs.jmlrac.WrapperMethod
buildArguments, buildWrapperBody, constraintCallArg, mandatoryReturn, optionalReturn, racMethodName, resultVarDecl, wrap, wrap2, wrap3
 
Methods inherited from class org.jmlspecs.jmlrac.TransUtils
applyBigintBinOperator, applyBigintCast, applyBigintToNumber, applyBigintUnOperator, applyUnaryPromoteExpression, beingTested, createBigintConvertionAssertion, defaultValue, dynamicCallName, evalOldName, evalOldName, evalOldName, evalOldName, excludedFromInheritance, getTypeID, initIncludedInInheritance, invariantLikeName, isBigintArray, isMain, modelPublicAccessorName, numberToBigint, specAccessorNeeded, specPublicAccessorName, subtypeConstraintName, toPrintableString, toString, toString, toString, typeToClass, unwrapObject, useReflection, wrappedValue, wrapValue
 
Methods inherited from class org.multijava.util.Utils
assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ConstructorWrapper

public ConstructorWrapper(String typeName,
                          JmlConstructorDeclaration mdecl)
Construct a new instance.

 requires typeName != null && mdecl != null;
 

Parameters:
mdecl - constructor to be wrapped
Method Detail

generate

public JMethodDeclarationType generate()
Returns a constructor wrapper for the given constructor declaration. The constructor body is replaced by a new block of code that forwards constructor calls to the orginal constructor (which now becomes a private method) and performs appropriate assertion checks (such as pre- and postoncodition checks) before and after forwarding. The new body looks something like the following:
 C(T1 x1, ..., Tn xn) {
   checkPre(x1, ..., xn);
   try {
     internal(x1, ..., xn);
     checkPost(x1, ..., xn);
   }
   catch (JMLEntryPreconditionError e) {
     throw new JMLInternalPreconditionError(e); 
   }
   catch (JMLAssertionError e) {
     throw e;
   }
   catch (Throwable e) {
     checkXPost(x1, ..., xn, e);
   }
   finally {
     checkInv(x1, ..., xn);
 }
 

 also
   modifies methodDecl.*;
   accessible methodDecl;
   ensures \result != null;
 

Overrides:
generate in class WrapperMethod

buildWrapperBody

private JBlock buildWrapperBody(JExpression explicitSuper)
Returns a body for the constructor wrapper being built. Refers to the method generate() for the structure of the constructor body.

 assignable args, postArgs, xpostArgs;
 accessible methodDecl;
 ensures \result != null;
 

Parameters:
explicitSuper - explicit super/this call to be added as the first statement of the body to be built; if null, no such call is added.
See Also:
generate(), WrapperMethod.buildWrapperBody()

nocheckDuringInit

protected String nocheckDuringInit()
Returns code for bypassing assertion checks during the class and instance initialization. The returned code has the following structure.
  if (!VN_CLASS_INIT || !VN_INIT) {
     T(x1, ..., xn);
     return;
  }
 

Overrides:
nocheckDuringInit in class WrapperMethod

checkPrecondition

protected String checkPrecondition()
Returns code for checking precondition. The precondition is always checked. The returned code has the following structure.
  // check precondition
  if (JMLChecker.isActive(JMLChecker.PRECONDITION)) {
    JMLChecker.enter();
    checkPre$$init$$T(x1,...,xn);
    JMLChecker.exit();
  }
 
where T is the name of target type.

Overrides:
checkPrecondition in class WrapperMethod
See Also:
WrapperMethod.checkPrecondition()

checkPreInvariant

protected String checkPreInvariant()
Returns code for checking invariant in the pre-state. Constructors should preserve static invariants, and have to establish non-static invariants. However, helpers are exempted from the obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.
  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
 
where T is the name of type being translated.

Overrides:
checkPreInvariant in class WrapperMethod

checkPostInvariant

protected String checkPostInvariant()
Returns code for checking invariant in the post-state. Constructors should preserve static invariants, and have to establish non-static invariants. However, helpers are exempted from the obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.
  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated.

Overrides:
checkPostInvariant in class WrapperMethod

checkPostInstanceInvariant

protected String checkPostInstanceInvariant()
Returns code for checking instance invariant in the post-state. Constructors have to establish non-static invariants. However, helpers are exempted from this obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated.


checkPostStaticInvariant

protected String checkPostStaticInvariant()
Returns code for checking static invariant in the post-state. Constructors should preserve static invariants. However, helpers are exempted from this obligation. Thus, for helpers, an empty string isq returned, and for non-helpers, the following form of code is returned.
  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
 


evalOldInConstraint

protected String evalOldInConstraint()
Returns code for evaluating old expressions in static constraint. All non-helper constructors must preserve static constraints, but not instance constraints. Thus, an empty string is returned for helpers, and the following form of code for non-helpers.
  // eval old exprs in static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$satic(); 
    JMLChecker.exit();
  }
 
where T is the name of type being translated.

Overrides:
evalOldInConstraint in class WrapperMethod

checkConstraint

protected String checkConstraint()
Returns code for checking history constraints. All non-helper constructors must preserve static constraints, but not instance constraints. Thus, an empty string is returned for helpers, and the following form of code for non-helpers.
  // check static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$static();
    JMLChecker.exit();
  }
 
where T is the name of type being translated.

Overrides:
checkConstraint in class WrapperMethod

callOriginalMethod

protected String callOriginalMethod()
Returns code for invoking the now-renamed original constructor. I.e., internal$m(x1,...,xn);.

Overrides:
callOriginalMethod in class WrapperMethod

checkPostcondition

protected String checkPostcondition()
Returns code for checking normal postcondition. The postcondition is checked only if the object is not being constructed. The returned code has the following structure.
  // check normal postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION) 
      && rac$constructed()) {
    JMLChecker.enter();
    checkPost$$init$$T(x1,...,xn);
    JMLChecker.exit();
  }
 
where T is the name of the target type.

Overrides:
checkPostcondition in class WrapperMethod

checkXPostcondition

protected String checkXPostcondition()
Returns code for checking exceptional postcondition. The exceptional postcondition is checked only if the object is not being constructed. The returned code has the following structure.
  // check exceptional postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)
      && rac$constructed()) {
    JMLChecker.enter();
    checkXPost$$init$T(x1,...,xn,e);
    JMLChecker.exit();
  }
 
where T is the name of the target type.

Overrides:
checkXPostcondition in class WrapperMethod

isActive

protected String isActive(String type)
Returns a string representation of the condition that tests if the given type of assertion is active. Assertion checking is active only when the instance has completed its construction.

Overrides:
isActive in class WrapperMethod

identification

protected String identification(String state)
Returns a string that identifies the method being translated.

Overrides:
identification in class WrapperMethod

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.