[bitc-dev] Mutability inference in BitC vs const inference in CQUAL

[Swaroop Sridhar]

Dr. Foster:

This note talks about a difference between the way mutability/const 
inference works in BitC and CQual[1]. I would appreciate if you can 
confirm/correct my understanding regarding this issue.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

[ I am ignoring the issues of inference due to let-polymorphism in BitC 
in this note. ]

In C, it is legal to write:

int *x = dup_int(10); /* malloc+initialize */
const int* y = x;
*x = 25;

That is, the const-ness of the location pointed to by y is only with 
respect to the pointer y, and is not a (global) property of that location.

However, in BitC, it is not legal to write:

(let ((x:(ref (mutable int)) (dup 10)))
   (let ((y:(ref int) x))  ;; ERROR !!
      (set! (deref y) 200)))

Mutability in BitC is not an attribute of a type, but an attribute of a 
location. We enforce a one-location-one-type rule across all aliases and 
any compatibility in mutability of two types happens only because of a 
copy operation (which uses a new location).

In this respect, the sub-typing relationship (written <=)

t <= const t holds in C, but

(mutable t) <= t does not hold in BitC.

CQUAL's const inference enforces the t <= const rule, which works fine 
for C programs. But, in order to enforce the copy (only) compatibility 
rule in BitC, we need maybe-mutable types[2], so that we can write:

(maybe t) <= t
(maybe t) <= (mutable t)

I think this relationship is sound because maybe types are only created 
  when a copy-operation is performed.

[1]Jeffrey S. Foster, Manuel Faehndrich, and Alexander Aiken. ``A theory 
of type qualifiers.'' In Proceedings of PLDI 1999.
www.cs.umd.edu/~jfoster/papers/pldi99.pdf

[2] Design of Type and Mutability Inference in BitC
http://www.coyotos.org/docs/bitc/mutinfer.html

Swaroop.