C complet (?) uhm... maybe too much!
C moins quelque chose? qu'est ce que on pourrait enlever et rester un C *réaliste*? C'est quoi la notion de réaliste? Est-il réaliste un ``C-bof'' tel quel je pourrait l'utiliser comme back-end pour un compilateur d'un langage à haut niveau à la Bigloo, Caml?
Le C-prime de Chez Dassault Aviation : pas d'allocation dynamique, pointeurs sans algèbre et pas sur de fonctions, pas de variables locales: il à été conçu comme langage intermédiaire pour la conception de compilateurs pour des langages ad-hoc.
La volonté de travailler sur un angage proche de la machine est-elle une obsession ou correspond-elle à une réalité industrielle?
Allocation dynamique de mémoire: à première vue on n'a pas forcement en besoin, car elle complique la formalisation et la certification, on pourra en revanche l'ajouter/certifier après.
Le cas CAML: dans la génération de code intermédiaire XL&co passent pour un dialecte de C qu'on pourrait appeler C-- avec des mécanisme de gestion d'exceptions et qui interface un GC
A propos, le nom d'action "concert" n'est pas peut-être pas si bien chosi, car il existe un projet de recherche à CMU avec un nom et un objectif apparentés: Certified code for grid computing, voir l'article introductif.
Le cas BIGLOO: le code intermédiaire généré (juste avant la génération du C qui sera après compile par gcc), reste du scheme-like dopé avec des types et copieusement optimisée et manipulée. Le code C généré semble être C ``in toto'', c.à.d. avec setjmp et longjmp.
Formalisations de C en HOL par Norrish. Dans le document il y a beaucoup des complications inutiles. Norrish a tenté de formaliser ANSI-C, c.à.d. le C qui notamment a un comportement non-spécifié dans l'ordre d'évaluation des expressions: cela à été fait essentiellement pour être ``compliant'' w.r.t. toutes les possibles implémentations réelles de C.
- About Norrish: juste pour vous donner un goût de la démarche à la Norrish w.r.t. ce qu'on peut trouver dans la définition ANSI-C: (c'est bien ps2ascii :-)1.5.1 C terminology The C community tends to use a language of its own to describe notions relating to its language's semantics. Here we introduce some of the more important terms (c.f. the glossary in [ANS89,1.6]). Firstly there are three distinct ways in which the standard under-specifies execution of C programs. We explaine a ch and describe in general how they are modelled in the formal semantics.
Implementation-defined: Implementation-defined constructs are those which must have a definite meaning, but for which the standard has passed responsibility to the implementation. The implementation is required to document its choice of meaning. An example is the byte-ordering with in multi-byte numeric objects (big-endian vs little-endian).
We handle implementation-defined behaviour by defining, but underspecifying some constant in the semantics. In this way, we model the fact that there is a well-defined behaviour, but make it impossible for a user to rely on it being a particular behaviour. For example, INT_MAX, the largest value that can be stored in the int type must be at least 32767, but can be more.
Unspecified: A construct or program form for which behaviour is unspecified is one where the standard imposes no requirement. For example, the order of evaluation of expressions is unspecified. Here an implementation need not document its behaviour, and thus may choose to do different things in quite similar, if not identical, situations. We handle unspecified behaviours by always allowing all possible behaviours. In the case of expression evaluation, all possible evaluation orders can arise. One cannot then claim that a program's behaviour will have a particular result without confirming that all possible behaviours lead to the same result.
Undefined: Undefined behaviour results when a program attempts to do something which is semantically illegal. For example, undefined behaviour occurs when uninitialised memory isaccessed, when a null pointer is dereferenced, or when a side effect attempts to update a memory object which has already been accessed in the same phase of expression evaluation. We treat all such behaviour as equivalent to a transition into a special state where no further action takes place. In implementations, a program which attempts an undefined behaviour will in all likelihood do something, and this something may in fact be quite reasonable. Nonetheless, there is no way of relying on undefined behaviour to do anything in particular, so our approach of effectively aborting the abstract machine as soon as undefined behaviour occurs is safest. To do anything else would be to suggest that a particular behaviour could be relied upon, and this would necessarily be erroneous.
Related to the above notions is that of being a strictly conforming program. Such a program's behaviour doesn't depend on any implementation defined, unspecified or undefined behaviour. Though strictly conforming C programs are the ideal, it is still the case that there are legal programs that are not strictly conforming. For example, there are legal programs that behave non-deterministically, and thesemantics as presented here and in the standard reflects this.
Remarque de Luigi Liquori: Est-ce que le système de types de C buggé? Bonne question: j'ai toujours pensé que oui, mais enfin Norrish + le premières pages de Type Systems de L. Cardelli me font plutôt penncher vers le fait que le système de types de C ne respecte tout simplement pas le slogan de Milner ``well typed programs dont go wrong'', et que la choix des erreurs ``trapped'' et ``untrapped'' est diffèrent w.r.t celle qu'on pourrait avoir dans système de type plus exigeants.