gcc/cp/logic.cc

   1 /* Derivation and subsumption rules for constraints.
   2    Copyright (C) 2013-2017 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 }