Static Analysis of Endian Portability by Abstract Interpretation
summary
A static analysis based on abstract interpretation proves when two endian-specific C variants produce identical outputs on identical inputs, despite pointer and union abuse. It defines a concrete collecting semantics and a joint memory abstraction that shares bi-cells across little- and big-endian views, plus a near-linear-cost symbolic predicate domain for byte-level relations. A 3,000-line OCaml prototype built on Mopsa analyzes open-source and Airbus code, finds all reported bugs, and reports zero false alarms at industrial scale.
AI-written summary · about
chapters (11)
- 0:00Intro
- 1:22Reading multi-byte input in network byte-order
- 2:32Endian portability analysis
- 3:04Simple and double programs
- 4:02Lifting simple program semantics to double programs
- 6:06Low-level memory abstraction
- 7:59Optimizing the memory model for the common case
- 9:22Analyzing the motivating example: from cells to bi-cells
- 10:51Implementation
- 11:10Benchmarks
- 12:36Conclusion
related talks
23mTargeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
19mA Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
01h 30mDangerous Optimizations in C and C++ Programming Languages
43mEverything I learned about static analysis and program safety in C++
18mMix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
51mCode Analysis ++
01h 27mDangerous Optimizations! in C++ - Part Deux
05mDetecting Programs That Rely on Undefined Behavior