# 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:** 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.

## 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_def".  Ç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
[BTLmatch.cfgsem], on définit une sémantique [BTL.fsem], où c'est
juste "l'entrée dans un bloc" qui change de sémantique. Intuitivement,
cette sémantique considère 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 pourrait moralement
commencer 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): c'est d'ailleurs plus proche de la vision SSA.  

En fait, on pourrait 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 BTL.fsem 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**

DONE.

## "Basic" symbolic execution / symbolic simulation

We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.fsem. 
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).

- BTL_SEsimuref.v: DONE (raffinement de la notion d'état symbolique)

- BTL_Schedulerproof: DONE (preuve que les simulations symboliques locales de blocks/blocks garantissent la simulation globale du programme pour BTL.fsem).

**TODO**

implem du hash-consing.

## 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.

**Remarque** déjà sur les superblocs, le test de simulation par
exécution symbolique est quadratique dans le pire cas. Si on a "n"
variables live sur les sorties et "m" sorties, la vérif est en
"n*m". En pratique, le nombre de sorties est limité, notamment à cause
des contraintes pour respecter la structure de superblocs. En RTLpath,
malgré ce coût quadratique théorique dans le pire cas, en pratique, le
vérificateur passe bien à l'échelle sur nos benchmarks.

### 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 et le test de simulation quadratique).
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) !

## Peut-on coder l'égalité modulo liveness comme un cas simple d'invariant symbolique (et faire la vérif de liveneness par execution symbolique) ?

On peut peut-être simplifier le cadre actuel pour rendre l'intégration des invariants symboliques plus facile !! Une piste à creuser...

Si la sémantique `BTL.fsem` a permis de rendre l'architecture un peu plus modulaire (mais sans vraiment simplifier sur le fond). 
Elle ne simplifie pas vraiment l'intégration de la liveness avec les invariants.
Une approche qui pourrait réellement simplifier: voir le raisonnement modulo liveness comme un cas particulier d'invariant symbolique. 

**Idée** pour tout chemin d'exécution passant de `pc` et `pc'`, on ramène la simulation modulo liveness de `ib1` par `ib2` au test:
    
    [ib1;str_inputs(pc')] lessdef [str_inputs(pc);ib2]
    
**Avantages possibles**

- plus de verif de liveness spécifique.
- plus de sémantique `BTL.fsem`
- les `str_inputs` ne seraient plus dans l'exécution symbolique, mais dans le test de simulation: ça évite les difficultés sur les jumptables.

Par contre, il faut réintroduire une preuve `lessdef` modulo liveness dans `BTL_Schedulerproof`.

### Plan d'implem. incrémentale (dans une branche)

1. Repartir d'une version de BTL sans info de liveness pour simplifier au maximum!! (ie on supprime la semantique fsem et on repart sur cfgsem).
2. Introduire la preuve `lessdef` modulo liveness dans `BTL_Schedulerproof` en *supposant* qu'on a le test de simulation symbolique qui nous arrange. 
   L'idée est de dégager des conditions suffisantes sur le test de simulation symbolique.
3. Réaliser le test de simulation symbolique.

## Symbolic 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.


### EXAMPLE OF STRENGTH REDUCTION

On veut passer du code C1:

    init: // inputs: int *t,  int n, int s 
    int i=0;
    loop: // inputs: int *t,  int n, int s, int i 
        if (i >= n) goto exit;
        s += t[i];
        i += 1;
        goto loop;
    exit: // inputs: int *t,  int s
    
au code C2:

    init: // inputs: int *t,  int n, int s 
    int *ti = t;
    int *tn = t+n;
    loop: // inputs: int *t,  int s, int *ti, int *tn
        if (ti >= tn) goto exit;
        s += *ti;
        ti += 1; // i.e. sizeof(int)
        goto loop;
    exit; // inputs: int *t,  int s
        
Pour donner la correspondance entre les variables des 2 blocs, pour chaque entrée "pc", on introduit une "fonction" de C1@pc.(inputs) -> C2@pc.(inputs).

Typiquement, cette fonction est codable comme un map associant une valeur symbolique sur les C1@pc.(inputs) aux variables de C2@pc.(inputs). Exemple:

    init: // map vide (identité)
    loop:
        ti = t+i
        tn = t+n
    exit: // map vide (identité)
 
Si on note `TRANSFER` cette fonction, alors la vérification par
exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo
`TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec
`TRANSFER(pc); ib2` pour la simulation symbolique usuelle.
 
Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`.

**REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`...

### Comment gérer le cas des registres résultat de call et builtin ?

Rem: c'est la gestion de ces cas particuliers qui conduit à la notion de `pre_output_regs` (ou `BTL.pre_input`) dans la verif de la simulation modulo liveness.
On va retrouver ça dans la verif de la simulation modulo invariants symboliques.
Mais pas évident à éviter. 

Concrètement, on ne pourra pas mettre d'invariant qui porte sur le résultat d'un call ou d'un builtin (à part un pur renommage de registre).

### GENERALISATION (What comes next ?)

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).

En gros, on pourrait passer d'invariants purement symboliques à des invariants combinant valeurs symboliques et valeurs abstraites.

## Support of SSA-optimizations

Minimum feature: extends BTL with "register renamings" at exits. This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.

Maximum feature: add also a basic instruction that performs parallel renaming of registers. 
This simple feature would help to represent a very general notion of "partial SSA forms": since they could appear in the middle of a block.

In both case, such register renamings would be forbidden in BTL<->RTL matching (SSA-optimizations could only happen within BTL passes).

## Alias analysis in the symbolic simulation

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