[bitc-dev] Mutability inference in BitC vs const inference in CQUAL
swaroop at cs.jhu.edu
Thu Sep 14 20:16:06 CDT 2006
This note talks about a difference between the way mutability/const
inference works in BitC and CQual. 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, 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.
Jeffrey S. Foster, Manuel Faehndrich, and Alexander Aiken. ``A theory
of type qualifiers.'' In Proceedings of PLDI 1999.
 Design of Type and Mutability Inference in BitC
More information about the bitc-dev