runtime1.abs

notation syntax rsyntax rels runtime ;
import syntax rsyntax wf runtime0 rsubst ;

reserve C for :id;
reserve id for :id;
reserve addr for :int;
reserve val for :rval;
reserve TE for :tyenv;
reserve heap for :heap;
reserve frames for :frames;
reserve s for :frames × heap;
reserve p for :cprog;
// stmt stmt_reduce stmt
// stmt !stmt_reduce []

// exp exp_reduce exp
// exp !--> RValue... | RVoid

// var var_reduce var
// var !var_reduce RStackVar... | RField... | RAccess...

lfp ground_until 
A  
      exp_ground(h) = T & ground_until(t)(m)
   // --------------------------------------
            ground_until(h×t)(m+1)

B 
             exp_ground(h) = F
  // ---------------------------------------
            ground_until(h×t)(0)



// these will be needed for the liveness result
//
//thm ground_until-EL
//   ground_until(l)(n) & n < LEN(l) --> ~exp_ground(EL(n)(l));

//thm ground_until-cases
//   (?k. k < LEN(exps) & ground_until(exps)(k)) |
//    (!j. j < LEN(exps) --> exp_ground(EL(j)(exps)));


lfp reduce 


//VARIABLES
FieldPartial 
                (e,s) exp_reduce(TE,p) (e',s')
     // ----------------------------------------------------------
                (RField(e,C,f),s) var_reduce(TE,p) 
                 (RField(e',C,f),s')


// Derefencing only occurs in expressions
FieldDeref 
                s = (frames,heap) &
                 FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C')) &
                 PLOOKUP(fldvals)(C,f) = SOME(fldval)
     // ----------------------------------------------------------
                (RVar(RField(RValue(RAddr(SOME(addr))),C,f)),s) exp_reduce(TE,p) 
                 (RValue(fldval),s)

FieldBadPtr 
     // ----------------------------------------------------------
                (RVar(RField(RValue(RAddr(NONE)),C,f)),s) exp_reduce(TE,p) 
                 (RValue(RExn(NullPointExc)),s)

// Array Access expressions. Lookup only occurs in expressions.

AccessPartialA 
                (arr0,s0) exp_reduce(TE,p) (arr1,s1)
     // ----------------------------------------------------------
                (RAccess(arr0,idx0),s0) var_reduce(TE,p) 
                 (RAccess(arr1,idx0),s1)

AccessPartialB 
                exp_ground(arr) = T & (idx0,s0) exp_reduce(TE,p) (idx1,s1)
     // ----------------------------------------------------------
                (RAccess(arr,idx0),s0) var_reduce(TE,p) 
                 (RAccess(arr,idx1),s1)


AccessArrayBadPtr 
     // ----------------------------------------------------------
            (RVar(RAccess(RValue(RAddr(NONE)),RValue(RPrim(Int(k32))))),s) exp_reduce(TE,p) 
             (RValue(RExn(NullPointExc)),s)

AccessArrayNegIndex 
            dest_int32(k32) << 0 = T
     // ----------------------------------------------------------
            (RVar(RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32))))),s) exp_reduce(TE,p) 
             (RValue(RExn(IndOutBndExc)),s)

AccessArrayOutOfBounds 
            dest_int32(k32) >>= 0 = T &
             s = (frames,heap) &
             FPLOOKUP(heap)(addr) = SOME(ARRAY(varty,vec)) &
             n = int_to_nat(dest_int32(k32)) &
             n >= LEN(vec)
     // ----------------------------------------------------------
            (RVar(RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32))))),s) exp_reduce(TE,p) 
             (RValue(RExn(IndOutBndExc)),s)

AccessArrayOK 
            dest_int32(k32) >>= 0 = T &
             n = int_to_nat(dest_int32(k32)) &
             s = (frames,heap) &
             FPLOOKUP(heap)(addr) = SOME(ARRAY(varty,vec)) &
             n < LEN(vec)
     // ----------------------------------------------------------
            (RVar(RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32))))),s) exp_reduce(TE,p) 
             (RValue(EL(n)(vec)),s)



//EXPRESSIONS


// evaluate an identifier.
StackVar 
            s = (frames,heap) &
             sGetStackVar(frames,fidx,id) = SOME(val)
     // -----------------------------------------------------------
            (RVar(RStackVar(fidx,id)),s) exp_reduce(TE,p) 
             (RValue(val),s)

// reduce a variable used as an expression.
VarPartial 
                (v,s) var_reduce(TE,p) (v',s')
     // -----------------------------------------------------------
                (RVar(v),s) exp_reduce(TE,p) 
                 (RVar(v'),s')




// allocate an object on the heap
NewClass  
            s = (frames,heap) &
             fldvals = initial o_p flds &
             sAlloc(heap,OBJECT(fldvals,C)) = (heap',addr) & 
             (frames,heap') = s'
     // ----------------------------------------------------------
            (RNewClass(C,flds),s) exp_reduce(TE,p) 
             (RValue(RAddr(SOME(addr))),s')

NewArrayPartial 
       LEN(dims) = n &
        ground_until(dims)(argn) &
        argn < n &
        (EL(argn)(dims),s) exp_reduce(TE,p) (dim',s') &
        dims' = REPLACE(argn)(dims)(dim')
  // -------------------------------------------------------------
       (RNewArray(st,dims,ext),s) exp_reduce(TE,p)
        (RNewArray(st,dims',ext),s')

NewArray 
       ndims = LEN(dims) &
        (!j. j < ndims --> exp_ground(EL(j)(dims)) = T) &
        LEN(dimns) = ndims &
        (!j. j < ndims --> 
         ?i32. EL(j)(dims) = RValue(RPrim(Int(i32))) &
         dest_int32(i32) >>= 0 = T & 
         int_to_nat(dest_int32(i32)) = EL(j)(dimns)) &
        s = (frames,heap) &
        val_alloc(heap,st,dimns,ext) = (val,heap') &
        (frames,heap') = s'
  // -------------------------------------------------------------
       (RNewArray(st,dims,ext),s) exp_reduce(TE,p)
        (RValue(val),s')

NewArrayBadSize 
       ndims = LEN(dims) &
        (!j. j < ndims --> exp_ground(EL(j)(dims)) = T) &
        baddim < ndims &
        EL(baddim)(dims) = RValue(RPrim(Int(badi32))) &
        dest_int32(badi32) << 0 = T
  // -------------------------------------------------------------
       (RNewArray(st,dims,ext),s) exp_reduce(TE,p)
        (RValue(RExn(BadSizeExc)),s)

// reduce the object being called
// bug found: e being returned instead of e'
MethodCallPartialA 
                (e,s) exp_reduce(TE,p) (e',s')
     // ----------------------------------------------------------
                (RCall(e,AT,C,args),s) exp_reduce(TE,p) 
                 (RCall(e',AT,C,args),s')

// reduce one of the arguments
MethodCallPartialB 
       exp_ground(e) = T &
        LEN(args) = n &
        ground_until(args)(argn) &
        argn < n &
        (EL(argn)(args),s) exp_reduce(TE,p) (arg',s') &
        REPLACE(argn)(args)(arg') = args'
  // -------------------------------------------------------------
       (RCall(e,AT,C,args),s) exp_reduce(TE,p)
        (RCall(e,AT,C,args'),s')


// exceptions occur when calling a null object
MethodCallBadPtr 
       LEN(args) = n &
        (!j. j < n --> exp_ground(EL(j)(args)) = T)
     // ----------------------------------------------------------
                (RCall(RValue(RAddr(NONE)),AT,m,args),s) exp_reduce(TE,p)
                 (RValue(RExn(NullPointExc)),s)

// call the method.
// Nb. C' (the class in which the method actually resides) is ignored.
//
// Frame allocation is needed here.  We zip up the argument names and the
// argument values into a table, and add the this pointer.  Gross.
//
MethodCall 
      // Nb. Turn args into values
       nargs = LEN(args) &
        (!j. j < nargs --> exp_ground(EL(j)(args)) = T) &
        LEN(argvals) = nargs &
        (!j. j < nargs --> EL(j)(args) = RValue(EL(j)(argvals))) &
        s = (frames,heap) &
        FPLOOKUP(heap)(addr) = SOME(heapobj) &
        MethBody(m,AT,hoType(heapobj),p)(Xord,body) &
        rbody = mk_rbody (sNextFrame(frames)) body &
        gframe =  { (x,z) | ?j. j < LEN(Xord) & x = EL(j)(Xord) & z = EL(j)(argvals) } &
        frames' = sAddFrame(frames0,PGRAPH gframe <+ (this, RAddr(SOME(addr)))) &
        (frames',heap) = s'
  // -------------------------------------------------------------
       (RCall(RValue(RAddr(SOME(addr))),AT,m,args),s) exp_reduce(TE,p)
        (RBody(rbody),s')


// reduce the body of a method call.
BodyPartialA  
                 (stmt,s) stmt_reduce(TE,p) (stmt',s')
     // -----------------------------------------------------------
                (RBody(stmt,rexp),s) exp_reduce(TE,p) (RBody(stmt',rexp),s')

// reduce the return expression of a method call.
BodyPartialB  
                stmt_ground(stmt) = T
     // -----------------------------------------------------------
                (RBody(stmt,rexp),s) exp_reduce(TE,p) (rexp,s)

// BLOCKS 

BlockPartialA 
        (stmt,s) stmt_reduce(TE,p) (stmt',s')
// --------------------------------------------------------------------------
       (RBlock(stmt×stmts),s) stmt_reduce(TE,p) 
        (RBlock(stmt'×stmts),s')

BlockPartialB 
         stmt_ground(stmt) = T
// --------------------------------------------------------------------------
       (RBlock(stmt×stmts),s) stmt_reduce(TE,p) 
        (RBlock(stmts),s)

// STATEMENTS

IfPartial         
               (e,s) exp_reduce(TE,p) (e',s')
     // -----------------------------------------------------------
               (RIf(e,stmt1,stmt2),s) stmt_reduce(TE,p) 
                (RIf(e',stmt1,stmt2),s')

If 
        
     // ------------------------------------------------------------
       (RIf(RValue(RPrim(Bool(b))),stmt1,stmt2),s) stmt_reduce(TE,p) 
        ((if b then stmt1 else stmt2),s)

ExprPartialA  
        (e,s) exp_reduce(TE,p) (e',s')
    // ----------------------------------------------
       (RExpr(e),s) stmt_reduce(TE,p) 
        (RExpr(e'),s')



// ASSIGNMENT



AssignPartialA 
             (v,s) var_reduce(TE,p) (v',s')
      // ---------------------------------------------------------
                (RAssign(v,e),s) stmt_reduce(TE,p) 
                 (RAssign(v',e),s')

AssignPartialB 
            var_ground(v) = T & (e,s) exp_reduce(TE,p) (e',s')
      // ----------------------------------------------------------
                (RAssign(v,e),s) stmt_reduce(TE,p) 
                 (RAssign(v,e'),s')

AssignStackVar  
                 val_ground(val) = T &
                  s = (frames,heap) &
                  sSetStackVar(frames,fidx,id,val) = frames' &
                  (frames',heap) = s'
     // ----------------------------------------------------------
                (RAssign(RStackVar(fidx,id),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RVoid),s')

AssignFieldBadPtr  
                 val_ground(val) = T
     // ----------------------------------------------------------
                (RAssign(RField(RValue(RAddr(NONE)),C,fld),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RValue(RExn(NullPointExc))),s)

AssignField  
                 val_ground(val) = T &
                  s = (frames,heap) &
                  sFieldSet(heap,addr,C,fld,val) = heap' &
                  (frames,heap') = s'
     // ----------------------------------------------------------
                (RAssign(RField(RValue(RAddr(SOME(addr))),C,fld),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RVoid),s')

AssignArrayBadPtr  
                 exp_ground(exp) = T & 
                  val_ground(val) = T
     // ----------------------------------------------------------
                (RAssign(RAccess(RValue(RAddr(NONE)),exp),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RValue(RExn(NullPointExc))),s)

AssignArrayNegIndex  // 
                 val_ground(val) = T & 
                  dest_int32(k32) << 0 = T
     // ----------------------------------------------------------
                (RAssign(RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32)))),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RValue(RExn(IndOutBndExc))),s)

AssignArrayBadIndex // 
            val_ground(val) = T & 
             dest_int32(k32) >>= 0 = T &
             idx = int_to_nat(dest_int32(k32)) &
             s = (frames,heap) &
             FPLOOKUP(heap)(addr) = SOME(ARRAY(vt,vec)) &
             idx >= LEN(vec) = T
     // ----------------------------------------------------------
                (RAssign(RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32)))),RValue(val)),s) stmt_reduce(TE,p) 
                 (RExpr(RValue(RExn(IndOutBndExc))),s)

// The next two rules are the only place G is needed, and then only the 
// subclass/widening relationship.
//
// bug found using compilation to ML: undeclared variable (typo)
AssignArrayBadType  // 
                 val_ground(sval) = T & 
                  dest_int32(k32) >>= 0 = T &
                  idx = int_to_nat(dest_int32(k32)) &
                  FPLOOKUP(heap)(taddr) = SOME(ARRAY(tvt,svec)) &
                  idx < LEN(svec) &
                  s = (frames,heap) &
                  typecheck((TE,heap),sval,tvt) = F
     // ----------------------------------------------------------
                (RAssign(RAccess(RValue(RAddr(SOME(taddr))),
                                  RValue(RPrim(Int(k32)))),
                          RValue(sval)),s) stmt_reduce(TE,p) 
                 (RExpr(RValue(RExn(ArrStoreExc))),s)


//
// bug found using compilation to ML: undeclared variable (typo)
AssignArray  
                 val_ground(sval) = T & 
                  dest_int32(k32) >>= 0 = T &
                  idx = int_to_nat(dest_int32(k32)) &
                  s = (frames,heap) &
                  FPLOOKUP(heap)(taddr) = SOME(ARRAY(tvt,svec)) &
                  idx < LEN(svec) &
                  typecheck((TE,heap),sval,tvt) = T &
                  heap' = heap <++ (taddr,ARRAY(tvt,REPLACE(idx)(svec)(sval))) &
                  (frames,heap') = s'
     // ----------------------------------------------------------
                (RAssign(RAccess(RValue(RAddr(SOME(taddr))),
                                  RValue(RPrim(Int(k32)))),
                          RValue(sval)),s) stmt_reduce(TE,p) 
                 (RExpr(RVoid),s')