org.jmlspecs.checker
Class JmlExpressionContext

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlContext
          org.jmlspecs.checker.JmlExpressionContext

All Implemented Interfaces:

CContextType, CExpressionContextType, Cloneable, Constants, Constants, Constants

public class JmlExpressionContext

extends JmlContext

implements CExpressionContextType

A class for representing the context in which JML expressions are typechecked. This is a subclass of the CExpressionContextType class to encode the JML expression-specific contextual information. For example, the JML \result expression is allowed only in the normal postcondition. To typecheck the expressions such as \result, we pass to them the fact whether they are being typechecked in the normal postcondition or not as contexutal information. In JML, there are seven context(state)-sensitive expression constructs: \fresh, \not_modified, \old, \result, \duration, \working_space, and \space. The typechecking rules for these constructs are defined as follows. In the table, the entry with O means that a particular construct is allowed in that particular context, and the X marks prohibition.

  --------------------------------------------------------
                        \not_                   
                \fresh  modified  \old  \result    others
  -------------------------------------------------------
   pre           X      X          X      X        O    
   post (N)      O      O          O      O        O
   post (E)      O      O          O      X        O
   internal      O      O          O      X        O
   old           X      X          X      X        O
   intra         X      X          X      X        O
   inter         O      O          O      X        O
   working_space O      O          O      O        O
   duration      O      O          O      O        O
  ------------------------------------------------------
 

Field Summary
protected  MJMathMode	arithmeticMode
private static int	CTX_DURATION
private static int	CTX_EXCEPTIONAL_POSTCONDITION
private static int	CTX_INTERCONDITION
private static int	CTX_INTERNAL_CONDITION
private static int	CTX_INTRACONDITION
private static int	CTX_OLD_EXPRESSION
private static int	CTX_POSTCONDITION
private static int	CTX_PRECONDITION
private static int	CTX_WORKING_SPACE
private  int	kind

 

Fields inherited from class org.jmlspecs.checker.JmlContext

cunit, delegee, parent

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

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_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, 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_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, 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, 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_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	JmlExpressionContext(CFlowControlContextType parent, int kind)

 

Method Summary
MJMathMode	arithmeticMode()           Indicates the integral arithmetic mode that should be used.
static JmlExpressionContext	createDuration(CFlowControlContextType parent)           Create and return a duration context.
static JmlExpressionContext	createExceptionalPostcondition(CFlowControlContextType parent)           Create and return an exceptional postcondition context.
static JmlExpressionContext	createIntercondition(CFlowControlContextType parent)           Create and return an intercondition context.
static JmlExpressionContext	createInternalCondition(CFlowControlContextType parent)           Create and return an internal condition context.
static JmlExpressionContext	createIntracondition(CFlowControlContextType parent)           Create and return an intracondition context.
static JmlExpressionContext	createOldExpression(CFlowControlContextType parent)           Create and return an old expression context.
static JmlExpressionContext	createPostcondition(CFlowControlContextType parent)           Create and return a normal postcondition context.
static JmlExpressionContext	createPrecondition(CFlowControlContextType parent)           Create and return a precondition context.
static JmlExpressionContext	createSameKind(CFlowControlContextType parent, JmlExpressionContext ctx)           Return a new JmlExpressionContext of the same kind as the given argument ctx.
static JmlExpressionContext	createWorkingSpace(CFlowControlContextType parent)           Create and return a working_space context.
boolean	discardValue()
boolean	freshOk()           Return true if \fresh is allowed in this context
boolean	isIncDec()
boolean	isLeftSide()
CFieldAccessor	lookupField(String ident)           searches for a field with the given identifier
CFieldAccessor	lookupOuterField(String ident)           Searches for a field of the given name in the context surrounding the current lexical contour.
boolean	notModifiedOk()           Return true if \not_modified is allowed in this context
boolean	oldOk()           Return true if \old expression is allowed in this context
boolean	resultOk()           Return true if \result is allowed in this context
void	setArithmeticMode(byte mode)
void	setDiscardValue(boolean discardValue)           set this context as a discarded value so result is ignored
void	setIncDec(boolean incDec)           Set this context as an increment or decrement expression, so we can generate appropriate getters and setters if necessary (and also generate proper code in the future).
void	setLeftSide(boolean leftSide)           Set this context as a left side in an assignment, so access to vars may be uninitialized

 

Methods inherited from class org.jmlspecs.checker.JmlContext

catchUp, check, check, check, check, classToGenerate, createClassContext, createDummyContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, enterSpecScope, exitSpecScope, fail, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getFlowControlContext, getHostClass, getMethodContext, getParentContext, initializeField, inSpecScope, isBeforeSuperConstructorCall, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupClass, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, replaceFieldInfoUpTo, reportTrouble, resolveMaybeExtMethodRef

 

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

 

Methods inherited from interface org.multijava.mjc.CContextType

catchUp, check, check, check, check, classToGenerate, createClassContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getFlowControlContext, getMethodContext, getParentContext, initializeField, isBeforeSuperConstructorCall, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupClass, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, replaceFieldInfoUpTo, reportTrouble, resolveMaybeExtMethodRef

 

Field Detail

kind

private int kind

CTX_PRECONDITION

private static final int CTX_PRECONDITION

CTX_POSTCONDITION

private static final int CTX_POSTCONDITION

CTX_EXCEPTIONAL_POSTCONDITION

private static final int CTX_EXCEPTIONAL_POSTCONDITION

CTX_INTERNAL_CONDITION

private static final int CTX_INTERNAL_CONDITION

CTX_OLD_EXPRESSION

private static final int CTX_OLD_EXPRESSION

CTX_INTRACONDITION

private static final int CTX_INTRACONDITION

CTX_INTERCONDITION

private static final int CTX_INTERCONDITION

CTX_WORKING_SPACE

private static final int CTX_WORKING_SPACE

CTX_DURATION

private static final int CTX_DURATION

arithmeticMode

protected MJMathMode arithmeticMode

JmlExpressionContext

private JmlExpressionContext(CFlowControlContextType parent,
                             int kind)

createPrecondition

public static JmlExpressionContext createPrecondition(CFlowControlContextType parent)

Create and return a precondition context.

Parameters:

parent - the parent context

Returns:

a new precondition context

createPostcondition

public static JmlExpressionContext createPostcondition(CFlowControlContextType parent)

Create and return a normal postcondition context.

Parameters:

parent - the parent context

Returns:

a new postcondition context

createExceptionalPostcondition

public static JmlExpressionContext createExceptionalPostcondition(CFlowControlContextType parent)

Create and return an exceptional postcondition context.

Parameters:

parent - the parent context

Returns:

a new exceptional postcondition context

createWorkingSpace

public static JmlExpressionContext createWorkingSpace(CFlowControlContextType parent)

Create and return a working_space context.

Parameters:

parent - the parent context

Returns:

a new working_space context

createDuration

public static JmlExpressionContext createDuration(CFlowControlContextType parent)

Create and return a duration context.

Parameters:

parent - the parent context

Returns:

a new duration context

createInternalCondition

public static JmlExpressionContext createInternalCondition(CFlowControlContextType parent)

Create and return an internal condition context. An internal condition context is for typechecking predicates over client-invisible, intermediate states such as assert clause.

Parameters:

parent - the parent context

Returns:

a new internal condition context

createOldExpression

public static JmlExpressionContext createOldExpression(CFlowControlContextType parent)

Create and return an old expression context. An old expression context is for typechecking old expressions.

Parameters:

parent - the parent context

Returns:

a new old expression condition context

createIntracondition

public static JmlExpressionContext createIntracondition(CFlowControlContextType parent)

Create and return an intracondition context. An intracondition context is for typechecking class-level specifications such as invariant clause that concern with a single state.

Parameters:

parent - the parent context

Returns:

a new intracondition context

createIntercondition

public static JmlExpressionContext createIntercondition(CFlowControlContextType parent)

Create and return an intercondition context. An intercondition context is for typechecking class-level specifications such as constraint clause that concern with a pair of states.

Parameters:

parent - the parent context

Returns:

a new intercondition context

createSameKind

public static JmlExpressionContext createSameKind(CFlowControlContextType parent,
                                                  JmlExpressionContext ctx)

Return a new JmlExpressionContext of the same kind as the given argument ctx.

Parameters:

parent - the parent context

Returns:

a new context

lookupField

public CFieldAccessor lookupField(String ident)
                           throws UnpositionedError

searches for a field with the given identifier

Specified by:

lookupField in interface CContextType

Overrides:

lookupField in class JmlContext

Returns:

a field from an ident in current context

Throws:

UnpositionedError - this error will be positioned soon

lookupOuterField

public CFieldAccessor lookupOuterField(String ident)
                                throws UnpositionedError

Searches for a field of the given name in the context surrounding the current lexical contour.

Specified by:

lookupOuterField in interface CContextType

Overrides:

lookupOuterField in class JmlContext

Parameters:

ident - the name of the field

Returns:

a variable from a field in the surrounding context, or null if none is found

Throws:

UnpositionedError - this error will be positioned soon

setIncDec

public void setIncDec(boolean incDec)

Set this context as an increment or decrement expression, so we can generate appropriate getters and setters if necessary (and also generate proper code in the future).

Specified by:

setIncDec in interface CExpressionContextType

Parameters:

incDec -

isIncDec

public boolean isIncDec()

Specified by:

isIncDec in interface CExpressionContextType

Returns:

true if this context is part of an increment or decrement expression

setLeftSide

public void setLeftSide(boolean leftSide)

Set this context as a left side in an assignment, so access to vars may be uninitialized

Specified by:

setLeftSide in interface CExpressionContextType

Parameters:

leftSide - set the side of current code flow

isLeftSide

public boolean isLeftSide()

Specified by:

isLeftSide in interface CExpressionContextType

Returns:

true if this context is on a left side of an assignement

setDiscardValue

public void setDiscardValue(boolean discardValue)

set this context as a discarded value so result is ignored

Specified by:

setDiscardValue in interface CExpressionContextType

Parameters:

discardValue - is the value of this expression in this context discarded?

discardValue

public boolean discardValue()

Specified by:

discardValue in interface CExpressionContextType

Returns:

true if the result value of this expression is discarded

freshOk

public boolean freshOk()

Return true if \fresh is allowed in this context

notModifiedOk

public boolean notModifiedOk()

Return true if \not_modified is allowed in this context

oldOk

public boolean oldOk()

Return true if \old expression is allowed in this context

resultOk

public boolean resultOk()

Return true if \result is allowed in this context

arithmeticMode

public MJMathMode arithmeticMode()

Description copied from interface: CContextType

Indicates the integral arithmetic mode that should be used.

Specified by:

arithmeticMode in interface CContextType

Overrides:

arithmeticMode in class JmlContext

setArithmeticMode

public void setArithmeticMode(byte mode)

Specified by:

setArithmeticMode in interface CExpressionContextType