4 ms·

Yes, it returned the same "FAILURE" along with a couple new checks about getc that do pass.

WalterBright 3y ago
Sounds like it's doing a solid job of data flow analysis. But I can still produce cases where it cannot determine either the range of the index or the length of the array being pointed to. The programmer will have to add code to keep track of the length of the array, and add code to check the value of the index. The good thing is the analyzer will tell you where you'll need to add those checks. With the proposal I made, none of this is necessary. It just works. Over two decades of experience with this approach in D is it-just-works.
- nanolith 3y ago
  I'm curious, have you used CBMC? The machine model tracks the array with its size and compares this to any index. This is loaded into an SMT solver. This is not a standard static analyzer. It's compiling the code to an abstract machine model and then running through this model with an SMT solver. CBMC isn't perfect, but the strategies you are talking about are meant to defeat a linter or a shallow analyzer in a compiler. CBMC isn't a linter.
  - WalterBright 3y ago
    I have never heard of CBMC before this thread. SMT cannot solve cases where it simply cannot know what the length of an array is. For example, when array is allocated in code not available to the solver, or is set by the environment. I remember trying out Spark a few years ago, which advertised its compile time checking abilities. I tried using an integer equation that used an OR, and it gave up on it. If you need to add in range checking code to help the solver along, then the range check itself is a source of bugs, and the range limit has to be made available somewhere and be correct. In my proposal, the array length is set at the time of creation of the array, and the length is carried along with the pointer. The solver's role then becomes one of eliminating the bounds check in the cases where it can prove the index is within range. The user doesn't have to do anything. We've been using it in the implementation of the D compiler for a very long time now, and problems with buffer overflows are a faded memory. P.S. I also added manual integer overflow checks when passing the size to malloc(), no matter how unlikely an overflow would be :-)
    - nanolith 3y ago
      > SMT cannot solve cases where it simply cannot know what the length of an array is. Sure it can. It sets the array length to a non-deterministic unsigned integer, and then finds a counter-example where this array length is invalid. CBMC will also make the array pointer itself non-deterministic if you haven't refined it. So, the pointer could be NULL, could be pointing to invalid memory, etc. Don't think of values as fixed numbers, but rather as functions shaping a non-deterministic value. The range check made upstream becomes part of this function. The goal of the SMT solver is to find a counter-example that crashes the machine model. If you want a rather leaky abstraction, imagine that by transforming the source code into an SMT equation, it's effectively turning it inside out and transforming it into a logic equation with modulo math. I agree with you that it would be nice if bounds were included in C arrays. But, we have to work with what we have. Unfortunately, especially in firmware that requires a commercial C compiler, we are stuck with C. In those cases, if we want safer software, we need tooling like this.
      - WalterBright 3y ago
        Thank you for the explanation. I agree that if one isn't going to enhance C, one is going to have to resort to these tools. C gets new features now and then. Why not add something incredibly useful, like the slice proposal? Instead, C23 got enhanced with the crazy Unicode identifiers. Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!! https://github.com/dlang/dmd/pull/15307 https://github.com/dlang/dmd/pull/15307 The entire C parser is 6000 lines of code: https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cparse.d https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
        nanolith 3y ago
        Yeah... I'm not too happy with some of the choices made in C18 and C23. One of the reasons why I chose to standardize my C SAX-like parser on C18 for now was to avoid the Unicode complexity. There's also a widening feature gap between modern C and modern C++ that makes interop harder.
        3y ago

Sounds like it's doing a solid job of data flow analysis. But I can still produce cases where it cannot determine either the range of the index or the length of the array being pointed to. The programmer will have to add code to keep track of the length of the array, and add code to check the value of the index. The good thing is the analyzer will tell you where you'll need to add those checks. With the proposal I made, none of this is necessary. It just works. Over two decades of experience with this approach in D is it-just-works.

nanolith 3y ago
I'm curious, have you used CBMC? The machine model tracks the array with its size and compares this to any index. This is loaded into an SMT solver. This is not a standard static analyzer. It's compiling the code to an abstract machine model and then running through this model with an SMT solver. CBMC isn't perfect, but the strategies you are talking about are meant to defeat a linter or a shallow analyzer in a compiler. CBMC isn't a linter.
- WalterBright 3y ago
  I have never heard of CBMC before this thread. SMT cannot solve cases where it simply cannot know what the length of an array is. For example, when array is allocated in code not available to the solver, or is set by the environment. I remember trying out Spark a few years ago, which advertised its compile time checking abilities. I tried using an integer equation that used an OR, and it gave up on it. If you need to add in range checking code to help the solver along, then the range check itself is a source of bugs, and the range limit has to be made available somewhere and be correct. In my proposal, the array length is set at the time of creation of the array, and the length is carried along with the pointer. The solver's role then becomes one of eliminating the bounds check in the cases where it can prove the index is within range. The user doesn't have to do anything. We've been using it in the implementation of the D compiler for a very long time now, and problems with buffer overflows are a faded memory. P.S. I also added manual integer overflow checks when passing the size to malloc(), no matter how unlikely an overflow would be :-)
  - nanolith 3y ago
    > SMT cannot solve cases where it simply cannot know what the length of an array is. Sure it can. It sets the array length to a non-deterministic unsigned integer, and then finds a counter-example where this array length is invalid. CBMC will also make the array pointer itself non-deterministic if you haven't refined it. So, the pointer could be NULL, could be pointing to invalid memory, etc. Don't think of values as fixed numbers, but rather as functions shaping a non-deterministic value. The range check made upstream becomes part of this function. The goal of the SMT solver is to find a counter-example that crashes the machine model. If you want a rather leaky abstraction, imagine that by transforming the source code into an SMT equation, it's effectively turning it inside out and transforming it into a logic equation with modulo math. I agree with you that it would be nice if bounds were included in C arrays. But, we have to work with what we have. Unfortunately, especially in firmware that requires a commercial C compiler, we are stuck with C. In those cases, if we want safer software, we need tooling like this.
    - WalterBright 3y ago
      Thank you for the explanation. I agree that if one isn't going to enhance C, one is going to have to resort to these tools. C gets new features now and then. Why not add something incredibly useful, like the slice proposal? Instead, C23 got enhanced with the crazy Unicode identifiers. Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!! https://github.com/dlang/dmd/pull/15307 https://github.com/dlang/dmd/pull/15307 The entire C parser is 6000 lines of code: https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cparse.d https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
      - nanolith 3y ago
        Yeah... I'm not too happy with some of the choices made in C18 and C23. One of the reasons why I chose to standardize my C SAX-like parser on C18 for now was to avoid the Unicode complexity. There's also a widening feature gap between modern C and modern C++ that makes interop harder.
      - 3y ago