5 ms·

What is static program analysis?

110 points by p4bl0 14y ago

tedunangst 14y ago
"You can't solve the halting problem" was high on the list of responses that made selling static analysis a pain in the butt.
- Tipzntrix 14y ago
  Admittedly, "I don't know" probably isn't the answer a company wants to hear from your commercial tool.
  - tedunangst 14y ago
    The answer usually provided was "yes, your program has bugs" to which people objected theoretically. "Look, we found a bug." "My theory says you didn't." Followed quickly by the prize winning "that's not a bug."
    - Tipzntrix 14y ago
      Yeah, the truth is the methods companies use to find their bugs currently won't be able to give a definitive "no" anyway. The answers are really "yes, you have bugs" or "maybe you have bugs but we can't find any", which is true no matter how you coded. Static analysis would be another tool just like peer review or unit tests. I wonder if you could bring it up that way...
  - ken 14y ago
    Call me crazy, but I love it when a person or machine admits "I don't know" -- doubly so if they distinguish between "it's not possible to know" and "we simply haven't handled that case yet". That can be extremely useful information to have!
- ScottBurson 14y ago
  Yes, even people who are aware of the halting problem often misunderstand its implications. What Turing proved is that no algorithm -- in the sense of an effective procedure, that is guaranteed to return the correct answer in finite time on any input -- can solve the halting problem. But there is a critical difference between algorithms and heuristics. A heuristic is not guaranteed to do anything, but nonetheless, collections of heuristics can be assembled that can analyze properties of programs in many cases of actual interest. The distinction between algorithms and heuristics is, in my opinion, insufficiently appreciated. For example, the very phrase "genetic algorithms" is a contradiction in terms -- these are clearly heuristics, not algorithms. Anyway, back to your point, we who are still selling static analysis -- I'm not sure why you used the past tense there; it's a growing business -- find that people who don't understand the halting problem at all are perhaps as much a source of difficulty as those who are aware of it but don't understand its implications. The latter group are skeptical that our products can work at all, but the former are often baffled and indignant that the products don't understand properties of their code that seem obvious. (The fact that analysis often takes a long time and needs large amounts of RAM also surprises some people.) But I think the world is gradually coming to understand what static analysis can and can't do. It's an education process and will take time.
  - tedunangst 14y ago
    Past tense because I no longer sell static analysis software.
    - jdp23 14y ago
      Do you miss it? I sometimes do ...
  - scott_s 14y ago
    The kinds of static analysis you're talking about are different than what Matt is talking about in his article. Matt is talking about situations where you can make guarantees. That is, if his analyzer says that a register can never take on a negative value, that is a guarantee. It is not based on a heuristic, it is based on a proof. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. If I understand you correctly, you're talking about heuristics which allow one to say "It is very likely that this program will exhibit that behavior." It's not a guarantee, because it's not based on a proof, but rather on heuristics which try to match patterns in the code in question to patterns in code that was known to exhibit such behavior. Carmack talks about using such static analysis in his projects in a popular blog post (HN discussions: http://news.ycombinator.com/item?id=4543553 http://news.ycombinator.com/item?id=4543553 and http://news.ycombinator.com/item?id=3388290 http://news.ycombinator.com/item?id=3388290). In simpler terms, Matt's approach avoids the halting problem by only providing guarantees on a limited set of behaviors. The approach you're talking about avoids the halting problem by not providing guarantees, but by providing likelihoods.
- iskander 14y ago
  It's not that you can't solve the halting problem--- it's that you can't always solve the halting problem. Sometimes (such as when you're building things that can explode or kill people) you'll settle for an overly conservative approximation to the halting problem (see http://en.wikipedia.org/wiki/Termination_analysis http://en.wikipedia.org/wiki/Termination_analysis). You'll reject some programs which are OK but anything which passes your analysis will be guaranteed to halt.
- opminion 14y ago
  Most practical functions, as implemented when programming, are primitive recursive, not partial recursive. Thus they don't suffer from the halting problem.
clobber 14y ago
Interesting write up. LLVM defines it as "a collection of algorithms and techniques used to analyze source code in order to automatically find bugs." http://clang-analyzer.llvm.org/ http://clang-analyzer.llvm.org/
SkyMarshal 14y ago
Something I've wondered but never got around to asking - why is it called Static Analysis? Why not Dynamic Analysis, or Runtime Analysis, or something else?
- ScottBurson 14y ago
  Precisely because it's done without actually running the program. Dynamic analysis is where you do actually run the program.
- Tipzntrix 14y ago
  It doesn't analyse at runtime. It simulates certain runtime states but looks at the code at compile time. Since it analyses static code that is not changing, the term Static Analysis is used.
- p4bl0 14y ago
  Precisely because it is not done at runtime not dynamically but statically: the goal is to verify properties of a given program without having to actually run it.
- lmm 14y ago
  It doesn't take place at runtime; that's kind of the point of the name. I suspect the static=compile time, dynamic=run time terminology comes from linking, in which context it makes more sense - the linkage of a "staticly linked" program really is static.
deleted 14y ago
[deleted]
d0mine 14y ago
Analyzing sign example doesn't work in C where signed integer overflow is undefined behavior. Example http://stackoverflow.com/questions/12729110/strange-integer-behavior-with-gcc-o2 http://stackoverflow.com/questions/12729110/strange-integer-...
- mattmight 14y ago
  Right. It works for the register language with infinite precision integers. If you want it to work for C, you'll have to redefine the abstractions of addition and multiplication (and every other operation) appropriately. You'll also have to parameterize it by word size, endianness, signedness and type of arithmetic. That is, sound static analysis for C is almost certainly going to be platform-specific. But, you can still do it.
  - wladimir 14y ago
    But, you can still do it. Indeed. Arguably, compilers do it all the time to be able to (safely) do optimizations. Hence static analyzers are usually an extension to an compiler. Frama-C kind of being the exception, using CIL instead of the intermediate representation of a production compiler.
randartie 14y ago
I wish I knew what I was reading right now

110 points by p4bl0 14y ago

"You can't solve the halting problem" was high on the list of responses that made selling static analysis a pain in the butt.

Tipzntrix 14y ago
Admittedly, "I don't know" probably isn't the answer a company wants to hear from your commercial tool.
- tedunangst 14y ago
  The answer usually provided was "yes, your program has bugs" to which people objected theoretically. "Look, we found a bug." "My theory says you didn't." Followed quickly by the prize winning "that's not a bug."
  - Tipzntrix 14y ago
    Yeah, the truth is the methods companies use to find their bugs currently won't be able to give a definitive "no" anyway. The answers are really "yes, you have bugs" or "maybe you have bugs but we can't find any", which is true no matter how you coded. Static analysis would be another tool just like peer review or unit tests. I wonder if you could bring it up that way...
- ken 14y ago
  Call me crazy, but I love it when a person or machine admits "I don't know" -- doubly so if they distinguish between "it's not possible to know" and "we simply haven't handled that case yet". That can be extremely useful information to have!
ScottBurson 14y ago
Yes, even people who are aware of the halting problem often misunderstand its implications. What Turing proved is that no algorithm -- in the sense of an effective procedure, that is guaranteed to return the correct answer in finite time on any input -- can solve the halting problem. But there is a critical difference between algorithms and heuristics. A heuristic is not guaranteed to do anything, but nonetheless, collections of heuristics can be assembled that can analyze properties of programs in many cases of actual interest. The distinction between algorithms and heuristics is, in my opinion, insufficiently appreciated. For example, the very phrase "genetic algorithms" is a contradiction in terms -- these are clearly heuristics, not algorithms. Anyway, back to your point, we who are still selling static analysis -- I'm not sure why you used the past tense there; it's a growing business -- find that people who don't understand the halting problem at all are perhaps as much a source of difficulty as those who are aware of it but don't understand its implications. The latter group are skeptical that our products can work at all, but the former are often baffled and indignant that the products don't understand properties of their code that seem obvious. (The fact that analysis often takes a long time and needs large amounts of RAM also surprises some people.) But I think the world is gradually coming to understand what static analysis can and can't do. It's an education process and will take time.
- tedunangst 14y ago
  Past tense because I no longer sell static analysis software.
  - jdp23 14y ago
    Do you miss it? I sometimes do ...
- scott_s 14y ago
  The kinds of static analysis you're talking about are different than what Matt is talking about in his article. Matt is talking about situations where you can make guarantees. That is, if his analyzer says that a register can never take on a negative value, that is a guarantee. It is not based on a heuristic, it is based on a proof. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. If I understand you correctly, you're talking about heuristics which allow one to say "It is very likely that this program will exhibit that behavior." It's not a guarantee, because it's not based on a proof, but rather on heuristics which try to match patterns in the code in question to patterns in code that was known to exhibit such behavior. Carmack talks about using such static analysis in his projects in a popular blog post (HN discussions: http://news.ycombinator.com/item?id=4543553 http://news.ycombinator.com/item?id=4543553 and http://news.ycombinator.com/item?id=3388290 http://news.ycombinator.com/item?id=3388290). In simpler terms, Matt's approach avoids the halting problem by only providing guarantees on a limited set of behaviors. The approach you're talking about avoids the halting problem by not providing guarantees, but by providing likelihoods.
iskander 14y ago
It's not that you can't solve the halting problem--- it's that you can't always solve the halting problem. Sometimes (such as when you're building things that can explode or kill people) you'll settle for an overly conservative approximation to the halting problem (see http://en.wikipedia.org/wiki/Termination_analysis http://en.wikipedia.org/wiki/Termination_analysis). You'll reject some programs which are OK but anything which passes your analysis will be guaranteed to halt.
opminion 14y ago
Most practical functions, as implemented when programming, are primitive recursive, not partial recursive. Thus they don't suffer from the halting problem.

clobber 14y ago

Interesting write up. LLVM defines it as "a collection of algorithms and techniques used to analyze source code in order to automatically find bugs." http://clang-analyzer.llvm.org/ http://clang-analyzer.llvm.org/

SkyMarshal 14y ago

Something I've wondered but never got around to asking - why is it called Static Analysis? Why not Dynamic Analysis, or Runtime Analysis, or something else?

ScottBurson 14y ago
Precisely because it's done without actually running the program. Dynamic analysis is where you do actually run the program.
Tipzntrix 14y ago
It doesn't analyse at runtime. It simulates certain runtime states but looks at the code at compile time. Since it analyses static code that is not changing, the term Static Analysis is used.
p4bl0 14y ago
Precisely because it is not done at runtime not dynamically but statically: the goal is to verify properties of a given program without having to actually run it.
lmm 14y ago
It doesn't take place at runtime; that's kind of the point of the name. I suspect the static=compile time, dynamic=run time terminology comes from linking, in which context it makes more sense - the linkage of a "staticly linked" program really is static.

deleted 14y ago

[deleted]

d0mine 14y ago

Analyzing sign example doesn't work in C where signed integer overflow is undefined behavior. Example http://stackoverflow.com/questions/12729110/strange-integer-behavior-with-gcc-o2 http://stackoverflow.com/questions/12729110/strange-integer-...

mattmight 14y ago
Right. It works for the register language with infinite precision integers. If you want it to work for C, you'll have to redefine the abstractions of addition and multiplication (and every other operation) appropriately. You'll also have to parameterize it by word size, endianness, signedness and type of arithmetic. That is, sound static analysis for C is almost certainly going to be platform-specific. But, you can still do it.
- wladimir 14y ago
  But, you can still do it. Indeed. Arguably, compilers do it all the time to be able to (safely) do optimizations. Hence static analyzers are usually an extension to an compiler. Frama-C kind of being the exception, using CIL instead of the intermediate representation of a production compiler.

randartie 14y ago

I wish I knew what I was reading right now