Commit e2502531 authored by Dario Pinto's avatar Dario Pinto
Browse files

Merge branch 'master' into 'master'

Add a bunch of FR articles + mappings + fix sabotage

See merge request OCamlPro/www!85
parents b1ccbdb0 a871e03c
......@@ -8,6 +8,8 @@ type article =
; url : string
}
exception ContentDoesntExistSoPleaseRaiseA404
let alt_ergo_footer =
{|
> ### **About Alt-Ergo**
......@@ -296,7 +298,7 @@ let links_to_home_pages =
</a>
</p>
</div>
<div class="col-4">
<div class="col-4">
<p class="toplinks">
<a href="/blog/category">
Categories
......@@ -394,9 +396,12 @@ let given_category category =
(fun article -> String.equal (normalize_url article.category) category)
articles_by_date
in
let category = (List.hd articles_of_category).category in
Format.asprintf {|<h1 id="page-title">Articles on %s</h1>%s%a@.|} category
links_to_home_pages pp_blog_posts articles_of_category
match articles_of_category with
| [] -> raise ContentDoesntExistSoPleaseRaiseA404
| _l ->
let category = (List.hd articles_of_category).category in
Format.asprintf {|<h1 id="page-title">Articles on %s</h1>%s%a@.|} category
links_to_home_pages pp_blog_posts articles_of_category
(** [given_author ocp_author] Displays the list of articles written by a given
[ocp_author] *)
......@@ -410,13 +415,16 @@ let given_author ocp_author =
article.authors )
articles_by_date
in
let authors = (List.hd articles_of_author).authors in
let author =
List.find (fun auth -> String.equal (normalize_url auth) ocp_author) authors
in
( Format.asprintf {|<h1 id="page-title">Articles by %s</h1>%s%a@.|} author
links_to_home_pages pp_blog_posts articles_of_author
, author )
match articles_of_author with
| [] -> raise ContentDoesntExistSoPleaseRaiseA404
| _l ->
let authors = (List.hd articles_of_author).authors in
let author =
List.find (fun auth -> String.equal (normalize_url auth) ocp_author) authors
in
( Format.asprintf {|<h1 id="page-title">Articles by %s</h1>%s%a@.|} author
links_to_home_pages pp_blog_posts articles_of_author
, author )
(** [given_tag tag] Displays the list of articles tagged with given [tag] *)
let given_tag tag =
......@@ -429,13 +437,16 @@ let given_tag tag =
article.tags )
articles_by_date
in
let tag =
List.find
(fun t -> String.equal (normalize_tag t) tag)
(List.hd articles_with_tag).tags
in
Format.asprintf {|<h1 id="page-title">Articles tagged with %s</h1>%s%a@.|} tag
links_to_home_pages pp_blog_posts articles_with_tag
match articles_with_tag with
| [] -> raise ContentDoesntExistSoPleaseRaiseA404
| _l ->
let tag =
List.find
(fun t -> String.equal (normalize_tag t) tag)
(List.hd articles_with_tag).tags
in
Format.asprintf {|<h1 id="page-title">Articles tagged with %s</h1>%s%a@.|} tag
links_to_home_pages pp_blog_posts articles_with_tag
(** [category_home] This is the home page for all available categories on the
Blog, along with number of articles of given category *)
......
title=Introduction aux RPCs dans Tezos : exemple d’un portefeuille (wallet) simple
authors=Fabrice Le Fessant
date=2018-11-20
category=Blockchains
tags=tezos,rpc,fr
Dans cet article technique, nous introduisons brièvement les RPCs dans Tezos à travers un exemple simple montrant comment le client Tezos
interagit avec le noeud lors d’une instruction de transfert. Les RPCs de Tezos sont des requêtes HTTP (GET ou POST) auxquelles les noeuds Tezos
répondent dans un fichier au format JSON. Elles sont la seule façon pour les wallets d’interagir avec [Read more…](/2018/11/15/an-introduction-to-tezos-rpcs-a-basic-wallet/)
title=Tezos et OCamlPro
authors=Fabrice Le Fessant
date=2019-01-31
category=Blockchains
tags=tezos,OCamlPro,fr
Tezos est aujourd’hui un projet open source, un réseau international développé par des équipes sur plus de cinq continents. Dans la genèse du
projet, l’entreprise française OCamlPro, qui développe encore aujourd’hui de nombreux projets liés à Tezos (TZscan, Liquidity, etc.), a
joué un rôle particulièrement important. C’est en effet en son sein que des ingénieurs-chercheurs ont posé les premières pierres du code, en
étroite collaboration avec Arthur Breitman, l’architecte du projet, et DLS pendant plusieurs années. Nous nous réjouissons aujourd’hui de
l’essor qu’a pris le projet.
Arthur et OCamlPro
(publication conjointe)
title=Optimisation du stockage dans Tezos : une branche de test sur Gitlab
authors=Fabrice Le Fessant
date=2019-02-04
category=Blockchains
tags=tezos,optimisation,fr
Ce troisième article consacré à l’amélioration du stockage dans Tezos fait suite à l’annonce de la mise à disposition d’une image docker pour
les beta testeurs souhaitant essayer notre système de stockage et garbage collector.
Voir [Improving Tezos Storage : Gitlab branch for testers](/2019/02/04/improving-tezos-storage-gitlab-branch-for-testers/)
title=Release de Techelson, moteur de tests pour Michelson et Liquidity
authors=Adrien Champion
date=2019-03-05
category=Blockchains
tags=techelson,fr
Nous sommes fiers d’annoncer la première release de Techelson, moteur d’exécution de tests pour Michelson. Les programmeurs Liquidity peuvent également l’utiliser.
Voir [Techelson, a test execution engine for Michelson](/2019/03/05/techelson-a-test-execution-engine-for-michelson/).
title=Résultats de la SMT-Comp 2019 pour Alt-Ergo
authors=Albin Coquereau
date=2019-07-10
category=Formal Methods
tags=alt-ergo,fr
Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop&nbsp; SMT de la [22e conférence SAT](https://smt2019.galois.com/). Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo [prend en charge](/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap/) le standard [SMT-LIB 2](https://smtlib.cs.uiowa.edu/).
> Alt-Ergo est un SAT solveur open-source maintenu et distribué par OCamlPro, et financé entre autres grâce à plusieurs projets de R&D collaborative (BWare, SOPRANO, Vocal, LChip).
> Si vous êtes un utilisateur d’Alt-Ergo, songez à rejoindre le [Club des Utilisateurs d’Alt-Ergo](https://alt-ergo.ocamlpro.com/#club)! L’histoire de ce logiciel remonte à 2006, où il est né de recherches académiques conjointes entre Inria et le CNRS dans le laboratoire du LRI. Il est depuis septembre 2013 maintenu, développé&nbsp; et distribué par OCamlPro (voir l’historique des [versions passées](https://alt-ergo.ocamlpro.com/#releases)).
> *Si vous êtes curieux des activités d’OCamlPro dans le domaine des méthodes formelles, vous pouvez lire le court témoignage d’un [client heureux](http://ocamlpro.com/clients-partners/#mitsubishi-merce).*
Voir [](/2019/07/09/alt-ergo-participation-to-the-smt-comp-2019/)
......@@ -2,7 +2,7 @@ title=Réunion annuelle du Club des utilisateurs d’Alt-Ergo
authors=Aurore Dromby
date=2020-03-03
category=Formal Methods
tags=alt-ergo
tags=alt-ergo,fr
![Alt-Ergo meeting](assets/img/altergo-meeting.jpeg)
![Logo Alt-Ergo](../assets/img/logo_altergo.png)
......@@ -23,4 +23,4 @@ Nos membres sont particulièrement intéressés par les points suivants :
– L’amélioration du support de l’arithmétique non linéaire dans Alt-Ergo
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](category/formal_methods) sur ce blog.
\ No newline at end of file
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](category/formal_methods) sur ce blog.
......@@ -2,7 +2,7 @@ title=Tutoriel Format
authors=OCamlPro
date=2020-06-01
category=Trainings
tags=tutoriel,format,documentation
tags=tutoriel,format,documentation,fr
*Article écrit par Mattias.*
......
......@@ -2,7 +2,7 @@ title=[Interview] Sylvain Conchon rejoint OCamlPro
authors=Aurore Dombry
date=2020-06-05
category=OCamlPro
tags=formal methods,interview,sylvain,conchon
tags=formal methods,interview,sylvain,conchon,fr
![](/blog/assets/img/picture_sylvainconchon.jpg)
......
......@@ -2,7 +2,7 @@ title=Réunion annuelle du Club des utilisateurs d’Alt-Ergo 2021
authors=OCamlPro
date=2021-04-29
category=Formal Methods
tags=alt-ergo
tags=alt-ergo,fr
La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.
......
title=Détection de fonctions d’identité dans Flambda
authors=Leo Boitel
date=2021-07-16
category=OCaml
tags=ocaml,flambda,fr
> Au cours de discussions parmi les développeurs OCaml sur le type vide ([PR#9459](https://github.com/ocaml/ocaml/issues/9459)), certains caressaient l’idée d’annoter des fonctions avec un attribut indiquant au compilateur que la fonction devrait être triviale, et toujours renvoyer une valeur strictement équivalente à son argument.
> Nous étions curieux de voir si l’implémentation d’une telle fonctionnalité serait possible et nous avons publié une offre de stage pour explorer ce sujet.
> L’équipe Compilation d’OCamlPro a ainsi accueilli Léo Boitel durant trois mois pour se consacrer à ce sujet, avec Vincent Laviron pour encadrant. Nous sommes fiers des résultats auxquels Léo a abouti !
>
> Voici ce que Léo en a écrit 🙂
### Description du problème
Le typage fort d’OCaml est un de ses grands avantages : il permet d’écrire du code plus sûr grâce à la capacité d’abstraction qu’il offre. La plupart des erreurs de conception se traduiront directement en erreur de typage, et l’utilisateur ne peut pas faire d’erreur avec la manipulation de la mémoire puisqu’elle est entièrement gérée par le compilateur.
Cependant, ces avantages empêchent l’utilisateur de faire certaines optimisations lui-même, en particulier celles liées aux représentations mémoires puisqu’il n’y accède pas directement.
Un cas classique serait le suivant :
```Ocaml
type return = Ok of int | Failure
let id = function
| Some x -> Ok x
| None -> Failure
```
Cette fonction est une identité, car la représentation mémoire de `Some x` et de `Ok x` est la même (idem pour `None` et `Failure`). Cependant, l’utilisateur ne le voit pas, et même s’il le voyait, il aurait besoin de cette fonction pour conserver un typage correct.
Un autre exemple serait le suivant:
Another good example would be this one:
```Ocaml
type record = { a:int; b:int }
let id (x,y) = { a = x; b = y }
```
Même si ces fonctions sont des identités, elles ont un coût : en plus de nous coûter un appel, elles réallouent le résultat au lieu de nous retourner leur argument directement. C’est pourquoi leur détection permettrait des optimisations intéressantes.
### Difficultés
Si on veut pouvoir détecter les identités, on se heurte rapidement au problème des fonctions récursives : comment définir l’identité pour ces dernières ? Est-ce qu’une fonction peut-être l’identité si elle ne termine pas toujours, voire jamais ?
Une fois qu’on a défini l’identité, le problème est la preuve qu’une fonction est bien l’identité. En effet, on veut garantir à l’utilisateur que cette optimisation ne changera pas le comportement observable du programme.
On veut aussi éviter d’ajouter des failles de sûreté au typage. Par exemple, si on a une fonction de la forme suivante:
```Ocaml
let rec fake_id = function
| [] -> 0
| t::q -> fake_id (t::q)
```
Une preuve naïve par induction nous ferait remplacer cette fonction par l’identité, car `[]` et `0` ont la même représentation mémoire. C’est dangereux car le résultat d’une application à une liste non-vide sera une liste alors qu’il est typé comme un entier (voir exemples plus bas).
Pour résoudre ces problèmes, nous avons commencé par une partie théorique qui a occupé les trois quarts du stage, pour finir par une partie pratique d’implémentation dans Flambda.
### Résultats théoriques
Pour cette partie, nous avons travaillé sur des extensions de lambda-calcul, implémentées en OCaml, pour pouvoir tester nos idées au fur et à mesure dans un cadre plus simple que Flambda.
#### Paires
Nous avons commencé par un lambda calcul auquel on ajoute seulement des paires. Pour effectuer nos preuves, on annote toutes les fonctions comme des identités ou non. On prouve ensuite ces annotations en β-réduisant le corps des fonctions. Après chaque réduction récursive, on applique une règle qui dit qu’une paire composée des deux projections d’une variable est égale à la variable. On ne réduit pas les applications, mais on les remplace par l’argument si la fonction est annotée comme une identité.
On garde ainsi une complexité raisonnable par rapport à une β-réduction complète qui serait évidemment irréaliste pour de gros programmes.
On passe ensuite à l’ordre supérieur en permettant des annotations de la forme `Annotation → Annotation`. Les fonctions comme `List.map` peuvent donc être représentées comme `Id → Id`. Bien que cette solution ne soit pas complète, elle couvre la grande majorité des cas d’utilisation.
#### Reconstruction de tuples
On passe ensuite des paires aux tuples de taille arbitraire. Cela complexifie le problème : si on construit une paire à partir des projections des deux premiers champs d’une variable, ce n’est pas forcément la variable, puisqu’elle peut avoir plus de champs.
On a alors deux solutions : tout d’abord, on peut annoter les projections avec la taille du tuple pour savoir si on reconstruit la variable en entier. Par exemple, si on reconstruit une paire avec deux projections d’un triplet, on sait qu’on ne peut pas simplifier cette reconstruction.
L’autre solution, plus ambitieuse, est d’adopter une définition moins stricte de l’égalité, et de dire qu’on peut remplacer, par exemple, `(x,y)` par `(x,y,z)`. En effet, si la variable a été typée comme une paire, on a la garantie qu’on accédera jamais au champ `z` de toute façon. Le comportement du programme sera donc le même si on étend la variable avec des champs supplémentaires.
Utiliser l’égalité observationnelle permet d’éviter beaucoup d’allocations, mais elle peut utiliser plus de mémoire dans certains cas : si le triplet cesse d’être utilisé, il ne sera pas désalloué par le Garbage Collector (GC), et le champ `z` restera donc en mémoire pour rien tant que `(x,y)` est utilisé.
Cette approche reste intéressante, au moins si on donne la possibilité à l’utilisateur de l’activer manuellement pour certains blocs.
#### Récursion
On ajoute maintenant les définitions récursives à notre langage, par le biais d’un opérateur de point fixe.
Pour prouver qu’une fonction récursive est l’identité, on doit procéder par induction. La difficulté est alors de prouver que la fonction termine, pour que l’induction soit correcte.
On peut distinguer trois niveaux de preuve : la première option est de ne pas prouver la terminaison, et de laisser l’utilisateur choisir les fonctions dont il est sûr qu’elles terminent. On suppose donc que la fonction est l’identité, et on simplifie son corps avec cette hypothèse. Cette approche est suffisante pour la plupart des cas pratiques, mais son problème principal est qu’elle autorise à écrire du code qui casse la sûreté du typage, comme discuté ci-dessus.
La seconde option est de faire notre hypothèse d’induction uniquement sur des applications de la fonction sur des éléments plus “petits” que l’argument. Un élément est défini comme tel s’il est une projection de l’argument, ou une projection d’un élément plus petit. Cela n’est pas suffisant pour prouver que la fonction termine (par exemple si l’argument est cyclique), mais c’est assez pour avoir un typage sûr. En effet, cela implique que toutes les valeurs de retour possibles de la fonction sont construites (puisqu’elles ne peuvent provenir directement d’un appel récursif), et ont donc un type défini. Le typage échouerait donc si la fonction pouvait renvoyer une valeur qui n’est pas identifiable à son argument.
Finalement, on peut vouloir une équivalence observationnelle parfaite entre la fonction et l’identité pour la simplifier. Dans ce cas, la solution que nous proposons est de créer une annotation spéciale pour les fonctions qui sont l’identité quand elles sont appliquées à un objet non cyclique. On peut prouver qu’elles ont cette propriété avec l’induction décrite ci-dessus. La difficulté est ensuite de faire la simplification sur les bonnes applications : si un objet est immutable, n’est pas défini récursivement, et que tous ses sous-objets satisfont cette propriété, on le dit inductif et on peut simplifier les applications sur lui. On propage le statut inductif des objets lors de notre passe récursive d’optimisation.
###Reconstruction de blocs
La représentation des blocs dans Flambda pose des problèmes intéressants pour détecter leur égalité, ce qui est souvent nécessaire pour prouver une identité. En effet, il est difficile de détecter la reconstruction d’un bloc à l’identique.
#### Blocs dans Flambda
##### Variants
The blocks in Flambda come from the existence of variants in OCaml: one type may have several different constructors, as we can see in
```Ocaml
type choice = A of int | B of int
```
Quand OCaml est compilé vers Flambda, l’information du constructeur utilisé par un objet est perdue, et est remplacée par un tag. Le tag est un nombre contenu dans un entête de la représentation mémoire de l’objet, et est un nombre entre `0` et `255` représentant le constructeur de l’objet. Par exemple, un objet de type choice aurait le tag `0` si c’est un `A` et `1` si c’est un `B`.
Le tag est ainsi présent dans la mémoire à l’exécution, ce qui permet par exemple d’implémenter le pattern matching de OCaml comme un switch en Flambda, qui fait de simples comparaisons sur le tag pour décider quelle branche prendre.
Ce système nous complique la tâche puisque le typage de Flambda ne nous dit pas quel type de constructeur contient un variant, et empêche donc de décider facilement si deux variants sont égaux.
##### Généralisation des tags
Pour plus de complexité, les tags sont en faits utilisés pour tous les blocs, c’est à dire les tuples, les modules, les fonctions (en fait presque toutes les valeurs sauf les entiers et les constructeurs constants). Quand l’objet n’est pas un variant, on lui donne généralement un tag 0. Ce tag n’est donc jamais lu par la suite (puisqu’on ne fait pas de match sur l’objet), mais nous empêche de comparer simplement deux tuples, puisqu’on verra simplement deux objets de tag inconnu en Flambda.
##### Inlining
Enfin, on optimise ce système en inlinant les tuples : si on a un variant de type `Pair of int*int`, au lieu d’être représenté comme le tag de Pair et une adresse mémoire pointant vers un couple (donc un tag 0 et les deux entiers), le couple est inliné et l’objet est de la forme `(tag Pair, entier, entier)`.
Cela implique que les variants sont de taille arbitraire, qui est aussi inconnue dans Flambda.
#### Approche existante
Une solution partielle au problème existait déjà dans une Pull Request (PR) disponible [ici](https://github.com/ocaml/ocaml/pull/8958).
L’approche qui y est adoptée est naturelle : on y utilise les switchs pour gagner de l’information sur le tag d’un bloc, en fonction de la branche prise. La PR permet aussi de connaître la mutabilité et la taille du bloc dans chaque branche, en partant de OCaml (où l’information est connue puisque le constructeur est explicite dans le match), et propageant l’information jusqu’à Flambda.
Cela permet d’enregistrer tous les blocs sur lesquels on a fait un switch dans l’environnement, avec leur tag, taille et mutabilité. On peut ensuite détecter si on reconstruit l’un d’entre eux avec la primitive `Pmakeblock`.
Cette approche est malheureusement limitée puisqu’ils existe de nombreux cas où on pourrait connaître le tag et la taille du bloc sans faire de switch dessus. Par exemple, on ne pourra jamais simplifier une reconstruction de tuple avec cette solution.
#### Nouvelle approche
Notre nouvelle approche commence donc par propager plus d’information depuis OCaml. La propagation est fondée sur deux PR qui existaient sur Flambda 2, et qui annotent dans lambda chaque projection (`Pfiel`) avec des informations dérivées du typage OCaml. Une ajoute la [mutabilité du bloc](https://github.com/ocaml-flambda/ocaml/commit/fa5de9e64ff1ef04b596270a8107d1f9dac9fb2d) et l’autre [son tag et enfin sa taille](https://github.com/ocaml-flambda/ocaml/pull/53).
Notre première contribution a été d’adapter ces PRs à Flambda 1 et de les propager de lambda à Flambda correctement.
Nous avons ensuite les informations nécessaires pour détecter les reconstructions de blocs : en plus d’avoir une liste de blocs sur lesquels on a switché, on crée une liste de blocs partiellement immutables, c’est à dire dont on sait que certains champs sont immutables.
On l’utilise ainsi :
###### Découverte de blocs
Dès qu’on voit une projection, on regarde si elle est faite sur un bloc immutable de taille connue. Si c’est le cas, on ajoute le bloc correspondant aux blocs partiels. On vérifie que l’information qu’on a sur le tag et la taille est compatible avec celle des projections de ce bloc vues précédemment. Si on connaît maintenant tous les champs du bloc, on l’ajoute à notre liste de blocs connus sur lesquels on peut faire des simplifications.
On garde aussi les informations sur les blocs qu’on connaît grâce aux switchs.
###### Simplification
Cette partie est similaire à celle de la PR originale : quand on construit un bloc immutable, on vérifie si on le connaît, et le cas échéant on ne le réalloue pas.
Par rapport à l’approche originale, nous avons aussi réduit la complexité de la PR originale (de quadratique à linéaire), en enregistrant l’association de chaque variable de projection à son index et bloc original. Nous avons aussi modifié des détails de l’implémentation originale qui auraient pu créer un bug lorsque associés à notre PR.
#### Exemple
Considérons cette fonction:
```Ocaml
type typ1 = A of int | B of int * int
type typ2 = C of int | D of {x:int; y:int}
let id = function
| A n -> C n
| B (x,y) -> D {x; y}
```
Le compilateur actuel produirait le Flambda suivant:
```
End of middle end:
let_symbol
(camlTest__id_21
(Set_of_closures (
(set_of_closures id=Test.8
(id/5 = fun param/7 ->
(switch*(0,2) param/7
case tag 0:
(let
(Pmakeblock_arg/11 (field 0<{../../test.ml:4,4-7}> param/7)
Pmakeblock/12
(makeblock 0 (int)<{../../test.ml:4,11-14}>
Pmakeblock_arg/11))
Pmakeblock/12)
case tag 1:
(let
(Pmakeblock_arg/15 (field 1<{../../test.ml:5,4-11}> param/7)
Pmakeblock_arg/16 (field 0<{../../test.ml:5,4-11}> param/7)
Pmakeblock/17
(makeblock 1 (int,int)<{../../test.ml:5,17-23}>
Pmakeblock_arg/16 Pmakeblock_arg/15))
Pmakeblock/17)))
free_vars={ } specialised_args={}) direct_call_surrogates={ }
set_of_closures_origin=Test.1])))
(camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
(camlTest (Block (tag 0, camlTest__id_5_closure)))
End camlTest
```
Notre amélioration permet de détecter que cette fonction reconstruit des blocs similaires et donc la simplifie:
```
End of middle end:
let_symbol
(camlTest__id_21
(Set_of_closures (
(set_of_closures id=Test.7
(id/5 = fun param/7 ->
(switch*(0,2) param/7
case tag 0 (1): param/7
case tag 1 (2): param/7))
free_vars={ } specialised_args={}) direct_call_surrogates={ }
set_of_closures_origin=Test.1])))
(camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
(camlTest (Block (tag 0, camlTest__id_5_closure)))
End camlTest
```
#### Pistes d’amélioration
##### Relâchement de l’égalité
On peut utiliser l’égalité observationnelle étudiée dans la partie théorique pour l’égalité de blocs, afin d’éviter plus d’allocations. L’implémentation est simple :
Quand on crée un bloc, pour voir si il est alloué, l’approche normale est de regarder si chacun de ses champs est une projection connue d’un autre bloc, a le même index et si les deux blocs sont de même taille. On peut simplement supprimer la dernière vérification.
L’implémentation a été un peu plus difficile que prévu à cause de détails pratiques. Tout d’abord, on veut appliquer cette optimisation uniquement sur certains blocs annotés par l’utilisateur. Il faut donc propager l’annotation jusqu’à Flambda.
De plus, si on se contente d’implémenter l’optimisation, beaucoup de cas seront ignorés car les variables inutilisées sont simplifiées avant notre passe. Par exemple, prenons une fonction de la forme suivante :
```Ocaml
let loose_id (a,b,c) = (a,b)
```
La variable `c` sera simplifiée avant d’atteindre Flambda, et on ne pourra donc plus prouver que `(a,b,c)` est immutable car son troisième champ pourrait ne pas l’être. Ce problème est en passe d’être résolu sur Flambda 2 grâce à une PR qui propage l’information de mutabilité pour tous les blocs, mais nous n’avons pas eu le temps nécessaire pour l’adapter à Flambda 1.
### Détection d’identités récursives
Maintenant que nous pouvons détecter les reconstructions de blocs, reste à résoudre le problème des fonctions récursives.
#### Approche sans garanties
Nous avons commencé par implémenter une approche qui ne comporte pas de preuve de terminaison. L’idée est de rajouter la preuve ensuite, ou d’autoriser les fonctions qui ne terminent pas toujours à être simplifiées à condition qu’elles soient correctes au niveau du typage (voir section 7 dans la partie théorique).
Ici, on fait confiance à l’utilisateur pour vérifier ces propriétés manuellement.
Nous avons donc modifié la simplification de fonction : quand on simplifie une fonction à un seul argument, on commence par supposer que cette fonction est l’identité avant de simplifier son corps. On vérifie ensuite si le résultat est équivalent à une identité en le parcourant récursivement, pour couvrir le plus de cas possible (par exemple les branchements conditionnels). Si c’est le cas, la fonction est remplacée par l’identité ; sinon, on revient à une simplification classique, sans hypothèse d’induction.
#### Propagation de constantes
Nous avons ensuite amélioré notre fonction qui détermine si le corps d’une fonction est une identité ou non, pour gérer les constantes. Il propage les informations d’égalité qu’on gagne sur l’argument lors des branchements conditionnels.
Ainsi, si on a une fonction de la forme
```Ocaml
type truc = A | B | C
let id = function
| A -> A
| B -> B
| C -> C
```
ou même
```Ocaml
let id x = if x=0 then 0 else x
```
on détectera bien que c’est l’identité.
#### Exemples
##### Fonctions récursives
Nous pouvons maintenant détecter les identités récursives :
```Ocaml
let rec listid = function
| t::q -> t::(listid q)
| [] -> []
```
compilait avant ainsi:
```
End of middle end:
let_rec_symbol
(camlTest__listid_5_closure
(Project_closure (camlTest__set_of_closures_20, listid/5)))
(camlTest__set_of_closures_20
(Set_of_closures (
(set_of_closures id=Test.11
(listid/5 = fun param/7 ->
(if param/7 then begin
(let
(apply_arg/13 (field 1<{../../test.ml:9,4-8}> param/7)
apply_funct/14 camlTest__listid_5_closure
Pmakeblock_arg/15
*(apply*&#091;listid/5]<{../../test.ml:9,15-25}> apply_funct/14
apply_arg/13)
Pmakeblock_arg/16 (field 0<{../../test.ml:9,4-8}> param/7)
Pmakeblock/17
(makeblock 0<{../../test.ml:9,12-25}> Pmakeblock_arg/16
Pmakeblock_arg/15))
Pmakeblock/17)
end else begin
(let (const_ptr_zero/27 Const(0a)) const_ptr_zero/27) end))
free_vars={ } specialised_args={}) direct_call_surrogates={ }
set_of_closures_origin=Test.1])))
let_symbol (camlTest (Block (tag 0, camlTest__listid_5_closure)))
End camlTest
```
On détecte maintenant que c’est l’identité :
```
End of middle end:
let_symbol
(camlTest__set_of_closures_20
(Set_of_closures (
(set_of_closures id=Test.13 (listid/5 = fun param/7 -> param/7)
free_vars={ } specialised_args={}) direct_call_surrogates={ }
set_of_closures_origin=Test.1])))
(camlTest__listid_5_closure
(Project_closure (camlTest__set_of_closures_20, listid/5)))
(camlTest (Block (tag 0, camlTest__listid_5_closure)))
End camlTest
```
##### Exemple non sûr
En revanche, on peut profiter de l’absence de garanties pour contourner le typage, et accéder à une adresse mémoire comme à un entier :
```Ocaml
type bugg = A of int*int | B of int
let rec bug = function
| A (a,b) -> (a,b)
| B x -> bug (B x)
let (a,b) = (bug (B 42))
let _ = print_int b
```
Cette fonction va être simplifiée vers l’identité alors que le type `bugg` n’est pas compatible avec le type tuple ; quand on essaie de projeter sur le second champ du variant `b`, on accède à une partie de la mémoire indéfinie :
```
$ ./unsafe.out
47423997875612
```
#### Pistes d’améliorations – court terme
##### Annotation des fonctions
Une amélioration simple en théorie, serait de laisser le choix à l’utilisateur des fonctions sur lesquelles il veut appliquer ces optimisations qui ne sont pas toujours correctes. Nous n’avons pas eu le temps de faire le travail de propagation de l’information jusqu’à Flambda, mais il ne devrait pas y avoir de difficultés d’implémentation.
##### Ordre sur les arguments
Pour avoir une optimisation plus sûre, on voudrait pouvoir utiliser l’idée développée dans la partie théorique, qui rend l’optimisation correcte sur les objets non cycliques, et surtout qui nous redonne les garanties du typage pour éviter le problème vu dans l’exemple ci-dessus.
Afin d’avoir cette garantie, on veut changer la passe de simplification pour que son environnement contienne une option de couple fonction – argument. Quand cette option existe, le couple indique que nous sommes dans le corps d’une fonction, en train de la simplifier, et donc que les applications de la fonction sur des éléments plus petits que l’argument peuvent être simplifiés en une identité. Bien sûr, on devrait aussi modifier la passe pour se rappeler des éléments qui ne sont pas plus petits que l’argument.
#### Pistes d’améliorations – long terme
##### Exclusion des objets cycliques
Comme décrit dans la partie théorique, on pourrait déduire récursivement quels objets sont cycliques et tenter de les exclure de notre optimisation. Le problème est alors qu’au lieu de remplacer les fonctions par l’identité, on doit avoir une annotation spéciale qui représente `IdRec`.
Cela devient bien plus complexe à implémenter quand on compile entre plusieurs fichiers, puisqu’on doit alors avoir cette information dans l’interface des fichiers déjà compilés pour pouvoir faire l’optimisation quand c’est nécessaire.
Une piste serait d’utiliser les fichiers .cmx pour enregistrer cette information quand on compile un fichier, mais ce genre d’implémentation était trop longue pour être réalisée pendant le stage. De plus, il n’est même pas évident qu’elle soit un bon choix pratique : elle complexifierait beaucoup l’optimisation pour un avantage faible par rapport à une version correcte sur les objets non cycliques et activée par une annotation de l’utilisateur.
title=Verification for Dummies: SMT and Induction
authors=Adrien Champion
date=2021-10-14
category=Formal Methods
tags=trainings,smt,formal logic
- Adrien Champion [adrien.champion@ocamlpro.com](mailto:adrien.champion@ocamlpro.com)
- [](http://creativecommons.org/licenses/by-sa/4.0/) This work is licensed under a [Creative Commons Attribution-ShareAlike 4.0 International License](http://creativecommons.org/licenses/by-sa/4.0/).
These posts broadly discusses *induction* as a *formal verification* technique, which here really means *formal program verification*. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing directly with induction.
The next chapters discuss the following notions:
- formal logics and formal frameworks;
- SMT-solving: modern, *low-level* verification building blocks;
- declarative transition systems;
- transition system unrolling;
- BMC and induction proofs over transition systems;
- candidate strengthening.
The approach presented here is far from being the only one when it comes to program verification. It happens to be relatively simple to
understand, and I believe that familiarity with the notions discussed here makes understanding other approaches significantly easier.
This book thus hopes to serve both as a relatively deep dive into the specific technique of SMT-based induction, as well as an example of the technical challenges inherent to both developing and using automated proof engines.