12 ms·

Yes, absolutely. Static analyzers are for when your test suite is subpar. If you're obsessive, like the SQLite guys [1], runtime checkers are better. But you

Yes, absolutely. Static analyzers are for when your test suite is subpar. If you're obsessive, like the SQLite guys [1], runtime checkers are better. But you have to be obsessive about an excessive test suite. [1]: https://sqlite.org/faq.html#q17 https://sqlite.org/faq.html#q17

AlotOfReading 3y ago
Yeah, no. They're different things. Formal methods, including static analyzers, can prove the absence of issues in all possible conditions under some assumptions. Tests verify that implementation, under the tested conditions, once. You can't replace testing with formal methods, but formal methods are more powerful when they work. That sqlite hasn't found them useful is just a reflection of how absurdly far out they are on the testing spectrum and how complicated the problem domain they're operating in is (very).
- gavinhoward 3y ago
  Don't get me wrong; I'm a fan of formal methods, when they can work. But you're also weakening your own point; you admit that if you test enough, they don't work as well, and you also admit that they work less well the more complicated things get. The other problem is showing that the artifact you proved is the same artifact that you are using. The enormous amount of effort put in by the seL4 people is proof that that is non-trivial, and seL4 is tiny compared to SQLite. So when you say, "formal methods are more powerful when they work," you are right, but "when they work" is carrying a lot of weight.
  - nicoburns 3y ago
    Stronger type systems can get you a lot of the benefits of formal methods with very little work. A SQLite level test suite is probably still better, but very few projects have the time or budget to do that.
    - gavinhoward 3y ago
      I agree. And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that. But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.
  - nanolith 3y ago
    seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker. Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough. I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.
    - gavinhoward 3y ago
      > It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. Sure, if you can. And I use such checkers too. But for a lot of people, the false positive false negative rates are still high. That's why tests can be better: there's no false positive or false negative. > The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. This is unfortunately completely naive. Of course model checkers miss things.
- derekerdmann 3y ago
  Static analyzers are NOT formal methods. Reporting no issues just means your tool didn’t find anything, not that your program is correct.
  - adrianN 3y ago
    Formal methods do not necessarily prove the absence of bugs either.
    - worik 3y ago
      > Formal methods do not necessarily prove the absence of bugs either. They can demonstrate the bugs, when found, are in the specifications Or in the methods....
  - int0x80 3y ago
    If a static analyzer is sound, which is something that can be mathematically proven (formal method), will find ALL existing issues plus some false positives if it's not complete (which is almost always the case).
josephg 3y ago
In my experience you can get surprisingly far with automated fuzz testing and runtime checks. Doing it well is a bit of an art form - it’s quite easy to accidentally write fuzz tests which almost never exercise some code paths. Or end up with fuzzers that spend 99.9% of your cpu checking invariants and things like that. But with a good fuzzer, the ratio of bugs found per line of testing code is insanely high. And they’re much easier to maintain than a big bank of unit tests. Highly recommended if you want to get more bang per line of testing code.
- gavinhoward 3y ago
  Oh, yes, absolutely. I fuzz religiously. In fact, in my current project, I add every single path found by AFL++ to my test suite. It tests all kinds of terrible things, and then those paths are tested forever. I even run all the paths AFL++ finds through the sanitizers and Valgrind.
rewmie 3y ago
> Static analyzers are for when your test suite is subpar. No, this statement is quite wrong and expresses a failure to understand the roles and responsibilities of each class of automated tests, and the purpose of static code analysis tools. Automated tests and static code analysis tools are complementary tools. They don't share responsibilities at all. Just because both can run in the same pipeline stage that does not mean they serve the same purpose.
- gavinhoward 3y ago
  They do serve the same purpose: they find defects. But I also didn't define "subpar" for a test suite; the SQLite guys have full-coverage testing. That's probably the line for "subpar," and (almost) nobody else actually has that.
  - rewmie 3y ago
    > They do serve the same purpose: they find defects. No, not really. If you read up on the basics of automated testing, you'll find out that test classes such as unit, integration, UI, performance, accessibility, and localization tests share the same goal: specify and check invariants in the code and in its interfaces. Static code analysis tools have an entirely different set of responsibilities. They do not have the responsibility of checking the compliance with contracts, including things like SLAs or whether a button is navigatable with a keyboard as per the wishes of a Program Manager.
    - gavinhoward 3y ago
      You claim that static code analysis has different responsibilities, but then you leave out what those responsibilities are. So what are those responsibilities?
      - rewmie 3y ago
        > You claim that static code analysis has different responsibilities, but then you leave out what those responsibilities are. https://en.wikipedia.org/wiki/Static_program_analysis https://en.wikipedia.org/wiki/Static_program_analysis If you're interested in onboarding onto the topic, you can start by reading the first paragraph of the Rationale section.
mumblemumble 3y ago
This idea that static analysis, runtime checks, and automated tests are somehow in competition with each other is possibly the single worst outcome of the protracted dynamic vs static typing flamewar that the profession's been having for the past few decades.
- gavinhoward 3y ago
  I never said that. What I said is that runtime checking is better if you have a test suite that's good enough.
  - mumblemumble 3y ago
    That "better/worse" way of wording it places them in competition with each other, regardless of whether you say it explicitly. A way of discussing it that doesn't place them in competition with each other would instead talk about their relative characteristics, including factors that might make different options more or less effective (or even inapplicable) in certain circumstances. For example, there are certain classes of defect that cannot be detected at runtime. But what does and does not fall into this category depends on what programming language you're using. There are other classes of defect that cannot be detected statically, and the specifics of this list also depends on what language you're using. And then there's also a bunch of overlap, but the relative merits of one or another way of solving things cannot be boiled down to a simple "better/worse" hierarchy. The optimal strategy is often domain-specific and finding it may require weighing many tradeoffs.
    - gavinhoward 3y ago
      > That "better/worse" way of wording it places them in competition with each other, regardless of whether you say it explicitly. Absolutely not. It says that they have tradeoffs, and one will be better in certain situations, while the other will be better in others. If you think that means competition, you're overreading it.
  - Nokinside 3y ago
    I have written safety-critical code and nobody has a test suite that could do what Astrée does. It can be used to proves the absence of errors with the abstract interpretation that catches all divisions by zero, data races, and deadlocks, and does static taint checking. You want a test suite, but it's never better or good enough. Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html

AlotOfReading 3y ago

Yeah, no. They're different things. Formal methods, including static analyzers, can prove the absence of issues in all possible conditions under some assumptions. Tests verify that implementation, under the tested conditions, once. You can't replace testing with formal methods, but formal methods are more powerful when they work. That sqlite hasn't found them useful is just a reflection of how absurdly far out they are on the testing spectrum and how complicated the problem domain they're operating in is (very).

gavinhoward 3y ago
Don't get me wrong; I'm a fan of formal methods, when they can work. But you're also weakening your own point; you admit that if you test enough, they don't work as well, and you also admit that they work less well the more complicated things get. The other problem is showing that the artifact you proved is the same artifact that you are using. The enormous amount of effort put in by the seL4 people is proof that that is non-trivial, and seL4 is tiny compared to SQLite. So when you say, "formal methods are more powerful when they work," you are right, but "when they work" is carrying a lot of weight.
- nicoburns 3y ago
  Stronger type systems can get you a lot of the benefits of formal methods with very little work. A SQLite level test suite is probably still better, but very few projects have the time or budget to do that.
  - gavinhoward 3y ago
    I agree. And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that. But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.
- nanolith 3y ago
  seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker. Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough. I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.
  - gavinhoward 3y ago
    > It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. Sure, if you can. And I use such checkers too. But for a lot of people, the false positive false negative rates are still high. That's why tests can be better: there's no false positive or false negative. > The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. This is unfortunately completely naive. Of course model checkers miss things.
derekerdmann 3y ago
Static analyzers are NOT formal methods. Reporting no issues just means your tool didn’t find anything, not that your program is correct.
- adrianN 3y ago
  Formal methods do not necessarily prove the absence of bugs either.
  - worik 3y ago
    > Formal methods do not necessarily prove the absence of bugs either. They can demonstrate the bugs, when found, are in the specifications Or in the methods....
- int0x80 3y ago
  If a static analyzer is sound, which is something that can be mathematically proven (formal method), will find ALL existing issues plus some false positives if it's not complete (which is almost always the case).

josephg 3y ago

In my experience you can get surprisingly far with automated fuzz testing and runtime checks. Doing it well is a bit of an art form - it’s quite easy to accidentally write fuzz tests which almost never exercise some code paths. Or end up with fuzzers that spend 99.9% of your cpu checking invariants and things like that. But with a good fuzzer, the ratio of bugs found per line of testing code is insanely high. And they’re much easier to maintain than a big bank of unit tests. Highly recommended if you want to get more bang per line of testing code.

gavinhoward 3y ago
Oh, yes, absolutely. I fuzz religiously. In fact, in my current project, I add every single path found by AFL++ to my test suite. It tests all kinds of terrible things, and then those paths are tested forever. I even run all the paths AFL++ finds through the sanitizers and Valgrind.

rewmie 3y ago

> Static analyzers are for when your test suite is subpar. No, this statement is quite wrong and expresses a failure to understand the roles and responsibilities of each class of automated tests, and the purpose of static code analysis tools. Automated tests and static code analysis tools are complementary tools. They don't share responsibilities at all. Just because both can run in the same pipeline stage that does not mean they serve the same purpose.

gavinhoward 3y ago
They do serve the same purpose: they find defects. But I also didn't define "subpar" for a test suite; the SQLite guys have full-coverage testing. That's probably the line for "subpar," and (almost) nobody else actually has that.
- rewmie 3y ago
  > They do serve the same purpose: they find defects. No, not really. If you read up on the basics of automated testing, you'll find out that test classes such as unit, integration, UI, performance, accessibility, and localization tests share the same goal: specify and check invariants in the code and in its interfaces. Static code analysis tools have an entirely different set of responsibilities. They do not have the responsibility of checking the compliance with contracts, including things like SLAs or whether a button is navigatable with a keyboard as per the wishes of a Program Manager.
  - gavinhoward 3y ago
    You claim that static code analysis has different responsibilities, but then you leave out what those responsibilities are. So what are those responsibilities?
    - rewmie 3y ago
      > You claim that static code analysis has different responsibilities, but then you leave out what those responsibilities are. https://en.wikipedia.org/wiki/Static_program_analysis https://en.wikipedia.org/wiki/Static_program_analysis If you're interested in onboarding onto the topic, you can start by reading the first paragraph of the Rationale section.

mumblemumble 3y ago

This idea that static analysis, runtime checks, and automated tests are somehow in competition with each other is possibly the single worst outcome of the protracted dynamic vs static typing flamewar that the profession's been having for the past few decades.

gavinhoward 3y ago
I never said that. What I said is that runtime checking is better if you have a test suite that's good enough.
- mumblemumble 3y ago
  That "better/worse" way of wording it places them in competition with each other, regardless of whether you say it explicitly. A way of discussing it that doesn't place them in competition with each other would instead talk about their relative characteristics, including factors that might make different options more or less effective (or even inapplicable) in certain circumstances. For example, there are certain classes of defect that cannot be detected at runtime. But what does and does not fall into this category depends on what programming language you're using. There are other classes of defect that cannot be detected statically, and the specifics of this list also depends on what language you're using. And then there's also a bunch of overlap, but the relative merits of one or another way of solving things cannot be boiled down to a simple "better/worse" hierarchy. The optimal strategy is often domain-specific and finding it may require weighing many tradeoffs.
  - gavinhoward 3y ago
    > That "better/worse" way of wording it places them in competition with each other, regardless of whether you say it explicitly. Absolutely not. It says that they have tradeoffs, and one will be better in certain situations, while the other will be better in others. If you think that means competition, you're overreading it.
- Nokinside 3y ago
  I have written safety-critical code and nobody has a test suite that could do what Astrée does. It can be used to proves the absence of errors with the abstract interpretation that catches all divisions by zero, data races, and deadlocks, and does static taint checking. You want a test suite, but it's never better or good enough. Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html