arXiv subjects

Uday P. Khedker

Publications and source records attributed to Uday P. Khedker.

15 recordsLinked to original sources

arXiv2026

Points-to Analysis Using MDE: A Multi-level Deduplication Engine for Repetitive Data and Operations

Precise pointer analysis is a foundational component of many client analyses and optimizations. Scaling flow- and context-sensitive pointer analysis has been a long-standing challenge, suffering from combinatorial growth in both memory usage and runtime. Existing approaches address this primarily by reducing the amount of information tracked often, at the cost of precision and soundness. In our experience a significant proportion of this cost comes from propagation of duplicate data and low-level data structure operations being repeated a large number of times. Our measurements on SPEC benchmarks show that more than 90% of all set-union operations performed can be redundant. We present Multi-level Deduplication Engine (MDE), a mechanism that recursively augments the representation of data through de-duplication and the assignment of unique identifiers to values to eliminate redundancy. This allows MDE to trivialize many operations, and memoize operations enabling their future reuse. MDE's recursive structure allows it to represent de-duplicated values that themselves are constructed from other de-deuplicated values, capturing structural redundancy not easily possible with non-recursive techniques. We provide a full C++ implementation of MDE as a library and integrate it into an existing implementation of a flow- and context-sensitive pointer analysis. Evaluation on selected SPEC benchmarks shows a reduction up to 18.10x in peak memory usage and 8.15x in runtime. More notably, MDE exhibits an upward trend of effectiveness with the increase in benchmark size. Besides performance improvements, this work highlights the importance of representation design and suggests new opportunities for bringing efficiency to future analyses.

cs.PL↗

arXiv2025

LatticeHashForest: An Efficient Data Structure for Repetitive Data and Operations

Analysis of entire programs as a single unit, or whole-program analysis, involves propagation of large amounts of information through the control flow of the program. This is especially true for pointer analysis, where, unless significant compromises are made in the precision of the analysis, there is a combinatorial blowup of information. One of the key problems we observed in our own efforts to this end is that a lot of duplicate data was being propagated, and many low-level data structure operations were repeated a large number of times. We present what we consider to be a novel and generic data structure, LatticeHashForest (LHF), to store and operate on such data in a manner that eliminates a majority of redundant computations and duplicate data in scenarios similar to those encountered in compilers and program optimization. LHF differs from similar work in this vein, such as hash-consing, ZDDs, and BDDs, by not only providing a way to efficiently operate on large, aggregate structures, but also modifying the elements of such structures in a manner that they can be deduplicated immediately. LHF also provides a way to perform a nested construction of elements such that they can be deduplicated at multiple levels, cutting down the need for additional, nested computations. We provide a detailed structural description, along with an abstract model of this data structure. An entire C++ implementation of LHF is provided as an artifact along with evaluations of LHF using examples and benchmark programs. We also supply API documentation and a user manual for users to make independent applications of LHF. Our main use case in the realm of pointer analysis shows memory usage reduction to an almost negligible fraction, and speedups beyond 4x for input sizes approaching 10 million when compared to other implementations.

cs.DS↗

arXiv2024

Which Part of the Heap is Useful? Improving Heap Liveness Analysis

With the growing sizes of data structures allocated in heap, understanding the actual use of heap memory is critically important for minimizing cache misses and reclaiming unused memory. A static analysis aimed at this is difficult because the heap locations are unnamed. Using allocation sites to name them creates very few distinctions making it difficult to identify allocated heap locations that are not used. Heap liveness analysis using access graphs solves this problem by (a) using a storeless model of heap memory by naming the locations with access paths, and (b) representing the unbounded sets of access paths (which are regular languages) as finite automata. We improve the scalability and efficiency of heap liveness analysis, and reduce the amount of computed heap liveness information by using deterministic automata and by minimizing the inclusion of aliased access paths in the language. Practically, our field-, flow-, context-sensitive liveness analysis on SPEC CPU2006 benchmarks scales to 36 kLoC (existing analysis scales to 10.5 kLoC) and improves efficiency even up to 99%. For some of the benchmarks, our technique shows multifold reduction in the computed liveness information, ranging from 2 to 100 times (in terms of the number of live access paths), without compromising on soundness.

cs.PL↗

arXiv2023

SpComp: A Sparsity Structure-Specific Compilation of Matrix Operations

Sparse matrix operations involve a large number of zero operands which makes most of the operations redundant. The amount of redundancy magnifies when a matrix operation repeatedly executes on sparse data. Optimizing matrix operations for sparsity involves either reorganization of data or reorganization of computations, performed either at compile-time or run-time. Although compile-time techniques avert from introducing run-time overhead, their application either is limited to simple sparse matrix operations generating dense output and handling immutable sparse matrices or requires manual intervention to customize the technique to different matrix operations. We contribute a compile time technique called SpComp that optimizes a sparse matrix operation by automatically customizing its computations to the positions of non-zero values of the data. Our approach neither incurs any run-time overhead nor requires any manual intervention. It is also applicable to complex matrix operations generating sparse output and handling mutable sparse matrices. We introduce a data-flow analysis, named Essential Indices Analysis, that statically collects the symbolic information about the computations and helps the code generator to reorganize the computations. The generated code includes piecewise-regular loops, free from indirect references and amenable to further optimization. We see a substantial performance gain by SpComp-generated SpMSpV code when compared against the state-of-the-art TACO compiler and piecewise-regular code generator. On average, we achieve 79% performance gain against TACO and 83% performance gain against the piecewise-regular code generator. When compared against the CHOLMOD library, SpComp generated sparse Cholesky decomposition code showcases 65% performance gain on average.

cs.MS↗

arXiv2018

Demand-driven Alias Analysis : Formalizing Bidirectional Analyses for Soundness and Precision

A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive approach computes all information in anticipation of it being used later. However, for a given set of demands, demand-driven methods are believed to compute the same information that would be computed by the corresponding exhaustive methods. We investigate the precision and bidirectional nature of demand-driven methods and show that: (a) demand-driven methods can be formalized inherently as bidirectional data flow analysis because the demands are propagated against the control flow and the information to satisfy the demands is propagated along the control flow. We extend the formalization of the Meet Over Paths solution to bidirectional flows. This formalization helps us to prove the soundness and precision of our analysis, and (b) since a demand-driven method computes only the required information to meet a demand, it should be able to reduce the imprecision caused by data abstractions and hence should be more precise than an exhaustive method. We show that while this is indeed the case with Java, for C/C++, the precision critically hinges on how indirect assignments are handled. We use this insight and propose a demand-driven alias analysis that is more precise than an exhaustive analysis for C/C++ too. We have chosen devirtualization as an application. Our measurements show that our method is not only more efficient but more precise than the existing demand-driven method, as well as the corresponding exhaustive method.

cs.PL↗

arXiv2018

Generalized Points-to Graphs: A New Abstraction of Memory in the Presence of Pointers

Flow- and context-sensitive points-to analysis is difficult to scale; for top-down approaches, the problem centers on repeated analysis of the same procedure; for bottom-up approaches, the abstractions used to represent procedure summaries have not scaled while preserving precision. We propose a novel abstraction called the Generalized Points-to Graph (GPG) which views points-to relations as memory updates and generalizes them using the counts of indirection levels leaving the unknown pointees implicit. This allows us to construct GPGs as compact representations of bottom-up procedure summaries in terms of memory updates and control flow between them. Their compactness is ensured by the following optimizations: strength reduction reduces the indirection levels, redundancy elimination removes redundant memory updates and minimizes control flow (without over-approximating data dependence between memory updates), and call inlining enhances the opportunities of these optimizations. We devise novel operations and data flow analyses for these optimizations. Our quest for scalability of points-to analysis leads to the following insight: The real killer of scalability in program analysis is not the amount of data but the amount of control flow that it may be subjected to in search of precision. The effectiveness of GPGs lies in the fact that they discard as much control flow as possible without losing precision (i.e., by preserving data dependence without over-approximation). This is the reason why the GPGs are very small even for main procedures that contain the effect of the entire program. This allows our implementation to scale to 158kLoC for C programs.

cs.PL↗

arXiv2017

Scaling Bounded Model Checking By Transforming Programs With Arrays

Bounded Model Checking is one the most successful techniques for finding bugs in program. However, model checkers are resource hungry and are often unable to verify programs with loops iterating over large arrays.We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating (ANSI-C) program to an array-free and loop-free (ANSI-C) program thereby reducing the resource requirements of a model checker significantly. Model checking of the transformed program using an off-the-shelf bounded model checker simulates the loop iterations efficiently. Thus, our transformed program is a sound abstraction of the original program and is also precise in a large number of cases - we formally characterize the class of programs for which it is guaranteed to be precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.

cs.LO↗

arXiv2016

Scaling Bounded Model Checking By Transforming Programs With Arrays

Bounded Model Checking is one the most successful techniques for finding bugs in program. However, for programs with loops iterating over large-sized arrays, bounded model checkers often exceed the limit of resources available to them. We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating program in ANSI-C to an array-free and loop-free program. The transformed program can efficiently be verified by an off-the-shelf bounded model checker. Though the transformed program is, in general, an abstraction of the original program, we formally characterize the properties for which the transformation is precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.

cs.PL↗

arXiv2016

Flow- and Context-Sensitive Points-to Analysis using Generalized Points-to Graphs

Computing precise (fully flow-sensitive and context-sensitive) and exhaustive points-to information is computationally expensive. Many practical tools approximate the points-to information trading precision for efficiency. This has adverse impact on computationally intensive analyses such as model checking. Past explorations in top-down approaches of fully flow- and context-sensitive points-to analysis (FCPA) have not scaled. We explore the alternative of bottom-up interprocedural approach which constructs summary flow functions for procedures to represent the effect of their calls. This approach has been effectively used for many analyses. However, it is computationally expensive for FCPA which requires modelling unknown locations accessed indirectly through pointers. Such accesses are commonly handled by using placeholders to explicate unknown locations or by using multiple call-specific summary flow functions. We generalize the concept of points-to relations by using the counts of indirection levels leaving the unknown locations implicit. This allows us to create summary flow functions in the form of generalized points-to graphs (GPGs) without the need of placeholders. By design, GPGs represent both memory (in terms of classical points-to facts) and memory transformers (in terms of generalized points-to facts). We perform FCPA by progressively reducing generalized points-to facts to classical points-to facts. GPGs distinguish between may and must pointer updates thereby facilitating strong updates within calling contexts. The size of GPG is linearly bounded by the number of variables and is independent of the number of statements in the procedure. Empirical measurements on SPEC benchmarks show that GPGs are indeed compact in spite of large procedure sizes. This allows us to scale FCPA to 158 kLoC using GPGs (compared to 35 kLoC reported by liveness-based FCPA).

cs.PL↗

arXiv2015

Heap Abstractions for Static Analysis

Heap data is potentially unbounded and seemingly arbitrary. As a consequence, unlike stack and static memory, heap memory cannot be abstracted directly in terms of a fixed set of source variable names appearing in the program being analysed. This makes it an interesting topic of study and there is an abundance of literature employing heap abstractions. Although most studies have addressed similar concerns, their formulations and formalisms often seem dissimilar and some times even unrelated. Thus, the insights gained in one description of heap abstraction may not directly carry over to some other description. This survey is a result of our quest for a unifying theme in the existing descriptions of heap abstractions. In particular, our interest lies in the abstractions and not in the algorithms that construct them. In our search of a unified theme, we view a heap abstraction as consisting of two features: a heap model to represent the heap memory and a summarization technique for bounding the heap representation. We classify the models as storeless, store based, and hybrid. We describe various summarization techniques based on k-limiting, allocation sites, patterns, variables, other generic instrumentation predicates, and higher-order logics. This approach allows us to compare the insights of a large number of seemingly dissimilar heap abstractions and also paves way for creating new abstractions by mix-and-match of models and summarization techniques.

cs.PL↗

arXiv2014

Buffer Overflow Analysis for C

Buffer overflow detection and mitigation for C programs has been an important concern for a long time. This paper defines a string buffer overflow analysis for C programs. The key ideas of our formulation are (a) separating buffers from the pointers that point to them, (b) modelling buffers in terms of sizes and sets of positions of null characters, and (c) defining stateless functions to compute the sets of null positions and mappings between buffers and pointers. This exercise has been carried out to test the feasibility of describing such an analysis in terms of lattice valued functions and relations to facilitate automatic construction of an analyser without the user having to write C/C++/Java code. This is facilitated by devising stateless formulations because stateful formulations combine features through side effects in states raising a natural requirement of C/C++/Java code to be written to describe them. Given the above motivation, the focus of this paper is not to build good static approximations for buffer overflow analysis but to show how given static approximations could be formalized in terms of stateless formulations so that they become amenable to automatic construction of analysers.

cs.PL↗

arXiv2014

Generalizing the Liveness Based Points-to Analysis

The original liveness based flow and context sensitive points-to analysis (LFCPA) is restricted to scalar pointer variables and scalar pointees on stack and static memory. In this paper, we extend it to support heap memory and pointer expressions involving structures, unions, arrays, and pointer arithmetic. The key idea behind these extensions involves constructing bounded names for locations in terms of compile time constants (names and fixed offsets), and introducing sound approximations when it is not possible to do so. We achieve this by defining a grammar for pointer expressions, suitable memory models and location naming conventions, and some key evaluations of pointer expressions that compute the named locations. These extensions preserve the spirit of the original LFCPA which is evidenced by the fact that although the lattices and flow functions change, the overall data flow equations remain unchanged.

cs.PL↗

arXiv2013

Interprocedural Data Flow Analysis in Soot using Value Contexts

An interprocedural analysis is precise if it is flow sensitive and fully context-sensitive even in the presence of recursion. Many methods of interprocedural analysis sacrifice precision for scalability while some are precise but limited to only a certain class of problems. Soot currently supports interprocedural analysis of Java programs using graph reachability. However, this approach is restricted to IFDS/IDE problems, and is not suitable for general data flow frameworks such as heap reference analysis and points-to analysis which have non-distributive flow functions. We describe a general-purpose interprocedural analysis framework for Soot using data flow values for context-sensitivity. This framework is not restricted to problems with distributive flow functions, although the lattice must be finite. It combines the key ideas of the tabulation method of the functional approach and the technique of value-based termination of call string construction. The efficiency and precision of interprocedural analyses is heavily affected by the precision of the underlying call graph. This is especially important for object-oriented languages like Java where virtual method invocations cause an explosion of spurious call edges if the call graph is constructed naively. We have instantiated our framework with a flow and context-sensitive points-to analysis in Soot, which enables the construction of call graphs that are far more precise than those constructed by Soot's SPARK engine.

cs.PL↗

arXiv2012

A Logic for Correlating Temporal Properties across Program Transformations

Program transformations are widely used in synthesis, optimization, and maintenance of software. Correctness of program transformations depends on preservation of some important properties of the input program. By regarding programs as Kripke structures, many interesting properties of programs can be expressed in temporal logics. In temporal logic, a formula is interpreted on a single program. However, to prove correctness of transformations, we encounter formulae which contain some subformulae interpreted on the input program and some on the transformed program. An example where such a situation arises is verification of optimizing program transformations applied by compilers. In this paper, we present a logic called Temporal Transformation Logic (TTL) to reason about such formulae. We consider different types of primitive transformations and present TTL inference rules for them. Our definitions of program transformations and temporal logic operators are novel in their use of the boolean matrix algebra. This results in specifications that are succinct and constructive. Further, we use the boolean matrix algebra in a uniform manner to prove soundness of the TTL inference rules.

cs.LO↗

arXiv2011

Lazy Pointer Analysis

Flow- and context-sensitive pointer analysis is generally considered too expensive for large programs; most tools relax one or both of the requirements for scalability. We formulate a flow- and context-sensitive points-to analysis that is lazy in the following sense: points-to information is computed only for live pointers and its propagation is sparse (restricted to live ranges of respective pointers). Further, our analysis (a) uses strong liveness, effectively including dead code elimination; (b) afterwards calculates must-points-to information from may-points-to information instead of using a mutual fixed-point; and (c) uses value-based termination of call strings during interprocedural analysis (which reduces the number of call strings significantly). A naive implementation of our analysis within GCC-4.6.0 gave analysis time and size of points-to measurements for SPEC2006. Using liveness reduced the amount of points-to information by an order of magnitude with no loss of precision. For all programs under 30kLoC we found that the results were much more precise than gcc's analysis. What comes as a pleasant surprise however, is the fact that below this cross-over point, our naive linked-list implementation is faster than a flow- and context-insensitive analysis which is primarily used for efficiency. We speculate that lazy flow- and context-sensitive analyses may be not only more precise, but also more efficient, than current approaches.

cs.PL↗