Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                         Lundi 20 septembre, 10h30

                                ------------
                                Xavier Leroy
                                ------------

                          INRIA Paris-Rocquencourt

       ==============================================================
       Nondeterministic expressions in C and how to compile them away
       ==============================================================

The C language has a rich sub-language of expressions, including many
operators that have side effects.  The C standards leave evaluation
order within expressions largely unspecified, resulting in
nondeterminism that is challenging both for programmers writing
portable programs and for semanticists trying to capture all that in a
formal semantics.  I will briefly review these difficulties and the
way they are addressed in Michael Norrish's formal C semantics.

The focus of the talk, however, is on working with this
nondeterminism, and possibly taking advantage of it, in tools that
operate over C programs: compilers, static analyzers, program provers.
Most of these tools commit early on a particular evaluation order,
captured by a source-to-source transformation that "pulls" side
effects "out" of expressions, materializing them as statements and
introducing temporaries in the process.  Necula et al's CIL library,
used in Frama-C and until recently in CompCert, implements a
particularly clever algorithm for pulling side-effects out of
expressions that does not follow a simple left-to-right or
right-to-left evaluation order, but instead takes advantage of the
additional flexibility permitted by the C standard to produce
simplified C that is more efficient in some sense.

I have recently completed a Coq verification of a simplification
algorithm similar to CIL's.  In this talk, I will present this
algorithm and the main steps in its correctness proof, which is a
surprisingly tricky exercise in context-based semantics in the style
of Wright and Felleisen.  This algorithm was integrated in the
CompCert C verified compiler as an additional front-end pass,
replacing an earlier untrusted code transformation by a
provably-correct one.