1 /* Derivation and subsumption rules for constraints. 2 Copyright (C) 2013-2018 Free Software Foundation, Inc. 3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com) 4 5 This file is part of GCC. 6 7 GCC is free software; you can redistribute it and/or modify 8 it under the terms of the GNU General Public License as published by 9 the Free Software Foundation; either version 3, or (at your option) 10 any later version. 11 12 GCC is distributed in the hope that it will be useful, 13 but WITHOUT ANY WARRANTY; without even the implied warranty of 14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15 GNU General Public License for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with GCC; see the file COPYING3. If not see 19 <http://www.gnu.org/licenses/>. */ 20 21 #include "config.h" 22 #define INCLUDE_LIST 23 #include "system.h" 24 #include "coretypes.h" 25 #include "tm.h" 26 #include "timevar.h" 27 #include "hash-set.h" 28 #include "machmode.h" 29 #include "vec.h" 30 #include "double-int.h" 31 #include "input.h" 32 #include "alias.h" 33 #include "symtab.h" 34 #include "wide-int.h" 35 #include "inchash.h" 36 #include "tree.h" 37 #include "stringpool.h" 38 #include "attribs.h" 39 #include "intl.h" 40 #include "flags.h" 41 #include "cp-tree.h" 42 #include "c-family/c-common.h" 43 #include "c-family/c-objc.h" 44 #include "cp-objcp-common.h" 45 #include "tree-inline.h" 46 #include "decl.h" 47 #include "toplev.h" 48 #include "type-utils.h" 49 50 namespace { 51 52 // Helper algorithms 53 54 template<typename I> 55 inline I 56 next (I iter) 57 { 58 return ++iter; 59 } 60 61 template<typename I, typename P> 62 inline bool 63 any_p (I first, I last, P pred) 64 { 65 while (first != last) 66 { 67 if (pred(*first)) 68 return true; 69 ++first; 70 } 71 return false; 72 } 73 74 bool prove_implication (tree, tree); 75 76 /*--------------------------------------------------------------------------- 77 Proof state 78 ---------------------------------------------------------------------------*/ 79 80 struct term_entry 81 { 82 tree t; 83 }; 84 85 /* Hashing function and equality for constraint entries. */ 86 87 struct term_hasher : ggc_ptr_hash<term_entry> 88 { 89 static hashval_t hash (term_entry *e) 90 { 91 return iterative_hash_template_arg (e->t, 0); 92 } 93 94 static bool equal (term_entry *e1, term_entry *e2) 95 { 96 return cp_tree_equal (e1->t, e2->t); 97 } 98 }; 99 100 /* A term list is a list of atomic constraints. It is used 101 to maintain the lists of assumptions and conclusions in a 102 proof goal. 103 104 Each term list maintains an iterator that refers to the current 105 term. This can be used by various tactics to support iteration 106 and stateful manipulation of the list. */ 107 struct term_list 108 { 109 typedef std::list<tree>::iterator iterator; 110 111 term_list (); 112 term_list (tree); 113 114 bool includes (tree); 115 iterator insert (iterator, tree); 116 iterator push_back (tree); 117 iterator erase (iterator); 118 iterator replace (iterator, tree); 119 iterator replace (iterator, tree, tree); 120 121 iterator begin() { return seq.begin(); } 122 iterator end() { return seq.end(); } 123 124 std::list<tree> seq; 125 hash_table<term_hasher> tab; 126 }; 127 128 inline 129 term_list::term_list () 130 : seq(), tab (11) 131 { 132 } 133 134 /* Initialize a term list with an initial term. */ 135 136 inline 137 term_list::term_list (tree t) 138 : seq (), tab (11) 139 { 140 push_back (t); 141 } 142 143 /* Returns true if T is the in the tree. */ 144 145 inline bool 146 term_list::includes (tree t) 147 { 148 term_entry ent = {t}; 149 return tab.find (&ent); 150 } 151 152 /* Append a term to the list. */ 153 inline term_list::iterator 154 term_list::push_back (tree t) 155 { 156 return insert (end(), t); 157 } 158 159 /* Insert a new (unseen) term T into the list before the proposition 160 indicated by ITER. Returns the iterator to the newly inserted 161 element. */ 162 163 term_list::iterator 164 term_list::insert (iterator iter, tree t) 165 { 166 gcc_assert (!includes (t)); 167 iter = seq.insert (iter, t); 168 term_entry ent = {t}; 169 term_entry** slot = tab.find_slot (&ent, INSERT); 170 term_entry* ptr = ggc_alloc<term_entry> (); 171 *ptr = ent; 172 *slot = ptr; 173 return iter; 174 } 175 176 /* Remove an existing term from the list. Returns an iterator referring 177 to the element after the removed term. This may be end(). */ 178 179 term_list::iterator 180 term_list::erase (iterator iter) 181 { 182 gcc_assert (includes (*iter)); 183 term_entry ent = {*iter}; 184 tab.remove_elt (&ent); 185 iter = seq.erase (iter); 186 return iter; 187 } 188 189 /* Replace the given term with that specified. If the term has 190 been previously seen, do not insert the term. Returns the 191 first iterator past the current term. */ 192 193 term_list::iterator 194 term_list::replace (iterator iter, tree t) 195 { 196 iter = erase (iter); 197 if (!includes (t)) 198 insert (iter, t); 199 return iter; 200 } 201 202 203 /* Replace the term at the given position by the supplied T1 204 followed by t2. This is used in certain logical operators to 205 load a list of assumptions or conclusions. */ 206 207 term_list::iterator 208 term_list::replace (iterator iter, tree t1, tree t2) 209 { 210 iter = erase (iter); 211 if (!includes (t1)) 212 insert (iter, t1); 213 if (!includes (t2)) 214 insert (iter, t2); 215 return iter; 216 } 217 218 /* A goal (or subgoal) models a sequent of the form 219 'A |- C' where A and C are lists of assumptions and 220 conclusions written as propositions in the constraint 221 language (i.e., lists of trees). */ 222 223 struct proof_goal 224 { 225 term_list assumptions; 226 term_list conclusions; 227 }; 228 229 /* A proof state owns a list of goals and tracks the 230 current sub-goal. The class also provides facilities 231 for managing subgoals and constructing term lists. */ 232 233 struct proof_state : std::list<proof_goal> 234 { 235 proof_state (); 236 237 iterator branch (iterator i); 238 iterator discharge (iterator i); 239 }; 240 241 /* Initialize the state with a single empty goal, and set that goal 242 as the current subgoal. */ 243 244 inline 245 proof_state::proof_state () 246 : std::list<proof_goal> (1) 247 { } 248 249 250 /* Branch the current goal by creating a new subgoal, returning a 251 reference to the new object. This does not update the current goal. */ 252 253 inline proof_state::iterator 254 proof_state::branch (iterator i) 255 { 256 gcc_assert (i != end()); 257 proof_goal& g = *i; 258 return insert (++i, g); 259 } 260 261 /* Discharge the current goal, setting it equal to the 262 next non-satisfied goal. */ 263 264 inline proof_state::iterator 265 proof_state::discharge (iterator i) 266 { 267 gcc_assert (i != end()); 268 return erase (i); 269 } 270 271 272 /*--------------------------------------------------------------------------- 273 Debugging 274 ---------------------------------------------------------------------------*/ 275 276 // void 277 // debug (term_list& ts) 278 // { 279 // for (term_list::iterator i = ts.begin(); i != ts.end(); ++i) 280 // verbatim (" # %E", *i); 281 // } 282 // 283 // void 284 // debug (proof_goal& g) 285 // { 286 // debug (g.assumptions); 287 // verbatim (" |-"); 288 // debug (g.conclusions); 289 // } 290 291 /*--------------------------------------------------------------------------- 292 Atomicity of constraints 293 ---------------------------------------------------------------------------*/ 294 295 /* Returns true if T is not an atomic constraint. */ 296 297 bool 298 non_atomic_constraint_p (tree t) 299 { 300 switch (TREE_CODE (t)) 301 { 302 case PRED_CONSTR: 303 case EXPR_CONSTR: 304 case TYPE_CONSTR: 305 case ICONV_CONSTR: 306 case DEDUCT_CONSTR: 307 case EXCEPT_CONSTR: 308 /* A pack expansion isn't atomic, but it can't decompose to prove an 309 atom, so it shouldn't cause analyze_atom to return undecided. */ 310 case EXPR_PACK_EXPANSION: 311 return false; 312 case CHECK_CONSTR: 313 case PARM_CONSTR: 314 case CONJ_CONSTR: 315 case DISJ_CONSTR: 316 return true; 317 default: 318 gcc_unreachable (); 319 } 320 } 321 322 /* Returns true if any constraints in T are not atomic. */ 323 324 bool 325 any_non_atomic_constraints_p (term_list& t) 326 { 327 return any_p (t.begin(), t.end(), non_atomic_constraint_p); 328 } 329 330 /*--------------------------------------------------------------------------- 331 Proof validations 332 ---------------------------------------------------------------------------*/ 333 334 enum proof_result 335 { 336 invalid, 337 valid, 338 undecided 339 }; 340 341 proof_result check_term (term_list&, tree); 342 343 344 proof_result 345 analyze_atom (term_list& ts, tree t) 346 { 347 /* FIXME: Hook into special cases, if any. */ 348 /* 349 term_list::iterator iter = ts.begin(); 350 term_list::iterator end = ts.end(); 351 while (iter != end) 352 { 353 ++iter; 354 } 355 */ 356 357 if (non_atomic_constraint_p (t)) 358 return undecided; 359 if (any_non_atomic_constraints_p (ts)) 360 return undecided; 361 return invalid; 362 } 363 364 /* Search for a pack expansion in the list of assumptions that would 365 make this expansion valid. */ 366 367 proof_result 368 analyze_pack (term_list& ts, tree t) 369 { 370 tree c1 = normalize_expression (PACK_EXPANSION_PATTERN (t)); 371 term_list::iterator iter = ts.begin(); 372 term_list::iterator end = ts.end(); 373 while (iter != end) 374 { 375 if (TREE_CODE (*iter) == TREE_CODE (t)) 376 { 377 tree c2 = normalize_expression (PACK_EXPANSION_PATTERN (*iter)); 378 if (prove_implication (c2, c1)) 379 return valid; 380 else 381 return invalid; 382 } 383 ++iter; 384 } 385 return invalid; 386 } 387 388 /* Search for concept checks in TS that we know subsume T. */ 389 390 proof_result 391 search_known_subsumptions (term_list& ts, tree t) 392 { 393 for (term_list::iterator i = ts.begin(); i != ts.end(); ++i) 394 if (TREE_CODE (*i) == CHECK_CONSTR) 395 { 396 if (bool* b = lookup_subsumption_result (*i, t)) 397 return *b ? valid : invalid; 398 } 399 return undecided; 400 } 401 402 /* Determine if the terms in TS provide sufficient support for proving 403 the proposition T. If any term in TS is a concept check that is known 404 to subsume T, then the proof is valid. Otherwise, we have to expand T 405 and continue searching for support. */ 406 407 proof_result 408 analyze_check (term_list& ts, tree t) 409 { 410 proof_result r = search_known_subsumptions (ts, t); 411 if (r != undecided) 412 return r; 413 414 tree tmpl = CHECK_CONSTR_CONCEPT (t); 415 tree args = CHECK_CONSTR_ARGS (t); 416 tree c = expand_concept (tmpl, args); 417 return check_term (ts, c); 418 } 419 420 /* Recursively check constraints of the parameterized constraint. */ 421 422 proof_result 423 analyze_parameterized (term_list& ts, tree t) 424 { 425 return check_term (ts, PARM_CONSTR_OPERAND (t)); 426 } 427 428 proof_result 429 analyze_conjunction (term_list& ts, tree t) 430 { 431 proof_result r = check_term (ts, TREE_OPERAND (t, 0)); 432 if (r == invalid || r == undecided) 433 return r; 434 return check_term (ts, TREE_OPERAND (t, 1)); 435 } 436 437 proof_result 438 analyze_disjunction (term_list& ts, tree t) 439 { 440 proof_result r = check_term (ts, TREE_OPERAND (t, 0)); 441 if (r == valid) 442 return r; 443 return check_term (ts, TREE_OPERAND (t, 1)); 444 } 445 446 proof_result 447 analyze_term (term_list& ts, tree t) 448 { 449 switch (TREE_CODE (t)) 450 { 451 case CHECK_CONSTR: 452 return analyze_check (ts, t); 453 454 case PARM_CONSTR: 455 return analyze_parameterized (ts, t); 456 457 case CONJ_CONSTR: 458 return analyze_conjunction (ts, t); 459 case DISJ_CONSTR: 460 return analyze_disjunction (ts, t); 461 462 case PRED_CONSTR: 463 case EXPR_CONSTR: 464 case TYPE_CONSTR: 465 case ICONV_CONSTR: 466 case DEDUCT_CONSTR: 467 case EXCEPT_CONSTR: 468 return analyze_atom (ts, t); 469 470 case EXPR_PACK_EXPANSION: 471 return analyze_pack (ts, t); 472 473 case ERROR_MARK: 474 /* Encountering an error anywhere in a constraint invalidates 475 the proof, since the constraint is ill-formed. */ 476 return invalid; 477 default: 478 gcc_unreachable (); 479 } 480 } 481 482 /* Check if a single term can be proven from a set of assumptions. 483 If the proof is not valid, then it is incomplete when either 484 the given term is non-atomic or any term in the list of assumptions 485 is not-atomic. */ 486 487 proof_result 488 check_term (term_list& ts, tree t) 489 { 490 /* Try the easy way; search for an equivalent term. */ 491 if (ts.includes (t)) 492 return valid; 493 494 /* The hard way; actually consider what the term means. */ 495 return analyze_term (ts, t); 496 } 497 498 /* Check to see if any term is proven by the assumptions in the 499 proof goal. The proof is valid if the proof of any term is valid. 500 If validity cannot be determined, but any particular 501 check was undecided, then this goal is undecided. */ 502 503 proof_result 504 check_goal (proof_goal& g) 505 { 506 term_list::iterator iter = g.conclusions.begin (); 507 term_list::iterator end = g.conclusions.end (); 508 bool incomplete = false; 509 while (iter != end) 510 { 511 proof_result r = check_term (g.assumptions, *iter); 512 if (r == valid) 513 return r; 514 if (r == undecided) 515 incomplete = true; 516 ++iter; 517 } 518 519 /* Was the proof complete? */ 520 if (incomplete) 521 return undecided; 522 else 523 return invalid; 524 } 525 526 /* Check if the the proof is valid. This is the case when all 527 goals can be discharged. If any goal is invalid, then the 528 entire proof is invalid. Otherwise, the proof is undecided. */ 529 530 proof_result 531 check_proof (proof_state& p) 532 { 533 proof_state::iterator iter = p.begin(); 534 proof_state::iterator end = p.end(); 535 while (iter != end) 536 { 537 proof_result r = check_goal (*iter); 538 if (r == invalid) 539 return r; 540 if (r == valid) 541 iter = p.discharge (iter); 542 else 543 ++iter; 544 } 545 546 /* If all goals are discharged, then the proof is valid. */ 547 if (p.empty()) 548 return valid; 549 else 550 return undecided; 551 } 552 553 /*--------------------------------------------------------------------------- 554 Left logical rules 555 ---------------------------------------------------------------------------*/ 556 557 term_list::iterator 558 load_check_assumption (term_list& ts, term_list::iterator i) 559 { 560 tree decl = CHECK_CONSTR_CONCEPT (*i); 561 tree tmpl = DECL_TI_TEMPLATE (decl); 562 tree args = CHECK_CONSTR_ARGS (*i); 563 return ts.replace(i, expand_concept (tmpl, args)); 564 } 565 566 term_list::iterator 567 load_parameterized_assumption (term_list& ts, term_list::iterator i) 568 { 569 return ts.replace(i, PARM_CONSTR_OPERAND(*i)); 570 } 571 572 term_list::iterator 573 load_conjunction_assumption (term_list& ts, term_list::iterator i) 574 { 575 tree t1 = TREE_OPERAND (*i, 0); 576 tree t2 = TREE_OPERAND (*i, 1); 577 return ts.replace(i, t1, t2); 578 } 579 580 /* Examine the terms in the list, and apply left-logical rules to move 581 terms into the set of assumptions. */ 582 583 void 584 load_assumptions (proof_goal& g) 585 { 586 term_list::iterator iter = g.assumptions.begin(); 587 term_list::iterator end = g.assumptions.end(); 588 while (iter != end) 589 { 590 switch (TREE_CODE (*iter)) 591 { 592 case CHECK_CONSTR: 593 iter = load_check_assumption (g.assumptions, iter); 594 break; 595 case PARM_CONSTR: 596 iter = load_parameterized_assumption (g.assumptions, iter); 597 break; 598 case CONJ_CONSTR: 599 iter = load_conjunction_assumption (g.assumptions, iter); 600 break; 601 default: 602 ++iter; 603 break; 604 } 605 } 606 } 607 608 /* In each subgoal, load constraints into the assumption set. */ 609 610 void 611 load_assumptions(proof_state& p) 612 { 613 proof_state::iterator iter = p.begin(); 614 while (iter != p.end()) 615 { 616 load_assumptions (*iter); 617 ++iter; 618 } 619 } 620 621 void 622 explode_disjunction (proof_state& p, proof_state::iterator gi, term_list::iterator ti1) 623 { 624 tree t1 = TREE_OPERAND (*ti1, 0); 625 tree t2 = TREE_OPERAND (*ti1, 1); 626 627 /* Erase the current term from the goal. */ 628 proof_goal& g1 = *gi; 629 proof_goal& g2 = *p.branch (gi); 630 631 /* Get an iterator to the equivalent position in th enew goal. */ 632 int n = std::distance (g1.assumptions.begin (), ti1); 633 term_list::iterator ti2 = g2.assumptions.begin (); 634 std::advance (ti2, n); 635 636 /* Replace the disjunction in both branches. */ 637 g1.assumptions.replace (ti1, t1); 638 g2.assumptions.replace (ti2, t2); 639 } 640 641 642 /* Search the assumptions of the goal for the first disjunction. */ 643 644 bool 645 explode_goal (proof_state& p, proof_state::iterator gi) 646 { 647 term_list& ts = gi->assumptions; 648 term_list::iterator ti = ts.begin(); 649 term_list::iterator end = ts.end(); 650 while (ti != end) 651 { 652 if (TREE_CODE (*ti) == DISJ_CONSTR) 653 { 654 explode_disjunction (p, gi, ti); 655 return true; 656 } 657 else ++ti; 658 } 659 return false; 660 } 661 662 /* Search for the first goal with a disjunction, and then branch 663 creating a clone of that subgoal. */ 664 665 void 666 explode_assumptions (proof_state& p) 667 { 668 proof_state::iterator iter = p.begin(); 669 proof_state::iterator end = p.end(); 670 while (iter != end) 671 { 672 if (explode_goal (p, iter)) 673 return; 674 ++iter; 675 } 676 } 677 678 679 /*--------------------------------------------------------------------------- 680 Right logical rules 681 ---------------------------------------------------------------------------*/ 682 683 term_list::iterator 684 load_disjunction_conclusion (term_list& g, term_list::iterator i) 685 { 686 tree t1 = TREE_OPERAND (*i, 0); 687 tree t2 = TREE_OPERAND (*i, 1); 688 return g.replace(i, t1, t2); 689 } 690 691 /* Apply logical rules to the right hand side. This will load the 692 conclusion set with all tpp-level disjunctions. */ 693 694 void 695 load_conclusions (proof_goal& g) 696 { 697 term_list::iterator iter = g.conclusions.begin(); 698 term_list::iterator end = g.conclusions.end(); 699 while (iter != end) 700 { 701 if (TREE_CODE (*iter) == DISJ_CONSTR) 702 iter = load_disjunction_conclusion (g.conclusions, iter); 703 else 704 ++iter; 705 } 706 } 707 708 void 709 load_conclusions (proof_state& p) 710 { 711 proof_state::iterator iter = p.begin(); 712 while (iter != p.end()) 713 { 714 load_conclusions (*iter); 715 ++iter; 716 } 717 } 718 719 720 /*--------------------------------------------------------------------------- 721 High-level proof tactics 722 ---------------------------------------------------------------------------*/ 723 724 /* Given two constraints A and C, try to derive a proof that 725 A implies C. */ 726 727 bool 728 prove_implication (tree a, tree c) 729 { 730 /* Quick accept. */ 731 if (cp_tree_equal (a, c)) 732 return true; 733 734 /* Build the initial proof state. */ 735 proof_state proof; 736 proof_goal& goal = proof.front(); 737 goal.assumptions.push_back(a); 738 goal.conclusions.push_back(c); 739 740 /* Perform an initial right-expansion in the off-chance that the right 741 hand side contains disjunctions. */ 742 load_conclusions (proof); 743 744 int step_max = 1 << 10; 745 int step_count = 0; /* FIXME: We shouldn't have this. */ 746 std::size_t branch_limit = 1024; /* FIXME: This needs to be configurable. */ 747 while (step_count < step_max && proof.size() < branch_limit) 748 { 749 /* Determine if we can prove that the assumptions entail the 750 conclusions. If so, we're done. */ 751 load_assumptions (proof); 752 753 /* Can we solve the proof based on this? */ 754 proof_result r = check_proof (proof); 755 if (r != undecided) 756 return r == valid; 757 758 /* If not, then we need to dig into disjunctions. */ 759 explode_assumptions (proof); 760 761 ++step_count; 762 } 763 764 if (step_count == step_max) 765 error ("subsumption failed to resolve"); 766 767 if (proof.size() == branch_limit) 768 error ("exceeded maximum number of branches"); 769 770 return false; 771 } 772 773 /* Returns true if the LEFT constraint subsume the RIGHT constraints. 774 This is done by deriving a proof of the conclusions on the RIGHT 775 from the assumptions on the LEFT assumptions. */ 776 777 bool 778 subsumes_constraints_nonnull (tree left, tree right) 779 { 780 gcc_assert (check_constraint_info (left)); 781 gcc_assert (check_constraint_info (right)); 782 783 auto_timevar time (TV_CONSTRAINT_SUB); 784 tree a = CI_ASSOCIATED_CONSTRAINTS (left); 785 tree c = CI_ASSOCIATED_CONSTRAINTS (right); 786 return prove_implication (a, c); 787 } 788 789 } /* namespace */ 790 791 /* Returns true if the LEFT constraints subsume the RIGHT 792 constraints. */ 793 794 bool 795 subsumes (tree left, tree right) 796 { 797 if (left == right) 798 return true; 799 if (!left) 800 return false; 801 if (!right) 802 return true; 803 return subsumes_constraints_nonnull (left, right); 804 } 805