Comment by pjmlp
4 days ago
Let's see, they are still a bit of a dream regarding what they wish for, and what current static analysers can achieve, especially the lifetime one.
4 days ago
Let's see, they are still a bit of a dream regarding what they wish for, and what current static analysers can achieve, especially the lifetime one.
I was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.
Yeah, the problem with the lifetimes profile vision, is the lack of acknowledgement of how MSVC and clang-tidy have struggled to achieve the Core Guidelines ideas for lifetimes (since 2015), without additional annotations.
MSVC requires SAL and clang has equally added extensions for type annotations.
The WG21 politics killed the Safe C++ proposal with the P3466 paper,
"(Re)affirm design principles for future C++ evolution"
https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p34...
> Do not add a feature that requires viral annotation
However it is quite clear, that without changing language semantics, for the lifetimes profile to be actually useful, as shown by MSVC and clang experience, we would need to have [[profile:lifetime(something)]] in plenty of places.
Not only would that be more verbose than what Rust and Safe C++ proposal, it would still require placing those annotations on the standard library (yet another complaint from the anti-Safe C++ proposal folks), and naturally violate the paper that was voted for as the design principles for future C++ evolution.
However in regards to how to check for C and C++ lifetime issues, at least if the source code is fully available, I have had some good experience with AI tools doing code review, like CoPilot on Visual Studio.
Maybe that is possible way forward, moreso if the code isn't being fully written by humans.
Regarding C specifically, what about having Frama-C's ACSL as some kind of ISO C annex?
Compilers would just ignore the annex and whoever wants to implement it, can already do this. And I also think ACSL is too complex for what is needed and also not well integrated with the rest of the language.
IIRC Rust's borrow checker analysis is more or less a subset of what SMT solving is capable of. It's "just" a question of tradeoffs made with respect to performance, complexity, precision, etc.
It is a really tiny and trivial subset of what model checkers can do. Model checkers can often prove memory safety of entirely unmodified C code. The problem is that this still runs into complexity problems and does not scale to non-toy programs. But this would also really be very far at the other end of the borrow checker that would require rewriting everything into a very specific form a borrow checker accepts.. IMHO a middle ground with some annotations is realistic and would be far more convenient than a borrow checker when supported by good tooling.
16 replies →