Taglia le funzioni costose nell'interpretazione astratta inter-procedurale

Question

Sto eseguendo alcune interpretazioni astratte inter-procedurali per catturare alcune proprietà del programma. Seguendo il modo standard, quello che sto facendo è mantenere un elenco di lavoro di funzioni analizzate e sceglierne uno dall'elenco di lavoro per eseguire analisi intra-procedurali fino a quando l'elenco di lavoro non è vuoto.

Attualmente, ho osservato che il intra-Procedural L'analisi di alcune funzioni non terminerebbe. Fondamentalmente, sta solo prendendo troppa memoria e diventa troppo lento per ragionare anche per un'altra affermazione.

Naturalmente, posso ottimizzare la mia base di codice e migliorare l'efficienza della memoria, ma fondamentalmente non dovrebbe aiutare troppo.

Ora sto cercando alcune strategie per bypassare tale ostacolo. Intuitivamente, quello che posso fare è Taglia un'analisi intra-procedurale Ogni volta che l'utilizzo della memoria diventa troppo in alto, restituisce un Superiore come valore di ritorno e passa alla funzione successiva nella mia lista di lavoro per l'analisi.

Questo sembra in modo molto naturale e dovrebbe esserlo suono anche! Tuttavia, dopo una rapida revisione di alcuni lavori di interpretazione astratta, non vedo alcun lavoro correlato che esegue un tale interruzione.

Quindi questa è la mia domanda:

1. Qual è l'approccio standard nell'interpretazione astratta se un'analisi intra-procedurale diventa troppo costosa per finire?

2. Presumo il taglio e il ritorno Superiore L'approccio è solido. Allora perché non dovrei trovare alcuna letteratura correlata che impiega tale approccio? È troppo ad hoc e ingenuo?