m-CFA Exhibits Perfect Stack Precision
m-CFA is a hierarchy of control-flow analyses (CFA) formulated as abstract abstract machines and designed to exhibit polynomial time complexity while remaining usefully precise. The Pushdown for Free (P4F) technique prescribes a continuation allocator which induces perfect stack precision wherein each function invocation returns to only its call. Unfortunately, it is difficult to apply the P4F technique to m-CFA as P4F is developed in an ANF setting but m-CFA is formulated in a CPS setting. In this paper, we recall that ANF corresponds to a CPS sublanguage without non-local control and show that m-CFA behaves identically on both. With an ANF-based m-CFA in hand, we turn to applying the P4F technique only to discover that it already follows the prescription. In other words, m-CFA has always had perfect stack precision, a characteristic neither intended nor recognized, at its development or since. In addition to being surprising, we discuss how this result allows a spectrum of non-local control constructs to be supported more easily and with more precision than previous techniques.
Wed 29 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00 | |||
10:30 30mTalk | Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection APLAS 2023 Wenhua Li National University of Singapore, Quang Loc Le University College London, Yahui Song , Wei-Ngan Chin National University of Singapore | ||
11:00 30mTalk | m-CFA Exhibits Perfect Stack Precision APLAS 2023 Kimball Germane Brigham Young University | ||
11:30 30mTalk | TorchProbe: Fuzzing Dynamic Deep Learning Compilers APLAS 2023 Qidong Su University of Toronto / Vector Institute, Chuqin Geng McGill University, Gennady Pekhimenko University of Toronto / Vector Institute, Xujie Si University of Toronto |