JML

org.jmlspecs.checker
Class JmlExpressionContext

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlContext
          extended byorg.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
  ------------------------------------------------------
 
where the precondition is over a single, visible, definite (determined) state (i.e., the pre-state); the normal or exceptional postcondition is over a pair of visible, definite states (i.e., the pre/post-states); the internal condition is over a pair of a pre-state and an invisible (internal, intermediate), definite state (e.g., assert clause); the old condition is for the \old expression and should denote the pre-state, but we have separated them here for the future extention; the intracondition is over a single, visible, indefinite (undetermined) state (i.e., some pre or post-state); the intercondition is over a pair of a pair of visible, undetermined states (i.e., some pre/post-states). Both the intra- and intercondition are for class-level specifications such as invariants (intracondition) and history constrainsts (intercondition). The working_space is for the clause of the same name, as is the duration context; both of these are assertions over pairs of states, a pre-state and a post-state


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_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 JmlExpressionContext(JmlExpressionContext parent)
           
private JmlExpressionContext(CFlowControlContextType parent, int kind)
           
 
Method Summary
 MJMathMode arithmeticMode()
          Indicates the integral arithmetic mode that should be used.
private  void constructorHelper(CContextType parent)
           
static JmlExpressionContext createDuration(CFlowControlContextType parent)
          Create and return a duration context.
static JmlExpressionContext createExceptionalPostcondition(CFlowControlContextType parent)
          Create and return an exceptional postcondition context.
 CExpressionContextType createExpressionContext_()
          Create a copy of this context to handle divergent paths, e.g., in conditional expressions
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
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, catchUp, check, check, check, check, classToGenerate, createClassContext, createDummyContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, enterSpecScope, exitSpecScope, fail, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getContextNullity, getFANonNulls, getFANulls, getFlowControlContext, getHostClass, getMethodContext, getParentContext, initializeField, inSpecScope, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupClass, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, removeAllFANullity, removeFANonNull, 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
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, catchUp, check, check, check, check, classToGenerate, createClassContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getFANonNulls, getFANulls, getFlowControlContext, getMethodContext, getParentContext, initializeField, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupClass, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, removeAllFANullity, removeFANonNull, 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
Constructor Detail

JmlExpressionContext

private JmlExpressionContext(CFlowControlContextType parent,
                             int kind)

JmlExpressionContext

private JmlExpressionContext(JmlExpressionContext parent)
Method Detail

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

constructorHelper

private void constructorHelper(CContextType parent)

createExpressionContext_

public CExpressionContextType createExpressionContext_()
Create a copy of this context to handle divergent paths, e.g., in conditional expressions

Specified by:
createExpressionContext_ in interface CExpressionContextType

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

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.