org.jmlspecs.jmlrac.qexpr
Class StaticAnalysis.EnumerationBased

java.lang.Object
  org.jmlspecs.jmlrac.qexpr.Translator
      org.jmlspecs.jmlrac.qexpr.StaticAnalysis
          org.jmlspecs.jmlrac.qexpr.StaticAnalysis.EnumerationBased

All Implemented Interfaces:

Constants, Constants, Constants, RacConstants

Enclosing class:

StaticAnalysis

private static class StaticAnalysis.EnumerationBased

extends StaticAnalysis

A concrete class for translating JML quantified expressions into Java source code. The translation is based on an explicit enumeration of all possible values for the quantified variable. A quantified variable of boolean is implemented in this way.

  protected invariant quantiExp.quantifiedVarDecls()[0].getType() 
    == JmlStdType.Boolean;
 

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.EnumerationBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)           Constructs a EnumerationBased 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

StaticAnalysis.EnumerationBased

private StaticAnalysis.EnumerationBased(VarGenerator varGen,
                                        RacContext ctx,
                                        JmlSpecQuantifiedExpression expr,
                                        String resultVar,
                                        AbstractExpressionTranslator transExp)

Constructs a EnumerationBased 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.

 requires expr.quantifiedVarDecls()[0].getType() == 
   JmlStdType.Boolean;
 

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:

  boolean[] v = { false, true };
  for (int i = 0; [cond &&] i < v.length; i++) {
    bool x = v[i];
    result
  }
 

where x is the quantified variable and v and i are fresh variables.

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.