org.jmlspecs.jmlrac
Class LocalConstraintMethod

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.LocalConstraintMethod

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

public class LocalConstraintMethod

extends ConstraintMethod

A class for generating constaint check methods that check locally specified type constraints without inheriting any constraints from supertypes. Two kinds of constraint check methods can be generated: instance constraint check methods 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.3 $

Author:

Yoonsik Cheon

See Also:

AssertionMethod, ConstraintMethod, generate(RacNode)

Field Summary
private  JmlMethodName[]	names           The names of methods to which the generated constraint check method is applicable; it is null if the constraint is applicable to all methods.
private  VarGenerator	varGen           The variable generator to be used in the translation.

 

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

LocalConstraintMethod(VarGenerator varGen, boolean isStatic, JmlTypeDeclaration typeDecl, JmlMethodName[] names, int suffix)           Construct a new instance.

 

Method Summary
protected  boolean	canInherit()           Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass or interfaces.
JMethodDeclarationType	generate(RacNode stmt)           Generates a constrain check method by using the given block of code, stmt, as the main body.
private  String	isApplicable(JmlMethodName name, String var)           Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.
private  RacNode	isApplicable(JmlMethodName[] names)           Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.
private  String	nameMatched(JmlMethodName name, String var)           Returns code that compares the given JML method name, name, with the method name given as a parameter (rac$name) to the constraint check method.
private  String	paramMatched(JmlMethodName name, String var)           Returns code that compares the foraml parameter types of the given JML method, name, with those of the constraint check method.
static String	postfix(boolean isStatic, JmlTypeDeclaration typeDecl, int suffix)           Returns the postfix to be used for constraint check method's name.
private  String	simpleName(JmlName[] subnames)           Returns a simplied method name of the given JML names, that can be compared with the method name given as a parameter of the constraint check method.

 

Methods inherited from class org.jmlspecs.jmlrac.ConstraintMethod

formalParameters, inheritCallArgs, inheritCallArgTypes

 

Methods inherited from class org.jmlspecs.jmlrac.InvariantLikeMethod

buildHeader, inheritAssertion, inheritFrom, nonReflectiveCall, reflectiveCall

 

Methods inherited from class org.jmlspecs.jmlrac.AssertionMethod

checker, 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

varGen

private final VarGenerator varGen

The variable generator to be used in the translation. If necessary, fresh variables are generated by this translator using this variable generator.

names

private JmlMethodName[] names

The names of methods to which the generated constraint check method is applicable; it is null if the constraint is applicable to all methods.

LocalConstraintMethod

public LocalConstraintMethod(VarGenerator varGen,
                             boolean isStatic,
                             JmlTypeDeclaration typeDecl,
                             JmlMethodName[] names,
                             int suffix)

Construct a new instance.

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.

names - method names that the generated constraint check method is applicable to.

suffix - a unique sequence number to be used as the suffix of the constraint check method's name.

postfix

public static String postfix(boolean isStatic,
                             JmlTypeDeclaration typeDecl,
                             int suffix)

Returns the postfix to be used for constraint check method's name.

generate

public JMethodDeclarationType generate(RacNode stmt)

Generates a constrain check method by using the given block of code, stmt, as the main body. This method prefixes the body with the code that tests if the constraint is applicable to the argument method and appends the code to throw a constraint violation error. Thus, the returned method has the following structure.

 public void checkHC$instance1$Constraint1(String rac$msg,
   String rac$name, java.lang.Class[] rac$params) {
   boolean b = false;
   b = ...; // test if applicable to method  
   if (!b) {
     return;
   }
   stmt
   if (!constraint_hold) {
     throw new JMLHistoryConstraintError(...);
   }
 }
 

Overrides:

generate in class InvariantLikeMethod

Parameters:

stmt - code to evaluate the constraint; 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.

isApplicable

private RacNode isApplicable(JmlMethodName[] names)

Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.

isApplicable

private String isApplicable(JmlMethodName name,
                            String var)

Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method. The code sets the given boolean variable, var to the result.

nameMatched

private String nameMatched(JmlMethodName name,
                           String var)

Returns code that compares the given JML method name, name, with the method name given as a parameter (rac$name) to the constraint check method. The code sets the given boolean variable, var to the result of the comparison.

paramMatched

private String paramMatched(JmlMethodName name,
                            String var)

Returns code that compares the foraml parameter types of the given JML method, name, with those of the constraint check method. The code sets the given boolean variable, var to the result of the comparison.

simpleName

private String simpleName(JmlName[] subnames)

Returns a simplied method name of the given JML names, that can be compared with the method name given as a parameter of the constraint check method. E.g., n for n or this.n, and null for all other cases.

canInherit

protected boolean canInherit()

Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass or interfaces.

 also
   protected normal_behavior
     ensures \result == false;
 

Overrides:

canInherit in class InvariantLikeMethod