SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Sun 17 Oct 2021 13:50 - 14:05 at Zurich B - Session 3A Chair(s): Mihaela Sighireanu
Sun 17 Oct 2021 21:50 - 22:05 at Zurich B - Session 3A Chair(s): Suvam Mukherjee

We present a static analysis of endian portability for C programs. Our analysis can infer that a given program, or two syntactically close versions thereof, compute the same outputs, when run with the same inputs on platforms with different byte-orders, a.k.a. endiannesses. We target low-level C programs that abuse C pointers and unions, hence rely on implementation-specific behaviors undefined in the C standard. Our method is based on abstract interpretation, and parametric in the choice of a numerical abstract domain. We first present a novel concrete collecting semantics, relating the behaviors of two versions of a program, running on platforms with different endiannesses. We propose a joint memory abstraction, able to infer equivalence relations between little- and big-endian memories. We introduce a novel symbolic predicate domain, to infer relations between individual bytes of the variables in the two programs, which has near-linear cost, and the right amount of relationality to express (bitwise) arithmetic properties relevant to endian portability. We implemented a prototype static analyzer, able to scale to large real-world industrial software, with zero false alarms.

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Session 3ASAS at Zurich B +8h
Chair(s): Mihaela Sighireanu IRIF, Université Paris Diderot, France
13:50
15m
Talk
Static Analysis of Endian Portability by Abstract InterpretationVirtual
SAS
David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
14:05
15m
Talk
Verified Functional Programming of an Abstract InterpreterVirtual
SAS
Lucas Franceschino INRIA, David Pichardie Facebook Paris, Jean-Pierre Talpin INRIA, France
14:30
15m
Talk
Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual
SAS
Julien Braine , Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS/VERIMAG
14:45
25m
Live Q&A
Session 3A Discussion, Questions and AnswersVirtual
SAS