3 ms·

> 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 inte

> 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.
- lifthrasiir 3y ago
  > Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!! I wondered if you were implementing a normalization (which is complicated), but that doesn't seem the case? I have read the PR and it's clear that it solves multiple issues at once: no start-continue distinction (bug), a code generator, the table itself (which is just an inefficiently formatted block of data). 6000 lines of code just for Unicode identifiers are simply an exaggeration.
  - WalterBright 3y ago
    There are different ways to count lines. I included in the C parser count the comment lines. 6000 is also a round number, I did that deliberately to imply the number was not exact.
    - lifthrasiir 3y ago
      A new generated code alone is 4000 lines long [1]. The actual code added is just 2000 lines, and some are used to pay debts, I mean, to make a proper code generator. It is debatable whether that generator should count in the number of lines, since you can always write a generator in a simpler scripting language (for example, Rust uses Python to generate the `unicode-xid` crate). In any case however it is far less complex and, in my opinion, much smaller than the entire C parser proper. [1] https://github.com/dlang/dmd/pull/15307/files#diff-3677bcc896b4eacdde46b6df9ddfd0be58e388de66016b53d2f4fcbc5cefab84 https://github.com/dlang/dmd/pull/15307/files#diff-3677bcc89...
  - mhh__ 3y ago
    Most big PRs are only big because pull requests are a fundamentally bad model for doing work that's already been planned.
- rurban 3y ago
  > C23 got enhanced with the crazy Unicode identifiers. Actually, this spec security bug was added with C11. But nobody really added it, until gcc decided that this new "feature" needs to be supported around C23 time. C23 tried to mitigate that mess by disallowing non-identifiable normalization variants, but still does not care about Unicode security guidelines.

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.
lifthrasiir 3y ago
> Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!! I wondered if you were implementing a normalization (which is complicated), but that doesn't seem the case? I have read the PR and it's clear that it solves multiple issues at once: no start-continue distinction (bug), a code generator, the table itself (which is just an inefficiently formatted block of data). 6000 lines of code just for Unicode identifiers are simply an exaggeration.
- WalterBright 3y ago
  There are different ways to count lines. I included in the C parser count the comment lines. 6000 is also a round number, I did that deliberately to imply the number was not exact.
  - lifthrasiir 3y ago
    A new generated code alone is 4000 lines long [1]. The actual code added is just 2000 lines, and some are used to pay debts, I mean, to make a proper code generator. It is debatable whether that generator should count in the number of lines, since you can always write a generator in a simpler scripting language (for example, Rust uses Python to generate the `unicode-xid` crate). In any case however it is far less complex and, in my opinion, much smaller than the entire C parser proper. [1] https://github.com/dlang/dmd/pull/15307/files#diff-3677bcc896b4eacdde46b6df9ddfd0be58e388de66016b53d2f4fcbc5cefab84 https://github.com/dlang/dmd/pull/15307/files#diff-3677bcc89...
- mhh__ 3y ago
  Most big PRs are only big because pull requests are a fundamentally bad model for doing work that's already been planned.
rurban 3y ago
> C23 got enhanced with the crazy Unicode identifiers. Actually, this spec security bug was added with C11. But nobody really added it, until gcc decided that this new "feature" needs to be supported around C23 time. C23 tried to mitigate that mess by disallowing non-identifiable normalization variants, but still does not care about Unicode security guidelines.