University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Cerberus C semantics & pointer provenance

Cerberus C semantics & pointer provenance

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jean Pichon-Pharabod.

The C programming language is notionally defined by an ISO standard, the “de facto” usage of the language has however diverged over time from the standard semantics. The main point of disagreement concerns the memory object model, and in particular the semantics of pointers. While system programmers often rely on a very concrete view of pointers (sometimes even more concrete than what the ISO standard describes), compiler implementers take a more abstract view. Some compiler optimisations, in particular the ones based on alias analysis, reason about how pointer values are constructed during the program execution instead of only considering their representation.

In this talk, I will present a source-language semantics for pointer values and memory operations formalising a notion of provenance. It aims at reconciling the concrete and abstract views of the C memory model.

This work is part of the Cerberus project, an executable semantics for a substantial fragment of C, which I will also present. In this model, we define the semantics of C by elaboration into a Core intermediate language where we make much of the language subtleties syntactically explicit, while at the same time keeping some level of implementation agnosticism. Being executable, Cerberus can be used as an oracle for exploring the range of behaviours that one should expect for reasonably sized programs.

More information, including a link to Cerberus’ web interface, is available at https://www.cl.cam.ac.uk/~pes20/cerberus

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity