[bitc-dev] NOALLOC analysis

[Sandro Magi]

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
> checking,

I've always thought of it that way: type systems perform dataflow
analysis, effect systems perform control flow analysis.

Sandro

> 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.
> 
> 
> shap
> 
> _______________________________________________
> bitc-dev mailing list
> bitc-dev at coyotos.org
> http://www.coyotos.org/mailman/listinfo/bitc-dev