Comment by aw1621107
4 days ago
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.
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.
The classification can not be done on the function level. There are two ways, either this is done using AI or using a SAT solver.
3 replies →