pith. sign in

arxiv: 1907.06522 · v1 · pith:N76I4RN2new · submitted 2019-07-15 · 💻 cs.PL

A Relational Static Semantics for Call Graph Construction

Xilong Zhuo , Chenyi Zhang This is my paper

Pith reviewed 2026-05-24 21:06 UTC · model grok-4.3

classification 💻 cs.PL
keywords type flow analysiscall graph constructionpoints-to analysisstatic semanticsvirtual method resolutionobject-oriented languagesclass reachabilityrelational analysis
0
0 comments X

The pith

Type flow analysis using relations matches points-to precision on class reachability to variables without a heap abstraction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces type flow analysis to address the challenge of resolving virtual method and interface calls in object-oriented programs. It models the propagation of type information between variables through a set of relations rather than constructing a heap abstraction. The central result is a proof that this relational method yields the same precision as points-to analysis when determining which classes can reach a given variable. Experiments indicate lower time and space costs in practice. Accurate reachability information supports construction of call graphs needed for downstream program analyses.

Core claim

Type flow analysis represents propagation of type information between program variables by a group of relations without the help of a heap abstraction. Regarding the precision on reachability of class information to a variable, this method produces results equivalent to that one can derive from a points-to analysis.

What carries the argument

Type flow analysis, a relational static semantics that tracks type propagation between variables to support call graph construction.

If this is right

  • Equivalent precision on reachability of class information to a variable compared with points-to analysis.
  • Lower time and space usage for call graph construction in practice.
  • Handling of programs with high levels of class inheritance and polymorphism through relational propagation rules.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The relational model may allow simpler incremental updates when the program changes.
  • Extending the relations to capture additional language features could preserve the equivalence result.
  • The approach might integrate with existing static analysis frameworks by replacing heap-based components.

Load-bearing premise

The relational semantics without heap abstraction captures all type flows that matter for class reachability under the language model used in the proof.

What would settle it

A program example where the type flow analysis misses a class reaching a variable that a points-to analysis identifies because of flows introduced by heap operations outside the modeled language semantics.

Figures

Figures reproduced from arXiv: 1907.06522 by Chenyi Zhang, Xilong Zhuo.

Figure 1
Figure 1. Figure 1: An example that compares precision on type flow in a program. Statement VTA fact A x = new A() x ← A B b = new B() b ← B A y = new A() y ← A C c = new C() c ← C x.f = b A.f ← b y.f = c A.f ← c A.m.this ← x z = x.m() A.m.return ← A.f z ← A.m.return [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: VTA facts on the example A.m.this z O1 : A O2 : B x O3 : A O4 : C y m f f f [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Type Flow Analysis for variable z in the example in the ellipses in [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Abstract syntax for the core language. In this simple language we do not model common types (e.g., int and float) that are irrelevant to our analysis, and we focus on the reference types which form a class hierarchical structure. Similar to Variable Type Analysis (VTA), we assume a context insensitive setting, such that every variable can be uniquely determined by its name together with its enclosing class… view at source ↗
Figure 6
Figure 6. Figure 6: Constraints for points-to analysis. have the same smallest model for all methods, then at each call site x = y.m(a) both analyses will assign y the same set of classes and thus resolve the call site to the same set of method definitions, and as a consequence, each method body will be given the same set of extra conditions, thus all methods will have the same initial condition for the next round iteration. … view at source ↗
Figure 7
Figure 7. Figure 7: Runtime cost with different analysis RQ 1: How efficient is our approach compared with the traditional class hierar￾chy analysis and points-to analysis? RQ 2: How accurate is the result of our approach when comparing with the other analyses? RQ 3: Does our optimization (or minimization) algorithm achieve significantly reduce storage consumption? 4.1 RQ1: Efficiency To answer the first research question, we… view at source ↗
Figure 8
Figure 8. Figure 8: Call sites generated by different analyses the table in [PITH_FULL_IMAGE:figures/full_fig_p010_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Optimization result after optimization process. Besides, time consumption is another factor that we consider. The results are shown in the table in [PITH_FULL_IMAGE:figures/full_fig_p011_9.png] view at source ↗
read the original abstract

The problem of resolving virtual method and interface calls in object-oriented languages has been a long standing challenge to the program analysis community. The complexities are due to various reasons, such as increased levels of class inheritance and polymorphism in large programs. In this paper, we propose a new approach called type flow analysis that represent propagation of type information between program variables by a group of relations without the help of a heap abstraction. We prove that regarding the precision on reachability of class information to a variable, our method produces results equivalent to that one can derive from a points-to analysis. Moreover, in practice, our method consumes lower time and space usage, as supported by the experimental results.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper proposes a relational type flow analysis for call graph construction in object-oriented languages. Type propagation between variables is modeled via a group of relations without any heap abstraction. The central claim is a proof that this yields identical precision to a points-to analysis on the reachability of class information to variables; the paper also reports lower time and space consumption in experiments.

Significance. If the equivalence holds inside the modeled language, the relational approach supplies a heap-free route to the same class-reachability precision that points-to analyses achieve, which would be a useful engineering contribution for scalable static analysis. The absence of heap abstraction and the claimed parameter-free character of the relations are concrete strengths that would be worth preserving in any revision.

major comments (1)
  1. [Proof of equivalence (formal development following the abstract)] The equivalence proof (abstract and the formal development that follows it) is scoped to the paper's language semantics. The load-bearing assumption is that every type flow relevant to class reachability is already captured by the relational rules under that semantics. The manuscript must explicitly enumerate the language features modeled (e.g., whether reflection, dynamic proxies, array aliasing, or certain interface dispatch patterns are included) and either extend the proof or state the conditions under which the equivalence would fail outside the model.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive comment on the scope of our equivalence result. We address it point-by-point below and will revise the manuscript to make the language assumptions explicit.

read point-by-point responses

  1. Referee: The equivalence proof (abstract and the formal development that follows it) is scoped to the paper's language semantics. The load-bearing assumption is that every type flow relevant to class reachability is already captured by the relational rules under that semantics. The manuscript must explicitly enumerate the language features modeled (e.g., whether reflection, dynamic proxies, array aliasing, or certain interface dispatch patterns are included) and either extend the proof or state the conditions under which the equivalence would fail outside the model.

    Authors: We agree that the equivalence is proven only for the language semantics defined in Sections 2–4. The modeled language includes single inheritance, interfaces, virtual dispatch, and basic field/array accesses but excludes reflection, dynamic proxies, native methods, and complex aliasing patterns arising from array stores. We will add a dedicated paragraph (new Section 2.3) that enumerates these features and states the precise conditions under which the relational rules capture all relevant type flows. Outside this model the equivalence does not necessarily hold; extending the proof would require additional relational rules for the omitted features. revision: yes

Circularity Check

0 steps flagged

No circularity; formal equivalence proof is self-contained within defined semantics

full rationale

The paper defines a relational type-flow analysis independently of points-to analysis and states a formal proof of equivalence on class-reachability precision inside its language model. No self-definitional equations, fitted inputs renamed as predictions, or load-bearing self-citations appear in the derivation chain. The equivalence is established directly rather than by construction from the baseline or prior author results, so the central claim does not reduce to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities are visible beyond the standard assumption that program semantics can be modeled by relations on types.

pith-pipeline@v0.9.0 · 5630 in / 1053 out tokens · 16471 ms · 2026-05-24T21:06:07.761747+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages

  1. [1]

    https://sable.github.io/soot/

    Soot. https://sable.github.io/soot/. Accessed: 2019-06-10

    work page 2019

  2. [2]

    https://www.spec.org/jvm2008/

    Specjvm2008. https://www.spec.org/jvm2008/. Accessed: 2019-06-18

    work page 2019

  3. [3]

    L. O. Andersen. Program analysis and specialization for the C programming lan- guage. PhD thesis, DIKU, University of Copenhagen, May 1994

    work page 1994

  4. [4]

    Bacon and Peter F

    David F. Bacon and Peter F. Sweeney. Fast static analysis of c++ virtual function calls. In Proceedings of the 11th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications , OOPSLA ’96, pages 324– 341, 1996

    work page 1996

  5. [5]

    Blackburn, Robin Garner, Chris Hoffmann, Asjad M

    Stephen M. Blackburn, Robin Garner, Chris Hoffmann, Asjad M. Khang, Kathryn S. McKinley, Rotem Bentzur, Amer Diwan, Daniel Feinberg, Daniel Frampton, Samuel Z. Guyer, Martin Hirzel, Antony Hosking, Maria Jump, Han Lee, J. Eliot B. Moss, Aashish Phansalkar, Darko Stefanovi´ c, Thomas VanDrunen, Daniel von Dincklage, and Ben Wiedermann. The DaCapo Benchmarks...

    work page 2006

  6. [6]

    Optimization of object-oriented programs using static class hierarchy analysis

    Jeffrey Dean, David Grove, and Craig Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In Proceedings of the 9th European Conference on Object-Oriented Programming, ECOOP ’95, pages 77–101, 1995

    work page 1995

  7. [7]

    Fern´ andez

    Mary F. Fern´ andez. Simple and effective link-time optimization of modula-3 pro- grams. In Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation , PLDI ’95, pages 103–115, 1995

    work page 1995

  8. [8]

    Call graph con- struction in object-oriented languages

    David Grove, Greg DeFouw, Jeffrey Dean, and Craig Chambers. Call graph con- struction in object-oriented languages. In Proceedings of the 12th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applica- tions, OOPSLA ’97, pages 108–124, 1997

    work page 1997

  9. [9]

    P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation , 86:43–68, 1990

    work page 1990

  10. [10]

    Hybrid context-sensitivity for points-to analysis

    George Kastrinis and Yannis Smaragdakis. Hybrid context-sensitivity for points-to analysis. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI ’13, pages 423–434, 2013

    work page 2013

  11. [11]

    Scaling java points-to analysis using spark

    Ondˇ rej Lhot´ ak and Laurie Hendren. Scaling java points-to analysis using spark. In Proceedings of the 12th International Conference on Compiler Construction , CC’03, pages 153–169, 2003

    work page 2003

  12. [12]

    Ana Milanova, Atanas Rountev, and Barbara G. Ryder. Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol. , 14(1):1–41, January 2005

    work page 2005

  13. [13]

    Paige and R

    R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16:973–989, 1987

    work page 1987

  14. [14]

    Call graph construction for java libraries

    Michael Reif, Michael Eichberg, Ben Hermann, Johannes Lerch, and Mira Mezini. Call graph construction for java libraries. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering , FSE 2016, pages 474–486, 2016

    work page 2016

  15. [15]

    Control-flow Analysis of Higher-order Languages or Taming Lambda

    Olin Grigsby Shivers. Control-flow Analysis of Higher-order Languages or Taming Lambda. PhD thesis, 1991

    work page 1991

  16. [16]

    Pick your contexts well: understanding object-sensitivity

    Yannis Smaragdakis, Martin Bravenboer, and Ondrej Lhot´ ak. Pick your contexts well: understanding object-sensitivity. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL ’11, pages 17–30, 2011

    work page 2011

  17. [17]

    Refinement-based context-sensitive points- to analysis for java

    Manu Sridharan and Rastislav Bod´ ık. Refinement-based context-sensitive points- to analysis for java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI ’06, pages 387–400, 2006

    work page 2006

  18. [18]

    Practical virtual method call resolution for java

    Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vall´ ee-Rai, Patrick Lam, Etienne Gagnon, and Charles Godin. Practical virtual method call resolution for java. In Proceedings of the 15th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications , OOPSLA ’00, pages 264–280, 2000

    work page 2000

  19. [19]

    Making k-object-sensitive pointer analysis more precise with still k-limiting

    Tian Tan, Yue Li, and Jingling Xue. Making k-object-sensitive pointer analysis more precise with still k-limiting. In International Static Analysis Symposium, SAS’16, 2016

    work page 2016

  20. [20]

    R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1:146–160, 1972

    work page 1972

  21. [21]

    Scalable propagation-based call graph construction algorithms

    Frank Tip and Jens Palsberg. Scalable propagation-based call graph construction algorithms. In Proceedings of the 15th ACM SIGPLAN Conference on Object- oriented Programming, Systems, Languages, and Applications, OOPSLA ’00, pages 281–293, 2000

    work page 2000