# BTL Development Roadmap

BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation).
It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event.
The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules.
The main info required from oracles: a "dupmap" mapping block entries (and maybe strategies for controlling path explosion during symbolic execution -- see below).
Moreover, the "global" optimizations would require some invariants annotations at block entry (provided by oracles).

Examples of optimizations that we aim to support:

 - instruction scheduling
 - instruction rewritings (instruction selection)
 - branch duplication, "if-lifting" (e.g. side-exit moved up in "traces").
 - strength-reduction
 - SSA optimizations

We sketch below the various kinds of supported optimizations in development order...

Remark that we may port most of the current optimizations from RTL to BTL (even maybe, register allocation).
However, RTL will probably remain useful for "fine-tuned" duplication that crosses block boundaries (e.g. Duplicate module).

## Introduction

En gros la syntaxe d'un bloc BTL est définie par:

    Inductive iblock: Type :=
    | ... (* instructions basiques ou "finales" (call, return, goto, etc) *)
    | Bseq (b1 b2: iblock)  (* séquence de deux blocs *)
    | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock)  (* if-then-else *)

Le modèle de base de l'exécution symbolique représente un tel bloc par un état symbolique de type:

    Inductive sstate :=
    | Sfinal (sis: sistate) (sfv: sfval)
    | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate)
    | Sabort
    .

où `sistate` est un PPA (preconditioned parallel assignment) des registres et `sfval` représente un branchement (call, return, goto, etc).
    
Autrement dit, un état symbolique représente tous les chemins
d'exécution possibles par une sorte de gros BDD ayant sur les feuilles
un `Sfinal` (ou un `Sabort` s'il manque une instruction de branchement sur ce chemin).

## Block boundaries, branch duplication or factorization

Two possibility of branch duplications (e.g tail-duplication, loop unrolling, etc):

- during RTL -> BTL (while "building" BTL blocks)
- during BTL -> BTL. Typically, the "if-lifting" à la Justus could be performed/verified in a single pass here !

Branch factorization should also be possible in BTL -> RTL pass. Example: revert "loop-unrolling".

**IMPLEM NOTE:** in a first step a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes.


**CURRENT STATUS** 

- verifier: implemented and proved w.r.t match_iblock specification.
- Proof:
  - BTL -> RTL: done.
  - RTL -> BTL: done.
- Oracles:
  - BTL -> RTL: TODO.
  - RTL -> BTL: started.

**TODO**

- lien BTL/RTL: autoriser le BTL à avoir des Bnop en plus du RTL, e.g. pour autoriser des "if-then" sans else.
Pour faciliter le vérificateur, faire comme le Bgoto: les Bnop en "trop" ne sont autorisés que s'il y a eu une instruction RTL avant.
Ajouter aussi un booléen (positionné par l'oracle) sur le Bnop qui indique si le "nop" existe ou pas au niveau RTL.

## Simulation modulo liveness and "Functional" semantics of BTL blocks

L'approche suivie pour réaliser la simulation modulo liveness dans
RTLpath est compliquée à adapter sur BTL.  En effet, un état
symbolique RTLpath correspond à un état symbolique BTL très
particulier: toutes les "feuilles" (les `Sfinal`) sont des `Sgoto`
sauf éventuellement une.  Or, dans RTLpath, le traitement de l'info de
liveness sur cette feuille particulière est très adhoc et laborieux
(cf. le traitement de `pre_output_regs` dans RTLpathScheduler, etc).
On n'a pas envie de généraliser cette usine à gaz.

On cherche donc une façon plus abstraite de faire... On a l'idée de
coder la "simulation modulo liveness" dans une "simulation
less_undef".  Ça peut rendre le cadre du test de simulation plus
simple et plus général.

**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL, on pourrait
définir une nouvelle sémantique (basée sur la même sémantique à grand
pas dans les blocs), où c'est juste "l'entrée dans un bloc" qui change
de sémantique. Intuitivement, cette nouvelle sémantique considèrerait
chaque bloc comme une sorte de fonction paramétrée par les `input_regs`
et appelée uniquement en "tailcall" (via les "goto").  C'est ce qu'on
va appeler la "functional semantics" de BTL (l'autre étant appelée
qqchose comme "CFG semantics" ?).

Autrement dit, sur l'entrée dans un bloc pour un état (rs,m), on
commence par mettre à Vundef tous les registres qui ne sont pas dans l'`input_regs`.

**NOTE** cette idée de voir les blocs comme des "fonctions" correpond
bien à la représentation "SSA" à la Appel/MLIR.  Donc cette sémantique
peut servir de base pour un support de formes SSA (partielles ou
totales) dans BTL.  Pour l'encodage de SSA, il suffira d'étendre le
mécanisme d'initialisation du "rs0" d'un bloc avec un passage de
paramètres.

**REM** pour le test d'exécution symbolique, il semble plus adapté de
mettre les Vundef juste à la fin de la transition (précédente) plutôt
qu'au début (de la suivante).  On pourrait aussi faire les deux (dans le détail, ça ne ferait pas exactement deux fois la même chose: 
par exemple, quand on sort sur un call ou un builtin, le résultat du call/builtin n'est jamais dans le liveout puisqu'il va être écrasé de toute façon pendant la transition, 
mais il peut être -- ou pas -- dans le livein de la transition suivante dans ce même bloc).

Avoir une initialisation à Vundef en début de bloc permettrait de
faire une analyse des expressions mal initialisées - par exemple à
partir du bloc d'entrée de la fonction. Ça semble complémentaire de
l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une
combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite).

Donc, dans un premier temps, la "functional semantics" encode/abstrait la notion de "liveout" pour le test d'exécution symbolique. 
Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée.

**STATUS**

1. See [BTL.fsem]  (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem)

**TODO**

1. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep").
2. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics.
   en gros: on implémente un vérificateur des infos de liveness.
   c'est la correction du "input_regs" qui garantit que la simulation est correct.
   La preuve devrait normalement être très similaire à RTLpathLivegenproof. 

## "Basic" symbolic execution / symbolic simulation

We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. 
Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté.

**STATUS**

- BTL_SEtheory: DONE
 - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem
 - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem).

**TODO**

1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof).
2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ?
Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ?

## Port of RTLpath optimizations to BTL

- Generalize superblock scheduling for a notion of "extended-blocks" such that each instruction of a block, except the block entry, has a single predecessor in the block. 
- Port rewriting rules of RTLpath.
- Justus's "poor man SSA" + if-lifting.

## Efficient comparison (guided by oracles) of "if-then-else" sequences.

Le pb est complexe. Comparer des expressions booleennes contenant juste des variables booleennes est déjà NP-complet, avec "explosion exponentielle" dans le pire cas.

Approche proposée: utiliser un mécanisme de vérification "simple", basée sur une comparaison par execution symbolique de "tous" les chemins d'execution (cf Intro ci-dessus).
Ça pète exponentiellement dans le pire cas: mais on pourra contrôler ce risque d'explosion par les oracles...

Ci-dessous, on liste quelques "techniques" de collaboration oracle/vérificateur pour contrôler l'explosion des chemins.
Idée: les conditions comportent une liste d'annotations qui permet le guidage du vérificateur par l'oracle.

### Contrôle des "joins internes" dans le bloc. 

Si dans le bloc, toute condition a au plus un "predecesseur" (au sens
du CFG RTL) dans le bloc: alors le nombre de "chemins sémantiques"
(explorés par l'exécution symbolique) est identique au nombre de
"branches syntaxiques" (présents dans le code). Une façon simple de
contrôler l'explosion de l'exécution symbolique est de fabriquer (avec
les oracles) des blocs avec un nombre borné (petit) de "joins
internes".

**Exemple d'application: généralisation des superblocks**

On considère le bloc BTL ci-dessous (où les `i*` sont des séquences d'instructions basiques sans branchement):
   
    i0;
    if (c1) { i1 } else { i1'; goto pc1 }
    if (c2) { i2; goto pc2 } else { i2' }
    if (c3} { i3; goto pc3 } else { i3'; goto pc3' }

Sur un tel bloc, il n'y a aucun "join interne" (l'exécution symbolique est donc linéaire).
Mais représenter en RTLpath un tel bloc nécessite au moins 4 blocks (1 superbloc et 3 basic-blocs):

    i0; c1; i1; c2; i2'; i3'; goto pc3'
    i1'; goto pc1 
    i2; goto pc2
    i3; goto pc3

La vérification BTL sur le gros bloc ne prendra à priori pas plus de
temps que la vérification RTLpath cumulée des 4 "petits" blocs. Mais
la vérification BTL sera plus *puissante*, puisque que quand on va
vérifier les chemins d'exécutions correspondant à ceux des 3
basic-blocs, on aura le `i0` en plus dans l'état symbolique (i.e. un
"contexte d'exécution" plus précis).

**Autre exemple d'application: le if-lifting à la Justus**

Le superblock suivant:
    
    y1 = e1(x)
    x = e2(a)
    y2 = e3(x)
    if (c[x]) { goto pc  } else { i4; goto pc' }
     
peut être directement montré équivalent à

    x' = e2(a)   // x' un registre "frais" (pas dans les "liveout")
    if (c[x']) { 
        y1 = e1(x);
        x = x';
        y2 = e3(x);
        goto pc
    } else {
        y1 = e1(x);
        x = x';
        y2 = e3(x);
        i4; 
        goto pc'
    }
   
Ici, la duplication de branche a donc lieu en BTL.

L'exécution symbolique de ces deux blocs va produire deux BDD comparables (avec comparaison des feuilles modulo liveness).

### Comparaison des BDD (modulo réordonnancement des conditions ?)

On peut avoir envie de montrer que les deux blocs ci-dessous sont équivalents (si les dépendences sur les variables le permettent):

    if (c1) { i1 } else { i1' }
    if (c2) { i2 } else { i2' }
    
et

    if (c2) { i2 } else { i2' }
    if (c1) { i1 } else { i1' }

Ça revient (en gros) à comparer les BDD:
   
    if (c1) { if (c2) {i1;i2} else {i1;i2'} } else { if (c2) {i1';i2} else {i1';i2'} }

et 

    if (c2) { if (c1) {i2;i1} else {i2;i1'} } else { if (c1) {i2';i1} else {i2';i1'} }

Pour gérer ça, on peut faire des "Ordered BDD": l'oracle du **bloc
transformé** annote (certaines) conditions avec des numéros de façon à
ce l'exécution symbolique du bloc transformé produise un "BDD" qui
correspond à celui du bloc d'origine (cf. "Principe"
ci-dessous). Cependant, il semble difficile d'appliquer complètement
les techniques de mémoïsation des BDD ayant des booléens sur les
feuilles.  Car ici on veut effectuer une comparaison sur des feuilles
2 à 2 qui n'est pas une égalité, mais une inclusion !

**Principe du réordonnancement de BDD:** l'exécution symbolique du **bloc transformé** réordonne le BDD de
façon à respecter la numérotation: un pére doit avoir un numéro inférieur à
chacun de ses fils (en l'absence de numéro, on ignore les contraintes
de numérotation entre ce noeud est ses voisins). Exemple ci-dessous
avec trois conditions distinctes (pour order c1 < c2 < c3):

    if (c3) { if (c1) {f1} else {f1'} } else { if (c2} {f2} else {f2'} } 
    
est réordonné en

    if (c1) { if (c2) { if (c3) {f1} else {f2} } else { if (c3) {f1} else {f2'} } } 
       else { if (c2) { if (c3) {f1'} else {f2} } else { if (c3) {f1'} else {f2'} } }

**rem:** on ajoute ici un undefined behavior potentiel à cause l'execution de c2 quand c3 est vrai. 
Mais si le **bloc d'origine** est simulé par cet état symbolique réordonné, c'est correct. 
Le bloc transformé a juste supprimé un test inutile...

Bon, à voir si le principe ci-dessus est vraiment utile dans toute sa
généralité. Pour simplifier, on peut aussi restreindre le
réordonnancement du BDD aux cas où il n'y a pas de test redondant
inséré (comme dans l'exemple initial).

**Version simplifiée: comparaison des BDD sans réordonnancement des conditions**

Dans un premier temps (jusqu'à ce qu'on trouve une optimisation où ça pourrait être utile): pas de réordonnacement des BDD.
On autorise juste le BDD du bloc transformé à supprimer des conditions par rapport au bloc d'origine.
Autrement dit, dans la comparaison récursive de `{if (c) BDD1 BDD2}` avec `{if (c') BDD1' BDD2}'`:

- soit `c=c'` et on compare récursivement `BDD1` avec `BDD1'` et `BDD2` avec `BDD2'`.
- soit `c<>c'` et  on compare récursivement `BDD1` et `BDD2` avec `{if (c') BDD1' BDD2'}`

Ce deuxième cas correspond au fait que le test sur `c` dans le bloc d'origine était inutile!

### Propagation de valeurs symbolique de conditions (et élimination de condition) pendant l'execution symbolique

L'exécution symbolique se propageant en "avant", on peut propager les valeurs des conditions symboliques, qu'on peut utiliser pour éliminer des conditions redondantes 
(et donc limiter l'explosion du nombre de chemin).

Pour rendre ce mécanisme efficace et puissant, on peut guider ce mécanisme de propagation/élimination avec des annotations introduites par les oracles.

- une annotation "bind_to x" qui indique de mémoriser la valeur (soit "true" soit "false" suivant la branche) de la condition symbolique avec le nom "x"
- une annotation "eval_to b proof" qui indique que la condition s'évalue sur la constante "b", ce qui est prouvable avec la preuve "proof".

Ici on peut imaginer un langage plus ou moins compliqué pour prouver l'évaluation des conditions. La version la plus simple:

- "eq(x)"  dit simplement que la condition symbolique est syntaxiquement égale celle appelée "x".
- "eqnot(x)" dit que c'est la négation.

Dans le cas général, on peut introduire tout un système de réécriture pour éliminer les conditions.

En fait, il serait sans doute intéressant de mettre en place un
"système de réécriture guidé par oracle" pour toutes les instructions
BTL.  Ça permet de concilier "puissance" de l'exécution symbolique et
"efficacité". L'exécution symbolique va pouvoir éventuellement faire
des réécritures compliquées, mais uniquement quand c'est nécessaire.

**Exemple: une "if-conversion" généralisée**
On aimerait montrer que le bloc d'origine:

    if (c) {
        x1 = e1
        x2 = e2
        y = e
        x3 = e3
    } else {
        x3 = e3'
        z = e'
        x1 = e1'
        x2 = e2'
    }
    
est simulable par le bloc transformé:

    x1 = (c?e1:e1')
    x2 = (c?e2:e2')
    x3 = (c?e3:e3')
    if (c) { y = e } else { z = e' }

une solution: ajouter une régle de réécriture `x = (c?e:e')` en `if (c) { x=e } else {x=e'}` 
(attention, ce n'est pas une règle de réécriture sur les valeurs
symboliques, mais sur du code BTL lui-même, avant l'exécution
symbolique de ce code).

L'exécution symbolique ouvre alors deux branches `c=true` et
`c=false` sur `x1 = (c?e1:e1')`, puis la propagation/élimination de la
condition symbolique `c` simplifie les conditionnelles sur `x2`, `x3` et `y`/`z`.
Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combinatoire).

**Rem** les mécanismes de propagation/réécritures décrits ci-dessus peuvent être aussi très utile pour la simulation symbolique modulo invariants (cf. ci-dessous) !

## Invariants at block entry

Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.

**IDEAS**

- En pratique, il faudra peut-être affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie.

- Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins).

## Support of SSA-optimizations

Extends BTL with "register renamings" at exits.

This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.

## Alias analysis in the symbolic simulation

A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf)