gcc/cp/logic.cc

   1 /* Derivation and subsumption rules for constraints.
   2    Copyright (C) 2013-2016 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 "hash-set.h"
  27 #include "machmode.h"
  28 #include "vec.h"
  29 #include "double-int.h"
  30 #include "input.h"
  31 #include "alias.h"
  32 #include "symtab.h"
  33 #include "wide-int.h"
  34 #include "inchash.h"
  35 #include "tree.h"
  36 #include "stringpool.h"
  37 #include "attribs.h"
  38 #include "intl.h"
  39 #include "flags.h"
  40 #include "cp-tree.h"
  41 #include "c-family/c-common.h"
  42 #include "c-family/c-objc.h"
  43 #include "cp-objcp-common.h"
  44 #include "tree-inline.h"
  45 #include "decl.h"
  46 #include "toplev.h"
  47 #include "type-utils.h"
  48
  49 namespace {
  50
  51 // Helper algorithms
  52
  53 // Increment iter distance(first, last) times.
  54 template<typename I1, typename I2, typename I3>
  55   I1 next_by_distance (I1 iter, I2 first, I3 last)
  56   {
  57     for ( ; first != last; ++first, ++iter)
  58       ;
  59     return iter;
  60   }
  61
  62 /*---------------------------------------------------------------------------
  63                            Proof state
  64 ---------------------------------------------------------------------------*/
  65
  66 /* A term list is a list of atomic constraints. It is used
  67    to maintain the lists of assumptions and conclusions in a
  68    proof goal.
  69
  70    Each term list maintains an iterator that refers to the current
  71    term. This can be used by various tactics to support iteration
  72    and stateful manipulation of the list. */
  73 struct term_list : std::list<tree>
  74 {
  75   term_list ();
  76   term_list (const term_list &x);
  77   term_list& operator= (const term_list &x);
  78
  79   tree       current_term ()       { return *current; }
  80   const_tree current_term () const { return *current; }
  81
  82
  83   void insert (tree t);
  84   tree erase ();
  85
  86   void start ();
  87   void next ();
  88   bool done() const;
  89
  90   iterator current;
  91 };
  92
  93 inline
  94 term_list::term_list ()
  95   : std::list<tree> (), current (end ())
  96 { }
  97
  98 inline
  99 term_list::term_list (const term_list &x)
 100   : std::list<tree> (x)
 101   , current (next_by_distance (begin (), x.begin (), x.current))
 102 { }
 103
 104 inline term_list&
 105 term_list::operator= (const term_list &x)
 106 {
 107   std::list<tree>::operator=(x);
 108   current = next_by_distance (begin (), x.begin (), x.current);
 109   return *this;
 110 }
 111
 112 /* Try saving the term T into the list of terms. If
 113    T is already in the list of terms, then no action is
 114    performed. Otherwise, insert T before the current
 115    position, making this term current.
 116
 117    Note that not inserting terms is an optimization
 118    that corresponds to the structural rule of
 119    contraction.
 120
 121    NOTE: With the contraction rule, this data structure
 122    would be more efficiently represented as an ordered set
 123    or hash set.  */
 124 void
 125 term_list::insert (tree t)
 126 {
 127   /* Search the current term list. If there is already
 128      a matching term, do not add the new one.  */
 129   for (iterator i = begin(); i != end(); ++i)
 130     if (cp_tree_equal (*i, t))
 131       return;
 132
 133   current = std::list<tree>::insert (current, t);
 134 }
 135
 136 /* Remove the current term from the list, repositioning to
 137    the term following the removed term. Note that the new
 138    position could be past the end of the list.
 139
 140    The removed term is returned. */
 141 inline tree
 142 term_list::erase ()
 143 {
 144   tree t = *current;
 145   current = std::list<tree>::erase (current);
 146   return t;
 147 }
 148
 149 /* Initialize the current term to the first in the list. */
 150 inline void
 151 term_list::start ()
 152 {
 153   current = begin ();
 154 }
 155
 156 /* Advance to the next term in the list. */
 157 inline void
 158 term_list::next ()
 159 {
 160   ++current;
 161 }
 162
 163 /* Returns true when the current position is past the end. */
 164 inline bool
 165 term_list::done () const
 166 {
 167   return current == end ();
 168 }
 169
 170
 171 /* A goal (or subgoal) models a sequent of the form
 172    'A |- C' where A and C are lists of assumptions and
 173    conclusions written as propositions in the constraint
 174    language (i.e., lists of trees).
 175 */
 176 struct proof_goal
 177 {
 178   term_list assumptions;
 179   term_list conclusions;
 180 };
 181
 182 /* A proof state owns a list of goals and tracks the
 183    current sub-goal. The class also provides facilities
 184    for managing subgoals and constructing term lists. */
 185 struct proof_state : std::list<proof_goal>
 186 {
 187   proof_state ();
 188
 189   iterator branch (iterator i);
 190 };
 191
 192 /* An alias for proof state iterators. */
 193 typedef proof_state::iterator goal_iterator;
 194
 195 /* Initialize the state with a single empty goal,
 196    and set that goal as the current subgoal. */
 197 inline
 198 proof_state::proof_state ()
 199   : std::list<proof_goal> (1)
 200 { }
 201
 202
 203 /* Branch the current goal by creating a new subgoal,
 204    returning a reference to // the new object. This does
 205    not update the current goal. */
 206 inline proof_state::iterator
 207 proof_state::branch (iterator i)
 208 {
 209   gcc_assert (i != end());
 210   proof_goal& g = *i;
 211   return insert (++i, g);
 212 }
 213
 214 /*---------------------------------------------------------------------------
 215                            Logical rules
 216 ---------------------------------------------------------------------------*/
 217
 218 /*These functions modify the current state and goal by decomposing
 219   logical expressions using the logical rules of sequent calculus for
 220   first order logic.
 221
 222   Note that in each decomposition rule, the term T has been erased
 223   from term list before the specific rule is applied. */
 224
 225 /* The left logical rule for conjunction adds both operands
 226    to the current set of constraints. */
 227 void
 228 left_conjunction (proof_state &, goal_iterator i, tree t)
 229 {
 230   gcc_assert (TREE_CODE (t) == CONJ_CONSTR);
 231
 232   /* Insert the operands into the current branch. Note that the
 233      final order of insertion is left-to-right. */
 234   term_list &l = i->assumptions;
 235   l.insert (TREE_OPERAND (t, 1));
 236   l.insert (TREE_OPERAND (t, 0));
 237 }
 238
 239 /* The left logical rule for disjunction creates a new goal,
 240    adding the first operand to the original set of
 241    constraints and the second operand to the new set
 242    of constraints. */
 243 void
 244 left_disjunction (proof_state &s, goal_iterator i, tree t)
 245 {
 246   gcc_assert (TREE_CODE (t) == DISJ_CONSTR);
 247
 248   /* Branch the current subgoal. */
 249   goal_iterator j = s.branch (i);
 250   term_list &l1 = i->assumptions;
 251   term_list &l2 = j->assumptions;
 252
 253   /* Insert operands into the different branches. */
 254   l1.insert (TREE_OPERAND (t, 0));
 255   l2.insert (TREE_OPERAND (t, 1));
 256 }
 257
 258 /* The left logical rules for parameterized constraints
 259    adds its operand to the current goal. The list of
 260    parameters are effectively discarded. */
 261 void
 262 left_parameterized_constraint (proof_state &, goal_iterator i, tree t)
 263 {
 264   gcc_assert (TREE_CODE (t) == PARM_CONSTR);
 265   term_list &l = i->assumptions;
 266   l.insert (PARM_CONSTR_OPERAND (t));
 267 }
 268
 269 /*---------------------------------------------------------------------------
 270                            Decomposition
 271 ---------------------------------------------------------------------------*/
 272
 273 /* The following algorithms decompose expressions into sets of
 274    atomic propositions. In terms of the sequent calculus, these
 275    functions exercise the logical rules only.
 276
 277    This is equivalent, for the purpose of determining subsumption,
 278    to rewriting a constraint in disjunctive normal form. It also
 279    allows the resulting assumptions to be used as declarations
 280    for the purpose of separate checking. */
 281
 282 /* Apply the left logical rules to the proof state. */
 283 void
 284 decompose_left_term (proof_state &s, goal_iterator i)
 285 {
 286   term_list &l = i->assumptions;
 287   tree t = l.current_term ();
 288   switch (TREE_CODE (t))
 289     {
 290     case CONJ_CONSTR:
 291       left_conjunction (s, i, l.erase ());
 292       break;
 293     case DISJ_CONSTR:
 294       left_disjunction (s, i, l.erase ());
 295       break;
 296     case PARM_CONSTR:
 297       left_parameterized_constraint (s, i, l.erase ());
 298       break;
 299     default:
 300       l.next ();
 301       break;
 302     }
 303 }
 304
 305 /* Apply the left logical rules of the sequent calculus
 306    until the current goal is fully decomposed into atomic
 307    constraints. */
 308 void
 309 decompose_left_goal (proof_state &s, goal_iterator i)
 310 {
 311   term_list& l = i->assumptions;
 312   l.start ();
 313   while (!l.done ())
 314     decompose_left_term (s, i);
 315 }
 316
 317 /* Apply the left logical rules of the sequent calculus
 318    until the antecedents are fully decomposed into atomic
 319    constraints. */
 320 void
 321 decompose_left (proof_state& s)
 322 {
 323   goal_iterator iter = s.begin ();
 324   goal_iterator end = s.end ();
 325   for ( ; iter != end; ++iter)
 326     decompose_left_goal (s, iter);
 327 }
 328
 329 /* Returns a vector of terms from the term list L. */
 330 tree
 331 extract_terms (term_list& l)
 332 {
 333   tree result = make_tree_vec (l.size());
 334   term_list::iterator iter = l.begin();
 335   term_list::iterator end = l.end();
 336   for (int n = 0; iter != end; ++iter, ++n)
 337     TREE_VEC_ELT (result, n) = *iter;
 338   return result;
 339 }
 340
 341 /* Extract the assumptions from the proof state S
 342    as a vector of vectors of atomic constraints. */
 343 inline tree
 344 extract_assumptions (proof_state& s)
 345 {
 346   tree result = make_tree_vec (s.size ());
 347   goal_iterator iter = s.begin ();
 348   goal_iterator end = s.end ();
 349   for (int n = 0; iter != end; ++iter, ++n)
 350     TREE_VEC_ELT (result, n) = extract_terms (iter->assumptions);
 351   return result;
 352 }
 353
 354 } // namespace
 355
 356 /* Decompose the required expression T into a constraint set: a
 357    vector of vectors containing only atomic propositions. If T is
 358    invalid, return an error. */
 359 tree
 360 decompose_assumptions (tree t)
 361 {
 362   if (!t || t == error_mark_node)
 363     return t;
 364
 365   /* Create a proof state, and insert T as the sole assumption. */
 366   proof_state s;
 367   term_list &l = s.begin ()->assumptions;
 368   l.insert (t);
 369
 370   /* Decompose the expression into a constraint set, and then
 371      extract the terms for the AST. */
 372   decompose_left (s);
 373   return extract_assumptions (s);
 374 }
 375
 376
 377 /*---------------------------------------------------------------------------
 378                            Subsumption Rules
 379 ---------------------------------------------------------------------------*/
 380
 381 namespace {
 382
 383 bool subsumes_constraint (tree, tree);
 384 bool subsumes_conjunction (tree, tree);
 385 bool subsumes_disjunction (tree, tree);
 386 bool subsumes_parameterized_constraint (tree, tree);
 387 bool subsumes_atomic_constraint (tree, tree);
 388
 389 /* Returns true if the assumption A matches the conclusion C. This
 390    is generally the case when A and C have the same syntax.
 391
 392    NOTE: There will be specialized matching rules to accommodate
 393    type equivalence, conversion, inheritance, etc. But this is not
 394    in the current concepts draft. */
 395 inline bool
 396 match_terms (tree a, tree c)
 397 {
 398   return cp_tree_equal (a, c);
 399 }
 400
 401 /* Returns true if the list of assumptions AS subsumes the atomic
 402    proposition C. This is the case when we can find a proposition
 403   in AS that entails the conclusion C. */
 404 bool
 405 subsumes_atomic_constraint (tree as, tree c)
 406 {
 407   for (int i = 0; i < TREE_VEC_LENGTH (as); ++i)
 408     if (match_terms (TREE_VEC_ELT (as, i), c))
 409       return true;
 410   return false;
 411 }
 412
 413 /* Returns true when both operands of C are subsumed by the
 414    assumptions AS. */
 415 inline bool
 416 subsumes_conjunction (tree as, tree c)
 417 {
 418   tree l = TREE_OPERAND (c, 0);
 419   tree r = TREE_OPERAND (c, 1);
 420   return subsumes_constraint (as, l) && subsumes_constraint (as, r);
 421 }
 422
 423 /* Returns true when either operand of C is subsumed by the
 424    assumptions AS. */
 425 inline bool
 426 subsumes_disjunction (tree as, tree c)
 427 {
 428   tree l = TREE_OPERAND (c, 0);
 429   tree r = TREE_OPERAND (c, 1);
 430   return subsumes_constraint (as, l) || subsumes_constraint (as, r);
 431 }
 432
 433 /* Returns true when the operand of C is subsumed by the
 434    assumptions in AS. The parameters are not considered in
 435    the subsumption rules. */
 436 bool
 437 subsumes_parameterized_constraint (tree as, tree c)
 438 {
 439   tree t = PARM_CONSTR_OPERAND (c);
 440   return subsumes_constraint (as, t);
 441 }
 442
 443
 444 /* Returns true when the list of assumptions AS subsumes the
 445    concluded proposition C. This is a simple recursive descent
 446    on C, matching against propositions in the assumption list AS. */
 447 bool
 448 subsumes_constraint (tree as, tree c)
 449 {
 450   switch (TREE_CODE (c))
 451     {
 452     case CONJ_CONSTR:
 453       return subsumes_conjunction (as, c);
 454     case DISJ_CONSTR:
 455       return subsumes_disjunction (as, c);
 456     case PARM_CONSTR:
 457       return subsumes_parameterized_constraint (as, c);
 458     default:
 459       return subsumes_atomic_constraint (as, c);
 460     }
 461 }
 462
 463 /* Returns true if the LEFT constraints subsume the RIGHT constraints.
 464    This is done by checking that the RIGHT requirements follow from
 465    each of the LEFT subgoals. */
 466 bool
 467 subsumes_constraints_nonnull (tree left, tree right)
 468 {
 469   gcc_assert (check_constraint_info (left));
 470   gcc_assert (check_constraint_info (right));
 471
 472   /* Check that the required expression in RIGHT is subsumed by each
 473      subgoal in the assumptions of LEFT. */
 474   tree as = CI_ASSUMPTIONS (left);
 475   tree c = CI_NORMALIZED_CONSTRAINTS (right);
 476   for (int i = 0; i < TREE_VEC_LENGTH (as); ++i)
 477     if (!subsumes_constraint (TREE_VEC_ELT (as, i), c))
 478       return false;
 479   return true;
 480 }
 481
 482 } /* namespace */
 483
 484 /* Returns true if the LEFT constraints subsume the RIGHT
 485    constraints. */
 486 bool
 487 subsumes (tree left, tree right)
 488 {
 489   if (left == right)
 490     return true;
 491   if (!left)
 492     return false;
 493   if (!right)
 494     return true;
 495   return subsumes_constraints_nonnull (left, right);
 496 }