This paper presents a scalable path- and context-sensitive data dependence analysis. The key is to address the aliasing-path-explosion problem when enforcing a path-sensitive memory model. Specifically, our approach decomposes the computational efforts of disjunctive reasoning into 1) a context- and semi-path-sensitive analysis that concisely summarizes data dependence as the symbolic and storeless value-flow graphs, and 2) a demand-driven phase that resolves transitive data dependence over the graphs, piggybacking the computation of fully path-sensitive pointer information with the resolution of data dependence of interest. We have applied the approach to two clients, namely thin slicing and value-flow bug finding. Using a suite of 16 C / C + + programs ranging from 13 KLoC to 8 MLoC, we compare our techniques against a diverse group of state-of-the-art analyses, illustrating the significant precision and scalability advantages of our approach.

Value-flow analysis is a fundamental technique in program analysis, benefiting various clients, such as memory corruption detection and taint analysis. However, existing efforts suffer from the low potential speedup that leads to a deficiency in scalability. In this work, we present a parallel algorithm Octopus to collect path conditions for realizable paths efficiently. Octopus builds on the realizability decomposition to collect the intraprocedural path conditions of different functions simultaneously on-demand and obtain realizable path conditions by concatenation, which achieves a high potential speedup in parallelization. We implement Octopus as a tool and evaluate it over 15 real-world programs. The experiment shows that Octopus significantly outperforms the state-of-the-art algorithms. Particularly, it detects NULL-pointer-dereference bugs for the project llvm with 6.3 MLoC within 6.9 minutes under the 40-thread setting. We also state and prove several theorems to demonstrate the soundness, completeness, and high potential speedup of Octopus . Our empirical and theoretical results demonstrate the great potential of Octopus in supporting various program analysis clients. The implementation has officially deployed at Ant Group, scaling the nightly code scan for massive FinTech applications.

Containers are ubiquitous data structures that support a variety of manipulations on the elements, inducing the indirect value flows in the program. Tracking value flows through containers is stunningly difficult, because it depends on container memory layouts, which are expensive to be discovered. This work presents a fast and precise value-flow analysis framework called Anchor for the programs using containers. We introduce the notion of anchored containers and propose the memory orientation analysis to construct a precise value-flow graph. Specifically, we establish a combined domain to identify anchored containers and apply strong updates to container memory layouts. Anchor finally conducts a demand-driven reachability analysis in the value-flow graph for a client. Experiments show that it removes 17.1% spurious statements from thin slices and discovers 20 null pointer exceptions with 9.1% as its false-positive ratio, while the smashing-based analysis reports 66.7% false positives. Anchor scales to millions of lines of code and checks the program with around 5.12 MLoC within 5 hours.

The static detection of divide-by-zero, a common programming error, is particularly prone to false positives because conventional static analysis reports a divide-by-zero bug whenever it cannot prove the safety property --- the divisor variable is not zero in all executions. When reasoning the program semantics over a large number of under-constrained variables, conventional static analyses significantly loose the bounds of divisor variables, which easily fails the safety proof and leads to a massive number of false positives. We propose a static analysis to detect divide-by-zero bugs taking additional evidence for under-constrained variables into consideration. Based on an extensive empirical study of known divide-by-zero bugs, we no longer arbitrarily report a bug once the safety verification fails. Instead, we actively look for affirmative evidences, namely source evidence and bound evidence, that imply a high possibility of the bug to be triggerable at runtime. When applying our tool Wit to the real-world software such as the Linux kernel, we have found 72 new divide-by-zero bugs with a low false positive rate of 22%.

Detecting memory leak at industrial scale is still not well addressed, in spite of the tremendous effort from both industry and academia in the past decades. Existing work suffers from an unresolved paradox - a highly precise analysis limits its scalability and an imprecise one seriously hurts its precision or recall. In this work, we present SMOKE, a staged approach to resolve this paradox. In the ?rst stage, instead of using a uniform precise analysis for all paths, we use a scalable but imprecise analysis to compute a succinct set of candidate memory leak paths. In the second stage, we leverage a more precise analysis to verify the feasibility of those candidates. The ?rst stage is scalable, due to the design of a new sparse program representation, the use-?ow graph (UFG), that models the problem as a polynomial-time state analysis. The second stage analysis is both precise and ef?cient, due to the smaller number of candidates and the design of a dedicated constraint solver. Experimental results show that SMOKE can ?nish checking industrial-sized projects, up to 8MLoC, in forty minutes with an average false positive rate of 24.4%. Besides, SMOKE is signi?cantly faster than the state-of-the-art research techniques as well as the industrial tools, with the speedup ranging from 5.2X to 22.8X. In the twenty-nine mature and extensively checked benchmark projects, SMOKE has discovered thirty previously unknown memory leaks which were con?rmed by developers, and one even assigned a CVE ID.

When dealing with millions of lines of code, we still cannot have the cake and eat it: sparse value-flow analysis is powerful in checking source-sink problems, but existing work cannot escape from the “pointer trap” – a precise points-to analysis limits its scalability and an imprecise one seriously undermines its precision. We present Pinpoint, a holistic approach that decomposes the cost of high-precision points-to analysis by precisely discovering local data dependence and delaying the expensive inter-procedural analysis through memorization. Such memorization enables the on-demand slicing of only the necessary inter-procedural data dependence and path feasibility queries, which are then solved by a costly SMT solver. Experiments show that Pinpoint can check programs such as MySQL (around 2 million lines of code) within 1.5 hours. The overall false positive rate is also very low (14.3% - 23.6%). Pinpoint has discovered over forty real bugs in mature and extensively checked open source systems. And the implementation of Pinpoint and all experimental results are freely available.

Pointer information, indispensable for static analysis tools, is expensive to compute and query. We provide a query-efficient persistence technique, Pestrie, to mitigate the costly computation and slow querying of precise pointer information. Leveraging equivalence and hub properties, Pestrie can compress pointer information and answers pointer related queries very efficiently. The experiment shows that Pestrie produces 10.5X and 17.5X smaller persistent files than the traditional bitmap and BDD encodings. Meanwhile, Pestrie is 2.9X to 123.6X faster than traditional demand-driven approaches for serving points-to related queries.

Predictive trace analysis (PTA) of concurrent programs is powerful in finding concurrency bugs unseen in past program executions. Unfortunately, existing PTA solutions face considerable challenges in scaling to large traces. In this article, we identify that a large percentage of events in the trace are redundant for presenting useful analysis results to the end user. Removing them from the trace can significantly improve the scalability of PTA without affecting the quality of the results. We present a trace redundancy theorem that specifies a redundancy criterion and the soundness guarantee that the PTA results are preserved after removing the redundancy. Based on this criterion, we design and implement TraceFilter, an efficient algorithm that automatically removes redundant events from a trace for the PTA of general concurrency access anomalies. We evaluated TraceFilter on a set of popular concurrent benchmarks as well as real world large server programs. Our experimental results show that TraceFilter is able to significantly improve the scalability of PTA by orders of magnitude, without impairing the analysis result.

Deterministic replay remains as one of the most effective ways to comprehend concurrent bugs. Existing approaches either maintain the exact shared read-write linkages with a large runtime overhead or use exponential off-line algorithms to search for a feasible interleaved execution. In this paper, we propose Stride, a hybrid solution that records the bounded shared memory access linkages at runtime and infers an equivalent interleaving in polynomial time, under the sequential consistency assumption. The recording scheme eliminates the need for synchronizing the shared read operations, which results in a significant overhead reduction. Comparing to the previous state-of-the-art approach of deterministic replay, Stride reduces, on average, 2.5 times of runtime overhead and produces, on average, 3.88 times smaller logs.

Analyzing the runtime behaviors of the data structures is important because they usually relate to the obscured program performance and understanding issues. The runtime evolution history of data structures creates the possibility of building a lightweight and non-checkpointing based solution for the backward analysis for validating and mining both the temporal and stationary properties of the data structure. We design and implement TAEDS, a framework that focuses on gathering the data evolution history of a program at the runtime and provides a virtual machine for programmers to examine the behavior of data structures back in time. We show that our approach facilitates many programming tasks such as diagnosing memory problems and improving the design of the data structures themselves.