Comment by uecker
3 days ago
It is interprocedural, but one obviously needs annotations for interfaces to libraries that are linked-in.
One example of a project wich goes in this direction is this work: https://www.sei.cmu.edu/projects/ai-powered-memory-safety-fo...
(I assume the AI is mostly marketing as it is not necessary)
Thanks for the link! That's an interesting approach indeed. If I'm reading the paper [0] correctly the concepts involved look pretty similar to what Rust uses. I think they turn the interprocedural analysis into an intraprocedural one as well by effectively deriving borrowing information from function implementations and attaching that to signatures for use by callers. It's a compatibility hazard, which is why Rust chose to not do the same, but in principle it makes it easier to derive more precise borrowing information.
[0]: https://dl.acm.org/doi/epdf/10.1145/3814943.3816182
They globally derive the borrowing information for all pointers in the whole program by classifying the role of each pointer. If there is a way to do this in a way that makes the program safe, this is computed automatically using a SAT solver.
> They globally derive the borrowing information for all pointers in the whole program by classifying the role of each pointer.
Right; by my reading this is done function-by-function by the constraint generator before passing that information to the solver for verification.
4 replies →