blob: dd6baa89b511ff9ae2820e14c576008875d888cc (
plain)
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
|
(* XXX uncomment
open !BTL
open DebugPrint
open AuxTools
open Maps*)
(** A quick note on the BTL renumber algorithm
This is a simple first version where we try to reuse the entry numbering from RTL.
In the futur, it would be great to implement a strongly connected components partitionning.
The numbering is done by a postorder traversal.
TODO gourdinl : note perso
- faire un comptage global du nombre d'instructions rtl à générer
- utiliser la structure d'info créée lors de la génération pour tenter de préserver au max
la relation d'ordre, avec une heuristique genre (1 + max des succs) pour l'insertion
- quand il y a un branchement conditionnel, privilégier le parcour du fils gauche en premier
(afin d'avoir de plus petits numéros à gauche)
*)
(*
let rec get_max_rtl_ninsts code entry =
let rec postorder_blk ib =
*)
(* XXX uncomment
let postorder code entry =
let renumbered_code = ref PTree.empty in
let rec renum_ibf e =
let ibf = get_some @@ PTree.get e code in
if ibf.binfo.visited then ()
else (
ibf.binfo.visited <- true;
let next_nodes = ref [] in
let ib = ibf.entry in
let rec renum_iblock ib =
match ib with
in
let rib = renum_iblock ib in
ibf.entry <- rib;
renumbered_code := PTree.set e ibf !renumbered_code;
let succs = !next_nodes in
List.iter renum_ibf succs)
in
renum_ibf entry
let renumber (f: BTL.coq_function) =
debug_flag := true;
let code = f.fn_code in
let entry = f.fn_entrypoint in
let renumbered_code = postorder code entry in
debug_flag := false;
renumbered_code*)
|
