Comment by uecker
3 days ago
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.
The paper explicitly says that if you use an LLM it is prompted function-by-function.
For the SAT solver I think classification can be done function-by-function if you manually drive the solver in the single-function mode, but I think you're more right in that the whole-program mode doesn't actually do that.
I think my misunderstanding stemmed from interpreting the start of section 5.4 and figure 3 as showing that constraint generation occurred strictly before the verifier was invoked and glossing over the bit at the start of section 6 that said that the process basically works the other way around when using the solver to build the p-model.
2 replies →