LCOV - code coverage report
Current view: top level - gcc/cp - logic.cc (source / functions) Hit Total Coverage
Test: gcc.info Lines: 189 299 63.2 %
Date: 2020-03-28 11:57:23 Functions: 19 30 63.3 %
Legend: Lines: hit not hit | Branches: + taken - not taken # not executed Branches: 0 0 -

           Branch data     Line data    Source code
       1                 :            : /* Derivation and subsumption rules for constraints.
       2                 :            :    Copyright (C) 2013-2020 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                 :            : /* Hash functions for atomic constrains.  */
      51                 :            : 
      52                 :            : struct constraint_hash : default_hash_traits<tree>
      53                 :            : {
      54                 :    2212860 :   static hashval_t hash (tree t)
      55                 :            :   {
      56                 :    2212860 :     return hash_atomic_constraint (t);
      57                 :            :   }
      58                 :            : 
      59                 :    3144040 :   static bool equal (tree t1, tree t2)
      60                 :            :   {
      61                 :    3144040 :     return atomic_constraints_identical_p (t1, t2);
      62                 :            :   }
      63                 :            : };
      64                 :            : 
      65                 :            : /* A conjunctive or disjunctive clause.
      66                 :            : 
      67                 :            :    Each clause maintains an iterator that refers to the current
      68                 :            :    term, which is used in the linear decomposition of a formula
      69                 :            :    into CNF or DNF.  */
      70                 :            : 
      71                 :            : struct clause
      72                 :            : {
      73                 :            :   typedef std::list<tree>::iterator iterator;
      74                 :            :   typedef std::list<tree>::const_iterator const_iterator;
      75                 :            : 
      76                 :            :   /* Initialize a clause with an initial term.  */
      77                 :            : 
      78                 :       1511 :   clause (tree t)
      79                 :       1511 :   {
      80                 :       1511 :     m_terms.push_back (t);
      81                 :       1511 :     if (TREE_CODE (t) == ATOMIC_CONSTR)
      82                 :        691 :       m_set.add (t);
      83                 :            : 
      84                 :       1511 :     m_current = m_terms.begin ();
      85                 :       1511 :   }
      86                 :            : 
      87                 :            :   /* Create a copy of the current term. The current
      88                 :            :      iterator is set to point to the same position in the
      89                 :            :      copied list of terms.  */
      90                 :            : 
      91                 :       1511 :   clause (clause const& c)
      92                 :       3022 :     : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
      93                 :            :   {
      94                 :       1511 :     std::advance (m_current, std::distance (c.begin (), c.current ()));
      95                 :       1511 :   }
      96                 :            : 
      97                 :            :   /* Returns true when all terms are atoms.  */
      98                 :            : 
      99                 :     405163 :   bool done () const
     100                 :            :   {
     101                 :     405163 :     return m_current == end ();
     102                 :            :   }
     103                 :            : 
     104                 :            :   /* Advance to the next term.  */
     105                 :            : 
     106                 :      52137 :   void advance ()
     107                 :            :   {
     108                 :          0 :     gcc_assert (!done ());
     109                 :      52137 :     ++m_current;
     110                 :            :   }
     111                 :            : 
     112                 :            :   /* Replaces the current term at position ITER with T.  If
     113                 :            :      T is an atomic constraint that already appears in the
     114                 :            :      clause, remove but do not replace ITER. Returns a pair
     115                 :            :      containing an iterator to the replace object or past
     116                 :            :      the erased object and a boolean value which is true if
     117                 :            :      an object was erased.  */
     118                 :            : 
     119                 :     299378 :   std::pair<iterator, bool> replace (iterator iter, tree t)
     120                 :            :   {
     121                 :     299378 :     gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
     122                 :     299378 :     if (TREE_CODE (t) == ATOMIC_CONSTR)
     123                 :            :       {
     124                 :     143125 :         if (m_set.add (t))
     125                 :     242168 :           return std::make_pair (m_terms.erase (iter), true);
     126                 :            :       }
     127                 :     178294 :     *iter = t;
     128                 :     178294 :     return std::make_pair (iter, false);
     129                 :            :   }
     130                 :            : 
     131                 :            :   /* Inserts T before ITER in the list of terms.  If T has 
     132                 :            :      already is an atomic constraint that already appears in
     133                 :            :      the clause, no action is taken, and the current iterator
     134                 :            :      is returned. Returns a pair of an iterator to the inserted
     135                 :            :      object or ITER if no insertion occurred and a boolean
     136                 :            :      value which is true if an object was inserted.  */
     137                 :            : 
     138                 :     299378 :   std::pair<iterator, bool> insert (iterator iter, tree t)
     139                 :            :   {
     140                 :     299378 :     if (TREE_CODE (t) == ATOMIC_CONSTR)
     141                 :            :     {
     142                 :     157073 :       if (m_set.add (t))
     143                 :     127668 :         return std::make_pair (iter, false);
     144                 :            :     }
     145                 :     171710 :     return std::make_pair (m_terms.insert (iter, t), true);
     146                 :            :   }
     147                 :            : 
     148                 :            :   /* Replaces the current term with T. In the case where the
     149                 :            :      current term is erased (because T is redundant), update
     150                 :            :      the position of the current term to the next term.  */
     151                 :            : 
     152                 :          0 :   void replace (tree t)
     153                 :            :   {
     154                 :          0 :     m_current = replace (m_current, t).first;
     155                 :            :   }
     156                 :            : 
     157                 :            :   /* Replace the current term with T1 and T2, in that order.  */
     158                 :            : 
     159                 :     299378 :   void replace (tree t1, tree t2)
     160                 :            :   {
     161                 :            :     /* Replace the current term with t1. Ensure that iter points
     162                 :            :        to the term before which t2 will be inserted.  Update the
     163                 :            :        current term as needed.  */
     164                 :     299378 :     std::pair<iterator, bool> rep = replace (m_current, t1);
     165                 :     299378 :     if (rep.second)
     166                 :     121084 :       m_current = rep.first;
     167                 :            :     else
     168                 :     178294 :       ++rep.first;
     169                 :            : 
     170                 :            :     /* Insert the t2. Make this the current term if we erased
     171                 :            :        the prior term.  */
     172                 :     299378 :     std::pair<iterator, bool> ins = insert (rep.first, t2);
     173                 :     299378 :     if (rep.second && ins.second)
     174                 :      28994 :       m_current = ins.first;
     175                 :     299378 :   }
     176                 :            : 
     177                 :            :   /* Returns true if the clause contains the term T.  */
     178                 :            : 
     179                 :      20988 :   bool contains (tree t)
     180                 :            :   {
     181                 :      20988 :     gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
     182                 :      20988 :     return m_set.contains (t);
     183                 :            :   }
     184                 :            : 
     185                 :            : 
     186                 :            :   /* Returns an iterator to the first clause in the formula.  */
     187                 :            : 
     188                 :          0 :   iterator begin ()
     189                 :            :   {
     190                 :          0 :     return m_terms.begin ();
     191                 :            :   }
     192                 :            : 
     193                 :            :   /* Returns an iterator to the first clause in the formula.  */
     194                 :            : 
     195                 :       1511 :   const_iterator begin () const
     196                 :            :   {
     197                 :       1511 :     return m_terms.begin ();
     198                 :            :   }
     199                 :            : 
     200                 :            :   /* Returns an iterator past the last clause in the formula.  */
     201                 :            : 
     202                 :          0 :   iterator end ()
     203                 :            :   {
     204                 :          0 :     return m_terms.end ();
     205                 :            :   }
     206                 :            : 
     207                 :            :   /* Returns an iterator past the last clause in the formula.  */
     208                 :            : 
     209                 :     405163 :   const_iterator end () const
     210                 :            :   {
     211                 :     405163 :     return m_terms.end ();
     212                 :            :   }
     213                 :            : 
     214                 :            :   /* Returns the current iterator.  */
     215                 :            : 
     216                 :     353026 :   const_iterator current () const
     217                 :            :   {
     218                 :       1511 :     return m_current;
     219                 :            :   }
     220                 :            : 
     221                 :            :   std::list<tree> m_terms; /* The list of terms.  */
     222                 :            :   hash_set<tree, false, constraint_hash> m_set; /* The set of atomic constraints.  */
     223                 :            :   iterator m_current; /* The current term.  */
     224                 :            : };
     225                 :            : 
     226                 :            : 
     227                 :            : /* A proof state owns a list of goals and tracks the
     228                 :            :    current sub-goal. The class also provides facilities
     229                 :            :    for managing subgoals and constructing term lists. */
     230                 :            : 
     231                 :       3022 : struct formula
     232                 :            : {
     233                 :            :   typedef std::list<clause>::iterator iterator;
     234                 :            :   typedef std::list<clause>::const_iterator const_iterator;
     235                 :            : 
     236                 :            :   /* Construct a formula with an initial formula in a
     237                 :            :      single clause.  */
     238                 :            : 
     239                 :       1511 :   formula (tree t)
     240                 :       1511 :   {
     241                 :            :     /* This should call emplace_back(). There's an extra copy being
     242                 :            :        invoked by using push_back().  */
     243                 :       1511 :     m_clauses.push_back (t);
     244                 :       1511 :     m_current = m_clauses.begin ();
     245                 :       1511 :   }
     246                 :            : 
     247                 :            :   /* Returns true when all clauses are atomic.  */
     248                 :       4533 :   bool done () const
     249                 :            :   {
     250                 :       4533 :     return m_current == end ();
     251                 :            :   }
     252                 :            : 
     253                 :            :   /* Advance to the next term.  */
     254                 :       1511 :   void advance ()
     255                 :            :   {
     256                 :          0 :     gcc_assert (!done ());
     257                 :       1511 :     ++m_current;
     258                 :            :   }
     259                 :            : 
     260                 :            :   /* Insert a copy of clause into the formula. This corresponds
     261                 :            :      to a distribution of one logical operation over the other.  */
     262                 :            : 
     263                 :          0 :   clause& branch ()
     264                 :            :   {
     265                 :          0 :     gcc_assert (!done ());
     266                 :          0 :     m_clauses.push_back (*m_current);
     267                 :          0 :     return m_clauses.back ();
     268                 :            :   }
     269                 :            : 
     270                 :            :   /* Returns the position of the current clause.  */
     271                 :            : 
     272                 :       1511 :   iterator current ()
     273                 :            :   {
     274                 :       1511 :     return m_current;
     275                 :            :   }
     276                 :            : 
     277                 :            :   /* Returns an iterator to the first clause in the formula.  */
     278                 :            : 
     279                 :       1511 :   iterator begin ()
     280                 :            :   {
     281                 :       1511 :     return m_clauses.begin ();
     282                 :            :   }
     283                 :            : 
     284                 :            :   /* Returns an iterator to the first clause in the formula.  */
     285                 :            : 
     286                 :            :   const_iterator begin () const
     287                 :            :   {
     288                 :            :     return m_clauses.begin ();
     289                 :            :   }
     290                 :            : 
     291                 :            :   /* Returns an iterator past the last clause in the formula.  */
     292                 :            : 
     293                 :       2253 :   iterator end ()
     294                 :            :   {
     295                 :       2253 :     return m_clauses.end ();
     296                 :            :   }
     297                 :            : 
     298                 :            :   /* Returns an iterator past the last clause in the formula.  */
     299                 :            : 
     300                 :       4533 :   const_iterator end () const
     301                 :            :   {
     302                 :          0 :     return m_clauses.end ();
     303                 :            :   }
     304                 :            : 
     305                 :            :   std::list<clause> m_clauses; /* The list of clauses.  */
     306                 :            :   iterator m_current; /* The current clause.  */
     307                 :            : };
     308                 :            : 
     309                 :            : void
     310                 :          0 : debug (clause& c)
     311                 :            : {
     312                 :          0 :   for (clause::iterator i = c.begin(); i != c.end(); ++i)
     313                 :          0 :     verbatim ("  # %E", *i);
     314                 :          0 : }
     315                 :            : 
     316                 :            : void
     317                 :          0 : debug (formula& f)
     318                 :            : {
     319                 :          0 :   for (formula::iterator i = f.begin(); i != f.end(); ++i)
     320                 :            :     {
     321                 :          0 :       verbatim ("(((");
     322                 :          0 :       debug (*i);
     323                 :          0 :       verbatim (")))");
     324                 :            :     }
     325                 :          0 : }
     326                 :            : 
     327                 :            : /* The logical rules used to analyze a logical formula. The
     328                 :            :    "left" and "right" refer to the position of formula in a
     329                 :            :    sequent (as in sequent calculus).  */
     330                 :            : 
     331                 :            : enum rules
     332                 :            : {
     333                 :            :   left, right
     334                 :            : };
     335                 :            : 
     336                 :            : /* Distribution counting.  */
     337                 :            : 
     338                 :            : static inline bool
     339                 :    1952520 : disjunction_p (tree t)
     340                 :            : {
     341                 :    1952520 :   return TREE_CODE (t) == DISJ_CONSTR;
     342                 :            : }
     343                 :            : 
     344                 :            : static inline bool
     345                 :    1353770 : conjunction_p (tree t)
     346                 :            : {
     347                 :    1353770 :   return TREE_CODE (t) == CONJ_CONSTR;
     348                 :            : }
     349                 :            : 
     350                 :            : static inline bool
     351                 :    1643040 : atomic_p (tree t)
     352                 :            : {
     353                 :    1643040 :   return TREE_CODE (t) == ATOMIC_CONSTR;
     354                 :            : }
     355                 :            : 
     356                 :            : /* Recursively count the number of clauses produced when converting T
     357                 :            :    to DNF. Returns a pair containing the number of clauses and a bool
     358                 :            :    value signifying that the tree would be rewritten as a result of
     359                 :            :    distributing. In general, a conjunction for which this flag is set
     360                 :            :    is considered a disjunction for the purpose of counting.  */
     361                 :            : 
     362                 :            : static std::pair<int, bool>
     363                 :     600267 : dnf_size_r (tree t)
     364                 :            : {
     365                 :     600267 :   if (atomic_p (t))
     366                 :            :     /* Atomic constraints produce no clauses.  */
     367                 :     300889 :     return std::make_pair (0, false);
     368                 :            : 
     369                 :            :   /* For compound constraints, recursively count clauses and unpack
     370                 :            :      the results.  */
     371                 :     299378 :   tree lhs = TREE_OPERAND (t, 0);
     372                 :     299378 :   tree rhs = TREE_OPERAND (t, 1);
     373                 :     299378 :   std::pair<int, bool> p1 = dnf_size_r (lhs);
     374                 :     299378 :   std::pair<int, bool> p2 = dnf_size_r (rhs);
     375                 :     299378 :   int n1 = p1.first, n2 = p2.first;
     376                 :     299378 :   bool d1 = p1.second, d2 = p2.second;
     377                 :            : 
     378                 :     299378 :   if (disjunction_p (t))
     379                 :            :     {
     380                 :            :       /* Matches constraints of the form P \/ Q. Disjunctions contribute
     381                 :            :          linearly to the number of constraints.  When both P and Q are
     382                 :            :          disjunctions, clauses are added. When only one of P and Q
     383                 :            :          is a disjunction, an additional clause is produced. When neither
     384                 :            :          P nor Q are disjunctions, two clauses are produced.  */
     385                 :          0 :       if (disjunction_p (lhs))
     386                 :            :         {
     387                 :          0 :           if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
     388                 :            :             /* Both P and Q are disjunctions.  */
     389                 :          0 :             return std::make_pair (n1 + n2, d1 | d2);
     390                 :            :           else
     391                 :            :             /* Only LHS is a disjunction.  */
     392                 :          0 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     393                 :            :           gcc_unreachable ();
     394                 :            :         }
     395                 :          0 :       if (conjunction_p (lhs))
     396                 :            :         {
     397                 :          0 :           if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
     398                 :            :             /* Both P and Q are disjunctions.  */
     399                 :          0 :             return std::make_pair (n1 + n2, d1 | d2);
     400                 :          0 :           if (disjunction_p (rhs)
     401                 :          0 :               || (conjunction_p (rhs) && d1 != d2)
     402                 :          0 :               || (atomic_p (rhs) && d1))
     403                 :            :             /* Either LHS or RHS is a disjunction.  */
     404                 :          0 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     405                 :            :           else
     406                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     407                 :          0 :             return std::make_pair (2, false);
     408                 :            :         }
     409                 :          0 :       if (atomic_p (lhs))
     410                 :            :         {
     411                 :          0 :           if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
     412                 :            :             /* Only RHS is a disjunction.  */
     413                 :          0 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     414                 :            :           else
     415                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     416                 :          0 :             return std::make_pair (2, false);
     417                 :            :         }
     418                 :            :     }
     419                 :            :   else /* conjunction_p (t)  */
     420                 :            :     {
     421                 :            :       /* Matches constraints of the form P /\ Q, possibly resulting
     422                 :            :          in the distribution of one side over the other. When both
     423                 :            :          P and Q are disjunctions, the number of clauses are multiplied.
     424                 :            :          When only one of P and Q is a disjunction, the number of
     425                 :            :          clauses are added. Otherwise, neither side is a disjunction and
     426                 :            :          no clauses are created.  */
     427                 :     299378 :       if (disjunction_p (lhs))
     428                 :            :         {
     429                 :          0 :           if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
     430                 :            :             /* Both P and Q are disjunctions.  */
     431                 :          0 :             return std::make_pair (n1 * n2, true);
     432                 :            :           else
     433                 :            :             /* Only LHS is a disjunction.  */
     434                 :          0 :             return std::make_pair (n1 + n2, true);
     435                 :            :           gcc_unreachable ();
     436                 :            :         }
     437                 :     299378 :       if (conjunction_p (lhs))
     438                 :            :         {
     439                 :     156253 :           if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
     440                 :            :             /* Both P and Q are disjunctions.  */
     441                 :          0 :             return std::make_pair (n1 * n2, true);
     442                 :     156253 :           if (disjunction_p (rhs)
     443                 :     156253 :               || (conjunction_p (rhs) && d1 != d2)
     444                 :     312506 :               || (atomic_p (rhs) && d1))
     445                 :            :             /* Either LHS or RHS is a disjunction.  */
     446                 :          0 :             return std::make_pair (n1 + n2, true);
     447                 :            :           else
     448                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     449                 :     156253 :             return std::make_pair (0, false);
     450                 :            :         }
     451                 :     143125 :       if (atomic_p (lhs))
     452                 :            :         {
     453                 :     143125 :           if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
     454                 :            :             /* Only RHS is a disjunction.  */
     455                 :          0 :             return std::make_pair (n1 + n2, true);
     456                 :            :           else
     457                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     458                 :     143125 :             return std::make_pair (0, false);
     459                 :            :         }
     460                 :            :     }
     461                 :          0 :   gcc_unreachable ();
     462                 :            : }
     463                 :            : 
     464                 :            : /* Recursively count the number of clauses produced when converting T
     465                 :            :    to CNF. Returns a pair containing the number of clauses and a bool
     466                 :            :    value signifying that the tree would be rewritten as a result of
     467                 :            :    distributing. In general, a disjunction for which this flag is set
     468                 :            :    is considered a conjunction for the purpose of counting.  */
     469                 :            : 
     470                 :            : static std::pair<int, bool>
     471                 :     600269 : cnf_size_r (tree t)
     472                 :            : {
     473                 :     600269 :   if (atomic_p (t))
     474                 :            :     /* Atomic constraints produce no clauses.  */
     475                 :     300890 :     return std::make_pair (0, false);
     476                 :            : 
     477                 :            :   /* For compound constraints, recursively count clauses and unpack
     478                 :            :      the results.  */
     479                 :     299379 :   tree lhs = TREE_OPERAND (t, 0);
     480                 :     299379 :   tree rhs = TREE_OPERAND (t, 1);
     481                 :     299379 :   std::pair<int, bool> p1 = cnf_size_r (lhs);
     482                 :     299379 :   std::pair<int, bool> p2 = cnf_size_r (rhs);
     483                 :     299379 :   int n1 = p1.first, n2 = p2.first;
     484                 :     299379 :   bool d1 = p1.second, d2 = p2.second;
     485                 :            : 
     486                 :     299379 :   if (disjunction_p (t))
     487                 :            :     {
     488                 :            :       /* Matches constraints of the form P \/ Q, possibly resulting
     489                 :            :          in the distribution of one side over the other. When both
     490                 :            :          P and Q are conjunctions, the number of clauses are multiplied.
     491                 :            :          When only one of P and Q is a conjunction, the number of
     492                 :            :          clauses are added. Otherwise, neither side is a conjunction and
     493                 :            :          no clauses are created.  */
     494                 :          0 :       if (disjunction_p (lhs))
     495                 :            :         {
     496                 :          0 :           if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
     497                 :            :             /* Both P and Q are conjunctions.  */
     498                 :          0 :             return std::make_pair (n1 * n2, true);
     499                 :          0 :           if ((disjunction_p (rhs) && d1 != d2)
     500                 :          0 :               || conjunction_p (rhs)
     501                 :          0 :               || (atomic_p (rhs) && d1))
     502                 :            :             /* Either LHS or RHS is a conjunction.  */
     503                 :          0 :             return std::make_pair (n1 + n2, true);
     504                 :            :           else
     505                 :            :             /* Neither LHS nor RHS is a conjunction.  */
     506                 :          0 :             return std::make_pair (0, false);
     507                 :            :           gcc_unreachable ();
     508                 :            :         }
     509                 :          0 :       if (conjunction_p (lhs))
     510                 :            :         {
     511                 :          0 :           if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
     512                 :            :             /* Both LHS and RHS are conjunctions.  */
     513                 :          0 :             return std::make_pair (n1 * n2, true);
     514                 :            :           else
     515                 :            :             /* Only LHS is a conjunction.  */
     516                 :          0 :             return std::make_pair (n1 + n2, true);
     517                 :            :         }
     518                 :          0 :       if (atomic_p (lhs))
     519                 :            :         {
     520                 :          0 :           if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
     521                 :            :             /* Only RHS is a disjunction.  */
     522                 :          0 :             return std::make_pair (n1 + n2, true);
     523                 :            :           else
     524                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     525                 :          0 :             return std::make_pair (0, false);
     526                 :            :         }
     527                 :            :     }
     528                 :            :   else /* conjunction_p (t)  */
     529                 :            :     {
     530                 :            :       /* Matches constraints of the form P /\ Q. Conjunctions contribute
     531                 :            :          linearly to the number of constraints.  When both P and Q are
     532                 :            :          conjunctions, clauses are added. When only one of P and Q
     533                 :            :          is a conjunction, an additional clause is produced. When neither
     534                 :            :          P nor Q are conjunctions, two clauses are produced.  */
     535                 :     299379 :       if (disjunction_p (lhs))
     536                 :            :         {
     537                 :          0 :           if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
     538                 :            :             /* Both P and Q are conjunctions.  */
     539                 :          0 :             return std::make_pair (n1 + n2, d1 | d2);
     540                 :          0 :           if ((disjunction_p (rhs) && d1 != d2)
     541                 :          0 :               || conjunction_p (rhs)
     542                 :          0 :               || (atomic_p (rhs) && d1))
     543                 :            :             /* Either LHS or RHS is a conjunction.  */
     544                 :          0 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     545                 :            :           else
     546                 :            :             /* Neither LHS nor RHS is a conjunction.  */
     547                 :          0 :             return std::make_pair (2, false);
     548                 :            :           gcc_unreachable ();
     549                 :            :         }
     550                 :     299379 :       if (conjunction_p (lhs))
     551                 :            :         {
     552                 :     156253 :           if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
     553                 :            :             /* Both LHS and RHS are conjunctions.  */
     554                 :     113005 :             return std::make_pair (n1 + n2, d1 | d2);
     555                 :            :           else
     556                 :            :             /* Only LHS is a conjunction.  */
     557                 :      43248 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     558                 :            :         }
     559                 :     143126 :       if (atomic_p (lhs))
     560                 :            :         {
     561                 :     143126 :           if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
     562                 :            :             /* Only RHS is a disjunction.  */
     563                 :      29300 :             return std::make_pair (1 + n1 + n2, d1 | d2);
     564                 :            :           else
     565                 :            :             /* Neither LHS nor RHS is a disjunction.  */
     566                 :     113826 :             return std::make_pair (2, false);
     567                 :            :         }
     568                 :            :     }
     569                 :          0 :   gcc_unreachable ();
     570                 :            : }
     571                 :            : 
     572                 :            : /* Count the number conjunctive clauses that would be created
     573                 :            :    when rewriting T to DNF. */
     574                 :            : 
     575                 :            : static int
     576                 :       1511 : dnf_size (tree t)
     577                 :            : {
     578                 :          0 :   std::pair<int, bool> result = dnf_size_r (t);
     579                 :       1511 :   return result.first == 0 ? 1 : result.first;
     580                 :            : }
     581                 :            : 
     582                 :            : 
     583                 :            : /* Count the number disjunctive clauses that would be created
     584                 :            :    when rewriting T to CNF. */
     585                 :            : 
     586                 :            : static int
     587                 :       1511 : cnf_size (tree t)
     588                 :            : {
     589                 :          0 :   std::pair<int, bool> result = cnf_size_r (t);
     590                 :       1511 :   return result.first == 0 ? 1 : result.first;
     591                 :            : }
     592                 :            : 
     593                 :            : 
     594                 :            : /* A left-conjunction is replaced by its operands.  */
     595                 :            : 
     596                 :            : void
     597                 :     299378 : replace_term (clause& c, tree t)
     598                 :            : {
     599                 :     299378 :   tree t1 = TREE_OPERAND (t, 0);
     600                 :     299378 :   tree t2 = TREE_OPERAND (t, 1);
     601                 :     299378 :   return c.replace (t1, t2);
     602                 :            : }
     603                 :            : 
     604                 :            : /* Create a new clause in the formula by copying the current
     605                 :            :    clause. In the current clause, the term at CI is replaced
     606                 :            :    by the first operand, and in the new clause, it is replaced
     607                 :            :    by the second.  */
     608                 :            : 
     609                 :            : void
     610                 :          0 : branch_clause (formula& f, clause& c1, tree t)
     611                 :            : {
     612                 :          0 :   tree t1 = TREE_OPERAND (t, 0);
     613                 :          0 :   tree t2 = TREE_OPERAND (t, 1);
     614                 :          0 :   clause& c2 = f.branch ();
     615                 :          0 :   c1.replace (t1);
     616                 :          0 :   c2.replace (t2);
     617                 :          0 : }
     618                 :            : 
     619                 :            : /* Decompose t1 /\ t2 according to the rules R.  */
     620                 :            : 
     621                 :            : inline void
     622                 :     299378 : decompose_conjuntion (formula& f, clause& c, tree t, rules r)
     623                 :            : {
     624                 :     299378 :   if (r == left)
     625                 :     299378 :     replace_term (c, t);
     626                 :            :   else
     627                 :          0 :     branch_clause (f, c, t);
     628                 :            : }
     629                 :            : 
     630                 :            : /* Decompose t1 \/ t2 according to the rules R.  */
     631                 :            : 
     632                 :            : inline void
     633                 :          0 : decompose_disjunction (formula& f, clause& c, tree t, rules r)
     634                 :            : {
     635                 :          0 :   if (r == right)
     636                 :          0 :     replace_term (c, t);
     637                 :            :   else
     638                 :          0 :     branch_clause (f, c, t);
     639                 :            : }
     640                 :            : 
     641                 :            : /* An atomic constraint is already decomposed.  */
     642                 :            : inline void
     643                 :      52137 : decompose_atom (clause& c)
     644                 :            : {
     645                 :     104274 :   c.advance ();
     646                 :      52137 : }
     647                 :            : 
     648                 :            : /* Decompose a term of clause C (in formula F) according to the
     649                 :            :    logical rules R. */
     650                 :            : 
     651                 :            : void
     652                 :     351515 : decompose_term (formula& f, clause& c, tree t, rules r)
     653                 :            : {
     654                 :     351515 :   switch (TREE_CODE (t))
     655                 :            :     {
     656                 :     299378 :       case CONJ_CONSTR:
     657                 :     299378 :         return decompose_conjuntion (f, c, t, r);
     658                 :          0 :       case DISJ_CONSTR:
     659                 :          0 :         return decompose_disjunction (f, c, t, r);
     660                 :      52137 :       default:
     661                 :      52137 :         return decompose_atom (c);
     662                 :            :     }
     663                 :            : }
     664                 :            : 
     665                 :            : /* Decompose C (in F) using the logical rules R until it
     666                 :            :    is comprised of only atomic constraints.  */
     667                 :            : 
     668                 :            : void
     669                 :       1511 : decompose_clause (formula& f, clause& c, rules r)
     670                 :            : {
     671                 :     353026 :   while (!c.done ())
     672                 :     351515 :     decompose_term (f, c, *c.current (), r);
     673                 :       1511 :   f.advance ();
     674                 :       1511 : }
     675                 :            : 
     676                 :            : /* Decompose the logical formula F according to the logical
     677                 :            :    rules determined by R.  The result is a formula containing
     678                 :            :    clauses that contain only atomic terms.  */
     679                 :            : 
     680                 :            : void
     681                 :       1511 : decompose_formula (formula& f, rules r)
     682                 :            : {
     683                 :       3022 :   while (!f.done ())
     684                 :       1511 :     decompose_clause (f, *f.current (), r);
     685                 :       1511 : }
     686                 :            : 
     687                 :            : /* Fully decomposing T into a list of sequents, each comprised of
     688                 :            :    a list of atomic constraints, as if T were an antecedent.  */
     689                 :            : 
     690                 :            : static formula
     691                 :       1511 : decompose_antecedents (tree t)
     692                 :            : {
     693                 :          0 :   formula f (t);
     694                 :       1511 :   decompose_formula (f, left);
     695                 :       1511 :   return f;
     696                 :            : }
     697                 :            : 
     698                 :            : /* Fully decomposing T into a list of sequents, each comprised of
     699                 :            :    a list of atomic constraints, as if T were a consequent.  */
     700                 :            : 
     701                 :            : static formula
     702                 :          0 : decompose_consequents (tree t)
     703                 :            : {
     704                 :          0 :   formula f (t);
     705                 :          0 :   decompose_formula (f, right);
     706                 :          0 :   return f;
     707                 :            : }
     708                 :            : 
     709                 :            : static bool derive_proof (clause&, tree, rules);
     710                 :            : 
     711                 :            : /* Derive a proof of both operands of T.  */
     712                 :            : 
     713                 :            : static bool
     714                 :      23375 : derive_proof_for_both_operands (clause& c, tree t, rules r)
     715                 :            : {
     716                 :      23375 :   if (!derive_proof (c, TREE_OPERAND (t, 0), r))
     717                 :            :     return false;
     718                 :      19477 :   return derive_proof (c, TREE_OPERAND (t, 1), r);
     719                 :            : }
     720                 :            : 
     721                 :            : /* Derive a proof of either operand of T.  */
     722                 :            : 
     723                 :            : static bool
     724                 :          0 : derive_proof_for_either_operand (clause& c, tree t, rules r)
     725                 :            : {
     726                 :          0 :   if (derive_proof (c, TREE_OPERAND (t, 0), r))
     727                 :            :     return true;
     728                 :          0 :   return derive_proof (c, TREE_OPERAND (t, 1), r);
     729                 :            : }
     730                 :            : 
     731                 :            : /* Derive a proof of the atomic constraint T in clause C.  */
     732                 :            : 
     733                 :            : static bool
     734                 :      20988 : derive_atomic_proof (clause& c, tree t)
     735                 :            : {
     736                 :          0 :   return c.contains (t);
     737                 :            : }
     738                 :            : 
     739                 :            : /* Derive a proof of T from the terms in C.  */
     740                 :            : 
     741                 :            : static bool
     742                 :      44363 : derive_proof (clause& c, tree t, rules r)
     743                 :            : {
     744                 :      44363 :   switch (TREE_CODE (t))
     745                 :            :   {
     746                 :      23375 :     case CONJ_CONSTR:
     747                 :      23375 :       if (r == left)
     748                 :      23375 :         return derive_proof_for_both_operands (c, t, r);
     749                 :            :       else
     750                 :          0 :         return derive_proof_for_either_operand (c, t, r);
     751                 :          0 :     case DISJ_CONSTR:
     752                 :          0 :       if (r == left)
     753                 :          0 :         return derive_proof_for_either_operand (c, t, r);
     754                 :            :       else
     755                 :          0 :         return derive_proof_for_both_operands (c, t, r);
     756                 :      20988 :     default:
     757                 :      20988 :       return derive_atomic_proof (c, t);
     758                 :            :   }
     759                 :            : }
     760                 :            : 
     761                 :            : /* Derive a proof of T from disjunctive clauses in F.  */
     762                 :            : 
     763                 :            : static bool
     764                 :       1511 : derive_proofs (formula& f, tree t, rules r)
     765                 :            : {
     766                 :       2253 :   for (formula::iterator i = f.begin(); i != f.end(); ++i)
     767                 :       1511 :     if (!derive_proof (*i, t, r))
     768                 :          0 :       return false;
     769                 :            :   return true;
     770                 :            : }
     771                 :            : 
     772                 :            : /* The largest number of clauses in CNF or DNF we accept as input
     773                 :            :    for subsumption. This an upper bound of 2^16 expressions.  */
     774                 :            : static int max_problem_size = 16;
     775                 :            : 
     776                 :            : static inline bool
     777                 :          0 : diagnose_constraint_size (tree t)
     778                 :            : {
     779                 :          0 :   error_at (input_location, "%qE exceeds the maximum constraint complexity", t);
     780                 :          0 :   return false;
     781                 :            : }
     782                 :            : 
     783                 :            : /* Key/value pair for caching subsumption results. This associates a pair of
     784                 :            :    constraints with a boolean value indicating the result.  */
     785                 :            : 
     786                 :            : struct GTY((for_user)) subsumption_entry
     787                 :            : {
     788                 :            :   tree lhs;
     789                 :            :   tree rhs;
     790                 :            :   bool result;
     791                 :            : };
     792                 :            : 
     793                 :            : /* Hashing function and equality for constraint entries.  */
     794                 :            : 
     795                 :            : struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
     796                 :            : {
     797                 :            :   static hashval_t hash (subsumption_entry *e)
     798                 :            :   {
     799                 :            :     hashval_t val = 0;
     800                 :            :     val = iterative_hash_constraint (e->lhs, val);
     801                 :            :     val = iterative_hash_constraint (e->rhs, val);
     802                 :            :     return val;
     803                 :            :   }
     804                 :            : 
     805                 :            :   static bool equal (subsumption_entry *e1, subsumption_entry *e2)
     806                 :            :   {
     807                 :            :     if (!constraints_equivalent_p (e1->lhs, e2->lhs))
     808                 :            :       return false;
     809                 :            :     if (!constraints_equivalent_p (e1->rhs, e2->rhs))
     810                 :            :       return false;
     811                 :            :     return true;
     812                 :            :   }
     813                 :            : };
     814                 :            : 
     815                 :            : /* Caches the results of subsumes_non_null(t1, t1).  */
     816                 :            : 
     817                 :            : static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;
     818                 :            : 
     819                 :            : /* Search for a previously cached subsumption result. */
     820                 :            : 
     821                 :            : static bool*
     822                 :       5691 : lookup_subsumption (tree t1, tree t2)
     823                 :            : {
     824                 :       5691 :   if (!subsumption_cache)
     825                 :            :     return NULL;
     826                 :       5108 :   subsumption_entry elt = { t1, t2, false };
     827                 :       5108 :   subsumption_entry* found = subsumption_cache->find (&elt);
     828                 :       5108 :   if (found)
     829                 :       4180 :     return &found->result;
     830                 :            :   else
     831                 :            :     return 0;
     832                 :            : }
     833                 :            : 
     834                 :            : /* Save a subsumption result. */
     835                 :            : 
     836                 :            : static bool
     837                 :       1511 : save_subsumption (tree t1, tree t2, bool result)
     838                 :            : {
     839                 :       1511 :   if (!subsumption_cache)
     840                 :        583 :     subsumption_cache = hash_table<subsumption_hasher>::create_ggc(31);
     841                 :       1511 :   subsumption_entry elt = {t1, t2, result};
     842                 :       1511 :   subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
     843                 :       1511 :   subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
     844                 :       1511 :   *entry = elt;
     845                 :       1511 :   *slot = entry;
     846                 :       1511 :   return result;
     847                 :            : }
     848                 :            : 
     849                 :            : 
     850                 :            : /* Returns true if the LEFT constraint subsume the RIGHT constraints.
     851                 :            :    This is done by deriving a proof of the conclusions on the RIGHT
     852                 :            :    from the assumptions on the LEFT assumptions.  */
     853                 :            : 
     854                 :            : static bool
     855                 :       5691 : subsumes_constraints_nonnull (tree lhs, tree rhs)
     856                 :            : {
     857                 :       5691 :   auto_timevar time (TV_CONSTRAINT_SUB);
     858                 :            : 
     859                 :       5691 :   if (bool *b = lookup_subsumption(lhs, rhs))
     860                 :       4180 :     return *b;
     861                 :            : 
     862                 :       1511 :   int n1 = dnf_size (lhs);
     863                 :       1511 :   int n2 = cnf_size (rhs);
     864                 :            : 
     865                 :            :   /* Make sure we haven't exceeded the largest acceptable problem.  */
     866                 :       1511 :   if (std::min (n1, n2) >= max_problem_size)
     867                 :            :     {
     868                 :          0 :       if (n1 < n2)
     869                 :          0 :         diagnose_constraint_size (lhs);
     870                 :            :       else
     871                 :          0 :         diagnose_constraint_size (rhs);
     872                 :          0 :       return false;
     873                 :            :     }
     874                 :            : 
     875                 :            :   /* Decompose the smaller of the two formulas, and recursively
     876                 :            :      check for implication of the larger.  */
     877                 :       1511 :   bool result;
     878                 :       1511 :   if (n1 <= n2)
     879                 :            :     {
     880                 :       3022 :       formula dnf = decompose_antecedents (lhs);
     881                 :       3022 :       result = derive_proofs (dnf, rhs, left);
     882                 :            :     }
     883                 :            :   else
     884                 :            :     {
     885                 :          0 :       formula cnf = decompose_consequents (rhs);
     886                 :          0 :       result = derive_proofs (cnf, lhs, right);
     887                 :            :     }
     888                 :            : 
     889                 :       1511 :   return save_subsumption (lhs, rhs, result);
     890                 :            : }
     891                 :            : 
     892                 :            : /* Returns true if the LEFT constraints subsume the RIGHT
     893                 :            :    constraints.  */
     894                 :            : 
     895                 :            : bool
     896                 :     366581 : subsumes (tree lhs, tree rhs)
     897                 :            : {
     898                 :     366581 :   if (lhs == rhs)
     899                 :            :     return true;
     900                 :      52292 :   if (!lhs || lhs == error_mark_node)
     901                 :            :     return false;
     902                 :      28994 :   if (!rhs || rhs == error_mark_node)
     903                 :            :     return true;
     904                 :       5691 :   return subsumes_constraints_nonnull (lhs, rhs);
     905                 :            : }
     906                 :            : 
     907                 :            : #include "gt-cp-logic.h"

Generated by: LCOV version 1.0

LCOV profile is generated on x86_64 machine using following configure options: configure --disable-bootstrap --enable-coverage=opt --enable-languages=c,c++,fortran,go,jit,lto --enable-host-shared. GCC test suite is run with the built compiler.