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 Translate

    java.lang.Object
      escjava.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:
  - 0. fOld = F;
  - 1. check 0 <= fOld;
  - 2. check F < fOld;

### 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)

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