[bitc-dev] NOALLOC analysis
bitc-dev at lists.lorens.org
Wed Oct 8 03:02:11 CDT 2008
On Tue, Oct 07, 2008 at 01:43:22PM -0400, Swaroop Sridhar wrote:
> It is possible to add a switch to the compiler so that it will not
> perform some of the effect checking (ex: alloc/noalloc), or make some
> conservative default assumptions for the lack of programmer annotation.
> However, code that must work in either mode (ex: libraries) must be
> written in a fully annotated form.
Does the C++ concept "const" have a meaning in BitC? The
problem seems to be much the same.
Looking at the problem from *way* above, I'd just like to make
quite sure I understand the use for noalloc. Is it to make sure
that calling some code will not create a memory leak? A kind of
confinement at the function level (like const...)? It's not just
to avoid memory consumption, since an infinite recursive will
consume all the memory you like without any dynamic allocation,
As I see it, either you have source or you don't. If you have
the source, you could place a constraint once, when you need
it, and ask the compiler to check all the called code.
If you don't have the source, but compiled code that you trust,
then you should have the constraint reflected somewhere in
the description, much like const is integrated in the type
In any case I'd have expected to find "don't allocate any memory
at all" as a special case of a list containing "don't leave more
than X bytes allocated after function exit", "do not use more
than X bytes of memory", "do not make any library calls that
could change system state", "do not change the memory pointed
to by any pointers I might have passed to you", "return in
less than x time". Basically, sandbox the function. Of course
most of these are much harder to analyze at compile-time than
"don't call the memory allocation function", but at the same
time they're the ones I would want when calling code I hadn't
analyzed myself in detail. I imagine that would be part of the
"push-down model checking framework"?
More information about the bitc-dev