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    }