diff options
Diffstat (limited to 'gcc/cp/logic.cc')
| -rw-r--r-- | gcc/cp/logic.cc | 497 |
1 files changed, 497 insertions, 0 deletions
diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc new file mode 100644 index 00000000000..7e016409c30 --- /dev/null +++ b/gcc/cp/logic.cc @@ -0,0 +1,497 @@ +/* Derivation and subsumption rules for constraints. + Copyright (C) 2013-2015 Free Software Foundation, Inc. + Contributed by Andrew Sutton (andrew.n.sutton@gmail.com) + +This file is part of GCC. + +GCC is free software; you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation; either version 3, or (at your option) +any later version. + +GCC is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with GCC; see the file COPYING3. If not see +<http://www.gnu.org/licenses/>. */ + +#include "config.h" +#include "system.h" +#include "coretypes.h" +#include "tm.h" +#include "hash-set.h" +#include "machmode.h" +#include "vec.h" +#include "double-int.h" +#include "input.h" +#include "alias.h" +#include "symtab.h" +#include "wide-int.h" +#include "inchash.h" +#include "tree.h" +#include "stringpool.h" +#include "attribs.h" +#include "intl.h" +#include "flags.h" +#include "cp-tree.h" +#include "c-family/c-common.h" +#include "c-family/c-objc.h" +#include "cp-objcp-common.h" +#include "tree-inline.h" +#include "decl.h" +#include "toplev.h" +#include "type-utils.h" + +#include <list> + +namespace { + +// Helper algorithms + +// Increment iter distance(first, last) times. +template<typename I1, typename I2, typename I3> + I1 next_by_distance (I1 iter, I2 first, I3 last) + { + for ( ; first != last; ++first, ++iter) + ; + return iter; + } + +/*--------------------------------------------------------------------------- + Proof state +---------------------------------------------------------------------------*/ + +/* A term list is a list of atomic constraints. It is used + to maintain the lists of assumptions and conclusions in a + proof goal. + + Each term list maintains an iterator that refers to the current + term. This can be used by various tactics to support iteration + and stateful manipulation of the list. */ +struct term_list : std::list<tree> +{ + term_list (); + term_list (const term_list &x); + term_list& operator= (const term_list &x); + + tree current_term () { return *current; } + const_tree current_term () const { return *current; } + + + void insert (tree t); + tree erase (); + + void start (); + void next (); + bool done() const; + + iterator current; +}; + +inline +term_list::term_list () + : std::list<tree> (), current (end ()) +{ } + +inline +term_list::term_list (const term_list &x) + : std::list<tree> (x) + , current (next_by_distance (begin (), x.begin (), x.current)) +{ } + +inline term_list& +term_list::operator= (const term_list &x) +{ + std::list<tree>::operator=(x); + current = next_by_distance (begin (), x.begin (), x.current); + return *this; +} + +/* Try saving the term T into the list of terms. If + T is already in the list of terms, then no action is + performed. Otherwise, insert T before the current + position, making this term current. + + Note that not inserting terms is an optimization + that corresponds to the structural rule of + contraction. + + NOTE: With the contraction rule, this data structure + would be more efficiently represented as an ordered set + or hash set. */ +void +term_list::insert (tree t) +{ + /* Search the current term list. If there is already + a matching term, do not add the new one. */ + for (iterator i = begin(); i != end(); ++i) + if (cp_tree_equal (*i, t)) + return; + + current = std::list<tree>::insert (current, t); +} + +/* Remove the current term from the list, repositioning to + the term following the removed term. Note that the new + position could be past the end of the list. + + The removed term is returned. */ +inline tree +term_list::erase () +{ + tree t = *current; + current = std::list<tree>::erase (current); + return t; +} + +/* Initialize the current term to the first in the list. */ +inline void +term_list::start () +{ + current = begin (); +} + +/* Advance to the next term in the list. */ +inline void +term_list::next () +{ + ++current; +} + +/* Returns true when the current position is past the end. */ +inline bool +term_list::done () const +{ + return current == end (); +} + + +/* A goal (or subgoal) models a sequent of the form + 'A |- C' where A and C are lists of assumptions and + conclusions written as propositions in the constraint + language (i.e., lists of trees). +*/ +struct proof_goal +{ + term_list assumptions; + term_list conclusions; +}; + +/* A proof state owns a list of goals and tracks the + current sub-goal. The class also provides facilities + for managing subgoals and constructing term lists. */ +struct proof_state : std::list<proof_goal> +{ + proof_state (); + + iterator branch (iterator i); +}; + +/* An alias for proof state iterators. */ +typedef proof_state::iterator goal_iterator; + +/* Initialize the state with a single empty goal, + and set that goal as the current subgoal. */ +inline +proof_state::proof_state () + : std::list<proof_goal> (1) +{ } + + +/* Branch the current goal by creating a new subgoal, + returning a reference to // the new object. This does + not update the current goal. */ +inline proof_state::iterator +proof_state::branch (iterator i) +{ + gcc_assert (i != end()); + proof_goal& g = *i; + return insert (++i, g); +} + +/*--------------------------------------------------------------------------- + Logical rules +---------------------------------------------------------------------------*/ + +/*These functions modify the current state and goal by decomposing + logical expressions using the logical rules of sequent calculus for + first order logic. + + Note that in each decomposition rule, the term T has been erased + from term list before the specific rule is applied. */ + +/* The left logical rule for conjunction adds both operands + to the current set of constraints. */ +void +left_conjunction (proof_state &, goal_iterator i, tree t) +{ + gcc_assert (TREE_CODE (t) == CONJ_CONSTR); + + /* Insert the operands into the current branch. Note that the + final order of insertion is left-to-right. */ + term_list &l = i->assumptions; + l.insert (TREE_OPERAND (t, 1)); + l.insert (TREE_OPERAND (t, 0)); +} + +/* The left logical rule for disjunction creates a new goal, + adding the first operand to the original set of + constraints and the second operand to the new set + of constraints. */ +void +left_disjunction (proof_state &s, goal_iterator i, tree t) +{ + gcc_assert (TREE_CODE (t) == DISJ_CONSTR); + + /* Branch the current subgoal. */ + goal_iterator j = s.branch (i); + term_list &l1 = i->assumptions; + term_list &l2 = j->assumptions; + + /* Insert operands into the different branches. */ + l1.insert (TREE_OPERAND (t, 0)); + l2.insert (TREE_OPERAND (t, 1)); +} + +/* The left logical rules for parameterized constraints + adds its operand to the current goal. The list of + parameters are effectively discarded. */ +void +left_parameterized_constraint (proof_state &, goal_iterator i, tree t) +{ + gcc_assert (TREE_CODE (t) == PARM_CONSTR); + term_list &l = i->assumptions; + l.insert (PARM_CONSTR_OPERAND (t)); +} + +/*--------------------------------------------------------------------------- + Decomposition +---------------------------------------------------------------------------*/ + +/* The following algorithms decompose expressions into sets of + atomic propositions. In terms of the sequent calculus, these + functions exercise the logical rules only. + + This is equivalent, for the purpose of determining subsumption, + to rewriting a constraint in disjunctive normal form. It also + allows the resulting assumptions to be used as declarations + for the purpose of separate checking. */ + +/* Apply the left logical rules to the proof state. */ +void +decompose_left_term (proof_state &s, goal_iterator i) +{ + term_list &l = i->assumptions; + tree t = l.current_term (); + switch (TREE_CODE (t)) + { + case CONJ_CONSTR: + left_conjunction (s, i, l.erase ()); + break; + case DISJ_CONSTR: + left_disjunction (s, i, l.erase ()); + break; + case PARM_CONSTR: + left_parameterized_constraint (s, i, l.erase ()); + break; + default: + l.next (); + break; + } +} + +/* Apply the left logical rules of the sequent calculus + until the current goal is fully decomposed into atomic + constraints. */ +void +decompose_left_goal (proof_state &s, goal_iterator i) +{ + term_list& l = i->assumptions; + l.start (); + while (!l.done ()) + decompose_left_term (s, i); +} + +/* Apply the left logical rules of the sequent calculus + until the antecedents are fully decomposed into atomic + constraints. */ +void +decompose_left (proof_state& s) +{ + goal_iterator iter = s.begin (); + goal_iterator end = s.end (); + for ( ; iter != end; ++iter) + decompose_left_goal (s, iter); +} + +/* Returns a vector of terms from the term list L. */ +tree +extract_terms (term_list& l) +{ + tree result = make_tree_vec (l.size()); + term_list::iterator iter = l.begin(); + term_list::iterator end = l.end(); + for (int n = 0; iter != end; ++iter, ++n) + TREE_VEC_ELT (result, n) = *iter; + return result; +} + +/* Extract the assumptions from the proof state S + as a vector of vectors of atomic constraints. */ +inline tree +extract_assumptions (proof_state& s) +{ + tree result = make_tree_vec (s.size ()); + goal_iterator iter = s.begin (); + goal_iterator end = s.end (); + for (int n = 0; iter != end; ++iter, ++n) + TREE_VEC_ELT (result, n) = extract_terms (iter->assumptions); + return result; +} + +} // namespace + +/* Decompose the required expression T into a constraint set: a + vector of vectors containing only atomic propositions. If T is + invalid, return an error. */ +tree +decompose_assumptions (tree t) +{ + if (!t || t == error_mark_node) + return t; + + /* Create a proof state, and insert T as the sole assumption. */ + proof_state s; + term_list &l = s.begin ()->assumptions; + l.insert (t); + + /* Decompose the expression into a constraint set, and then + extract the terms for the AST. */ + decompose_left (s); + return extract_assumptions (s); +} + + +/*--------------------------------------------------------------------------- + Subsumption Rules +---------------------------------------------------------------------------*/ + +namespace { + +bool subsumes_constraint (tree, tree); +bool subsumes_conjunction (tree, tree); +bool subsumes_disjunction (tree, tree); +bool subsumes_parameterized_constraint (tree, tree); +bool subsumes_atomic_constraint (tree, tree); + +/* Returns true if the assumption A matches the conclusion C. This + is generally the case when A and C have the same syntax. + + NOTE: There will be specialized matching rules to accommodate + type equivalence, conversion, inheritance, etc. But this is not + in the current concepts draft. */ +inline bool +match_terms (tree a, tree c) +{ + return cp_tree_equal (a, c); +} + +/* Returns true if the list of assumptions AS subsumes the atomic + proposition C. This is the case when we can find a proposition + in AS that entails the conclusion C. */ +bool +subsumes_atomic_constraint (tree as, tree c) +{ + for (int i = 0; i < TREE_VEC_LENGTH (as); ++i) + if (match_terms (TREE_VEC_ELT (as, i), c)) + return true; + return false; +} + +/* Returns true when both operands of C are subsumed by the + assumptions AS. */ +inline bool +subsumes_conjunction (tree as, tree c) +{ + tree l = TREE_OPERAND (c, 0); + tree r = TREE_OPERAND (c, 1); + return subsumes_constraint (as, l) && subsumes_constraint (as, r); +} + +/* Returns true when either operand of C is subsumed by the + assumptions AS. */ +inline bool +subsumes_disjunction (tree as, tree c) +{ + tree l = TREE_OPERAND (c, 0); + tree r = TREE_OPERAND (c, 1); + return subsumes_constraint (as, l) || subsumes_constraint (as, r); +} + +/* Returns true when the operand of C is subsumed by the + assumptions in AS. The parameters are not considered in + the subsumption rules. */ +bool +subsumes_parameterized_constraint (tree as, tree c) +{ + tree t = PARM_CONSTR_OPERAND (c); + return subsumes_constraint (as, t); +} + + +/* Returns true when the list of assumptions AS subsumes the + concluded proposition C. This is a simple recursive descent + on C, matching against propositions in the assumption list AS. */ +bool +subsumes_constraint (tree as, tree c) +{ + switch (TREE_CODE (c)) + { + case CONJ_CONSTR: + return subsumes_conjunction (as, c); + case DISJ_CONSTR: + return subsumes_disjunction (as, c); + case PARM_CONSTR: + return subsumes_parameterized_constraint (as, c); + default: + return subsumes_atomic_constraint (as, c); + } +} + +/* Returns true if the LEFT constraints subsume the RIGHT constraints. + This is done by checking that the RIGHT requirements follow from + each of the LEFT subgoals. */ +bool +subsumes_constraints_nonnull (tree left, tree right) +{ + gcc_assert (check_constraint_info (left)); + gcc_assert (check_constraint_info (right)); + + /* Check that the required expression in RIGHT is subsumed by each + subgoal in the assumptions of LEFT. */ + tree as = CI_ASSUMPTIONS (left); + tree c = CI_NORMALIZED_CONSTRAINTS (right); + for (int i = 0; i < TREE_VEC_LENGTH (as); ++i) + if (!subsumes_constraint (TREE_VEC_ELT (as, i), c)) + return false; + return true; +} + +} /* namespace */ + +/* Returns true if the LEFT constraints subsume the RIGHT + constraints. */ +bool +subsumes (tree left, tree right) +{ + if (left == right) + return true; + if (!left) + return false; + if (!right) + return true; + return subsumes_constraints_nonnull (left, right); +} |