C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are(…)
summary
A new weakly relational pointer domain for C, C-2PO, tracks must-equalities and -disequalities between pointer expressions, models address arithmetic confined to single objects, and implements a quantitative congruence closure (union‑find with offsets) plus block-disequalities. It is implemented in Goblint, instruments coreutils to generate ~20k assertions (C-2PO verifies its own invariants; a non-relational analysis proves ~20%, a relational Varoo ~40%), and slows SV-COMP reachability runs by under 3x for 95% of cases.
AI-written summary · about
chapters (14)
- 0:00C-2PO introduction
- 1:02Weakly relational domains
- 2:24C-2PO and two-pointer logic
- 3:48Pointer expressions in C-2PO
- 5:53Block disequalities and allocation
- 7:18Kernel representation
- 10:27Meet operation in C-2PO
- 11:52Join and widening in C-2PO
- 15:01Assignments and pointer changes
- 17:29Dynamic memory with malloc
- 18:11Coreutils evaluation
- 19:35SV-COMP benchmarks
- 20:37Precision limits and future
- 21:42Q&A
related talks
19mA Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
01h 02mFancy Pointers for Fun and Profit
53mSmart Pointers in C++
30mC to checked C by 3c
51mThe Smart Pointers I Wish I Had
52mNon-conforming C++: the Secrets the Committee Is Hiding From You
05mco_pilot
55mBreaking Dependencies: Type Erasure - The Implementation Details