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 }