gcc/cp/logic.cc

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