Hacker News Reader

Comment by aw1621107 | Hacker News Reader

> The problem is that this still runs into complexity problems and does not scale to non-toy programs.

Right; that is why Rust's borrow checker was designed to be intraprocedural only. That obviously is a tradeoff of its own: now functions need to be annotated to convey information across function boundaries, and the annotations picked will influence what can and cannot be expressed.

> IMHO a middle ground with some annotations is realistic and would be far more convenient than a borrow checker when supported by good tooling.

I'd be interested in seeing what such a middle ground looks like, particularly in respect to what tradeoffs it makes!

View on HN

I don't know yet. My current expectation from what I have seen is that lifetime analysis can be done fully automatic for most C code as long as it can be done independently from other program state, i.e. the checker has to reason only about the state of pointers and not also simultaneously about all other variables. I have seen quite promising work on this.

> lifetime analysis can be done fully automatic for most C code as long as it can be done independently from other program state

Is this an interprocedural or intraprocedural analysis?

> I have seen quite promising work on this.

Is this work public? I'm interested in seeing more!

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.

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.

Perhaps the LLM can infer enough context from one function.

Possibly? Though given its outputs apparently aren't completely out there I'd hazard a guess that the inferred context usually shouldn't be too far off of what can be deduced using more traditional methods.

Reply on news.ycombinator.com