org.jmlspecs.checker
Class JmlRepresentsDecl

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlDeclaration
                      org.jmlspecs.checker.JmlRepresentsDecl

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, PhylumType

public class JmlRepresentsDecl

extends JmlDeclaration

This AST node represents a JML represents declaration annotation. The syntax for the represents declaration is as follows.

  represents-decl ::= represents-keyword store-ref "<-" spec-expression ";"
    | represents-keyword store-ref "=" spec-expression ";"
    | represetns-keyword store-ref "\such_that" predicate ";"
  represents-keyword ::= "represents" | "represents_redundantly"
 

Version:

$Revision: 1.17 $

Author:

Curtis Clifton

Nested Class Summary

 

Nested classes inherited from class org.jmlspecs.checker.JmlNode

JmlNode.DummyInitializerDeclaration

 

Field Summary
private  JmlPredicate	predicate
private  JmlSpecExpression	specExpression
protected  JmlStoreRefExpression	storeRef           An AST for the storeRef expression of the more abstract variable in this.

 

Fields inherited from class org.jmlspecs.checker.JmlDeclaration

modifiers, redundantly

 

Fields inherited from class org.jmlspecs.checker.JmlNode

MJCVISIT_MESSAGE

 

Fields inherited from class org.multijava.util.compiler.Phylum

 

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

JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlPredicate predicate)           Creates a new JmlRepresentsDecl instance.

JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlSpecExpression specExpression)           Creates a new JmlRepresentsDecl instance.

 

Method Summary
void	accept(MjcVisitor p)           Accepts the specified visitor.
protected  void	checkRightHandSide(JmlExpressionContext context)           Performs type-checking of right-hand side of the represents clause.
protected  void	checkStoreRef(JmlExpressionContext context)           Checks the store ref of this depends/represents clause.
JmlSourceField	getField()           Returns the JmlSourceField of the model variable that this represents clause specifies for.
String	ident()           Returns the identifier of the represented model field.
protected static boolean	isInheritedOrOuter(JClassFieldExpression field)           Returns true if the given field expression refers to a field declared in this class, inherited from a superclasse or interface, or defined in an outer class or interface.
JmlPredicate	predicate()           Returns the predicate of this represents declaration.
JmlSpecExpression	specExpression()           Returns the spec expression of this represents declaration.
JmlStoreRefExpression	storeRef()           Returns the store ref expression of this represents declaration.
void	typecheck(CContextType context)           Typechecks this depends/represents clause in the context in which it appears.
boolean	usesAbstractionFunction()           Indicates whether this represents declaration uses an abstraction function.
boolean	usesAbstractionRelation()           Indicates whether this represents declaration uses an abstraction relations.

 

Methods inherited from class org.jmlspecs.checker.JmlDeclaration

checkModifiers, clone, createContext, createContextHelper, isRedundantly, isStatic, modifiers, privacy

 

Methods inherited from class org.jmlspecs.checker.JmlNode

enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString

 

Methods inherited from class org.multijava.mjc.JPhylum

check, check, check, check, fail, fail, fail, warn, warn, warn, warn

 

Methods inherited from class org.multijava.util.compiler.Phylum

getTokenReference, setTokenReference

 

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

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

storeRef

protected JmlStoreRefExpression storeRef

An AST for the storeRef expression of the more abstract variable in this.

specExpression

private JmlSpecExpression specExpression

predicate

private JmlPredicate predicate

JmlRepresentsDecl

public JmlRepresentsDecl(TokenReference where,
                         long modifiers,
                         boolean redundantly,
                         JmlStoreRefExpression storeRef,
                         JmlSpecExpression specExpression)

Creates a new JmlRepresentsDecl instance.

Parameters:

where - a TokenReference value

modifiers - modifier bit-mask

redundantly - true ==> this is a representsDecl_redundantly statement

storeRef - the model variable whose representation is being defined

specExpression - the abstract function that gives the value of storeRef based on its dependees

JmlRepresentsDecl

public JmlRepresentsDecl(TokenReference where,
                         long modifiers,
                         boolean redundantly,
                         JmlStoreRefExpression storeRef,
                         JmlPredicate predicate)

Creates a new JmlRepresentsDecl instance.

Parameters:

where - a TokenReference value

modifiers - modifier bit-mask

redundantly - true ==> this is a representsDecl_redundantly statement

storeRef - the model variable whose representation is being defined

predicate - the abstract relation that relates the value of storeRef to its dependees

storeRef

public JmlStoreRefExpression storeRef()

Returns the store ref expression of this represents declaration.

specExpression

public JmlSpecExpression specExpression()

Returns the spec expression of this represents declaration. If this declaration uses an abstraction relation, null is returned.

predicate

public JmlPredicate predicate()

Returns the predicate of this represents declaration. If this declaration uses an abstraction function, null is returned.

usesAbstractionFunction

public boolean usesAbstractionFunction()

Indicates whether this represents declaration uses an abstraction function.

 ensures \result <==> specExpression != null;
 

usesAbstractionRelation

public boolean usesAbstractionRelation()

Indicates whether this represents declaration uses an abstraction relations.

 ensures \result <==> predicate != null;
 

ident

public String ident()

Returns the identifier of the represented model field. This method can be called before typechecking. But to get the accurate result, one should call the getField method after typechecking.

getField

public JmlSourceField getField()

Returns the JmlSourceField of the model variable that this represents clause specifies for. This method must be called after typechecking.

typecheck

public void typecheck(CContextType context)
               throws PositionedError

Typechecks this depends/represents clause in the context in which it appears. The type checking rules for depends/represents clauses are defined as follows.

• Both left-hand side and right-hand side must be type-correct.
• The store-ref must be a reference to a model field.
• A non-static clause must not have a static model variable on the left-hand side (i.e., store-ref).
• A static clause must appear in the same type where the model variable on the left-hand side is declared.
• For a non-static clause, the model variable on the left-hand side must be declared in the current class, superclasses, interfaces, or outter classes or interfaces.

Parameters:

context - the context in which this type declaration appears

Throws:

PositionedError - if any checks fail

checkStoreRef

protected void checkStoreRef(JmlExpressionContext context)
                      throws PositionedError

Checks the store ref of this depends/represents clause. The store ref on the left-hand side must be type-correct and refer to a model field. If this clause is non-static, the store ref must refer to a non-static model field. For static, this clause must appear in the same class (interface) where the model field on the left-hand side is declared in. For non-static, this clause must appear in in a type descended from or nested in the type where the model field (on the left-hand side) is declared.

Throws:

PositionedError

checkRightHandSide

protected void checkRightHandSide(JmlExpressionContext context)
                           throws PositionedError

Performs type-checking of right-hand side of the represents clause. E.g., typechecks the right-hand side spec-expression (or predicate). For a functional abstraction form, the spec-expression must be assignment-compatible to the model field on the left-hand side.

Throws:

PositionedError

isInheritedOrOuter

protected static boolean isInheritedOrOuter(JClassFieldExpression field)

Returns true if the given field expression refers to a field declared in this class, inherited from a superclasse or interface, or defined in an outer class or interface.

accept

public void accept(MjcVisitor p)

Accepts the specified visitor.

Overrides:

accept in class JmlDeclaration

Parameters:

p - the visitor