From 659ea263a5b1971ae365bf9d97758abf7e89ebdc Mon Sep 17 00:00:00 2001 From: Julien Blond Date: Wed, 16 Oct 2024 09:51:30 +0200 Subject: [PATCH 1/5] Added some debugger infos. --- "src/\303\251tude/C.typ" | 12 +++++++++++- "src/\303\251tude/links.typ" | 6 +++++- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git "a/src/\303\251tude/C.typ" "b/src/\303\251tude/C.typ" index 5e620a2..9c3cfa5 100644 --- "a/src/\303\251tude/C.typ" +++ "b/src/\303\251tude/C.typ" @@ -463,6 +463,7 @@ propre à une utilisation dans le domaine critique. des systèmes d'exploitation et des architectures. Pour simplifier la lecture de ce document, nous ne listons ici que les principaux débugueurs connus. + #figure( table( columns: (auto, auto, auto), @@ -471,9 +472,11 @@ de ce document, nous ne listons ici que les principaux débugueurs connus. [*#gdb*], [x86, x86-64, ARM, PowerPC, SPARC, ...], [GPLv3], [*#lldb*], [i386, x86-65, AArch64, ARM], [Apache v2], [*#totalview*], [x86-64, ARM64, CUDA], [Propriétaire], - [*#undo*], [?], [Propriétaire], + [*#undo*], [x86-64], [Propriétaire], [*#valgrind*], [x86, x86-64, PowerPC, ARMv7], [GPL], [*#vsd*], [x86, x86-64], [Propriétaire], + [*#windbg*], [x86, x86-64], [Gratuit], + [*#rr*], [x86, x86-64, ARM], [GPLv2], ) ) @@ -510,6 +513,13 @@ qu'il soit donc compatible avec toutes les architectures supportées par #gcc. #vsd est le débugueur associé à la suite de développement #visualstudio de #microsoft. Il est propriétaire et ne fonctionne que sous Windows mais offre un support avancé de tous les langages supportés par #visualstudio. +Il ne faut pas confondre #vsd avec #windbg qui est un débugueur plus bas +niveau pour les plateformes Windows et qui est gratuit. + +#rr est un débugueur qui propose la même interface que #gdb mais qui exécute +le code dans une machine virtuelle et permet de remonter dans le temps et rejouer +les exécutions de manière déterministe. Cela permet de débuguer plus facilement +les erreurs aléatoires. ], diff --git "a/src/\303\251tude/links.typ" "b/src/\303\251tude/links.typ" index ca7dfec..6cf3c66 100644 --- "a/src/\303\251tude/links.typ" +++ "b/src/\303\251tude/links.typ" @@ -204,4 +204,8 @@ #let spark = link("https://www.adacore.com/about-spark", "SPARK") -#let cvc4 = link("https://cvc4.github.io/", "CVC4") \ No newline at end of file +#let cvc4 = link("https://cvc4.github.io/", "CVC4") + + +#let windbg = link("https://docs.microsoft.com/en-us/windows-hardware/drivers/debugger/debugger-download-tools")[WinDBG] +#let rr = link("https://rr-project.org/")[rr] \ No newline at end of file From 9d0c9b5aaf94ce219165d044442ed556e3e4d8b6 Mon Sep 17 00:00:00 2001 From: Julien Blond Date: Wed, 16 Oct 2024 17:27:40 +0200 Subject: [PATCH 2/5] Added C part on slides. --- Makefile | 2 +- src/base.typ | 1 + ...mlPro_PPAQSE-COTS_pr\303\251sentation.typ" | 339 ++++++++++++++++++ 3 files changed, 341 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 6856c2b..8637127 100644 --- a/Makefile +++ b/Makefile @@ -32,7 +32,7 @@ all: $(PDFS) watch: while inotifywait -e close_write "src/étude/OCamlPro_PPAQSE-COTS_rapport.typ" || true; do make; done -$(BUILD_DIR)/%.pdf: src/%.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. +$(BUILD_DIR)/%.pdf: src/%.typ src/base.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. $(TYPST) c $(TYPST_ARGS) $< # force moving file for typst seems to always try building locally oO mv -f src/$*.pdf $@ diff --git a/src/base.typ b/src/base.typ index 65307f0..d3b728d 100644 --- a/src/base.typ +++ b/src/base.typ @@ -66,6 +66,7 @@ dir: ttb, spacing: 2pt, line(length: 100%), + v(5pt), align( center + horizon, [ diff --git "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" index e69de29..b2872ae 100644 --- "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" +++ "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" @@ -0,0 +1,339 @@ + +#import "../base.typ": * +#import "../étude/links.typ": * + + +#show: presentation + +#title-slide( + title: [ + Écosystèmes COTS de développement et de vérification des logiciels + critiques et temps réel + ], + subtitle: "", + authors: [Julien Blond (julien.blond\@ocaml.pro)], +) + +#slide[ + = OCamlPro + + - PME française créée en 2011 + - ADN recherche et liens étroits avec la recherche académique. + - OCaml : core team, opam & optimisations + - R&D langages (DSL) & dette technque (Cobol) + - Méthodes formelles (Alt-Ergo) + - Certification Sécurité (CC EAL6+) + - Formations (OCaml, Rust, Coq) + + Jane street, Inria, DGFiP, Samsung, Mitsubishi, Thales, CEA, Adacore, + TrustInSoft +] + +#slide[ + = Objectif + + Tour d'horizon des langages de programmation dans la sûreté: + - C + - C++ + - Ada + - Scade + - OCaml + - Rust + + Donner suffisamment d'informations pour faire un choix éclairé +] + +#slide[ + = C + + - Créé en 1972 par Dennis Ritchie + - Programmation système (Unix) + - Langage bas niveau + - Standardisé : C89, C99, C11, C18, C23 (draft)... + - ... mais une sémantique indéterministe. + + +] + +#slide[ + == C : Paradigme + + Essentiellement *impératif* et *procédural* + + ```c + int add_value(struct state *s, int v) + { + int code = KO; + if (nullptr != s) { + s->acc += v; + code = OK; + } + return code; + } + ``` +] + +#slide[ + == C : Mécanismes de protection intrinsèques + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Avantage*], align(center)[*Inconvénient*], + [Système de type], [Trop rudimentaire et laxe], + [ ], [Gestion manuelle des pointeurs], + [Analyses des compilateurs], [ + - Pas activées par défaut + - Pas standardisées + ], + ) + ) +] + +#slide[ + == C : Compilateurs + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Compilateur*], align(center)[*Remarques*], + [GCC], [La référence], + [Clang], [Le challenger], + [icc/icx], [Intel], + [MSVC], [Microsoft], + [AOCC], [AMD], + [sdcc], [microcontrôleurs], + [CompCert], [Vérifié formellement], + ) + ) +] + +#slide[ + == C : Interfaçage + + #v(2cm) + - Le C permet d'écrire de l'assembleur dans le texte. + + - Il sert de cible pour la plupart des langages. + +] + +#slide[ + == C : Adhérence + + #v(2cm) + Aucune, il faut juste un compilateur pour l'architecture cible. +] + +#slide[ + == C : Gestionnaires de paquets + + - Deux gestionnaires classiques : Conan & vcpkg + - Un gestionnaire de _vendoring_ : Clib + - Possibibilité d'utiliser des gestionnaires agnostriques (Nix, 0install, ...) + + Pour les systèmes embarqués : Buildroot, Yocto, ... ont leur propre + _packaging_. +] + +#slide[ + == C : Communauté + + - Très large + - Entreprises + - OS (FSF) + - Système (Linux) + - Embarqué +] + +#slide[ + == C : Debugueurs + + #{ + set text(size: 16pt) + + figure( + table( + columns: (auto, auto, auto), + [*Debugueur*], [*Architectures*], [*License*], + [*#linaro*], [x86-64, ARM, PowerPC, Intel Xeon Phi, CUDA], [Propriétaire], + [*#gdb*], [x86, x86-64, ARM, PowerPC, SPARC, ...], [GPLv3], + [*#lldb*], [i386, x86-65, AArch64, ARM], [Apache v2], + [*#totalview*], [x86-64, ARM64, CUDA], [Propriétaire], + [*#undo*], [x86-64], [Propriétaire], + [*#valgrind*], [x86, x86-64, PowerPC, ARMv7], [GPL], + [*#vsd*], [x86, x86-64], [Propriétaire], + [*#windbg*], [x86, x86-64], [Gratuit], + [*#rr*], [x86, x86-64, ARM], [GPLv2], + ) + ) + } +] + +#slide[ + == C : Tests + + #figure( + table( + columns: (auto, auto, auto, auto, auto), + [*Outil*], [*Tests*], [*Generation*], [*Gestion*], [_*mocking*_], + [*#cantata*], [UIRC], [+++], [✓], [], + [*#criterion*], [U], [+], [], [], + [*#libcester*], [U], [+], [✓], [✓], + [*#novaprova*], [U], [+], [✓], [✓], + [*#opmock*], [U], [++], [], [✓], + [*#parasoft*], [UC], [++], [✓], [], + [*#TPT*], [UINC], [+++], [✓], [], + [*#vectorcast*], [UC], [++], [✓], [✓], + ), + ) +] + +#slide[ + + == C : Parsing + + Il existe beaucoup d'outils d'analyse syntaxique en C mais les plus + connus/matures qui suffisent dans la grande majorité des cas sont: + - Flex/Bison + - ANTLR + + +] + +#slide[ + == C : Méta-programmation + + - Le préprocesseur permet de faire précalculer des expressions simples + par le compilateur (souvent inutile) + - Il existe des _tricks_ d'expansion récursive bornée (à éviter) + ```c + /* #define sum(n) ((n * (n + 1)) / 2) */ + inline int sum(int n) { return (n * (n + 1)) / 2; } + int main() { return sum(10); } + ``` + ```asm + 0x0000000000001040 : endbr64 + 0x0000000000001044 : mov $0x37,%eax + 0x0000000000001049 : retq + ``` +] + +#slide[ + == C : Dérivation + + - Les macros permettent une forme archaïque de dérivation + ```c + #define COULEUR X(ROUGE, 0xFF0000) X(VERT, 0x00FF00) X(BLEU, 0x0000FF) + #define X(c, v) c = v, + typedef enum { COULEUR } couleur_t; + #undef X + ``` +] + + #slide[ + == C : Runtime Errors + + Les analyseurs statiques corrects permettant de se prémunir contre des + erreurs à _runtime_ sont: + - #astree + - #eclair + - #framac + - #polyspace + - #tisanalyser + ] + + #slide[ + == C : Formalisation + + #[ + #set text(size: 18pt) + - Par transpilation (automatique ou manuelle) vers Coq (VerifiedC): + #align(center, + grid( + columns: (auto, auto, auto, auto, auto), + [C], [$=>$], [Coq], [$=>$], [Preuves (Hoare, WP)] + ) + ) + + - Par annotation et preuve (semi) automatiques (Frama-C, RedefinedC, VerCors): + ```c + /*@ requires \valid(a) && \valid(b); + @ ensures A: *a == \old(*b) ; + @ ensures B: *b == \old(*a) ; + @ assigns *a,*b ; + @*/ + void swap(int *a,int *b); + ``` + ] + + ] + + +#slide[ + == C : WCET + + Il existe plusieurs outils basés sur une analyse statique binaire : + - #chronos (IR) + - #bound-T + - #aiT + - #sweet (IR) + - #otawa (modulaire) + - #rapidtime + +] + +#slide[ + == C : Pile + + Pour l'analyse statique de la pile: + - #gcc + - #stackanalyser + - #t1stack (+ annotations) + - #armlink +] + +#slide[ + == C : Qualité numérique + + #[ + #set text(size: 18pt) + Se prémunir contre les erreurs numériques (overflow, précision, ...) + - par analyse statique: + - #fluctuat + - #astree + - #polyspace + - #gappa (+ annotations #framac) + - par un calcul dynamique: + - #cadna + - #mpfr + - #gmp + ] + +] + +#slide[ + == C : Assurances + + Niveau d'assurance donné par le C est paradoxal : + - quasiment pas de sécurité intrinsèque + - l'histoire et l'usage ont apporté des outils externes qui fiabilisent le C + + Le développpement reste relativement peu productif et coûteux: + - même un bon programmeur fait des erreurs + - A/R entre services de développement et de vérification + - licences, formations, ... +] + +#slide[ + == C : Critique + + Le C est utilisé dans tous les domaines critiques soit + - directement pour écrire le système (en entier ou au moins les interfaces + avec le matériel); + - indirectement comme langage cible (#Ada, #Scade, ...). +] From a88374330724d9871aee115f7b6e0cb796cf9824 Mon Sep 17 00:00:00 2001 From: Julien Blond Date: Fri, 18 Oct 2024 09:56:34 +0200 Subject: [PATCH 3/5] Added CC BY logo. --- src/base.typ | 4 ++-- src/imgs/by.png | Bin 0 -> 12588 bytes 2 files changed, 2 insertions(+), 2 deletions(-) create mode 100644 src/imgs/by.png diff --git a/src/base.typ b/src/base.typ index d3b728d..82c3a74 100644 --- a/src/base.typ +++ b/src/base.typ @@ -241,8 +241,8 @@ ) } ), - v(10%), - + v(1fr), + image("imgs/by.png") ) ) diff --git a/src/imgs/by.png b/src/imgs/by.png new file mode 100644 index 0000000000000000000000000000000000000000..c8473a24786ab016d9c3e717a380910f7cbb0fff GIT binary patch literal 12588 zcmXY21ys}R+a8ECNOyOalu|OfrKB5FI;2xzv^0{^t@KNGhp2Q&cju(@d-$J^b8s8m zZ`)J%758PtTU9wMbTV`Z1cId?FRcNAAS8nO(WuDaUzdgyad3n5396ul3VwW1EyKZM zG$(nzPY?(f$I~wYwr#u}_#>&SjIOJu<9k;RGZ!m}hldB3wS(;^3o|DxE=QLS8AqaI z5C{!KL0VGF^V{K~m!Zn_Bg)APXG5Cz6_kbu*5aB>jBu$QB3vT(-%i zKB=J`SOT?pH7U?g#dr`&s3Ol>2tvPZV> z&77JHeIvU}8=sv(M#NJdtRUhBsw>z2nrgl}Ru|sXi|wC?~nY zkR)+n-LEiAX;X&pQSZ3Z?zrPc5k@78a&f^kkqj7bUT~${R*R>7Lpia(SGTvfKii!_ zDSA)YX*Z?lZiWY5Ag-$Z5cWbNtJwFZIt34Md9!S7V`F|=!^jYi177ia+`c@jZ#emllvMD) zp@Abs2*qB&_Gp99+1YskHKimDQZ5g;J33z-JI+k~iY3?Kh8vQTD8sxfCj+i$`8EQV z5n}YMiGg9(MPDh7+(+eF; z*2+QYOP-GwpQ*6L#wK!^51RkR2cSsPbG}Y<5~gTX4T#=GQ}E16`qKK%ke~)bT}ul# z@`DjWN=2odwkg#hJzq)3z_ofGktj;W;tZ+F#7c${${j`{%0SU4(}#D=Ex}DaLr3S# zNr$IQ$n@>ot;JpM>Bous=-ykV4U;G(rUOJl^COw{Y-Y81xG3qS)n@IbI+(r41N05c z?G>4y7}Bt5ZF50h0ZE;fik*o{Ztw*q6(W8)((LFM7(|r}k~ca%AkIFwOY41Wq#Zr4 z-hktGDQ+0{NZn3)iB;=XYlVkFORX=>$I8wwW#`IqwAdb20Fwq|>ta^uoELIDz4&b) zEh`<=XWli|MEworOzs1@Ee{E1TCa31$BQG0&R38Bc|KmWl}RDIy=3D!aAC=-So}P* z6MsUoi=Zt4zu8wR7#-TUZ@EOpZvG-7bez-NtUtZVuc50O{=-biN#Fo|uHF_SRz2&= zduL`t>?Li&Br*5u_I}u8N@)#tp&l4Bs_-W&ot{e51=uOcmZ0)9Ev`mU+|Y*Gjjdtx zi4c{v1di>2l)lR+7iahmnxXI|@q$=rk3EdMwzkfak|>wPL3*k4w5PqKyqs{?*UHMO z)_$HSG&EGDJyn^>#lJ8t}feJV%ca?tRi&HX)|1xNU)nGhcr=JDA>-L zyuH1hJUqgRiDt|4~T;h za#pAPw-(Y!wvO0(oYHl`6~lokr3lFI&PpRq1OkO^u!pbTL%IK?!Sk5tjp|JUNw>FFt+xq^qwFRZ+qE`t_>@ z>1@E|1*L;g2bvT;eeLn6@!CBuoc-L2O|atcXHW|Q?bDQ*wnnmJJ3HSrHZ=tfCH-O7 zBqt~TmG%;)sHiABHdfA=_fdfBn?AO=g?ZPiliAE~RW@F{gp>z1tkZ1KSHqjB3fkI) z*oP9~J1t|i#yTb@)D8{~RrU2-uSl+&5)u+Z5r!_0mxb;wd%|8g-(J{jX={(+8R+Se zUL2fsJw`kAB<*SzTm%QkQF}Fc&4Q^Zd>&3kMK#;tNX@}v`RQMAS=krrfIHkoCYA1` zHlJ#<9^^nF<3I%B+#kc;;QB<3BpCmY5g#iHOXnX>k@)1B$mD&$^C_K^latS3VJH-o zlp)6QC5460m6Vip^#%R54Ky@@Y-cKH`S}S}S62uB5It%yOjWVV`<>z`B|m;~4?XN{ zr^+Q^V`HoOG>lC^NQ7qB;(cyo_qRrdYnrR{#}AA1y(uRbm+n+vi<8rJx%R{RnA@(# zHs1EVrD#VH=;`28>d=0z>%nZzGir&G$IuNq8JXu&p_tb4G?cI9i-jpuhWpkBVsXjH zB1cExiu&K_mhD?x+nP-^Ygg4ADQm)DtzdO$+w6s?#8)J$%JcFNO-xLb)A(e{9>ymo zoZ%Y^qTXkyU|a4iwg~mdQpdLY-A1}C>Qowc_4GXBHf~*+SJl+SUutRS8tj!XdqDl0 zFpqFGyMrQJbqQf(XP0@M-DPSzUZ5~rV}1Ru>bP-Owh)*Ypid4E3v+^mMZLKh%PD zBwU7#pS}KVN$TjNZ0$%}yni1``tp6}(h}83mY9^kfBWbRC^<4`iyy(6MfoqLMlBBM z{%E=Fg~YPNReg0$O?SCLgQ+9;l1g8l?aawx!?K{rpMgymTuMqTfKX@qGin>+larG? z&TG;e8yhEnuen*dByWDWg44w$a6mA*{p^JAzGHCH#o6@u7!*n4g0BaQEgl0?KXhfiq++t@_QQs`Iv@vhuyV-WWXl~}rC3#@p=>1Knq`i5>J zOgVALZUZ z64FzukJ~Oy!nfO``Zx5JN=y>bCSZz2AA+ITLT24a(lRo+D&&2}tPU0y!Htc=m}LC& zCI4(}ZL8;fh{uf!6_|LSY{C@Sf3nsdpSiAfhop-62-^FlXJjZ9l+!RVF`;5(hc-9A z9ubUPqgs_geF&z8 z-Tu$j^~4-At)GSp)6~?|>}DH2HC*DYxE!c}4-XHsRc65(h>5sNi4pm7vF6L|eo(?q zb~cXg_DmlcE(O&=RVyn-u5b5I+s@!6pd3!<7vPqV2b`Xs;?6pN0q)FJ)0g`_>+Frd z=QZtwWDRHn-gGK;I{hBEhH=Vr&1Z+ixacH6?T+=?vu6v9&d)$iOfc1|Y4|us2apL} zn@JRu_Pe3QZ{27wu%#p=5k}Vk`!G^u)!Fvy<%d7L3r(NAsHk7NveetpGsU+fn9fuf z`Nn38xV@vjV5UoFuCv7RW+iBFSjbywH)?VBJXt}wxjg1>%Gn6d$RIyjY+;^!omMrR z>sgTF)8ZTP{rh*PS0{WU>vMB+x(yDQ(iXz5J2*kX!Mt{}Jhj#n$l&iz?(Y3ygW!;o zvW|W4@w++ex;kC=q8j=6t2=Q(jbU1XR!>9W2`)oAmaTstYHMpd?~XI35mqM>f@MHL zLP9-{TwiH_25l2$uw*{fqx<>urze$3wRwmZQ;MgzHyv2irluyqe|y1+XT+*}_WCkMw>yAA&PmpssR`Bs~gkWa+0=1<1e=FgebvN*cJH(eI>YMN~GBB7vKHN7tuZQZc<6K-^ zT-Q3<>SD7YHb>}H8mw>)zNLL2@K+@BRWb?w<*!bk) zBH2_ra{Y2SU;xksTtY&b()*!&=Bn*Zo|3h$o}Ri*c4B6*Qec3RFdI}WcFj}btFD1T&)i&keLEdJy|n_vIXJA&H~iPh7je;0Ht{TwQ;z>#+67x?&qnf==R zAXS=3u?}f^dV03enZB_8E8*8hJTltVa8xrwLLyo*&dlx8czQWSUb1VRrvtp>iYSHG6Iu{pL?Q&Wj|EH~Ax!>&Qq4aOn)oK5JM$O&W+=5deInGpM z&Wcd5(Se=QPS_!luzQ3qM>iy$T8t<8!#tunz%xV8K5w$Vpb=@N@??24CXUM;A!C~t z1tpBz{aY2F7NW7$e_J2_pk7PgdN}VzrN}GF=S{kU6Kk?zl*YoOk`AkEzlqeCA04KJ zmhaOtM49mM^7AK|Gr$Y&=j)%Y4$=4m%XxMP>c{PLaXhq>%yPrs*do^!$Noi@k z6F(9mLmGeVu`L(eGSBIw5kkQ6w2|T=0DeS2Kfl*4$Pm$h2a2?`w87zFP|~P#%FD6v z@$pkrQ#)s8Nsy6|YcJ6tfB*iKS5$=h`-{W>{R1r0)Xr{Uv@$*(cX`dd8!#y-I3doD z4}R^3ib{&7{14P;d+TqMI$%3j_ofV$P3b!F{mKN`_Cp1L37rx|)t<6Tah8E%-Lh^udJx3dFye6O4U8(P^J%SXgVgS7fwVvD#Ryh-6QTG`nNCl@MF zA-d8sHl`xtHpT>d(Qc`g6qI{Jj9pOaR@eHXo=9qGDQjz6Ti+aGya{WhnwVO_yTH$J z97IZC+tmvThODx5CUCf?qgZ)ip$uL`P%dX01EWTU*v952qq_-MdT6C_8xAh*jm`1w ztZrj-v-w1kN>cF{;L61H_4TtI0TOK23-<7T5BEN0djBE!gks@0Nrz-+QUcXD+7pzzPtO@U9HzxLPGP29*Mp}Ls5iL;pR6%HVCd6UUq zra79$syj<{91S9681uq zW$vgxsJ=cK6beO(G3f2>HNC$%pKW$yFZ74J0rCy#1<8*eS(e=k`r{8yefWlc{VHga zFfcIS(622S0}d25(cX~vT&?x!*tO$=Irxy;KAqTQc5!e{J;CU;bbeq{zSb((cU)>s z8z)hiueWzz?S76)!jm&peRk&hD@%+V@N=%9osEsj9c`UAZy*{P8b}wzmVDJ7$Hu?1 zB|3(91v8=rY^PU7bEQN_gaiZ%`E!;GTZ0nN(ki)q?h+IX4JiQCFSkGfz%H3B?nmag zwY|-(#is|@KyO3HijeUjof;E*Sn`aa*1I1zHa3xGFSd3kic!(faAzwF8XP`hw%Q&7HxpjY5#c~rFiN%W zHJoW+uE8-@DhzuS5cO06+vLu6aXG7VSKw+5z8pdICLtw1^<~u4)C@j3ablHY@Oky> zmFL+G?#Ox(<<4Ka)Ho{d1hf!le07~0DhdB@8Y0xx)PX))KT1oVknkgr_mCVQsZcR6 zq+DJ3LorFmOYD`EF%uGy)I1)px3hsYz)-aaxD*+l_U*-?^T~>2L1CfU(Lxiz6I@UK zPgmtM4_fMG@$xgwJ7eFq*h^(EPC7j5X_m5- zrOPFIkL$F=0R8z{If{vi`J@(j(v+VB!-p2Y8PHpkLqn0bex*s3nlLglQV2UiVyVQs zVevOUq9R)=N1>sH32qzJKh|CF=Ywu zSFx=8aGdp4L&L`Xpt7U{wZUPryUMJ`5-06U8yJ3kdNz}nU}|39o_9U(xYHNME!SD19ftgWrR zkL4x7oV{cilE#h5R0digG7_mHk$7_mX0u2KPH%4IZ#BTZM;tHI+;&C-r~N|;^YX@d z9(rCVFu}WW)f}@1?(Xm7Q&U;`K3aYNl}|KQ&%HjVKBoRGi1s7BJ0B|>2cGT@4$k2a z%!Ibl8{lhg$|;eSeqk0U%H{WwK|g>Fw(~ z6Nj=N&KQ(@%%!1sc$`lh5lk~0|`T27+zr)m2lJ-7& zBSS+Z<8^=?(97G6A^f?1uM*WvCPLlKky*6$oT8%sf1a|k$g;6iDz{Xx$G7(PqX3;c zwO>E~E&tIrakn!vCd(3PwjiBk*==4u+9q~l?yf&h zDLSE5pYP9D0BYe|teu>a(lb1aae1_8d*%fyA~H5bI5^bnpt3_CVC0Q0Ef@zv92}Sy z12KfcDuAB-R-w9FZuJUId-)+xDTV84myK#dOFOpcESTWoz>7Mq>EjVtH&IxfF$w4c z!b-Y*H?IE4lx%E7{bu#b_Q6iqW3}xl^eu-5`Aguj<6BQ_55!RNT8}dX9yS_sO;?({ z0Nf4<8F}q|zxmMS6$LhsKdbBO&)C`74colGZVS-S(UDC(%WrN0CKk=j*>14J!__mj zY;hSkH-XR1GAV$wK|B2Ks~i?zXKiTu#>$C@iG^i9>lfE&o?BCc2Q)^~&GlA>BbmL%=Gqz}=)g%!OQVVky?RADQLKjY zwqZwIQ!^2+cmsfD4G^QGBKm+xMK6CoW4gz=TKizDA1P)Nb1GOubibS256OVt36K;K zj5_ybw%$JDt%Ym1RuA%?pjn2v-)q2vn5*ow{ryfBH_)I)*>M524ERzOHia5oChZ&= zeAQJ|pR=>6`(r5CC%w8k-rE5m%Gb{?!`J`j%vxAjn1-G{7+wcm7r00E0Am048|qaq{mnvjNo!OGI%j+b0tF9^Q*%)w%6 zd%Jj0P*4u2&hhOt7&84It)L`q6(q16i? zkWSEu!43;%*Qr3YD+UGrk5QS-UT_?x#|w`#{RVV0GBU*Z>B-5J!Fc+r+S*<~tQga^ z0Lq;VPzU4yfq1oIUL!s-1`ZC&3%`bQO%FshHNA2_m<{ahm40$vcmD17 z_4hxC0@D_-&N&qoTrLu@1J`5g*z%Uvu|IKh)4vJ}3ukMs@xMezkAZDsx7bVwJXZ68 zQ=nET#JmZBqznrTL?}|rR&Dwc2T;jB_4L`+1Aof+nLo6e7sAiskowAlDYU62(v=q2 ztzIv;)}-23#N-{8+oKVlA%{=T5 z=9lk(;dnD)a*t$741iMSd^jf{>UTrn<>iGHdsnVs7ZeeJ_S$s^0vasJsXPc36&1CZ zq7_ChM1aN;&N^(Qs;8a>uUJpP?%24v`W=oJ(FkdX=c zmVTd(HhL=K+}tmKGR86?B_$0H5AOtHm0^ph1omm)a7t%8^Syx$K73VQn!)$QqmXq( zy(J>#!M_-ng5gSF8Yo*v{r4F?t1F<9@D`k>y`f<2zP>&dPEHxX^sOo9O9xh+M(b>K z3JMBP?OH63v0ZC;ip7wj&46?`t?i&KG_rZJHS)N+x#i~N1>N2Gw!7`Ytme81Bq|Nj z6EDsjid6yTkVBnMn5{bv>!Ort|DU{2ov`w`r==XbiA)%Cd>Ad2~uvZw{ z<};2h3Ut?qV>kFCW%+5H<2Y{?*{i{Uo%nlB{Pf+96>rqeJ$AWQKcZUycVHJ0Juhh9 zSIIuMq;+8+J2Npk*;_!(wAzs0VR2H`h1U{Kw?TgRID>+TXV^>$aad@Sw3fv?&0hAu zjfO9A-Wz$UxiJwKfJR!?tq1ilJz?VV^Mc1SquA1J*o=^|@QM!({lJ&J)wAC#{%92EW|WN zhgH9bKjTne>!TsXMCK^x82b_X3>lkBemWWl>!TVIa7IC6GBU2?`HNm=28NXpiN{{x znC@Wb_x%MDaFZ?||M@|pWG%&$$Li)0@}q_Q=kW09!H}kCqz~*$?v#ZKuN8xNO1$~6 zhg79F_Rdrb@!#>!ACsk-0(@fNyuRtc zR5%O;2A&xhbBlvXU@4SM4gU_fY9JiZw_+ycB%pkfI@s~}5EV@>WDW#T0&1bm{|bzb zFQtHc5-gvV03o>Rb96bDon6KeardT+x`qZKXcVuwbd67i)W-<2w#$dhm*Ezpw?&xsf)Duk9_Ly-u1_R`k>*Eosof|rlv+fJn<4k zM*XQZ45-lN=4R5|kCGD8y;w~~asm+YpvDVeHn;r{B`Jlh?vNc9_Zj#L8t+nyP2o;A>^I4P^l$C?ysoZQ*5(G9s&x=ao z4y>uEL87Ne4Z=~j(F{1lI;*z(?UG9*arpN?6yPm$`eSYa_3Y&8O7Q(1X>eC(5F>{C zD~uqTjUcV@P4Lc$P0{WaLwA4}scWD~v~AxREK z%Vt=BCT4`zwB<$6tDX1D(Jr^2Um~Dl=G5a<8Ux1^hkyX-!*;SJ*5%1+&yx!d<= z=%o}65-p|`guJ&+-rAb=`;Q-^Z76jzpD>Z1iTPZ1PcT2`tXLpy`ajv)pbPP|Qh)#I z(O#;_tEmluzQrjZr)Yi^AzvBaIqIrhk7NRWyiMeSpLI_TBzJ`7`jxwbd*UzHqFsCd zIp8q)57GO^8+us>mIwIhtKc2b{{_QAnb&Rgx3v*8x$NX!xrE zY^p*-ngkkDC`BzJKA02w4r<)Ju$HWLs``Tk^#4>TLynH`Z!c3{ePU|%IOdvk)wgEn z<{r2>oClgd5ImFr{k!6h?U~a~1gA&?)Icr+{z|BFS-N`yDfgBRY=h^Vl}&quHGkh~ zYunc!2ym07laXAVzq!jemo1Q7Yi$+%Cgwu~n!$mbf$sF+c~vRaH_CtneZX<3aXMF5BIR{j1vyu-P=;E0F_Wwsq60su3!;&h9JZ?%A}Z2@YU93#KaO2 z6SM!S^$Vf`?K5yVI?8UIw^81P`$hxg5%xMm0udqWFUsO)t~(J=5t>Xhk@!EAWo5n1 zU-wU5b7pQ0qIzv^Z_72IBZc)yIyi6vFFFj!zE!|lJTEIw%Z7gFRCZ5I)s1}sCzyoK zGQ4yDc&UvXyu|)Y5AZWPdwW*LBiUL^@cEFO??sVV211?PKQ%UNK`?=Kr}7OF%JV3( zPR`%<>lo+ z!fRjp-+3A~It6am+1c5h9Q=LBlNMcE9!v2G4=f^GpBxKU>95T4vXb7Sx{SD_I2I6y z(9$|tyu@GmcT4q@$r-9Od0pkIcjdoldGM-Hr%YNyTRUWNsYRZS7B&u?zHg#lcx^t9 zmu;6IG<2}k)}mkl$p1$hcvgH88v4t4TxfK_V_EH~KAYKoP-=Q>@d@-wR@?m9@v`Cxk4*AF z53Osd-I=l#215dzkLKme|5o=wtr?x3cF_1-_u#|Lz)-OIAIb|VQ~1V^X|*m^cC{`C zNT7kXRK5Zx@DqB|1#HRu-l?l2JmDKbTy+a~yq57NfxWn{P5^!8sq;Mg6)7nhVd0}r z3oU*xK&Fm!rU2s!((Q>c$@oyYf(?5WY0kwr0zO}cmU||ihlZk}$xJTTa(Q@Mz8BKb z)X^CLE-q-YCdg(>c)^iCLx1VThqIkARCIKkGd*DCf&5rpdivZ++V}5lSrP%*pFaJQ zwFj&{9E)5q94<$v4=H6%^ac`($fBK6Y5p8|f_T}CYe(fGAiyaDVm9_OM9F%^F-}xF znA-?{YL8%77t0N^&Hfnhe{ky-rd&^$0@FF@LgiLIE??4R{C03BKMW5?1>q-wYrCtH zRjdxsQ{fbJTv{km@%DZVcstuffCtPjBH#x{9>6mekS>@j+l8iJSU;I$Py9>h*5S(e zNLf@(9;#uEmw=bG?xx=?eVH&bF%w*#$!T}koVTxIWM*k6?L%G4ZESv9bjazCVFBd> z&`idd2s$D{^H1%6d1Yn0Gn-#PZvkL_3O4|i`>tGnYNIvV|0V+LmT$ij&>)6rEkR|! zIDVP5LhR@2a}S#VMci2({m;x`9#};MqH0~Y9>-l=ERdGZMwfjRw{;~|;TkpSIyzyw z)wo~2V1e&}WPxwtT3=1%rO!a!c{3hy-w`pa$N<5Y-ys!KxTOt;CR2YVDgBnWx7Tiwjv^Qs7z~Vz0(!+7Bfoz~Z_i?!ZpP1BB2E&%admr?_(CS~ zea!rOGHiI0PVhAm!iSOd!;FR+?69|x-;9Zb?C)r}Dx3w7m=e)GeE9H%gcniF=faNP zHlb%V$K!Y@Ja+q$$P_f3Ks3WBaU?h>i0Az;65a;_X(jrZp@OXM>1?4sF`s8Xa>olU zB+JDmDE+xWJSh=kz(Q`jbD=-0P5h(p=8*8f% zA9@DmPtr>Oyw%#yc;1Lm+V+5{FWOgzY3u7petx-)3-{omxE1NP8imZx{blPFa_<^I z1O7&{od}#LMHQf%QhY4Qh7UPaH%T zz%W$FTCp%Uw~I|V!4BoZ1UrP%;-d}cRtGLBsAo?9wp6aJu4ot;Wk9@` zGY(q*k`@(_hmSAM5I3*3mcVhjozPZ-T1jb`sRfn*llF~azz6CFYUiRYkP2whTV;l{ zrxd+8J&3CVwo0zR1RlX=|3CL$gtXFD77U)CA(->Anq Date: Fri, 18 Oct 2024 09:57:01 +0200 Subject: [PATCH 4/5] Moved links. --- "src/\303\251tude/Ada.typ" | 42 +---------------------- "src/\303\251tude/C++.typ" | 17 ---------- "src/\303\251tude/links.typ" | 66 +++++++++++++++++++++++++++++++++++- 3 files changed, 66 insertions(+), 59 deletions(-) diff --git "a/src/\303\251tude/Ada.typ" "b/src/\303\251tude/Ada.typ" index 8c52d35..95d7604 100644 --- "a/src/\303\251tude/Ada.typ" +++ "b/src/\303\251tude/Ada.typ" @@ -157,10 +157,6 @@ ], pile: [ - #let gnatstack = link( - "https://www.adacore.com/gnatpro/toolsuite/gnatstack", - "GNATstack" - ) Les outils analysant l'exécutable peuvent le faire tout autant pour les programmes #Ada. Pour les outils ciblant spécifiquement #Ada, il y @@ -369,24 +365,6 @@ tests: [ - #let aunit = link("https://github.com/AdaCore/aunit", "AUnit") - #let adatest95 = link( - "https://www.qa-systems.fr/tools/adatest-95/", - "Ada Test 95" - ) - #let avhen = link("http://ahven.stronglytyped.org/", "Avhen") - #let ldra = link("https://ldra.com/products/ldra-tool-suite/", "LDRA") - #let vectorcastAda = link( - "https://www.vector.com/int/en/products/products-a-z/software/vectorcast/vectorcast-ada/", - "VectorCAST/Ada" - ) - - - #let rtrt = link( - "https://www.ibm.com/products/rational-test-realtime", - "Rational Test RealTime" - ) - Les différents outils de tests recensés pour #Ada sont inddiqués dans la @ada-test. @@ -401,7 +379,7 @@ [*#vectorcastAda*], [UC], [++], [✓], [✓], [*#rtrt*], [UIC], [], [], [], ), - caption: [Comparaison des outils de tests pour le langage C], + caption: [Comparaison des outils de tests pour le langage #Ada], ) #aunit et #avhen sont des implémentations xUnit pour #Ada. Les fonctionnalités sont @@ -446,24 +424,6 @@ Parmi tous les compilateurs Ada, nous listons uniquement ceux qui semblent maintenus et de qualité industrielle. - #let ptcdobjada = link( - "https://www.ptc.com/en/products/developer-tools/objectada", - "PTC ObjectAda" - ) - #let ptcapexada = link( - "https://www.ptc.com/en/products/developer-tools/apexada", - "PTC ApexAda" - ) - #let gnatpro = link("https://www.adacore.com/gnatpro", "GNAT Pro") - #let gnatllvm = link("https://github.com/AdaCore/gnat-llvm", "GNAT LLVM") - #let gaoc = link( - "https://www.ghs.com/products/ada_optimizing_compilers.html", - "GreenHills Ada Optimizing Compiler") - - #let janusada = link( - "http://www.rrsoftware.com/html/blog/ja-312-rel.html", - "Janus/Ada" - ) #figure( diff --git "a/src/\303\251tude/C++.typ" "b/src/\303\251tude/C++.typ" index a726be2..25cada9 100644 --- "a/src/\303\251tude/C++.typ" +++ "b/src/\303\251tude/C++.typ" @@ -207,11 +207,6 @@ va en partie dépendre de l'utilisation d'outils tiers. tests: [ -#let boost_test = link( - "https://www.boost.org/doc/libs/1_85_0/libs/test/doc/html/index.html", - [Boost Test Library] -) -#let catch2 = link("https://github.com/catchorg/Catch2", "Catch2") Certains des outils cités pour le C fonctionnent également pour le C++. C'est le cas pour #cantata ou #parasoft par exemple. D'autres outils ou bibliothèques @@ -223,13 +218,6 @@ les rapports de test ou les possibilités de _fuzzing_. Le _mocking_ est également disponible via une extension. #catch2 propose sensiblement la même chose que #boost_test. -#let gtest = link("https://github.com/google/googletest", "Google Test") -#let google = link("https://about.google", "Google") - -#let safetynet = link( - "https://bitbucket.org/rajinder_yadav/safetynet/src/master/", - "Safetynet" -) #gtest est un cadre logiciel proposé par #google pour le test unitaire. Il est très complet et utilisé pour de gros projets. Il permet de découvrir les @@ -246,11 +234,6 @@ Ruby. L'outil semble cependant moins mature et complet que #gtest. conjointement avec d'autres outils de tests unitaires pour simuler des comportements de fonctions ou de classes à la manière de #opmock. -#let testwell_ctc = link( - "https://www.verifysoft.com/fr_ctcpp.html", - "Testwell CTC++" -) - #testwell_ctc est un outil commercial qui, comme #cantata, #parasoft ou #vectorcast que nous avons déjà présenté dans la partie C, couvre différents types de tests diff --git "a/src/\303\251tude/links.typ" "b/src/\303\251tude/links.typ" index 6cf3c66..e1f2143 100644 --- "a/src/\303\251tude/links.typ" +++ "b/src/\303\251tude/links.typ" @@ -208,4 +208,68 @@ #let windbg = link("https://docs.microsoft.com/en-us/windows-hardware/drivers/debugger/debugger-download-tools")[WinDBG] -#let rr = link("https://rr-project.org/")[rr] \ No newline at end of file +#let rr = link("https://rr-project.org/")[rr] + +#let boost_test = link( + "https://www.boost.org/doc/libs/1_85_0/libs/test/doc/html/index.html", + [Boost Test Library] +) +#let catch2 = link("https://github.com/catchorg/Catch2", "Catch2") + +#let gtest = link("https://github.com/google/googletest", "Google Test") +#let google = link("https://about.google", "Google") + +#let safetynet = link( + "https://bitbucket.org/rajinder_yadav/safetynet/src/master/", + "Safetynet" +) + + +#let testwell_ctc = link( + "https://www.verifysoft.com/fr_ctcpp.html", + "Testwell CTC++" +) + + +#let aunit = link("https://github.com/AdaCore/aunit", "AUnit") +#let adatest95 = link( + "https://www.qa-systems.fr/tools/adatest-95/", + "Ada Test 95" +) +#let avhen = link("http://ahven.stronglytyped.org/", "Avhen") +#let ldra = link("https://ldra.com/products/ldra-tool-suite/", "LDRA") +#let vectorcastAda = link( + "https://www.vector.com/int/en/products/products-a-z/software/vectorcast/vectorcast-ada/", + "VectorCAST/Ada" +) + + +#let rtrt = link( + "https://www.ibm.com/products/rational-test-realtime", + "Rational Test RealTime" +) + + +#let ptcdobjada = link( + "https://www.ptc.com/en/products/developer-tools/objectada", + "PTC ObjectAda" +) +#let ptcapexada = link( + "https://www.ptc.com/en/products/developer-tools/apexada", + "PTC ApexAda" +) +#let gnatpro = link("https://www.adacore.com/gnatpro", "GNAT Pro") +#let gnatllvm = link("https://github.com/AdaCore/gnat-llvm", "GNAT LLVM") +#let gaoc = link( + "https://www.ghs.com/products/ada_optimizing_compilers.html", + "GreenHills Ada Optimizing Compiler") + +#let janusada = link( + "http://www.rrsoftware.com/html/blog/ja-312-rel.html", + "Janus/Ada" +) + +#let gnatstack = link( + "https://www.adacore.com/gnatpro/toolsuite/gnatstack", + "GNATstack" +) From 88440aa7cd81f0465bd53e9c9142c85b5e08650e Mon Sep 17 00:00:00 2001 From: Julien Blond Date: Fri, 18 Oct 2024 10:48:25 +0200 Subject: [PATCH 5/5] Added slides. --- src/base.typ | 4 +- ...mlPro_PPAQSE-COTS_pr\303\251sentation.typ" | 623 +++++++++++++----- 2 files changed, 471 insertions(+), 156 deletions(-) diff --git a/src/base.typ b/src/base.typ index 82c3a74..0e4f1ef 100644 --- a/src/base.typ +++ b/src/base.typ @@ -90,7 +90,9 @@ text(size: 40pt, [*#title*]), text(size: 30pt, [*#subtitle*]), authors, - body + body, + v(1fr), + image("imgs/by.png") ) ) ] diff --git "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" index b2872ae..1c0ddf7 100644 --- "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" +++ "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" @@ -20,7 +20,7 @@ - PME française créée en 2011 - ADN recherche et liens étroits avec la recherche académique. - OCaml : core team, opam & optimisations - - R&D langages (DSL) & dette technque (Cobol) + - R&D langages (DSL) & dette technique (Cobol) - Méthodes formelles (Alt-Ergo) - Certification Sécurité (CC EAL6+) - Formations (OCaml, Rust, Coq) @@ -56,157 +56,267 @@ ] #slide[ - == C : Paradigme + = C++ - Essentiellement *impératif* et *procédural* + - Créé en 1979 par Bjarne Stroustrup + - C++ = C + classes + templates + exceptions + ... + - Mêmes usages que le C mais censé être plus efficace/productif + - Standardisé : C++98, C++03, C++11, C++14, C++17, C++20, C++23... + - ... mais sémantique indéterministe. +] - ```c - int add_value(struct state *s, int v) - { - int code = KO; - if (nullptr != s) { - s->acc += v; - code = OK; - } - return code; - } - ``` +#slide[ + = Ada + + - Initié par le DoD dans les années 1970 + - Langage de programmation de haut niveau pour la sûreté + - Standardisé : Ada83, Ada95, Ada2005, Ada2012, Ada2023 + - Sémantique claire +] + +#slide[ + = Scade + + - Créé dans les années 1990 par VERIMAG/VERILOG + - Repris par Esterel Technologies/Ansys + - Langage de programmation graphique basé sur Lustre + - Propriétaire + - Sémantique déterministe ] #slide[ - == C : Mécanismes de protection intrinsèques + = OCaml + + - Créé en 1996 par l'INRIA + - Lignée des langages ML + - Lien étroit avec Coq + - Centré sur l'algorithmique et la simplicité + - Sémantique mathématique issue du $lambda$-calcul +] + +#slide[ + = Rust + + - Créé dans les années 2000 chez Mozilla + - Première version en 2015 + - C++ amélioré + - Qualifications/standarisation en cours +] + +#slide[ + = Paradigmes #align( center, table( - columns: (auto, auto), - align: (left, left), - align(center)[*Avantage*], align(center)[*Inconvénient*], - [Système de type], [Trop rudimentaire et laxe], - [ ], [Gestion manuelle des pointeurs], - [Analyses des compilateurs], [ - - Pas activées par défaut - - Pas standardisées - ], + columns: (auto, auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Impératif*], + align(center)[*Fonctionnel*], + align(center)[*Objet*], + align(center)[*Déclaratif*], + [C], [✓], [\~], [], [], + [C++], [✓], [\~], [✓], [], + [Ada], [✓], [], [\~], [], + [Scade], [], [], [], [_dataflow_, graphique], + [OCaml], [✓], [✓], [✓], [], + [Rust], [✓], [✓], [\~], [], ) ) ] #slide[ - == C : Compilateurs + = Mécanismes de protection intrinsèques #align( center, table( - columns: (auto, auto), - align: (left, left), - align(center)[*Compilateur*], align(center)[*Remarques*], - [GCC], [La référence], - [Clang], [Le challenger], - [icc/icx], [Intel], - [MSVC], [Microsoft], - [AOCC], [AMD], - [sdcc], [microcontrôleurs], - [CompCert], [Vérifié formellement], + columns: (auto, auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Typage*], + align(center)[*Pointeurs*], + align(center)[*Mémoire*], + align(center)[*Contrôles*], + [C], [😕], [😨], [😨], [😕], + [C++], [😕], [😨], [😨], [😐], + [Ada], [😊], [😌], [😨], [😊], + [Scade], [😊], [😊], [😊], [😊], + [OCaml], [😃], [😊], [😃], [😊], + [Rust], [😊], [😕], [😌], [😊], ) ) ] #slide[ - == C : Interfaçage + = Compilateurs - #v(2cm) - - Le C permet d'écrire de l'assembleur dans le texte. + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Compilateurs*], + [C], [GCC, Clang/LLVM, icx, MSVC, AOCC, sdcc, CompCert, ...], + [C++], [G++, Clang/LLVM, icx, MSVC, AOCC, C++ Builder, ...], + [Ada], [GNAT (GCC), GNAT Pro/LLVM, GreenHills Ada, PTC, Janus/Ada], + [Scade], [Scade Suite], + [OCaml], [OCaml (ocamlc, ocamlopt)], + [Rust], [rustc] + ) + ) +] - - Il sert de cible pour la plupart des langages. +#slide[ + = Interfaçage + #align( + center, + table( + columns: (auto, auto), + align: (left, left, left, left), + align(center)[*Langage source*], align(center)[*Langage(s) cibles(s)*], + [C], [ASM], + [C++], [C, ASM], + [Ada], [C], + [Scade], [C, Ada (out)], + [OCaml], [C], + [Rust], [C] + ) + ) ] + #slide[ - == C : Adhérence + = Adhérence - #v(2cm) - Aucune, il faut juste un compilateur pour l'architecture cible. + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Adhérence*], + [C], [], + [C++], [], + [Ada], [], + [Scade], [], + [OCaml], [POSIX (natif), VM (objet)], + [Rust], [] + ) + ) ] #slide[ - == C : Gestionnaires de paquets + = Gestionnaires de paquets - - Deux gestionnaires classiques : Conan & vcpkg - - Un gestionnaire de _vendoring_ : Clib - - Possibibilité d'utiliser des gestionnaires agnostriques (Nix, 0install, ...) + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Gestionnaire(s) de paquet(s)*], + [C], [Clib, Conan, vcpkg], + [C++], [Buckaroo, Conan, vcpkg], + [Ada], [Alire], + [Scade], [], + [OCaml], [opam], + [Rust], [Cargo] + ) + ) - Pour les systèmes embarqués : Buildroot, Yocto, ... ont leur propre - _packaging_. + - Agnotisques: Nix, 0install, opam, ... + - Systèmes embarqué : Yocto, Buildroot, ... ] #slide[ - == C : Communauté + = Communauté - - Très large - - Entreprises - - OS (FSF) - - Système (Linux) - - Embarqué + #[ + #set text(size: 18pt) + #align( + center, + table( + columns: (auto, auto, auto, auto, auto), + align: (left, left), + align(center)[*Langage*], + align(center)[*Fondation(s)/Association(s)*], + align(center)[*Entreprise(s)*], + align(center)[*Recherche*], + align(center)[*Volume*], + [C], [FSF], [+++], [], [+++], + [C++], [FSF], [+++], [], [+++], + [Ada], [Ada Europe, Ada Resource Association, Ada France], [Adacore, +], [], [+], + [Scade], [], [Ansys], [Verimag], [+], + [OCaml], [OSF], [Jane Street, OCamlPro, Tarides, +], [INRIA], [+], + [Rust], [RF, Rust France], [AWS, Mozilla, +], [], [++], + ) + ) + ] ] #slide[ - == C : Debugueurs + = Debugueurs #{ set text(size: 16pt) figure( table( - columns: (auto, auto, auto), - [*Debugueur*], [*Architectures*], [*License*], - [*#linaro*], [x86-64, ARM, PowerPC, Intel Xeon Phi, CUDA], [Propriétaire], - [*#gdb*], [x86, x86-64, ARM, PowerPC, SPARC, ...], [GPLv3], - [*#lldb*], [i386, x86-65, AArch64, ARM], [Apache v2], - [*#totalview*], [x86-64, ARM64, CUDA], [Propriétaire], - [*#undo*], [x86-64], [Propriétaire], - [*#valgrind*], [x86, x86-64, PowerPC, ARMv7], [GPL], - [*#vsd*], [x86, x86-64], [Propriétaire], - [*#windbg*], [x86, x86-64], [Gratuit], - [*#rr*], [x86, x86-64, ARM], [GPLv2], + columns: (auto, auto), + align(center)[*Langage*], + align(center)[*Debugueur(s)*], + [C], [#gdb, #lldb, #totalview, #undo, #valgrind, #vsd, #windbg, #rr, #linaro], + [C++], [#gdb, #lldb, ...], + [Ada], [#gdb, #lldb], + [Scade], [Scade Suite], + [OCaml], [ocamldebug (objet), #gdb, #lldb, ...], + [Rust], [#gdb, #lldb, #windbg] + ) ) } ] #slide[ - == C : Tests + = Tests - #figure( + #align( + center, table( - columns: (auto, auto, auto, auto, auto), - [*Outil*], [*Tests*], [*Generation*], [*Gestion*], [_*mocking*_], - [*#cantata*], [UIRC], [+++], [✓], [], - [*#criterion*], [U], [+], [], [], - [*#libcester*], [U], [+], [✓], [✓], - [*#novaprova*], [U], [+], [✓], [✓], - [*#opmock*], [U], [++], [], [✓], - [*#parasoft*], [UC], [++], [✓], [], - [*#TPT*], [UINC], [+++], [✓], [], - [*#vectorcast*], [UC], [++], [✓], [✓], + columns: (auto, auto), + [C], [#cantata, #parasoft, #TPT, #vectorcast, ...], + [C++], [#cantata, #parasoft, #TPT, #vectorcast, #testwell_ctc, #boost, #gtest, ...], + [Ada], [#aunit, #adatest95, #avhen, #ldra, #vectorcastAda, #rtrt], + [Scade], [Scade Suite], + [OCaml], [#ounit, #alcotest, #qcheck, #crowbar, PPX, Cram, ...], + [Rust], [_builtin_, quickcheck, proptest, mockall, ...] + ), - ) + ) ] #slide[ - == C : Parsing - - Il existe beaucoup d'outils d'analyse syntaxique en C mais les plus - connus/matures qui suffisent dans la grande majorité des cas sont: - - Flex/Bison - - ANTLR + = Parsing + #align( + center, + table( + columns: (auto, auto), + [C], [Flex/Bison, ANTLR, ...], + [C++], [Flex/Bison, ANTLR, ...], + [Ada], [AFlex/AYacc], + [Scade], [], + [OCaml], [sedlex, ulex, Menhir, ocamllex, ocamlyacc, angstrom, dypgen, ...], + [Rust], [LALRPOP, Hime, Syntax] + ) + ) ] #slide[ - == C : Méta-programmation + = Méta-programmation (C) - Le préprocesseur permet de faire précalculer des expressions simples par le compilateur (souvent inutile) @@ -224,9 +334,69 @@ ] #slide[ - == C : Dérivation + = Méta-programmation (C++) + + Les _templates_ sont Turing-complets et permettent de calculer virtuellement + n'importe quoi qui ne dépende pas d'une IO. + ```cpp + template struct Fact { + enum {Value = N * Fact::Value}; + }; + template<> struct Fact<0> { + enum {Value = 1}; + }; + unsigned int x = Fact<4>::Value; + ``` +] + +#slide[ + = Méta-programmation (Ada & Scade) + + Pas de support de méta-programmation. +] + +#slide[ + = Méta-programmation (OCaml) + + Les PPX permettent de transformer le code source avant la compilation + + ```ocaml + let main () = + [%init 42]; + let v = some_calculus () in + [%do_something v] + ``` +] + +#slide[ + = Méta-programmation (Rust) + + Les macros permettent de transformer le code source avant la compilation + + #[ + #set text(size: 18pt) + ```rust + macro_rules! vec { + ($($x:expr),*) => { + { + let mut temp_vec = Vec::new(); + $(temp_vec.push($x);)* + temp_vec + } + }; + } + ``` + + ```rust + let v = vec![1, 2, 3]; + ``` + ] +] + +#slide[ + = Dérivation (C) - - Les macros permettent une forme archaïque de dérivation + Les macros permettent une forme archaïque de dérivation ```c #define COULEUR X(ROUGE, 0xFF0000) X(VERT, 0x00FF00) X(BLEU, 0x0000FF) #define X(c, v) c = v, @@ -235,105 +405,248 @@ ``` ] +#slide[ + = Dérivation (C++) + + On peut avoir une forme de dérivation via les _templates_: + ```cpp + template + struct is_pointer { + static const bool value = false; + }; + template + struct is_pointer { + static const bool value = true; + }; + ``` +] + +#slide[ + = Dérivation (Ada & Scade) + + Pas de support de dérivation. +] + +#slide[ + = Dérivation (OCaml) + + Les PPX permettent de transformer le code source avant la compilation + + ```ocaml + type couleur = Rouge | Vert | Bleu | RGB of int * int * int + [@@deriving show] + + (* val show : couleur -> string + val pp_couleur : Format.formatter -> couleur -> unit *) + ``` +] + +#slide[ + = Dérivation (Rust) + + Les macros permettent de transformer le code source avant la compilation + + ```rust + #[derive(Debug)] + struct Point { + x: i32, + y: i32, + } + ``` +] + + + #slide[ - == C : Runtime Errors - - Les analyseurs statiques corrects permettant de se prémunir contre des - erreurs à _runtime_ sont: - - #astree - - #eclair - - #framac - - #polyspace - - #tisanalyser + = Runtime Errors + + Analyseurs sans faux négatifs: + + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#astree, #eclair, #framac, #polyspace, #tisanalyser], + [C++], [#astree (C++17), #framac (?)], + [Ada], [#codepeer, #polyspace, #spark], + [Scade], [Scade suite ?, + outils C/Ada sur le code généré], + [OCaml], [], + [Rust], [(Mirai)], + ) + ) ] #slide[ - == C : Formalisation + = Formalisation - #[ - #set text(size: 18pt) - - Par transpilation (automatique ou manuelle) vers Coq (VerifiedC): - #align(center, - grid( - columns: (auto, auto, auto, auto, auto), - [C], [$=>$], [Coq], [$=>$], [Preuves (Hoare, WP)] - ) - ) + Il y a globalement deux approches : - - Par annotation et preuve (semi) automatiques (Frama-C, RedefinedC, VerCors): + - Par transpilation de ou vers Coq (ou autre) + - Langage $=>$ Coq $=>$ Preuves (Hoare, WP) + - Coq + Preuves $=>$ Langage + - Par annotation et preuve (semi) automatiques: + #[ + #set text(size: 16pt) ```c /*@ requires \valid(a) && \valid(b); - @ ensures A: *a == \old(*b) ; - @ ensures B: *b == \old(*a) ; - @ assigns *a,*b ; - @*/ + @ ensures A: *a == \old(*b) ; + @ ensures B: *b == \old(*a) ; + @ assigns *a,*b ; + @*/ void swap(int *a,int *b); ``` - ] - + ] ] #slide[ - == C : WCET + = WCET - Il existe plusieurs outils basés sur une analyse statique binaire : - - #chronos (IR) - - #bound-T - - #aiT - - #sweet (IR) - - #otawa (modulaire) - - #rapidtime + Le WCET par analyse statique fonctionne par analyse du binaire avec les + contraintes de l'architecture cible. + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#chronos, #bound-T, #aiT, #sweet, #otawa, #rapidtime], + [C++], [outils C], + [Ada], [#rapidtime, #aiT], + [Scade], [#aiT], + [OCaml], [outils C], + [Rust], [outils C], + ) + ) +] + +#slide[ + = Pile + L'analyse statique de la pile fonctionne également par analyse du + binaire: + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#stackanalyser, #armlink, #gcc], + [C++], [outils du C], + [Ada], [#gnatstack], + [Scade], [#stackanalyser], + [OCaml], [outils du C (natif)], + [Rust], [outils du C], + ) + ) ] #slide[ - == C : Pile + = Qualité numérique + + #align( + center, + table( + columns: (auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs statiques*], + align(center)[*Calcul dynamique*], + [C], [#fluctuat, #astree, #polyspace, #gappa (+ annotations)], [#cadna, #mpfr, #gmp], + [C++], [#astree, #polyspace], [#cadna, #mpfr, #boost, #xsc], + [Ada], [_builtin_, #polyspace, #spark (+annotations)], [#mpfr, #gmp], + [Scade], [], [Scade library ?], + [OCaml], [], [#mpfr, #gmp], + [Rust], [], [biblothèques, #mpfr, #gmp], + ) + ) - Pour l'analyse statique de la pile: - - #gcc - - #stackanalyser - - #t1stack (+ annotations) - - #armlink ] #slide[ - == C : Qualité numérique + = Assurances - #[ - #set text(size: 18pt) - Se prémunir contre les erreurs numériques (overflow, précision, ...) - - par analyse statique: - - #fluctuat - - #astree - - #polyspace - - #gappa (+ annotations #framac) - - par un calcul dynamique: - - #cadna - - #mpfr - - #gmp - ] + #align( + center, + table( + columns: (auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Intrinsèque*], + align(center)[*Externe*], + [C], [😨], [😊], + [C++], [😕], [😕], + [Ada], [😊], [😊], + [Scade], [😊], [😊], + [OCaml], [😊], [😨], + [Rust], [😊], [😕], + ) + ) +] + +#slide[ + + = Assurances / Coût (Sécurité) + #align( + center, + table( + columns: (auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Intrinsèque*], + align(center)[*Externe*], + align(center)[*Coût*], + [C], [😨], [😊], [😨], + [C++], [😕], [😕], [😕], + [Ada], [😊], [😊], [😕], + [Scade], [😊], [😊], [😌], + [OCaml], [😊], [😨], [😊], + [Rust], [😊], [😕], [😕], + ) + ) ] #slide[ - == C : Assurances - Niveau d'assurance donné par le C est paradoxal : - - quasiment pas de sécurité intrinsèque - - l'histoire et l'usage ont apporté des outils externes qui fiabilisent le C + = Critique - Le développpement reste relativement peu productif et coûteux: - - même un bon programmeur fait des erreurs - - A/R entre services de développement et de vérification - - licences, formations, ... + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Domaines critiques*], + [C], [Tous], + [C++], [Tous], + [Ada], [Spatial, Aéronautique, Ferroviaire ], + [Scade], [Aéronautique, Ferroviaire, Nucléaire], + [OCaml], [Outillage (Astree, KCG, ...)], + [Rust], [], + ) + ) ] #slide[ - == C : Critique - Le C est utilisé dans tous les domaines critiques soit - - directement pour écrire le système (en entier ou au moins les interfaces - avec le matériel); - - indirectement comme langage cible (#Ada, #Scade, ...). + = Conclusion + + - Quand on peut, privilégier les langages métiers + - OCaml est souvent un bon choix pour l'outillage + - Rust est à la mode mais encore jeune pour être recommandé sans réserve + - Innover pour s'adapter aux nouveaux besoins/contraintes + ] + +#slide[ + + #v(3cm) + #align(center)[*Questions ?*] + +] \ No newline at end of file