1 // Copyright 2016 The Go Authors. All rights reserved. 2 // Use of this source code is governed by a BSD-style 3 // license that can be found in the LICENSE file. 4 5 package ssa 6 7 import ( 8 "fmt" 9 "math" 10 ) 11 12 type branch int 13 14 const ( 15 unknown branch = iota 16 positive 17 negative 18 ) 19 20 // relation represents the set of possible relations between 21 // pairs of variables (v, w). Without a priori knowledge the 22 // mask is lt | eq | gt meaning v can be less than, equal to or 23 // greater than w. When the execution path branches on the condition 24 // `v op w` the set of relations is updated to exclude any 25 // relation not possible due to `v op w` being true (or false). 26 // 27 // E.g. 28 // 29 // r := relation(...) 30 // 31 // if v < w { 32 // newR := r & lt 33 // } 34 // if v >= w { 35 // newR := r & (eq|gt) 36 // } 37 // if v != w { 38 // newR := r & (lt|gt) 39 // } 40 type relation uint 41 42 const ( 43 lt relation = 1 << iota 44 eq 45 gt 46 ) 47 48 var relationStrings = [...]string{ 49 0: "none", lt: "<", eq: "==", lt | eq: "<=", 50 gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any", 51 } 52 53 func (r relation) String() string { 54 if r < relation(len(relationStrings)) { 55 return relationStrings[r] 56 } 57 return fmt.Sprintf("relation(%d)", uint(r)) 58 } 59 60 // domain represents the domain of a variable pair in which a set 61 // of relations is known. For example, relations learned for unsigned 62 // pairs cannot be transferred to signed pairs because the same bit 63 // representation can mean something else. 64 type domain uint 65 66 const ( 67 signed domain = 1 << iota 68 unsigned 69 pointer 70 boolean 71 ) 72 73 var domainStrings = [...]string{ 74 "signed", "unsigned", "pointer", "boolean", 75 } 76 77 func (d domain) String() string { 78 s := "" 79 for i, ds := range domainStrings { 80 if d&(1<<uint(i)) != 0 { 81 if len(s) != 0 { 82 s += "|" 83 } 84 s += ds 85 d &^= 1 << uint(i) 86 } 87 } 88 if d != 0 { 89 if len(s) != 0 { 90 s += "|" 91 } 92 s += fmt.Sprintf("0x%x", uint(d)) 93 } 94 return s 95 } 96 97 type pair struct { 98 v, w *Value // a pair of values, ordered by ID. 99 // v can be nil, to mean the zero value. 100 // for booleans the zero value (v == nil) is false. 101 d domain 102 } 103 104 // fact is a pair plus a relation for that pair. 105 type fact struct { 106 p pair 107 r relation 108 } 109 110 // a limit records known upper and lower bounds for a value. 111 type limit struct { 112 min, max int64 // min <= value <= max, signed 113 umin, umax uint64 // umin <= value <= umax, unsigned 114 } 115 116 func (l limit) String() string { 117 return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax) 118 } 119 120 func (l limit) intersect(l2 limit) limit { 121 if l.min < l2.min { 122 l.min = l2.min 123 } 124 if l.umin < l2.umin { 125 l.umin = l2.umin 126 } 127 if l.max > l2.max { 128 l.max = l2.max 129 } 130 if l.umax > l2.umax { 131 l.umax = l2.umax 132 } 133 return l 134 } 135 136 var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64} 137 138 // a limitFact is a limit known for a particular value. 139 type limitFact struct { 140 vid ID 141 limit limit 142 } 143 144 // factsTable keeps track of relations between pairs of values. 145 // 146 // The fact table logic is sound, but incomplete. Outside of a few 147 // special cases, it performs no deduction or arithmetic. While there 148 // are known decision procedures for this, the ad hoc approach taken 149 // by the facts table is effective for real code while remaining very 150 // efficient. 151 type factsTable struct { 152 // unsat is true if facts contains a contradiction. 153 // 154 // Note that the factsTable logic is incomplete, so if unsat 155 // is false, the assertions in factsTable could be satisfiable 156 // *or* unsatisfiable. 157 unsat bool // true if facts contains a contradiction 158 unsatDepth int // number of unsat checkpoints 159 160 facts map[pair]relation // current known set of relation 161 stack []fact // previous sets of relations 162 163 // order is a couple of partial order sets that record information 164 // about relations between SSA values in the signed and unsigned 165 // domain. 166 order [2]*poset 167 168 // known lower and upper bounds on individual values. 169 limits map[ID]limit 170 limitStack []limitFact // previous entries 171 172 // For each slice s, a map from s to a len(s)/cap(s) value (if any) 173 // TODO: check if there are cases that matter where we have 174 // more than one len(s) for a slice. We could keep a list if necessary. 175 lens map[ID]*Value 176 caps map[ID]*Value 177 178 // zero is a zero-valued constant 179 zero *Value 180 } 181 182 // checkpointFact is an invalid value used for checkpointing 183 // and restoring factsTable. 184 var checkpointFact = fact{} 185 var checkpointBound = limitFact{} 186 187 func newFactsTable(f *Func) *factsTable { 188 ft := &factsTable{} 189 ft.order[0] = f.newPoset() // signed 190 ft.order[1] = f.newPoset() // unsigned 191 ft.order[0].SetUnsigned(false) 192 ft.order[1].SetUnsigned(true) 193 ft.facts = make(map[pair]relation) 194 ft.stack = make([]fact, 4) 195 ft.limits = make(map[ID]limit) 196 ft.limitStack = make([]limitFact, 4) 197 ft.zero = f.ConstInt64(f.Config.Types.Int64, 0) 198 return ft 199 } 200 201 // update updates the set of relations between v and w in domain d 202 // restricting it to r. 203 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) { 204 if parent.Func.pass.debug > 2 { 205 parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r) 206 } 207 // No need to do anything else if we already found unsat. 208 if ft.unsat { 209 return 210 } 211 212 // Self-fact. It's wasteful to register it into the facts 213 // table, so just note whether it's satisfiable 214 if v == w { 215 if r&eq == 0 { 216 ft.unsat = true 217 } 218 return 219 } 220 221 if d == signed || d == unsigned { 222 var ok bool 223 idx := 0 224 if d == unsigned { 225 idx = 1 226 } 227 switch r { 228 case lt: 229 ok = ft.order[idx].SetOrder(v, w) 230 case gt: 231 ok = ft.order[idx].SetOrder(w, v) 232 case lt | eq: 233 ok = ft.order[idx].SetOrderOrEqual(v, w) 234 case gt | eq: 235 ok = ft.order[idx].SetOrderOrEqual(w, v) 236 case eq: 237 ok = ft.order[idx].SetEqual(v, w) 238 case lt | gt: 239 ok = ft.order[idx].SetNonEqual(v, w) 240 default: 241 panic("unknown relation") 242 } 243 if !ok { 244 if parent.Func.pass.debug > 2 { 245 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r) 246 } 247 ft.unsat = true 248 return 249 } 250 } else { 251 if lessByID(w, v) { 252 v, w = w, v 253 r = reverseBits[r] 254 } 255 256 p := pair{v, w, d} 257 oldR, ok := ft.facts[p] 258 if !ok { 259 if v == w { 260 oldR = eq 261 } else { 262 oldR = lt | eq | gt 263 } 264 } 265 // No changes compared to information already in facts table. 266 if oldR == r { 267 return 268 } 269 ft.stack = append(ft.stack, fact{p, oldR}) 270 ft.facts[p] = oldR & r 271 // If this relation is not satisfiable, mark it and exit right away 272 if oldR&r == 0 { 273 if parent.Func.pass.debug > 2 { 274 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r) 275 } 276 ft.unsat = true 277 return 278 } 279 } 280 281 // Extract bounds when comparing against constants 282 if v.isGenericIntConst() { 283 v, w = w, v 284 r = reverseBits[r] 285 } 286 if v != nil && w.isGenericIntConst() { 287 // Note: all the +1/-1 below could overflow/underflow. Either will 288 // still generate correct results, it will just lead to imprecision. 289 // In fact if there is overflow/underflow, the corresponding 290 // code is unreachable because the known range is outside the range 291 // of the value's type. 292 old, ok := ft.limits[v.ID] 293 if !ok { 294 old = noLimit 295 if v.isGenericIntConst() { 296 switch d { 297 case signed: 298 old.min, old.max = v.AuxInt, v.AuxInt 299 if v.AuxInt >= 0 { 300 old.umin, old.umax = uint64(v.AuxInt), uint64(v.AuxInt) 301 } 302 case unsigned: 303 old.umin = v.AuxUnsigned() 304 old.umax = old.umin 305 if int64(old.umin) >= 0 { 306 old.min, old.max = int64(old.umin), int64(old.umin) 307 } 308 } 309 } 310 } 311 lim := noLimit 312 switch d { 313 case signed: 314 c := w.AuxInt 315 switch r { 316 case lt: 317 lim.max = c - 1 318 case lt | eq: 319 lim.max = c 320 case gt | eq: 321 lim.min = c 322 case gt: 323 lim.min = c + 1 324 case lt | gt: 325 lim = old 326 if c == lim.min { 327 lim.min++ 328 } 329 if c == lim.max { 330 lim.max-- 331 } 332 case eq: 333 lim.min = c 334 lim.max = c 335 } 336 if lim.min >= 0 { 337 // int(x) >= 0 && int(x) >= N ⇒ uint(x) >= N 338 lim.umin = uint64(lim.min) 339 } 340 if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 { 341 // 0 <= int(x) <= N ⇒ 0 <= uint(x) <= N 342 // This is for a max update, so the lower bound 343 // comes from what we already know (old). 344 lim.umax = uint64(lim.max) 345 } 346 case unsigned: 347 uc := w.AuxUnsigned() 348 switch r { 349 case lt: 350 lim.umax = uc - 1 351 case lt | eq: 352 lim.umax = uc 353 case gt | eq: 354 lim.umin = uc 355 case gt: 356 lim.umin = uc + 1 357 case lt | gt: 358 lim = old 359 if uc == lim.umin { 360 lim.umin++ 361 } 362 if uc == lim.umax { 363 lim.umax-- 364 } 365 case eq: 366 lim.umin = uc 367 lim.umax = uc 368 } 369 // We could use the contrapositives of the 370 // signed implications to derive signed facts, 371 // but it turns out not to matter. 372 } 373 ft.limitStack = append(ft.limitStack, limitFact{v.ID, old}) 374 lim = old.intersect(lim) 375 ft.limits[v.ID] = lim 376 if v.Block.Func.pass.debug > 2 { 377 v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String()) 378 } 379 if lim.min > lim.max || lim.umin > lim.umax { 380 ft.unsat = true 381 return 382 } 383 } 384 385 // Derived facts below here are only about numbers. 386 if d != signed && d != unsigned { 387 return 388 } 389 390 // Additional facts we know given the relationship between len and cap. 391 // 392 // TODO: Since prove now derives transitive relations, it 393 // should be sufficient to learn that len(w) <= cap(w) at the 394 // beginning of prove where we look for all len/cap ops. 395 if v.Op == OpSliceLen && r< == 0 && ft.caps[v.Args[0].ID] != nil { 396 // len(s) > w implies cap(s) > w 397 // len(s) >= w implies cap(s) >= w 398 // len(s) == w implies cap(s) >= w 399 ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt) 400 } 401 if w.Op == OpSliceLen && r> == 0 && ft.caps[w.Args[0].ID] != nil { 402 // same, length on the RHS. 403 ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt) 404 } 405 if v.Op == OpSliceCap && r> == 0 && ft.lens[v.Args[0].ID] != nil { 406 // cap(s) < w implies len(s) < w 407 // cap(s) <= w implies len(s) <= w 408 // cap(s) == w implies len(s) <= w 409 ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt) 410 } 411 if w.Op == OpSliceCap && r< == 0 && ft.lens[w.Args[0].ID] != nil { 412 // same, capacity on the RHS. 413 ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt) 414 } 415 416 // Process fence-post implications. 417 // 418 // First, make the condition > or >=. 419 if r == lt || r == lt|eq { 420 v, w = w, v 421 r = reverseBits[r] 422 } 423 switch r { 424 case gt: 425 if x, delta := isConstDelta(v); x != nil && delta == 1 { 426 // x+1 > w ⇒ x >= w 427 // 428 // This is useful for eliminating the 429 // growslice branch of append. 430 ft.update(parent, x, w, d, gt|eq) 431 } else if x, delta := isConstDelta(w); x != nil && delta == -1 { 432 // v > x-1 ⇒ v >= x 433 ft.update(parent, v, x, d, gt|eq) 434 } 435 case gt | eq: 436 if x, delta := isConstDelta(v); x != nil && delta == -1 { 437 // x-1 >= w && x > min ⇒ x > w 438 // 439 // Useful for i > 0; s[i-1]. 440 lim, ok := ft.limits[x.ID] 441 if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) { 442 ft.update(parent, x, w, d, gt) 443 } 444 } else if x, delta := isConstDelta(w); x != nil && delta == 1 { 445 // v >= x+1 && x < max ⇒ v > x 446 lim, ok := ft.limits[x.ID] 447 if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) { 448 ft.update(parent, v, x, d, gt) 449 } 450 } 451 } 452 453 // Process: x+delta > w (with delta constant) 454 // Only signed domain for now (useful for accesses to slices in loops). 455 if r == gt || r == gt|eq { 456 if x, delta := isConstDelta(v); x != nil && d == signed { 457 if parent.Func.pass.debug > 1 { 458 parent.Func.Warnl(parent.Pos, "x+d %s w; x:%v %v delta:%v w:%v d:%v", r, x, parent.String(), delta, w.AuxInt, d) 459 } 460 if !w.isGenericIntConst() { 461 // If we know that x+delta > w but w is not constant, we can derive: 462 // if delta < 0 and x > MinInt - delta, then x > w (because x+delta cannot underflow) 463 // This is useful for loops with bounds "len(slice)-K" (delta = -K) 464 if l, has := ft.limits[x.ID]; has && delta < 0 { 465 if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) || 466 (x.Type.Size() == 4 && l.min >= math.MinInt32-delta) { 467 ft.update(parent, x, w, signed, r) 468 } 469 } 470 } else { 471 // With w,delta constants, we want to derive: x+delta > w ⇒ x > w-delta 472 // 473 // We compute (using integers of the correct size): 474 // min = w - delta 475 // max = MaxInt - delta 476 // 477 // And we prove that: 478 // if min<max: min < x AND x <= max 479 // if min>max: min < x OR x <= max 480 // 481 // This is always correct, even in case of overflow. 482 // 483 // If the initial fact is x+delta >= w instead, the derived conditions are: 484 // if min<max: min <= x AND x <= max 485 // if min>max: min <= x OR x <= max 486 // 487 // Notice the conditions for max are still <=, as they handle overflows. 488 var min, max int64 489 var vmin, vmax *Value 490 switch x.Type.Size() { 491 case 8: 492 min = w.AuxInt - delta 493 max = int64(^uint64(0)>>1) - delta 494 495 vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min) 496 vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max) 497 498 case 4: 499 min = int64(int32(w.AuxInt) - int32(delta)) 500 max = int64(int32(^uint32(0)>>1) - int32(delta)) 501 502 vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min) 503 vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max) 504 505 default: 506 panic("unimplemented") 507 } 508 509 if min < max { 510 // Record that x > min and max >= x 511 ft.update(parent, x, vmin, d, r) 512 ft.update(parent, vmax, x, d, r|eq) 513 } else { 514 // We know that either x>min OR x<=max. factsTable cannot record OR conditions, 515 // so let's see if we can already prove that one of them is false, in which case 516 // the other must be true 517 if l, has := ft.limits[x.ID]; has { 518 if l.max <= min { 519 if r&eq == 0 || l.max < min { 520 // x>min (x>=min) is impossible, so it must be x<=max 521 ft.update(parent, vmax, x, d, r|eq) 522 } 523 } else if l.min > max { 524 // x<=max is impossible, so it must be x>min 525 ft.update(parent, x, vmin, d, r) 526 } 527 } 528 } 529 } 530 } 531 } 532 533 } 534 535 var opMin = map[Op]int64{ 536 OpAdd64: math.MinInt64, OpSub64: math.MinInt64, 537 OpAdd32: math.MinInt32, OpSub32: math.MinInt32, 538 } 539 540 var opMax = map[Op]int64{ 541 OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64, 542 OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32, 543 } 544 545 var opUMax = map[Op]uint64{ 546 OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64, 547 OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32, 548 } 549 550 // isNonNegative reports whether v is known to be non-negative. 551 func (ft *factsTable) isNonNegative(v *Value) bool { 552 if isNonNegative(v) { 553 return true 554 } 555 556 var max int64 557 switch v.Type.Size() { 558 case 1: 559 max = math.MaxInt8 560 case 2: 561 max = math.MaxInt16 562 case 4: 563 max = math.MaxInt32 564 case 8: 565 max = math.MaxInt64 566 default: 567 panic("unexpected integer size") 568 } 569 570 // Check if the recorded limits can prove that the value is positive 571 if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= uint64(max)) { 572 return true 573 } 574 575 // Check if v = x+delta, and we can use x's limits to prove that it's positive 576 if x, delta := isConstDelta(v); x != nil { 577 if l, has := ft.limits[x.ID]; has { 578 if delta > 0 && l.min >= -delta && l.max <= max-delta { 579 return true 580 } 581 if delta < 0 && l.min >= -delta { 582 return true 583 } 584 } 585 } 586 587 // Check if the signed poset can prove that the value is >= 0 588 return ft.order[0].OrderedOrEqual(ft.zero, v) 589 } 590 591 // checkpoint saves the current state of known relations. 592 // Called when descending on a branch. 593 func (ft *factsTable) checkpoint() { 594 if ft.unsat { 595 ft.unsatDepth++ 596 } 597 ft.stack = append(ft.stack, checkpointFact) 598 ft.limitStack = append(ft.limitStack, checkpointBound) 599 ft.order[0].Checkpoint() 600 ft.order[1].Checkpoint() 601 } 602 603 // restore restores known relation to the state just 604 // before the previous checkpoint. 605 // Called when backing up on a branch. 606 func (ft *factsTable) restore() { 607 if ft.unsatDepth > 0 { 608 ft.unsatDepth-- 609 } else { 610 ft.unsat = false 611 } 612 for { 613 old := ft.stack[len(ft.stack)-1] 614 ft.stack = ft.stack[:len(ft.stack)-1] 615 if old == checkpointFact { 616 break 617 } 618 if old.r == lt|eq|gt { 619 delete(ft.facts, old.p) 620 } else { 621 ft.facts[old.p] = old.r 622 } 623 } 624 for { 625 old := ft.limitStack[len(ft.limitStack)-1] 626 ft.limitStack = ft.limitStack[:len(ft.limitStack)-1] 627 if old.vid == 0 { // checkpointBound 628 break 629 } 630 if old.limit == noLimit { 631 delete(ft.limits, old.vid) 632 } else { 633 ft.limits[old.vid] = old.limit 634 } 635 } 636 ft.order[0].Undo() 637 ft.order[1].Undo() 638 } 639 640 func lessByID(v, w *Value) bool { 641 if v == nil && w == nil { 642 // Should not happen, but just in case. 643 return false 644 } 645 if v == nil { 646 return true 647 } 648 return w != nil && v.ID < w.ID 649 } 650 651 var ( 652 reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7} 653 654 // maps what we learn when the positive branch is taken. 655 // For example: 656 // OpLess8: {signed, lt}, 657 // v1 = (OpLess8 v2 v3). 658 // If v1 branch is taken then we learn that the rangeMask 659 // can be at most lt. 660 domainRelationTable = map[Op]struct { 661 d domain 662 r relation 663 }{ 664 OpEq8: {signed | unsigned, eq}, 665 OpEq16: {signed | unsigned, eq}, 666 OpEq32: {signed | unsigned, eq}, 667 OpEq64: {signed | unsigned, eq}, 668 OpEqPtr: {pointer, eq}, 669 670 OpNeq8: {signed | unsigned, lt | gt}, 671 OpNeq16: {signed | unsigned, lt | gt}, 672 OpNeq32: {signed | unsigned, lt | gt}, 673 OpNeq64: {signed | unsigned, lt | gt}, 674 OpNeqPtr: {pointer, lt | gt}, 675 676 OpLess8: {signed, lt}, 677 OpLess8U: {unsigned, lt}, 678 OpLess16: {signed, lt}, 679 OpLess16U: {unsigned, lt}, 680 OpLess32: {signed, lt}, 681 OpLess32U: {unsigned, lt}, 682 OpLess64: {signed, lt}, 683 OpLess64U: {unsigned, lt}, 684 685 OpLeq8: {signed, lt | eq}, 686 OpLeq8U: {unsigned, lt | eq}, 687 OpLeq16: {signed, lt | eq}, 688 OpLeq16U: {unsigned, lt | eq}, 689 OpLeq32: {signed, lt | eq}, 690 OpLeq32U: {unsigned, lt | eq}, 691 OpLeq64: {signed, lt | eq}, 692 OpLeq64U: {unsigned, lt | eq}, 693 694 OpGeq8: {signed, eq | gt}, 695 OpGeq8U: {unsigned, eq | gt}, 696 OpGeq16: {signed, eq | gt}, 697 OpGeq16U: {unsigned, eq | gt}, 698 OpGeq32: {signed, eq | gt}, 699 OpGeq32U: {unsigned, eq | gt}, 700 OpGeq64: {signed, eq | gt}, 701 OpGeq64U: {unsigned, eq | gt}, 702 703 OpGreater8: {signed, gt}, 704 OpGreater8U: {unsigned, gt}, 705 OpGreater16: {signed, gt}, 706 OpGreater16U: {unsigned, gt}, 707 OpGreater32: {signed, gt}, 708 OpGreater32U: {unsigned, gt}, 709 OpGreater64: {signed, gt}, 710 OpGreater64U: {unsigned, gt}, 711 712 // For these ops, the negative branch is different: we can only 713 // prove signed/GE (signed/GT) if we can prove that arg0 is non-negative. 714 // See the special case in addBranchRestrictions. 715 OpIsInBounds: {signed | unsigned, lt}, // 0 <= arg0 < arg1 716 OpIsSliceInBounds: {signed | unsigned, lt | eq}, // 0 <= arg0 <= arg1 717 } 718 ) 719 720 // prove removes redundant BlockIf branches that can be inferred 721 // from previous dominating comparisons. 722 // 723 // By far, the most common redundant pair are generated by bounds checking. 724 // For example for the code: 725 // 726 // a[i] = 4 727 // foo(a[i]) 728 // 729 // The compiler will generate the following code: 730 // 731 // if i >= len(a) { 732 // panic("not in bounds") 733 // } 734 // a[i] = 4 735 // if i >= len(a) { 736 // panic("not in bounds") 737 // } 738 // foo(a[i]) 739 // 740 // The second comparison i >= len(a) is clearly redundant because if the 741 // else branch of the first comparison is executed, we already know that i < len(a). 742 // The code for the second panic can be removed. 743 // 744 // prove works by finding contradictions and trimming branches whose 745 // conditions are unsatisfiable given the branches leading up to them. 746 // It tracks a "fact table" of branch conditions. For each branching 747 // block, it asserts the branch conditions that uniquely dominate that 748 // block, and then separately asserts the block's branch condition and 749 // its negation. If either leads to a contradiction, it can trim that 750 // successor. 751 func prove(f *Func) { 752 ft := newFactsTable(f) 753 ft.checkpoint() 754 755 // Find length and capacity ops. 756 for _, b := range f.Blocks { 757 for _, v := range b.Values { 758 if v.Uses == 0 { 759 // We don't care about dead values. 760 // (There can be some that are CSEd but not removed yet.) 761 continue 762 } 763 switch v.Op { 764 case OpStringLen: 765 ft.update(b, v, ft.zero, signed, gt|eq) 766 case OpSliceLen: 767 if ft.lens == nil { 768 ft.lens = map[ID]*Value{} 769 } 770 ft.lens[v.Args[0].ID] = v 771 ft.update(b, v, ft.zero, signed, gt|eq) 772 case OpSliceCap: 773 if ft.caps == nil { 774 ft.caps = map[ID]*Value{} 775 } 776 ft.caps[v.Args[0].ID] = v 777 ft.update(b, v, ft.zero, signed, gt|eq) 778 } 779 } 780 } 781 782 // Find induction variables. Currently, findIndVars 783 // is limited to one induction variable per block. 784 var indVars map[*Block]indVar 785 for _, v := range findIndVar(f) { 786 if indVars == nil { 787 indVars = make(map[*Block]indVar) 788 } 789 indVars[v.entry] = v 790 } 791 792 // current node state 793 type walkState int 794 const ( 795 descend walkState = iota 796 simplify 797 ) 798 // work maintains the DFS stack. 799 type bp struct { 800 block *Block // current handled block 801 state walkState // what's to do 802 } 803 work := make([]bp, 0, 256) 804 work = append(work, bp{ 805 block: f.Entry, 806 state: descend, 807 }) 808 809 idom := f.Idom() 810 sdom := f.sdom() 811 812 // DFS on the dominator tree. 813 // 814 // For efficiency, we consider only the dominator tree rather 815 // than the entire flow graph. On the way down, we consider 816 // incoming branches and accumulate conditions that uniquely 817 // dominate the current block. If we discover a contradiction, 818 // we can eliminate the entire block and all of its children. 819 // On the way back up, we consider outgoing branches that 820 // haven't already been considered. This way we consider each 821 // branch condition only once. 822 for len(work) > 0 { 823 node := work[len(work)-1] 824 work = work[:len(work)-1] 825 parent := idom[node.block.ID] 826 branch := getBranch(sdom, parent, node.block) 827 828 switch node.state { 829 case descend: 830 ft.checkpoint() 831 if iv, ok := indVars[node.block]; ok { 832 addIndVarRestrictions(ft, parent, iv) 833 } 834 835 if branch != unknown { 836 addBranchRestrictions(ft, parent, branch) 837 if ft.unsat { 838 // node.block is unreachable. 839 // Remove it and don't visit 840 // its children. 841 removeBranch(parent, branch) 842 ft.restore() 843 break 844 } 845 // Otherwise, we can now commit to 846 // taking this branch. We'll restore 847 // ft when we unwind. 848 } 849 850 // Add inductive facts for phis in this block. 851 addLocalInductiveFacts(ft, node.block) 852 853 work = append(work, bp{ 854 block: node.block, 855 state: simplify, 856 }) 857 for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) { 858 work = append(work, bp{ 859 block: s, 860 state: descend, 861 }) 862 } 863 864 case simplify: 865 simplifyBlock(sdom, ft, node.block) 866 ft.restore() 867 } 868 } 869 870 ft.restore() 871 872 // Return the posets to the free list 873 for _, po := range ft.order { 874 // Make sure it's empty as it should be. A non-empty poset 875 // might cause errors and miscompilations if reused. 876 if checkEnabled { 877 if err := po.CheckEmpty(); err != nil { 878 f.Fatalf("prove poset not empty after function %s: %v", f.Name, err) 879 } 880 } 881 f.retPoset(po) 882 } 883 } 884 885 // getBranch returns the range restrictions added by p 886 // when reaching b. p is the immediate dominator of b. 887 func getBranch(sdom SparseTree, p *Block, b *Block) branch { 888 if p == nil || p.Kind != BlockIf { 889 return unknown 890 } 891 // If p and p.Succs[0] are dominators it means that every path 892 // from entry to b passes through p and p.Succs[0]. We care that 893 // no path from entry to b passes through p.Succs[1]. If p.Succs[0] 894 // has one predecessor then (apart from the degenerate case), 895 // there is no path from entry that can reach b through p.Succs[1]. 896 // TODO: how about p->yes->b->yes, i.e. a loop in yes. 897 if sdom.isAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 { 898 return positive 899 } 900 if sdom.isAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 { 901 return negative 902 } 903 return unknown 904 } 905 906 // addIndVarRestrictions updates the factsTables ft with the facts 907 // learned from the induction variable indVar which drives the loop 908 // starting in Block b. 909 func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) { 910 d := signed 911 if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) { 912 d |= unsigned 913 } 914 915 if iv.flags&indVarMinExc == 0 { 916 addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq) 917 } else { 918 addRestrictions(b, ft, d, iv.min, iv.ind, lt) 919 } 920 921 if iv.flags&indVarMaxInc == 0 { 922 addRestrictions(b, ft, d, iv.ind, iv.max, lt) 923 } else { 924 addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq) 925 } 926 } 927 928 // addBranchRestrictions updates the factsTables ft with the facts learned when 929 // branching from Block b in direction br. 930 func addBranchRestrictions(ft *factsTable, b *Block, br branch) { 931 c := b.Control 932 switch br { 933 case negative: 934 addRestrictions(b, ft, boolean, nil, c, eq) 935 case positive: 936 addRestrictions(b, ft, boolean, nil, c, lt|gt) 937 default: 938 panic("unknown branch") 939 } 940 if tr, has := domainRelationTable[b.Control.Op]; has { 941 // When we branched from parent we learned a new set of 942 // restrictions. Update the factsTable accordingly. 943 d := tr.d 944 if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) { 945 d |= unsigned 946 } 947 switch b.Control.Op { 948 case OpIsInBounds, OpIsSliceInBounds: 949 // 0 <= a0 < a1 (or 0 <= a0 <= a1) 950 // 951 // On the positive branch, we learn: 952 // signed: 0 <= a0 < a1 (or 0 <= a0 <= a1) 953 // unsigned: a0 < a1 (or a0 <= a1) 954 // 955 // On the negative branch, we learn (0 > a0 || 956 // a0 >= a1). In the unsigned domain, this is 957 // simply a0 >= a1 (which is the reverse of the 958 // positive branch, so nothing surprising). 959 // But in the signed domain, we can't express the || 960 // condition, so check if a0 is non-negative instead, 961 // to be able to learn something. 962 switch br { 963 case negative: 964 d = unsigned 965 if ft.isNonNegative(c.Args[0]) { 966 d |= signed 967 } 968 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq)) 969 case positive: 970 addRestrictions(b, ft, signed, ft.zero, c.Args[0], lt|eq) 971 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r) 972 } 973 default: 974 switch br { 975 case negative: 976 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq)) 977 case positive: 978 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r) 979 } 980 } 981 982 } 983 } 984 985 // addRestrictions updates restrictions from the immediate 986 // dominating block (p) using r. 987 func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) { 988 if t == 0 { 989 // Trivial case: nothing to do. 990 // Shoult not happen, but just in case. 991 return 992 } 993 for i := domain(1); i <= t; i <<= 1 { 994 if t&i == 0 { 995 continue 996 } 997 ft.update(parent, v, w, i, r) 998 } 999 } 1000 1001 // addLocalInductiveFacts adds inductive facts when visiting b, where 1002 // b is a join point in a loop. In contrast with findIndVar, this 1003 // depends on facts established for b, which is why it happens when 1004 // visiting b. addLocalInductiveFacts specifically targets the pattern 1005 // created by OFORUNTIL, which isn't detected by findIndVar. 1006 // 1007 // TODO: It would be nice to combine this with findIndVar. 1008 func addLocalInductiveFacts(ft *factsTable, b *Block) { 1009 // This looks for a specific pattern of induction: 1010 // 1011 // 1. i1 = OpPhi(min, i2) in b 1012 // 2. i2 = i1 + 1 1013 // 3. i2 < max at exit from b.Preds[1] 1014 // 4. min < max 1015 // 1016 // If all of these conditions are true, then i1 < max and i1 >= min. 1017 1018 for _, i1 := range b.Values { 1019 if i1.Op != OpPhi { 1020 continue 1021 } 1022 1023 // Check for conditions 1 and 2. This is easy to do 1024 // and will throw out most phis. 1025 min, i2 := i1.Args[0], i1.Args[1] 1026 if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 { 1027 continue 1028 } 1029 1030 // Try to prove condition 3. We can't just query the 1031 // fact table for this because we don't know what the 1032 // facts of b.Preds[1] are (in general, b.Preds[1] is 1033 // a loop-back edge, so we haven't even been there 1034 // yet). As a conservative approximation, we look for 1035 // this condition in the predecessor chain until we 1036 // hit a join point. 1037 uniquePred := func(b *Block) *Block { 1038 if len(b.Preds) == 1 { 1039 return b.Preds[0].b 1040 } 1041 return nil 1042 } 1043 pred, child := b.Preds[1].b, b 1044 for ; pred != nil; pred = uniquePred(pred) { 1045 if pred.Kind != BlockIf { 1046 continue 1047 } 1048 1049 br := unknown 1050 if pred.Succs[0].b == child { 1051 br = positive 1052 } 1053 if pred.Succs[1].b == child { 1054 if br != unknown { 1055 continue 1056 } 1057 br = negative 1058 } 1059 1060 tr, has := domainRelationTable[pred.Control.Op] 1061 if !has { 1062 continue 1063 } 1064 r := tr.r 1065 if br == negative { 1066 // Negative branch taken to reach b. 1067 // Complement the relations. 1068 r = (lt | eq | gt) ^ r 1069 } 1070 1071 // Check for i2 < max or max > i2. 1072 var max *Value 1073 if r == lt && pred.Control.Args[0] == i2 { 1074 max = pred.Control.Args[1] 1075 } else if r == gt && pred.Control.Args[1] == i2 { 1076 max = pred.Control.Args[0] 1077 } else { 1078 continue 1079 } 1080 1081 // Check condition 4 now that we have a 1082 // candidate max. For this we can query the 1083 // fact table. We "prove" min < max by showing 1084 // that min >= max is unsat. (This may simply 1085 // compare two constants; that's fine.) 1086 ft.checkpoint() 1087 ft.update(b, min, max, tr.d, gt|eq) 1088 proved := ft.unsat 1089 ft.restore() 1090 1091 if proved { 1092 // We know that min <= i1 < max. 1093 if b.Func.pass.debug > 0 { 1094 printIndVar(b, i1, min, max, 1, 0) 1095 } 1096 ft.update(b, min, i1, tr.d, lt|eq) 1097 ft.update(b, i1, max, tr.d, lt) 1098 } 1099 } 1100 } 1101 } 1102 1103 var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero} 1104 var mostNegativeDividend = map[Op]int64{ 1105 OpDiv16: -1 << 15, 1106 OpMod16: -1 << 15, 1107 OpDiv32: -1 << 31, 1108 OpMod32: -1 << 31, 1109 OpDiv64: -1 << 63, 1110 OpMod64: -1 << 63} 1111 1112 // simplifyBlock simplifies some constant values in b and evaluates 1113 // branches to non-uniquely dominated successors of b. 1114 func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) { 1115 for _, v := range b.Values { 1116 switch v.Op { 1117 case OpSlicemask: 1118 // Replace OpSlicemask operations in b with constants where possible. 1119 x, delta := isConstDelta(v.Args[0]) 1120 if x == nil { 1121 continue 1122 } 1123 // slicemask(x + y) 1124 // if x is larger than -y (y is negative), then slicemask is -1. 1125 lim, ok := ft.limits[x.ID] 1126 if !ok { 1127 continue 1128 } 1129 if lim.umin > uint64(-delta) { 1130 if v.Args[0].Op == OpAdd64 { 1131 v.reset(OpConst64) 1132 } else { 1133 v.reset(OpConst32) 1134 } 1135 if b.Func.pass.debug > 0 { 1136 b.Func.Warnl(v.Pos, "Proved slicemask not needed") 1137 } 1138 v.AuxInt = -1 1139 } 1140 case OpCtz8, OpCtz16, OpCtz32, OpCtz64: 1141 // On some architectures, notably amd64, we can generate much better 1142 // code for CtzNN if we know that the argument is non-zero. 1143 // Capture that information here for use in arch-specific optimizations. 1144 x := v.Args[0] 1145 lim, ok := ft.limits[x.ID] 1146 if !ok { 1147 continue 1148 } 1149 if lim.umin > 0 || lim.min > 0 || lim.max < 0 { 1150 if b.Func.pass.debug > 0 { 1151 b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op) 1152 } 1153 v.Op = ctzNonZeroOp[v.Op] 1154 } 1155 1156 case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64, 1157 OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64, 1158 OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64, 1159 OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64, 1160 OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64, 1161 OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64, 1162 OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64, 1163 OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64, 1164 OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64, 1165 OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64, 1166 OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64, 1167 OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64: 1168 // Check whether, for a << b, we know that b 1169 // is strictly less than the number of bits in a. 1170 by := v.Args[1] 1171 lim, ok := ft.limits[by.ID] 1172 if !ok { 1173 continue 1174 } 1175 bits := 8 * v.Args[0].Type.Size() 1176 if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) { 1177 v.AuxInt = 1 // see shiftIsBounded 1178 if b.Func.pass.debug > 0 { 1179 b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op) 1180 } 1181 } 1182 case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64: 1183 // On amd64 and 386 fix-up code can be avoided if we know 1184 // the divisor is not -1 or the dividend > MinIntNN. 1185 divr := v.Args[1] 1186 divrLim, divrLimok := ft.limits[divr.ID] 1187 divd := v.Args[0] 1188 divdLim, divdLimok := ft.limits[divd.ID] 1189 if (divrLimok && (divrLim.max < -1 || divrLim.min > -1)) || 1190 (divdLimok && divdLim.min > mostNegativeDividend[v.Op]) { 1191 v.AuxInt = 1 // see NeedsFixUp in genericOps - v.AuxInt = 0 means we have not proved 1192 // that the divisor is not -1 and the dividend is not the most negative, 1193 // so we need to add fix-up code. 1194 if b.Func.pass.debug > 0 { 1195 b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op) 1196 } 1197 } 1198 } 1199 } 1200 1201 if b.Kind != BlockIf { 1202 return 1203 } 1204 1205 // Consider outgoing edges from this block. 1206 parent := b 1207 for i, branch := range [...]branch{positive, negative} { 1208 child := parent.Succs[i].b 1209 if getBranch(sdom, parent, child) != unknown { 1210 // For edges to uniquely dominated blocks, we 1211 // already did this when we visited the child. 1212 continue 1213 } 1214 // For edges to other blocks, this can trim a branch 1215 // even if we couldn't get rid of the child itself. 1216 ft.checkpoint() 1217 addBranchRestrictions(ft, parent, branch) 1218 unsat := ft.unsat 1219 ft.restore() 1220 if unsat { 1221 // This branch is impossible, so remove it 1222 // from the block. 1223 removeBranch(parent, branch) 1224 // No point in considering the other branch. 1225 // (It *is* possible for both to be 1226 // unsatisfiable since the fact table is 1227 // incomplete. We could turn this into a 1228 // BlockExit, but it doesn't seem worth it.) 1229 break 1230 } 1231 } 1232 } 1233 1234 func removeBranch(b *Block, branch branch) { 1235 if b.Func.pass.debug > 0 { 1236 verb := "Proved" 1237 if branch == positive { 1238 verb = "Disproved" 1239 } 1240 c := b.Control 1241 if b.Func.pass.debug > 1 { 1242 b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c) 1243 } else { 1244 b.Func.Warnl(b.Pos, "%s %s", verb, c.Op) 1245 } 1246 } 1247 b.Kind = BlockFirst 1248 b.SetControl(nil) 1249 if branch == positive { 1250 b.swapSuccessors() 1251 } 1252 } 1253 1254 // isNonNegative reports whether v is known to be greater or equal to zero. 1255 func isNonNegative(v *Value) bool { 1256 switch v.Op { 1257 case OpConst64: 1258 return v.AuxInt >= 0 1259 1260 case OpConst32: 1261 return int32(v.AuxInt) >= 0 1262 1263 case OpStringLen, OpSliceLen, OpSliceCap, 1264 OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64: 1265 return true 1266 1267 case OpRsh64Ux64: 1268 by := v.Args[1] 1269 return by.Op == OpConst64 && by.AuxInt > 0 1270 1271 case OpRsh64x64: 1272 return isNonNegative(v.Args[0]) 1273 } 1274 return false 1275 } 1276 1277 // isConstDelta returns non-nil if v is equivalent to w+delta (signed). 1278 func isConstDelta(v *Value) (w *Value, delta int64) { 1279 cop := OpConst64 1280 switch v.Op { 1281 case OpAdd32, OpSub32: 1282 cop = OpConst32 1283 } 1284 switch v.Op { 1285 case OpAdd64, OpAdd32: 1286 if v.Args[0].Op == cop { 1287 return v.Args[1], v.Args[0].AuxInt 1288 } 1289 if v.Args[1].Op == cop { 1290 return v.Args[0], v.Args[1].AuxInt 1291 } 1292 case OpSub64, OpSub32: 1293 if v.Args[1].Op == cop { 1294 aux := v.Args[1].AuxInt 1295 if aux != -aux { // Overflow; too bad 1296 return v.Args[0], -aux 1297 } 1298 } 1299 } 1300 return nil, 0 1301 } 1302
View as plain text