Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis
<br xmlns:etd="http://www.ouls.ox.ac.uk/ora/modsextensions">Interprocedural analyses are compositional when they compute over-approximations of procedures in a bottom-up fashion. These analyses are usually more scalable than top-down analyses, which compute a different procedure summ...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer
2015
|
| _version_ | 1826283840425951232 |
|---|---|
| author | Castelnuovo, G Naik, M Rinetzky, N Sagiv, M Yang, H |
| author_facet | Castelnuovo, G Naik, M Rinetzky, N Sagiv, M Yang, H |
| author_sort | Castelnuovo, G |
| collection | OXFORD |
| description | <br xmlns:etd="http://www.ouls.ox.ac.uk/ora/modsextensions">Interprocedural analyses are compositional when they compute over-approximations of procedures in a bottom-up fashion. These analyses are usually more scalable than top-down analyses, which compute a different procedure summary for every calling context. However, compositional analyses are rare in practice as it is difficult to develop them with enough precision.</br><br xmlns:etd="http://www.ouls.ox.ac.uk/ora/modsextensions">We establish a connection between compositional analyses and modular lattices, which require certain associativity between the lattice join and meet operations, and use it to develop a compositional version of the connection analysis by Ghiya and Hendren. Our version is slightly more conservative than the original top-down analysis in order to meet our modularity requirement. When applied to real-world Java programs our analysis scaled much better than the original top-down version: The top-down analysis times out in the largest two of our five programs, while ours incurred only 2–5% of precision loss in the remaining programs.</br> |
| first_indexed | 2024-03-07T01:04:54Z |
| format | Conference item |
| id | oxford-uuid:8afe6cc2-700e-4530-8018-ff394ed65cdc |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:04:54Z |
| publishDate | 2015 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:8afe6cc2-700e-4530-8018-ff394ed65cdc2022-03-26T22:35:14ZModularity in lattices: a case study on the correspondence between top-down and bottom-up analysisConference itemhttp://purl.org/coar/resource_type/c_5794uuid:8afe6cc2-700e-4530-8018-ff394ed65cdcSymplectic Elements at OxfordSpringer2015Castelnuovo, GNaik, MRinetzky, NSagiv, MYang, H<br xmlns:etd="http://www.ouls.ox.ac.uk/ora/modsextensions">Interprocedural analyses are compositional when they compute over-approximations of procedures in a bottom-up fashion. These analyses are usually more scalable than top-down analyses, which compute a different procedure summary for every calling context. However, compositional analyses are rare in practice as it is difficult to develop them with enough precision.</br><br xmlns:etd="http://www.ouls.ox.ac.uk/ora/modsextensions">We establish a connection between compositional analyses and modular lattices, which require certain associativity between the lattice join and meet operations, and use it to develop a compositional version of the connection analysis by Ghiya and Hendren. Our version is slightly more conservative than the original top-down analysis in order to meet our modularity requirement. When applied to real-world Java programs our analysis scaled much better than the original top-down version: The top-down analysis times out in the largest two of our five programs, while ours incurred only 2–5% of precision loss in the remaining programs.</br> |
| spellingShingle | Castelnuovo, G Naik, M Rinetzky, N Sagiv, M Yang, H Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title | Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title_full | Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title_fullStr | Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title_full_unstemmed | Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title_short | Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis |
| title_sort | modularity in lattices a case study on the correspondence between top down and bottom up analysis |
| work_keys_str_mv | AT castelnuovog modularityinlatticesacasestudyonthecorrespondencebetweentopdownandbottomupanalysis AT naikm modularityinlatticesacasestudyonthecorrespondencebetweentopdownandbottomupanalysis AT rinetzkyn modularityinlatticesacasestudyonthecorrespondencebetweentopdownandbottomupanalysis AT sagivm modularityinlatticesacasestudyonthecorrespondencebetweentopdownandbottomupanalysis AT yangh modularityinlatticesacasestudyonthecorrespondencebetweentopdownandbottomupanalysis |