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 TrAnExpr

java.lang.Object
  extended byescjava.translate.TrAnExpr

public class TrAnExpr
extends java.lang.Object

Translates Annotation Expressions to GCExpr.


Field Summary
private static int[][] binary_table
           
static java.util.LinkedList boundStack
           
private static int cSubstReplacements
           
static VariableAccess currentAlloc
           
static VariableAccess currentState
           
static java.util.LinkedList declStack
           
static boolean extraSpecs
           
protected static TrAnExpr inst
           
static int level
           
static int maxLevel
           
private static int newStringCount
          This hashtable keeps track of cautions issued, with respect to using variables in \old pragmas that were not mentioned in modifies pragmas.
protected static Expr specialResultExpr
          This is the full form of function TrSpecExpr described in ESCJ 16.
protected static Expr specialThisExpr
           
static int tempn
           
static Translate translate
           
static java.util.Set trSpecAuxAxiomsNeeded
           
static ExprVec trSpecExprAuxAssumptions
           
static ExprVec trSpecExprAuxConditions
           
static java.util.Map trSpecModelVarsUsed
           
private static int[][] unary_table
           
 
Constructor Summary
TrAnExpr()
           
 
Method Summary
protected static VariableAccess apply(java.util.Hashtable map, VariableAccess va)
           
static void closeForClause()
           
private static Expr createForall(Expr expr, Expr fcall, java.util.ArrayList bounds)
           
private static Expr createFunctionCall(RoutineDecl rd, java.util.ArrayList bounds, java.util.Hashtable sp)
           
static boolean doRewrites()
           
static Expr elemsTypeCorrect(GenericVarDecl edecl)
           
static Expr fieldTypeCorrect(FieldDecl fdecl)
           
static Identifier fullName(RoutineDecl rd, boolean useSuper)
           
static void getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)
           
static Expr getEquivalentAxioms(RepHelper o, java.util.Hashtable sp)
           
static int getGCTagForBinary(BinaryExpr be)
           
static int getGCTagForUnary(UnaryExpr e)
          TBW.
static ExprVec getModelVarAxioms(TypeDecl td, FieldDecl fd, java.util.Hashtable sp)
           
static int getReplacementCount()
          Returns the number of variable substitutions that calls to trSpecExpr have caused.
static Expr getRepresentsAxiom(NamedExprDeclPragma p, java.util.Hashtable sp)
          Translates an individual represents clause into a class-level axiom.
static void initForClause()
           
static void initForClause(boolean b)
           
static void initForRoutine()
           
private static java.util.ArrayList makeBounds(RoutineDecl rd, GenericVarDecl newThis)
           
static VariableAccess makeVarAccess(GenericVarDecl decl, int loc)
           
static Expr quantTypeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
           
static Identifier representsMethodName(java.lang.Object pt)
           
static Expr resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, java.util.Hashtable sp)
           
static VariableAccess stateVar(java.util.Hashtable sp)
           
static Expr targetTypeCorrect(GenericVarDecl vd, java.util.Hashtable wt)
          This method implements the ESCJ 16 function TargetTypeCorrect, except for the init$ case!
(package private) static VariableAccess tempName(int loc, java.lang.String prefix, Type type)
           
static Expr trSpecExpr(Expr e)
          This is the abbreviated form of function TrSpecExpr described in ESCJ 16.
static Expr trSpecExpr(Expr e, Expr thisExpr)
           
static Expr trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
static Expr trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st, Expr thisExpr)
           
 Expr trSpecExprI(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
static TypeExpr trType(Type type)
           
static ExprVec typeAndNonNullAllocCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp, boolean mentionAllocated)
          Returns a vector of conjuncts.
static Expr typeAndNonNullCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp)
           
static Expr typeCorrect(GenericVarDecl vd)
          This method implements the ESCJ 16 function TypeCorrect.
static Expr typeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
           
static Expr typeCorrectAs(GenericVarDecl vd, Type type)
           
static java.util.Hashtable union(java.util.Hashtable h0, java.util.Hashtable h1)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

newStringCount

private static int newStringCount
This hashtable keeps track of cautions issued, with respect to using variables in \old pragmas that were not mentioned in modifies pragmas. The purpose of this hashtable is to prevent issuing duplicate cautions.


translate

public static Translate translate

level

public static int level

maxLevel

public static int maxLevel

extraSpecs

public static boolean extraSpecs

trSpecExprAuxConditions

public static ExprVec trSpecExprAuxConditions

trSpecExprAuxAssumptions

public static ExprVec trSpecExprAuxAssumptions

trSpecModelVarsUsed

public static java.util.Map trSpecModelVarsUsed

trSpecAuxAxiomsNeeded

public static java.util.Set trSpecAuxAxiomsNeeded

tempn

public static int tempn

declStack

public static java.util.LinkedList declStack

currentAlloc

public static VariableAccess currentAlloc

currentState

public static VariableAccess currentState

boundStack

public static java.util.LinkedList boundStack

specialResultExpr

protected static Expr specialResultExpr
This is the full form of function TrSpecExpr described in ESCJ 16. Each of the parameters sp and st is allowed to be null, which is interpreted as the empty map.


specialThisExpr

protected static Expr specialThisExpr

inst

protected static TrAnExpr inst

binary_table

private static final int[][] binary_table

unary_table

private static final int[][] unary_table

cSubstReplacements

private static int cSubstReplacements
Constructor Detail

TrAnExpr

public TrAnExpr()
Method Detail

trSpecExpr

public static Expr trSpecExpr(Expr e)
This is the abbreviated form of function TrSpecExpr described in ESCJ 16. It is a shorthand for the full form in which sp and st are passed in as empty maps.


trSpecExpr

public static Expr trSpecExpr(Expr e,
                              Expr thisExpr)

initForClause

public static void initForClause(boolean b)

initForClause

public static void initForClause()

closeForClause

public static void closeForClause()

initForRoutine

public static void initForRoutine()

doRewrites

public static boolean doRewrites()

trSpecExpr

public static Expr trSpecExpr(Expr e,
                              java.util.Hashtable sp,
                              java.util.Hashtable st,
                              Expr thisExpr)

trSpecExpr

public static Expr trSpecExpr(Expr e,
                              java.util.Hashtable sp,
                              java.util.Hashtable st)

trSpecExprI

public Expr trSpecExprI(Expr e,
                        java.util.Hashtable sp,
                        java.util.Hashtable st)

tempName

static VariableAccess tempName(int loc,
                               java.lang.String prefix,
                               Type type)

union

public static java.util.Hashtable union(java.util.Hashtable h0,
                                        java.util.Hashtable h1)

targetTypeCorrect

public static Expr targetTypeCorrect(GenericVarDecl vd,
                                     java.util.Hashtable wt)
This method implements the ESCJ 16 function TargetTypeCorrect, except for the init$ case!


typeCorrect

public static Expr typeCorrect(GenericVarDecl vd)
This method implements the ESCJ 16 function TypeCorrect.


typeCorrect

public static Expr typeCorrect(GenericVarDecl vd,
                               java.util.Hashtable sp)

quantTypeCorrect

public static Expr quantTypeCorrect(GenericVarDecl vd,
                                    java.util.Hashtable sp)

resultEqualsCall

public static Expr resultEqualsCall(GenericVarDecl vd,
                                    RoutineDecl rd,
                                    java.util.Hashtable sp)

typeCorrectAs

public static Expr typeCorrectAs(GenericVarDecl vd,
                                 Type type)

typeAndNonNullCorrectAs

public static Expr typeAndNonNullCorrectAs(GenericVarDecl vd,
                                           Type type,
                                           SimpleModifierPragma nonNullPragma,
                                           boolean forceNonNull,
                                           java.util.Hashtable sp)

typeAndNonNullAllocCorrectAs

public static ExprVec typeAndNonNullAllocCorrectAs(GenericVarDecl vd,
                                                   Type type,
                                                   SimpleModifierPragma nonNullPragma,
                                                   boolean forceNonNull,
                                                   java.util.Hashtable sp,
                                                   boolean mentionAllocated)
Returns a vector of conjuncts. This vector is "virgin" and can be modified by the caller. It contains at least 2 empty slots, allows clients to append a couple of items without incurring another allocation.


fieldTypeCorrect

public static Expr fieldTypeCorrect(FieldDecl fdecl)

elemsTypeCorrect

public static Expr elemsTypeCorrect(GenericVarDecl edecl)

getGCTagForBinary

public static int getGCTagForBinary(BinaryExpr be)

getGCTagForUnary

public static int getGCTagForUnary(UnaryExpr e)
TBW. Requires e.getTag() in { UNARYSUB, NOT, BITNOT, INC, POSTFIXINC, DEC, POSTFIXDEC }


makeVarAccess

public static VariableAccess makeVarAccess(GenericVarDecl decl,
                                           int loc)

getReplacementCount

public static int getReplacementCount()
Returns the number of variable substitutions that calls to trSpecExpr have caused. To find out how many times a substitution was made, a caller can surround the call to trSpecExpr by two calls to this method and compute the difference.


apply

protected static VariableAccess apply(java.util.Hashtable map,
                                      VariableAccess va)

trType

public static TypeExpr trType(Type type)

getCalledSpecs

public static void getCalledSpecs(RoutineDecl decl,
                                  ObjectDesignator od,
                                  ExprVec ev,
                                  Expr resultVar,
                                  java.util.Hashtable sp,
                                  java.util.Hashtable st)

fullName

public static Identifier fullName(RoutineDecl rd,
                                  boolean useSuper)

getEquivalentAxioms

public static Expr getEquivalentAxioms(RepHelper o,
                                       java.util.Hashtable sp)

makeBounds

private static java.util.ArrayList makeBounds(RoutineDecl rd,
                                              GenericVarDecl newThis)

createFunctionCall

private static Expr createFunctionCall(RoutineDecl rd,
                                       java.util.ArrayList bounds,
                                       java.util.Hashtable sp)

createForall

private static Expr createForall(Expr expr,
                                 Expr fcall,
                                 java.util.ArrayList bounds)

getRepresentsAxiom

public static Expr getRepresentsAxiom(NamedExprDeclPragma p,
                                      java.util.Hashtable sp)
Translates an individual represents clause into a class-level axiom.


representsMethodName

public static Identifier representsMethodName(java.lang.Object pt)

getModelVarAxioms

public static ExprVec getModelVarAxioms(TypeDecl td,
                                        FieldDecl fd,
                                        java.util.Hashtable sp)

stateVar

public static VariableAccess stateVar(java.util.Hashtable sp)

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