1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
# 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...
## 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: specified but not yet implemented.
- BTL -> RTL: proof started.
## "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).
## 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.
## 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.
## 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
...
|
