org.jmlspecs.jmlrac
Class TransConstraint

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.TransConstraint

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

public class TransConstraint

extends TransUtils

A class for translating JML (history) constraints. A history constraint is translated into a couple of constraint check methods, one for static (class) constraints and the other for non-static (instance) constraints. The translation also produce a couple of old expression evaluation methods, one for static constraints and the other for both static and non-static constraints. The latter is supposed to be called by non-static methods. The old expression evaluation methods, if called in the pre-state, evaluate old expressions appearing in the constraints and store the results to newly introduced private fields, called old expression fields. An old expression field is a temporary location to hold the value of an old expression (evaluated in the pre-state). The constraint check methods use the old variable in place of the original old expression. The client of this class is responsible for (1) adding constraint check methods and old expression evaluation methods to the host type declaration containing the target constraint clauses, (2) declaring appropriate old expression fields to the host type declaration, and (3) making calls to the old expression evaluation methods in the appropriate pre-state (e.g., in the wrapper method).

Version:

$Revision: 1.30 $

Author:

Yoonsik Cheon

See Also:

ConstraintMethod

Field Summary
private  List	oldExprsInstance           The set of (translated) old expressions appearing in the non-static constraints.
private  List	oldExprsStatic           The set of (translated) old expressions appearing in the static constraints.
private  List	restoreMethods           The names of restore methods generated so far.
private  List	stackVarsInstance           The set of private stack field names used to save and restore old expression values appearing in non-static constraint clauses.
private  List	stackVarsStatic           The set of private stack field names used to save and restore old expression values appearing in static constraint clauses.
private  JmlTypeDeclaration	typeDecl           The host type declaration containing the target constraint clause to be translated by this translator.
private  VarGenerator	varGen           The variable generator to be used in the translation.

 

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

TransConstraint(JmlTypeDeclaration typeDecl, VarGenerator varGen)           Constructs a TransConstraint object.

 

Method Summary
private  RacNode	constraintMethod(boolean forStatic, int cnt, JExpression pred, JmlMethodName[] names)           Returns a constraint check method that checks the given predicate, pred as a hisotry constraint.
private  RacNode	constraintMethod(JmlConstraint constraint, int cnt)           Returns a constraint check method for the given hisotry constraint, constraint.
private  RacNode	constraintMethod(JmlConstraint[] constraints, boolean forStatic)           Returns a static or an instance constraint check method for the given history constraints, constraints.
private  String	evalSuperHC(VarGenerator varGen, boolean forStatic, CClass clazz)           Return code that evaluates the old expressions of the given supertype, clazz, by making an appropriate call to its old expression evaluation method.
private  RacNode	genStackMethods(boolean forStatic, String stackVar, List oldExprs)           Returns a private stack field declaration with a pair of push and pop methods.
private static boolean	isCheckable(JmlConstraint cons)           Returns true if the given constraint clause is checkable.
PreValueVars.Entry[]	oldExprFields(boolean forStatic)           Returns field declarations for the old expressions appearing in the constraint clause.
private  RacNode	oldMethod(List exprs, boolean forStatic)           Returns an old-expression evaluation method for the given old expressions, exprs.
RacNode	translate(JmlConstraint[] constraints)           Translates the given history constraints, constraints, and returns the translation result.

 

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

typeDecl

private final JmlTypeDeclaration typeDecl

The host type declaration containing the target constraint clause to be translated by this translator.

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 during the translation.

oldExprsStatic

private List oldExprsStatic

The set of (translated) old expressions appearing in the static constraints. Each old expression appearing in the static constraints is translated into a sequence of statements (i.e., an instance of RacNode), which, if executed, evaluate the old expression and store the result into a freshly introduced field, called an old expression field. The name of the old expression field is given by the name field of the class RacNode in the form of "T n;\n", where T is the type and n is the field name.

 
 public invariant (\forall Object o; oldExprsStatic.contains(o); 
   o instanceof RacNode);
 

See Also:

TransPostcondition.visitJmlPreExpression(JmlPreExpression), TransPostcondition.visitJmlOldExpression(JmlOldExpression)

oldExprsInstance

private List oldExprsInstance

The set of (translated) old expressions appearing in the non-static constraints. Each old expression appearing in the non-static constraints is translated into a sequence of statements (i.e., an instance of RacNode), which, if executed, evaluate the old expression and store the result into a freshly introduced field, called an old expression field. The name of the old expression field is given by the name field of the class RacNode in the form of "T n;\n", where T is the type and n is the field name.

 
 public invariant (\forall Object o; oldExprsInstance.contains(o); 
   o instanceof RacNode);
 

See Also:

TransPostcondition.visitJmlPreExpression(JmlPreExpression), TransPostcondition.visitJmlOldExpression(JmlOldExpression)

stackVarsStatic

private List stackVarsStatic

The set of private stack field names used to save and restore old expression values appearing in static constraint clauses. The set becomes empty if no such stack field is needed, e.g., no old expression in any static constraints.

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

stackVarsInstance

private List stackVarsInstance

The set of private stack field names used to save and restore old expression values appearing in non-static constraint clauses. The set becomes empty if no such stack field is needed, e.g., no old expression in any non-static constraints.

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

restoreMethods

private List restoreMethods

The names of restore methods generated so far.

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

TransConstraint

public TransConstraint(JmlTypeDeclaration typeDecl,
                       VarGenerator varGen)

Constructs a TransConstraint object.

  requires typeDecl != null && varGen != null;
 

Parameters:

typeDecl - host type declaration containing the target constraint clause to be translated

varGen - variable generator to be used for the translation

oldExprFields

public PreValueVars.Entry[] oldExprFields(boolean forStatic)

Returns field declarations for the old expressions appearing in the constraint clause. Each field declaration has the following string form: "[static] T n;\n", where T is the type and n is the field name. Note that the old expression evaluation methods, returned by the method translate, if called, evaluate old expressions and initialize the declared fields. These fields are called old expression fields. This method must be called after the translation.

 ensures \result != null;
 

Parameters:

forStatic - true for static old expressions; false for instance old expressions.

See Also:

translate(JmlConstraint[]), oldExprsStatic, oldExprsInstance, PreValueVars.Entry

translate

public RacNode translate(JmlConstraint[] constraints)

Translates the given history constraints, constraints, and returns the translation result. This method translates the given history constraints and produces a couple of new field declarations and several new methods:

• A static constraint check method (see ConstraintMethod).
• A non-static (instance) constraint check method (see ConstraintMethod).
• A static old-expression evaluation method.
• A static stack field declaration.
• A static old values save method.
• A static old values restoration method.
• A non-static stack field declaration.
• A non-static old values save method.
• A non-static old values restoration method.

The old expression evaluation methods, if called, evaluate the old expressions appearing in the constraints and store the results into newly introduced fields, called old expression fields. The old expression fields are used instead of the original old expressions by the constraint check methods. The generated methods are concatenated and returned as the translation result.

The stack variables and their access methods are used to correctly pass, in the presence recursive method calls, old expression values evaluated in the pre=state to the constraint check methods executed in the post-state.

  requires constraints != null;
  assignable oldExprsStatic, oldExprsInstance;
  assignable stackVarsStatic, stackVarsInstance, restoreMethods;
  ensures \result != null;
 

Parameters:

constraints - history constraints to be translated

See Also:

oldExprFields(boolean)

constraintMethod

private RacNode constraintMethod(JmlConstraint[] constraints,
                                 boolean forStatic)

Returns a static or an instance constraint check method for the given history constraints, constraints. As a side-effect, this method also translates and accumulates into private fields old expressions appearing in the constraints for future use.

  requires constraints != null;
  assignable oldExprsStatic, oldExprsInstance;
  assignable stackVarsStatic, stackVarsInstance, restoreMethods;
  ensures \result != null;
 

Parameters:

constraints - history constraints to be translated

forStatic - type of constraints to be translated (static or non-static)

Returns:

object of RacNode representing a constraint check method.

See Also:

oldExprsStatic, oldExprsInstance

constraintMethod

private RacNode constraintMethod(JmlConstraint constraint,
                                 int cnt)

Returns a constraint check method for the given hisotry constraint, constraint. The parameter cnt is used as a suffix for the name of generated check method. As a side-effect, this method also translates and accumulates into private fields all the old expressions appearing in the given constraint.

  requires constraint != null;
  assignable oldExprsStatic, oldExprsInstance;
  assignable stackVarsStatic, stackVarsInstance;
  ensures \result != null;
 

Parameters:

constraint - history constraint to be translated

Returns:

object of RacNode representing a constraint check method.

See Also:

oldExprsStatic, oldExprsInstance, stackVarsStatic, stackVarsInstance

constraintMethod

private RacNode constraintMethod(boolean forStatic,
                                 int cnt,
                                 JExpression pred,
                                 JmlMethodName[] names)

Returns a constraint check method that checks the given predicate, pred as a hisotry constraint. If the parameter forStatic is true, the given predicate is regarded as a static constraint; otherwise, it is regared as a non-static constraint. The parameter cnt is used as a suffix for the name of generated check method. As a side-effect, this method also translates and accumulates into private fields all the old expressions appearing in the given constraint.

  assignable oldExprsStatic, oldExprsInstance;
  assignable stackVarsStatic, stackVarsInstance;
  ensures \result != null;
 

Returns:

object of RacNode representing a constraint check method.

See Also:

oldExprsStatic, oldExprsInstance, stackVarsStatic, stackVarsInstance, restoreMethods

isCheckable

private static boolean isCheckable(JmlConstraint cons)

Returns true if the given constraint clause is checkable. The clause is checkable if it is not a redundant specification or the command line option "noredundancy" is not turned on.

oldMethod

private RacNode oldMethod(List exprs,
                          boolean forStatic)

Returns an old-expression evaluation method for the given old expressions, exprs. The resulting method, if called, evaluates old expressions given by exprs and stores the results into the so-called old expression fields.

  requires exprs != null && 
    (\forall Object o; exprs.contains(o);
       o instanceof RacNode);
  ensures \result != null;
 

Parameters:

exprs - a list of (translated) old expressions (RacNode)

forStatic - type of constraint (static or non-static)

Returns:

object of RacNode representing an old expression evaluation method.

See Also:

oldExprsStatic, oldExprsInstance

evalSuperHC

private String evalSuperHC(VarGenerator varGen,
                           boolean forStatic,
                           CClass clazz)

Return code that evaluates the old expressions of the given supertype, clazz, by making an appropriate call to its old expression evaluation method.

See Also:

#reflectiveCall(CClass)

genStackMethods

private RacNode genStackMethods(boolean forStatic,
                                String stackVar,
                                List oldExprs)

Returns a private stack field declaration with a pair of push and pop methods. The stack is used to save into the pre-state old expression values, and restore them from. The reason is to pass correct pre-state values to the post-state assertion check in the presence of recursive method calls. The returned code has the following form.

 private [static] Stack var = new Stack();
 private [static] void saveTo$var() {
   Object val[] = new Object[n];
   val[1] = preVar1;
   ...
   val[n] = preVarn;
   var.push(val);
 }
 private [static] void restoreFrom$var() {
   Object val[] = (Object[]) var.pop();
   preVar1 = val[1];
   ...
   preVarn = val[n];
 }
 

  requires (\forall Object o; oldExprs.contains(o);
             o instanceof PreValueVars.Entry);
 assignable \nothing;
 

Parameters:

forStatic - true if the stack and methods should be static

stackVar - name of the stack field to be declared

oldExprs - fields to store into and restore from the stack