org.jmlspecs.jmlrac
Class MotherConstraintMethod

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.AssertionMethod
              org.jmlspecs.jmlrac.InvariantLikeMethod
                  org.jmlspecs.jmlrac.ConstraintMethod
                      org.jmlspecs.jmlrac.MotherConstraintMethod

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

Direct Known Subclasses:

SubtypeConstraintMethod

public class MotherConstraintMethod

extends ConstraintMethod

A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes. The generated constraint methods are supposed to be called by wrapper methods and constructors. This class can generate both instance and static constraint check methods. For details on constraint check methods, refer to the class ConstraintMethod.

The class implements a variant of the Template Pattern [GoF95], prescribed in the class AssertionMethod.

Version:

$Revision: 1.5 $

Author:

Yoonsik Cheon

See Also:

AssertionMethod

Field Summary
private  List	restoreMethods           The names of the restoration methods that can restore the correct values for old expressions appearing in the constraint clause in the presence of recursive method calls.

 

Fields inherited from class org.jmlspecs.jmlrac.AssertionMethod

exceptionToThrow, isStatic, javadoc, methodIdentification, methodName, prefix, typeDecl

 

Fields inherited from class org.jmlspecs.jmlrac.TransUtils

 

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
protected	MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, String postfix, List restoreMethods)           Construct a new instance.
	MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, List restoreMethods)           Construct a new instance.

 

Method Summary
protected  StringBuffer	buildHeader(String returnType, String name, JFormalParameter[] parameters, CClassType[] exceptions)           Builds, in a string form, the header of constraint method.
protected  String	checker(boolean initValue, RacNode stmt, JFormalParameter[] params)           Returns the given constraint check code, stmt, wrapped with code to inherit supertypes's constraints.
JMethodDeclarationType	generate(RacNode stmt)           Returns a constraint check method with the given body, stmt.
protected  String	inheritAssertion(JFormalParameter[] parameters)           Return the code to inherit constraints of the superclass and interfaces, i.e., to call the constraint methods of the superclass and interfaces.
protected  String	inheritCallArgs()           Returns, in the string form, the arguments for calling supertype's constraint check method.
protected  String	inheritCallArgTypes()           Returns, in the string form, the formal parameter types of the supertype's constraint check method.
protected  String	inheritFrom(boolean isWeaksubtype, CClass clazz)           Returns code that, if executed, inherits constraints from the given type, clazz.
protected  String	nonReflectiveCall(boolean isWeakly, CClass clazz)           Return code, in the string form, that calls non-reflectively the constraint check method of the given supertype, claszz.
private static String	postfix(boolean isStatic, JmlTypeDeclaration typeDecl)           Returns the postfix to be used for constraint check method's name.
protected  String	reflectiveCall(boolean isWeakly, CClass clazz)           Return code, in the string form, that calls reflectively the constraint check method of the given supertype, claszz.

 

Methods inherited from class org.jmlspecs.jmlrac.ConstraintMethod

formalParameters

 

Methods inherited from class org.jmlspecs.jmlrac.InvariantLikeMethod

canInherit, inheritFrom, nonReflectiveCall, reflectiveCall

 

Methods inherited from class org.jmlspecs.jmlrac.AssertionMethod

hasExplicitSuperClass

 

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

 

Field Detail

restoreMethods

private List restoreMethods

The names of the restoration methods that can restore the correct values for old expressions appearing in the constraint clause in the presence of recursive method calls. Each entry of this list is a string.

 private invariant (\forall Object o; restoreMethods.contains(o);
   o instanceof String);
 

MotherConstraintMethod

public MotherConstraintMethod(boolean isStatic,
                              JmlTypeDeclaration typeDecl,
                              List restoreMethods)

Construct a new instance.

  requires (\forall Object o; restoreMethods.contains(o);
    o instanceof String);
 

Parameters:

isStatic - the kind of constraint method to generate; true for static and false for non-static (instance) constraint method.

typeDecl - the target type declaration whose constraint methods are to be generated.

restoreMethods - the names of resore methods to be used to restore the values of old expression fields.

MotherConstraintMethod

protected MotherConstraintMethod(boolean isStatic,
                                 JmlTypeDeclaration typeDecl,
                                 String postfix,
                                 List restoreMethods)

Construct a new instance.

  requires typeDecl != null;
  requires (\forall Object o; restoreMethods.contains(o);
    o instanceof String);
 

Parameters:

isStatic - the kind of constraint method to generate; true for static and false for non-static (instance) constraint method.

typeDecl - the target type declaration whose constraint methods are to be generated.

restoreMethods - the names of resore methods to be used to restore the values of old expression fields.

postfix

private static String postfix(boolean isStatic,
                              JmlTypeDeclaration typeDecl)

Returns the postfix to be used for constraint check method's name. The return value is of the form: [static|instance$T].

generate

public JMethodDeclarationType generate(RacNode stmt)

Returns a constraint check method with the given body, stmt. Appended to the body (stmt) are (1) code to check the inherited assertions if any, and (2) code to throw an appropriate exception to notify an assertion violation.

Overrides:

generate in class InvariantLikeMethod

Parameters:

stmt - code to evaluate the assertions; the result is supposed to be stored in the variable VN_ASSERTION. A null value means that no assertion is specified or the assertion is not executable.

buildHeader

protected StringBuffer buildHeader(String returnType,
                                   String name,
                                   JFormalParameter[] parameters,
                                   CClassType[] exceptions)

Builds, in a string form, the header of constraint method. The header of a constraint method has the following form.

  public [static] void name(String rac$msg, String rac$name,
    String rac$params)
 

Overrides:

buildHeader in class InvariantLikeMethod

Parameters:

returnType - return type

name - method name

parameters - formal parameters

exceptions - checked exceptions

checker

protected String checker(boolean initValue,
                         RacNode stmt,
                         JFormalParameter[] params)

Returns the given constraint check code, stmt, wrapped with code to inherit supertypes's constraints. For each supertype, its strong or weak form of constraint check method is called to inherit its constraints.

Overrides:

checker in class AssertionMethod

Parameters:

initValue - not used

stmt - constraint check code to be wrapped

params - not used

inheritAssertion

protected String inheritAssertion(JFormalParameter[] parameters)

Return the code to inherit constraints of the superclass and interfaces, i.e., to call the constraint methods of the superclass and interfaces.

Overrides:

inheritAssertion in class InvariantLikeMethod

Parameters:

parameters - parameters to the inherited assertion check method; not used in this specialization.

inheritFrom

protected String inheritFrom(boolean isWeaksubtype,
                             CClass clazz)

Returns code that, if executed, inherits constraints from the given type, clazz.

See Also:

#reflectiveCall(CClass), #nonReflectiveCall(CClass)

reflectiveCall

protected String reflectiveCall(boolean isWeakly,
                                CClass clazz)

Return code, in the string form, that calls reflectively the constraint check method of the given supertype, claszz. If the argument, isWeakly is true, the code calls the supertype's constraint method that checks constraints according to the weak subtyping; otherwise, called is the one that checks constraints according to the strong form of subtyping.

See Also:

inheritFrom(boolean, CClass)

nonReflectiveCall

protected String nonReflectiveCall(boolean isWeakly,
                                   CClass clazz)

Return code, in the string form, that calls non-reflectively the constraint check method of the given supertype, claszz. If the argument, isWeakly is true, the code calls the supertype's constraint method that checks constraints according to the weak subtyping; otherwise, called is the one that checks constraints according to the strong form of subtyping.

See Also:

inheritFrom(boolean, CClass)

inheritCallArgTypes

protected String inheritCallArgTypes()

Returns, in the string form, the formal parameter types of the supertype's constraint check method. The returned value is used to look up the supertype's constraint check method using the Java's reflection facility.

Overrides:

inheritCallArgTypes in class ConstraintMethod

See Also:

reflectiveCall(boolean, CClass), nonReflectiveCall(boolean, CClass)

inheritCallArgs

protected String inheritCallArgs()

Returns, in the string form, the arguments for calling supertype's constraint check method.

Overrides:

inheritCallArgs in class ConstraintMethod

See Also:

reflectiveCall(boolean, CClass), nonReflectiveCall(boolean, CClass)