Pith. sign in

REVIEW

Hybrid Inlining: A Compositional and Context Sensitive Static Analysis Framework

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2210.14436 v1 pith:4CRSPVQA submitted 2022-10-26 cs.LO

Hybrid Inlining: A Compositional and Context Sensitive Static Analysis Framework

classification cs.LO
keywords analysiscontextstatementssensitivecompositionalcriticalframeworkstatic
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original abstract

Context sensitivity is essential for achieving the precision in inter-procedural static analysis. To be (fully) context sensitive, top-down analysis needs to fully inline all statements of the callees at each callsite, leading to statement explosion. Compositional analysis, which inlines summaries of the callees, scales up but often loses precision, as it is not strictly context sensitive. We propose a compositional and strictly context sensitive framework for static analysis. This framework is based on one key observation: a compositional static analysis often loses precision only on some critical statements that need to be analyzed context sensitively. Our approach hybridly inlines the critical statements and the summaries of non-critical statements of each callee, thus avoiding the re-analysis of non-critical ones. In addition, our analysis lazily summarizes the critical statements, by stopping propagating the critical statements once the calling context accumulated is adequate. Hybrid Inlining can be as precise as context sensitive top-down analysis. We have designed and implemented a pointer analysis based on this framework. It can analyze large Java programs from the Dacapo benchmark suite and industry in minutes. In our evaluation, compared to context insensitive analysis, Hybrid Inlining just brings 65% and 1% additional time overhead on Dacapo and industrial applications respectively.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.