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)
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/>. */
23 #include "coretypes.h"
28 #include "double-int.h"
35 #include "stringpool.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"
46 #include "type-utils.h"
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
)
58 for ( ; first
!= last
; ++first
, ++iter
)
63 /*---------------------------------------------------------------------------
65 ---------------------------------------------------------------------------*/
67 /* A term list is a list of atomic constraints. It is used
68 to maintain the lists of assumptions and conclusions in a
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
>
77 term_list (const term_list
&x
);
78 term_list
& operator= (const term_list
&x
);
80 tree
current_term () { return *current
; }
81 const_tree
current_term () const { return *current
; }
95 term_list::term_list ()
96 : std::list
<tree
> (), current (end ())
100 term_list::term_list (const term_list
&x
)
101 : std::list
<tree
> (x
)
102 , current (next_by_distance (begin (), x
.begin (), x
.current
))
106 term_list::operator= (const term_list
&x
)
108 std::list
<tree
>::operator=(x
);
109 current
= next_by_distance (begin (), x
.begin (), x
.current
);
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.
118 Note that not inserting terms is an optimization
119 that corresponds to the structural rule of
122 NOTE: With the contraction rule, this data structure
123 would be more efficiently represented as an ordered set
126 term_list::insert (tree t
)
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
))
134 current
= std::list
<tree
>::insert (current
, t
);
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.
141 The removed term is returned. */
146 current
= std::list
<tree
>::erase (current
);
150 /* Initialize the current term to the first in the list. */
157 /* Advance to the next term in the list. */
164 /* Returns true when the current position is past the end. */
166 term_list::done () const
168 return current
== end ();
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).
179 term_list assumptions
;
180 term_list conclusions
;
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
>
190 iterator
branch (iterator i
);
193 /* An alias for proof state iterators. */
194 typedef proof_state::iterator goal_iterator
;
196 /* Initialize the state with a single empty goal,
197 and set that goal as the current subgoal. */
199 proof_state::proof_state ()
200 : std::list
<proof_goal
> (1)
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
)
210 gcc_assert (i
!= end());
212 return insert (++i
, g
);
215 /*---------------------------------------------------------------------------
217 ---------------------------------------------------------------------------*/
219 /*These functions modify the current state and goal by decomposing
220 logical expressions using the logical rules of sequent calculus for
223 Note that in each decomposition rule, the term T has been erased
224 from term list before the specific rule is applied. */
226 /* The left logical rule for conjunction adds both operands
227 to the current set of constraints. */
229 left_conjunction (proof_state
&, goal_iterator i
, tree t
)
231 gcc_assert (TREE_CODE (t
) == CONJ_CONSTR
);
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));
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
245 left_disjunction (proof_state
&s
, goal_iterator i
, tree t
)
247 gcc_assert (TREE_CODE (t
) == DISJ_CONSTR
);
249 /* Branch the current subgoal. */
250 goal_iterator j
= s
.branch (i
);
251 term_list
&l1
= i
->assumptions
;
252 term_list
&l2
= j
->assumptions
;
254 /* Insert operands into the different branches. */
255 l1
.insert (TREE_OPERAND (t
, 0));
256 l2
.insert (TREE_OPERAND (t
, 1));
259 /* The left logical rules for parameterized constraints
260 adds its operand to the current goal. The list of
261 parameters are effectively discarded. */
263 left_parameterized_constraint (proof_state
&, goal_iterator i
, tree t
)
265 gcc_assert (TREE_CODE (t
) == PARM_CONSTR
);
266 term_list
&l
= i
->assumptions
;
267 l
.insert (PARM_CONSTR_OPERAND (t
));
270 /*---------------------------------------------------------------------------
272 ---------------------------------------------------------------------------*/
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.
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. */
283 /* Apply the left logical rules to the proof state. */
285 decompose_left_term (proof_state
&s
, goal_iterator i
)
287 term_list
&l
= i
->assumptions
;
288 tree t
= l
.current_term ();
289 switch (TREE_CODE (t
))
292 left_conjunction (s
, i
, l
.erase ());
295 left_disjunction (s
, i
, l
.erase ());
298 left_parameterized_constraint (s
, i
, l
.erase ());
306 /* Apply the left logical rules of the sequent calculus
307 until the current goal is fully decomposed into atomic
310 decompose_left_goal (proof_state
&s
, goal_iterator i
)
312 term_list
& l
= i
->assumptions
;
315 decompose_left_term (s
, i
);
318 /* Apply the left logical rules of the sequent calculus
319 until the antecedents are fully decomposed into atomic
322 decompose_left (proof_state
& s
)
324 goal_iterator iter
= s
.begin ();
325 goal_iterator end
= s
.end ();
326 for ( ; iter
!= end
; ++iter
)
327 decompose_left_goal (s
, iter
);
330 /* Returns a vector of terms from the term list L. */
332 extract_terms (term_list
& l
)
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
;
342 /* Extract the assumptions from the proof state S
343 as a vector of vectors of atomic constraints. */
345 extract_assumptions (proof_state
& s
)
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
);
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. */
361 decompose_assumptions (tree t
)
363 if (!t
|| t
== error_mark_node
)
366 /* Create a proof state, and insert T as the sole assumption. */
368 term_list
&l
= s
.begin ()->assumptions
;
371 /* Decompose the expression into a constraint set, and then
372 extract the terms for the AST. */
374 return extract_assumptions (s
);
378 /*---------------------------------------------------------------------------
380 ---------------------------------------------------------------------------*/
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
);
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.
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. */
397 match_terms (tree a
, tree c
)
399 return cp_tree_equal (a
, c
);
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. */
406 subsumes_atomic_constraint (tree as
, tree c
)
408 for (int i
= 0; i
< TREE_VEC_LENGTH (as
); ++i
)
409 if (match_terms (TREE_VEC_ELT (as
, i
), c
))
414 /* Returns true when both operands of C are subsumed by the
417 subsumes_conjunction (tree as
, tree c
)
419 tree l
= TREE_OPERAND (c
, 0);
420 tree r
= TREE_OPERAND (c
, 1);
421 return subsumes_constraint (as
, l
) && subsumes_constraint (as
, r
);
424 /* Returns true when either operand of C is subsumed by the
427 subsumes_disjunction (tree as
, tree c
)
429 tree l
= TREE_OPERAND (c
, 0);
430 tree r
= TREE_OPERAND (c
, 1);
431 return subsumes_constraint (as
, l
) || subsumes_constraint (as
, r
);
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. */
438 subsumes_parameterized_constraint (tree as
, tree c
)
440 tree t
= PARM_CONSTR_OPERAND (c
);
441 return subsumes_constraint (as
, t
);
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. */
449 subsumes_constraint (tree as
, tree c
)
451 switch (TREE_CODE (c
))
454 return subsumes_conjunction (as
, c
);
456 return subsumes_disjunction (as
, c
);
458 return subsumes_parameterized_constraint (as
, c
);
460 return subsumes_atomic_constraint (as
, c
);
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. */
468 subsumes_constraints_nonnull (tree left
, tree right
)
470 gcc_assert (check_constraint_info (left
));
471 gcc_assert (check_constraint_info (right
));
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
))
485 /* Returns true if the LEFT constraints subsume the RIGHT
488 subsumes (tree left
, tree right
)
496 return subsumes_constraints_nonnull (left
, right
);