1// Copyright 2017 The Wuffs Authors. 2// 3// Licensed under the Apache License, Version 2.0 (the "License"); 4// you may not use this file except in compliance with the License. 5// You may obtain a copy of the License at 6// 7// https://www.apache.org/licenses/LICENSE-2.0 8// 9// Unless required by applicable law or agreed to in writing, software 10// distributed under the License is distributed on an "AS IS" BASIS, 11// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12// See the License for the specific language governing permissions and 13// limitations under the License. 14 15package check 16 17import ( 18 "errors" 19 "fmt" 20 "math/big" 21 22 "github.com/google/wuffs/lib/interval" 23 24 a "github.com/google/wuffs/lang/ast" 25 t "github.com/google/wuffs/lang/token" 26) 27 28type bounds = interval.IntRange 29 30var numShiftBounds = [...]bounds{ 31 t.IDU8: {zero, big.NewInt(7)}, 32 t.IDU16: {zero, big.NewInt(15)}, 33 t.IDU32: {zero, big.NewInt(31)}, 34 t.IDU64: {zero, big.NewInt(63)}, 35} 36 37var numTypeBounds = [...]bounds{ 38 t.IDI8: {big.NewInt(-1 << 7), big.NewInt(1<<7 - 1)}, 39 t.IDI16: {big.NewInt(-1 << 15), big.NewInt(1<<15 - 1)}, 40 t.IDI32: {big.NewInt(-1 << 31), big.NewInt(1<<31 - 1)}, 41 t.IDI64: {big.NewInt(-1 << 63), big.NewInt(1<<63 - 1)}, 42 t.IDU8: {zero, big.NewInt(0).SetUint64(1<<8 - 1)}, 43 t.IDU16: {zero, big.NewInt(0).SetUint64(1<<16 - 1)}, 44 t.IDU32: {zero, big.NewInt(0).SetUint64(1<<32 - 1)}, 45 t.IDU64: {zero, big.NewInt(0).SetUint64(1<<64 - 1)}, 46 t.IDBool: {zero, one}, 47} 48 49var ( 50 minusOne = big.NewInt(-1) 51 zero = big.NewInt(+0) 52 one = big.NewInt(+1) 53 two = big.NewInt(+2) 54 three = big.NewInt(+3) 55 four = big.NewInt(+4) 56 five = big.NewInt(+5) 57 six = big.NewInt(+6) 58 seven = big.NewInt(+7) 59 eight = big.NewInt(+8) 60 sixteen = big.NewInt(+16) 61 thirtyTwo = big.NewInt(+32) 62 sixtyFour = big.NewInt(+64) 63 oneTwentyEight = big.NewInt(+128) 64 ffff = big.NewInt(0xFFFF) 65 66 minIdeal = big.NewInt(0).Lsh(minusOne, 1000) 67 maxIdeal = big.NewInt(0).Lsh(one, 1000) 68 69 maxIntBits = big.NewInt(t.MaxIntBits) 70 71 zeroExpr = a.NewExpr(0, 0, 0, t.ID0, nil, nil, nil, nil) 72) 73 74func init() { 75 zeroExpr.SetConstValue(zero) 76 zeroExpr.SetMBounds(bounds{zero, zero}) 77 zeroExpr.SetMType(typeExprIdeal) 78} 79 80func isErrorStatus(literal t.ID, tm *t.Map) bool { 81 s := literal.Str(tm) 82 return (len(s) >= 2) && (s[0] == '"') && (s[1] == '#') 83} 84 85func btoi(b bool) *big.Int { 86 if b { 87 return one 88 } 89 return zero 90} 91 92func add1(i *big.Int) *big.Int { 93 return big.NewInt(0).Add(i, one) 94} 95 96func sub1(i *big.Int) *big.Int { 97 return big.NewInt(0).Sub(i, one) 98} 99 100func neg(i *big.Int) *big.Int { 101 return big.NewInt(0).Neg(i) 102} 103 104func min(i, j *big.Int) *big.Int { 105 if i.Cmp(j) < 0 { 106 return i 107 } 108 return j 109} 110 111func max(i, j *big.Int) *big.Int { 112 if i.Cmp(j) > 0 { 113 return i 114 } 115 return j 116} 117 118// bitMask returns (1<<nBits - 1) as a big integer. 119func bitMask(nBits int) *big.Int { 120 switch nBits { 121 case 0: 122 return zero 123 case 1: 124 return one 125 case 8: 126 return numTypeBounds[t.IDU8][1] 127 case 16: 128 return numTypeBounds[t.IDU16][1] 129 case 32: 130 return numTypeBounds[t.IDU32][1] 131 case 64: 132 return numTypeBounds[t.IDU64][1] 133 } 134 z := big.NewInt(0).Lsh(one, uint(nBits)) 135 return z.Sub(z, one) 136} 137 138func invert(tm *t.Map, n *a.Expr) (*a.Expr, error) { 139 if !n.MType().IsBool() { 140 return nil, fmt.Errorf("check: invert(%q) called on non-bool-typed expression", n.Str(tm)) 141 } 142 if cv := n.ConstValue(); cv != nil { 143 return nil, fmt.Errorf("check: invert(%q) called on constant expression", n.Str(tm)) 144 } 145 op, lhs, rhs, args := n.Operator(), n.LHS().AsExpr(), n.RHS().AsExpr(), []*a.Node(nil) 146 switch op { 147 case t.IDXUnaryNot: 148 return rhs, nil 149 case t.IDXBinaryNotEq: 150 op = t.IDXBinaryEqEq 151 case t.IDXBinaryLessThan: 152 op = t.IDXBinaryGreaterEq 153 case t.IDXBinaryLessEq: 154 op = t.IDXBinaryGreaterThan 155 case t.IDXBinaryEqEq: 156 op = t.IDXBinaryNotEq 157 case t.IDXBinaryGreaterEq: 158 op = t.IDXBinaryLessThan 159 case t.IDXBinaryGreaterThan: 160 op = t.IDXBinaryLessEq 161 case t.IDXBinaryAnd, t.IDXBinaryOr: 162 var err error 163 lhs, err = invert(tm, lhs) 164 if err != nil { 165 return nil, err 166 } 167 rhs, err = invert(tm, rhs) 168 if err != nil { 169 return nil, err 170 } 171 if op == t.IDXBinaryAnd { 172 op = t.IDXBinaryOr 173 } else { 174 op = t.IDXBinaryAnd 175 } 176 case t.IDXAssociativeAnd, t.IDXAssociativeOr: 177 args = make([]*a.Node, 0, len(n.Args())) 178 for _, a := range n.Args() { 179 v, err := invert(tm, a.AsExpr()) 180 if err != nil { 181 return nil, err 182 } 183 args = append(args, v.AsNode()) 184 } 185 if op == t.IDXAssociativeAnd { 186 op = t.IDXAssociativeOr 187 } else { 188 op = t.IDXAssociativeAnd 189 } 190 default: 191 op, lhs, rhs = t.IDXUnaryNot, nil, n 192 } 193 o := a.NewExpr(n.AsNode().AsRaw().Flags(), op, 0, 0, lhs.AsNode(), nil, rhs.AsNode(), args) 194 o.SetMType(n.MType()) 195 return o, nil 196} 197 198func (q *checker) bcheckBlock(block []*a.Node) error { 199 // TODO: after a "break loop", do we need to set placeholder MBounds so 200 // that everything (including unreachable code) is bounds checked? 201loop: 202 for _, o := range block { 203 if err := q.bcheckStatement(o); err != nil { 204 return err 205 } 206 switch o.Kind() { 207 case a.KJump: 208 break loop 209 case a.KRet: 210 if o.AsRet().Keyword() == t.IDReturn { 211 break loop 212 } 213 // o is a yield statement. 214 // 215 // Drop any facts involving args or this. 216 if err := q.facts.update(func(x *a.Expr) (*a.Expr, error) { 217 if x.Mentions(exprArgs) || x.Mentions(exprThis) { 218 return nil, nil 219 } 220 return x, nil 221 }); err != nil { 222 return err 223 } 224 // TODO: drop any facts involving ptr-typed local variables? 225 } 226 } 227 return nil 228} 229 230func (q *checker) bcheckStatement(n *a.Node) error { 231 q.errFilename, q.errLine = n.AsRaw().FilenameLine() 232 233 switch n.Kind() { 234 case a.KAssert: 235 if err := q.bcheckAssert(n.AsAssert()); err != nil { 236 return err 237 } 238 239 case a.KAssign: 240 n := n.AsAssign() 241 if err := q.bcheckAssignment(n.LHS(), n.Operator(), n.RHS()); err != nil { 242 return err 243 } 244 245 case a.KIOBind: 246 n := n.AsIOBind() 247 if _, err := q.bcheckExpr(n.IO(), 0); err != nil { 248 return err 249 } 250 if _, err := q.bcheckExpr(n.Arg1(), 0); err != nil { 251 return err 252 } 253 if err := q.bcheckBlock(n.Body()); err != nil { 254 return err 255 } 256 // TODO: invalidate any facts regarding the io_bind expressions. 257 258 case a.KIf: 259 if err := q.bcheckIf(n.AsIf()); err != nil { 260 return err 261 } 262 263 case a.KIterate: 264 n := n.AsIterate() 265 for _, o := range n.Assigns() { 266 o := o.AsAssign() 267 if err := q.bcheckAssignment(o.LHS(), o.Operator(), o.RHS()); err != nil { 268 return err 269 } 270 } 271 // TODO: this isn't right, as the body is a loop, not an 272 // execute-exactly-once block. We should have pre / inv / post 273 // conditions, a la bcheckWhile. 274 275 assigns := n.Assigns() 276 for ; n != nil; n = n.ElseIterate() { 277 q.facts = q.facts[:0] 278 for _, o := range assigns { 279 lhs := o.AsAssign().LHS() 280 q.facts = append(q.facts, makeSliceLengthEqEq(lhs.Ident(), lhs.MType(), n.Length())) 281 } 282 if err := q.bcheckBlock(n.Body()); err != nil { 283 return err 284 } 285 } 286 287 q.facts = q.facts[:0] 288 289 case a.KJump: 290 n := n.AsJump() 291 skip := t.IDPost 292 if n.Keyword() == t.IDBreak { 293 skip = t.IDPre 294 } 295 for _, o := range n.JumpTarget().Asserts() { 296 if o.AsAssert().Keyword() == skip { 297 continue 298 } 299 if err := q.bcheckAssert(o.AsAssert()); err != nil { 300 return err 301 } 302 } 303 q.facts = q.facts[:0] 304 305 case a.KRet: 306 n := n.AsRet() 307 lTyp := q.astFunc.Out() 308 if q.astFunc.Effect().Coroutine() { 309 lTyp = typeExprStatus 310 } else if lTyp == nil { 311 lTyp = typeExprEmptyStruct 312 } 313 if _, err := q.bcheckAssignment1(nil, lTyp, t.IDEq, n.Value()); err != nil { 314 return err 315 } 316 317 if lTyp.IsStatus() { 318 if v := n.Value(); v.Operator() == 0 { 319 if id := v.Ident(); (id != t.IDOk) && (q.hasIsErrorFact(id) || isErrorStatus(id, q.tm)) { 320 n.SetRetsError() 321 } 322 } 323 } 324 325 case a.KVar: 326 if err := q.bcheckVar(n.AsVar()); err != nil { 327 return err 328 } 329 330 case a.KWhile: 331 if err := q.bcheckWhile(n.AsWhile()); err != nil { 332 return err 333 } 334 335 default: 336 return fmt.Errorf("check: unrecognized ast.Kind (%s) for bcheckStatement", n.Kind()) 337 } 338 return nil 339} 340 341func (q *checker) hasIsErrorFact(id t.ID) bool { 342 for _, x := range q.facts { 343 if (x.Operator() != t.IDOpenParen) || (len(x.Args()) != 0) { 344 continue 345 } 346 x = x.LHS().AsExpr() 347 if (x.Operator() != t.IDDot) || (x.Ident() != t.IDIsError) { 348 continue 349 } 350 x = x.LHS().AsExpr() 351 if (x.Operator() != 0) || (x.Ident() != id) { 352 continue 353 } 354 return true 355 } 356 return false 357} 358 359func (q *checker) bcheckAssert(n *a.Assert) error { 360 condition := n.Condition() 361 if _, err := q.bcheckExpr(condition, 0); err != nil { 362 return err 363 } 364 for _, o := range n.Args() { 365 if _, err := q.bcheckExpr(o.AsArg().Value(), 0); err != nil { 366 return err 367 } 368 } 369 370 for _, x := range q.facts { 371 if x.Eq(condition) { 372 return nil 373 } 374 } 375 err := errFailed 376 377 if cv := condition.ConstValue(); cv != nil { 378 if cv.Cmp(one) == 0 { 379 err = nil 380 } 381 } else if reasonID := n.Reason(); reasonID != 0 { 382 if reasonFunc := q.reasonMap[reasonID]; reasonFunc != nil { 383 err = reasonFunc(q, n) 384 } else { 385 err = fmt.Errorf("no such reason %s", reasonID.Str(q.tm)) 386 } 387 } else if condition.Operator().IsBinaryOp() && condition.Operator() != t.IDAs { 388 err = q.proveBinaryOp(condition.Operator(), 389 condition.LHS().AsExpr(), condition.RHS().AsExpr()) 390 } 391 392 if err != nil { 393 if err == errFailed { 394 return fmt.Errorf("check: cannot prove %q", condition.Str(q.tm)) 395 } 396 return fmt.Errorf("check: cannot prove %q: %v", condition.Str(q.tm), err) 397 } 398 o, err := simplify(q.tm, condition) 399 if err != nil { 400 return err 401 } 402 q.facts.appendFact(o) 403 return nil 404} 405 406func (q *checker) bcheckAssignment(lhs *a.Expr, op t.ID, rhs *a.Expr) error { 407 lTyp := (*a.TypeExpr)(nil) 408 if lhs != nil { 409 if _, err := q.bcheckExpr(lhs, 0); err != nil { 410 return err 411 } 412 lTyp = lhs.MType() 413 } 414 415 nb, err := q.bcheckAssignment1(lhs, lTyp, op, rhs) 416 if err != nil { 417 return err 418 } 419 420 if lhs == nil { 421 return nil 422 } 423 424 if op == t.IDEq { 425 // Drop any facts involving lhs. 426 if err := q.facts.update(func(x *a.Expr) (*a.Expr, error) { 427 if x.Mentions(lhs) { 428 return nil, nil 429 } 430 return x, nil 431 }); err != nil { 432 return err 433 } 434 435 if lhs.MType().IsNumType() && rhs.Effect().Pure() { 436 q.facts.appendBinaryOpFact(t.IDXBinaryEqEq, lhs, rhs) 437 } 438 439 } else { 440 // Update any facts involving lhs. 441 if err := q.facts.update(func(x *a.Expr) (*a.Expr, error) { 442 xOp, xLHS, xRHS := parseBinaryOp(x) 443 if xOp == 0 || !xLHS.Eq(lhs) { 444 if x.Mentions(lhs) { 445 return nil, nil 446 } 447 return x, nil 448 } 449 if xRHS.Mentions(lhs) { 450 return nil, nil 451 } 452 switch op { 453 case t.IDPlusEq, t.IDMinusEq: 454 oRHS := a.NewExpr(0, op.BinaryForm(), 0, 0, xRHS.AsNode(), nil, rhs.AsNode(), nil) 455 // TODO: call SetMBounds? 456 oRHS.SetMType(typeExprIdeal) 457 oRHS, err := simplify(q.tm, oRHS) 458 if err != nil { 459 return nil, err 460 } 461 o := a.NewExpr(0, xOp, 0, 0, xLHS.AsNode(), nil, oRHS.AsNode(), nil) 462 o.SetMBounds(bounds{zero, one}) 463 o.SetMType(typeExprBool) 464 return o, nil 465 } 466 return nil, nil 467 }); err != nil { 468 return err 469 } 470 } 471 472 if lhs.MType().IsNumType() && ((op != t.IDEq) || (rhs.ConstValue() == nil)) { 473 lb, err := q.bcheckTypeExpr(lhs.MType()) 474 if err != nil { 475 return err 476 } 477 if lb[0].Cmp(nb[0]) < 0 { 478 c, err := makeConstValueExpr(q.tm, nb[0]) 479 if err != nil { 480 return err 481 } 482 q.facts.appendBinaryOpFact(t.IDXBinaryGreaterEq, lhs, c) 483 } 484 if lb[1].Cmp(nb[1]) > 0 { 485 c, err := makeConstValueExpr(q.tm, nb[1]) 486 if err != nil { 487 return err 488 } 489 q.facts.appendBinaryOpFact(t.IDXBinaryLessEq, lhs, c) 490 } 491 } 492 493 return nil 494} 495 496func (q *checker) bcheckAssignment1(lhs *a.Expr, lTyp *a.TypeExpr, op t.ID, rhs *a.Expr) (bounds, error) { 497 if lhs == nil && op != t.IDEq { 498 return bounds{}, fmt.Errorf("check: internal error: missing LHS for op key 0x%02X", op) 499 } 500 501 lb, err := bounds{}, (error)(nil) 502 if lTyp != nil { 503 lb, err = q.bcheckTypeExpr(lTyp) 504 if err != nil { 505 return bounds{}, err 506 } 507 } 508 509 rb := bounds{} 510 if op == t.IDEq || op == t.IDEqQuestion { 511 rb, err = q.bcheckExpr(rhs, 0) 512 } else { 513 rb, err = q.bcheckExprBinaryOp(op.BinaryForm(), lhs, rhs, 0) 514 } 515 if err != nil { 516 return bounds{}, err 517 } 518 519 if (lTyp != nil) && ((rb[0].Cmp(lb[0]) < 0) || (rb[1].Cmp(lb[1]) > 0)) { 520 if op == t.IDEq { 521 return bounds{}, fmt.Errorf("check: expression %q bounds %v is not within bounds %v", 522 rhs.Str(q.tm), rb, lb) 523 } else { 524 return bounds{}, fmt.Errorf("check: assignment %q bounds %v is not within bounds %v", 525 lhs.Str(q.tm)+" "+op.Str(q.tm)+" "+rhs.Str(q.tm), rb, lb) 526 } 527 } 528 return rb, nil 529} 530 531// terminates returns whether a block of statements terminates. In other words, 532// whether the block is non-empty and its final statement is a "return", 533// "break", "continue" or an "if-else" chain where all branches terminate. 534// 535// TODO: strengthen this to include "while" statements? For inspiration, the Go 536// spec has https://golang.org/ref/spec#Terminating_statements 537func terminates(body []*a.Node) bool { 538 if len(body) > 0 { 539 n := body[len(body)-1] 540 switch n.Kind() { 541 case a.KIf: 542 n := n.AsIf() 543 for { 544 if !terminates(n.BodyIfTrue()) { 545 return false 546 } 547 bif := n.BodyIfFalse() 548 if len(bif) > 0 && !terminates(bif) { 549 return false 550 } 551 n = n.ElseIf() 552 if n == nil { 553 return len(bif) > 0 554 } 555 } 556 case a.KJump: 557 return true 558 case a.KRet: 559 return n.AsRet().Keyword() == t.IDReturn 560 } 561 return false 562 } 563 return false 564} 565 566func snapshot(facts []*a.Expr) []*a.Expr { 567 return append([]*a.Expr(nil), facts...) 568} 569 570func (q *checker) unify(branches [][]*a.Expr) error { 571 q.facts = q.facts[:0] 572 if len(branches) == 0 { 573 return nil 574 } 575 q.facts = append(q.facts[:0], branches[0]...) 576 if len(branches) == 1 { 577 return nil 578 } 579 if len(branches) > 10000 { 580 return fmt.Errorf("too many if-else branches") 581 } 582 583 m := map[string]int{} 584 for _, b := range branches { 585 for _, f := range b { 586 m[f.Str(q.tm)]++ 587 } 588 } 589 590 return q.facts.update(func(n *a.Expr) (*a.Expr, error) { 591 if m[n.Str(q.tm)] == len(branches) { 592 return n, nil 593 } 594 return nil, nil 595 }) 596} 597 598func (q *checker) bcheckIf(n *a.If) error { 599 branches := [][]*a.Expr(nil) 600 for n != nil { 601 snap := snapshot(q.facts) 602 // Check the if condition. 603 if _, err := q.bcheckExpr(n.Condition(), 0); err != nil { 604 return err 605 } 606 607 // Check the if-true branch, assuming the if condition. 608 if n.Condition().ConstValue() == nil { 609 q.facts.appendFact(n.Condition()) 610 } 611 if err := q.bcheckBlock(n.BodyIfTrue()); err != nil { 612 return err 613 } 614 if !terminates(n.BodyIfTrue()) { 615 branches = append(branches, snapshot(q.facts)) 616 } 617 618 // Check the if-false branch, assuming the inverted if condition. 619 q.facts = append(q.facts[:0], snap...) 620 if n.Condition().ConstValue() == nil { 621 if inverse, err := invert(q.tm, n.Condition()); err != nil { 622 return err 623 } else { 624 q.facts.appendFact(inverse) 625 } 626 } 627 if bif := n.BodyIfFalse(); len(bif) > 0 { 628 if err := q.bcheckBlock(bif); err != nil { 629 return err 630 } 631 if !terminates(bif) { 632 branches = append(branches, snapshot(q.facts)) 633 } 634 break 635 } 636 n = n.ElseIf() 637 if n == nil { 638 branches = append(branches, snapshot(q.facts)) 639 break 640 } 641 } 642 return q.unify(branches) 643} 644 645func (q *checker) bcheckWhile(n *a.While) error { 646 // Check the pre and inv conditions on entry. 647 for _, o := range n.Asserts() { 648 if o.AsAssert().Keyword() == t.IDPost { 649 continue 650 } 651 if err := q.bcheckAssert(o.AsAssert()); err != nil { 652 return err 653 } 654 } 655 656 // Check the while condition. 657 if _, err := q.bcheckExpr(n.Condition(), 0); err != nil { 658 return err 659 } 660 661 // Check the post conditions on exit, assuming only the pre and inv 662 // (invariant) conditions and the inverted while condition. 663 // 664 // We don't need to check the inv conditions, even though we add them to 665 // the facts after the while loop, since we have already proven each inv 666 // condition on entry, and below, proven them on each explicit continue and 667 // on the implicit continue after the body. 668 if cv := n.Condition().ConstValue(); cv != nil && cv.Cmp(one) == 0 { 669 // We effectively have a "while true { etc }" loop. There's no need to 670 // prove the post conditions here, since we won't ever exit the while 671 // loop naturally. We only exit on an explicit break. 672 } else { 673 q.facts = q.facts[:0] 674 for _, o := range n.Asserts() { 675 if o.AsAssert().Keyword() == t.IDPost { 676 continue 677 } 678 q.facts.appendFact(o.AsAssert().Condition()) 679 } 680 if inverse, err := invert(q.tm, n.Condition()); err != nil { 681 return err 682 } else { 683 q.facts.appendFact(inverse) 684 } 685 for _, o := range n.Asserts() { 686 if o.AsAssert().Keyword() == t.IDPost { 687 if err := q.bcheckAssert(o.AsAssert()); err != nil { 688 return err 689 } 690 } 691 } 692 } 693 694 if cv := n.Condition().ConstValue(); cv != nil && cv.Sign() == 0 { 695 // We effectively have a "while false { etc }" loop. There's no need to 696 // check the body. 697 } else { 698 // Assume the pre and inv conditions... 699 q.facts = q.facts[:0] 700 for _, o := range n.Asserts() { 701 if o.AsAssert().Keyword() == t.IDPost { 702 continue 703 } 704 q.facts.appendFact(o.AsAssert().Condition()) 705 } 706 // ...and the while condition, unless it is the redundant "true". 707 if cv == nil { 708 q.facts.appendFact(n.Condition()) 709 } 710 // Check the body. 711 if err := q.bcheckBlock(n.Body()); err != nil { 712 return err 713 } 714 // Check the pre and inv conditions on the implicit continue after the 715 // body. 716 if !terminates(n.Body()) { 717 for _, o := range n.Asserts() { 718 if o.AsAssert().Keyword() == t.IDPost { 719 continue 720 } 721 if err := q.bcheckAssert(o.AsAssert()); err != nil { 722 return err 723 } 724 } 725 } 726 } 727 728 // Assume the inv and post conditions. 729 q.facts = q.facts[:0] 730 for _, o := range n.Asserts() { 731 if o.AsAssert().Keyword() == t.IDPre { 732 continue 733 } 734 q.facts.appendFact(o.AsAssert().Condition()) 735 } 736 return nil 737} 738 739func (q *checker) bcheckVar(n *a.Var) error { 740 if _, err := q.bcheckTypeExpr(n.XType()); err != nil { 741 return err 742 } 743 744 lhs := a.NewExpr(0, 0, 0, n.Name(), nil, nil, nil, nil) 745 lhs.SetMType(n.XType()) 746 // "var x T" has an implicit "= 0". 747 // 748 // TODO: check that T is an integer type. 749 rhs := zeroExpr 750 return q.bcheckAssignment(lhs, t.IDEq, rhs) 751} 752 753func (q *checker) bcheckExpr(n *a.Expr, depth uint32) (bounds, error) { 754 if depth > a.MaxExprDepth { 755 return bounds{}, fmt.Errorf("check: expression recursion depth too large") 756 } 757 depth++ 758 759 if b := n.MBounds(); b[0] != nil { 760 return b, nil 761 } 762 if n.ConstValue() != nil { 763 return bcheckExprConstValue(n), nil 764 } 765 766 nb, err := q.bcheckExpr1(n, depth) 767 if err != nil { 768 return bounds{}, err 769 } 770 nb, err = q.facts.refine(n, nb, q.tm) 771 if err != nil { 772 return bounds{}, err 773 } 774 tb, err := q.bcheckTypeExpr(n.MType()) 775 if err != nil { 776 return bounds{}, err 777 } 778 779 if (nb[0].Cmp(tb[0]) < 0) || (nb[1].Cmp(tb[1]) > 0) { 780 return bounds{}, fmt.Errorf("check: expression %q bounds %v is not within bounds %v", 781 n.Str(q.tm), nb, tb) 782 } 783 784 n.SetMBounds(nb) 785 return nb, nil 786} 787 788func bcheckExprConstValue(n *a.Expr) bounds { 789 if o := n.LHS(); o != nil { 790 bcheckExprConstValue(o.AsExpr()) 791 } 792 if o := n.MHS(); o != nil { 793 bcheckExprConstValue(o.AsExpr()) 794 } 795 if o := n.RHS(); o != nil && n.Operator() != t.IDXBinaryAs { 796 bcheckExprConstValue(o.AsExpr()) 797 } 798 cv := n.ConstValue() 799 b := bounds{cv, cv} 800 n.SetMBounds(b) 801 return b 802} 803 804func (q *checker) bcheckExpr1(n *a.Expr, depth uint32) (bounds, error) { 805 switch op := n.Operator(); { 806 case op.IsXUnaryOp(): 807 return q.bcheckExprUnaryOp(n, depth) 808 case op.IsXBinaryOp(): 809 if op == t.IDXBinaryAs { 810 return q.bcheckExpr(n.LHS().AsExpr(), depth) 811 } 812 return q.bcheckExprBinaryOp(op, n.LHS().AsExpr(), n.RHS().AsExpr(), depth) 813 case op.IsXAssociativeOp(): 814 return q.bcheckExprAssociativeOp(n, depth) 815 } 816 817 return q.bcheckExprOther(n, depth) 818} 819 820func (q *checker) bcheckExprOther(n *a.Expr, depth uint32) (bounds, error) { 821 switch n.Operator() { 822 case 0: 823 // Look for named consts. 824 // 825 // TODO: look up "foo[i]" const expressions. 826 // 827 // TODO: allow imported consts, "foo.bar", not just "bar"? 828 qid := t.QID{0, n.Ident()} 829 if c, ok := q.c.consts[qid]; ok { 830 if cv := c.Value().ConstValue(); cv != nil { 831 return bounds{cv, cv}, nil 832 } 833 } 834 835 case t.IDOpenParen: 836 lhs := n.LHS().AsExpr() 837 if _, err := q.bcheckExpr(lhs, depth); err != nil { 838 return bounds{}, err 839 } 840 if err := q.bcheckExprCall(n, depth); err != nil { 841 return bounds{}, err 842 } 843 if nb, err := q.bcheckExprCallSpecialCases(n, depth); err == nil { 844 return nb, nil 845 } else if err != errNotASpecialCase { 846 return bounds{}, err 847 } 848 849 case t.IDOpenBracket: 850 lhs := n.LHS().AsExpr() 851 if _, err := q.bcheckExpr(lhs, depth); err != nil { 852 return bounds{}, err 853 } 854 rhs := n.RHS().AsExpr() 855 if _, err := q.bcheckExpr(rhs, depth); err != nil { 856 return bounds{}, err 857 } 858 859 lengthExpr := (*a.Expr)(nil) 860 if lTyp := lhs.MType(); lTyp.IsArrayType() { 861 lengthExpr = lTyp.ArrayLength() 862 } else { 863 lengthExpr = makeSliceLength(lhs) 864 } 865 866 if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, rhs); err != nil { 867 return bounds{}, err 868 } 869 if err := proveReasonRequirementForRHSLength(q, t.IDXBinaryLessThan, rhs, lengthExpr); err != nil { 870 return bounds{}, err 871 } 872 873 case t.IDColon: 874 lhs := n.LHS().AsExpr() 875 if _, err := q.bcheckExpr(lhs, depth); err != nil { 876 return bounds{}, err 877 } 878 mhs := n.MHS().AsExpr() 879 if mhs != nil { 880 if _, err := q.bcheckExpr(mhs, depth); err != nil { 881 return bounds{}, err 882 } 883 } 884 rhs := n.RHS().AsExpr() 885 if rhs != nil { 886 if _, err := q.bcheckExpr(rhs, depth); err != nil { 887 return bounds{}, err 888 } 889 } 890 891 if mhs == nil && rhs == nil { 892 return bounds{zero, zero}, nil 893 } 894 895 lengthExpr := (*a.Expr)(nil) 896 if lTyp := lhs.MType(); lTyp.IsArrayType() { 897 lengthExpr = lTyp.ArrayLength() 898 } else { 899 lengthExpr = makeSliceLength(lhs) 900 } 901 902 if mhs == nil { 903 mhs = zeroExpr 904 } 905 if rhs == nil { 906 rhs = lengthExpr 907 } 908 909 if mhs != zeroExpr { 910 if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, mhs); err != nil { 911 return bounds{}, err 912 } 913 } 914 if err := proveReasonRequirement(q, t.IDXBinaryLessEq, mhs, rhs); err != nil { 915 return bounds{}, err 916 } 917 if rhs != lengthExpr { 918 if err := proveReasonRequirementForRHSLength(q, t.IDXBinaryLessEq, rhs, lengthExpr); err != nil { 919 return bounds{}, err 920 } 921 } 922 923 case t.IDDot: 924 if _, err := q.bcheckExpr(n.LHS().AsExpr(), depth); err != nil { 925 return bounds{}, err 926 } 927 928 // TODO: delete this hack that only matches "args". 929 if n.LHS().AsExpr().Ident() == t.IDArgs { 930 for _, o := range q.astFunc.In().Fields() { 931 o := o.AsField() 932 if o.Name() == n.Ident() { 933 return q.bcheckTypeExpr(o.XType()) 934 } 935 } 936 lTyp := n.LHS().AsExpr().MType() 937 return bounds{}, fmt.Errorf("check: no field named %q found in struct type %q for expression %q", 938 n.Ident().Str(q.tm), lTyp.QID().Str(q.tm), n.Str(q.tm)) 939 } 940 941 case t.IDComma: 942 for _, o := range n.Args() { 943 if _, err := q.bcheckExpr(o.AsExpr(), depth); err != nil { 944 return bounds{}, err 945 } 946 } 947 948 default: 949 return bounds{}, fmt.Errorf("check: unrecognized token (0x%X) for bcheckExprOther", n.Operator()) 950 } 951 return q.bcheckTypeExpr(n.MType()) 952} 953 954func (q *checker) bcheckExprCall(n *a.Expr, depth uint32) error { 955 // TODO: handle func pre/post conditions. 956 lhs := n.LHS().AsExpr() 957 f, err := q.c.resolveFunc(lhs.MType()) 958 if err != nil { 959 return err 960 } 961 inFields := f.In().Fields() 962 if len(inFields) != len(n.Args()) { 963 return fmt.Errorf("check: %q has %d arguments but %d were given", 964 lhs.MType().Str(q.tm), len(inFields), len(n.Args())) 965 } 966 for i, o := range n.Args() { 967 if _, err := q.bcheckAssignment1(nil, inFields[i].AsField().XType(), t.IDEq, o.AsArg().Value()); err != nil { 968 return err 969 } 970 } 971 972 recv := lhs.LHS().AsExpr() 973 if recv.MType().Decorator() != t.IDNptr { 974 return nil 975 } 976 // Check that q.facts contain "recv != nullptr". 977 for _, x := range q.facts { 978 if x.Operator() != t.IDXBinaryNotEq { 979 continue 980 } 981 xLHS := x.LHS().AsExpr() 982 xRHS := x.RHS().AsExpr() 983 if (xLHS.Eq(exprNullptr) && xRHS.Eq(recv)) || 984 (xRHS.Eq(exprNullptr) && xLHS.Eq(recv)) { 985 return nil 986 } 987 } 988 return fmt.Errorf("check: cannot prove %q", recv.Str(q.tm)+" != nullptr") 989} 990 991var errNotASpecialCase = errors.New("not a special case") 992 993func (q *checker) bcheckExprCallSpecialCases(n *a.Expr, depth uint32) (bounds, error) { 994 lhs := n.LHS().AsExpr() 995 recv := lhs.LHS().AsExpr() 996 method := lhs.Ident() 997 998 if recvTyp := recv.MType(); recvTyp == nil { 999 return bounds{}, errNotASpecialCase 1000 1001 } else if recvTyp.IsNumType() { 1002 // For a numeric type's low_bits, etc. methods. The bound on the output 1003 // is dependent on bound on the input, similar to dependent types, and 1004 // isn't expressible in Wuffs' function syntax and type system. 1005 switch method { 1006 case t.IDLowBits, t.IDHighBits: 1007 ab, err := q.bcheckExpr(n.Args()[0].AsArg().Value(), depth) 1008 if err != nil { 1009 return bounds{}, err 1010 } 1011 return bounds{ 1012 zero, 1013 bitMask(int(ab[1].Int64())), 1014 }, nil 1015 1016 case t.IDMin, t.IDMax: 1017 // TODO: lhs has already been bcheck'ed. There should be no 1018 // need to bcheck lhs.LHS().Expr() twice. 1019 lb, err := q.bcheckExpr(lhs.LHS().AsExpr(), depth) 1020 if err != nil { 1021 return bounds{}, err 1022 } 1023 ab, err := q.bcheckExpr(n.Args()[0].AsArg().Value(), depth) 1024 if err != nil { 1025 return bounds{}, err 1026 } 1027 if method == t.IDMin { 1028 return bounds{ 1029 min(lb[0], ab[0]), 1030 min(lb[1], ab[1]), 1031 }, nil 1032 } else { 1033 return bounds{ 1034 max(lb[0], ab[0]), 1035 max(lb[1], ab[1]), 1036 }, nil 1037 } 1038 } 1039 1040 } else if recvTyp.IsIOType() { 1041 advance, update := (*big.Int)(nil), false 1042 1043 if method == t.IDUndoByte { 1044 if err := q.canUndoByte(recv); err != nil { 1045 return bounds{}, err 1046 } 1047 1048 } else if method == t.IDCopyNFromHistoryFast { 1049 if err := q.canCopyNFromHistoryFast(recv, n.Args()); err != nil { 1050 return bounds{}, err 1051 } 1052 1053 } else if method == t.IDSkipFast { 1054 args := n.Args() 1055 if len(args) != 2 { 1056 return bounds{}, fmt.Errorf("check: internal error: bad skip_fast arguments") 1057 } 1058 actual := args[0].AsArg().Value() 1059 worstCase := args[1].AsArg().Value() 1060 if err := q.proveBinaryOp(t.IDXBinaryLessEq, actual, worstCase); err == errFailed { 1061 return bounds{}, fmt.Errorf("check: could not prove skip_fast pre-condition: %s <= %s", 1062 actual.Str(q.tm), worstCase.Str(q.tm)) 1063 } else if err != nil { 1064 return bounds{}, err 1065 } 1066 advance, update = worstCase.ConstValue(), true 1067 if advance == nil { 1068 return bounds{}, fmt.Errorf("check: skip_fast worst_case is not a constant value") 1069 } 1070 1071 } else if method >= t.IDPeekU8 { 1072 if m := method - t.IDPeekU8; m < t.ID(len(ioMethodAdvances)) { 1073 au := ioMethodAdvances[m] 1074 advance, update = au.advance, au.update 1075 } 1076 } 1077 1078 if advance != nil { 1079 if ok, err := q.optimizeIOMethodAdvance(recv, advance, update); err != nil { 1080 return bounds{}, err 1081 } else if !ok { 1082 return bounds{}, fmt.Errorf("check: could not prove %s pre-condition: %s.available() >= %v", 1083 method.Str(q.tm), recv.Str(q.tm), advance) 1084 } 1085 // TODO: drop other recv-related facts? 1086 } 1087 } 1088 1089 return bounds{}, errNotASpecialCase 1090} 1091 1092func (q *checker) canUndoByte(recv *a.Expr) error { 1093 for _, x := range q.facts { 1094 if x.Operator() != t.IDOpenParen || len(x.Args()) != 0 { 1095 continue 1096 } 1097 x = x.LHS().AsExpr() 1098 if x.Operator() != t.IDDot || x.Ident() != t.IDCanUndoByte { 1099 continue 1100 } 1101 x = x.LHS().AsExpr() 1102 if !x.Eq(recv) { 1103 continue 1104 } 1105 return q.facts.update(func(o *a.Expr) (*a.Expr, error) { 1106 if o.Mentions(recv) { 1107 return nil, nil 1108 } 1109 return o, nil 1110 }) 1111 } 1112 return fmt.Errorf("check: could not prove %s.can_undo_byte()", recv.Str(q.tm)) 1113} 1114 1115func (q *checker) canCopyNFromHistoryFast(recv *a.Expr, args []*a.Node) error { 1116 // As per cgen's io-private.h, there are three pre-conditions: 1117 // - n <= this.available() 1118 // - distance > 0 1119 // - distance <= this.history_available() 1120 1121 if len(args) != 2 { 1122 return fmt.Errorf("check: internal error: inconsistent copy_n_from_history_fast arguments") 1123 } 1124 n := args[0].AsArg().Value() 1125 distance := args[1].AsArg().Value() 1126 1127 // Check "n <= this.available()". 1128check0: 1129 for { 1130 for _, x := range q.facts { 1131 if x.Operator() != t.IDXBinaryLessEq { 1132 continue 1133 } 1134 1135 // Check that the LHS is "n as base.u64". 1136 lhs := x.LHS().AsExpr() 1137 if lhs.Operator() != t.IDXBinaryAs { 1138 continue 1139 } 1140 llhs, lrhs := lhs.LHS().AsExpr(), lhs.RHS().AsTypeExpr() 1141 if !llhs.Eq(n) || !lrhs.Eq(typeExprU64) { 1142 continue 1143 } 1144 1145 // Check that the RHS is "recv.available()". 1146 y, method, yArgs := splitReceiverMethodArgs(x.RHS().AsExpr()) 1147 if method != t.IDAvailable || len(yArgs) != 0 { 1148 continue 1149 } 1150 if !y.Eq(recv) { 1151 continue 1152 } 1153 1154 break check0 1155 } 1156 return fmt.Errorf("check: could not prove n <= %s.available()", recv.Str(q.tm)) 1157 } 1158 1159 // Check "distance > 0". 1160check1: 1161 for { 1162 for _, x := range q.facts { 1163 if x.Operator() != t.IDXBinaryGreaterThan { 1164 continue 1165 } 1166 if lhs := x.LHS().AsExpr(); !lhs.Eq(distance) { 1167 continue 1168 } 1169 if rcv := x.RHS().AsExpr().ConstValue(); rcv == nil || rcv.Sign() != 0 { 1170 continue 1171 } 1172 break check1 1173 } 1174 return fmt.Errorf("check: could not prove distance > 0") 1175 } 1176 1177 // Check "distance <= this.history_available()". 1178check2: 1179 for { 1180 for _, x := range q.facts { 1181 if x.Operator() != t.IDXBinaryLessEq { 1182 continue 1183 } 1184 1185 // Check that the LHS is "distance as base.u64". 1186 lhs := x.LHS().AsExpr() 1187 if lhs.Operator() != t.IDXBinaryAs { 1188 continue 1189 } 1190 llhs, lrhs := lhs.LHS().AsExpr(), lhs.RHS().AsTypeExpr() 1191 if !llhs.Eq(distance) || !lrhs.Eq(typeExprU64) { 1192 continue 1193 } 1194 1195 // Check that the RHS is "recv.history_available()". 1196 y, method, yArgs := splitReceiverMethodArgs(x.RHS().AsExpr()) 1197 if method != t.IDHistoryAvailable || len(yArgs) != 0 { 1198 continue 1199 } 1200 if !y.Eq(recv) { 1201 continue 1202 } 1203 1204 break check2 1205 } 1206 return fmt.Errorf("check: could not prove distance <= %s.history_available()", recv.Str(q.tm)) 1207 } 1208 1209 return nil 1210} 1211 1212var ioMethodAdvances = [...]struct { 1213 advance *big.Int 1214 update bool 1215}{ 1216 t.IDPeekU8 - t.IDPeekU8: {one, false}, 1217 1218 t.IDPeekU16BE - t.IDPeekU8: {two, false}, 1219 t.IDPeekU16LE - t.IDPeekU8: {two, false}, 1220 1221 t.IDPeekU8AsU32 - t.IDPeekU8: {one, false}, 1222 t.IDPeekU16BEAsU32 - t.IDPeekU8: {two, false}, 1223 t.IDPeekU16LEAsU32 - t.IDPeekU8: {two, false}, 1224 t.IDPeekU24BEAsU32 - t.IDPeekU8: {three, false}, 1225 t.IDPeekU24LEAsU32 - t.IDPeekU8: {three, false}, 1226 t.IDPeekU32BE - t.IDPeekU8: {four, false}, 1227 t.IDPeekU32LE - t.IDPeekU8: {four, false}, 1228 1229 t.IDPeekU8AsU64 - t.IDPeekU8: {one, false}, 1230 t.IDPeekU16BEAsU64 - t.IDPeekU8: {two, false}, 1231 t.IDPeekU16LEAsU64 - t.IDPeekU8: {two, false}, 1232 t.IDPeekU24BEAsU64 - t.IDPeekU8: {three, false}, 1233 t.IDPeekU24LEAsU64 - t.IDPeekU8: {three, false}, 1234 t.IDPeekU32BEAsU64 - t.IDPeekU8: {four, false}, 1235 t.IDPeekU32LEAsU64 - t.IDPeekU8: {four, false}, 1236 t.IDPeekU40BEAsU64 - t.IDPeekU8: {five, false}, 1237 t.IDPeekU40LEAsU64 - t.IDPeekU8: {five, false}, 1238 t.IDPeekU48BEAsU64 - t.IDPeekU8: {six, false}, 1239 t.IDPeekU48LEAsU64 - t.IDPeekU8: {six, false}, 1240 t.IDPeekU56BEAsU64 - t.IDPeekU8: {seven, false}, 1241 t.IDPeekU56LEAsU64 - t.IDPeekU8: {seven, false}, 1242 t.IDPeekU64BE - t.IDPeekU8: {eight, false}, 1243 t.IDPeekU64LE - t.IDPeekU8: {eight, false}, 1244 1245 t.IDWriteFastU8 - t.IDPeekU8: {one, true}, 1246 t.IDWriteFastU16BE - t.IDPeekU8: {two, true}, 1247 t.IDWriteFastU16LE - t.IDPeekU8: {two, true}, 1248 t.IDWriteFastU24BE - t.IDPeekU8: {three, true}, 1249 t.IDWriteFastU24LE - t.IDPeekU8: {three, true}, 1250 t.IDWriteFastU32BE - t.IDPeekU8: {four, true}, 1251 t.IDWriteFastU32LE - t.IDPeekU8: {four, true}, 1252 t.IDWriteFastU40BE - t.IDPeekU8: {five, true}, 1253 t.IDWriteFastU40LE - t.IDPeekU8: {five, true}, 1254 t.IDWriteFastU48BE - t.IDPeekU8: {six, true}, 1255 t.IDWriteFastU48LE - t.IDPeekU8: {six, true}, 1256 t.IDWriteFastU56BE - t.IDPeekU8: {seven, true}, 1257 t.IDWriteFastU56LE - t.IDPeekU8: {seven, true}, 1258 t.IDWriteFastU64BE - t.IDPeekU8: {eight, true}, 1259 t.IDWriteFastU64LE - t.IDPeekU8: {eight, true}, 1260} 1261 1262func makeConstValueExpr(tm *t.Map, cv *big.Int) (*a.Expr, error) { 1263 id, err := tm.Insert(cv.String()) 1264 if err != nil { 1265 return nil, err 1266 } 1267 o := a.NewExpr(0, 0, 0, id, nil, nil, nil, nil) 1268 o.SetConstValue(cv) 1269 o.SetMBounds(bounds{cv, cv}) 1270 o.SetMType(typeExprIdeal) 1271 return o, nil 1272} 1273 1274// makeSliceLength returns "x.length()". 1275func makeSliceLength(slice *a.Expr) *a.Expr { 1276 x := a.NewExpr(0, t.IDDot, 0, t.IDLength, slice.AsNode(), nil, nil, nil) 1277 x.SetMBounds(bounds{one, one}) 1278 x.SetMType(a.NewTypeExpr(t.IDFunc, 0, t.IDLength, slice.MType().AsNode(), nil, nil)) 1279 x = a.NewExpr(0, t.IDOpenParen, 0, 0, x.AsNode(), nil, nil, nil) 1280 // TODO: call SetMBounds? 1281 x.SetMType(typeExprU64) 1282 return x 1283} 1284 1285// makeSliceLengthEqEq returns "x.length() == n". 1286// 1287// n must be the t.ID of a small power of 2. 1288func makeSliceLengthEqEq(x t.ID, xTyp *a.TypeExpr, n t.ID) *a.Expr { 1289 xExpr := a.NewExpr(0, 0, 0, x, nil, nil, nil, nil) 1290 xExpr.SetMType(xTyp) 1291 1292 lhs := makeSliceLength(xExpr) 1293 1294 nValue := n.SmallPowerOf2Value() 1295 if nValue == 0 { 1296 panic("check: internal error: makeSliceLengthEqEq called but not with a small power of 2") 1297 } 1298 cv := big.NewInt(int64(nValue)) 1299 1300 rhs := a.NewExpr(0, 0, 0, n, nil, nil, nil, nil) 1301 rhs.SetConstValue(cv) 1302 rhs.SetMBounds(bounds{cv, cv}) 1303 rhs.SetMType(typeExprIdeal) 1304 1305 ret := a.NewExpr(0, t.IDXBinaryEqEq, 0, 0, lhs.AsNode(), nil, rhs.AsNode(), nil) 1306 ret.SetMBounds(bounds{zero, one}) 1307 ret.SetMType(typeExprBool) 1308 return ret 1309} 1310 1311func (q *checker) bcheckExprUnaryOp(n *a.Expr, depth uint32) (bounds, error) { 1312 rb, err := q.bcheckExpr(n.RHS().AsExpr(), depth) 1313 if err != nil { 1314 return bounds{}, err 1315 } 1316 1317 switch n.Operator() { 1318 case t.IDXUnaryPlus: 1319 return rb, nil 1320 case t.IDXUnaryMinus: 1321 return bounds{neg(rb[1]), neg(rb[0])}, nil 1322 case t.IDXUnaryNot: 1323 return bounds{zero, one}, nil 1324 case t.IDXUnaryRef, t.IDXUnaryDeref: 1325 return q.bcheckTypeExpr(n.MType()) 1326 } 1327 1328 return bounds{}, fmt.Errorf("check: unrecognized token (0x%X) for bcheckExprUnaryOp", n.Operator()) 1329} 1330 1331func (q *checker) bcheckExprXBinaryPlus(lhs *a.Expr, lb bounds, rhs *a.Expr, rb bounds) (bounds, error) { 1332 return lb.Add(rb), nil 1333} 1334 1335func (q *checker) bcheckExprXBinaryMinus(lhs *a.Expr, lb bounds, rhs *a.Expr, rb bounds) (bounds, error) { 1336 nb := lb.Sub(rb) 1337 for _, x := range q.facts { 1338 xOp, xLHS, xRHS := parseBinaryOp(x) 1339 if !lhs.Eq(xLHS) || !rhs.Eq(xRHS) { 1340 continue 1341 } 1342 switch xOp { 1343 case t.IDXBinaryLessThan: 1344 nb[1] = min(nb[1], minusOne) 1345 case t.IDXBinaryLessEq: 1346 nb[1] = min(nb[1], zero) 1347 case t.IDXBinaryGreaterEq: 1348 nb[0] = max(nb[0], zero) 1349 case t.IDXBinaryGreaterThan: 1350 nb[0] = max(nb[0], one) 1351 } 1352 } 1353 return nb, nil 1354} 1355 1356func (q *checker) bcheckExprBinaryOp(op t.ID, lhs *a.Expr, rhs *a.Expr, depth uint32) (bounds, error) { 1357 lb, err := q.bcheckExpr(lhs, depth) 1358 if err != nil { 1359 return bounds{}, err 1360 } 1361 return q.bcheckExprBinaryOp1(op, lhs, lb, rhs, depth) 1362} 1363 1364func (q *checker) bcheckExprBinaryOp1(op t.ID, lhs *a.Expr, lb bounds, rhs *a.Expr, depth uint32) (bounds, error) { 1365 rb, err := q.bcheckExpr(rhs, depth) 1366 if err != nil { 1367 return bounds{}, err 1368 } 1369 1370 switch op { 1371 case t.IDXBinaryPlus: 1372 return q.bcheckExprXBinaryPlus(lhs, lb, rhs, rb) 1373 1374 case t.IDXBinaryMinus: 1375 return q.bcheckExprXBinaryMinus(lhs, lb, rhs, rb) 1376 1377 case t.IDXBinaryStar: 1378 return lb.Mul(rb), nil 1379 1380 case t.IDXBinarySlash, t.IDXBinaryPercent: 1381 // Prohibit division by zero. 1382 if lb[0].Sign() < 0 { 1383 return bounds{}, fmt.Errorf("check: divide/modulus op argument %q is possibly negative", lhs.Str(q.tm)) 1384 } 1385 if rb[0].Sign() <= 0 { 1386 return bounds{}, fmt.Errorf("check: divide/modulus op argument %q is possibly non-positive", rhs.Str(q.tm)) 1387 } 1388 if op == t.IDXBinarySlash { 1389 nb, _ := lb.Quo(rb) 1390 return nb, nil 1391 } 1392 return bounds{ 1393 zero, 1394 big.NewInt(0).Sub(rb[1], one), 1395 }, nil 1396 1397 case t.IDXBinaryShiftL, t.IDXBinaryTildeModShiftL, t.IDXBinaryShiftR: 1398 shiftBounds := bounds{} 1399 typeBounds := bounds{} 1400 if lTyp := lhs.MType(); lTyp.IsNumType() { 1401 id := int(lTyp.QID()[1]) 1402 if id < len(numShiftBounds) { 1403 shiftBounds = numShiftBounds[id] 1404 } 1405 if id < len(numTypeBounds) { 1406 typeBounds = numTypeBounds[id] 1407 } 1408 } 1409 if shiftBounds[0] == nil { 1410 return bounds{}, fmt.Errorf("check: shift op argument %q of type %q does not have unsigned integer type", 1411 lhs.Str(q.tm), lhs.MType().Str(q.tm)) 1412 } else if !shiftBounds.ContainsIntRange(rb) { 1413 return bounds{}, fmt.Errorf("check: shift op argument %q is outside the range %s", rhs.Str(q.tm), shiftBounds) 1414 } 1415 1416 switch op { 1417 case t.IDXBinaryShiftL: 1418 nb, _ := lb.Lsh(rb) 1419 return nb, nil 1420 case t.IDXBinaryTildeModShiftL: 1421 nb, _ := lb.Lsh(rb) 1422 nb[1] = min(nb[1], typeBounds[1]) 1423 return nb, nil 1424 case t.IDXBinaryShiftR: 1425 nb, _ := lb.Rsh(rb) 1426 return nb, nil 1427 } 1428 1429 case t.IDXBinaryAmp, t.IDXBinaryPipe, t.IDXBinaryHat: 1430 // TODO: should type-checking ensure that bitwise ops only apply to 1431 // *unsigned* integer types? 1432 if lb[0].Sign() < 0 { 1433 return bounds{}, fmt.Errorf("check: bitwise op argument %q is possibly negative", lhs.Str(q.tm)) 1434 } 1435 if rb[0].Sign() < 0 { 1436 return bounds{}, fmt.Errorf("check: bitwise op argument %q is possibly negative", rhs.Str(q.tm)) 1437 } 1438 switch op { 1439 case t.IDXBinaryAmp: 1440 nb, _ := lb.And(rb) 1441 return nb, nil 1442 case t.IDXBinaryPipe: 1443 nb, _ := lb.Or(rb) 1444 return nb, nil 1445 case t.IDXBinaryHat: 1446 z := max(lb[1], rb[1]) 1447 // Return [0, z rounded up to the next power-of-2-minus-1]. This is 1448 // conservative, but works fine in practice. 1449 return bounds{ 1450 zero, 1451 bitMask(z.BitLen()), 1452 }, nil 1453 } 1454 1455 case t.IDXBinaryTildeModPlus, t.IDXBinaryTildeModMinus: 1456 typ := lhs.MType() 1457 if typ.IsIdeal() { 1458 typ = rhs.MType() 1459 } 1460 if qid := typ.QID(); qid[0] == t.IDBase { 1461 return numTypeBounds[qid[1]], nil 1462 } 1463 1464 case t.IDXBinaryTildeSatPlus, t.IDXBinaryTildeSatMinus: 1465 typ := lhs.MType() 1466 if typ.IsIdeal() { 1467 typ = rhs.MType() 1468 } 1469 if qid := typ.QID(); qid[0] == t.IDBase { 1470 b := numTypeBounds[qid[1]] 1471 1472 nFunc := (*checker).bcheckExprXBinaryPlus 1473 if op != t.IDXBinaryTildeSatPlus { 1474 nFunc = (*checker).bcheckExprXBinaryMinus 1475 } 1476 nb, err := nFunc(q, lhs, lb, rhs, rb) 1477 if err != nil { 1478 return bounds{}, err 1479 } 1480 1481 if op == t.IDXBinaryTildeSatPlus { 1482 nb[0] = min(nb[0], b[1]) 1483 nb[1] = min(nb[1], b[1]) 1484 } else { 1485 nb[0] = max(nb[0], b[0]) 1486 nb[1] = max(nb[1], b[0]) 1487 } 1488 return nb, nil 1489 } 1490 1491 case t.IDXBinaryNotEq, t.IDXBinaryLessThan, t.IDXBinaryLessEq, t.IDXBinaryEqEq, 1492 t.IDXBinaryGreaterEq, t.IDXBinaryGreaterThan, t.IDXBinaryAnd, t.IDXBinaryOr: 1493 return bounds{zero, one}, nil 1494 1495 case t.IDXBinaryAs: 1496 // Unreachable, as this is checked by the caller. 1497 } 1498 return bounds{}, fmt.Errorf("check: unrecognized token (0x%X) for bcheckExprBinaryOp", op) 1499} 1500 1501func (q *checker) bcheckExprAssociativeOp(n *a.Expr, depth uint32) (bounds, error) { 1502 op := n.Operator().AmbiguousForm().BinaryForm() 1503 if op == 0 { 1504 return bounds{}, fmt.Errorf( 1505 "check: unrecognized token (0x%X) for bcheckExprAssociativeOp", n.Operator()) 1506 } 1507 args := n.Args() 1508 if len(args) < 1 { 1509 return bounds{}, fmt.Errorf("check: associative op has no arguments") 1510 } 1511 lb, err := q.bcheckExpr(args[0].AsExpr(), depth) 1512 if err != nil { 1513 return bounds{}, err 1514 } 1515 for i, o := range args { 1516 if i == 0 { 1517 continue 1518 } 1519 lhs := a.NewExpr(n.AsNode().AsRaw().Flags(), 1520 n.Operator(), 0, n.Ident(), n.LHS(), n.MHS(), n.RHS(), args[:i]) 1521 lb, err = q.bcheckExprBinaryOp1(op, lhs, lb, o.AsExpr(), depth) 1522 if err != nil { 1523 return bounds{}, err 1524 } 1525 } 1526 return lb, nil 1527} 1528 1529func (q *checker) bcheckTypeExpr(typ *a.TypeExpr) (bounds, error) { 1530 if b := typ.AsNode().MBounds(); b[0] != nil { 1531 return b, nil 1532 } 1533 b, err := q.bcheckTypeExpr1(typ) 1534 if err != nil { 1535 return bounds{}, err 1536 } 1537 typ.AsNode().SetMBounds(b) 1538 return b, nil 1539} 1540 1541func (q *checker) bcheckTypeExpr1(typ *a.TypeExpr) (bounds, error) { 1542 if typ.IsIdeal() { 1543 return bounds{minIdeal, maxIdeal}, nil 1544 } 1545 1546 if innTyp := typ.Inner(); innTyp != nil { 1547 if _, err := q.bcheckTypeExpr(innTyp); err != nil { 1548 return bounds{}, err 1549 } 1550 } 1551 1552 switch typ.Decorator() { 1553 case 0: 1554 // No-op. 1555 case t.IDArray: 1556 if _, err := q.bcheckExpr(typ.ArrayLength(), 0); err != nil { 1557 return bounds{}, err 1558 } 1559 return bounds{zero, zero}, nil 1560 case t.IDFunc: 1561 if _, err := q.bcheckTypeExpr(typ.Receiver()); err != nil { 1562 return bounds{}, err 1563 } 1564 return bounds{one, one}, nil 1565 case t.IDNptr: 1566 return bounds{zero, one}, nil 1567 case t.IDPtr: 1568 return bounds{one, one}, nil 1569 case t.IDSlice, t.IDTable: 1570 return bounds{zero, zero}, nil 1571 default: 1572 return bounds{}, fmt.Errorf("check: internal error: unrecognized decorator") 1573 } 1574 1575 b := bounds{zero, zero} 1576 1577 if qid := typ.QID(); qid[0] == t.IDBase { 1578 if qid[1] == t.IDDagger1 || qid[1] == t.IDDagger2 { 1579 return bounds{zero, zero}, nil 1580 } else if qid[1] < t.ID(len(numTypeBounds)) { 1581 if x := numTypeBounds[qid[1]]; x[0] != nil { 1582 b = x 1583 } 1584 } 1585 } 1586 1587 if typ.IsRefined() { 1588 if x := typ.Min(); x != nil { 1589 if _, err := q.bcheckExpr(x, 0); err != nil { 1590 return bounds{}, err 1591 } 1592 if cv := x.ConstValue(); cv == nil { 1593 return bounds{}, fmt.Errorf("check: internal error: refinement has no const-value") 1594 } else if cv.Cmp(b[0]) < 0 { 1595 return bounds{}, fmt.Errorf("check: type refinement %v for %q is out of bounds", cv, typ.Str(q.tm)) 1596 } else { 1597 b[0] = cv 1598 } 1599 } 1600 1601 if x := typ.Max(); x != nil { 1602 if _, err := q.bcheckExpr(x, 0); err != nil { 1603 return bounds{}, err 1604 } 1605 if cv := x.ConstValue(); cv == nil { 1606 return bounds{}, fmt.Errorf("check: internal error: refinement has no const-value") 1607 } else if cv.Cmp(b[1]) > 0 { 1608 return bounds{}, fmt.Errorf("check: type refinement %v for %q is out of bounds", cv, typ.Str(q.tm)) 1609 } else { 1610 b[1] = cv 1611 } 1612 } 1613 } 1614 1615 return b, nil 1616} 1617