[bitc-dev] NOALLOC analysis
naasking at higherlogics.com
Tue Oct 7 10:22:10 CDT 2008
Jonathan S. Shapiro wrote:
> The BitC compiler currently supports a --noalloc flag, which raises an
> error if the unit of compilation being compiled performs allocation.
> This is a useful check, but it can be done in a static analyzer. On the
> other hand, it can also be handled with a form of effect typing.
> Question: is non-allocation sufficiently important enough that it should
> be part of the in-language type system, or is the use-case for it rare
> enough that we should handle it in a static checker?
I can see the usefulness of having it in the language, since it allows
code producers and consumers to state and verify invariants in a more
fine-grained manner than is possible via an external tool. Then again,
this allocate yes/no invariant is pretty coarse-grained, so that will
limit its usefulness.
> As background to this question, it occurred to me this morning that
> effect analysis can be viewed as a degenerate case of control-flow model
I've always thought of it that way: type systems perform dataflow
analysis, effect systems perform control flow analysis.
> and it is already my intention to add a push-down model
> checking framework to BitC. Those properties would be checked by the
> checker rather than the compiler, but they would be checkable in
> whole-program form.
> bitc-dev mailing list
> bitc-dev at coyotos.org
More information about the bitc-dev