Skip to content

CrabPapers

Jump to bottom
Jorge Navas edited this page Jun 29, 2023 · 11 revisions

These papers explain the theory behind Crab implementation:

  • The implementation of functional (aka persistent) maps (domains/patricia_trees.hpp) is based on "Fast Mergeable Integer Maps" PDF.

    Functional maps are used in all the non-relational domains. They play a major role in the efficiency of binary operations such as join, meet, widening and narrowing.

  • The computation of weak topological orderings (fixpoint/wto.hpp). "Efficient chaotic iteration strategies with widenings" (PDF) by F. Bourdoncle. The paper describes a recursive algorithm. We implemented a non-recursive version to avoid stack overflows.

  • The fixpoint algorithm (fixpoint/interleaved_fixpoint_iterator.hpp). "Localizing widening and narrowing" (PDF) by G. Amato and F. Scozzari.

  • This is the paper for the zones domain (domains/split_dbm.hpp). "Exploiting Sparsity in Difference-Bounds Matrices" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. SAS'16.

    This paper presents a novel form for weighted graphs called Split Normal Form (SNF). This representation avoids any relationship which can be deduced by interval reasoning. E.g., if x<=5 and y >= 10 then the constraint y>=x is redundant and it is not stored in the graph. As a result, the graphs tend to be less dense. Moreover, the performance of several graph representations are discussed and implemented: domains/graphs/ht_graph.hpp (hash-based graphs), domains/graphs/pt_graph.hpp (patricia-trees-based graphs), domains/graphs/sparse_graph.hpp (sparse graphs), and domains/graphs/adapt_sgraph.hpp (hybrid of dense and sparse adjacency lists)

  • This is the paper for the octagons domain (domains/split_soct.hpp). "A Fresh Look at Zones and Octagons" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. In TOPLAS Volume 43, Issue 3 September 2021.

    This octagons implementation manipulates graphs in SNF. Therefore, it has the same benefits than the zones domain.

  • This is the paper for the terms domain (domains/term_equiv.hpp). "An Abstract Domain of Uninterpreted Functions" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. VMCAI'16.

  • This is the paper for the wrapped interval domain (domains/wrapped_interval_domain.hpp). "Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code" (PDF) by J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. APLAS'12.

  • This is the paper for the Boxes domain (domains/boxes.hpp). "Boxes: A Symbolic Abstract Domain of Boxes" (PDF) by A. Gurfinkel and S. Chaki. SAS'10.

  • For the constant and sign domains (domains/sign_domain.hpp and domains/constant_domain.hpp), I recommend to look at this tutorial.

  • This is the paper for the congruence domain (domains/congruences.hpp). "Static Analysis of Arithmetical Congruences" (PDF)

  • A new look at widening. "Dissecting Widening: Separating Termination from Information" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. APLAS'19.

  • The refining forward+backward analyzer is described by Cousot and Cousot in these two papers: JLP'92 and ASE'99 (section 4).

  • For the top-down interprocedural analysis the closest reference I think it would be this.

  • The paper "Abstract Interpretation of LLVM with a Region-Based Memory Model" by A.Gurfinkel and J. A. Navas (PDF) that describes CrabIR, the Crab Intermediate Representation.

Clone this wiki locally