CFA2: A Context-Free Approach to Control-Flow Analysis

In a functional language, the dominant control-flow mechanism is function call and return. Most higher-order flow analyses, including k-CFA, do not handle call and return well: they remember only a bounded number of pending calls because they approximate programs with control-flow graphs. Call/return mismatch introduces precision-degrading spurious control-flow paths and increases the analysis time. We describe CFA2, the first flow analysis with precise call/return matching in the presence of higher-order functions and tail calls. We formulate CFA2 as an abstract interpretation of programs in continuation passing style and describe a sound and complete summarization algorithm for our abstract semantics. A preliminary evaluation shows that CFA2 gives more accurate data-flow information than 0CFA and 1CFA.

• Publication year

  2010

• Venue

  European Symposium on Programming

• Publication date

  2010-03-20

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.2168/LMCS-7(2:3)2011arXiv 1102.3676
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Pushdown Control-Flow Analysis of Higher-Order Programs

  2010cited by this paper
• Control-flow analysis of function calls and returns by abstract interpretation

  2009cited by this paper
• Types and higher-order recursion schemes for verification of higher-order programs

  2009cited by this paper
• Snugglebug: a powerful approach to weakest preconditions

  2009cited by this paper
• Deciding kCFA is complete for EXPTIME

  2008cited by this paper
• Type-based flow analysis and context-free language reachability

  2008cited by this paper
• Subcubic algorithms for recursive state machines

  2008cited by this paper
• Environment Analysis of Higher-Order Languages

  2007cited by this paper
• Refinement-based context-sensitive points-to analysis for Java

  2006cited by this paper
• Improving flow analyses via ΓCFA: abstract garbage collection and counting

  2006cited by this paper
• Analysis of recursive state machines

  2005cited by this paper
• Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned

  2004cited by this paper
• RETROSPECTIVE : Orbit : An Optimizing Compiler for Scheme

  2002cited by this paper
• Model checking pushdown systems

  2002cited by this paper
• Type-base flow analysis: from polymorphic subtyping to CFL-reachability

  2001cited by this paper
• Pointer analysis: haven't we solved this problem yet?

  2001cited by this paper
• Constraint Abstractions

  2001cited by this paper
• Interconvertibility of a class of set constraints and context-free-language reachability

  2000influential reference
• Polymorphic splitting: an effective polyvariant flow analysis

  1998cited by this paper
• Interprocedural control flow analysis of first-order programs with tail-call optimization

  1997cited by this paper
• A direct symbolic approach to model checking pushdown systems

  1997cited by this paper
• Reachability Analysis of Pushdown Automata: Application to Model-Checking

  1997cited by this paper
• Flow analysis of typed higher-order programs

  1996cited by this paper
• Precise interprocedural dataflow analysis via graph reachability

  1995cited by this paper
• The Cartesian Product Algorithm: Simple and Precise Type Inference Of Parametric Polymorphism

  1995cited by this paper
• Lambda, the ultimate label or a simple optimizing compiler for Scheme

  1994cited by this paper
• The essence of compiling with continuations

  1993cited by this paper
• Set based program analysis

  1992cited by this paper
• Reasoning about programs in continuation-passing style

  1992cited by this paper
• Control-flow analysis of higher-order languages of taming lambda

  1991cited by this paper
• Graph-theoretic methods in database theory

  1990cited by this paper
• Orbit: an optimizing compiler for scheme

  1986cited by this paper
• Rabbit: A Compiler for Scheme

  1978cited by this paper

• Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages

  2025cites this paper
• Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis: A Case of Higher-Order Control-Flow Analysis

  2025cites this paper
• Call-Guarded Abstract Definitional Interpreters

  2025cites this paper
• A Pure Demand Operational Semantics with Applications to Program Analysis

  2023cites this paper
• Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence

  2023cites this paper
• Formalizing Path Explosion for Recursive Functions via Asymptotic Path Complexity

  2023cites this paper
• Analyzing binding extent in 3CPS

  2022influential citation
• Input splitting for cloud-based static application security testing platforms

  2022cites this paper
• DFI: An Interprocedural Value-Flow Analysis Framework that Scales to Large Codebases

  2022cites this paper
• Reachability types: tracking aliasing and separation in higher-order functional programs

  2021cites this paper
• 3CPS: The Design of an Environment-Focussed Intermediate Representation

  2021cites this paper
• Newly-single and loving it: improving higher-order must-alias analysis with heap fragments

  2021cites this paper
• Trace-based control-flow analysis

  2021influential citation
• Data flow refinement type inference

  2020cites this paper
• Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap

  2020cites this paper
• Type and Control-Flow Analysis for Scheme in Sturdy

  2020cites this paper
• A Set-Based Context Model for Program Analysis

  2020influential citation
• Abstracting Faceted Execution

  2020cites this paper
• A scalable, flow-and-context-sensitive taint analysis of android applications

  2019cites this paper
• Stack-Liberated Abstract Garbage Collection

  2019cites this paper
• Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings

  2019cites this paper
• Bar-Hillel Theorem Mechanization in Coq

  2019cites this paper
• Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science, Vol. 11541

  2019cites this paper
• Demand Control-Flow Analysis

  2019cites this paper
• Effect-Driven Flow Analysis

  2019cites this paper
• Relatively Complete Pushdown Analysis of Escape Continuations

  2019cites this paper
• Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems

  2019cites this paper
• Higher-order Demand-driven Program Analysis

  2019influential citation
• Staged abstract interpreters: fast and modular whole-program analysis via meta-programming

  2019cites this paper
• Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)

  2018cites this paper
• Abstracting Faceted Execution 1 : 3 Next

  2018cites this paper
• Abstract allocation as a unified approach to polyvariance in control-flow analyses

  2018cites this paper
• Refunctionalization of Abstract Abstract Machines (Functional Pearl)

  2018cites this paper
• Abstracting Faceted Execution Static Analysis of Dynamic Information-Flow Control for Higher-Order Languages

  2018cites this paper
• Introspective Polyvariance for Control-Flow Analyses

  2017cites this paper
• Cauliflower: a Solver Generator for Context-Free Language Reachability

  2017cites this paper
• A posteriori environment analysis with Pushdown Delta CFA

  2017influential citation
• Abstracting definitional interpreters (functional pearl)

  2017cites this paper
• Purity analysis for JavaScript through abstract interpretation

  2017cites this paper
• Relative Store Fragments for Singleton Abstraction

  2017cites this paper
• 19 : 2 Higher-Order Demand-Driven Program

  2016cites this paper
• Verification of message passing concurrent systems

  2016cites this paper
• Higher-Order Demand-Driven Program Analysis

  2016influential citation
• 1 Higher-Order Demand-Driven Program Analysis

  2016influential citation
• An Introduction to Redex with Abstracting Abstract Machines ( v 0 . 6 )

  2016cites this paper
• Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis

  2016cites this paper
• Higher-Order Demand-Driven Program Analysis ( draft )

  2016cites this paper
• Alternate Control-Flow Analyses for Defunctionalization in the MLton Compiler

  2016cites this paper
• H-CFA: a Simplified Approach for Pushdown Control Flow Analysis

  2016influential citation
• Automating Abstract Interpretation of Abstract Machines

  2015cites this paper
• Control Flow Analysis for SF Combinator Calculus

  2015cites this paper
• Ahead of Time Compilation of EcmaScript Code Using Type Inference

  2015cites this paper
• Pushdown control-flow analysis for free

  2015influential citation
• Towards a Scalable Framework for Context-Free Language Reachability

  2015cites this paper
• Techniques and tools for secure Web browser extension development

  2015cites this paper
• Control-Based Program Analysis

  2015influential citation
• PROCEEDINGS OF THE 2014 SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP

  2015cites this paper
• Control-flow analysis of dynamic languages via pointer analysis

  2015cites this paper
• Environment Unrolling

  2014cites this paper
• A Linear Encoding of Pushdown Control-Flow Analysis

  2014cites this paper
• A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join

  2014cites this paper
• Retargetting Legacy Browser Extensions to Modern Extension Frameworks

  2014influential citation
• Verifying higher-order programs with the dijkstra monad

  2013cites this paper
• Information Flow Analysis for a Dynamically Typed Language with Staged Metaprogramming

  2013cites this paper
• Efficient construction of approximate call graphs for JavaScript IDE services

  2013cites this paper
• Abstracting abstract control

  2013influential citation
• Correctly Optimizing Abstract Abstract Machines

  2013influential citation
• Pushdown Exception-Flow Analysis of Object-Oriented Programs

  2013cites this paper
• OOCFA2: a PDA-based higher-order flow analysis for object-oriented programs

  2013cites this paper
• Information flow analysis for a dynamically typed language with staged metaprogramming

  2013cites this paper
• JavaScript Code Quality Analysis

  2012cites this paper
• Correlation Tracking for Points-To Analysis of JavaScript

  2012cites this paper
• Monadic Refinement Types for Verifying JavaScript Programs

  2012cites this paper
• Towards JavaScript Verification with the Dijkstra State Monad

  2012cites this paper
• Introspective pushdown analysis of higher-order programs

  2012influential citation
• Analysis and Enforcement of Web Application Security Policies

  2012cites this paper
• Exact Flow Analysis by Higher-Order Model Checking

  2012influential citation
• Optimizing abstract abstract machines

  2012influential citation
• Higher-Order Model Checking: From Theory to Practice

  2011cites this paper
• Certifying assembly programs with trails

  2011cites this paper
• An Analytic Framework for JavaScript

  2011cites this paper
• Systematic abstraction of abstract machines

  2011cites this paper
• Beyond autocomplete: Automatic function definition

  2011cites this paper
• Automated Analysis of Security-Critical JavaScript APIs

  2011cites this paper
• Building-Blocks for Performance Oriented DSLs

  2011cites this paper
• Pushdown Abstractions of JavaScript

  2011influential citation
• Pushdown flow analysis of first-class control

  2011cites this paper
• Flow-sensitive type recovery in linear-log time

  2011cites this paper
• 2 An End-to-End System for Embedded Parallel DSLs

  2011cites this paper
• Flow-sensitive control-flow analysis in linear-log time

  2011cites this paper
• Stack-Summarizing Control-Flow Analysis of Higher-Order Programs

  2010cites this paper
• Flow-Sensitive Sub-Zero Control-Flow Analysis in Linear-Log Time

  2010cites this paper
• Pushdown Control-Flow Analysis of Higher-Order Programs

  2010influential citation
• Control-flow analysis of functional programs

  2007cites this paper
• Under Consideration for Publication in J. Functional Programming Pushdown Flow Analysis with Abstract Garbage Collection

  year unknowncites this paper