[2717] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open String |
---|
| 4 | |
---|
| 5 | open Sets |
---|
| 6 | |
---|
| 7 | open Listb |
---|
| 8 | |
---|
| 9 | open LabelledObjects |
---|
| 10 | |
---|
| 11 | open Graphs |
---|
| 12 | |
---|
| 13 | open I8051 |
---|
| 14 | |
---|
| 15 | open Order |
---|
| 16 | |
---|
| 17 | open Registers |
---|
| 18 | |
---|
| 19 | open BitVectorTrie |
---|
| 20 | |
---|
| 21 | open CostLabel |
---|
| 22 | |
---|
| 23 | open Hide |
---|
| 24 | |
---|
| 25 | open Proper |
---|
| 26 | |
---|
| 27 | open PositiveMap |
---|
| 28 | |
---|
| 29 | open Deqsets |
---|
| 30 | |
---|
| 31 | open ErrorMessages |
---|
| 32 | |
---|
| 33 | open PreIdentifiers |
---|
| 34 | |
---|
| 35 | open Errors |
---|
| 36 | |
---|
| 37 | open Extralib |
---|
| 38 | |
---|
| 39 | open Setoids |
---|
| 40 | |
---|
| 41 | open Monad |
---|
| 42 | |
---|
| 43 | open Option |
---|
| 44 | |
---|
| 45 | open Lists |
---|
| 46 | |
---|
| 47 | open Identifiers |
---|
| 48 | |
---|
| 49 | open Integers |
---|
| 50 | |
---|
| 51 | open AST |
---|
| 52 | |
---|
| 53 | open Division |
---|
| 54 | |
---|
| 55 | open Exp |
---|
| 56 | |
---|
| 57 | open Arithmetic |
---|
| 58 | |
---|
| 59 | open Extranat |
---|
| 60 | |
---|
| 61 | open Vector |
---|
| 62 | |
---|
| 63 | open Div_and_mod |
---|
| 64 | |
---|
| 65 | open Jmeq |
---|
| 66 | |
---|
| 67 | open Russell |
---|
| 68 | |
---|
| 69 | open List |
---|
| 70 | |
---|
| 71 | open Util |
---|
| 72 | |
---|
| 73 | open FoldStuff |
---|
| 74 | |
---|
| 75 | open BitVector |
---|
| 76 | |
---|
| 77 | open Types |
---|
| 78 | |
---|
| 79 | open Bool |
---|
| 80 | |
---|
| 81 | open Relations |
---|
| 82 | |
---|
| 83 | open Nat |
---|
| 84 | |
---|
| 85 | open Hints_declaration |
---|
| 86 | |
---|
| 87 | open Core_notation |
---|
| 88 | |
---|
| 89 | open Pts |
---|
| 90 | |
---|
| 91 | open Logic |
---|
| 92 | |
---|
| 93 | open Positive |
---|
| 94 | |
---|
| 95 | open Z |
---|
| 96 | |
---|
| 97 | open BitVectorZ |
---|
| 98 | |
---|
| 99 | open Pointers |
---|
| 100 | |
---|
| 101 | open ByteValues |
---|
| 102 | |
---|
| 103 | open BackEndOps |
---|
| 104 | |
---|
| 105 | open Joint |
---|
| 106 | |
---|
| 107 | open Joint_LTL_LIN |
---|
| 108 | |
---|
| 109 | open LTL |
---|
| 110 | |
---|
| 111 | open Fixpoints |
---|
| 112 | |
---|
| 113 | open Set_adt |
---|
| 114 | |
---|
| 115 | open ERTL |
---|
| 116 | |
---|
| 117 | open ERTLptr |
---|
| 118 | |
---|
| 119 | open Liveness |
---|
| 120 | |
---|
| 121 | open Interference |
---|
| 122 | |
---|
| 123 | open Deqsets |
---|
| 124 | |
---|
| 125 | open State |
---|
| 126 | |
---|
| 127 | open Bind_new |
---|
| 128 | |
---|
| 129 | open BindLists |
---|
| 130 | |
---|
| 131 | open Blocks |
---|
| 132 | |
---|
| 133 | open TranslateUtils |
---|
| 134 | |
---|
| 135 | type arg_decision = |
---|
| 136 | | Arg_decision_colour of I8051.register |
---|
| 137 | | Arg_decision_spill of Nat.nat |
---|
| 138 | | Arg_decision_imm of BitVector.byte |
---|
| 139 | |
---|
| 140 | (** val arg_decision_rect_Type4 : |
---|
| 141 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 142 | arg_decision -> 'a1 **) |
---|
| 143 | let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 144 | | Arg_decision_colour x_18601 -> h_arg_decision_colour x_18601 |
---|
| 145 | | Arg_decision_spill x_18602 -> h_arg_decision_spill x_18602 |
---|
| 146 | | Arg_decision_imm x_18603 -> h_arg_decision_imm x_18603 |
---|
| 147 | |
---|
| 148 | (** val arg_decision_rect_Type5 : |
---|
| 149 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 150 | arg_decision -> 'a1 **) |
---|
| 151 | let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 152 | | Arg_decision_colour x_18608 -> h_arg_decision_colour x_18608 |
---|
| 153 | | Arg_decision_spill x_18609 -> h_arg_decision_spill x_18609 |
---|
| 154 | | Arg_decision_imm x_18610 -> h_arg_decision_imm x_18610 |
---|
| 155 | |
---|
| 156 | (** val arg_decision_rect_Type3 : |
---|
| 157 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 158 | arg_decision -> 'a1 **) |
---|
| 159 | let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 160 | | Arg_decision_colour x_18615 -> h_arg_decision_colour x_18615 |
---|
| 161 | | Arg_decision_spill x_18616 -> h_arg_decision_spill x_18616 |
---|
| 162 | | Arg_decision_imm x_18617 -> h_arg_decision_imm x_18617 |
---|
| 163 | |
---|
| 164 | (** val arg_decision_rect_Type2 : |
---|
| 165 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 166 | arg_decision -> 'a1 **) |
---|
| 167 | let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 168 | | Arg_decision_colour x_18622 -> h_arg_decision_colour x_18622 |
---|
| 169 | | Arg_decision_spill x_18623 -> h_arg_decision_spill x_18623 |
---|
| 170 | | Arg_decision_imm x_18624 -> h_arg_decision_imm x_18624 |
---|
| 171 | |
---|
| 172 | (** val arg_decision_rect_Type1 : |
---|
| 173 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 174 | arg_decision -> 'a1 **) |
---|
| 175 | let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 176 | | Arg_decision_colour x_18629 -> h_arg_decision_colour x_18629 |
---|
| 177 | | Arg_decision_spill x_18630 -> h_arg_decision_spill x_18630 |
---|
| 178 | | Arg_decision_imm x_18631 -> h_arg_decision_imm x_18631 |
---|
| 179 | |
---|
| 180 | (** val arg_decision_rect_Type0 : |
---|
| 181 | (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 182 | arg_decision -> 'a1 **) |
---|
| 183 | let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function |
---|
| 184 | | Arg_decision_colour x_18636 -> h_arg_decision_colour x_18636 |
---|
| 185 | | Arg_decision_spill x_18637 -> h_arg_decision_spill x_18637 |
---|
| 186 | | Arg_decision_imm x_18638 -> h_arg_decision_imm x_18638 |
---|
| 187 | |
---|
| 188 | (** val arg_decision_inv_rect_Type4 : |
---|
| 189 | arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) |
---|
| 190 | -> (BitVector.byte -> __ -> 'a1) -> 'a1 **) |
---|
| 191 | let arg_decision_inv_rect_Type4 hterm h1 h2 h3 = |
---|
| 192 | let hcut = arg_decision_rect_Type4 h1 h2 h3 hterm in hcut __ |
---|
| 193 | |
---|
| 194 | (** val arg_decision_inv_rect_Type3 : |
---|
| 195 | arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) |
---|
| 196 | -> (BitVector.byte -> __ -> 'a1) -> 'a1 **) |
---|
| 197 | let arg_decision_inv_rect_Type3 hterm h1 h2 h3 = |
---|
| 198 | let hcut = arg_decision_rect_Type3 h1 h2 h3 hterm in hcut __ |
---|
| 199 | |
---|
| 200 | (** val arg_decision_inv_rect_Type2 : |
---|
| 201 | arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) |
---|
| 202 | -> (BitVector.byte -> __ -> 'a1) -> 'a1 **) |
---|
| 203 | let arg_decision_inv_rect_Type2 hterm h1 h2 h3 = |
---|
| 204 | let hcut = arg_decision_rect_Type2 h1 h2 h3 hterm in hcut __ |
---|
| 205 | |
---|
| 206 | (** val arg_decision_inv_rect_Type1 : |
---|
| 207 | arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) |
---|
| 208 | -> (BitVector.byte -> __ -> 'a1) -> 'a1 **) |
---|
| 209 | let arg_decision_inv_rect_Type1 hterm h1 h2 h3 = |
---|
| 210 | let hcut = arg_decision_rect_Type1 h1 h2 h3 hterm in hcut __ |
---|
| 211 | |
---|
| 212 | (** val arg_decision_inv_rect_Type0 : |
---|
| 213 | arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) |
---|
| 214 | -> (BitVector.byte -> __ -> 'a1) -> 'a1 **) |
---|
| 215 | let arg_decision_inv_rect_Type0 hterm h1 h2 h3 = |
---|
| 216 | let hcut = arg_decision_rect_Type0 h1 h2 h3 hterm in hcut __ |
---|
| 217 | |
---|
| 218 | (** val arg_decision_discr : arg_decision -> arg_decision -> __ **) |
---|
| 219 | let arg_decision_discr x y = |
---|
| 220 | Logic.eq_rect_Type2 x |
---|
| 221 | (match x with |
---|
| 222 | | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 223 | | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 224 | | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
| 225 | |
---|
| 226 | (** val arg_decision_jmdiscr : arg_decision -> arg_decision -> __ **) |
---|
| 227 | let arg_decision_jmdiscr x y = |
---|
| 228 | Logic.eq_rect_Type2 x |
---|
| 229 | (match x with |
---|
| 230 | | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 231 | | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 232 | | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
| 233 | |
---|
| 234 | (** val preserve_carry_bit : |
---|
| 235 | AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list -> |
---|
| 236 | Joint.joint_seq List.list **) |
---|
| 237 | let preserve_carry_bit globals do_it steps = |
---|
| 238 | match do_it with |
---|
| 239 | | Bool.True -> |
---|
| 240 | List.Cons ((Joint.Extension_seq (Obj.magic Joint_LTL_LIN.SAVE_CARRY)), |
---|
| 241 | (List.append steps (List.Cons ((Joint.Extension_seq |
---|
| 242 | (Obj.magic Joint_LTL_LIN.RESTORE_CARRY)), List.Nil)))) |
---|
| 243 | | Bool.False -> steps |
---|
| 244 | |
---|
| 245 | (** val a : Types.unit0 **) |
---|
| 246 | let a = |
---|
| 247 | Types.It |
---|
| 248 | |
---|
| 249 | (** val set_dp_by_offset : |
---|
| 250 | AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **) |
---|
| 251 | let set_dp_by_offset globals off = |
---|
| 252 | List.Cons ((Joint.MOVE |
---|
| 253 | (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, (Joint.byte_of_nat off))))), |
---|
| 254 | (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a), |
---|
| 255 | (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPL)))), (List.Cons |
---|
| 256 | ((Joint.MOVE |
---|
| 257 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPL, a)))), (List.Cons |
---|
| 258 | ((Joint.MOVE |
---|
| 259 | (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))), (List.Cons |
---|
| 260 | ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a), |
---|
| 261 | (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPH)))), (List.Cons |
---|
| 262 | ((Joint.MOVE |
---|
| 263 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPH, a)))), |
---|
| 264 | List.Nil))))))))))) |
---|
| 265 | |
---|
| 266 | (** val get_stack : |
---|
| 267 | AST.ident List.list -> I8051.register -> Nat.nat -> Joint.joint_seq |
---|
| 268 | List.list **) |
---|
| 269 | let get_stack globals r off = |
---|
| 270 | List.append (set_dp_by_offset globals off) |
---|
| 271 | (List.append (List.Cons ((Joint.LOAD ((Obj.magic a), |
---|
| 272 | (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil)) |
---|
| 273 | (match I8051.eq_Register r I8051.RegisterA with |
---|
| 274 | | Bool.True -> List.Nil |
---|
| 275 | | Bool.False -> |
---|
| 276 | List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))), |
---|
| 277 | List.Nil))) |
---|
| 278 | |
---|
| 279 | (** val set_stack_not_a : |
---|
| 280 | AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq |
---|
| 281 | List.list **) |
---|
| 282 | let set_stack_not_a globals off r = |
---|
| 283 | List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE |
---|
| 284 | (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE |
---|
| 285 | ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))), |
---|
| 286 | List.Nil)))) |
---|
| 287 | |
---|
| 288 | (** val set_stack_a : |
---|
| 289 | AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **) |
---|
| 290 | let set_stack_a globals off = |
---|
| 291 | List.append (List.Cons ((Joint.MOVE |
---|
| 292 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil)) |
---|
| 293 | (set_stack_not_a globals off I8051.registerST1) |
---|
| 294 | |
---|
| 295 | (** val set_stack : |
---|
| 296 | AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq |
---|
| 297 | List.list **) |
---|
| 298 | let set_stack globals off r = |
---|
| 299 | match I8051.eq_Register r I8051.RegisterA with |
---|
| 300 | | Bool.True -> set_stack_a globals off |
---|
| 301 | | Bool.False -> set_stack_not_a globals off r |
---|
| 302 | |
---|
| 303 | (** val set_stack_int : |
---|
| 304 | AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq |
---|
| 305 | List.list **) |
---|
| 306 | let set_stack_int globals off int0 = |
---|
| 307 | List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE |
---|
| 308 | (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), (List.Cons |
---|
| 309 | ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It), |
---|
| 310 | (Obj.magic a))), List.Nil)))) |
---|
| 311 | |
---|
| 312 | (** val move : |
---|
| 313 | AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision |
---|
| 314 | -> Joint.joint_seq List.list **) |
---|
| 315 | let move globals carry_lives_after dst src = |
---|
| 316 | match dst with |
---|
| 317 | | Interference.Decision_spill dsto -> |
---|
| 318 | (match src with |
---|
| 319 | | Arg_decision_colour srcr -> |
---|
| 320 | preserve_carry_bit globals carry_lives_after |
---|
| 321 | (set_stack globals dsto srcr) |
---|
| 322 | | Arg_decision_spill srco -> |
---|
| 323 | (match Nat.eqb srco dsto with |
---|
| 324 | | Bool.True -> List.Nil |
---|
| 325 | | Bool.False -> |
---|
| 326 | preserve_carry_bit globals carry_lives_after |
---|
| 327 | (List.append (get_stack globals I8051.RegisterA srco) |
---|
| 328 | (set_stack globals dsto I8051.RegisterA))) |
---|
| 329 | | Arg_decision_imm int0 -> |
---|
| 330 | preserve_carry_bit globals carry_lives_after |
---|
| 331 | (set_stack_int globals dsto int0)) |
---|
| 332 | | Interference.Decision_colour dstr -> |
---|
| 333 | (match src with |
---|
| 334 | | Arg_decision_colour srcr -> |
---|
| 335 | (match I8051.eq_Register dstr srcr with |
---|
| 336 | | Bool.True -> List.Nil |
---|
| 337 | | Bool.False -> |
---|
| 338 | (match I8051.eq_Register dstr I8051.RegisterA with |
---|
| 339 | | Bool.True -> |
---|
| 340 | List.Cons ((Joint.MOVE |
---|
| 341 | (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil) |
---|
| 342 | | Bool.False -> |
---|
| 343 | (match I8051.eq_Register srcr I8051.RegisterA with |
---|
| 344 | | Bool.True -> |
---|
| 345 | List.Cons ((Joint.MOVE |
---|
| 346 | (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil) |
---|
| 347 | | Bool.False -> |
---|
| 348 | List.Cons ((Joint.MOVE |
---|
| 349 | (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons |
---|
| 350 | ((Joint.MOVE |
---|
| 351 | (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), |
---|
| 352 | List.Nil)))))) |
---|
| 353 | | Arg_decision_spill srco -> |
---|
| 354 | preserve_carry_bit globals carry_lives_after |
---|
| 355 | (get_stack globals dstr srco) |
---|
| 356 | | Arg_decision_imm int0 -> |
---|
| 357 | List.append (List.Cons ((Joint.MOVE |
---|
| 358 | (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), List.Nil)) |
---|
| 359 | (match I8051.eq_Register dstr I8051.RegisterA with |
---|
| 360 | | Bool.True -> List.Nil |
---|
| 361 | | Bool.False -> |
---|
| 362 | List.Cons ((Joint.MOVE |
---|
| 363 | (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil))) |
---|
| 364 | |
---|
| 365 | (** val arg_is_spilled : arg_decision -> Bool.bool **) |
---|
| 366 | let arg_is_spilled = function |
---|
| 367 | | Arg_decision_colour x0 -> Bool.False |
---|
| 368 | | Arg_decision_spill x0 -> Bool.True |
---|
| 369 | | Arg_decision_imm x0 -> Bool.False |
---|
| 370 | |
---|
| 371 | (** val is_spilled : Interference.decision -> Bool.bool **) |
---|
| 372 | let is_spilled = function |
---|
| 373 | | Interference.Decision_spill x0 -> Bool.True |
---|
| 374 | | Interference.Decision_colour x0 -> Bool.False |
---|
| 375 | |
---|
| 376 | (** val newframe : |
---|
| 377 | AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **) |
---|
| 378 | let newframe globals stack_sz = |
---|
| 379 | List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE |
---|
| 380 | (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons |
---|
| 381 | ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a), |
---|
| 382 | (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))), |
---|
| 383 | (List.Cons ((Joint.MOVE |
---|
| 384 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons |
---|
| 385 | ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))), |
---|
| 386 | (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a), |
---|
| 387 | (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons |
---|
| 388 | ((Joint.MOVE |
---|
| 389 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))), |
---|
| 390 | List.Nil))))))))))))) |
---|
| 391 | |
---|
| 392 | (** val delframe : |
---|
| 393 | AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **) |
---|
| 394 | let delframe globals stack_sz = |
---|
| 395 | List.Cons ((Joint.MOVE |
---|
| 396 | (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons |
---|
| 397 | ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a), |
---|
| 398 | (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))), |
---|
| 399 | (List.Cons ((Joint.MOVE |
---|
| 400 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons |
---|
| 401 | ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))), |
---|
| 402 | (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a), |
---|
| 403 | (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons |
---|
| 404 | ((Joint.MOVE |
---|
| 405 | (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))), |
---|
| 406 | List.Nil))))))))))) |
---|
| 407 | |
---|
| 408 | (** val commutative : BackEndOps.op2 -> Bool.bool **) |
---|
| 409 | let commutative = function |
---|
| 410 | | BackEndOps.Add -> Bool.True |
---|
| 411 | | BackEndOps.Addc -> Bool.True |
---|
| 412 | | BackEndOps.Sub -> Bool.False |
---|
| 413 | | BackEndOps.And -> Bool.True |
---|
| 414 | | BackEndOps.Or -> Bool.True |
---|
| 415 | | BackEndOps.Xor -> Bool.True |
---|
| 416 | |
---|
| 417 | (** val uses_carry : BackEndOps.op2 -> Bool.bool **) |
---|
| 418 | let uses_carry = function |
---|
| 419 | | BackEndOps.Add -> Bool.False |
---|
| 420 | | BackEndOps.Addc -> Bool.True |
---|
| 421 | | BackEndOps.Sub -> Bool.True |
---|
| 422 | | BackEndOps.And -> Bool.False |
---|
| 423 | | BackEndOps.Or -> Bool.False |
---|
| 424 | | BackEndOps.Xor -> Bool.False |
---|
| 425 | |
---|
| 426 | (** val sets_carry : BackEndOps.op2 -> Bool.bool **) |
---|
| 427 | let sets_carry = function |
---|
| 428 | | BackEndOps.Add -> Bool.True |
---|
| 429 | | BackEndOps.Addc -> Bool.True |
---|
| 430 | | BackEndOps.Sub -> Bool.True |
---|
| 431 | | BackEndOps.And -> Bool.False |
---|
| 432 | | BackEndOps.Or -> Bool.False |
---|
| 433 | | BackEndOps.Xor -> Bool.False |
---|
| 434 | |
---|
| 435 | (** val translate_op2 : |
---|
| 436 | AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> |
---|
| 437 | Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq |
---|
| 438 | List.list **) |
---|
| 439 | let translate_op2 globals carry_lives_after op4 dst arg1 arg2 = |
---|
| 440 | List.append |
---|
| 441 | (preserve_carry_bit globals |
---|
| 442 | (Bool.andb (uses_carry op4) |
---|
| 443 | (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))) |
---|
| 444 | (List.append |
---|
| 445 | (move globals Bool.False (Interference.Decision_colour |
---|
| 446 | I8051.RegisterB) arg2) |
---|
| 447 | (move globals Bool.False (Interference.Decision_colour |
---|
| 448 | I8051.RegisterA) arg1))) |
---|
| 449 | (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), (Obj.magic a), |
---|
| 450 | (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil)) |
---|
| 451 | (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst |
---|
| 452 | (Arg_decision_colour I8051.RegisterA))) |
---|
| 453 | |
---|
| 454 | (** val translate_op2_smart : |
---|
| 455 | AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> |
---|
| 456 | Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq |
---|
| 457 | List.list **) |
---|
| 458 | let translate_op2_smart globals carry_lives_after op4 dst arg1 arg2 = |
---|
| 459 | preserve_carry_bit globals |
---|
| 460 | (Bool.andb (Bool.andb (Bool.notb (sets_carry op4)) carry_lives_after) |
---|
| 461 | (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)) |
---|
| 462 | (is_spilled dst))) |
---|
| 463 | (match arg2 with |
---|
| 464 | | Arg_decision_colour arg2r -> |
---|
| 465 | List.append |
---|
| 466 | (move globals (uses_carry op4) (Interference.Decision_colour |
---|
| 467 | I8051.RegisterA) arg1) |
---|
| 468 | (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), |
---|
| 469 | (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))), |
---|
| 470 | List.Nil)) |
---|
| 471 | (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst |
---|
| 472 | (Arg_decision_colour I8051.RegisterA))) |
---|
| 473 | | Arg_decision_spill x -> |
---|
| 474 | (match commutative op4 with |
---|
| 475 | | Bool.True -> |
---|
| 476 | (match arg1 with |
---|
| 477 | | Arg_decision_colour arg1r -> |
---|
| 478 | List.append |
---|
| 479 | (move globals (uses_carry op4) (Interference.Decision_colour |
---|
| 480 | I8051.RegisterA) arg2) |
---|
| 481 | (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), |
---|
| 482 | (Obj.magic a), |
---|
| 483 | (Obj.magic (Joint.hdw_argument_from_reg arg1r)))), |
---|
| 484 | List.Nil)) |
---|
| 485 | (move globals (Bool.andb (sets_carry op4) carry_lives_after) |
---|
| 486 | dst (Arg_decision_colour I8051.RegisterA))) |
---|
| 487 | | Arg_decision_spill x0 -> |
---|
| 488 | translate_op2 globals carry_lives_after op4 dst arg1 arg2 |
---|
| 489 | | Arg_decision_imm arg1i -> |
---|
| 490 | List.append |
---|
| 491 | (move globals (uses_carry op4) (Interference.Decision_colour |
---|
| 492 | I8051.RegisterA) arg2) |
---|
| 493 | (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), |
---|
| 494 | (Obj.magic a), |
---|
| 495 | (Obj.magic (Joint.hdw_argument_from_byte arg1i)))), |
---|
| 496 | List.Nil)) |
---|
| 497 | (move globals (Bool.andb (sets_carry op4) carry_lives_after) |
---|
| 498 | dst (Arg_decision_colour I8051.RegisterA)))) |
---|
| 499 | | Bool.False -> |
---|
| 500 | translate_op2 globals carry_lives_after op4 dst arg1 arg2) |
---|
| 501 | | Arg_decision_imm arg2i -> |
---|
| 502 | List.append |
---|
| 503 | (move globals (uses_carry op4) (Interference.Decision_colour |
---|
| 504 | I8051.RegisterA) arg1) |
---|
| 505 | (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), |
---|
| 506 | (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))), |
---|
| 507 | List.Nil)) |
---|
| 508 | (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst |
---|
| 509 | (Arg_decision_colour I8051.RegisterA)))) |
---|
| 510 | |
---|
| 511 | (** val dec_to_arg_dec : Interference.decision -> arg_decision **) |
---|
| 512 | let dec_to_arg_dec = function |
---|
| 513 | | Interference.Decision_spill n -> Arg_decision_spill n |
---|
| 514 | | Interference.Decision_colour r -> Arg_decision_colour r |
---|
| 515 | |
---|
| 516 | (** val translate_op1 : |
---|
| 517 | AST.ident List.list -> Bool.bool -> BackEndOps.op1 -> |
---|
| 518 | Interference.decision -> Interference.decision -> Joint.joint_seq |
---|
| 519 | List.list **) |
---|
| 520 | let translate_op1 globals carry_lives_after op4 dst arg = |
---|
| 521 | let preserve_carry = |
---|
| 522 | Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg)) |
---|
| 523 | in |
---|
| 524 | preserve_carry_bit globals preserve_carry |
---|
| 525 | (List.append |
---|
| 526 | (move globals Bool.False (Interference.Decision_colour I8051.RegisterA) |
---|
| 527 | (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op4, |
---|
| 528 | (Obj.magic Types.It), (Obj.magic Types.It))), |
---|
| 529 | (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA))))) |
---|
| 530 | |
---|
| 531 | (** val translate_opaccs : |
---|
| 532 | AST.ident List.list -> Bool.bool -> BackEndOps.opAccs -> |
---|
| 533 | Interference.decision -> Interference.decision -> arg_decision -> |
---|
| 534 | arg_decision -> Joint.joint_seq List.list **) |
---|
| 535 | let translate_opaccs globals carry_lives_after op4 dst1 dst2 arg1 arg2 = |
---|
| 536 | List.append |
---|
| 537 | (move globals Bool.False (Interference.Decision_colour I8051.RegisterB) |
---|
| 538 | arg2) |
---|
| 539 | (List.append |
---|
| 540 | (move globals Bool.False (Interference.Decision_colour I8051.RegisterA) |
---|
| 541 | arg1) (List.Cons ((Joint.OPACCS (op4, (Obj.magic Types.It), |
---|
| 542 | (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It))), |
---|
| 543 | (List.append |
---|
| 544 | (move globals Bool.False dst1 (Arg_decision_colour I8051.RegisterA)) |
---|
| 545 | (List.append |
---|
| 546 | (move globals Bool.False dst2 (Arg_decision_colour |
---|
| 547 | I8051.RegisterB)) |
---|
| 548 | (match Bool.andb carry_lives_after |
---|
| 549 | (Bool.orb (is_spilled dst1) (is_spilled dst2)) with |
---|
| 550 | | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil) |
---|
| 551 | | Bool.False -> List.Nil)))))) |
---|
| 552 | |
---|
| 553 | (** val move_to_dp : |
---|
| 554 | AST.ident List.list -> arg_decision -> arg_decision -> Joint.joint_seq |
---|
| 555 | List.list **) |
---|
| 556 | let move_to_dp globals arg1 arg2 = |
---|
| 557 | match Bool.notb (arg_is_spilled arg1) with |
---|
| 558 | | Bool.True -> |
---|
| 559 | List.append |
---|
| 560 | (move globals Bool.False (Interference.Decision_colour |
---|
| 561 | I8051.RegisterDPH) arg2) |
---|
| 562 | (move globals Bool.False (Interference.Decision_colour |
---|
| 563 | I8051.RegisterDPL) arg1) |
---|
| 564 | | Bool.False -> |
---|
| 565 | (match Bool.notb (arg_is_spilled arg2) with |
---|
| 566 | | Bool.True -> |
---|
| 567 | List.append |
---|
| 568 | (move globals Bool.False (Interference.Decision_colour |
---|
| 569 | I8051.RegisterDPL) arg1) |
---|
| 570 | (move globals Bool.False (Interference.Decision_colour |
---|
| 571 | I8051.RegisterDPH) arg2) |
---|
| 572 | | Bool.False -> |
---|
| 573 | List.append |
---|
| 574 | (move globals Bool.False (Interference.Decision_colour |
---|
| 575 | I8051.RegisterB) arg1) |
---|
| 576 | (List.append |
---|
| 577 | (move globals Bool.False (Interference.Decision_colour |
---|
| 578 | I8051.RegisterDPH) arg2) |
---|
| 579 | (move globals Bool.False (Interference.Decision_colour |
---|
| 580 | I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB)))) |
---|
| 581 | |
---|
| 582 | (** val translate_store : |
---|
| 583 | AST.ident List.list -> Bool.bool -> arg_decision -> arg_decision -> |
---|
| 584 | arg_decision -> Joint.joint_seq List.list **) |
---|
| 585 | let translate_store globals carry_lives_after addr1 addr2 src = |
---|
| 586 | preserve_carry_bit globals |
---|
| 587 | (Bool.andb carry_lives_after |
---|
| 588 | (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1)) |
---|
| 589 | (arg_is_spilled src))) |
---|
| 590 | (let move_to_dptr = move_to_dp globals addr1 addr2 in |
---|
| 591 | List.append |
---|
| 592 | (match arg_is_spilled src with |
---|
| 593 | | Bool.True -> |
---|
| 594 | List.append |
---|
| 595 | (move globals Bool.False (Interference.Decision_colour |
---|
| 596 | I8051.registerST0) src) |
---|
| 597 | (List.append move_to_dptr (List.Cons ((Joint.MOVE |
---|
| 598 | (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))), |
---|
| 599 | List.Nil))) |
---|
| 600 | | Bool.False -> move_to_dptr) (List.Cons ((Joint.STORE |
---|
| 601 | ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))), |
---|
| 602 | List.Nil))) |
---|
| 603 | |
---|
| 604 | (** val translate_load : |
---|
| 605 | AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision |
---|
| 606 | -> arg_decision -> Joint.joint_seq List.list **) |
---|
| 607 | let translate_load globals carry_lives_after dst addr1 addr2 = |
---|
| 608 | preserve_carry_bit globals |
---|
| 609 | (Bool.andb carry_lives_after |
---|
| 610 | (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1)) |
---|
| 611 | (arg_is_spilled addr1))) |
---|
| 612 | (List.append (move_to_dp globals addr1 addr2) |
---|
| 613 | (List.append (List.Cons ((Joint.LOAD ((Obj.magic a), |
---|
| 614 | (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil)) |
---|
| 615 | (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA)))) |
---|
| 616 | |
---|
| 617 | (** val translate_address : |
---|
| 618 | __ List.list -> Bool.bool -> __ -> Interference.decision -> |
---|
| 619 | Interference.decision -> Joint.joint_seq List.list **) |
---|
| 620 | let translate_address globals carry_lives_after id addr1 addr2 = |
---|
| 621 | preserve_carry_bit (Obj.magic globals) |
---|
| 622 | (Bool.andb carry_lives_after |
---|
| 623 | (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons |
---|
| 624 | ((Joint.ADDRESS ((Obj.magic id), (Obj.magic Types.It), |
---|
| 625 | (Obj.magic Types.It))), |
---|
| 626 | (List.append |
---|
| 627 | (move (Obj.magic globals) Bool.False addr1 (Arg_decision_colour |
---|
| 628 | I8051.RegisterDPL)) |
---|
| 629 | (move (Obj.magic globals) Bool.False addr2 (Arg_decision_colour |
---|
| 630 | I8051.RegisterDPH))))) |
---|
| 631 | |
---|
| 632 | (** val translate_low_address : |
---|
| 633 | AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label |
---|
| 634 | -> Joint.joint_seq List.list **) |
---|
| 635 | let translate_low_address globals carry_lives_after dst lbl = |
---|
| 636 | match dst with |
---|
| 637 | | Interference.Decision_spill x -> |
---|
| 638 | List.Cons ((Joint.Extension_seq |
---|
| 639 | (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (I8051.RegisterA, lbl)))), |
---|
| 640 | (move globals carry_lives_after dst (Arg_decision_colour |
---|
| 641 | I8051.RegisterA))) |
---|
| 642 | | Interference.Decision_colour r -> |
---|
| 643 | List.Cons ((Joint.Extension_seq |
---|
| 644 | (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (r, lbl)))), List.Nil) |
---|
| 645 | |
---|
| 646 | (** val translate_high_address : |
---|
| 647 | AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label |
---|
| 648 | -> Joint.joint_seq List.list **) |
---|
| 649 | let translate_high_address globals carry_lives_after dst lbl = |
---|
| 650 | match dst with |
---|
| 651 | | Interference.Decision_spill x -> |
---|
| 652 | List.Cons ((Joint.Extension_seq |
---|
| 653 | (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (I8051.RegisterA, lbl)))), |
---|
| 654 | (move globals carry_lives_after dst (Arg_decision_colour |
---|
| 655 | I8051.RegisterA))) |
---|
| 656 | | Interference.Decision_colour r -> |
---|
| 657 | List.Cons ((Joint.Extension_seq |
---|
| 658 | (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (r, lbl)))), List.Nil) |
---|
| 659 | |
---|
| 660 | (** val translate_step : |
---|
| 661 | AST.ident List.list -> Fixpoints.valuation -> Interference.coloured_graph |
---|
| 662 | -> Nat.nat -> Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **) |
---|
| 663 | let translate_step globals after grph stack_sz lbl s = |
---|
| 664 | Bind_new.Bret |
---|
| 665 | (let lookup1 = fun r -> grph.Interference.colouring (Types.Inl r) in |
---|
| 666 | let lookup_arg = fun a0 -> |
---|
| 667 | match a0 with |
---|
| 668 | | Joint.Reg r -> dec_to_arg_dec (lookup1 r) |
---|
| 669 | | Joint.Imm b -> Arg_decision_imm b |
---|
| 670 | in |
---|
| 671 | let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl) |
---|
| 672 | in |
---|
| 673 | let move0 = move globals carry_lives_after in |
---|
| 674 | (match s with |
---|
| 675 | | Joint.COST_LABEL cost_lbl -> |
---|
| 676 | { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x -> |
---|
| 677 | Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil } |
---|
| 678 | | Joint.CALL (f, n_args, x) -> |
---|
| 679 | (match f with |
---|
| 680 | | Types.Inl f0 -> |
---|
| 681 | { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 -> |
---|
| 682 | Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) }; |
---|
| 683 | Types.snd = List.Nil } |
---|
| 684 | | Types.Inr dp -> |
---|
| 685 | let { Types.fst = dpl; Types.snd = dph } = dp in |
---|
| 686 | { Types.fst = { Types.fst = |
---|
| 687 | (Blocks.add_dummy_variance |
---|
| 688 | (move_to_dp globals (Obj.magic lookup_arg dpl) |
---|
| 689 | (Obj.magic lookup_arg dph))); Types.snd = (fun x0 -> Joint.CALL |
---|
| 690 | ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd = |
---|
| 691 | (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) }; |
---|
| 692 | Types.snd = List.Nil }) |
---|
| 693 | | Joint.COND (r, ltrue) -> |
---|
| 694 | { Types.fst = { Types.fst = |
---|
| 695 | (Blocks.add_dummy_variance |
---|
| 696 | (move0 (Interference.Decision_colour I8051.RegisterA) |
---|
| 697 | (dec_to_arg_dec (Obj.magic lookup1 r)))); Types.snd = (fun x -> |
---|
| 698 | Joint.COND ((Obj.magic Types.It), ltrue)) }; Types.snd = List.Nil } |
---|
| 699 | | Joint.Step_seq s' -> |
---|
| 700 | (match s' with |
---|
| 701 | | Joint.COMMENT c -> |
---|
| 702 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 703 | globals (List.Cons ((Joint.COMMENT c), List.Nil)) |
---|
| 704 | | Joint.MOVE pair_regs -> |
---|
| 705 | let lookup_move_dst = fun x -> |
---|
| 706 | match x with |
---|
| 707 | | ERTL.PSD r -> lookup1 r |
---|
| 708 | | ERTL.HDW r -> Interference.Decision_colour r |
---|
| 709 | in |
---|
| 710 | let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in |
---|
| 711 | let src = |
---|
| 712 | match (Obj.magic pair_regs).Types.snd with |
---|
| 713 | | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r) |
---|
| 714 | | Joint.Imm b -> Arg_decision_imm b |
---|
| 715 | in |
---|
| 716 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 717 | globals (move0 dst src) |
---|
| 718 | | Joint.POP r -> |
---|
| 719 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 720 | globals (List.Cons ((Joint.POP (Obj.magic a)), |
---|
| 721 | (move0 (Obj.magic lookup1 r) (Arg_decision_colour |
---|
| 722 | I8051.RegisterA)))) |
---|
| 723 | | Joint.PUSH a0 -> |
---|
| 724 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 725 | globals |
---|
| 726 | (List.append |
---|
| 727 | (move0 (Interference.Decision_colour I8051.RegisterA) |
---|
| 728 | (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH |
---|
| 729 | (Obj.magic a)), List.Nil))) |
---|
| 730 | | Joint.ADDRESS (lbl0, dpl, dph) -> |
---|
| 731 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 732 | globals |
---|
| 733 | (translate_address (Obj.magic globals) carry_lives_after |
---|
| 734 | (Obj.magic lbl0) (Obj.magic lookup1 dpl) |
---|
| 735 | (Obj.magic lookup1 dph)) |
---|
| 736 | | Joint.OPACCS (op4, dst1, dst2, arg1, arg2) -> |
---|
| 737 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 738 | globals |
---|
| 739 | (translate_opaccs globals carry_lives_after op4 |
---|
| 740 | (Obj.magic lookup1 dst1) (Obj.magic lookup1 dst2) |
---|
| 741 | (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2)) |
---|
| 742 | | Joint.OP1 (op4, dst, arg) -> |
---|
| 743 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 744 | globals |
---|
| 745 | (translate_op1 globals carry_lives_after op4 |
---|
| 746 | (Obj.magic lookup1 dst) (Obj.magic lookup1 arg)) |
---|
| 747 | | Joint.OP2 (op4, dst, arg1, arg2) -> |
---|
| 748 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 749 | globals |
---|
| 750 | (translate_op2_smart globals carry_lives_after op4 |
---|
| 751 | (Obj.magic lookup1 dst) (Obj.magic lookup_arg arg1) |
---|
| 752 | (Obj.magic lookup_arg arg2)) |
---|
| 753 | | Joint.CLEAR_CARRY -> |
---|
| 754 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 755 | globals (List.Cons (Joint.CLEAR_CARRY, List.Nil)) |
---|
| 756 | | Joint.SET_CARRY -> |
---|
| 757 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 758 | globals (List.Cons (Joint.CLEAR_CARRY, List.Nil)) |
---|
| 759 | | Joint.LOAD (dstr, addr1, addr2) -> |
---|
| 760 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 761 | globals |
---|
| 762 | (translate_load globals carry_lives_after |
---|
| 763 | (Obj.magic lookup1 dstr) (Obj.magic lookup_arg addr1) |
---|
| 764 | (Obj.magic lookup_arg addr2)) |
---|
| 765 | | Joint.STORE (addr1, addr2, srcr) -> |
---|
| 766 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 767 | globals |
---|
| 768 | (translate_store globals carry_lives_after |
---|
| 769 | (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2) |
---|
| 770 | (Obj.magic lookup_arg srcr)) |
---|
| 771 | | Joint.Extension_seq ext -> |
---|
| 772 | Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) |
---|
| 773 | globals |
---|
| 774 | (match Obj.magic ext with |
---|
| 775 | | ERTLptr.Ertlptr_ertl ext' -> |
---|
| 776 | (match ext' with |
---|
| 777 | | ERTL.Ertl_new_frame -> newframe globals stack_sz |
---|
| 778 | | ERTL.Ertl_del_frame -> delframe globals stack_sz |
---|
| 779 | | ERTL.Ertl_frame_size r -> |
---|
| 780 | move0 (lookup1 r) (Arg_decision_imm |
---|
| 781 | (Joint.byte_of_nat stack_sz))) |
---|
| 782 | | ERTLptr.LOW_ADDRESS (r5, l) -> |
---|
| 783 | translate_low_address globals carry_lives_after (lookup1 r5) l |
---|
| 784 | | ERTLptr.HIGH_ADDRESS (r5, l) -> |
---|
| 785 | translate_high_address globals carry_lives_after (lookup1 r5) |
---|
| 786 | l)))) |
---|
| 787 | |
---|
| 788 | (** val translate_fin_step : |
---|
| 789 | AST.ident List.list -> Graphs.label -> Joint.joint_fin_step -> |
---|
| 790 | Blocks.bind_fin_block **) |
---|
| 791 | let translate_fin_step globals lbl s = |
---|
| 792 | Bind_new.Bret { Types.fst = List.Nil; Types.snd = |
---|
| 793 | (match s with |
---|
| 794 | | Joint.GOTO l -> Joint.GOTO l |
---|
| 795 | | Joint.RETURN -> Joint.RETURN |
---|
| 796 | | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) } |
---|
| 797 | |
---|
| 798 | (** val translate_data : |
---|
| 799 | Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer -> |
---|
| 800 | AST.ident List.list -> Joint.joint_closed_internal_function -> |
---|
| 801 | (Registers.register, TranslateUtils.b_graph_translate_data) |
---|
| 802 | Bind_new.bind_new **) |
---|
| 803 | let translate_data the_fixpoint build globals int_fun = |
---|
| 804 | let after = |
---|
| 805 | Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun) |
---|
| 806 | in |
---|
| 807 | let coloured_graph0 = build after in |
---|
| 808 | let stack_sz = |
---|
| 809 | Nat.plus coloured_graph0.Interference.spilled_no |
---|
| 810 | (Types.pi1 int_fun).Joint.joint_if_stacksize |
---|
| 811 | in |
---|
| 812 | Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It); |
---|
| 813 | TranslateUtils.init_params = (Obj.magic Types.It); |
---|
| 814 | TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue = |
---|
| 815 | List.Nil; TranslateUtils.f_step = |
---|
| 816 | (translate_step globals after coloured_graph0 stack_sz); |
---|
| 817 | TranslateUtils.f_fin = (translate_fin_step globals) } |
---|
| 818 | |
---|
| 819 | (** val ertlptr_to_ltl : |
---|
| 820 | Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer -> |
---|
| 821 | ERTLptr.ertlptr_program -> LTL.ltl_program **) |
---|
| 822 | let ertlptr_to_ltl the_fixpoint build = |
---|
| 823 | TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL |
---|
| 824 | (translate_data the_fixpoint build) |
---|
| 825 | |
---|