runtime0.abs
notation syntax rsyntax rels runtime ; import syntax rsyntax statics1 wf ; reserve C for :id; reserve id for :id; reserve prog for :cprog; reserve mbody for :cmethodbody; reserve stmts for :rstmt list; reserve addr for :int; reserve val for :rval; reserve frames for :frames; reserve heap for :heap; reserve vt for :varType; // -------------------------------------------------------------------------- // MethBodyC - search the program for the method body for a call // to an object. // -------------------------------------------------------------------------- lfp MethBodyC Hit (C,(Csupo,mbodies)) :: ELS(prog) & (m,mbody) :: ELS(mbodies) & mbody = ((Xord,Xtys),body) & MAP(PAPPLY(Xtys))(Xord) = AT // --------------------------------------------------------- MethBodyC(m,AT,C,prog)(Xord,body) Miss (C,(SOME(Csup),mbodies)) :: ELS(prog) & (!Xord Xtys body. (m,((Xord,Xtys),body)) :: ELS(mbodies) --> MAP(PAPPLY(Xtys))(Xord) <> AT) & MethBodyC(m,AT,Csup,prog)(Xord,body) // --------------------------------------------------------- MethBodyC(m,AT,C,prog)(Xord,body) // -------------------------------------------------------------------------- // MethBodyA - get the method body for a call to an array method. // The special method clone() is not // yet supported, so we just return the method body from Object. // -------------------------------------------------------------------------- def MethBodyA MethBodyA(m,AT,vt,prog)(Xord,body) <=> MethBodyC(m,AT,Object,prog)(Xord,body) // -------------------------------------------------------------------------- // MethBody - get the method body for a call to an reference type. // -------------------------------------------------------------------------- def MethBody MethBody(m,AT,VT(st,dim),prog)(Xord,body) <=> MATCH res. ( 0 < dim andalso res = MethBodyA(m,AT,VT(st,dim),prog)(Xord,body)) | (?i. dim = 0 & st = Interface(i) andalso res = F) | (?C. dim = 0 & st = Class(C) andalso res = MethBodyC(m,AT,C,prog)(Xord,body)) | (?p. dim = 0 & st = PrimT(p) andalso res = F)// Heap Objects (things that get stored on the heap) // // The varType stored in the array indicates the type of elements stored in the array, // not the typ of the array itself
datatype OBJECT: ((id × id) -> rval option) × id -> heapobj | ARRAY: (varType×rval list) -> heapobj def hoType hoType(heapobj) = MATCH res. (?fldvals C. heapobj = OBJECT(fldvals,C) andalso res = VT(Class(C),0)) | (?st1 dim vec. heapobj = ARRAY(VT(st1,dim),vec) andalso res = VT(st1,dim+1)); def hoFieldSet hoFieldSet(OBJECT(fldvals,C),C',fld,val) = OBJECT(fldvals <+ ((C',fld),val),C)
// axiomatize a fresh address function
constant freshi :(int)fset -> int thm freshi ~(freshi(s) ::: s)
// Heap //
def sFieldSet sFieldSet(heap,addr,C,fld,val) = heap <++ (addr,hoFieldSet(FPAPPLY(heap)(addr),C,fld,val)) def sAlloc sAlloc(heap,heapobj) = let addr = freshi(FPDOM(heap)) in (heap <++ (addr,heapobj),addr)
// Frames // // Local (stack) variables are allocated in frames. The frames are never deallocated // in the small-step semantics.
def sGetStackVar sGetStackVar(frames,fidx,id) = PLOOKUP(EL(fidx)(frames))(id) def sSetStackVar sSetStackVar(frames,fidx,id,val) = REPLACE(fidx)(frames)(EL(fidx)(frames) <+ (id,val)) def sAddFrame sAddFrame(frames,frame) = frames ×! frame def sNextFrame sNextFrame(frames) = LEN(frames)
// initial values during allocation //
constant initial :varType -> rval thm initial [exec,defn] initial(VT(st,n)) = if (0 < n) then RAddr(NONE) else MATCH res. ( st = PrimT(boolT) andalso res = RPrim(Bool(F))) | ( st = PrimT(charT) andalso res = RPrim(Char(mk_uchar(32)))) | ( st = PrimT(byteT) andalso res = RPrim(Byte(mk_int8(0)))) | ( st = PrimT(shortT) andalso res = RPrim(Short(mk_int16(0)))) | ( st = PrimT(intT) andalso res = RPrim(Int(mk_int32(0)))) | ( st = PrimT(longT) andalso res = RPrim(Long(mk_int64(0)))) | ( st = PrimT(floatT) andalso res = RPrim(Float(mk_ieee32(0)))) | ( st = PrimT(doubleT) andalso res = RPrim(Double(mk_ieee64(0)))) | (?i. st = Interface(i) andalso res = RAddr(NONE)) | (?C. st = Class(C) andalso res = RAddr(NONE))
// A gross procedure to allocate up an array, or indeed any initial value. // We recurse through dimensions, allocating loads of pointers, // totalling dim1 x dim2 x ... dim(n-1), and then dim(n) non-allocated values // for each of these. // // In the base case we drop through to initial which, if ext = 0, // will actually give us a real primitive value, othesimpise will // give us a null pointer. // // artificiality: not tail recursive to give an easier induction - think about this.
constant val_alloc :(heap × simpType × nat list × nat) -> (rval × heap) thm val_alloc val_alloc (heap,st,dims,ext) = MATCH res. (?dim dims'. dims = dim×dims' andalso res = let (vec,heap') = REPEATN dim ([],heap) (LAM(vec,heap). let (val,heap') = val_alloc(heap,st,dims',ext) in (val×vec,heap')) in let (heap'',addr) = sAlloc(heap',ARRAY(VT(st,LEN(dims')+ext),vec)) in (RAddr(SOME(addr)),heap'')) | ( dims = [] andalso res = (initial(VT(st,ext)),heap)) // -------------------------------------------------------------------------- // Define ground expressions, values, variables etc. // What all good expressions aspire to be. // // RVar expressions are not ground even when the variable is. // This is because field/array lookup is resolved at the expression level. // -------------------------------------------------------------------------- def val_ground [exec,defn] val_ground val = MATCH res. (?x1. val = RPrim(x1) andalso res = T) | (?x2. val = RAddr(x2) andalso res = T) | (?x3. val = RExn(x3) andalso res = F) def exp_ground [exec,defn] exp_ground exp = MATCH res. (?val. exp = RValue(val) andalso res = val_ground(val)) | ( exp = RVoid andalso res = T) | (?x5. exp = RVar(x5) andalso res = F) | (?x6. exp = RNewClass(x6) andalso res = F) | (?x7. exp = RNewArray(x7) andalso res = F) | (?x8. exp = RCall(x8) andalso res = F) | (?x9. exp = RBody(x9) andalso res = F) def var_ground [exec,defn] var_ground var = MATCH res. (?fidx id. var = RStackVar(fidx,id) andalso res = T) | (?e1 e2. var = RAccess(e1,e2) andalso res = (exp_ground(e1) andalso exp_ground(e2))) | (?e1 C f. var = RField(e1,C,f) andalso res = exp_ground(e1)) def stmts_ground [exec,defn] stmts_ground(stmts) = NULL(stmts) def stmt_ground [exec,defn] stmt_ground(stmt) = MATCH res. (?e. stmt = RExpr(e) andalso res = exp_ground(e) = T) | (?g b1 b2. stmt = RIf(g,b1,b2) andalso res = F) | (?v1 e1. stmt = RAssign(v1,e1) andalso res = F) | (?stmts. stmt = RBlock(stmts) andalso res = stmts_ground(stmts)) // ------------------------------------------------------------------------- // Runtime type checking. This *is* part of the runtime model, i.e. it must be executable. // bug found be compilation analysis to ML: undeclared variable. // // Modelling error: we should not be able to check conformance of // primitive values at runtime, e.g. in array assignment. The fact // that the primitive value being assigned is well-typed should be enough. // // The old problem here was we are conflating runtime type checking with the // inveriant we need to constrain the state changes by. Should have // v wconforms_to t' iff v : t & t < t' // // Note that we check even in the primitive case, and for null pointers, unlike // any real Java imlementation. It would be possible // not to, but we would need to strengthen the invariant in the case // of array assignments to assert that if the type being assigned into is primitive, // then the assignment is always welltyped. // -------------------------------------------------------------------------- def typecheck typecheck((TE,heap),sval,vt) <=> MATCH res. (?pval. sval = RPrim(pval) andalso res = (?pt. vt = VT(PrimT(pt),0) & pval prim_hastype pt)) | ( sval = RAddr(NONE) andalso res = ((?C. vt = VT(Class(C),0)) | (?i. vt = VT(Class(i),0)) | (?st dim. 0 < dim & vt = VT(st,dim)))) | (?addr fldvals C. sval = RAddr(SOME(addr)) andalso FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C)) andalso res = (TE |- VT(Class(C),0) varty_widens_to vt)) | (?addr st dim vec. sval = RAddr(SOME(addr)) andalso FPLOOKUP(heap)(addr) = SOME(ARRAY(VT(st,dim),vec)) andalso res = (TE |- VT(st,dim+1) varty_widens_to vt))
