ABSTRACT. Static analyses predominantly use discrete modes of logical reasoning to derive facts about programs. Despite significant strides, this form of reasoning faces new challenges in modern software applications and practices. These challenges concern not only traditional analysis objectives such as scalability, accuracy, and soundness, but also emerging ones such as tailoring analysis conclusions based on relevance or severity of particular code changes, and needs of individual programmers.

We advocate seamlessly extending static analyses to leverage continuous modes of logical reasoning in order to address these challenges. Central to our approach is expressing the specification of the static analysis in a constraint language that is amenable to computing provenance information. We use the logic programming language Datalog as proof-of-concept for this purpose. We illustrate the benefits of exploiting provenance even in the discrete setting. Moreover, by associating weights with constraints, we show how to amplify these benefits in the continuous setting.

We also present open problems in aspects of analysis usability, language expressiveness, and solver techniques. The overall process constitutes a fundamental rethinking of how to design, implement, deploy, and adapt static analyses.

ABSTRACT. By distinguishing the fields of an object, Andersen's field-sensitive pointer analysis yields better precision than its field-insensitive counterpart. A typical field-sensitive solution to inclusion-based pointer analysis for C/C++ is to add positive weights to the edges in Andersen's constraint graph to model field access. However, the precise modeling is at the cost of introducing a new type of constraint cycles, called positive weight cycles (PWCs). A PWC, which contains at least one positive weight constraint, can cause infinite and redundant field derivations of an object unless the number of its fields is bounded by a pre-defined value. PWCs significantly affect analysis performance when analyzing large C/C++ programs with heavy use of structs and classes.

This paper presents DEA, a fast and precise approach to handling of PWCs that significantly accelerates existing field-sensitive pointer analyses by using a new field collapsing technique that captures the derivation equivalence of fields derived from the same object when resolving a PWC. Two fields are derivation equivalent in a PWC if they are always pointed to by the same variables (nodes) in this PWC. A stride-based field representation is proposed to identify and collapse derivation equivalent fields into one, avoiding redundant field derivations with significantly fewer field objects during points-to propagation. We have conducted experiments using 12 popular open-source C/C++ programs (8.2 million lines of LLVM instructions in total). The experimental results show that DEA is on average 7.1X faster than Pearce et al.'s field-sensitive analysis PKH, obtaining the best speedup of 14.1X while maintaining the same precision.

ABSTRACT. We address the problem of verifying the temporal safety of heap memory at each pointer dereference. Unlike separation-logic-based approaches, our whole-program analysis approach is undertaken from the perspective of pointer analysis, allowing us to leverage the advantages of and advances in pointer analysis to improve precision and scalability. A dereference ω, say, via pointer q is unsafe iff there exists a deallocation ψ, say, via pointer p such that on a control-flow path ρ, p aliases with q (with both pointing to an object o representing an allocation), denoted A^ψ_ω(ρ), and reaches ψ on ρ via control flow, denoted R^ψ_ω(ρ). Applying directly any existing pointer analysis, which is typically solved separately with an associated control-flow reachability analysis, will render such verification highly imprecise, since ∃ρ:A^ψ_ω(ρ) ∧ ∃ρ:R^ψ_ω(ρ) ⇏ ∃ρ:A^ψ_ω(ρ) ∧ R^ψ_ω(ρ) (i.e., ∃ does not distribute over ∧). For precision, we solve ∃ρ:A^ψ_ω(ρ) ∧ R^ψ_ω(ρ), with a control-flow path ρ containing an allocation o, a deallocation ψ and a dereference ω abstracted by a tuple of three contexts (c_o, c_ψ, c_ω). For scalability, a demand-driven full context-sensitive (modulo recursion) pointer analysis, which operates on pre-computed def-use chains with adaptive context sensitivity, is used to infer (c_o, c_ψ, c_ω), without losing soundness or precision. Our evaluation shows that our approach can successfully verify the safety of 81.3% (or 93,141/114,508) of all the dereferences in a set of 10 C programs totalling 1,166 KLOC.

ABSTRACT. We improve the policy iteration-based algorithm for value set analysis by giving a new heuristic for policy selection based on a local static analysis. In particular, we detect loops in the program and perform an analysis to discover the relative changes of variables in the loop, that is, whether a variable is constant or whether its value rises, falls or both. We use these relative changes to improve the old heuristic, achieving better (that is, smaller) fixed points than the original approach.

ABSTRACT. We show that the classical approach to the soundness of dataflow analysis is with respect to a syntactic path abstraction that may be problematic with respect to a semantics trace-based specification. The fix is a rigorous abstract interpretation based approach to formally construct dataflow analysis algorithms by calculational design.

ABSTRACT. Data science software is playing an increasingly important role in every aspect of our daily lives and is even slowly creeping into mission critical scenarios, despite being often opaque and unpredictable. In this paper, we will discuss some key challenges and a number of research questions that we are currently addressing in developing static analysis methods and tools for data science software.

ABSTRACT. Indexed grammars are a generalization of context-free grammars and recognize a proper subset of context-sensitive languages. The class of languages recognized by indexed grammars are called indexed languages and they correspond to the languages recognized by nested stack automata. For example indexed grammars can recognize the language {a^nb^nc^n | n >= 1} which is not context-free, but they cannot recognize {(ab^n)^n | n >= 1} which is context-sensitive. Indexed grammars identify a set of languages that are more expressive than context-free languages, while having decidability results that lie in between the ones of context-free and context-sensitive languages. In this work we study indexed grammars in order to formalize the relation between indexed languages and the other classes of languages in the Chomsky hierarchy. To this end, we provide a fixpoint characterization of the languages recognized by an indexed grammar and we study possible ways to abstract, in the abstract interpretation sense, these languages and their grammars into context-free and regular languages.

ABSTRACT. We study the language inclusion problem L1 ⊆ L2 where L1 is regular. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by successively overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2 . We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e. its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e. it guarantees termination of least fixpoint computations). Such overapproximating abstraction function on languages can be defined using quasiorder relations on words where the abstraction gives the language of all words “greater than or equal to” a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms like the so-called antichain algorithms. Finally, we provide an equivalent greatest fixpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known.

ABSTRACT. The Monniaux Problem in abstract interpretation asks, given a program P, a safety (i.e., non-reachability) specification S, and an abstract domain of invariants D, whether the following problem is decidable:

Determine whether there exists an inductive invariant J in D guaranteeing that program P meets its specification S.

The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers.

In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.