4 ms·

Out of interest, where is that quoted sentence from? My understanding is that while this tool aims to catch undefined behavior, it also tries to keep going whe

Out of interest, where is that quoted sentence from? My understanding is that while this tool aims to catch undefined behavior, it also tries to keep going when it encounters implementation-defined behavior. I think you can choose a concrete target platform (CPU/OS/compiler) to model, at least you can do that in Frama-C, which tis-interpreter is based on. So if you specified, say, x86-64 Linux with GCC as your platform, and you happen to be mostly sure that x86-64 GCC on Linux generates code as they expect, then that's fine. It makes no sense to interpret C code independent of a model of a target platform. There is just too much implementation-defined stuff.

MaxBarraclough 9y ago
> Out of interest, where is that quoted sentence from? Oops, I should've replied to modless's comment - it's from this blog post: https://trust-in-soft.com/out-of-bounds-pointers-a-common-pattern-and-how-to-avoid-it/ https://trust-in-soft.com/out-of-bounds-pointers-a-common-pa... > you happen to be mostly sure that x86-64 GCC on Linux generates code as they expect, then that's fine. Being 'mostly sure' isn't good enough; that's the point of rigorous tools like this. If a new GCC optimisation breaks your code because you failed to follow the letter of the law and had UB in your code, that's your fault, not GCC's. > There is just too much implementation-defined stuff. Take that thinking to an extreme and you're barely able to reason rigorously about C code at all. Any number of dangerous constructs might happen to work on a given CPU+compiler. Good C code should be portable. Detecting dangerous, poor quality code is the whole point of tools like tis-interpreter. Things like casting int* to int and back to int* might happen to work on your CPU+compiler, but it should cause warnings.
- tom_mellior 9y ago
  > Take that thinking to an extreme and you're barely able to reason rigorously about C code at all. No reason to take things to the extreme. Is the code int i = 32767; int n = i + i; well-defined? It is implementation-defined whether it is undefined [0], since that depends on the implementation's size for int. You are barely able to reason rigorously about C code without considering some concrete real-world implementation's behavior. (I agree that the uintptr_t thing would merit an optional warning; maybe there is one.) [0] Language lawyers might disagree with this statement and just call it undefined. But if anything, that's even less useful.
  - MaxBarraclough 9y ago
    That's a good example. I see two ways to handle that one: 1. Don't use int, use a type that gives stronger range assurances, like int_fast32_t (though I'm not sure at a glance what's the minimum legal value of INT_FAST32_MAX) 2. Put a compile-time assert to ensure that your range assumptions are met by the target platform's 'int' A pity that Ada's 'range types' approach to fixed-point types never caught on. It solves this platform-variance question, expresses the programmer's intent better, and enables useful runtime checks. It's possible with C++ templates (libraries exist for the purpose), but no-one does it. As for the question of what our static/dynamic analysis tools should do: they should be paranoid, and warn that the code might invoke UB, unless specifically configured to make strong platform assumptions. By default, we should aim to write good portable C.
    - dhekir 9y ago
      Even CompCert, the formally verified C compiler, had to make some concessions concerning the standard: it does not verify C per se, but CompCert C (http://compcert.inria.fr/man/manual005.html http://compcert.inria.fr/man/manual005.html), which is very close to C99 but with fixed-size integers (32-bit), two's complement signed integers (so no UB in signed overflows), etc. Otherwise, it is practically impossible to find some actually useful C code that is fully portable and compliant. But I agree that analysis tools should be as configurable as possible, and report UB whenever they can. However, if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off. It's a delicate balance between paranoia and usability. Even -Wall -Wextra -pedantic do not activate all warnings about detectable UBs, and that's about as paranoid as you can get in GCC/Clang.
      - tom_mellior 9y ago
        CompCert doesn't verify C, it compiles it. And like any compiler, it uses the type sizes defined by the ABI it targets.
      - MaxBarraclough 9y ago
        As tom_mellior says, CompCert is just a compiler, and it's not deviating from the C standard. The C standard says that sizeof(int) is implementation defined. CompCert has to choose a size, and they go with the unsurprising choice of 32-bit. As for no UB in signed overflows: where the C standard says 'undefined behavior', that doesn't prohibit an implementation (i.e. a compiler) from picking a well-defined behavior. It just means that portable code mustn't rely on that behavior - build such code on a different standards-compliant compiler and you might end up with demons flying out of your nose, etc. > it is practically impossible to find some actually useful C code that is fully portable and compliant. Disagree. The C/C++ code I've written has been portable and standard. The hardest part was that CMake is a trainwreck. > if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off That's more an issue with legacy code that when writing new code.
- mcguire 9y ago
  One of the major difficulties of doing static analysis for systems programming languages like C is that the semantics are defined by the whole system, not just the language. Writing a value to an obscure location not otherwise mentioned in your program is how you turn on that led. No, it's not portable. Yes, it's necessary. And that's ok. Better tools are needed.(TM) Check out "Some were meant for C" for an interesting read. http://www.cl.cam.ac.uk/~srk31/#onward17 http://www.cl.cam.ac.uk/~srk31/#onward17
  - MaxBarraclough 9y ago
    > No, it's not portable. Yes, it's necessary. And that's ok. Indeed, and it may be necessary to have an analysis tool skip over that code, but it applies to only a tiny minority of C code. Interesting skim-read, that paper. I agree with the author's lamentation that we so often pretend there's nothing we can do about C's safety issues. Even configuring GCC to check all dereferences for NULL, strikes many people as unusually rigorous. Dev+debug builds in particular should have as many runtime checks as possible, but for no obvious good reason, that's just not how we do things.

MaxBarraclough 9y ago

> Out of interest, where is that quoted sentence from? Oops, I should've replied to modless's comment - it's from this blog post: https://trust-in-soft.com/out-of-bounds-pointers-a-common-pattern-and-how-to-avoid-it/ https://trust-in-soft.com/out-of-bounds-pointers-a-common-pa... > you happen to be mostly sure that x86-64 GCC on Linux generates code as they expect, then that's fine. Being 'mostly sure' isn't good enough; that's the point of rigorous tools like this. If a new GCC optimisation breaks your code because you failed to follow the letter of the law and had UB in your code, that's your fault, not GCC's. > There is just too much implementation-defined stuff. Take that thinking to an extreme and you're barely able to reason rigorously about C code at all. Any number of dangerous constructs might happen to work on a given CPU+compiler. Good C code should be portable. Detecting dangerous, poor quality code is the whole point of tools like tis-interpreter. Things like casting int* to int and back to int* might happen to work on your CPU+compiler, but it should cause warnings.

tom_mellior 9y ago
> Take that thinking to an extreme and you're barely able to reason rigorously about C code at all. No reason to take things to the extreme. Is the code int i = 32767; int n = i + i; well-defined? It is implementation-defined whether it is undefined [0], since that depends on the implementation's size for int. You are barely able to reason rigorously about C code without considering some concrete real-world implementation's behavior. (I agree that the uintptr_t thing would merit an optional warning; maybe there is one.) [0] Language lawyers might disagree with this statement and just call it undefined. But if anything, that's even less useful.
- MaxBarraclough 9y ago
  That's a good example. I see two ways to handle that one: 1. Don't use int, use a type that gives stronger range assurances, like int_fast32_t (though I'm not sure at a glance what's the minimum legal value of INT_FAST32_MAX) 2. Put a compile-time assert to ensure that your range assumptions are met by the target platform's 'int' A pity that Ada's 'range types' approach to fixed-point types never caught on. It solves this platform-variance question, expresses the programmer's intent better, and enables useful runtime checks. It's possible with C++ templates (libraries exist for the purpose), but no-one does it. As for the question of what our static/dynamic analysis tools should do: they should be paranoid, and warn that the code might invoke UB, unless specifically configured to make strong platform assumptions. By default, we should aim to write good portable C.
  - dhekir 9y ago
    Even CompCert, the formally verified C compiler, had to make some concessions concerning the standard: it does not verify C per se, but CompCert C (http://compcert.inria.fr/man/manual005.html http://compcert.inria.fr/man/manual005.html), which is very close to C99 but with fixed-size integers (32-bit), two's complement signed integers (so no UB in signed overflows), etc. Otherwise, it is practically impossible to find some actually useful C code that is fully portable and compliant. But I agree that analysis tools should be as configurable as possible, and report UB whenever they can. However, if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off. It's a delicate balance between paranoia and usability. Even -Wall -Wextra -pedantic do not activate all warnings about detectable UBs, and that's about as paranoid as you can get in GCC/Clang.
    - tom_mellior 9y ago
      CompCert doesn't verify C, it compiles it. And like any compiler, it uses the type sizes defined by the ABI it targets.
    - MaxBarraclough 9y ago
      As tom_mellior says, CompCert is just a compiler, and it's not deviating from the C standard. The C standard says that sizeof(int) is implementation defined. CompCert has to choose a size, and they go with the unsurprising choice of 32-bit. As for no UB in signed overflows: where the C standard says 'undefined behavior', that doesn't prohibit an implementation (i.e. a compiler) from picking a well-defined behavior. It just means that portable code mustn't rely on that behavior - build such code on a different standards-compliant compiler and you might end up with demons flying out of your nose, etc. > it is practically impossible to find some actually useful C code that is fully portable and compliant. Disagree. The C/C++ code I've written has been portable and standard. The hardest part was that CMake is a trainwreck. > if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off That's more an issue with legacy code that when writing new code.
mcguire 9y ago
One of the major difficulties of doing static analysis for systems programming languages like C is that the semantics are defined by the whole system, not just the language. Writing a value to an obscure location not otherwise mentioned in your program is how you turn on that led. No, it's not portable. Yes, it's necessary. And that's ok. Better tools are needed.(TM) Check out "Some were meant for C" for an interesting read. http://www.cl.cam.ac.uk/~srk31/#onward17 http://www.cl.cam.ac.uk/~srk31/#onward17
- MaxBarraclough 9y ago
  > No, it's not portable. Yes, it's necessary. And that's ok. Indeed, and it may be necessary to have an analysis tool skip over that code, but it applies to only a tiny minority of C code. Interesting skim-read, that paper. I agree with the author's lamentation that we so often pretend there's nothing we can do about C's safety issues. Even configuring GCC to check all dereferences for NULL, strikes many people as unusually rigorous. Dev+debug builds in particular should have as many runtime checks as possible, but for no obvious good reason, that's just not how we do things.