4 ms·

No, I'm talking about the same thing Matt is. Notice how, in his sign analysis example, the analyzer can return {-, 0, +}, indicating that it doesn't know the

No, I'm talking about the same thing Matt is. Notice how, in his sign analysis example, the analyzer can return {-, 0, +}, indicating that it doesn't know the sign of some particular value. Thus, it's not an algorithm for determining the signs of values computed by an arbitrary program; it's only a heuristic that will sometimes tell you the sign. (And I don't mean "sometimes" probabilistically -- I mean "for some expressions in some programs". Given a particular expression in a particular program, it's deterministic.) The art of static analysis, then, is to design heuristics that provide useful information in enough cases to be of practical value.

Darmani 14y ago
It's useful to make a distinction between the "sound" static analyses Matt Might posted about and heuristic-based, or "pragmatic" analyses. Cousot's Analysis of Signs is sound. It can fail by returning {-,0,+}. However, when it succeeds, it does make guarantees. If it returns {0} for an integer, then it has proven that that integer will always and only have the value 0. Furthermore, if that integer can be 0, it is guaranteed the analysis will return a set containing 0. Pragmatic analyses have no such guarantees; if a pragmatic analysis of signs returns {0}, then anything could happen. They are "pragmatic" in that their value is determined by how correlated their output is with the answer on real programs; there are no theorems to prove about them.
scott_s 14y ago
I think we have a disagreement on semantics. If you can provide a guarantee based on a proof, then I do not consider that a heuristic. I consider there to be two differences between proof-based analysis and heuristic-based analysis: 1. Proof-based analysis may provide guarantees. In other words, no false-positives, but false-negatives are possible. Heuristics cannot provide guarantees, only probabilities, and they can have both false-positives and false-negatives. 2. Heuristic-based analysis require data to create. For example, let's say we analyzed some code and saw: struct thing* = alloc_thing(); process_thing(thing); thing = alloc_thing(); A heuristic based analysis may say "The pattern of allocations and uses in this code is consistent with known memory leaks in other applications." That is, we have recognized a pattern in code that when seen elsewhere, there was a memory leak. This is a very different animal than proof-based analysis because it relies on historical data and pattern matching against it. But it may be a false-positive. In contrast, a proof-based analysis does not need to look at any other code but the one in question; it has proven what the behavior is. It could not provide a false-positive.
- ScottBurson 14y ago
  There are two different kinds of proofs in discussion here. You're talking about the proofs the analyzer provides about the behavior of the program under analysis. I'm talking about what we can or cannot prove about the behavior of the analyzer itself. Can we prove that it will never construct an incorrect proof? Or that it will find a proof if one exists?
  - Darmani 14y ago
    Those are all actually the same proof. The proofs that the analysis provides about the program are essentially the soundness proof of the analysis combined with its output. So if I prove that the signs that values of a variable can hold will be contained in the set found by my static analysis, and my analyzer outputs {+}, then that is a proof that that variable can only store positive values. It produces a proof in the same sense that, if I prove the Pythagorean theorem, then I can evaluate the expression sqrt(x^2+y^2) with x=3 and y=4 to get a proof that the corresponding line has length 5. Getting an incorrect proof out of that would be tantamount to an arithmetic error. Note that most analyses do no actual automated theorem proving; they just, conceptually at least, instantiate existing proofs. If, by "find a proof," you mean "show the presence of bugs if there are any," then that's part of the same soundness proof. Conversely, showing the absence of bugs if there aren't any is completeness; you can't have both due to the halting problem. Whether an analyzer correctly implements an analysis is a totally separate beast, and is an example of verification. Xavier Leroy has done some excellent work in verifying static analyzers.
- cwzwarich 14y ago
  You can use heuristics in provably sound static analyses as well, so your distinction isn't really valid.
  - scott_s 14y ago
    The is a clear distinction between analysis that relies solely on heuristics and analysis that can provide a proof, even if it also uses heuristics.

Darmani 14y ago

It's useful to make a distinction between the "sound" static analyses Matt Might posted about and heuristic-based, or "pragmatic" analyses. Cousot's Analysis of Signs is sound. It can fail by returning {-,0,+}. However, when it succeeds, it does make guarantees. If it returns {0} for an integer, then it has proven that that integer will always and only have the value 0. Furthermore, if that integer can be 0, it is guaranteed the analysis will return a set containing 0. Pragmatic analyses have no such guarantees; if a pragmatic analysis of signs returns {0}, then anything could happen. They are "pragmatic" in that their value is determined by how correlated their output is with the answer on real programs; there are no theorems to prove about them.

scott_s 14y ago

I think we have a disagreement on semantics. If you can provide a guarantee based on a proof, then I do not consider that a heuristic. I consider there to be two differences between proof-based analysis and heuristic-based analysis: 1. Proof-based analysis may provide guarantees. In other words, no false-positives, but false-negatives are possible. Heuristics cannot provide guarantees, only probabilities, and they can have both false-positives and false-negatives. 2. Heuristic-based analysis require data to create. For example, let's say we analyzed some code and saw: struct thing* = alloc_thing(); process_thing(thing); thing = alloc_thing(); A heuristic based analysis may say "The pattern of allocations and uses in this code is consistent with known memory leaks in other applications." That is, we have recognized a pattern in code that when seen elsewhere, there was a memory leak. This is a very different animal than proof-based analysis because it relies on historical data and pattern matching against it. But it may be a false-positive. In contrast, a proof-based analysis does not need to look at any other code but the one in question; it has proven what the behavior is. It could not provide a false-positive.

ScottBurson 14y ago
There are two different kinds of proofs in discussion here. You're talking about the proofs the analyzer provides about the behavior of the program under analysis. I'm talking about what we can or cannot prove about the behavior of the analyzer itself. Can we prove that it will never construct an incorrect proof? Or that it will find a proof if one exists?
- Darmani 14y ago
  Those are all actually the same proof. The proofs that the analysis provides about the program are essentially the soundness proof of the analysis combined with its output. So if I prove that the signs that values of a variable can hold will be contained in the set found by my static analysis, and my analyzer outputs {+}, then that is a proof that that variable can only store positive values. It produces a proof in the same sense that, if I prove the Pythagorean theorem, then I can evaluate the expression sqrt(x^2+y^2) with x=3 and y=4 to get a proof that the corresponding line has length 5. Getting an incorrect proof out of that would be tantamount to an arithmetic error. Note that most analyses do no actual automated theorem proving; they just, conceptually at least, instantiate existing proofs. If, by "find a proof," you mean "show the presence of bugs if there are any," then that's part of the same soundness proof. Conversely, showing the absence of bugs if there aren't any is completeness; you can't have both due to the halting problem. Whether an analyzer correctly implements an analysis is a totally separate beast, and is an example of verification. Xavier Leroy has done some excellent work in verifying static analyzers.
cwzwarich 14y ago
You can use heuristics in provably sound static analyses as well, so your distinction isn't really valid.
- scott_s 14y ago
  The is a clear distinction between analysis that relies solely on heuristics and analysis that can provide a proof, even if it also uses heuristics.