|
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 |
java.lang.Objectescjava.translate.Frame
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
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 |
private final Translate translator
private final boolean issueCautions
private final RoutineDecl rdCurrent
private final java.util.Hashtable premap
private boolean pFreshResult
private static final Identifier thisId
private java.lang.String kindOfModCheck
private boolean definitelyNotAssignable
Constructor Detail |
public Frame(Translate t, boolean issueCautions, RoutineDecl rdCurrent, java.util.Hashtable premap)
t
- The instance of Translate to which this Frame belongsissueCautions
- Whether to issue Caution messages to the userrdCurrent
- The RoutineDecl whose body is being translatedpremap
- The mapping to pre-state values to be used in translationMethod Detail |
public boolean isDefinitelyNotAssignable(Expr eod, FieldDecl fd)
eod
- The object whose field is being assigned, or null if the field
is staticfd
- The declaration corresponding to the field being assigned.
void modifiesCheckField(Expr lhs, int callLoc, FieldDecl fd)
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 assignedprivate Expr modifiesCheckFieldHelper(Expr eod, int callLoc, FieldDecl fd, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
eod
- The object owning the field being assigned; null if the field
is staticcallLoc
- The location of the field access being assigned tofd
- The declaration of the field being assigned tocalleeLoc
- The location of the assignment or method callcallee_tprecondition
- The precondition under which the callee might
assign this field; null is equivalent to truegenExpr
- true if an Expr containing the formjula to be checked is
to be returned, false if checks are to be inserted in the codemg
- the set of specifications against which the assignment of the
field is to be testedthisexpr
- the expression to be used for 'this' in translating
input expressions, or null if no translation is to be doneargs
- the set of variable mappings to be used in translation
void modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions, Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, TypeDecl td_callee)
calleeFrameConditions
- the frame conditions of the calleeeod
- the receiver object of the callloccall
- the location of the callargs
- the mapping of the arguments of the callfreshResult
- - true if eod is known to be fresh since the prestatetd_callee
- The TypeDecl in which the called method is declaredprivate Expr modifiesCheckMethod(Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, java.lang.Object calleeStoreRef, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg)
eod
- The receiver object of the called methodloccall
- The location of the callargs
- The mapping to be used for callee variablesfreshResult
- 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 checkcallee_tprecondition
- The precondition of the store-ref under investigationgenExpr
- if true, an expression is returned that must be true to allow
the store-ref; if false, a check is created and null is returnedmg
- the caller frame conditions against which to check
void modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc)
array
- the array object whose element is being assignedarrayIndex
- the index of the elemtn being assignedcallLoc
- the location of the assignmentprivate Expr modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
array
- the array object whose element is being assignedarrayIndex
- the index of the elemtn being assignedcallLoc
- the location of the assignmentcalleeLoc
- callee_tprecondition
- The precondition under which the callee might
assign this array element; null is equivalent to truegenExpr
- true if an Expr containing the formula to be checked is
to be returned, false if checks are to be inserted in the codemg
- the set of specifications against which the assignment of the
field is to be testedthisexpr
- the expression to be used for 'this' in translating
input expressions, or null if no translation is to be doneargs
- the set of variable mappings to be used in translation
private void addAllocExpression(ExprVec ev, Expr e)
Also uses pFreshResult, which must be true iff e is known to be fresh since the prestate.
ev
- A vector to accumulate assertionse
- An expression to be tested for freshnessprivate Expr modChecksComplete(Expr precondition, Expr tprecond2, ExprVec ev, int callLoc, int aloc, int aloc2, boolean genExpr)
precondition
- A precondition, not yet translatedtprecond2
- A second, already translated, precondition
(possibly null, meaning true)ev
- Disjunction of conditions to be proven; an empty list means falsecallLoc
- Location of the assignment statement or method callaloc
- First associated location, possibly nullaloc2
- Second associated location, possibly nullgenExpr
- if true, returns an Expr that must be true;
if false, creates a check for that expression and
returns null
private Expr modTranslate(Expr e, boolean old, Expr thisexpr, java.util.Hashtable args)
e
- the Expr to translateold
- 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)
private boolean isTrueLiteral(Expr p)
p
- The expression to be tested
|
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 |