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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
open RTLpathLivegenaux
open RTLpathCommon
open Datatypes
open Maps
open RTL
open Op
open Asmgen
open DebugPrint
open PrintRTL
open! Integers
let reg = ref 1
let node = ref 1
let r2p () = Camlcoq.P.of_int !reg
let n2p () = Camlcoq.P.of_int !node
let n2pi () = node := !node + 1; n2p()
type immt = Xori | Slti
let load_hilo32 dest hi lo succ k =
if Int.eq lo Int.zero then
Iop (OEluiw hi, [], dest, succ) :: k
else (
Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
let loadimm32 dest n succ k =
match make_immed32 n with
| Imm32_single imm ->
Iop (OEaddiwr0 imm, [], dest, succ) :: k
| Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
let get_opimm imm = function
| Xori -> OExoriw imm
| Slti -> OEsltiw imm
let opimm32 a1 dest n succ k op opimm =
match make_immed32 n with
| Imm32_single imm ->
Iop (get_opimm imm opimm, [a1], dest, succ) :: k
| Imm32_pair (hi, lo) ->
reg := !reg + 1;
load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori
let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti
let cond_int32s_x0 cmp a1 dest succ k =
match cmp with
| Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
| Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
| Clt -> Iop (OEsltw (Some false), [a1;a1], dest, succ) :: k
| Cle -> Iop (OEsltw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
| Cgt -> Iop (OEsltw (Some true), [a1;a1], dest, succ) :: k
| Cge -> Iop (OEsltw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
let cond_int32s_reg cmp a1 a2 dest succ k =
match cmp with
| Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
| Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
| Clt -> Iop (OEsltw None, [a1;a2], dest, succ) :: k
| Cle -> Iop (OEsltw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
| Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k
| Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
let expanse_condimm_int32s cmp a1 n dest succ k =
if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else
match cmp with
| Ceq | Cne ->
xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp dest dest succ k)
| Clt -> sltimm32 a1 dest n succ k
| Cle -> if Int.eq n (Int.repr Int.max_signed)
then loadimm32 dest Int.one succ k
else sltimm32 a1 dest (Int.add n Int.one) succ k
| _ -> reg := !reg + 1;
loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)
let cond_int32u_reg cmp a1 a2 dest succ k =
match cmp with
| Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
| Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
| Clt -> Iop (OEsltuw None, [a1;a2], dest, succ) :: k
| Cle -> Iop (OEsltuw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
| Cgt -> Iop (OEsltuw None, [a2;a1], dest, succ) :: k
| Cge -> Iop (OEsltuw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
let rec write_tree exp n code' =
match exp with
| (Iop (_,_,_,succ)) as inst :: k ->
print_instruction stderr (0,inst);
Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);
code' := PTree.set n inst !code';
Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);
write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
| _ -> !code'
let get_regindent = function
| Coq_inr _ -> []
| Coq_inl r -> [r]
let get_regs_inst = function
| Inop (_) -> []
| Iop (_,args,dest,_) -> dest :: args
| Iload (_,_,_,args,dest,_) -> dest :: args
| Istore (_,_,args,src,_) -> src :: args
| Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args)
| Itailcall (_,t,args) -> (get_regindent t) @ args
| Ibuiltin (_,args,dest,_) ->
(AST.params_of_builtin_res dest) @
AST.params_of_builtin_args args
| Icond (_,args,_,_,_) -> args
| Ijumptable (arg,_) -> [arg]
| Ireturn (Some r) -> [r]
| _ -> []
let generate_head_order n start_node new_order =
Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) (Camlcoq.P.to_int start_node) !node;
for i = !node downto (Camlcoq.P.to_int start_node) do
new_order := !new_order @ [Camlcoq.P.of_int i];
done;
new_order := n :: !new_order
let expanse (sb: superblock) code =
debug_flag := true;
let new_order = ref [] in
let code' = ref code in
Array.iter (fun n ->
let inst = get_some @@ PTree.get n code in
match inst with
| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> (
Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;
Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;
Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);
Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);
debug "[EXPANSION] Replace this:\n";
print_instruction stderr (0,inst);
debug "[EXPANSION] With:\n";
let start_node = Camlcoq.P.of_int (!node + 1) in
let exp = cond_int32u_reg c a1 a2 dest succ [] in
code' := write_tree (List.rev exp) start_node code';
let first = Inop (n2pi()) in
code' := PTree.set n first !code';
generate_head_order n start_node new_order)
| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
let start_node = Camlcoq.P.of_int (!node + 1) in
let exp = expanse_condimm_int32s c a1 imm dest succ [] in
code' := write_tree (List.rev exp) start_node code';
let first = Inop (n2pi()) in
code' := PTree.set n first !code';
generate_head_order n start_node new_order)
(*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
(*entry := n2p()*)
| _ -> new_order := !new_order @ [n]
) sb.instructions;
sb.instructions <- Array.of_list !new_order;
(*print_arrayp sb.instructions;*)
debug_flag := false;
!code'
let rec find_last_node_reg = function
| [] -> ()
| (pc, i) :: k ->
let rec traverse_list var = function
| [] -> ()
| e :: t ->
(let e' = Camlcoq.P.to_int e in
if e' > !var then var := e';
traverse_list var t) in
traverse_list node [pc];
traverse_list reg (get_regs_inst i);
find_last_node_reg k
|
