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

escjava.translate
Class Frame

java.lang.Object
  extended byescjava.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

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

The ESC/Java2 Project Homepage