Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algorithmic Details behind the Predator Shape Analyser

Kamil Dudka, Petr Muller, Petr Peringer, Veronika Šoková, Tomáš Vojnar

TL;DR

Predator tackles the verification of pointer-heavy, low-level C code by introducing Symbolic Memory Graphs ($SMG$) and an abstract interpretation framework that can handle unbounded linked data structures, pointer arithmetic, and memory reinterpretation. The core ideas are complemented by a robust join/abstraction mechanism, 0/1 abstract objects, and reinterpretation operators that preserve soundness while enabling scalable analysis. PredatorHP augments the core verifier with multiple specialized hunters to reduce false positives and improve throughput, leveraging parallel exploration. Empirical results on NSRP, lvm2, and SV-COMP benchmarks show Predator achieving strong termination properties and high accuracy, with PredatorHP reducing false alarms and accelerating analysis in many scenarios.

Abstract

This chapter, which is an extended and revised version of the conference paper 'Predator: Byte-Precise Verification of Low-Level List Manipulation', concentrates on a detailed description of the algorithms behind the Predator shape analyser based on abstract interpretation and symbolic memory graphs. Predator is particularly suited for formal analysis and verification of sequential non-recursive C code that uses low-level pointer operations to manipulate various kinds of linked lists of unbounded size as well as various other kinds of pointer structures of bounded size. The tool supports practically relevant forms of pointer arithmetic, block operations, address alignment, or memory reinterpretation. We present the overall architecture of the tool, along with selected implementation details of the tool as well as its extension into so-called Predator Hunting Party, which utilises multiple concurrently-running Predator analysers with various restrictions on their behaviour. Results of experiments with Predator within the SV-COMP competition as well as on our own benchmarks are provided.

Algorithmic Details behind the Predator Shape Analyser

TL;DR

Predator tackles the verification of pointer-heavy, low-level C code by introducing Symbolic Memory Graphs () and an abstract interpretation framework that can handle unbounded linked data structures, pointer arithmetic, and memory reinterpretation. The core ideas are complemented by a robust join/abstraction mechanism, 0/1 abstract objects, and reinterpretation operators that preserve soundness while enabling scalable analysis. PredatorHP augments the core verifier with multiple specialized hunters to reduce false positives and improve throughput, leveraging parallel exploration. Empirical results on NSRP, lvm2, and SV-COMP benchmarks show Predator achieving strong termination properties and high accuracy, with PredatorHP reducing false alarms and accelerating analysis in many scenarios.

Abstract

This chapter, which is an extended and revised version of the conference paper 'Predator: Byte-Precise Verification of Low-Level List Manipulation', concentrates on a detailed description of the algorithms behind the Predator shape analyser based on abstract interpretation and symbolic memory graphs. Predator is particularly suited for formal analysis and verification of sequential non-recursive C code that uses low-level pointer operations to manipulate various kinds of linked lists of unbounded size as well as various other kinds of pointer structures of bounded size. The tool supports practically relevant forms of pointer arithmetic, block operations, address alignment, or memory reinterpretation. We present the overall architecture of the tool, along with selected implementation details of the tool as well as its extension into so-called Predator Hunting Party, which utilises multiple concurrently-running Predator analysers with various restrictions on their behaviour. Results of experiments with Predator within the SV-COMP competition as well as on our own benchmarks are provided.
Paper Structure (43 sections, 2 equations, 12 figures, 4 tables, 13 algorithms)

This paper contains 43 sections, 2 equations, 12 figures, 4 tables, 13 algorithms.

Table of Contents

  1. Introduction
  2. Symbolic Memory Graphs
  3. The Intuition behind SMGs
  4. Further Illustration of the Notion of SMGs
  5. Formal Definition of Symbolic Memory Graphs
  6. Symbolic Memory Graphs
  7. Consistent Symbolic Memory Graphs
  8. Symbolic Program Configurations
  9. Special Kinds of SMGs and SPCs
  10. The Semantics of SMGs
  11. Operations on SMGs
  12. Data Reinterpretation
  13. Join of SMGs
  14. Abstraction
  15. Checking Equality and Inequality of Values
  16. ...and 28 more sections

Figures (12)

  • Figure 1: A cyclic Linux-style DLL (top) and its SMG (bottom), with some SMG attributes left out for readability. For the meaning of the acronyms (e.g., hfo stands for the head-field offset) see Section \ref{['sec:defOfSMGs']}.
  • Figure 2: A cyclic Linux-style DLL of DLLs with a shared data element (top) and its SMG (bottom).
  • Figure 3: A Linux-style list used in hash tables (top) and its SMG (bottom).
  • Figure 4: (a) An SMG and (b) its possible concretisation for the case when the DLS $d$ represents exactly two regions (showing key attributes only).
  • Figure 5: Materialisation of a DLS: (a) input, (b) output (region $r$ got materialised from DLS $d$). Removal of a DLS: (c) input, (d) output. Sub-SMGs $\widehat{G}_d$ and $G_r'$ are highlighted without their roots.
  • ...and 7 more figures