# 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 only info required from oracles: a "dupmap" mapping block entries.
In contrast, 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...

## 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.
- BTL -> RTL: done.
- 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.


## "Basic" symbolic execution / symbolic simulation

IMPLEM PLAN in two steps:

1. a very basic version without rewriting rules, and without support for simulation modulo-liveness.

2. Support a "SVundef" symbolic value, and implement symbolic simulation wrt "less_undef" relation. 
This will allow more general rewriting rules and will generalize modulo-liveness (see next section).

**CURRENT STATUS**

- model of symbolic execution in Continuation-Passing Style, with basic "correctness" thm ("completness" not yet done).

## Simulation modulo liveness

Extends BTL with the possibility of destroying a set of registers at each exit (a destroyed register is simply set to Vundef).

We can the provide a "MarkUnused" pass of BTL -> BTL that insert these destructions at each exit using liveness info !
(NB: the liveness info could be provided by the RTL -> BTL oracle like on RTLpath).

In the symbolic execution, destroying a register corresponds to associate it SVundef value.

NB: this approach through "destroyed registers" and "SVundef" seems more modular (thus simpler) and more general than the current approach on RTLpath.

The proof of "simulation modulo liveness" of a BTL B1 by a BTL B2 will simply corresponds to compose two forward simulations:  B1 --> MarkUnused(B1) --> B2.

**IMPLEM NOTE:** "MarkUnused" checks the correctness of liveness informations while performing its transformation.
It should computes alive register from block entry, by forward proceeding of "internal instructions" (like in RTLPathLivegen).
When arriving on a final instruction, we marked as "destroyed" all alive registers that are not in the input registers of the exit
Semantically, the destruction of registers happens "in parallel" of the final step of the block.

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

## Support of SSA-optimizations

Extends BTL with "register renamings" at exits (in a sense, "register renaming" extends the feature of "register destroying").

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)