I am performing some inter-procedural abstract interpretation to capture certain program properties. Following the standard way, what I am doing is to maintain a work list of to-be-analyzed functions, and pick one from the work list to perform intra-procedural analysis until the work list is empty.

Currently, I observed that the intra-procedural analysis of certain functions would not terminate. Basically, it is just taking too much memory and become too slow to reason for even one more statement.

Of course, I can optimize my code base and improve the memory efficiency, but fundamentally that shouldn't help too much.

Now I am seeking for some strategies to bypass such obstacle. Intuitively, what I can do is to cut a intra-procedural analysis off whenever the memory usage grows too high, return a Top as the return value, and switch to the next function in my work list for analysis.

This seems very naturally, and should be sound as well! However, after some quick review of some abstract interpretation work, I don't see any related work performing such cut off.

So here is my question:

  1. What is the standard approach in abstract interpretation if a intra-procedural analysis becomes too costly to finish?

  2. I assume the cut off and return Top approach is sound. Then why shouldn't I find any related literature employing such approach? Is it too ad-hoc and naive?


Sure. "Cut off and return Top" is sound. It's valid. It seems like a reasonable thing to do.

I don't know if it has been studied or used before in the literature. I wouldn't be surprised if it has. It feels to me like a variant on widening, even though it's not identical to the usual widening operator. I've seen similar methods applied before (if you get stuck, give up and return Top) in other situations.

I don't think there's a single standard approach to this problem. My impression is that there are multiple techniques. You can memoize analysis of a function (so you lazily generate a transfer function that summarizes the effect of the function, in terms of its arguments, and then reuse that information when you need it again in the future). You can use widening operators. You can use counter-example guided refinement to start with a coarse abstraction (which is efficient for static analysis), and then make the abstraction more precise as needed. I imagine you could also do the converse: start with a fine-grained abstraction, and if it is taking too long, switch to a more coarse abstraction and restart the analysis with that coarser abstraction. There are probably many other possible techniques, and the best one might depend on the specifics of your particular analysis.

  • $\begingroup$ Thanks a lot for your answer! My current (summary-based) inter-procedural solution is actually comparable to your suggestion one, i.e., "memoize analysis of a function". On the other hand, whenever a new input is not a subset of the already-recorded input-output pairs, I have to merge inputs together and re-run the intra-procedural analysis of this function. $\endgroup$ – lllllllllllll May 6 '17 at 16:15
  • $\begingroup$ Could you please shed more lights on the counter-example guided refinement method? I never heard of such approaches. Thank you! $\endgroup$ – lllllllllllll May 6 '17 at 16:16
  • $\begingroup$ Of course, when I said a new input is not a subset of the already-recorded input in the procedural summary. I assume the flow functions of my analysis are all monotonic. $\endgroup$ – lllllllllllll May 6 '17 at 16:21
  • $\begingroup$ @computereasy, a search on Google Scholar on counter-example guided refinement (CEGAR) will turn up lots of examples. For example, you can read about the BLAST software model checker project, as one example of this approach (but there are many others). $\endgroup$ – D.W. May 6 '17 at 16:33
  • $\begingroup$ Great! I will search the literatures! $\endgroup$ – lllllllllllll May 6 '17 at 16:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.