4 ms·

D. Richard Hipp and the SQLite project have not had such a positive experience with static code analysis. They already use a massive amount of testing though. T

by asb 15y ago

D. Richard Hipp and the SQLite project have not had such a positive experience with static code analysis. They already use a massive amount of testing though. There's also no mention of commercial tools like Coverity. See the "Static Analysis" section: http://www.sqlite.org/testing.html http://www.sqlite.org/testing.html

kevingadd 15y ago
I would be shocked if any static analyzer could be truly useful for validating the implementation of a virtual machine, let alone one like SQLite's. The fact that SQLite makes heavy use of dynamic typing also seems like it would defeat attempts by a static analyzer to validate code.
- thesz 15y ago
  http://compcert.inria.fr/ http://compcert.inria.fr/ CompCert is a verified compiler that transforms code from "virtual machine" of language C to "virtual machine" of PowerPC. It is generated from Coq, though. But, please see ynot: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ They have a verified SQL compiler. Again, generated from Coq source. So I think you're wrong claiming that static analysis isn't useful for virtual machines. For C you have to have very extensive annotations, as it is not very expressive by itself, but static analysis is still possible.
  - _delirium 15y ago
    That's true, but I think a different class of tools: theorem-provers that depend on extensive domain-specific annotations (e.g. about SQL semantics) to prove correctness aren't usually applied in the same situations as tools like Coverity that do static analysis of raw C/C++ code to find likely bugs; though there's some convergence in the past 10 years.
masklinn 15y ago
> They already use a massive amount of testing though. Yes, as the page notes the SQLite codebase has a > 1000:1 tests to code ratio. I don't think there's any other codebase this thoroughly tested, and it makes sense that static analysis tools won't discover anything not already covered by tests.
- barkmadley 15y ago
  and it makes sense that static analysis tools won't discover anything not already covered by tests That assertion doesn't make a lot of sense to me. Most static analysers are capable of looking at the edge cases that a human may forget to write a test for, or may not even notice are there.
  - masklinn 15y ago
    When you have 1000 times as much test code and data as you have code to test, the odds of having missed a subset of the bugspace a static analyzer can find are very, very low I would say. Unless the people who wrote the tests are functionally retarded of course, but let's consider that not to be the case.
    - scott_s 15y ago
      I'm not so sure. I'm reading their testing document (and it's a great read), and it sounds like most of those tests are reactive: Whenever a bug is reported against SQLite, that bug is not considered fixed until new test cases have been added to the TCL test suite which would exhibit the bug in an unpatched version of SQLite. Over the years, this has resulted in thousands and thousands of new tests being added to the TCL test suite. These regression tests ensure that bugs that have been fixed in the past are not reintroduced into future versions of SQLite. While this is a great practice, it's reactive. It's the result of particular bugs, not someone asking, "What are the situations we haven't covered?" The coverage they have for error conditions (file system, out of memory, bit-flips) is impressive. I'm not saying I know you're wrong, but I think there are too many variables to say with confidence either way.
      - dasil003 15y ago
        The closest you can get to complete test coverage is a policy of writing test coverage for every single new feature coupled with this regression test policy, because once the code base gets to a certain size it's impossible for anyone to form a complete mental model of what is covered or not. If that's not good enough then I think static analysis is a decent step, but probably pales in comparison to using stricter languages (eg. Haskell).
groby_b 15y ago
At least this passage is complete nonsense: We cannot call to mind a single problem in SQLite that was detected by static analysis that was not first seen by one of the other testing methods described above If SA discovers a problem, you'll discover it the moment you run it through the analyzer, while by the dev's admission many of their bugs are discovered as bug reports. Which is clearly a bit later :) Now, it might well be that most of SQLite's bugs simply are not discovered by SA. But SA is not going to report them later than bug reports, unless you use it very infrequently.
- rogerbinns 15y ago
  Also look for 22nd November in the timeline - http://www.sqlite.org/src/timeline http://www.sqlite.org/src/timeline 3 problems were detected by Coverity and fixed in SQLite.

by asb 15y ago

kevingadd 15y ago

I would be shocked if any static analyzer could be truly useful for validating the implementation of a virtual machine, let alone one like SQLite's. The fact that SQLite makes heavy use of dynamic typing also seems like it would defeat attempts by a static analyzer to validate code.

thesz 15y ago
http://compcert.inria.fr/ http://compcert.inria.fr/ CompCert is a verified compiler that transforms code from "virtual machine" of language C to "virtual machine" of PowerPC. It is generated from Coq, though. But, please see ynot: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ They have a verified SQL compiler. Again, generated from Coq source. So I think you're wrong claiming that static analysis isn't useful for virtual machines. For C you have to have very extensive annotations, as it is not very expressive by itself, but static analysis is still possible.
- _delirium 15y ago
  That's true, but I think a different class of tools: theorem-provers that depend on extensive domain-specific annotations (e.g. about SQL semantics) to prove correctness aren't usually applied in the same situations as tools like Coverity that do static analysis of raw C/C++ code to find likely bugs; though there's some convergence in the past 10 years.

masklinn 15y ago

> They already use a massive amount of testing though. Yes, as the page notes the SQLite codebase has a > 1000:1 tests to code ratio. I don't think there's any other codebase this thoroughly tested, and it makes sense that static analysis tools won't discover anything not already covered by tests.

barkmadley 15y ago
and it makes sense that static analysis tools won't discover anything not already covered by tests That assertion doesn't make a lot of sense to me. Most static analysers are capable of looking at the edge cases that a human may forget to write a test for, or may not even notice are there.
- masklinn 15y ago
  When you have 1000 times as much test code and data as you have code to test, the odds of having missed a subset of the bugspace a static analyzer can find are very, very low I would say. Unless the people who wrote the tests are functionally retarded of course, but let's consider that not to be the case.
  - scott_s 15y ago
    I'm not so sure. I'm reading their testing document (and it's a great read), and it sounds like most of those tests are reactive: Whenever a bug is reported against SQLite, that bug is not considered fixed until new test cases have been added to the TCL test suite which would exhibit the bug in an unpatched version of SQLite. Over the years, this has resulted in thousands and thousands of new tests being added to the TCL test suite. These regression tests ensure that bugs that have been fixed in the past are not reintroduced into future versions of SQLite. While this is a great practice, it's reactive. It's the result of particular bugs, not someone asking, "What are the situations we haven't covered?" The coverage they have for error conditions (file system, out of memory, bit-flips) is impressive. I'm not saying I know you're wrong, but I think there are too many variables to say with confidence either way.
    - dasil003 15y ago
      The closest you can get to complete test coverage is a policy of writing test coverage for every single new feature coupled with this regression test policy, because once the code base gets to a certain size it's impossible for anyone to form a complete mental model of what is covered or not. If that's not good enough then I think static analysis is a decent step, but probably pales in comparison to using stricter languages (eg. Haskell).

groby_b 15y ago

At least this passage is complete nonsense: We cannot call to mind a single problem in SQLite that was detected by static analysis that was not first seen by one of the other testing methods described above If SA discovers a problem, you'll discover it the moment you run it through the analyzer, while by the dev's admission many of their bugs are discovered as bug reports. Which is clearly a bit later :) Now, it might well be that most of SQLite's bugs simply are not discovered by SA. But SA is not going to report them later than bug reports, unless you use it very infrequently.

rogerbinns 15y ago
Also look for 22nd November in the timeline - http://www.sqlite.org/src/timeline http://www.sqlite.org/src/timeline 3 problems were detected by Coverity and fixed in SQLite.