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 GetSpec

java.lang.Object
  extended byescjava.translate.GetSpec

public final class GetSpec
extends java.lang.Object

Responsible for getting Spec for calls. Includes ... from ESCJ16c.


Field Summary
private static java.util.HashSet collectInvariantsAxsToAdd
          Collects the invariants in scope.
private static ASTDecoration dmdDecoration
           
private static ASTDecoration nonnullDecoration
          * Decorates GenericVarDecl's to point to * NonNullPragmas (SimpleModifierPragma's).
 
Constructor Summary
GetSpec()
           
 
Method Summary
private static void addAssumptions(ExprVec ev, StackVector code)
          Appends code with an assume C command for every condition C in cv.
static void addAxioms(java.util.Set axsToAdd, ExprVec assumptions)
          axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper.
static ConditionVec addConstraintClauses(ConditionVec post, TypeDecl decl, java.util.Hashtable wt, ExprVec postAssumptions)
           
private static void addFreeTypeCorrectAs(GenericVarDecl vd, Type type, ConditionVec cv)
          Adds to cv a condition stating that vd has type type.
private static void addInvariantBody(InvariantInfo ii, Spec spec, Set synTargs)
          Extend spec, in a way appropriate for checking the body of a method or constructor, to account for invariant ii.J declared in class ii.U.
private static void addModifiersToDMD(DerivedMethodDecl dmd, RoutineDecl rd)
          * Add the modifiers of rd to dmd, making any necessary substitions * of parameter names.
private static ExprVec addNewAxs(java.util.HashSet axsToAdd, ExprVec assumptions)
           
private static void addSuperInterfaces(TypeDecl td, Set set)
           
private static void assumeConditions(ConditionVec cv, StackVector code)
           
private static void checkConditions(ConditionVec cv, int loc, StackVector code)
          Appends code with an check loc: C command for every condition C in cv.
private static void checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)
           
private static ExprVec collectAxioms(FindContributors scope)
          Collects the axioms in scope.
static void collectFields(Expr e, java.util.Set s)
           
private static InvariantInfo collectInvariants(FindContributors scope, java.util.Hashtable premap)
           
private static ParamAndGlobalVarInfo collectParamsAndGlobals(Spec spec, FindContributors scope)
          Collects the parameters of spec.args and the static fields in scope, whose types are class types.
(package private) static VariableAccess createVarVariant(GenericVarDecl vd, java.lang.String postfix)
          * Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ ". * * This handles ESCJ 23b case 13.
private static CondExprModifierPragma doSubst(java.util.Hashtable subst, CondExprModifierPragma emp)
          Perform a substitution on a CondExprModifierPragma *
private static ExprModifierPragma doSubst(java.util.Hashtable subst, ExprModifierPragma emp)
          Perform a substitution on an ExprModifierPragma *
private static VarExprModifierPragma doSubst(java.util.Hashtable subst, VarExprModifierPragma vemp)
          Perform a substitution on a VarExprModifierPragma *
private static boolean exprIsVisible(TypeSig originType, Expr e)
           
private static Spec extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)
          Implements ExtendSpecForBody, section 7.4 of ESCJ 16.
private static Spec extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)
          Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
private static ExprModifierPragmaVec filterExprModPragmas(ExprModifierPragmaVec vec, FindContributors scope)
           
static DerivedMethodDecl filterMethodDecl(DerivedMethodDecl dmd, FindContributors scope)
           
private static ModifiesGroupPragmaVec filterModifies(ModifiesGroupPragmaVec mvec, FindContributors scope)
           
private static VarExprModifierPragmaVec filterVarExprModPragmas(VarExprModifierPragmaVec vec, FindContributors scope)
           
static DerivedMethodDecl getCombinedMethodDecl(RoutineDecl rd)
          * Implement GetCombinedMethodDecl from ESCJ 16c section 7: * * Precondition: the type declaring rd has been typechecked.
private static Spec getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)
           
static java.util.Enumeration getFirstInheritedInterfaces(ClassDecl cd)
           
static TypeDeclElemVec getRepresentsClauses(TypeDecl td, FieldDecl fd)
          Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td.
static Spec getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)
           
static Spec getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)
           
static Spec getSpecForInline(RoutineDecl rd, FindContributors scope)
           
(package private) static java.util.Hashtable makeSubst(java.util.Enumeration e, java.lang.String postfix)
          Converts a GenericVarDecl enumeration to a mapping from those variables to new Variableaccesses.
(package private) static java.util.Hashtable makeSubst(FormalParaDeclVec args, java.lang.String postfix)
           
private static InvariantInfo mergeInvariants(InvariantInfo ii)
           
private static void nonNullInitChecks(TypeDecl td, ConditionVec post)
          Add to post all NonNullInit checks for non_null instance fields and instance ghost fields declared in td.
static SimpleModifierPragma NonNullPragma(GenericVarDecl v)
          * Has a particular declaration been declared non_null?
(package private) static java.util.Hashtable restrict(java.util.Hashtable map, java.util.Enumeration e)
          Creates and returns a new map that is map restricted to the domain e.
private static void setNonNullPragma(GenericVarDecl v, SimpleModifierPragma nonnull)
          * Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.)
private static VariableAccess shave(Expr e)
          Shaves a GC designator.
static SimpleModifierPragma superNonNullPragma(GenericVarDecl v)
          Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method.
static GuardedCmd surroundBodyBySpec(GuardedCmd body, Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int locEndCurlyBrace)
          Returns a command that first does an assume for each precondition in spec, then does body, then checks the postconditions of spec, and finally checks the modifies constraints implied by spec.
private static Spec trMethodDecl(DerivedMethodDecl dmd, java.util.Hashtable premap)
          Translates a MethodDecl to a Spec.
private static ConditionVec trMethodDeclPostcondition(DerivedMethodDecl dmd, java.util.Hashtable wt, ExprVec postAssumptions)
          Computes the postconditions, according to section 7.2.2 of ESCJ 16.
private static ConditionVec trMethodDeclPreconditions(DerivedMethodDecl dmd, ExprVec preAssumptions)
          Computes the preconditions, according to section 7.2.0 of ESCJ 16.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

dmdDecoration

private static ASTDecoration dmdDecoration

collectInvariantsAxsToAdd

private static java.util.HashSet collectInvariantsAxsToAdd
Collects the invariants in scope.


nonnullDecoration

private static ASTDecoration nonnullDecoration
* Decorates GenericVarDecl's to point to * NonNullPragmas (SimpleModifierPragma's).

Constructor Detail

GetSpec

public GetSpec()
Method Detail

getSpecForCall

public static Spec getSpecForCall(RoutineDecl rd,
                                  FindContributors scope,
                                  Set predictedSynTargs)

getSpecForInline

public static Spec getSpecForInline(RoutineDecl rd,
                                    FindContributors scope)

getSpecForBody

public static Spec getSpecForBody(RoutineDecl rd,
                                  FindContributors scope,
                                  Set synTargs,
                                  java.util.Hashtable premap)

getCommonSpec

private static Spec getCommonSpec(RoutineDecl rd,
                                  FindContributors scope,
                                  java.util.Hashtable premap)

getCombinedMethodDecl

public static DerivedMethodDecl getCombinedMethodDecl(RoutineDecl rd)
* Implement GetCombinedMethodDecl from ESCJ 16c section 7:

* * Precondition: the type declaring rd has been typechecked.

* * Note: this routine may typecheck the supertypes of the type that * declares rd.


addModifiersToDMD

private static void addModifiersToDMD(DerivedMethodDecl dmd,
                                      RoutineDecl rd)
* Add the modifiers of rd to dmd, making any necessary substitions * of parameter names. Also propagates non_null's.

* * Precondition: rd has been typechecked.


doSubst

private static ExprModifierPragma doSubst(java.util.Hashtable subst,
                                          ExprModifierPragma emp)
Perform a substitution on an ExprModifierPragma *


doSubst

private static CondExprModifierPragma doSubst(java.util.Hashtable subst,
                                              CondExprModifierPragma emp)
Perform a substitution on a CondExprModifierPragma *


doSubst

private static VarExprModifierPragma doSubst(java.util.Hashtable subst,
                                             VarExprModifierPragma vemp)
Perform a substitution on a VarExprModifierPragma *


filterMethodDecl

public static DerivedMethodDecl filterMethodDecl(DerivedMethodDecl dmd,
                                                 FindContributors scope)

filterExprModPragmas

private static ExprModifierPragmaVec filterExprModPragmas(ExprModifierPragmaVec vec,
                                                          FindContributors scope)

filterModifies

private static ModifiesGroupPragmaVec filterModifies(ModifiesGroupPragmaVec mvec,
                                                     FindContributors scope)

filterVarExprModPragmas

private static VarExprModifierPragmaVec filterVarExprModPragmas(VarExprModifierPragmaVec vec,
                                                                FindContributors scope)

trMethodDecl

private static Spec trMethodDecl(DerivedMethodDecl dmd,
                                 java.util.Hashtable premap)
Translates a MethodDecl to a Spec.


trMethodDeclPreconditions

private static ConditionVec trMethodDeclPreconditions(DerivedMethodDecl dmd,
                                                      ExprVec preAssumptions)
Computes the preconditions, according to section 7.2.0 of ESCJ 16.


trMethodDeclPostcondition

private static ConditionVec trMethodDeclPostcondition(DerivedMethodDecl dmd,
                                                      java.util.Hashtable wt,
                                                      ExprVec postAssumptions)
Computes the postconditions, according to section 7.2.2 of ESCJ 16.


addAxioms

public static void addAxioms(java.util.Set axsToAdd,
                             ExprVec assumptions)
axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper.


addConstraintClauses

public static ConditionVec addConstraintClauses(ConditionVec post,
                                                TypeDecl decl,
                                                java.util.Hashtable wt,
                                                ExprVec postAssumptions)

extendSpecForCall

private static Spec extendSpecForCall(Spec spec,
                                      FindContributors scope,
                                      Set predictedSynTargs)
Implements ExtendSpecForCall, section 7.3 of ESCJ 16.


extendSpecForBody

private static Spec extendSpecForBody(Spec spec,
                                      FindContributors scope,
                                      Set synTargs)
Implements ExtendSpecForBody, section 7.4 of ESCJ 16.


nonNullInitChecks

private static void nonNullInitChecks(TypeDecl td,
                                      ConditionVec post)
Add to post all NonNullInit checks for non_null instance fields and instance ghost fields declared in td.


getFirstInheritedInterfaces

public static java.util.Enumeration getFirstInheritedInterfaces(ClassDecl cd)

addSuperInterfaces

private static void addSuperInterfaces(TypeDecl td,
                                       Set set)

addInvariantBody

private static void addInvariantBody(InvariantInfo ii,
                                     Spec spec,
                                     Set synTargs)
Extend spec, in a way appropriate for checking the body of a method or constructor, to account for invariant ii.J declared in class ii.U. The body to be checked has syntactic targets synTargs.


collectAxioms

private static ExprVec collectAxioms(FindContributors scope)
Collects the axioms in scope.


getRepresentsClauses

public static TypeDeclElemVec getRepresentsClauses(TypeDecl td,
                                                   FieldDecl fd)
Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td. If td is null, then all represents clauses are returned, in any loaded class.


collectInvariants

private static InvariantInfo collectInvariants(FindContributors scope,
                                               java.util.Hashtable premap)

collectParamsAndGlobals

private static ParamAndGlobalVarInfo collectParamsAndGlobals(Spec spec,
                                                             FindContributors scope)
Collects the parameters of spec.args and the static fields in scope, whose types are class types.


addNewAxs

private static ExprVec addNewAxs(java.util.HashSet axsToAdd,
                                 ExprVec assumptions)

shave

private static VariableAccess shave(Expr e)
Shaves a GC designator.


restrict

static java.util.Hashtable restrict(java.util.Hashtable map,
                                    java.util.Enumeration e)
Creates and returns a new map that is map restricted to the domain e. Assumes that every element in e is in the domain of map.


makeSubst

static java.util.Hashtable makeSubst(java.util.Enumeration e,
                                     java.lang.String postfix)
Converts a GenericVarDecl enumeration to a mapping from those variables to new Variableaccesses.


makeSubst

static java.util.Hashtable makeSubst(FormalParaDeclVec args,
                                     java.lang.String postfix)

createVarVariant

static VariableAccess createVarVariant(GenericVarDecl vd,
                                       java.lang.String postfix)
* Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ ". * * This handles ESCJ 23b case 13.


addFreeTypeCorrectAs

private static void addFreeTypeCorrectAs(GenericVarDecl vd,
                                         Type type,
                                         ConditionVec cv)
Adds to cv a condition stating that vd has type type.


surroundBodyBySpec

public static GuardedCmd surroundBodyBySpec(GuardedCmd body,
                                            Spec spec,
                                            FindContributors scope,
                                            Set syntargets,
                                            java.util.Hashtable premap,
                                            int locEndCurlyBrace)
Returns a command that first does an assume for each precondition in spec, then does body, then checks the postconditions of spec, and finally checks the modifies constraints implied by spec.


addAssumptions

private static void addAssumptions(ExprVec ev,
                                   StackVector code)
Appends code with an assume C command for every condition C in cv.


assumeConditions

private static void assumeConditions(ConditionVec cv,
                                     StackVector code)

checkConditions

private static void checkConditions(ConditionVec cv,
                                    int loc,
                                    StackVector code)
Appends code with an check loc: C command for every condition C in cv.


checkModifiesConstraints

private static void checkModifiesConstraints(Spec spec,
                                             FindContributors scope,
                                             Set syntargets,
                                             java.util.Hashtable premap,
                                             int loc,
                                             StackVector code)

mergeInvariants

private static InvariantInfo mergeInvariants(InvariantInfo ii)

exprIsVisible

private static boolean exprIsVisible(TypeSig originType,
                                     Expr e)

collectFields

public static void collectFields(Expr e,
                                 java.util.Set s)

setNonNullPragma

private static void setNonNullPragma(GenericVarDecl v,
                                     SimpleModifierPragma nonnull)
* Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.)


NonNullPragma

public static SimpleModifierPragma NonNullPragma(GenericVarDecl v)
* Has a particular declaration been declared non_null? If so, * return the non_null pragma responsible. Otherwise, return null.

* * Precondition: if the declaration is a formal parameter, then the * spec of it's routine has already been computed.

* * * WARNING: this is the only authorized way to determine this * information. Do *not* attempt to search for NON_NULL modifiers * directly. (This is needed to handle inherited NON_NULL's * properly.)


superNonNullPragma

public static SimpleModifierPragma superNonNullPragma(GenericVarDecl v)
Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method.


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