JML

org.jmlspecs.jmlrac.qexpr
Class StaticAnalysis.SetBased

java.lang.Object
  extended byorg.jmlspecs.jmlrac.qexpr.Translator
      extended byorg.jmlspecs.jmlrac.qexpr.StaticAnalysis
          extended byorg.jmlspecs.jmlrac.qexpr.StaticAnalysis.SetBased
All Implemented Interfaces:
Constants, Constants, Constants, RacConstants
Enclosing class:
StaticAnalysis

private static class StaticAnalysis.SetBased
extends StaticAnalysis

A concrete class for translating JML quantified expressions into Java source code. The translation is based on the set-based static analysis of the expression's structures.


Field Summary
protected  RacContext context
          current translation context
protected static TokenReference NO_REF
           
protected  JmlSpecQuantifiedExpression quantiExp
          taget quantified expression to translate
protected  String resultVar
          variable name to have the value of quantified expression in the translated code
protected  AbstractExpressionTranslator transExp
           
protected  VarGenerator varGen
          variable generator for generating unique local variables
 
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
private StaticAnalysis.SetBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
          Constructs a SetBased object.
 
Method Summary
 RacNode generateLoop(RacNode body)
          Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected  RacNode generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result)
          Returns Java source code for evaluating quantified expressions using the QSet-based translation.
static StaticAnalysis getInstance(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
          Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.
protected  RacNode transExpression(JExpression expr, String var)
          Returns code for evaluating expression expr and storing the result to the variable var.
 RacNode translate()
          Translate a JML quantified expression into Java source code and return the result.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

NO_REF

protected static final TokenReference NO_REF

varGen

protected VarGenerator varGen
variable generator for generating unique local variables


context

protected RacContext context
current translation context


quantiExp

protected JmlSpecQuantifiedExpression quantiExp
taget quantified expression to translate


resultVar

protected String resultVar
variable name to have the value of quantified expression in the translated code


transExp

protected AbstractExpressionTranslator transExp
Constructor Detail

StaticAnalysis.SetBased

private StaticAnalysis.SetBased(VarGenerator varGen,
                                RacContext ctx,
                                JmlSpecQuantifiedExpression expr,
                                String resultVar,
                                AbstractExpressionTranslator transExp)
Constructs a SetBased object.

Parameters:
varGen - variable generator to be used in translation for generating unique local variables.
expr - quantified expression to be translated.
resultVar - variable name to have the value of quantified expression in the translated code.
transExp - translator to use for translating subexpressions of the quantified expression.
Method Detail

generateLoop

protected RacNode generateLoop(JVariableDefinition varDef,
                               JExpression qexpr,
                               String cond,
                               RacNode result)
                        throws NonExecutableQuantifierException
Returns Java source code for evaluating quantified expressions using the QSet-based translation. The returned code has the following general form:
  java.util.Collection c = new java.util.HashSet();
  [[eval of c from qexpr]]
  java.util.Iterator iter = c.iterator();
  while ([condr &&] c.hasNext()) {
    T x = iter.next();
    result
  }
 
where x is the quantified variable of type T.

Parameters:
varDef - quantified variable
qexpr - target expression for interval calculation (i.e., normally, the predicate part of the quantified expression)
cond - additional condition to be conjoined (&&) to the loop condition; null for no extra condition.
result - code for evaluating expression part (or inner loop)
Throws:
NonExecutableQuantifierException - if not executable.

getInstance

public static StaticAnalysis getInstance(VarGenerator varGen,
                                         RacContext ctx,
                                         JmlSpecQuantifiedExpression expr,
                                         String resultVar,
                                         AbstractExpressionTranslator transExp)
Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.

Parameters:
varGen - variable generator to be used in translation for generating unique local variables.
expr - quantified expression to be translated.
resultVar - variable name to store the result value of quantified expression in the translated code.
transExp - translator to use for translating subexpressions.

translate

public RacNode translate()
                  throws NonExecutableQuantifierException
Translate a JML quantified expression into Java source code and return the result.

Returns:
translated Java source code.
Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

generateLoop

public RacNode generateLoop(RacNode body)
                     throws NonExecutableQuantifierException
Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range. For example, the interval-based approach returns the following form of code:
  { 
    T l = 0;
    T u = 0;
    [[eval of l and u from predicate part]]
    while (l < u) {
      T x = l;
      result
      l = l + 1;
    }
  }
 
where x is the quantified variable.

Parameters:
body - code to be executed as the loop body
Throws:
NonExecutableQuantifierException - if not executable.

transExpression

protected RacNode transExpression(JExpression expr,
                                  String var)
Returns code for evaluating expression expr and storing the result to the variable var. As a special case, returns var = true; if expr is null.


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.