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 Translate

java.lang.Object
  extended byescjava.translate.Translate

public final class Translate
extends java.lang.Object


Nested Class Summary
 class Translate.EverythingLoc
           
static class Translate.Strings
           
 
Field Summary
static java.util.Set axsToAdd
           
private  Identifier cacheVar
           
private  StackVector code
          Contains the guarded commands generated so far for the current method.
private  GuardedCmdVec codevec
           
private  StackVector declaredLocals
          Contains the local Java variables declared in the current block so far for the current block and enclosing blocks of the current method.
(package private)  Frame frameHandler
           
private  boolean inConstructorContext
          Indicates whether or not the current routine is in a "constructor context", meaning that it is a constructor being checked or a method in the same class that's being inlined into the constructor.
 int inlineCheckDepth
           
static ASTDecoration inlineDecoration
          Describes what aspects of an inlined call to check and what aspects to either assert or simply ignore.
 int inlineDepthPastCheck
           
private  Translate inlineParent
          Singly-linked list of the inline parents.
private  boolean issueCautions
          Indicates whether to issue cautions.
private  java.util.ArrayList locList
           
private  ExprStmtPragmaVec loopDecreases
          List of loop decreases pragmas seen so far (and not yet used) within the current method.
private  ExprStmtPragmaVec loopinvariants
          List of loop invariant pragmas seen so far (and not yet used) within the current method.
private  ExprStmtPragmaVec loopPredicates
           
 java.util.ArrayList modifyEverythingLocations
           
private  ExprVec mutexList
          Used by readCheck and writeCheck to accumulate the list of mutexes protecting a shared variable.
private  Set predictedSynTargs
          Describes the current predicted set of synTargs.
private  java.util.Hashtable premap
           
private  java.util.Hashtable premapWithArgs
           
private  RoutineDecl rdCurrent
          References the routine currently being checked by trBody.
private  FindContributors scope
          Describes the current scope.
protected  LocalVarDeclVec skolemConstants
           
private  StackVector temporaries
          Contains the temporaries that generated for the current method that haven't yet been declared in a VARINCMD.
private  int tmpcount
          Countains the number of temporaries generated for the method currently being translated.
private  TypeDecl typeDecl
          The type containing the routine whose body is being translated.
 
Constructor Summary
Translate()
           
 
Method Summary
private  void addAssumption(Expr pred)
           
private  void addAssumptions(ExprVec ev)
           
private  void addCheck(ASTNode use, int errorName, Expr pred)
          Calls GC.check to create a check and appends the result to code.
private  void addCheck(int locUse, Condition cond)
          Calls GC.check to create a check and appends the result to code.
(package private)  void addCheck(int locUse, int errorName, Expr pred)
          Calls GC.check to create a check and appends the result to code.
private  void addCheck(int locUse, int errorName, Expr pred, ASTNode prag)
          Calls GC.check to create a check and appends the result to code.
private  void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl)
          Calls GC.check to create a check and appends the result to code.
(package private)  void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc)
           
private  void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, java.lang.Object aux)
          Calls GC.check to create a check and appends the result to code.
private  void addLoopDecreases(LoopCmd loop, int piece)
          Adds to code the various pieces of the translation of the decreases pragma.
 void addMoreLocations(java.util.Set s)
           
private  void addNewAssumptions()
           
private  void addNewAssumptionsHelper()
           
(package private)  ExprVec addNewAssumptionsNow()
           
private  void addNewAssumptionsNow(ExprVec ev)
           
 Expr addNewString(VarInit x, Expr left, Expr right)
           
private static Expr addRelAsgCast(Expr rval, Type lType, Type rType)
           
static void addTraceLabelSequenceNumbers(GuardedCmd gc)
          Destructively change the trace labels in gc to insert sequence numbers that are used by the ErrorMsg class in printing trace labels in the correct execution order.
private  VariableAccess adorn(VariableAccess v)
          Make a fresh version of a special variable to save it in.
private  void arrayAccessCheck(Expr Array, Expr array, Expr Index, Expr index, int locOpenBracket)
          Emit the checks that array is non-null and that index is inbounds for array.
private  Expr breakLabel(Stmt s)
           
 VariableAccess cacheValue(Expr e)
           
private  Call call(RoutineDecl rd, ExprVec argsRaw, ExprVec args, FindContributors scope, int scall, int ecall, int locOpenParen, boolean superOrSiblingConstructorCall, InlineSettings inline, Expr eod, boolean freshResult)
          Creates and desugars a call node, extended to allow the possibility of inlining a call.
private  void checkLoopInvariants(LoopCmd loop, ExprVec axs)
          Add to "code" checks for all loop invariants of "loop".
private  GuardedCmd cloneGuardedCommand(GuardedCmd gc)
          This method returns a guarded command G that is like gc except that where gc contains a mutable command, G contains a fresh copy of that command.
private  InlineSettings computeInlineSettings(RoutineDecl rd, ExprVec argsRaw, InlineSettings inline, int scall)
          Computes the inlining settings for a given call.
private  Expr continueLabel(Stmt s)
           
private  void desugarLoopFast(LoopCmd loop, ExprVec axs)
          Desugars loop according to the fast option.
 void desugarLoopSafe(LoopCmd loop, ExprVec axs)
          Desugars loop according to the safe option.
private  VariableAccess fresh(VarInit e, int loc)
          Generate a temporary for the result of a given expression.
private  VariableAccess fresh(VarInit e, int loc, java.lang.String suffix)
           
private  TypeExpr getClassObject(TypeDecl tdClass)
           
private static VariableAccess getInitVar(GenericVarDecl d)
          Return the VariableAccesss associated with d by a call to setInitVar.
static void globallyTurnOffChecks(boolean flag)
          If the flag is true, set all assertion checks to assumes.
private  void guard(Expr e, Expr label)
          Computes purity information for Java expression e, translates e (emitting any code needed to account for impurities or side effects in the expression), and emits code that performs a RAISE label command if the expression evaluates to false.
private  VariableAccess initadorn(LocalVarDecl d)
          Make a fresh "boolean" variable to hold the initialized status of a Java variable that is marked as "uninitialized".
private  java.util.Hashtable initializeRWCheckSubstMap(java.util.Hashtable prevMap, Expr actualSelf, int loc)
          The following method is used in readCheck and writeCheck to lazily construct a substitution map (which may also create another temporary variable).
private  void instanceInitializers(TypeDecl tdecl)
          This method implements "InstanceInitializers", as described in section 8.1 of ESCJ 16.
private  void instanceInitializeZero(TypeDecl tdecl)
          Called by instanceInitializers.
static boolean isFinal(Type t)
           
private  boolean isRecursiveInvocation(RoutineDecl r)
           
private  boolean isStandaloneConstructor(RoutineDecl rd)
           
private  void makeLoop(int sLoop, int eLoop, int locHotspot, GenericVarDeclVec tempVars, GuardedCmd guard, GuardedCmd body, ExprStmtPragmaVec J, ExprStmtPragmaVec decreases, LocalVarDeclVec skolemConsts, ExprStmtPragmaVec P, Expr label)
          Appends to code commands that make up a loop with nominal body guard;body, where label is raised within body to terminate the loop.
static Expr mapLocation(Expr e, int loc)
           
private  GuardedCmd modify(Expr e, java.util.Hashtable pt, int loc)
           
 GuardedCmd modify(Set simpleTargets, int loc)
           
private  GuardedCmd modify(VariableAccess va, int loc)
          Modifies a GC designator.
 GuardedCmd modifyATargets(Set aTargets, int loc)
          targets is set of GenericVarDecls. aTargets is set of ATargets.
private  void nullCheck(VarInit E, Expr e, int loc)
          Emit a check at location loc that guarded command expression e, which was translated from the Java expression E, is not null.
private  void nullCheck(VarInit E, Expr e, int loc, int errorName, int locPragma)
           
private  GuardedCmd opBlockCmd(Expr label)
          Reduces number of stack marks by 1.
private static int orderTraceLabel(LabelExpr le, int count)
          If the given label is a trace label, add the count number to the given label expression's label name, so that trace labels will sort correctly.
private static int orderTraceLabels(GuardedCmd gc, int count)
          Walk through the guarded command translation of a method, adding unique number to its location sequence, in order to sort trace labels in order of execution.
private  GuardedCmd popDeclBlock()
          Pops the code and declared local variables, makes these into a command (usually a VAR ..
private static Expr predArrayOwnerNull(VariableAccess allocOld, VariableAccess allocNew, VariableAccess arr)
          Returns the guarded-command expression: (FORALL o :: !
private static Expr predEvathangsAnArray(VariableAccess allocOld, VariableAccess allocNew)
          Returns the guarded-command expression: (FORALL o :: !
private  Expr protect(boolean protect, Expr e, int loc)
          Extends the code array with a command that evaluates e and returns an expession which denotes this value in the poststate of that command.
private  Expr protect(boolean protect, Expr e, int loc, java.lang.String suffix)
           
private  Expr ptrExpr(VarInit expr)
          Purify and translate expr without protection
private  void raise(Expr label)
          Emits the commands EC= label; raise to code.
private  void readCheck(Expr va, int locId)
          Insert checks done before reading variables.
private static void setInitVar(GenericVarDecl d, VariableAccess init)
          Associates init with d; will be returned by a call to getInitVar.
(package private) static void setop(ASTNode e)
           
private  GuardedCmd spill()
          Pops temporaries and code, and makes these into a VARINCMD command that is returned.
private static GuardedCmd substituteGC(java.util.Hashtable pt, GuardedCmd gc)
          When a call is inlined, we need to substitute the new names given to its formal parameters for its original names in the inlined body.
private  VariableAccess temporary(java.lang.String s, int locAccess)
          Generate a temporary variable with prefix s and associated expression location information locAccess.
private  VariableAccess temporary(java.lang.String s, int locAccess, int locIdDecl)
           
private  GuardedCmd traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag)
           
private  GuardedCmd traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag, int loc)
           
private  GuardedCmd traceInfoLabelCmd(int sloc, int eloc, java.lang.String traceInfoTag, int loc)
           
private  GuardedCmd traceInfoLabelCmd(int sloc, int eloc, java.lang.String traceInfoTag, java.lang.String sortSeq)
           
 GuardedCmd trBody(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap, Set predictedSynTargs, Translate inlineParent, boolean issueCautions)
          Translates the body of a method or constructor, as described in ESCJ 16, section 8.
private  void trConstructorBody(ConstructorDecl cd, java.util.Hashtable premap)
          Auxiliary routine used by trBody to translate the body of a constructor, as described in ESCJ 16, section 8.
private  void trConstructorCallStmt(ConstructorInvocation ci)
          This method implements "TrConstructorCallStmt" as described in section 6 of ESCJ 16.
private  Expr trExpr(boolean protect, VarInit expr)
          Translate expr into a sequence of guarded commands that are appended to code and return an expression denoting the value of the expression.
private  Expr trFieldAccess(boolean protectObject, FieldAccess fa)
          Returns either a VariableAccess if fa is a class variable or a SELECT application if fa is an instance variable access, or an ARRAYLENGTH application if fa is the final array field length.
private  void trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl)
          Translate an "if" statement.
private  VarInit trim(VarInit E)
          Peels off parentheses and casts from E and returns the result
private  Expr trMethodInvocation(boolean protect, MethodInvocation mi)
          This translation of method invocation follows section 4.1 of ESCJ 16.
private  void trStmt(Stmt stmt, TypeDecl decl)
          Translate stmt into a sequence of guarded commands that are appended to code.
private  void trSynchronizedBody(Expr mu, Stmt stmt, int loc, TypeDecl decl)
           
private  void wrapUpDeclBlock()
          Pops declaredLocals and code and then appends code with a VARINCMD (if there were any new declared locals) or a sequence of commands (otherwise).
private  GuardedCmd wrapUpUnrolledIteration(java.lang.String locString, int iteration, GenericVarDeclVec tempVars)
           
private  void writeCheck(Expr va, VarInit Rval, Expr rval, int locAssignOp, boolean inInitializerContext)
          Insert checks done before writing variables, as prescribed by WriteCheck in ESCJ 16.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

frameHandler

Frame frameHandler

axsToAdd

public static java.util.Set axsToAdd

premap

private java.util.Hashtable premap

premapWithArgs

private java.util.Hashtable premapWithArgs

typeDecl

private TypeDecl typeDecl
The type containing the routine whose body is being translated.


rdCurrent

private RoutineDecl rdCurrent
References the routine currently being checked by trBody.


inlineParent

private Translate inlineParent
Singly-linked list of the inline parents. Is null if this translation is not being inlined.


issueCautions

private boolean issueCautions
Indicates whether to issue cautions. Value is set from outer call to trBody and also used by nested/recursive calls.


inConstructorContext

private boolean inConstructorContext
Indicates whether or not the current routine is in a "constructor context", meaning that it is a constructor being checked or a method in the same class that's being inlined into the constructor.


code

private final StackVector code
Contains the guarded commands generated so far for the current method. As the translation enters into Java blocks, code gets pushed. As blocks are left, code is poped into a GuardedCmdVec which is wrapped inside a BLOCK guarded command that gets appended onto code.


loopinvariants

private ExprStmtPragmaVec loopinvariants
List of loop invariant pragmas seen so far (and not yet used) within the current method.


loopDecreases

private ExprStmtPragmaVec loopDecreases
List of loop decreases pragmas seen so far (and not yet used) within the current method.


loopPredicates

private ExprStmtPragmaVec loopPredicates

skolemConstants

protected LocalVarDeclVec skolemConstants

declaredLocals

private final StackVector declaredLocals
Contains the local Java variables declared in the current block so far for the current block and enclosing blocks of the current method. This variable is maintained parallel to code: Each time a Java block is entered, declaredLocals gets pushed; when a block is left, declaredLocals is popped into a GenericVarDeclVec that gets wrapped inside a BLOCK guarded command.


temporaries

private final StackVector temporaries
Contains the temporaries that generated for the current method that haven't yet been declared in a VARINCMD.


scope

private FindContributors scope
Describes the current scope.


predictedSynTargs

private Set predictedSynTargs
Describes the current predicted set of synTargs.

If non-null, then represents an *upper* bound on freeVars of the result of the current trBody(...) call.


inlineDecoration

public static final ASTDecoration inlineDecoration
Describes what aspects of an inlined call to check and what aspects to either assert or simply ignore. A call (MethodInvocation, ConstructorInvocation, NewInstanceExpr) may map to an InlineSettings object in which the nextInlineCheckDepth and nextInlineDepthPastCheck fields are unused.

This variable is used only for some call-site specific inlining, in particular, currently only to handle the -inlineConstructors flag. Other reasons for inlining are taken care of in method computeInlineSettings.


mutexList

private ExprVec mutexList
Used by readCheck and writeCheck to accumulate the list of mutexes protecting a shared variable. Thus, these methods are not thread re-entrant.


locList

private java.util.ArrayList locList

inlineCheckDepth

public int inlineCheckDepth

inlineDepthPastCheck

public int inlineDepthPastCheck

tmpcount

private int tmpcount
Countains the number of temporaries generated for the method currently being translated.

Reset to 0 on entry to trExpr(boolean, VarInit).


modifyEverythingLocations

public java.util.ArrayList modifyEverythingLocations

codevec

private GuardedCmdVec codevec

cacheVar

private Identifier cacheVar
Constructor Detail

Translate

public Translate()
Method Detail

trBody

public GuardedCmd trBody(RoutineDecl rd,
                         FindContributors scope,
                         java.util.Hashtable premap,
                         Set predictedSynTargs,
                         Translate inlineParent,
                         boolean issueCautions)
Translates the body of a method or constructor, as described in ESCJ 16, section 8.

Parameters:
predictedSynTargs - for correct translation, this must contain an upper bound for the syntactic targets of the result of this call. A value of null is taken to represent the set of all variables & is hence always a safe value.
Note:
passing a value of for predictedSynTargs will give a translation missing assert statements for checking call preconditions, but otherwise correct. The resulting computation runs faster than passing null, while still having the same set of targets. escjava.Main is currently using this trick as a kludge to compute the syntactic targets upper bound.

isStandaloneConstructor

private boolean isStandaloneConstructor(RoutineDecl rd)
Returns:
true when rd is a constructor that does not call a sibling constructor.

trConstructorBody

private void trConstructorBody(ConstructorDecl cd,
                               java.util.Hashtable premap)
Auxiliary routine used by trBody to translate the body of a constructor, as described in ESCJ 16, section 8.


getClassObject

private TypeExpr getClassObject(TypeDecl tdClass)

instanceInitializers

private void instanceInitializers(TypeDecl tdecl)
This method implements "InstanceInitializers", as described in section 8.1 of ESCJ 16.


instanceInitializeZero

private void instanceInitializeZero(TypeDecl tdecl)
Called by instanceInitializers.


spill

private GuardedCmd spill()
Pops temporaries and code, and makes these into a VARINCMD command that is returned. If there are no temporaries, only the code is returned.


adorn

private VariableAccess adorn(VariableAccess v)
Make a fresh version of a special variable to save it in. (This partially handles ESCJ 23b, case 4.)


initadorn

private VariableAccess initadorn(LocalVarDecl d)
Make a fresh "boolean" variable to hold the initialized status of a Java variable that is marked as "uninitialized". (This partially handles ESCJ 23b, case 13.)


isRecursiveInvocation

private boolean isRecursiveInvocation(RoutineDecl r)

opBlockCmd

private GuardedCmd opBlockCmd(Expr label)
Reduces number of stack marks by 1.


breakLabel

private Expr breakLabel(Stmt s)

continueLabel

private Expr continueLabel(Stmt s)

raise

private void raise(Expr label)
Emits the commands EC= label; raise to code.


guard

private void guard(Expr e,
                   Expr label)
Computes purity information for Java expression e, translates e (emitting any code needed to account for impurities or side effects in the expression), and emits code that performs a RAISE label command if the expression evaluates to false. As usual, emitted code is appended to code and temporaries are appended to temporaries.


makeLoop

private void makeLoop(int sLoop,
                      int eLoop,
                      int locHotspot,
                      GenericVarDeclVec tempVars,
                      GuardedCmd guard,
                      GuardedCmd body,
                      ExprStmtPragmaVec J,
                      ExprStmtPragmaVec decreases,
                      LocalVarDeclVec skolemConsts,
                      ExprStmtPragmaVec P,
                      Expr label)
Appends to code commands that make up a loop with nominal body guard;body, where label is raised within body to terminate the loop. The vector J contains the user-declared loop invariant pragmas. The vector decreases contains the user-declared bound function pragmas. The scope of the variables in tempVars is the nominal body; this method will wrap an appropriate var .. in .. end command around these.


desugarLoopFast

private void desugarLoopFast(LoopCmd loop,
                             ExprVec axs)
Desugars loop according to the fast option. In particular, sets loop.desugared to the desugaring.


wrapUpUnrolledIteration

private GuardedCmd wrapUpUnrolledIteration(java.lang.String locString,
                                           int iteration,
                                           GenericVarDeclVec tempVars)

addLoopDecreases

private void addLoopDecreases(LoopCmd loop,
                              int piece)
Adds to code the various pieces of the translation of the decreases pragma. The pieces are:


modifyATargets

public GuardedCmd modifyATargets(Set aTargets,
                                 int loc)
targets is set of GenericVarDecls. aTargets is set of ATargets.


modify

public GuardedCmd modify(Set simpleTargets,
                         int loc)

desugarLoopSafe

public void desugarLoopSafe(LoopCmd loop,
                            ExprVec axs)
Desugars loop according to the safe option. In particular, sets loop.desugared to the desugaring.


checkLoopInvariants

private void checkLoopInvariants(LoopCmd loop,
                                 ExprVec axs)
Add to "code" checks for all loop invariants of "loop".


traceInfoLabelCmd

private GuardedCmd traceInfoLabelCmd(ASTNode ast,
                                     java.lang.String traceInfoTag)

traceInfoLabelCmd

private GuardedCmd traceInfoLabelCmd(ASTNode ast,
                                     java.lang.String traceInfoTag,
                                     int loc)

traceInfoLabelCmd

private GuardedCmd traceInfoLabelCmd(int sloc,
                                     int eloc,
                                     java.lang.String traceInfoTag,
                                     int loc)

traceInfoLabelCmd

private GuardedCmd traceInfoLabelCmd(int sloc,
                                     int eloc,
                                     java.lang.String traceInfoTag,
                                     java.lang.String sortSeq)

cloneGuardedCommand

private GuardedCmd cloneGuardedCommand(GuardedCmd gc)
This method returns a guarded command G that is like gc except that where gc contains a mutable command, G contains a fresh copy of that command. Thus, the resulting command is as good as a fresh copy of gc, since all other guarded commands are to be read-only after construction.

There is only one mutable command, namely an "assume" command of the form:

     assume (lblpos id true)
 
where "id" is a trace label. A fresh copy of this command consists of a fresh assume command with a fresh labeled expression. However, the "id" reference may be shared in the fresh command.


wrapUpDeclBlock

private void wrapUpDeclBlock()
Pops declaredLocals and code and then appends code with a VARINCMD (if there were any new declared locals) or a sequence of commands (otherwise). The new code becomes the body of the VARINCMD or the sequence of commands.


popDeclBlock

private GuardedCmd popDeclBlock()
Pops the code and declared local variables, makes these into a command (usually a VAR .. IN .. END command, but possibly a sequence command if there are no declared local variables). The command is then returned.


trStmt

private void trStmt(Stmt stmt,
                    TypeDecl decl)
Translate stmt into a sequence of guarded commands that are appended to code.

Temporaries generated for expressions in stmt are added to temporaries, loop invariant pragmas are added to loopinvariants, decreases pragmas are added to loopDecreases, loop predicates are added to looppredicates, and local skolemized variables are added to skolemConstants.

Parameters:
stmt - the statement that is to be translated.

trIfStmt

private void trIfStmt(Expr guard,
                      Stmt thenStmt,
                      Stmt elseStmt,
                      TypeDecl decl)
Translate an "if" statement.

Design:
This method was refactored out to handle Java's "assert" keyword as well as normal "if" statements.

trSynchronizedBody

private void trSynchronizedBody(Expr mu,
                                Stmt stmt,
                                int loc,
                                TypeDecl decl)

trConstructorCallStmt

private void trConstructorCallStmt(ConstructorInvocation ci)
This method implements "TrConstructorCallStmt" as described in section 6 of ESCJ 16.


protect

private Expr protect(boolean protect,
                     Expr e,
                     int loc)
Extends the code array with a command that evaluates e and returns an expession which denotes this value in the poststate of that command. If protect is true, then the expression returned will depend only on values of temporary variables (that is, the expression returned will not be affected by changes to program variables).

If protect is true, then the value returned is certain to be of type VariableAccess.


protect

private Expr protect(boolean protect,
                     Expr e,
                     int loc,
                     java.lang.String suffix)

ptrExpr

private Expr ptrExpr(VarInit expr)
Purify and translate expr without protection


trExpr

private Expr trExpr(boolean protect,
                    VarInit expr)
Translate expr into a sequence of guarded commands that are appended to code and return an expression denoting the value of the expression. New temporaries may be generated; these are added to temporaries.

Parameters:
protect - if true, then the expression return will depend only on values of temporary variables (that is, the expression returned will not be affected by changes in program variables).

addRelAsgCast

private static Expr addRelAsgCast(Expr rval,
                                  Type lType,
                                  Type rType)

predEvathangsAnArray

private static Expr predEvathangsAnArray(VariableAccess allocOld,
                                         VariableAccess allocNew)
Returns the guarded-command expression:
 (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
              ==> isNewArray(o))
 


predArrayOwnerNull

private static Expr predArrayOwnerNull(VariableAccess allocOld,
                                       VariableAccess allocNew,
                                       VariableAccess arr)
Returns the guarded-command expression:
 (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
              ==> o.owner == null)
 


isFinal

public static boolean isFinal(Type t)
Returns:
true if there can be no subtypes of t.
Design:
The definition of final used by this method is as follows. Reference types are "final" if they have the final modifier. Array types are "final" if their element types satisfy isFinal. Primitive types are "final".

trFieldAccess

private Expr trFieldAccess(boolean protectObject,
                           FieldAccess fa)
Returns either a VariableAccess if fa is a class variable or a SELECT application if fa is an instance variable access, or an ARRAYLENGTH application if fa is the final array field length. In the second case, will emit code for computing the object designator and also a check to ensure that object is not null.


trMethodInvocation

private Expr trMethodInvocation(boolean protect,
                                MethodInvocation mi)
This translation of method invocation follows section 4.1 of ESCJ 16.


nullCheck

private void nullCheck(VarInit E,
                       Expr e,
                       int loc)
Emit a check at location loc that guarded command expression e, which was translated from the Java expression E, is not null. If E denotes an expression that is guaranteed not to be null, no check is emitted.


nullCheck

private void nullCheck(VarInit E,
                       Expr e,
                       int loc,
                       int errorName,
                       int locPragma)

trim

private VarInit trim(VarInit E)
Peels off parentheses and casts from E and returns the result


arrayAccessCheck

private void arrayAccessCheck(Expr Array,
                              Expr array,
                              Expr Index,
                              Expr index,
                              int locOpenBracket)
Emit the checks that array is non-null and that index is inbounds for array. Implements the ArrayAccessCheck function of ESCJ16.


readCheck

private void readCheck(Expr va,
                       int locId)
Insert checks done before reading variables.

This method implements ReadCheck as defined in ESCJ16. Handles reads of local, class, and instance variables (ESCJ16 splits these into two ReadCheck functions).

Parameters:
va - is the variable being read; it must be either a VariableAccess (in the case of local variables and class fields) or a SELECT NaryExpr (in the case of instance fields).
locId - is the location of the variable or field being read. It is used to determine the location of the "wrong" part of the check's label.

writeCheck

private void writeCheck(Expr va,
                        VarInit Rval,
                        Expr rval,
                        int locAssignOp,
                        boolean inInitializerContext)
Insert checks done before writing variables, as prescribed by WriteCheck in ESCJ 16. Handles writes of local, class, and instance variables (ESCJ 16 splits these into two WriteCheck functions).

Parameters:
va - is the variable being written; it must be either a VariableAccess (in the case of local variables and class fields) or a SELECT NaryExpr (in the case of instance fields).
rval - is the guarded command expression being written into va. The argument Rval is either the Java expression from which rval was translated, or null if rval was somehow synthesized.
locAssignOp - is the location of the assignment operator that prescribes the write. It is used to determine the location of the "wrong" part of the check's label.
inInitializerContext - indicates whether or not the expression whose write check is to be performed is the initializing expression of a field.

initializeRWCheckSubstMap

private java.util.Hashtable initializeRWCheckSubstMap(java.util.Hashtable prevMap,
                                                      Expr actualSelf,
                                                      int loc)
The following method is used in readCheck and writeCheck to lazily construct a substitution map (which may also create another temporary variable).


addCheck

private void addCheck(int locUse,
                      Condition cond)
Calls GC.check to create a check and appends the result to code.


addCheck

void addCheck(int locUse,
              int errorName,
              Expr pred)
Calls GC.check to create a check and appends the result to code.


addCheck

private void addCheck(ASTNode use,
                      int errorName,
                      Expr pred)
Calls GC.check to create a check and appends the result to code.


addCheck

private void addCheck(int locUse,
                      int errorName,
                      Expr pred,
                      int locPragmaDecl)
Calls GC.check to create a check and appends the result to code.


addCheck

void addCheck(int locUse,
              int errorName,
              Expr pred,
              int locPragmaDecl,
              int auxLoc)

addCheck

private void addCheck(int locUse,
                      int errorName,
                      Expr pred,
                      int locPragmaDecl,
                      java.lang.Object aux)
Calls GC.check to create a check and appends the result to code.


addCheck

private void addCheck(int locUse,
                      int errorName,
                      Expr pred,
                      ASTNode prag)
Calls GC.check to create a check and appends the result to code.


addAssumption

private void addAssumption(Expr pred)

addAssumptions

private void addAssumptions(ExprVec ev)

addNewAssumptions

private void addNewAssumptions()

addNewAssumptionsNow

ExprVec addNewAssumptionsNow()

addNewAssumptionsNow

private void addNewAssumptionsNow(ExprVec ev)

addNewAssumptionsHelper

private void addNewAssumptionsHelper()

getInitVar

private static VariableAccess getInitVar(GenericVarDecl d)
Return the VariableAccesss associated with d by a call to setInitVar. If none has been associated with d, returns null.


setInitVar

private static void setInitVar(GenericVarDecl d,
                               VariableAccess init)
Associates init with d; will be returned by a call to getInitVar.


modify

private GuardedCmd modify(VariableAccess va,
                          int loc)
Modifies a GC designator. GC designator can include SubstExpr.


modify

private GuardedCmd modify(Expr e,
                          java.util.Hashtable pt,
                          int loc)

call

private Call call(RoutineDecl rd,
                  ExprVec argsRaw,
                  ExprVec args,
                  FindContributors scope,
                  int scall,
                  int ecall,
                  int locOpenParen,
                  boolean superOrSiblingConstructorCall,
                  InlineSettings inline,
                  Expr eod,
                  boolean freshResult)
Creates and desugars a call node, extended to allow the possibility of inlining a call.


computeInlineSettings

private InlineSettings computeInlineSettings(RoutineDecl rd,
                                             ExprVec argsRaw,
                                             InlineSettings inline,
                                             int scall)
Computes the inlining settings for a given call. A return value of null means "don't inline".


globallyTurnOffChecks

public static void globallyTurnOffChecks(boolean flag)
If the flag is true, set all assertion checks to assumes. Otherwise, make sure that regular checking of assertions is performed.


substituteGC

private static GuardedCmd substituteGC(java.util.Hashtable pt,
                                       GuardedCmd gc)
When a call is inlined, we need to substitute the new names given to its formal parameters for its original names in the inlined body.


addTraceLabelSequenceNumbers

public static void addTraceLabelSequenceNumbers(GuardedCmd gc)
Destructively change the trace labels in gc to insert sequence numbers that are used by the ErrorMsg class in printing trace labels in the correct execution order. This method requires that trace labels do not yet contain sequence numbers.


orderTraceLabels

private static int orderTraceLabels(GuardedCmd gc,
                                    int count)
Walk through the guarded command translation of a method, adding unique number to its location sequence, in order to sort trace labels in order of execution. This is a destructive operation.


orderTraceLabel

private static int orderTraceLabel(LabelExpr le,
                                   int count)
If the given label is a trace label, add the count number to the given label expression's label name, so that trace labels will sort correctly.


fresh

private VariableAccess fresh(VarInit e,
                             int loc)
Generate a temporary for the result of a given expression.

This partially implements ESCJ 23b, case 6.


fresh

private VariableAccess fresh(VarInit e,
                             int loc,
                             java.lang.String suffix)

temporary

private VariableAccess temporary(java.lang.String s,
                                 int locAccess)
Generate a temporary variable with prefix s and associated expression location information locAccess.


temporary

private VariableAccess temporary(java.lang.String s,
                                 int locAccess,
                                 int locIdDecl)

mapLocation

public static Expr mapLocation(Expr e,
                               int loc)

addMoreLocations

public void addMoreLocations(java.util.Set s)

setop

static void setop(ASTNode e)

addNewString

public Expr addNewString(VarInit x,
                         Expr left,
                         Expr right)

cacheValue

public VariableAccess cacheValue(Expr e)

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