JML

org.jmlspecs.jmlrac
Class TransConstraint

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.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);
 

Constructor Detail

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
Method Detail

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:

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

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.