    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.translate;
    004
    005
    006    import java.util.Hashtable;
    007    import java.util.Enumeration;
    008
    009    import javafe.ast.*;
    010    import javafe.tc.TypeSig;
    011    import javafe.util.Location;
    012
    013    import escjava.ast.GhostDeclPragma;
    014    import escjava.ast.TagConstants;
    015    import escjava.ast.NaryExpr;
    016
    017    import escjava.backpred.FindContributors;
    018
    019
    020    /**
    021     ** This class provides two methods used in the generation of a
    022     ** verification condition for a method or constructor (see section 8
    023     ** of ESCJ 16). <p>
    024     **/
    025
    026    public final class InitialState {
    027      private /*@ non_null @*/ Hashtable premap;
    028      private /*@ non_null @*/ Expr is;
    029
    030      public InitialState(/*@ non_null @*/ FindContributors scope) {
    031        premap = new Hashtable();
    032        ExprVec conjuncts = ExprVec.make();
    033
    034        // static fields and instance variables
    035        Enumeration fields = scope.fields();
    036        while (fields.hasMoreElements()) {
    037              FieldDecl fd = (FieldDecl)fields.nextElement();
    038
    039              VariableAccess va = TrAnExpr.makeVarAccess(fd, Location.NULL);
    040              VariableAccess variant = addMapping(fd);
    041
    042              // g@pre == g    and    f@pre == f
    043              conjuncts.addElement(GC.nary(TagConstants.ANYEQ, variant, va));
    044              Expr typeCorrect;
    045              if (Modifiers.isStatic(fd.modifiers)) {
    046                // TypeCorrect[[ g ]]
    047                typeCorrect = TrAnExpr.typeCorrect(fd);
    048              } else {
    049                // FieldTypeCorrect[[ f ]]
    050                typeCorrect = TrAnExpr.fieldTypeCorrect(fd);
    051              }
    052              conjuncts.addElement(typeCorrect);
    053        }
    054
    055            /* The preFields Set accumulates every location that occurs inside a \old()
    056               construct.  These are the mappings needed to map variable uses that occur
    057               in expressions back to a token representing the pre-state value.
    058               This should be all that is needed (though it is overkill for any one method),
    059               and we should not need the set added above (which are those locations that
    060               appear in modifies clauses), but we keep those for good measure (to avoid
    061               introducing bugs because some kind of access does not make it into a proper
    062               representation in the loop below).
    063               By using all the \old() locations we (a) make the verification of method bodies
    064               robust against errors in the modifies clauses and (b) allow the implementation
    065               of modifies \everything.
    066            */
    067        fields = scope.preFields.elements();
    068        while (fields.hasMoreElements()) {
    069              FieldDecl fd = ((FieldAccess)fields.nextElement()).decl;
    070              if (premap.get(fd) != null) continue;
    071
    072              VariableAccess va = TrAnExpr.makeVarAccess(fd, Location.NULL);
    073              VariableAccess variant = addMapping(fd);
    074
    075              // g@pre == g    and    f@pre == f
    076              conjuncts.addElement(GC.nary(TagConstants.ANYEQ, variant, va));
    077              Expr typeCorrect;
    078              if (Modifiers.isStatic(fd.modifiers)) {
    079                // TypeCorrect[[ g ]]
    080                typeCorrect = TrAnExpr.typeCorrect(fd);
    081              } else {
    082                // FieldTypeCorrect[[ f ]]
    083                typeCorrect = TrAnExpr.fieldTypeCorrect(fd);
    084              }
    085              conjuncts.addElement(typeCorrect);
    086        }
    087
    088        // elems@pre == elems
    089        conjuncts.addElement(GC.nary(TagConstants.ANYEQ,
    090                                     addMapping(GC.elemsvar.decl), GC.elemsvar));
    091        // ElemsTypeCorrect[[ elems ]]
    092        conjuncts.addElement(TrAnExpr.elemsTypeCorrect(GC.elemsvar.decl));
    093
    094        // LS == asLockSet(LS)
    095        conjuncts.addElement(GC.nary(TagConstants.ANYEQ, GC.LSvar,
    096                                     GC.nary(TagConstants.ASLOCKSET, GC.LSvar)));
    097
    098        // alloc@pre == alloc
    099        conjuncts.addElement(GC.nary(TagConstants.ANYEQ,
    100                                     addMapping(GC.allocvar.decl), GC.allocvar));
    101
    102        // state@pre == state
    103        conjuncts.addElement(GC.nary(TagConstants.ANYEQ,
    104                                     addMapping(GC.statevar.decl), GC.statevar));
    105
    106        // conjoin the conjuncts
    107        is = GC.and(conjuncts);
    108      }
    109
    110      private VariableAccess addMapping(GenericVarDecl vd) {
    111        VariableAccess variant = GetSpec.createVarVariant(vd, "pre");
    112        premap.put(vd, variant);
    113        return variant;
    114      }
    115
    116      public /*@ non_null @*/ Hashtable getPreMap() {
    117        return premap;
    118      }
    119
    120      public /*@ non_null @*/ Expr getInitialState() {
    121        return is;
    122      }
    123    }