HCoop / hcoop / debian / mlton.git / blame
| Commit | Line | Data |
|---|---|---|
| 7f918cf1 CE |
1 | (* Copyright (C) 2009 Matthew Fluet. |
| 2 | * Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh | |
| 3 | * Jagannathan, and Stephen Weeks. | |
| 4 | * Copyright (C) 1997-2000 NEC Research Institute. | |
| 5 | * | |
| 6 | * MLton is released under a BSD-style license. | |
| 7 | * See the file MLton-LICENSE for details. | |
| 8 | *) | |
| 9 | ||
| 10 | functor x86Liveness(S: X86_LIVENESS_STRUCTS) : X86_LIVENESS = | |
| 11 | struct | |
| 12 | open S | |
| 13 | open x86 | |
| 14 | ||
| 15 | val tracer = x86.tracer | |
| 16 | val tracerTop = x86.tracerTop | |
| 17 | ||
| 18 | structure LiveSet = struct | |
| 19 | open MemLocSet | |
| 20 | fun toMemLocSet s = s | |
| 21 | end | |
| 22 | fun track memloc = ClassSet.contains(!x86MLtonBasic.Classes.livenessClasses, | |
| 23 | MemLoc.class memloc) | |
| 24 | ||
| 25 | fun livenessOperands live | |
| 26 | = List.fold | |
| 27 | (live, | |
| 28 | LiveSet.empty, | |
| 29 | fn (operand, live) | |
| 30 | => (case Operand.deMemloc operand | |
| 31 | of NONE => live | |
| 32 | | SOME memloc | |
| 33 | => if track memloc | |
| 34 | then LiveSet.add(live, memloc) | |
| 35 | else live)) | |
| 36 | ||
| 37 | structure LiveInfo = | |
| 38 | struct | |
| 39 | datatype t = T of {get: Label.t -> LiveSet.t, | |
| 40 | set: Label.t * LiveSet.t -> unit} | |
| 41 | ||
| 42 | fun newLiveInfo () | |
| 43 | = let | |
| 44 | val {get : Label.t -> LiveSet.t, | |
| 45 | set : Label.t * LiveSet.t -> unit, ...} | |
| 46 | = Property.getSet | |
| 47 | (Label.plist, Property.initRaise ("liveInfo", Label.layout)) | |
| 48 | in | |
| 49 | T {get = get, set = set} | |
| 50 | end | |
| 51 | ||
| 52 | fun setLiveOperands (T {set, ...}, label, live) | |
| 53 | = set(label, livenessOperands live) | |
| 54 | fun setLive (T {set, ...}, label, live) | |
| 55 | = set(label, live) | |
| 56 | fun getLive (T {get, ...}, label) | |
| 57 | = get label | |
| 58 | end | |
| 59 | ||
| 60 | fun liveness_uses_defs {uses : Operand.t list, | |
| 61 | defs : Operand.t list} : | |
| 62 | {uses : LiveSet.t, | |
| 63 | defs : LiveSet.t} | |
| 64 | = let | |
| 65 | val baseUses = livenessOperands uses | |
| 66 | val livenessUses | |
| 67 | = let | |
| 68 | fun doit (operands, livenessUses) | |
| 69 | = List.fold | |
| 70 | (operands, | |
| 71 | livenessUses, | |
| 72 | fn (operand, livenessUses) | |
| 73 | => case Operand.deMemloc operand | |
| 74 | of SOME memloc | |
| 75 | => List.fold | |
| 76 | (MemLoc.utilized memloc, | |
| 77 | livenessUses, | |
| 78 | fn (memloc, livenessUses) | |
| 79 | => if track memloc | |
| 80 | then LiveSet.add(livenessUses, memloc) | |
| 81 | else livenessUses) | |
| 82 | | NONE => livenessUses) | |
| 83 | in | |
| 84 | doit(defs, | |
| 85 | doit(uses, | |
| 86 | baseUses)) | |
| 87 | end | |
| 88 | ||
| 89 | val baseDefs = livenessOperands defs | |
| 90 | val livenessDefs = baseDefs | |
| 91 | in | |
| 92 | {uses = livenessUses, | |
| 93 | defs = livenessDefs} | |
| 94 | end | |
| 95 | ||
| 96 | structure Liveness = | |
| 97 | struct | |
| 98 | datatype t = T of {liveIn: LiveSet.t, | |
| 99 | liveOut: LiveSet.t, | |
| 100 | dead: LiveSet.t} | |
| 101 | ||
| 102 | local | |
| 103 | fun make f (T r) = f r | |
| 104 | in | |
| 105 | val dead = make #dead | |
| 106 | val liveIn = make #liveIn | |
| 107 | end | |
| 108 | ||
| 109 | fun toString (T {liveIn, liveOut, dead}) | |
| 110 | = let | |
| 111 | fun doit (name, l, toString, s) | |
| 112 | = LiveSet.fold(l, s, | |
| 113 | fn (x, s) | |
| 114 | => concat [name, toString x, "\n", s]) | |
| 115 | in | |
| 116 | doit("liveIn: ", liveIn, MemLoc.toString, | |
| 117 | doit("liveOut: ", liveOut, MemLoc.toString, | |
| 118 | doit("dead: ", dead, MemLoc.toString, | |
| 119 | ""))) | |
| 120 | end | |
| 121 | ||
| 122 | ||
| 123 | fun eq (T {liveIn = liveIn1, | |
| 124 | liveOut = liveOut1, | |
| 125 | dead = dead1}, | |
| 126 | T {liveIn = liveIn2, | |
| 127 | liveOut = liveOut2, | |
| 128 | dead = dead2}) | |
| 129 | = LiveSet.equals(liveIn1, liveIn2) andalso | |
| 130 | LiveSet.equals(liveOut1, liveOut2) andalso | |
| 131 | LiveSet.equals(dead1, dead2) | |
| 132 | ||
| 133 | fun liveness ({uses : LiveSet.t, | |
| 134 | defs : LiveSet.t, | |
| 135 | live : LiveSet.t}) : t | |
| 136 | = let | |
| 137 | val liveOut = live | |
| 138 | ||
| 139 | (* liveIn = uses \/ (liveOut - defs) *) | |
| 140 | val liveIn = LiveSet.+(uses, LiveSet.-(live, defs)) | |
| 141 | ||
| 142 | (* dead = (liveIn \/ defs) - liveOut *) | |
| 143 | val dead = LiveSet.-(LiveSet.+(liveIn, defs), liveOut) | |
| 144 | in | |
| 145 | T {liveIn = liveIn, | |
| 146 | liveOut = liveOut, | |
| 147 | dead = dead} | |
| 148 | end | |
| 149 | ||
| 150 | fun livenessEntry {entry : Entry.t, | |
| 151 | live : LiveSet.t} : t | |
| 152 | = let | |
| 153 | val {uses, defs, ...} = Entry.uses_defs_kills entry | |
| 154 | val {uses, defs} = liveness_uses_defs {uses = uses, defs = defs} | |
| 155 | val defs = MemLocSet.fold | |
| 156 | (Entry.live entry, | |
| 157 | defs, | |
| 158 | fn (memloc, defs) | |
| 159 | => if track memloc | |
| 160 | then LiveSet.add(defs, memloc) | |
| 161 | else defs) | |
| 162 | in | |
| 163 | liveness {uses = uses, | |
| 164 | defs = defs, | |
| 165 | live = live} | |
| 166 | end | |
| 167 | ||
| 168 | fun livenessAssembly {assembly : Assembly.t, | |
| 169 | live : LiveSet.t} : t | |
| 170 | = let | |
| 171 | val {uses, defs, ...} = Assembly.uses_defs_kills assembly | |
| 172 | val {uses, defs} = liveness_uses_defs {uses = uses, defs = defs} | |
| 173 | in | |
| 174 | liveness {uses = uses, | |
| 175 | defs = defs, | |
| 176 | live = live} | |
| 177 | end | |
| 178 | ||
| 179 | fun livenessTransfer' {transfer: Transfer.t, | |
| 180 | live : LiveSet.t} : t | |
| 181 | = let | |
| 182 | val {uses,defs,...} = Transfer.uses_defs_kills transfer | |
| 183 | val {uses,defs} = liveness_uses_defs {uses = uses, defs = defs} | |
| 184 | (* Transfer.live transfer could be considered uses, | |
| 185 | * but the Liveness.t of a transfer should have | |
| 186 | * Transfer.live transfer as liveOut. | |
| 187 | *) | |
| 188 | val live = MemLocSet.fold | |
| 189 | (Transfer.live transfer, | |
| 190 | live, | |
| 191 | fn (memloc, live) | |
| 192 | => if track memloc | |
| 193 | then LiveSet.add(live, memloc) | |
| 194 | else live) | |
| 195 | in | |
| 196 | liveness {uses = uses, | |
| 197 | defs = defs, | |
| 198 | live = live} | |
| 199 | end | |
| 200 | ||
| 201 | fun livenessTransfer {transfer: Transfer.t, | |
| 202 | liveInfo: LiveInfo.t} : t | |
| 203 | = let | |
| 204 | val targets = Transfer.nearTargets transfer | |
| 205 | val live | |
| 206 | = List.fold | |
| 207 | (targets, | |
| 208 | LiveSet.empty, | |
| 209 | fn (target, live) | |
| 210 | => LiveSet.union(LiveInfo.getLive(liveInfo, target), | |
| 211 | live)) | |
| 212 | in | |
| 213 | livenessTransfer' {transfer = transfer, | |
| 214 | live = live} | |
| 215 | end | |
| 216 | ||
| 217 | fun livenessBlock {block = Block.T {entry, statements, transfer, ...}, | |
| 218 | liveInfo : LiveInfo.t} | |
| 219 | = let | |
| 220 | val T {liveIn = live, ...} | |
| 221 | = livenessTransfer {transfer = transfer, | |
| 222 | liveInfo = liveInfo} | |
| 223 | ||
| 224 | val live | |
| 225 | = List.foldr | |
| 226 | (statements, | |
| 227 | live, | |
| 228 | fn (asm,live) | |
| 229 | => let | |
| 230 | val T {liveIn = live, ...} | |
| 231 | = livenessAssembly {assembly = asm, | |
| 232 | live = live} | |
| 233 | in | |
| 234 | live | |
| 235 | end) | |
| 236 | ||
| 237 | val T {liveIn = live, ...} | |
| 238 | = livenessEntry {entry = entry, | |
| 239 | live = live} | |
| 240 | in | |
| 241 | live | |
| 242 | end | |
| 243 | end | |
| 244 | ||
| 245 | structure LiveInfo = | |
| 246 | struct | |
| 247 | open LiveInfo | |
| 248 | ||
| 249 | fun completeLiveInfo {chunk = Chunk.T {blocks, ...}, | |
| 250 | liveInfo : LiveInfo.t, | |
| 251 | pass: string} | |
| 252 | = let | |
| 253 | val {get = getBlockInfo : | |
| 254 | Label.t -> {pred: Label.t list ref, | |
| 255 | block: Block.t option ref, | |
| 256 | topo: int ref}, | |
| 257 | destroy = destBlockInfo} | |
| 258 | = Property.destGet | |
| 259 | (Label.plist, | |
| 260 | Property.initFun (fn _ => {pred = ref [], | |
| 261 | block = ref NONE, | |
| 262 | topo = ref ~1})) | |
| 263 | val get_pred = (#pred o getBlockInfo) | |
| 264 | val get_topo = (#topo o getBlockInfo) | |
| 265 | val get_pred' = (! o #pred o getBlockInfo) | |
| 266 | val get_block' = (! o #block o getBlockInfo) | |
| 267 | val get_topo' = (! o #topo o getBlockInfo) | |
| 268 | ||
| 269 | val labels | |
| 270 | = List.map | |
| 271 | (blocks, | |
| 272 | fn block' as Block.T {entry, transfer,...} | |
| 273 | => let | |
| 274 | val label = Entry.label entry | |
| 275 | val {block,topo,...} = getBlockInfo label | |
| 276 | val targets = Transfer.nearTargets transfer | |
| 277 | in | |
| 278 | block := SOME block'; | |
| 279 | topo := 0; | |
| 280 | List.foreach | |
| 281 | (targets, | |
| 282 | fn target => List.push(get_pred target, label)); | |
| 283 | label | |
| 284 | end) | |
| 285 | ||
| 286 | local | |
| 287 | val todo = ref [] | |
| 288 | fun topo_order(x,y) = Int.compare(get_topo' x, get_topo' y) | |
| 289 | ||
| 290 | fun insert (l, x, compare) | |
| 291 | = let | |
| 292 | val rec insert' | |
| 293 | = fn ([],acc) => List.appendRev(acc, [x]) | |
| 294 | | (l as h::t,acc) | |
| 295 | => (case compare(h,x) | |
| 296 | of LESS | |
| 297 | => insert' (t, h::acc) | |
| 298 | | EQUAL | |
| 299 | => List.appendRev(acc, l) | |
| 300 | | GREATER | |
| 301 | => List.appendRev(acc, x::l)) | |
| 302 | in | |
| 303 | insert' (l,[]) | |
| 304 | end | |
| 305 | in | |
| 306 | fun add_todo x = todo := insert(!todo, x, topo_order) | |
| 307 | fun push_todo x = todo := x::(!todo) | |
| 308 | fun rev_todo () = todo := List.rev (!todo) | |
| 309 | fun get_todo () | |
| 310 | = (case !todo | |
| 311 | of [] => NONE | |
| 312 | | (x::todo') => (todo := todo'; | |
| 313 | SOME x)) | |
| 314 | end | |
| 315 | ||
| 316 | local | |
| 317 | val num = Counter.new 1 | |
| 318 | in | |
| 319 | fun topo_sort label | |
| 320 | = let | |
| 321 | val {topo, pred, ...} = getBlockInfo label | |
| 322 | in | |
| 323 | if !topo = 0 | |
| 324 | then (topo := Counter.next num; | |
| 325 | push_todo label; | |
| 326 | List.foreach(!pred, topo_sort)) | |
| 327 | else () | |
| 328 | end | |
| 329 | fun topo_root label | |
| 330 | = (get_topo label := Counter.next num; | |
| 331 | push_todo label) | |
| 332 | end | |
| 333 | ||
| 334 | fun loop (labels, n) | |
| 335 | = if List.isEmpty labels | |
| 336 | then () | |
| 337 | else let | |
| 338 | val {yes = exits, no = labels} | |
| 339 | = List.partition | |
| 340 | (labels, | |
| 341 | fn label | |
| 342 | => let | |
| 343 | val Block.T {transfer, ...} | |
| 344 | = valOf (get_block' label) | |
| 345 | val targets = Transfer.nearTargets transfer | |
| 346 | ||
| 347 | val targets' | |
| 348 | = List.fold(targets, | |
| 349 | 0, | |
| 350 | fn (target,targets') | |
| 351 | => if get_topo' target = ~1 | |
| 352 | then targets' | |
| 353 | else targets' + 1) | |
| 354 | in | |
| 355 | targets' = n | |
| 356 | end) | |
| 357 | val exits | |
| 358 | = List.removeAll | |
| 359 | (exits, | |
| 360 | fn label => get_topo' label <> 0) | |
| 361 | val _ | |
| 362 | = (List.foreach | |
| 363 | (exits, | |
| 364 | fn label => topo_root label); | |
| 365 | List.foreach | |
| 366 | (exits, | |
| 367 | fn label | |
| 368 | => List.foreach(get_pred' label, topo_sort))) | |
| 369 | in | |
| 370 | loop(labels, n + 1) | |
| 371 | end | |
| 372 | val _ = loop(labels, 0) | |
| 373 | val _ = rev_todo () | |
| 374 | ||
| 375 | val changed = ref false | |
| 376 | fun doit () | |
| 377 | = (case get_todo () | |
| 378 | of NONE => () | |
| 379 | | SOME label | |
| 380 | => let | |
| 381 | val {pred, block, ...} = getBlockInfo label | |
| 382 | val block = valOf (!block) | |
| 383 | val live = Liveness.livenessBlock {block = block, | |
| 384 | liveInfo = liveInfo} | |
| 385 | ||
| 386 | val live' = LiveInfo.getLive(liveInfo, label) | |
| 387 | in | |
| 388 | if LiveSet.equals(live, live') | |
| 389 | then () | |
| 390 | else (LiveInfo.setLive(liveInfo, label, live); | |
| 391 | List.foreach(!pred, add_todo); | |
| 392 | if true then () else | |
| 393 | (print "completeLiveInfo:"; | |
| 394 | print pass; | |
| 395 | print ": "; | |
| 396 | print (Label.toString label); | |
| 397 | print ": "; | |
| 398 | if LiveSet.<(live, live') | |
| 399 | then print "new < old" | |
| 400 | else if LiveSet.<(live', live) | |
| 401 | then print "old < new" | |
| 402 | else print "?"; | |
| 403 | print "\n"; | |
| 404 | if true | |
| 405 | then (print "old: "; | |
| 406 | LiveSet.foreach | |
| 407 | (live', fn m => | |
| 408 | (print (MemLoc.toString m); | |
| 409 | print " ")); | |
| 410 | print "\n"; | |
| 411 | print "new: "; | |
| 412 | LiveSet.foreach | |
| 413 | (live, fn m => | |
| 414 | (print (MemLoc.toString m); | |
| 415 | print " ")); | |
| 416 | print "\n") | |
| 417 | else ()); | |
| 418 | changed := true); | |
| 419 | doit () | |
| 420 | end) | |
| 421 | ||
| 422 | val _ = doit () | |
| 423 | val _ = destBlockInfo () | |
| 424 | in | |
| 425 | () | |
| 426 | end | |
| 427 | ||
| 428 | val (completeLiveInfo : {chunk: Chunk.t, | |
| 429 | liveInfo: LiveInfo.t, | |
| 430 | pass: string} -> unit, | |
| 431 | completeLiveInfo_msg) | |
| 432 | = tracerTop | |
| 433 | "completeLiveInfo" | |
| 434 | completeLiveInfo | |
| 435 | ||
| 436 | fun verifyLiveInfo {chunk = Chunk.T {blocks, ...}, | |
| 437 | liveInfo : t} | |
| 438 | = List.forall | |
| 439 | (blocks, | |
| 440 | fn block as Block.T {entry, ...} | |
| 441 | => let | |
| 442 | val label = Entry.label entry | |
| 443 | val live = LiveInfo.getLive(liveInfo, label) | |
| 444 | val live' = Liveness.livenessBlock {block = block, | |
| 445 | liveInfo = liveInfo} | |
| 446 | in | |
| 447 | LiveSet.equals(live, live') | |
| 448 | end) | |
| 449 | ||
| 450 | val (verifyLiveInfo : {chunk: Chunk.t, liveInfo: LiveInfo.t} -> bool, | |
| 451 | verifyLiveInfo_msg) | |
| 452 | = tracer | |
| 453 | "verifyLiveInfo" | |
| 454 | verifyLiveInfo | |
| 455 | ||
| 456 | end | |
| 457 | ||
| 458 | structure LivenessBlock = | |
| 459 | struct | |
| 460 | datatype t = T of {entry: (Entry.t * Liveness.t), | |
| 461 | profileLabel: ProfileLabel.t option, | |
| 462 | statements: (Assembly.t * Liveness.t) list, | |
| 463 | transfer: Transfer.t * Liveness.t} | |
| 464 | ||
| 465 | fun printBlock (T {entry, statements, transfer, ...}) | |
| 466 | = (let | |
| 467 | val (entry,info) = entry | |
| 468 | in | |
| 469 | print (Entry.toString entry); | |
| 470 | print "\n"; | |
| 471 | print (Liveness.toString info) | |
| 472 | end; | |
| 473 | List.foreach | |
| 474 | (statements, | |
| 475 | fn (asm,info) | |
| 476 | => (print (Assembly.toString asm); | |
| 477 | print "\n"; | |
| 478 | print (Liveness.toString info))); | |
| 479 | let | |
| 480 | val (trans,info) = transfer | |
| 481 | in | |
| 482 | print (Transfer.toString trans); | |
| 483 | print "\n"; | |
| 484 | print (Liveness.toString info); | |
| 485 | print "\n" | |
| 486 | end) | |
| 487 | ||
| 488 | fun toLivenessEntry {entry, | |
| 489 | live} | |
| 490 | = let | |
| 491 | val info as Liveness.T {liveIn = live, ...} | |
| 492 | = Liveness.livenessEntry {entry = entry, | |
| 493 | live = live} | |
| 494 | in | |
| 495 | {entry = (entry,info), | |
| 496 | live = live} | |
| 497 | end | |
| 498 | ||
| 499 | fun reLivenessEntry {entry, | |
| 500 | live} | |
| 501 | = let | |
| 502 | val (entry,_) = entry | |
| 503 | val info as Liveness.T {liveIn = live, ...} | |
| 504 | = Liveness.livenessEntry {entry = entry, | |
| 505 | live = live} | |
| 506 | in | |
| 507 | {entry = (entry,info), | |
| 508 | live = live} | |
| 509 | end | |
| 510 | ||
| 511 | fun toLivenessStatements {statements, | |
| 512 | live} | |
| 513 | = let | |
| 514 | val {statements,live} | |
| 515 | = List.foldr(statements, | |
| 516 | {statements = [], live = live}, | |
| 517 | fn (asm,{statements,live}) | |
| 518 | => let | |
| 519 | val info as Liveness.T {liveIn = live, ...} | |
| 520 | = Liveness.livenessAssembly | |
| 521 | {assembly = asm, | |
| 522 | live = live} | |
| 523 | in | |
| 524 | {statements = (asm, info)::statements, | |
| 525 | live = live} | |
| 526 | end) | |
| 527 | in | |
| 528 | {statements = statements, | |
| 529 | live = live} | |
| 530 | end | |
| 531 | ||
| 532 | fun reLivenessStatements {statements: (Assembly.t * Liveness.t) list, | |
| 533 | live} | |
| 534 | = let | |
| 535 | val {statements,live,...} | |
| 536 | = List.foldr(statements, | |
| 537 | {statements = [], | |
| 538 | live = live, | |
| 539 | continue = false}, | |
| 540 | fn ((asm,info),{statements,live,continue}) | |
| 541 | => if continue | |
| 542 | then {statements = (asm,info)::statements, | |
| 543 | live = Liveness.liveIn info, | |
| 544 | continue = continue} | |
| 545 | else let | |
| 546 | val info' as Liveness.T {liveIn = live',...} | |
| 547 | = Liveness.livenessAssembly | |
| 548 | {assembly = asm, | |
| 549 | live = live} | |
| 550 | in | |
| 551 | {statements = (asm, info')::statements, | |
| 552 | live = live', | |
| 553 | continue = Liveness.eq(info,info')} | |
| 554 | end) | |
| 555 | in | |
| 556 | {statements = statements, | |
| 557 | live = live} | |
| 558 | end | |
| 559 | ||
| 560 | fun toLivenessTransfer {transfer, | |
| 561 | liveInfo} | |
| 562 | = let | |
| 563 | val info as Liveness.T {liveIn = live, ...} | |
| 564 | = Liveness.livenessTransfer {transfer = transfer, | |
| 565 | liveInfo = liveInfo} | |
| 566 | in | |
| 567 | {transfer = (transfer,info), | |
| 568 | live = live} | |
| 569 | end | |
| 570 | ||
| 571 | fun reLivenessTransfer {transfer: Transfer.t * Liveness.t} | |
| 572 | = let | |
| 573 | val (transfer, Liveness.T {liveOut,...}) = transfer | |
| 574 | val info as Liveness.T {liveIn = live, ...} | |
| 575 | = Liveness.livenessTransfer' {transfer = transfer, | |
| 576 | live = liveOut} | |
| 577 | in | |
| 578 | {transfer = (transfer, info), | |
| 579 | live = live} | |
| 580 | end | |
| 581 | ||
| 582 | fun toLivenessBlock {block = Block.T {entry, profileLabel, | |
| 583 | statements, transfer}, | |
| 584 | liveInfo : LiveInfo.t} | |
| 585 | = let | |
| 586 | val {transfer, live} | |
| 587 | = toLivenessTransfer {transfer = transfer, | |
| 588 | liveInfo = liveInfo} | |
| 589 | ||
| 590 | val {statements, live} | |
| 591 | = toLivenessStatements {statements =statements, | |
| 592 | live = live} | |
| 593 | ||
| 594 | val {entry, ...} | |
| 595 | = toLivenessEntry {entry = entry, | |
| 596 | live = live} | |
| 597 | ||
| 598 | val liveness_block | |
| 599 | = T {entry = entry, | |
| 600 | profileLabel = profileLabel, | |
| 601 | statements = statements, | |
| 602 | transfer = transfer} | |
| 603 | in | |
| 604 | liveness_block | |
| 605 | end | |
| 606 | ||
| 607 | val (toLivenessBlock: {block: Block.t, liveInfo: LiveInfo.t} -> t, | |
| 608 | toLivenessBlock_msg) | |
| 609 | = tracer | |
| 610 | "toLivenessBlock" | |
| 611 | toLivenessBlock | |
| 612 | ||
| 613 | fun verifyLivenessEntry {entry = (entry,info), | |
| 614 | live} | |
| 615 | = let | |
| 616 | val info' as Liveness.T {liveIn = live', ...} | |
| 617 | = Liveness.livenessEntry {entry = entry, | |
| 618 | live = live} | |
| 619 | in | |
| 620 | {verified = Liveness.eq(info, info'), | |
| 621 | live = live'} | |
| 622 | end | |
| 623 | ||
| 624 | fun verifyLivenessStatements {statements, | |
| 625 | live} | |
| 626 | = List.foldr(statements, | |
| 627 | {verified = true, live = live}, | |
| 628 | fn ((asm,info),{verified, live}) | |
| 629 | => let | |
| 630 | val info' as Liveness.T {liveIn = live', ...} | |
| 631 | = Liveness.livenessAssembly | |
| 632 | {assembly = asm, | |
| 633 | live = live} | |
| 634 | val eq = Liveness.eq(info, info') | |
| 635 | val () = | |
| 636 | if eq | |
| 637 | then () | |
| 638 | else (print "asm ::\n"; | |
| 639 | print (Assembly.toString asm); | |
| 640 | print "\n"; | |
| 641 | print "info ::\n"; | |
| 642 | print (Liveness.toString info); | |
| 643 | print "\n"; | |
| 644 | print "info' ::\n"; | |
| 645 | print (Liveness.toString info'); | |
| 646 | print "\n") | |
| 647 | in | |
| 648 | {verified = verified andalso | |
| 649 | Liveness.eq(info, info'), | |
| 650 | live = live'} | |
| 651 | end) | |
| 652 | ||
| 653 | fun verifyLivenessTransfer {transfer = (transfer,info), | |
| 654 | liveInfo} | |
| 655 | = let | |
| 656 | val info' as Liveness.T {liveIn = live', ...} | |
| 657 | = Liveness.livenessTransfer {transfer = transfer, | |
| 658 | liveInfo = liveInfo} | |
| 659 | in | |
| 660 | {verified = Liveness.eq(info, info'), | |
| 661 | live = live'} | |
| 662 | end | |
| 663 | ||
| 664 | fun verifyLivenessBlock {block = T {entry, statements, transfer, ...}, | |
| 665 | liveInfo: LiveInfo.t} | |
| 666 | = let | |
| 667 | val {verified = verified_transfer, | |
| 668 | live} | |
| 669 | = verifyLivenessTransfer {transfer = transfer, | |
| 670 | liveInfo = liveInfo} | |
| 671 | ||
| 672 | val {verified = verified_statements, | |
| 673 | live} | |
| 674 | = verifyLivenessStatements {statements =statements, | |
| 675 | live = live} | |
| 676 | ||
| 677 | val {verified = verified_entry, | |
| 678 | ...} | |
| 679 | = verifyLivenessEntry {entry = entry, | |
| 680 | live = live} | |
| 681 | ||
| 682 | (* FIXME -- the live-in set changed because of dead code elimination. | |
| 683 | val live' = get label | |
| 684 | ||
| 685 | val verified_live = List.equalsAsSet(live, live', MemLoc.eq) | |
| 686 | *) | |
| 687 | val verified_live = true | |
| 688 | in | |
| 689 | verified_transfer andalso | |
| 690 | verified_statements andalso | |
| 691 | verified_entry andalso | |
| 692 | verified_live | |
| 693 | end | |
| 694 | ||
| 695 | val (verifyLivenessBlock: {block: t, liveInfo: LiveInfo.t} -> bool, | |
| 696 | verifyLivenessBlock_msg) | |
| 697 | = tracer | |
| 698 | "verifyLivenessBlock" | |
| 699 | verifyLivenessBlock | |
| 700 | ||
| 701 | fun toBlock {block = T {entry, profileLabel, | |
| 702 | statements, transfer}} | |
| 703 | = let | |
| 704 | val (entry,_) = entry | |
| 705 | val statements = List.map(statements, fn (asm,_) => asm) | |
| 706 | val (transfer,_) = transfer | |
| 707 | in | |
| 708 | Block.T {entry = entry, | |
| 709 | profileLabel = profileLabel, | |
| 710 | statements = statements, | |
| 711 | transfer = transfer} | |
| 712 | end | |
| 713 | ||
| 714 | val (toBlock: {block: t} -> Block.t, | |
| 715 | toBlock_msg) | |
| 716 | = tracer | |
| 717 | "toBlock" | |
| 718 | toBlock | |
| 719 | end | |
| 720 | ||
| 721 | end |