Re:Open-sourcing Facebook Infer: Identify bugs before you ship
by cactusface on Thursday June 11, 2015 @07:33PM
(#9703118)
Cool, thanks for the details. So... what do you do about cycles?
By "change" I didn't mean code change, I meant change in the information about the procedure collected during an iteration of the fixed point computation. But from the sounds of things you aren't computing a fixed point.
For example: A calls B and B calls A. You have information A0 and B0 about A and B. Analyze B, you have information B1 about B. Then you go and analyze A using B1. This gives you A1. Now you have to redo B, and compute B2. Use this to compute A2. This carries on until the information is not changing, i.e. An = An + 1 and Bn = Bn + 1.
Re:Open-sourcing Facebook Infer: Identify bugs before you ship
by theblatte on Thursday June 11, 2015 @07:48PM
(#9703162)
Infer computes fixpoints whenever there is a cycle in the call graph, until it reaches stable procedure summaries or timeouts.
Re:Open-sourcing Facebook Infer: Identify bugs before you ship
by cactusface on Thursday June 11, 2015 @08:42PM
(#9703352)
Ok, thanks for indulging my curiosity guys!
It's true that it a procedure changes that you may have to re-analyze all dependent procedures (and calling procedures!) in the worst case. However, in the bottom-up scheme you only need to re-analyze a procedure when the code change produces a change in the computed summary, and in practice summaries are frequently quite stable.