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)
5 This file is part of GCC.
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)
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.
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/>. */
24 #include "coretypes.h"
29 #include "double-int.h"
36 #include "stringpool.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"
47 #include "type-utils.h"
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
)
57 for ( ; first
!= last
; ++first
, ++iter
)
62 /*---------------------------------------------------------------------------
64 ---------------------------------------------------------------------------*/
66 /* A term list is a list of atomic constraints. It is used
67 to maintain the lists of assumptions and conclusions in a
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
>
76 term_list (const term_list
&x
);
77 term_list
& operator= (const term_list
&x
);
79 tree
current_term () { return *current
; }
80 const_tree
current_term () const { return *current
; }
94 term_list::term_list ()
95 : std::list
<tree
> (), current (end ())
99 term_list::term_list (const term_list
&x
)
100 : std::list
<tree
> (x
)
101 , current (next_by_distance (begin (), x
.begin (), x
.current
))
105 term_list::operator= (const term_list
&x
)
107 std::list
<tree
>::operator=(x
);
108 current
= next_by_distance (begin (), x
.begin (), x
.current
);
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.
117 Note that not inserting terms is an optimization
118 that corresponds to the structural rule of
121 NOTE: With the contraction rule, this data structure
122 would be more efficiently represented as an ordered set
125 term_list::insert (tree t
)
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
))
133 current
= std::list
<tree
>::insert (current
, t
);
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.
140 The removed term is returned. */
145 current
= std::list
<tree
>::erase (current
);
149 /* Initialize the current term to the first in the list. */
156 /* Advance to the next term in the list. */
163 /* Returns true when the current position is past the end. */
165 term_list::done () const
167 return current
== end ();
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).
178 term_list assumptions
;
179 term_list conclusions
;
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
>
189 iterator
branch (iterator i
);
192 /* An alias for proof state iterators. */
193 typedef proof_state::iterator goal_iterator
;
195 /* Initialize the state with a single empty goal,
196 and set that goal as the current subgoal. */
198 proof_state::proof_state ()
199 : std::list
<proof_goal
> (1)
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
)
209 gcc_assert (i
!= end());
211 return insert (++i
, g
);
214 /*---------------------------------------------------------------------------
216 ---------------------------------------------------------------------------*/
218 /*These functions modify the current state and goal by decomposing
219 logical expressions using the logical rules of sequent calculus for
222 Note that in each decomposition rule, the term T has been erased
223 from term list before the specific rule is applied. */
225 /* The left logical rule for conjunction adds both operands
226 to the current set of constraints. */
228 left_conjunction (proof_state
&, goal_iterator i
, tree t
)
230 gcc_assert (TREE_CODE (t
) == CONJ_CONSTR
);
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));
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
244 left_disjunction (proof_state
&s
, goal_iterator i
, tree t
)
246 gcc_assert (TREE_CODE (t
) == DISJ_CONSTR
);
248 /* Branch the current subgoal. */
249 goal_iterator j
= s
.branch (i
);
250 term_list
&l1
= i
->assumptions
;
251 term_list
&l2
= j
->assumptions
;
253 /* Insert operands into the different branches. */
254 l1
.insert (TREE_OPERAND (t
, 0));
255 l2
.insert (TREE_OPERAND (t
, 1));
258 /* The left logical rules for parameterized constraints
259 adds its operand to the current goal. The list of
260 parameters are effectively discarded. */
262 left_parameterized_constraint (proof_state
&, goal_iterator i
, tree t
)
264 gcc_assert (TREE_CODE (t
) == PARM_CONSTR
);
265 term_list
&l
= i
->assumptions
;
266 l
.insert (PARM_CONSTR_OPERAND (t
));
269 /*---------------------------------------------------------------------------
271 ---------------------------------------------------------------------------*/
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.
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. */
282 /* Apply the left logical rules to the proof state. */
284 decompose_left_term (proof_state
&s
, goal_iterator i
)
286 term_list
&l
= i
->assumptions
;
287 tree t
= l
.current_term ();
288 switch (TREE_CODE (t
))
291 left_conjunction (s
, i
, l
.erase ());
294 left_disjunction (s
, i
, l
.erase ());
297 left_parameterized_constraint (s
, i
, l
.erase ());
305 /* Apply the left logical rules of the sequent calculus
306 until the current goal is fully decomposed into atomic
309 decompose_left_goal (proof_state
&s
, goal_iterator i
)
311 term_list
& l
= i
->assumptions
;
314 decompose_left_term (s
, i
);
317 /* Apply the left logical rules of the sequent calculus
318 until the antecedents are fully decomposed into atomic
321 decompose_left (proof_state
& s
)
323 goal_iterator iter
= s
.begin ();
324 goal_iterator end
= s
.end ();
325 for ( ; iter
!= end
; ++iter
)
326 decompose_left_goal (s
, iter
);
329 /* Returns a vector of terms from the term list L. */
331 extract_terms (term_list
& l
)
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
;
341 /* Extract the assumptions from the proof state S
342 as a vector of vectors of atomic constraints. */
344 extract_assumptions (proof_state
& s
)
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
);
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. */
360 decompose_assumptions (tree t
)
362 if (!t
|| t
== error_mark_node
)
365 /* Create a proof state, and insert T as the sole assumption. */
367 term_list
&l
= s
.begin ()->assumptions
;
370 /* Decompose the expression into a constraint set, and then
371 extract the terms for the AST. */
373 return extract_assumptions (s
);
377 /*---------------------------------------------------------------------------
379 ---------------------------------------------------------------------------*/
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
);
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.
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. */
396 match_terms (tree a
, tree c
)
398 return cp_tree_equal (a
, c
);
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. */
405 subsumes_atomic_constraint (tree as
, tree c
)
407 for (int i
= 0; i
< TREE_VEC_LENGTH (as
); ++i
)
408 if (match_terms (TREE_VEC_ELT (as
, i
), c
))
413 /* Returns true when both operands of C are subsumed by the
416 subsumes_conjunction (tree as
, tree c
)
418 tree l
= TREE_OPERAND (c
, 0);
419 tree r
= TREE_OPERAND (c
, 1);
420 return subsumes_constraint (as
, l
) && subsumes_constraint (as
, r
);
423 /* Returns true when either operand of C is subsumed by the
426 subsumes_disjunction (tree as
, tree c
)
428 tree l
= TREE_OPERAND (c
, 0);
429 tree r
= TREE_OPERAND (c
, 1);
430 return subsumes_constraint (as
, l
) || subsumes_constraint (as
, r
);
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. */
437 subsumes_parameterized_constraint (tree as
, tree c
)
439 tree t
= PARM_CONSTR_OPERAND (c
);
440 return subsumes_constraint (as
, t
);
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. */
448 subsumes_constraint (tree as
, tree c
)
450 switch (TREE_CODE (c
))
453 return subsumes_conjunction (as
, c
);
455 return subsumes_disjunction (as
, c
);
457 return subsumes_parameterized_constraint (as
, c
);
459 return subsumes_atomic_constraint (as
, c
);
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. */
467 subsumes_constraints_nonnull (tree left
, tree right
)
469 gcc_assert (check_constraint_info (left
));
470 gcc_assert (check_constraint_info (right
));
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
))
484 /* Returns true if the LEFT constraints subsume the RIGHT
487 subsumes (tree left
, tree right
)
495 return subsumes_constraints_nonnull (left
, right
);