3 ms·

> The whole point is that with some additional code changes (especially around pointer usage) one WOULD detect errors at compile-time. The point isn't just det

> The whole point is that with some additional code changes (especially around pointer usage) one WOULD detect errors at compile-time. The point isn't just detecting errors, but rather completely disallowing code that does unsafe things, by turning every undefined behavior into a compilation error. Unfortunately, determining whether a C++ program has undefined behavior is equivalent to solving the Halting problem.

comex 10y ago
> Unfortunately, determining whether a C++ program has undefined behavior is equivalent to solving the Halting problem. The Core Guidelines analyzers do not try to accept all valid C++ programs, or even a large percentage of real-world C++ programs. In principle they will accept a subset (+ annotations), a language within a language, designed to make it possible to statically verify memory safety, similar to Rust.
- catnaroek 10y ago
  > The Core Guidelines analyzers do not try to accept all valid C++ programs I'm aware. My point is: Are the Core Guidelines enough to completely rule out memory errors? This is essentially a type safety claim, and thus requires (possibly informal) proof.
  - coldtea 10y ago
    >Are the Core Guidelines enough to completely rule out memory errors? Does it matter? As long as they rule out the vast majority of memory errors, e.g. many times more than static analysis tools find today.
    - catnaroek 10y ago
      Static analysis tools for C and C++ have a horrible track record at this. I wouldn't use them as benchmark.
      - the_why_of_y 10y ago
        My experience is the same: static analysis tools like Coverity, PVS-Studio, etc. find just a small fraction of memory safety errors, mostly the ones that can be found by just looking at a single function with not overly complex control flow.
Animats 10y ago
"Unfortunately, determining whether a C++ program has undefined behavior is equivalent to solving the Halting problem." Sigh. You can write undecidable programs, but you don't want to. This issue has been neatly addressed by the Windows Static Driver Verifier. If it can't decide if a driver is memory-safe and API safe in some number of minutes, it quits, and Microsoft won't sign the driver. About 5% of drivers hit this problem, and need some rewriting. If your kernel driver is anywhere near undecidability in memory safety, it's broken.
- catnaroek 10y ago
  > Sigh. You can write undecidable programs, but you don't want to. What does “undecidable program” even mean? The label “undecidable” applies to decision problems: https://en.wikipedia.org/wiki/Decision_problem https://en.wikipedia.org/wiki/Decision_problem > If it can't decide if a driver is memory-safe and API safe in some number of minutes, it quits, and Microsoft won't sign the driver. About 5% of drivers hit this problem, and need some rewriting. We're talking about the universe of C++ programs that meet the Core Guidelines, not just drivers.
  - coldtea 10y ago
    >What does “undecidable program” even mean? It's pretty clear what it means in this context, especially after the Halting problem was mentioned earlier in the thread, and the parent wrote about MS driver verification program "deciding whether a driver is memory-safe".
    - catnaroek 10y ago
      > It's pretty clear what it means in this context Sorry, no. Imprecise use of jargon is one of the main ways how technical discussions get derailed. So I shall insist on precise use of terminology.
      - coldtea 10y ago
        >Imprecise use of jargon is one of the main ways how technical discussions get derailed. Yes. And the other main way is insistence on pointless pedantic distinctions.

comex 10y ago

> Unfortunately, determining whether a C++ program has undefined behavior is equivalent to solving the Halting problem. The Core Guidelines analyzers do not try to accept all valid C++ programs, or even a large percentage of real-world C++ programs. In principle they will accept a subset (+ annotations), a language within a language, designed to make it possible to statically verify memory safety, similar to Rust.

catnaroek 10y ago
> The Core Guidelines analyzers do not try to accept all valid C++ programs I'm aware. My point is: Are the Core Guidelines enough to completely rule out memory errors? This is essentially a type safety claim, and thus requires (possibly informal) proof.
- coldtea 10y ago
  >Are the Core Guidelines enough to completely rule out memory errors? Does it matter? As long as they rule out the vast majority of memory errors, e.g. many times more than static analysis tools find today.
  - catnaroek 10y ago
    Static analysis tools for C and C++ have a horrible track record at this. I wouldn't use them as benchmark.
    - the_why_of_y 10y ago
      My experience is the same: static analysis tools like Coverity, PVS-Studio, etc. find just a small fraction of memory safety errors, mostly the ones that can be found by just looking at a single function with not overly complex control flow.

Animats 10y ago

"Unfortunately, determining whether a C++ program has undefined behavior is equivalent to solving the Halting problem." Sigh. You can write undecidable programs, but you don't want to. This issue has been neatly addressed by the Windows Static Driver Verifier. If it can't decide if a driver is memory-safe and API safe in some number of minutes, it quits, and Microsoft won't sign the driver. About 5% of drivers hit this problem, and need some rewriting. If your kernel driver is anywhere near undecidability in memory safety, it's broken.

catnaroek 10y ago
> Sigh. You can write undecidable programs, but you don't want to. What does “undecidable program” even mean? The label “undecidable” applies to decision problems: https://en.wikipedia.org/wiki/Decision_problem https://en.wikipedia.org/wiki/Decision_problem > If it can't decide if a driver is memory-safe and API safe in some number of minutes, it quits, and Microsoft won't sign the driver. About 5% of drivers hit this problem, and need some rewriting. We're talking about the universe of C++ programs that meet the Core Guidelines, not just drivers.
- coldtea 10y ago
  >What does “undecidable program” even mean? It's pretty clear what it means in this context, especially after the Halting problem was mentioned earlier in the thread, and the parent wrote about MS driver verification program "deciding whether a driver is memory-safe".
  - catnaroek 10y ago
    > It's pretty clear what it means in this context Sorry, no. Imprecise use of jargon is one of the main ways how technical discussions get derailed. So I shall insist on precise use of terminology.
    - coldtea 10y ago
      >Imprecise use of jargon is one of the main ways how technical discussions get derailed. Yes. And the other main way is insistence on pointless pedantic distinctions.