rstatics1.absnotation syntax rsyntax rels rstatics runtime ; import syntax rsyntax wf runtime0 statics1 ; // statics1 needed for prim_hastype. reserve TE for :tyenv; reserve FT for :ftyenv; reserve heap for :heap; reserve C for :id; reserve id for :id; reserve varty for :varType; reserve expty for :varType option; reserve stmts for :rstmt list; // FT is the typing for local variables on the stack, organised into frames. reserve FT for :(id,varType)pfun list; def wf_ftyenv "TE |- FT wf_ftyenv <=> !fidx. fidx < LEN(FT) --> !id vt. id :: PDOM(EL(fidx)(FT)) & PLOOKUP(EL(fidx)(FT))(id) = SOME(vt) --> TE |- vt wf_vartype // RULES FOR VALUES // // These rules are very similar to those for weak conformance, though // without any subtyping allowed (i.e. the types allowed are not // closed up to widening). // // Lemma4_1 states the correlation between these sets of rules. // // Null pointer values can type to any array, class or interface. // // These means we can't assign unique types to runtime expressions, // but that's OK. Note we can for the subset that corresponds to // compiled programs. // // Theorem: Addresses never type to primitive values. // // BUG: Null pointers should be allowed to type to // interfaces at runtime after all. It is necessary for the // conformance theorem (Lemma4_1). e.g. a null pointer stored // in a identifier with type interface - the result // of reducing the identifier is a null pointer with type // interface (though it may later be used in some narrower sense). lfp rval_hastype NullToClass // ----------------------------------------------------------------- (TE,heap) |- RAddr(NONE) rval_hastype VT(Class(C),0) NullToArray 0 < dim // ----------------------------------------------------------------- (TE,heap) |- RAddr(NONE) rval_hastype VT(simpty,dim) NullToInterface // ----------------------------------------------------------------- (TE,heap) |- RAddr(NONE) rval_hastype VT(Interface(i),0) AddrToClass FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C)) // ----------------------------------------------------------------- (TE,heap) |- RAddr(SOME(addr)) rval_hastype VT(Class(C),0) AddrToArray FPLOOKUP(heap)(addr) = SOME(ARRAY(VT(simpty,dim),vec)) & ndim = dim+1 // ----------------------------------------------------------------------------- (TE,heap) |- RAddr(SOME(addr)) rval_hastype VT(simpty,ndim) // Primitive values Prim p prim_hastype pt // ---------------------------------------- (TE,heap) |- RPrim(p) rval_hastype VT(PrimT(pt),0) // Rules for expressions, statements, variables // Rationale for these rules: // // The old rules were a bit overloaded - they served to type // both compiled programs (that had RId's) and runtime // expression (that had RStackVar's). The G component // was really two things: the class typing etc. (needed for // both activities), and the local variable typing (needed for // typing RIds. The FT (frame typing) is needed only // for typing RStackVars. // // For various resons these relations are non-executable, e.g. we // cannot guess the return type of the body of an expression // (it changes during execution, and maybe indeterminate, e.g. if // the return value has been reduced to null). lfp rstatics // RULES FOR VARIABLES StackVar fidx < LEN(FT) & EL(fidx)(FT) = FS & PLOOKUP(FS)(x) = SOME(varty) // ----------------------------------------------- (TE,FT,heap) |- RStackVar(fidx,x) rvar_hastype varty Access (TE,FT,heap) |- exp1 rexp_hastype SOME(VT(simpty,dim)) & 0 < dim & (TE,FT,heap) |- exp2 rexp_hastype SOME(VT(PrimT(intT),0)) & ndim = dim-1 // ---------------------------------------------------- (TE,FT,heap) |- RAccess(exp1,exp2) rvar_hastype VT(simpty,ndim) // We don't re-disambiguate the field lookup. This could get the // wrong field if e has widened to a subclass with an intervening // declaration of the field! // // nb. non-executable because we can't guess C (it may be indeterminate). // // The first two lines could be: // (TE,FT,heap) |- e rexp_hastype vt & // TE |- vt varty_widens_to VT(Class(C'),0) // but it seems better to avoid awkward reasoning about the case // C' = Object. // // Note e must type to a class - it cannot type to an interface because // interfaces can't have fields (is this true in full Java?) Field (TE,FT,heap) |- obj rexp_hastype SOME(VT(Class(C),0)) & ((C',f),vt) :: FDecs(TE,C) // ---------------------------------------------------- (TE,FT,heap) |- RField(obj,C',f) rvar_hastype vt Value (TE,heap) |- v rval_hastype vt // ----------------------------------------------------------------------------- (TE,FT,heap) |- RValue(v) rexp_hastype SOME(vt) Var (TE,FT,heap) |- var rvar_hastype varty // ------------------------------------------------------ (TE,FT,heap) |- RVar(var) rexp_hastype SOME(varty) Void // ----------------------------------------- (TE,FT,heap) |- RVoid rexp_hastype NONE // Creating things on the heap. // // The NewClass rule must check that the field specifiers are the correct // graph of FDecs. NewClass (!fld vt. (fld,vt) :: FDecs(TE,C) --> TE |- vt wf_vartype) & flds = PGRAPH {fspec | FDecs(TE,C)(fspec)} // ----------------------------------------------------------------- (TE,FT,heap) |- RNewClass(C,flds) rexp_hastype SOME(VT(Class(C),0)) NewArray dim = LEN(dims)+ext & 0 < dim & TE |- st wf_simptype & (!j. j < LEN(dims) --> (TE,FT,heap) |- EL(j)(dims) rexp_hastype SOME(VT(PrimT(intT),0))) // --------------------------------------------------------------------- (TE,FT,heap) |- RNewArray(st,dims,ext) rexp_hastype SOME(VT(st,dim)) // Typing method calls in runtime expressions. // // Do we need to re-disambiguate the method reference? // This would seem to be almost harmful if we don't take AT into // account, e.g. // // e1.F(e2) // where statically e1:C0, e2: B0, B1 < B0, C1 < C0. // If at runtime e1 narrows to C1 and e0 B1 then disambiguation // might find a completely different best method in C1. // // However, we know AT, and we can just use this as the basis for // looking up the method table in the runtime class of e. // // Note that as reduction of e1 and e2 continues, the return // type can change (by narrowing) because a different method // gets selected. This is dynamic dispatch at its best! // // MSigsC can find at most one return type for a given AT, and will // be guranteed to find one for originally well-typed programs. // Call LEN(args) = nargs & LEN(AT) = nargs & (TE,FT,heap) |- e rexp_hastype SOME(vt) & MSigs(TE,vt)(m,MT(AT,rt)) & (!j. j < nargs --> ?varty. (TE,FT,heap) |- EL(j)(args) rexp_hastype SOME(varty) & TE |- varty varty_widens_to EL(j)(AT)) // ---------------------------------------------------- (TE,FT,heap) |- RCall(e,AT,m,args) rexp_hastype rt Body (TE,FT,heap) |- stmt rstmt_hastype & (TE,FT,heap) |- rexp rexp_hastype expty // --------------------------------------------------------------- (TE,FT,heap) |- RBody(stmt,rexp) rexp_hastype expty // In the runtime model, bad assignments to arrays are allowed. This is // because they are checked at runtime. // // Direct assignments to adresses are not allowed - this would require additional // runtime typechecking. AssignToStackVar (TE,FT,heap) |- e rexp_hastype SOME(varty') & (TE,FT,heap) |- RStackVar(fidx,id) rvar_hastype varty & TE |- varty' varty_widens_to varty // ----------------------------------------------- (TE,FT,heap) |- RAssign(RStackVar(fidx,id),e) rstmt_hastype AssignToField (TE,FT,heap) |- e rexp_hastype SOME(varty') & (TE,FT,heap) |- RField(e1,C,f) rvar_hastype varty & TE |- varty' varty_widens_to varty // ----------------------------------------------- (TE,FT,heap) |- RAssign(RField(e1,C,f),e) rstmt_hastype AssignToArray (TE,FT,heap) |- e rexp_hastype ety & (TE,FT,heap) |- RAccess(e1,e2) rvar_hastype varty // ----------------------------------------------------------------- (TE,FT,heap) |- RAssign(RAccess(e1,e2),e) rstmt_hastype If (TE,FT,heap) |- stmt1 rstmt_hastype & (TE,FT,heap) |- stmt2 rstmt_hastype & (TE,FT,heap) |- e rexp_hastype SOME(VT(PrimT(boolT),0)) // ------------------------------------------------------------------ (TE,FT,heap) |- RIf(e,stmt1,stmt2) rstmt_hastype Expr (TE,FT,heap) |- e rexp_hastype vto // ---------------------------------------- (TE,FT,heap) |- RExpr(e) rstmt_hastype Block !j. j < LEN(stmts) --> (TE,FT,heap) |- EL(j)(stmts) rstmt_hastype // ---------------------------------------------------------------------- (TE,FT,heap) |- RBlock(stmts) rstmt_hastype |