Static Analysis of Endian Portability by Abstract Interpretation
summary
A static analyzer infers whether two C variants produce identical outputs across little- and big-endian platforms by building a B-cell memory abstraction plus a symbolic predicate domain for bit-slices and byte relations, implemented on top of the Upset framework. The prototype analyses million-line avionics modules, finds known endian bugs in GitHub patches, and scales with zero false alarms on industrial targets, trading costly polyhedra for pattern matching and symbolic propagation to prove endian portability.
AI-written summary · about
chapters (10)
- 0:00Start
- 3:21Endian portability analysis
- 3:51Simple and double programs
- 7:22Lifting simple program semantics to double programs
- 9:28Low-level memory abstraction
- 12:08Optimizing the memory model for the common case
- 13:47Analyzing the motivating example, with bi-cells
- 19:46Implementation
- 21:57Benchmarks
- 23:39Conclusion