Detail publikace
Scaling Type-Based Points-to Analysis with Saturation
points-to analýza, statická analýza, ukazatelová analýza, Java, GraalVM
Návrh celoprogramové statické analýzy vyžaduje kompromis mezi přesností a škálovatelností. Kontextově necitlivá points-to analýza je sice často považována za dobrý kompromis, ale stále se vyznačuje nelineární složitostí, která při analýze velkých aplikací vede k problémům se škálovatelností. Na druhé straně rychlá typová analýza se dobře škáluje, ale chybí jí přesnost. V kontextově necitlivé analýze používáme saturaci, aby byla stejně škálovatelná jako rychlá analýza typu a zároveň si zachovala většinu přesnosti points-to analýzy. Se saturací propaguje points-to analýza pro proměnné pouze malé množiny. Pokud může mít proměnná více hodnot, než je určitá prahová hodnota, je proměnná a všechna její použití považována za saturovanou a dále se neanalyzuje.
Naše implementace v analýze points-to v GraalVM Native Image, což je uzavřený přístup k sestavování samostatných binárních souborů pro aplikace Java, ukazuje, že saturace umožňuje GraalVM Native Image analyzovat velké aplikace se stovkami tisíc metod za méně než dvě minuty.
@article{BUT189291,
author="Christian {Wimmer} and Condrut {Stancu} and David {Kozák} and Thomas {Wuerthinger}",
title="Scaling Type-Based Points-to Analysis with Saturation",
journal="Proceedings of the ACM on Programming Languages",
year="2024",
volume="8",
number="PLDI",
pages="990--1013",
doi="10.1145/3656417",
issn="2475-1421",
url="https://dl.acm.org/doi/pdf/10.1145/3656417"
}