4 ms·
> Start at leaf functions and walk your way back up the program until you're done. If you run into a situation where there is an ambiguity, you throw an error a
by SkiFire13 2y ago
> Start at leaf functions and walk your way back up the program until you're done. If you run into a situation where there is an ambiguity, you throw an error and let the developer know.
This assumes no recursive functions, no virtual functions/function pointers, no external functions etc etc
> Heck, we just got 'auto' type inference working in C++11, shouldn't we be able to do this too?
Aliasing is much trickier than type inference.
For example aliasing can change over time (i.e. some variables may alias at some point but not at a later point, while types are always the same) and you want any analysis to reflect it because you will likely rely on that.
Granularity is also much more important: does a pointer alias with every element of a vector or only one? The former is surely easier to represent, but it may unnecessary propagate and result in errors.
So effectively you have an infinite domain of places that can alias, while type inference is limited to locals, parameters, functions, etc etc. And even then, aliasing is quadratic, because you want to know which pairs of places alias.
I hope you can see how this can quickly get impractical, both due to the complexity of the analysis and the fact that small imprecisions can result in very big false positives.
- thadt 2y agoHence the term 'deceptively'. Even if a sufficiently advanced proof assistant could internally maintain and propagate constraints up through functions (eg. 'vec must not alias x'), your point about small imprecisions cascading into large false positives is well made. Bottom up constraints become increasingly difficult to untangle the further away they get from their inception, whereas top down rules such as "no mutable aliasing" are much easier to reason about locally.