Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.translate
Class Frame

    java.lang.Object
      escjava.translate.Frame

public class Frame
extends java.lang.Object

Author:
  David Cok This class contains methods for handling frame conditions.

  Note the following about the implementation of Modifies Pragmas. The desugared frame specifications of a method are contained in a ModifiesGroupPragmaVec, which is a vector of ModifiesGroupPragma elements. Each ModifiesGroupPragma instance corresponds to the frame conditions for a single specification case. Since each specification case of a method must be independently satisfied, each ModifiesGroupPragma must be satisfied.

  A ModifiesGroupPragma contains a precondition (the Expr .precondition) and a set of CondExprModifierPragma elements in a CondExprModifierPragmaVec. Each CondExprModifierPragma corresponds to one store-ref location as might be listed in an assignable clause (e.g. a field, an array reference, wild-card items such as obj.* or array[*], array ranges such as array[i..j]). The Expr that is in a CondExprModifierPragma is obsolete. [It used to be that an assignable clause had an optional conditional expression, but that has been deprecated.] The list of store-refs in a ModifierGroupPragma is essentially a union - within a specification case a specifier can list multiple store-ref locations that may be assigned. A particular assignment statement will have a lhs which must match one of the store-ref locations in the ModifiesGroup Pragma, and must do so for each ModifiesGroupPragma in the ModifiesGroupPragmaVec.

Nested Class Summary
`(package private) static class` | `Frame.ModifiesIterator` This class enables iterating over the set of store-ref locations in a ModifiesGroupPragma.

Field Summary
`private boolean` | `definitelyNotAssignable` A private variable used to get information without using the return value, in support of method isDefinitelylNotAssignable.
`private boolean` | `issueCautions` The value of issueCautions obtained from the Translate owner
`private java.lang.String` | `kindOfModCheck` The kind of expression being checked, e.g. assignment or method call.
`private boolean` | `pFreshResult` This holds a value across recursive invocations of methods within this class; it designates that the object whose field is being assigned is known to be fresh.
`private java.util.Hashtable` | `premap` The mapping to be used for \old variables to get pre-state values
`private RoutineDecl` | `rdCurrent` The RoutineDecl whose body is in the process of being translated
`private static Identifier` | `thisId` A precomputed Identifier for 'this', to be used in constructing Expressions.
`private Translate` | `translator` The Translate instance that owns this instance of Frame

Constructor Summary
`Frame(Translate t, boolean issueCautions, RoutineDecl rdCurrent, java.util.Hashtable premap)` The constructor of a Frame instance; should be called only from Translate

Method Summary
`private void` | `addAllocExpression(ExprVec ev, Expr e)` Adds an expression into ev stating that e is allocated now but was not allocated in the pre-state.
`boolean` | `isDefinitelyNotAssignable(Expr eod, FieldDecl fd)` This method returns whether the given field (fd) of the given object (eod) (which is null if the field is static) is definitely not allowed to be assigned according to the specs of the current RoutineDecl.
`private boolean` | `isTrueLiteral(Expr p)` A utility function that returns true if the argument expression is null or strictly equal to a boolean TRUE.
`private Expr` | `modChecksComplete(Expr precondition, Expr tprecond2, ExprVec ev, int callLoc, int aloc, int aloc2, boolean genExpr)` Generates the actual check with the condition 'if (precondition && tprecond2) then (disjunction of ev)'
`(package private) void` | `modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc)` This adds checks for whether the given array with the given index may be assigned to.
`private Expr` | `modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)` This adds checks for whether the given array with the given index may be assigned to.
`(package private) void` | `modifiesCheckField(Expr lhs, int callLoc, FieldDecl fd)` This method generates checks that the field in lhs is allowed to be assigned according to the specification of the current RoutineDecl (rdCurrent).
`private Expr` | `modifiesCheckFieldHelper(Expr eod, int callLoc, FieldDecl fd, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)` This is a helper method to generate checks that a particular field assignment is allowed by the frame conditions.
`private Expr` | `modifiesCheckMethod(Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, java.lang.Object calleeStoreRef, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg)` Helper method that checks that a particular store-ref in the frame conditions of a called method against the frame conditions of the caller.
`(package private) void` | `modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions, Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, TypeDecl td_callee)` This method generates checks that the locations possibly assigned by a called method are allowed to be assigned by the caller.
`private Expr` | `modTranslate(Expr e, boolean old, Expr thisexpr, java.util.Hashtable args)` Translates the Expr e into guarded commands: if old is true, uses the premap to map variables if old is false, uses args as the variable mapping

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### translator

    private final Translate translator

  The Translate instance that owns this instance of Frame

### issueCautions

    private final boolean issueCautions

  The value of issueCautions obtained from the Translate owner

### rdCurrent

    private final RoutineDecl rdCurrent

  The RoutineDecl whose body is in the process of being translated

### premap

    private final java.util.Hashtable premap

  The mapping to be used for \old variables to get pre-state values

### pFreshResult

    private boolean pFreshResult

  This holds a value across recursive invocations of methods within this class; it designates that the object whose field is being assigned is known to be fresh.

### thisId

    private static final Identifier thisId

  A precomputed Identifier for 'this', to be used in constructing Expressions.

### kindOfModCheck

    private java.lang.String kindOfModCheck

  The kind of expression being checked, e.g. assignment or method call. Used in the message displayed to the user when the check fails.

### definitelyNotAssignable

    private boolean definitelyNotAssignable

  A private variable used to get information without using the return value, in support of method isDefinitelylNotAssignable.

Constructor Detail

### Frame

    public Frame(Translate t,
                 boolean issueCautions,
                 RoutineDecl rdCurrent,
                 java.util.Hashtable premap)

  The constructor of a Frame instance; should be called only from Translate

Parameters:
  `t` - The instance of Translate to which this Frame belongs
  `issueCautions` - Whether to issue Caution messages to the user
  `rdCurrent` - The RoutineDecl whose body is being translated
  `premap` - The mapping to pre-state values to be used in translation

Method Detail

### isDefinitelyNotAssignable

    public boolean isDefinitelyNotAssignable(Expr eod,
                                             FieldDecl fd)

  This method returns whether the given field (fd) of the given object (eod) (which is null if the field is static) is definitely not allowed to be assigned according to the specs of the current RoutineDecl. By definitely not allowed, we mean that it can be determined without needing to prove the truth or falsity of a given expression. For example, if the FieldDecl is nowhere mentioned in the ModifiesGroupPragma, then it definitely may not be assigned. In a situation where the assignable clause contained something like .field where field matches fd, then the assignment is allowed if == eod. But that would have to be proved: it might be that the assignment is not allowed, if != eod, but we don't definitely know for sure.

  Parameters:
    `eod` - The object whose field is being assigned, or null if the field is static
    `fd` - The declaration corresponding to the field being assigned.
  Returns:
    true if it is known without a prover that the field may not be assigned; false if it may or possibly may be assigned

### modifiesCheckField

    void modifiesCheckField(Expr lhs,
                            int callLoc,
                            FieldDecl fd)

  This method generates checks that the field in lhs is allowed to be assigned according to the specification of the current RoutineDecl (rdCurrent). This may depend on the object whose field is being assigned. This is called for both static and instance fields.

  Parameters:
    `lhs` - The expression being assigned to (which will be a field dereference).
    `callLoc` - The location of the field access expression (the lhs).
    `fd` - The location of the declaration of the field being assigned

### modifiesCheckFieldHelper

    private Expr modifiesCheckFieldHelper(Expr eod,
                                          int callLoc,
                                          FieldDecl fd,
                                          int calleeLoc,
                                          Expr callee_tprecondition,
                                          boolean genExpr,
                                          ModifiesGroupPragmaVec mg,
                                          Expr thisexpr,
                                          java.util.Hashtable args)

  This is a helper method to generate checks that a particular field assignment is allowed by the frame conditions.

  Parameters:
    `eod` - The object owning the field being assigned; null if the field is static
    `callLoc` - The location of the field access being assigned to
    `fd` - The declaration of the field being assigned to
    `calleeLoc` - The location of the assignment or method call
    `callee_tprecondition` - The precondition under which the callee might assign this field; null is equivalent to true
    `genExpr` - true if an Expr containing the formjula to be checked is to be returned, false if checks are to be inserted in the code
    `mg` - the set of specifications against which the assignment of the field is to be tested
    `thisexpr` - the expression to be used for 'this' in translating input expressions, or null if no translation is to be done
    `args` - the set of variable mappings to be used in translation
  Returns:
    the expression that must be true to allow the assignment, if genExpr is true; if genExpr is false, null is returned

### modifiesCheckMethodI

    void modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions,
                              Expr eod,
                              int loccall,
                              java.util.Hashtable args,
                              boolean freshResult,
                              TypeDecl td_callee)

  This method generates checks that the locations possibly assigned by a called method are allowed to be assigned by the caller.

  Parameters:
    `calleeFrameConditions` - the frame conditions of the callee
    `eod` - the receiver object of the call
    `loccall` - the location of the call
    `args` - the mapping of the arguments of the call
    `freshResult` - - true if eod is known to be fresh since the prestate
    `td_callee` - The TypeDecl in which the called method is declared

### modifiesCheckMethod

    private Expr modifiesCheckMethod(Expr eod,
                                     int loccall,
                                     java.util.Hashtable args,
                                     boolean freshResult,
                                     java.lang.Object calleeStoreRef,
                                     Expr callee_tprecondition,
                                     boolean genExpr,
                                     ModifiesGroupPragmaVec mg)

  Helper method that checks that a particular store-ref in the frame conditions of a called method against the frame conditions of the caller.

  Parameters:
    `eod` - The receiver object of the called method
    `loccall` - The location of the call
    `args` - The mapping to be used for callee variables
    `freshResult` - true if the receiver is known to be fresh (allocated since the pre-state of the caller)
    `calleeStoreRef` - the store-ref of the callee to check
    `callee_tprecondition` - The precondition of the store-ref under investigation
    `genExpr` - if true, an expression is returned that must be true to allow the store-ref; if false, a check is created and null is returned
    `mg` - the caller frame conditions against which to check
  Returns:
    if genExpr is true, the expression that constitutes the condition that must be true if the frame condition is to be allowed is returned; if genExpr is false, null is returned (a assertion check is inserted into the generated guarded commands)

### modifiesCheckArray

    void modifiesCheckArray(Expr array,
                            Expr arrayIndex,
                            int callLoc)

  This adds checks for whether the given array with the given index may be assigned to.

  Parameters:
    `array` - the array object whose element is being assigned
    `arrayIndex` - the index of the elemtn being assigned
    `callLoc` - the location of the assignment

### modifiesCheckArray

    private Expr modifiesCheckArray(Expr array,
                                    Expr arrayIndex,
                                    int callLoc,
                                    int calleeLoc,
                                    Expr callee_tprecondition,
                                    boolean genExpr,
                                    ModifiesGroupPragmaVec mg,
                                    Expr thisexpr,
                                    java.util.Hashtable args)

  This adds checks for whether the given array with the given index may be assigned to.

  Parameters:
    `array` - the array object whose element is being assigned
    `arrayIndex` - the index of the elemtn being assigned
    `callLoc` - the location of the assignment
    `calleeLoc` -
    `callee_tprecondition` - The precondition under which the callee might assign this array element; null is equivalent to true
    `genExpr` - true if an Expr containing the formula to be checked is to be returned, false if checks are to be inserted in the code
    `mg` - the set of specifications against which the assignment of the field is to be tested
    `thisexpr` - the expression to be used for 'this' in translating input expressions, or null if no translation is to be done
    `args` - the set of variable mappings to be used in translation
  Returns:
    the expression that must be true to allow the assignment, if genExpr is true; if genExpr is false, null is returned

### addAllocExpression

    private void addAllocExpression(ExprVec ev,
                                    Expr e)

  Adds an expression into ev stating that e is allocated now but was not allocated in the pre-state. No expression is added to ev if it is definitely false that e is fresh - such as if e is this or is null (meaning the field is static). Otherwise if pFreshResult is true, a literal True expression is added. Otherwise some non-trivial expression is added.

  Also uses pFreshResult, which must be true iff e is known to be fresh since the prestate.

  Parameters:
    `ev` - A vector to accumulate assertions
    `e` - An expression to be tested for freshness

### modChecksComplete

    private Expr modChecksComplete(Expr precondition,
                                   Expr tprecond2,
                                   ExprVec ev,
                                   int callLoc,
                                   int aloc,
                                   int aloc2,
                                   boolean genExpr)

  Generates the actual check with the condition 'if (precondition && tprecond2) then (disjunction of ev)'

  Parameters:
    `precondition` - A precondition, not yet translated
    `tprecond2` - A second, already translated, precondition (possibly null, meaning true)
    `ev` - Disjunction of conditions to be proven; an empty list means false
    `callLoc` - Location of the assignment statement or method call
    `aloc` - First associated location, possibly null
    `aloc2` - Second associated location, possibly null
    `genExpr` - if true, returns an Expr that must be true; if false, creates a check for that expression and returns null
  Returns:
    The expr to be proved true, if genExpr is true; if genExpr is false, returns null

### modTranslate

    private Expr modTranslate(Expr e,
                              boolean old,
                              Expr thisexpr,
                              java.util.Hashtable args)

  Translates the Expr e into guarded commands:
  if old is true, uses the premap to map variables if old is false, uses args as the variable mapping

  Parameters:
    `e` - the Expr to translate
    `old` - if true, translates in the context of the pre-state (using the mapping in the class field 'premap'
    `thisexpr` - the Expr to use for 'this'
    `args` - the mapping to use if old is false (if args is not null)
  Returns:
    the translated expression

### isTrueLiteral

    private boolean isTrueLiteral(Expr p)

  A utility function that returns true if the argument expression is null or strictly equal to a boolean TRUE.

  Parameters:
    `p` - The expression to be tested
  Returns:
    true if the argument is null or a Boolean LiteralExpr with value true

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage