Skip to content

Theory of partial functions.

module partial_function(f,d,r) = {
1) for any x there is at most one y such that f(x,y), 
    axiom ~f(X:d,Y:r) | ~f(X:d,Z:r) | Y:r = Z:r
2) dom[f] is the domain of f, 
    relation dom[f](X:d)
    axiom ~f(X:d,Y:r) | dom[f](X:d)
3) for any x in dom[f], we have f(x,f[x]). 
    schema img[f](x) = ~dom[f](x) | f(x,f[x])
4) This defines how dom[f] updates as we update f: 
     update dom[f] from f
       params v:d,w:r in v.f := w ->
        ensures ((~old dom[f](X:d) | dom[f](X:d)) & dom[f](v))
       params v:d in v.f := null ->
        ensures (~old dom[f](X:d) | X:d = v | dom[f](X:d))
       params v:d,w:d in v.f := w.f ->
         ensures (old dom[f](Y:d) & Y:d ~= v | old dom[f](w) & Y:d = v) ->
                      dom[f](Y:d)
}
Type of abstract heap objects 
type object
Type of machine addresses 
type addr

module hack(f,x,d) = {
    individual f[x] : d
}

instantiate hack(m0,ae1,addr)
instantiate hack(m1,ae1,addr)

relation (X:addr < Y:addr)
relation (X:addr <= Y:addr)
bug 6: forgot to say this: 
axiom ~(X < X)
axiom (X < Y & Y < Z) -> (X < Z)
axiom X <= Y <-> (X < Y | X = Y)
bug 10: forgot to say this: 
axiom X < Y | X = Y | Y < X
boundaries of from and to regions 
individual flo:addr,fhi:addr,tlo:addr,thi:addr
definitions of from and to regions 
derived faddr(X:addr) = flo <= X & X < fhi
derived taddr(X:addr) = tlo <= X & X < thi
from and to regions are disjoint 
axiom ~(faddr(X) & taddr(X))
bug 5: forgot to say from and to regions can't be empty axiom faddr(flo) 
axiom taddr(tlo)

individual temp_addr:addr # TODO: this should be in macro below

macro incr_addr(x) = {
   temp_addr := x;
   x := *;
   assume temp_addr < x;
   assume ~(temp_addr < X & X < x);
   temp_addr := *
}
representation relation between objects and addresses

relation repr(X:object,Y:addr)
instantiate partial_function(repr,object,addr)
the abstract heap

individual hroot:object #root of the abstract heap
each abstract heap cell has two pointer fields

relation h0(X:object,Y:object)
relation h1(X:object,Y:object) 
instantiate partial_function(h0,object,object)
instantiate partial_function(h1,object,object)

the machine memory

individual mroot:addr #address of root in machine memory
each machine memory cell has two pointer fields 
relation m0(X:addr,Y:addr)
relation m1(X:addr,Y:addr) 
instantiate partial_function(m0,addr,addr)
instantiate partial_function(m1,addr,addr)

copied map

relation copied_to(A1:addr,A2:addr)
the representation invariant

macro rep_inv = forall [O1,O2,A1,A2] ( repr(hroot,mroot) & (repr(O1,A1) & h0(O1,O2) -> domm0) & (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) -> repr(O2,A2)) & (repr(O1,A1) & h1(O1,O2) -> domm1) & (repr(O1,A1) & h1(O1,O2) & m1(A1,A2) -> repr(O2,A2)))

init
representation invariant holds initially 
  repr(hroot,mroot)
  & (repr(O1,A1) & h0(O1,O2) -> dom[m0](A1))
  & (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) -> repr(O2,A2))
& (repr(O1,A1) & h1(O1,O2) -> domm1) & (repr(O1,A1) & h1(O1,O2) & m1(A1,A2) -> repr(O2,A2)) bug 7: repr should be an injection 
  & (repr(O1,A1) & repr(O2,A1) -> O1 = O2)
bug 12: other direction of the connection between m0 and h0 
  & (repr(O1,A1) & m0(A1,A2) -> dom[h0](O1))
  & ((repr(O1,A1) & repr(O2, A2)) -> (m0(A1,A2) <-> h0(O1,O2)))
bug 8: initially, repr points only into from region 
  & (repr(O1,A1) -> faddr(A1))

  & faddr(mroot)  # root is in "from" region
"from" region is closed 
  & ~(m0(A1,A2) & faddr(A1) & ~faddr(A2))
& ~(m1(A1,A2) & faddr(A1) & ~faddr(A2)) 
  & ~copied_to(A1,A2)
represenation invarianr

algorithm state variables 

individual tnext:addr,talloc:addr
aux variables: TODO: should be local 
individual oe1:object,oe2:object,ae1:addr,ae2:addr,a:addr,obj:object,a2:addr

macro copy_obj(fr,to) = {
    to.m0 := fr.m0;
to.m1 := fr.m1; 
    fr.copied_to := to;
bug 4: forgot next lines TODO: need this assertion assert rngrepr; 
    obj := *;
    assume repr(obj,fr);
    obj.repr := to;
    instantiate incr_addr(to)
}

macro sweep(field) = {
    a := *;  # TODO: should be a := tnext.field
    a2 := *;
    if (dom[field](tnext)) {
        assume field(tnext,a);
bug 1: had tnext instead of talloc 
        if * {
            assume ~copied_to(a,X);
bug 9: was a.field, should have been tnext.field 
            tnext.field := talloc;
bug 11: forgot next line 
            assume talloc < thi;
            instantiate copy_obj(a,talloc)
        } else {
            assume copied_to(a,a2);
            tnext.field := a2
        }
    }
}

action initialize = {
  talloc := tlo;  # allocation pointer
  tnext := tlo; # next object to sweep
  instantiate copy_obj(mroot,talloc);
bug 3: forgot next line: 
  mroot := tlo
hroot.repr := mroot # ODED: don't think this is needed, as it's done in copy_obj 
}

action step = {
  assume tnext < talloc & talloc < thi;
  instantiate sweep(m0);
instantiate sweep(m1); bug 2: forgot next line 
  instantiate incr_addr(tnext)
}


action error = {
  assume tnext = talloc;
representation invariant does not hold TODO: this should be a macro 
  instantiate img[m0](ae1);
instantiate imgm1; 
  assume ~(
   repr(hroot,mroot)
   & taddr(mroot)
   & (repr(oe1,ae1) & h0(oe1,oe2) & taddr(ae1) -> dom[m0](ae1))
   & (repr(oe1,ae1) & h0(oe1,oe2) & taddr(ae1) & m0(ae1,ae2) -> repr(oe2,ae2) & taddr(ae2))
& (repr(oe1,ae1) & h1(oe1,oe2) & taddr(ae1) -> domm1) & (repr(oe1,ae1) & h1(oe1,oe2) & taddr(ae1) & m1(ae1,ae2) -> repr(oe2,ae2) & taddr(ae2)) 
   & (repr(oe1,ae1) & repr(oe2,ae1) -> oe1 = oe2)
  )
}
bug in forward image? conjecture (repr(O1, A1) & repr(O2, A2) & m0(A1, A2)) -> h0(O1, O2) concept c(O1,O2,A1,A2) = ((repr(O1, A1) + ~repr(O1, A1)) * (repr(O2, A2) + ~repr(O2, A2)) * (m0(A1, A2) + ~m0(A1, A2)) * (h0(O1, O2) + ~h0(O1, O2)))

concept spaces from interpolants

concept itp_a = ~domrepr concept itp_b = ~repr(hroot, mroot) concept itp_d = ~taddr(mroot) concept itp_c = (tnext = talloc) concept itp_e = (talloc = fhi * tnext = fhi * ~repr(hroot, mroot)) concept itp_f = (tnext = talloc * ~repr(hroot, mroot)) concept itp_g = (thi = temp_addr) concept itp_h = (~taddr(talloc) * talloc < thi) concept itp_i = (tnext = talloc * ~taddr(talloc)) concept itp_j = (~taddr(tnext)) concept itp_k(V0) = (~domm1 * h1(hroot, V0)) concept itp_l(V1) = (tnext = talloc * h1(hroot, V1)) concept itp_m(V0, V1, V2) = (~repr(V1, V0) * h1(V2, V1) * m1(V0, V0) * repr(V2, V0) * taddr(V0)) concept itp_n(V0, V1) = (talloc = fhi * tnext = fhi * ~repr(hroot, V0) * h1(V1, hroot) * m1(V0, V0) * repr(V1, V0) * taddr(V0)) concept itp_o(V0, V1) = (~domm0 * tnext < V0 * h0(V1, V1) * repr(V1, V0)) concept itp_p(V1) = (~domm0 * h0(V1, V1) * repr(V1, talloc)) concept itp_q = (tnext < mroot) concept itp_r = (tnext = mroot) concept itp_s(V2) = (talloc < flo * h0(V2, obj) * m0(talloc, talloc) * repr(V2, talloc)) concept itp_t(V3) = (talloc < thi * h0(V3, obj) * m0(thi, talloc) * repr(V3, thi)) concept itp_u(V3) = (talloc < thi * h0(V3, hroot) * m0(thi, talloc) * repr(V3, thi)) concept itp_v(V0, V2) = (thi = flo * V0 < flo * h0(V2, hroot) * m0(V0, V0) * repr(V2, V0)) concept itp_w(V2) = (talloc < flo * h0(V2, hroot) * m0(talloc, talloc) * repr(V2, talloc)) concept itp_x(V3) = (talloc < thi * h0(V3, hroot) * m0(talloc, talloc) * repr(V3, talloc)) concept itp_y(V1, V4, V2) = (V2 < thi * tnext < V2 * h0(V4, hroot) * m0(V1, V2) * repr(V4, V1)) concept itp_z(V2, V0) = (tnext = talloc * h0(V2, hroot) * m0(V0, talloc) * repr(V2, V0)) concept itp_a0 = (tnext < temp_addr) concept itp_b0(V0, V1) = (~domm1 * tnext < V0 * h1(V1, V1) * repr(V1, V0)) concept itp_c0(V0) = (V0 < tnext * taddr(V0)) concept itp_e0(V0, V1, V2) = (V0 < tnext * h0(V1, V2) * repr(V1, V0) * ~domm0) concept itp_e1(V0, V1, V2) = (V0 < tnext * h1(V1, V2) * repr(V1, V0) * ~domm1)

conjecture repr(hroot, mroot)
conjecture taddr(mroot)
conjecture tlo <= tnext & tnext <= talloc
conjecture tnext < thi
conjecture tlo <= talloc & talloc <= thi
conjecture mroot = tlo

conjecture repr(O1, A) & repr(O2, A) -> O1 = O2
conjecture repr(O, A) -> ((faddr(A) & ~copied_to(A, X)) | (tlo <= A & A < talloc))


conjecture (repr(O1,A1) & h0(O1,O2) -> dom[m0](A1))
conjecture V0 = V2 | copied_to(V2, V0) | ~h0(V4, V3) | ~m0(V1, V2) | ~repr(V3, V0) | ~repr(V4, V1) 
conjecture (repr(O1, A1) & h0(O1, O2) & repr(O2, A2) & m0(A1, A3)) -> (A2 = A3 | copied_to(A3, A2))
conjecture (taddr(A1) & m0(A1,A2) & A1 < tnext) -> (taddr(A2) & A2 < talloc)
conjecture (tnext <= A1 & A1 < talloc & m0(A1,A2)) -> faddr(A2)
conjecture (repr(O1, A1) & repr(O2, A2) & m0(A1, A2)) -> h0(O1, O2)
conjecture (faddr(A1) & m0(A1,A2)) -> faddr(A2)
conjecture (repr(O1, A1) & repr(O2, A3) & m0(A1, A2) & copied_to(A2, A3)) -> h0(O1, O2)
the following conjectures may demonstrate a bug in reverse (reversing them results in a refuted goal, but no refinement is possible): conjecture (repr(O1, A1) & repr(O2, A2) & m0(A1, A2)) -> h0(O1, O2) conjecture (taddr(A1) & m0(A1,A2) & tnext <= A1) -> faddr(A2) conjecture (m0(__A1, __new_a) & repr(__O1, __A1) & repr(__new_obj, __new_a) & ~h0(__O1, __new_obj))

conjecture (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) & taddr(A2)) -> repr(O2,A2)
conjecture (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) & copied_to(A2, A3)) -> repr(O2,A3)
conjecture ~(m0(A1,A2) & faddr(A1) & ~faddr(A2))

conjecture copied_to(A1,A2) -> faddr(A1)
conjecture copied_to(A1,A2) -> tlo <= A2

conjecture copied_to(A1,A2) -> A2 < tallocยค

conjecture (copied_to(A,A1) & copied_to(A,A2)) -> A1 = A2
conjecture (copied_to(A1,A) & copied_to(A2,A)) -> A1 = A2
notes: we need some kind of "natural join" instrumentation to say that repr(O1, A1) & h0(O1, O2) & m0(A1, A2) implies that either repr(O2, A2) or A2 is copied to A3 and repr(O2, A3) without this, I don't think there's a universal invariant, since we may lose A3 from above, and then we'll never restore the repr relation

well, actually, it turn's out we can do without it by using strong enought universal clauses, and put all of the existential that we need in the unproved "assert rng[repr]" in copy_obj. But it might stil be a useful idea.