From patchwork Wed Jan 8 09:02:42 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: David Malcolm X-Patchwork-Id: 1219460 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-516860-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=fail (p=none dis=none) header.from=redhat.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="mahSV3JP"; dkim=fail reason="signature verification failed" (1024-bit key; unprotected) header.d=redhat.com header.i=@redhat.com header.b="R+yY+MBp"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 47t3MD1BNgz9sNx for ; Wed, 8 Jan 2020 20:08:38 +1100 (AEDT) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:from :to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-type:content-transfer-encoding; q=dns; s= default; b=uNRePysmv+EZOpO54OtqkOz0UYhM1wsBppvP6h1wyLR8VgbpQSSXR MpqYSmo8kZNxLYc5p5zQIhkg98eg1Stw+2e1rk2QWoL8k/Wis18s+yafbZolVIZN 94uoyv4XcMS3qjFw/9xQbY8X9umnu96y4ArbyNeEuccMsS5nSQ4qRs= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:from :to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-type:content-transfer-encoding; s=default; bh=wOmXFD+KFLweAKZfftyUb5hCRww=; b=mahSV3JPWplCL3xOtGBMA4XAbZjR cON6JqQ1g2SQStivzGLixHMmRwhb8S5op70V9jheECqyBbLEjLRco/8a1jsJnI32 5mVreg5N+VujeC6JuqRBfSxagxJ+synCAbn0heJpuRu7V4k95vgA93Q8PZ8/sBb5 tBRC5p3eykOVIxU= Received: (qmail 71640 invoked by alias); 8 Jan 2020 09:03:47 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 70911 invoked by uid 89); 8 Jan 2020 09:03:38 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-23.3 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_0, GIT_PATCH_1, GIT_PATCH_2, GIT_PATCH_3, KAM_SHORT, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.1 spammy=cleaning, visitors, overriding, 1023 X-HELO: us-smtp-1.mimecast.com Received: from us-smtp-delivery-1.mimecast.com (HELO us-smtp-1.mimecast.com) (207.211.31.120) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 08 Jan 2020 09:03:23 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1578474201; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=L4I1e5qGLVa5AbjsoUbm2oyeZCTLWwytM2qtX9IpB94=; b=R+yY+MBpN1saIumbih3Kx1kmIs27LvuGqD8tXxDrJ2zMh7ubWaY47K65vuZ7FJ+wSCkBMq F8HJd1ia5lfrbeSfQZwH10Hknjb9vK9bwsO7/NNQihWY+XkSo0iX7J6eSrBhrSm7zkF5Zh KR7Ce5iIxmOa1LXmWwz8hM7hINDwr4I= Received: from mimecast-mx01.redhat.com (mimecast-mx01.redhat.com [209.132.183.4]) (Using TLS) by relay.mimecast.com with ESMTP id us-mta-293-KeYYDuxoMvSveNiYGSHWKg-1; Wed, 08 Jan 2020 04:03:19 -0500 Received: from smtp.corp.redhat.com (int-mx07.intmail.prod.int.phx2.redhat.com [10.5.11.22]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by mimecast-mx01.redhat.com (Postfix) with ESMTPS id DB4D5800A02 for ; Wed, 8 Jan 2020 09:03:18 +0000 (UTC) Received: from t470.redhat.com (ovpn-117-41.phx2.redhat.com [10.3.117.41]) by smtp.corp.redhat.com (Postfix) with ESMTP id 6337A10013A7; Wed, 8 Jan 2020 09:03:18 +0000 (UTC) From: David Malcolm To: gcc-patches@gcc.gnu.org Cc: David Malcolm Subject: [PATCH 21/41] analyzer: new files: constraint-manager.{cc|h} Date: Wed, 8 Jan 2020 04:02:42 -0500 Message-Id: <20200108090302.2425-22-dmalcolm@redhat.com> In-Reply-To: <20200108090302.2425-1-dmalcolm@redhat.com> References: <20200108090302.2425-1-dmalcolm@redhat.com> MIME-Version: 1.0 X-Mimecast-Spam-Score: 0 X-IsSubscribed: yes Needs review. Changed in v5: - update ChangeLog path - updated copyright years to include 2020 Changed in v4: - Remove include of gcc-plugin.h, reworking includes accordingly. - Wrap everything in #if ENABLE_ANALYZER - Remove /// comment lines This patch adds classes for tracking the equivalence classes and constraints that hold at a point on an execution path. gcc/analyzer/ChangeLog: * constraint-manager.cc: New file. * constraint-manager.h: New file. --- gcc/analyzer/constraint-manager.cc | 2251 ++++++++++++++++++++++++++++ gcc/analyzer/constraint-manager.h | 248 +++ 2 files changed, 2499 insertions(+) create mode 100644 gcc/analyzer/constraint-manager.cc create mode 100644 gcc/analyzer/constraint-manager.h diff --git a/gcc/analyzer/constraint-manager.cc b/gcc/analyzer/constraint-manager.cc new file mode 100644 index 000000000000..8dff49e25cf9 --- /dev/null +++ b/gcc/analyzer/constraint-manager.cc @@ -0,0 +1,2251 @@ +/* Tracking equivalence classes and constraints at a point on an execution path. + Copyright (C) 2019-2020 Free Software Foundation, Inc. + Contributed by David Malcolm . + +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 +. */ + +#include "config.h" +#include "system.h" +#include "coretypes.h" +#include "tree.h" +#include "function.h" +#include "basic-block.h" +#include "gimple.h" +#include "gimple-iterator.h" +#include "fold-const.h" +#include "selftest.h" +#include "graphviz.h" +#include "analyzer/analyzer.h" +#include "analyzer/supergraph.h" +#include "analyzer/constraint-manager.h" +#include "analyzer/analyzer-selftests.h" + +#if ENABLE_ANALYZER + +/* One of the end-points of a range. */ + +struct bound +{ + bound () : m_constant (NULL_TREE), m_closed (false) {} + bound (tree constant, bool closed) + : m_constant (constant), m_closed (closed) {} + + void ensure_closed (bool is_upper); + + const char * get_relation_as_str () const; + + tree m_constant; + bool m_closed; +}; + +/* A range of values, used for determining if a value has been + constrained to just one possible constant value. */ + +struct range +{ + range () : m_lower_bound (), m_upper_bound () {} + range (const bound &lower, const bound &upper) + : m_lower_bound (lower), m_upper_bound (upper) {} + + void dump (pretty_printer *pp) const; + + bool constrained_to_single_element (tree *out); + + bound m_lower_bound; + bound m_upper_bound; +}; + +/* struct bound. */ + +/* Ensure that this bound is closed by converting an open bound to a + closed one. */ + +void +bound::ensure_closed (bool is_upper) +{ + if (!m_closed) + { + /* Offset by 1 in the appropriate direction. + For example, convert 3 < x into 4 <= x, + and convert x < 5 into x <= 4. */ + gcc_assert (CONSTANT_CLASS_P (m_constant)); + m_constant = fold_build2 (is_upper ? MINUS_EXPR : PLUS_EXPR, + TREE_TYPE (m_constant), + m_constant, integer_one_node); + gcc_assert (CONSTANT_CLASS_P (m_constant)); + m_closed = true; + } +} + +/* Get "<=" vs "<" for this bound. */ + +const char * +bound::get_relation_as_str () const +{ + if (m_closed) + return "<="; + else + return "<"; +} + +/* struct range. */ + +/* Dump this range to PP, which must support %E for tree. */ + +void +range::dump (pretty_printer *pp) const +{ +PUSH_IGNORE_WFORMAT + pp_printf (pp, "%qE %s x %s %qE", + m_lower_bound.m_constant, + m_lower_bound.get_relation_as_str (), + m_upper_bound.get_relation_as_str (), + m_upper_bound.m_constant); +POP_IGNORE_WFORMAT +} + +/* Determine if there is only one possible value for this range. + If so, return true and write the constant to *OUT. + Otherwise, return false. */ + +bool +range::constrained_to_single_element (tree *out) +{ + if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound.m_constant))) + return false; + if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound.m_constant))) + return false; + + /* Convert any open bounds to closed bounds. */ + m_lower_bound.ensure_closed (false); + m_upper_bound.ensure_closed (true); + + // Are they equal? + tree comparison + = fold_build2 (EQ_EXPR, boolean_type_node, + m_lower_bound.m_constant, + m_upper_bound.m_constant); + if (comparison == boolean_true_node) + { + *out = m_lower_bound.m_constant; + return true; + } + else + return false; +} + +/* class equiv_class. */ + +/* equiv_class's default ctor. */ + +equiv_class::equiv_class () +: m_constant (NULL_TREE), m_cst_sid (svalue_id::null ()), + m_vars () +{ +} + +/* equiv_class's copy ctor. */ + +equiv_class::equiv_class (const equiv_class &other) +: m_constant (other.m_constant), m_cst_sid (other.m_cst_sid), + m_vars (other.m_vars.length ()) +{ + int i; + svalue_id *sid; + FOR_EACH_VEC_ELT (other.m_vars, i, sid) + m_vars.quick_push (*sid); +} + +/* Print an all-on-one-line representation of this equiv_class to PP, + which must support %E for trees. */ + +void +equiv_class::print (pretty_printer *pp) const +{ + pp_character (pp, '{'); + int i; + svalue_id *sid; + FOR_EACH_VEC_ELT (m_vars, i, sid) + { + if (i > 0) + pp_string (pp, " == "); + sid->print (pp); + } + if (m_constant) + { + if (i > 0) + pp_string (pp, " == "); +PUSH_IGNORE_WFORMAT + pp_printf (pp, "%qE", m_constant); +POP_IGNORE_WFORMAT + } + pp_character (pp, '}'); +} + +/* Generate a hash value for this equiv_class. */ + +hashval_t +equiv_class::hash () const +{ + inchash::hash hstate; + int i; + svalue_id *sid; + + inchash::add_expr (m_constant, hstate); + FOR_EACH_VEC_ELT (m_vars, i, sid) + inchash::add (*sid, hstate); + return hstate.end (); +} + +/* Equality operator for equiv_class. */ + +bool +equiv_class::operator== (const equiv_class &other) +{ + if (m_constant != other.m_constant) + return false; // TODO: use tree equality here? + + /* FIXME: should we compare m_cst_sid? */ + + if (m_vars.length () != other.m_vars.length ()) + return false; + + int i; + svalue_id *sid; + FOR_EACH_VEC_ELT (m_vars, i, sid) + if (! (*sid == other.m_vars[i])) + return false; + + return true; +} + +/* Add SID to this equiv_class, using CM to check if it's a constant. */ + +void +equiv_class::add (svalue_id sid, const constraint_manager &cm) +{ + gcc_assert (!sid.null_p ()); + if (tree cst = cm.maybe_get_constant (sid)) + { + gcc_assert (CONSTANT_CLASS_P (cst)); + /* FIXME: should we canonicalize which svalue is the constant + when there are multiple equal constants? */ + m_constant = cst; + m_cst_sid = sid; + } + m_vars.safe_push (sid); +} + +/* Remove SID from this equivalence class. + Return true if SID was the last var in the equivalence class (suggesting + a possible leak). */ + +bool +equiv_class::del (svalue_id sid) +{ + gcc_assert (!sid.null_p ()); + gcc_assert (sid != m_cst_sid); + + int i; + svalue_id *iv; + FOR_EACH_VEC_ELT (m_vars, i, iv) + { + if (*iv == sid) + { + m_vars[i] = m_vars[m_vars.length () - 1]; + m_vars.pop (); + return m_vars.length () == 0; + } + } + + /* SID must be in the class. */ + gcc_unreachable (); + return false; +} + +/* Get a representative member of this class, for handling cases + where the IDs can change mid-traversal. */ + +svalue_id +equiv_class::get_representative () const +{ + if (!m_cst_sid.null_p ()) + return m_cst_sid; + else + { + gcc_assert (m_vars.length () > 0); + return m_vars[0]; + } +} + +/* Remap all svalue_ids within this equiv_class using MAP. */ + +void +equiv_class::remap_svalue_ids (const svalue_id_map &map) +{ + int i; + svalue_id *iv; + FOR_EACH_VEC_ELT (m_vars, i, iv) + map.update (iv); + map.update (&m_cst_sid); +} + +/* Comparator for use by equiv_class::canonicalize. */ + +static int +svalue_id_cmp_by_id (const void *p1, const void *p2) +{ + const svalue_id *sid1 = (const svalue_id *)p1; + const svalue_id *sid2 = (const svalue_id *)p2; + return sid1->as_int () - sid2->as_int (); +} + +/* Sort the svalues_ids within this equiv_class. */ + +void +equiv_class::canonicalize () +{ + m_vars.qsort (svalue_id_cmp_by_id); +} + +/* Get a debug string for C_OP. */ + +const char * +constraint_op_code (enum constraint_op c_op) +{ + switch (c_op) + { + default: + gcc_unreachable (); + case CONSTRAINT_NE: return "!="; + case CONSTRAINT_LT: return "<"; + case CONSTRAINT_LE: return "<="; + } +} + +/* Convert C_OP to an enum tree_code. */ + +enum tree_code +constraint_tree_code (enum constraint_op c_op) +{ + switch (c_op) + { + default: + gcc_unreachable (); + case CONSTRAINT_NE: return NE_EXPR; + case CONSTRAINT_LT: return LT_EXPR; + case CONSTRAINT_LE: return LE_EXPR; + } +} + +/* Given "lhs C_OP rhs", determine "lhs T_OP rhs". + + For example, given "x < y", then "x > y" is false. */ + +static tristate +eval_constraint_op_for_op (enum constraint_op c_op, enum tree_code t_op) +{ + switch (c_op) + { + default: + gcc_unreachable (); + case CONSTRAINT_NE: + if (t_op == EQ_EXPR) + return tristate (tristate::TS_FALSE); + if (t_op == NE_EXPR) + return tristate (tristate::TS_TRUE); + break; + case CONSTRAINT_LT: + if (t_op == LT_EXPR || t_op == LE_EXPR || t_op == NE_EXPR) + return tristate (tristate::TS_TRUE); + if (t_op == EQ_EXPR || t_op == GT_EXPR || t_op == GE_EXPR) + return tristate (tristate::TS_FALSE); + break; + case CONSTRAINT_LE: + if (t_op == LE_EXPR) + return tristate (tristate::TS_TRUE); + if (t_op == GT_EXPR) + return tristate (tristate::TS_FALSE); + break; + } + return tristate (tristate::TS_UNKNOWN); +} + +/* class constraint. */ + +/* Print this constraint to PP (which must support %E for trees), + using CM to look up equiv_class instances from ids. */ + +void +constraint::print (pretty_printer *pp, const constraint_manager &cm) const +{ + m_lhs.print (pp); + pp_string (pp, ": "); + m_lhs.get_obj (cm).print (pp); + pp_string (pp, " "); + pp_string (pp, constraint_op_code (m_op)); + pp_string (pp, " "); + m_rhs.print (pp); + pp_string (pp, ": "); + m_rhs.get_obj (cm).print (pp); +} + +/* Generate a hash value for this constraint. */ + +hashval_t +constraint::hash () const +{ + inchash::hash hstate; + hstate.add_int (m_lhs.m_idx); + hstate.add_int (m_op); + hstate.add_int (m_rhs.m_idx); + return hstate.end (); +} + +/* Equality operator for constraints. */ + +bool +constraint::operator== (const constraint &other) const +{ + if (m_lhs != other.m_lhs) + return false; + if (m_op != other.m_op) + return false; + if (m_rhs != other.m_rhs) + return false; + return true; +} + +/* class equiv_class_id. */ + +/* Get the underlying equiv_class for this ID from CM. */ + +const equiv_class & +equiv_class_id::get_obj (const constraint_manager &cm) const +{ + return cm.get_equiv_class_by_index (m_idx); +} + +/* Access the underlying equiv_class for this ID from CM. */ + +equiv_class & +equiv_class_id::get_obj (constraint_manager &cm) const +{ + return cm.get_equiv_class_by_index (m_idx); +} + +/* Print this equiv_class_id to PP. */ + +void +equiv_class_id::print (pretty_printer *pp) const +{ + if (null_p ()) + pp_printf (pp, "null"); + else + pp_printf (pp, "ec%i", m_idx); +} + +/* class constraint_manager. */ + +/* constraint_manager's copy ctor. */ + +constraint_manager::constraint_manager (const constraint_manager &other) +: m_equiv_classes (other.m_equiv_classes.length ()), + m_constraints (other.m_constraints.length ()) +{ + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec) + m_equiv_classes.quick_push (new equiv_class (*ec)); + constraint *c; + FOR_EACH_VEC_ELT (other.m_constraints, i, c) + m_constraints.quick_push (*c); +} + +/* constraint_manager's assignment operator. */ + +constraint_manager& +constraint_manager::operator= (const constraint_manager &other) +{ + gcc_assert (m_equiv_classes.length () == 0); + gcc_assert (m_constraints.length () == 0); + + int i; + equiv_class *ec; + m_equiv_classes.reserve (other.m_equiv_classes.length ()); + FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec) + m_equiv_classes.quick_push (new equiv_class (*ec)); + constraint *c; + m_constraints.reserve (other.m_constraints.length ()); + FOR_EACH_VEC_ELT (other.m_constraints, i, c) + m_constraints.quick_push (*c); + + return *this; +} + +/* Generate a hash value for this constraint_manager. */ + +hashval_t +constraint_manager::hash () const +{ + inchash::hash hstate; + int i; + equiv_class *ec; + constraint *c; + + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + hstate.merge_hash (ec->hash ()); + FOR_EACH_VEC_ELT (m_constraints, i, c) + hstate.merge_hash (c->hash ()); + return hstate.end (); +} + +/* Equality operator for constraint_manager. */ + +bool +constraint_manager::operator== (const constraint_manager &other) const +{ + if (m_equiv_classes.length () != other.m_equiv_classes.length ()) + return false; + if (m_constraints.length () != other.m_constraints.length ()) + return false; + + int i; + equiv_class *ec; + + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + if (!(*ec == *other.m_equiv_classes[i])) + return false; + + constraint *c; + + FOR_EACH_VEC_ELT (m_constraints, i, c) + if (!(*c == other.m_constraints[i])) + return false; + + return true; +} + +/* Print this constraint_manager to PP (which must support %E for trees). */ + +void +constraint_manager::print (pretty_printer *pp) const +{ + pp_string (pp, "{"); + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + if (i > 0) + pp_string (pp, ", "); + equiv_class_id (i).print (pp); + pp_string (pp, ": "); + ec->print (pp); + } + pp_string (pp, " | "); + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + if (i > 0) + pp_string (pp, " && "); + c->print (pp, *this); + } + pp_printf (pp, "}"); +} + +/* Dump a multiline representation of this constraint_manager to PP + (which must support %E for trees). */ + +void +constraint_manager::dump_to_pp (pretty_printer *pp) const +{ + // TODO + pp_string (pp, " equiv classes:"); + pp_newline (pp); + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + pp_string (pp, " "); + equiv_class_id (i).print (pp); + pp_string (pp, ": "); + ec->print (pp); + pp_newline (pp); + } + pp_string (pp, " constraints:"); + pp_newline (pp); + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + pp_printf (pp, " %i: ", i); + c->print (pp, *this); + pp_newline (pp); + } +} + +/* Dump a multiline representation of this constraint_manager to FP. */ + +void +constraint_manager::dump (FILE *fp) const +{ + pretty_printer pp; + pp_format_decoder (&pp) = default_tree_printer; + pp_show_color (&pp) = pp_show_color (global_dc->printer); + pp.buffer->stream = fp; + dump_to_pp (&pp); + pp_flush (&pp); +} + +/* Dump a multiline representation of this constraint_manager to stderr. */ + +DEBUG_FUNCTION void +constraint_manager::dump () const +{ + dump (stderr); +} + +/* Dump a multiline representation of CM to stderr. */ + +DEBUG_FUNCTION void +debug (const constraint_manager &cm) +{ + cm.dump (); +} + +/* Attempt to add the constraint LHS OP RHS to this constraint_manager. + Return true if the constraint could be added (or is already true). + Return false if the constraint contradicts existing knowledge. */ + +bool +constraint_manager::add_constraint (svalue_id lhs, + enum tree_code op, + svalue_id rhs) +{ + equiv_class_id lhs_ec_id = get_or_add_equiv_class (lhs); + equiv_class_id rhs_ec_id = get_or_add_equiv_class (rhs); + return add_constraint (lhs_ec_id, op,rhs_ec_id); +} + +/* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this + constraint_manager. + Return true if the constraint could be added (or is already true). + Return false if the constraint contradicts existing knowledge. */ + +bool +constraint_manager::add_constraint (equiv_class_id lhs_ec_id, + enum tree_code op, + equiv_class_id rhs_ec_id) +{ + tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id); + + /* Discard constraints that are already known. */ + if (t.is_true ()) + return true; + + /* Reject unsatisfiable constraints. */ + if (t.is_false ()) + return false; + + gcc_assert (lhs_ec_id != rhs_ec_id); + + /* For now, simply accumulate constraints, without attempting any further + optimization. */ + switch (op) + { + case EQ_EXPR: + { + /* Merge rhs_ec into lhs_ec. */ + equiv_class &lhs_ec_obj = lhs_ec_id.get_obj (*this); + const equiv_class &rhs_ec_obj = rhs_ec_id.get_obj (*this); + + int i; + svalue_id *sid; + FOR_EACH_VEC_ELT (rhs_ec_obj.m_vars, i, sid) + lhs_ec_obj.add (*sid, *this); + + if (rhs_ec_obj.m_constant) + { + //gcc_assert (lhs_ec_obj.m_constant == NULL); + lhs_ec_obj.m_constant = rhs_ec_obj.m_constant; + } + + /* Drop rhs equivalence class, overwriting it with the + final ec (which might be the same one). */ + equiv_class_id final_ec_id = m_equiv_classes.length () - 1; + equiv_class *old_ec = m_equiv_classes[rhs_ec_id.m_idx]; + equiv_class *final_ec = m_equiv_classes.pop (); + if (final_ec != old_ec) + m_equiv_classes[rhs_ec_id.m_idx] = final_ec; + delete old_ec; + + /* Update the constraints. */ + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + /* Update references to the rhs_ec so that + they refer to the lhs_ec. */ + if (c->m_lhs == rhs_ec_id) + c->m_lhs = lhs_ec_id; + if (c->m_rhs == rhs_ec_id) + c->m_rhs = lhs_ec_id; + + /* Renumber all constraints that refer to the final rhs_ec + to the old rhs_ec, where the old final_ec now lives. */ + if (c->m_lhs == final_ec_id) + c->m_lhs = rhs_ec_id; + if (c->m_rhs == final_ec_id) + c->m_rhs = rhs_ec_id; + } + } + break; + case GE_EXPR: + add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id); + break; + case LE_EXPR: + add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id); + break; + case NE_EXPR: + add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id); + break; + case GT_EXPR: + add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id); + break; + case LT_EXPR: + add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id); + break; + default: + /* do nothing. */ + break; + } + validate (); + return true; +} + +/* Subroutine of constraint_manager::add_constraint, for handling all + operations other than equality (for which equiv classes are merged). */ + +void +constraint_manager::add_constraint_internal (equiv_class_id lhs_id, + enum constraint_op c_op, + equiv_class_id rhs_id) +{ + /* Add the constraint. */ + m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id)); + + if (!flag_analyzer_transitivity) + return; + + if (c_op != CONSTRAINT_NE) + { + /* The following can potentially add EQ_EXPR facts, which could lead + to ECs being merged, which would change the meaning of the EC IDs. + Hence we need to do this via representatives. */ + svalue_id lhs = lhs_id.get_obj (*this).get_representative (); + svalue_id rhs = rhs_id.get_obj (*this).get_representative (); + + /* We have LHS is_ordering_p ()) + { + /* Refresh the EC IDs, in case any mergers have happened. */ + lhs_id = get_or_add_equiv_class (lhs); + rhs_id = get_or_add_equiv_class (rhs); + + tree lhs_const = lhs_id.get_obj (*this).m_constant; + tree rhs_const = rhs_id.get_obj (*this).m_constant; + tree other_lhs_const + = other->m_lhs.get_obj (*this).m_constant; + tree other_rhs_const + = other->m_rhs.get_obj (*this).m_constant; + + /* We have "LHS m_lhs + && other->m_rhs == lhs_id) + { + /* We must have equality for this to be possible. */ + gcc_assert (c_op == CONSTRAINT_LE + && other->m_op == CONSTRAINT_LE); + add_constraint (lhs_id, EQ_EXPR, rhs_id); + /* Adding an equality will merge the two ECs and potentially + reorganize the constraints. Stop iterating. */ + return; + } + /* Otherwise, check for transitivity. */ + if (rhs_id == other->m_lhs) + { + /* With RHS == other.lhs, we have: + "LHS m_op == CONSTRAINT_LE)); + tree constant; + if (r.constrained_to_single_element (&constant)) + { + svalue_id cst_sid = get_sid_for_constant (constant); + add_constraint + (rhs_id, EQ_EXPR, + get_or_add_equiv_class (cst_sid)); + return; + } + } + + /* Otherwise, add the constraint implied by transitivity. */ + enum tree_code new_op + = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE) + ? LE_EXPR : LT_EXPR); + add_constraint (lhs_id, new_op, other->m_rhs); + } + else if (other->m_rhs == lhs_id) + { + /* With other.rhs == LHS, we have: + "other.lhs m_op == CONSTRAINT_LE), + bound (rhs_const, + c_op == CONSTRAINT_LE)); + tree constant; + if (r.constrained_to_single_element (&constant)) + { + svalue_id cst_sid = get_sid_for_constant (constant); + add_constraint + (lhs_id, EQ_EXPR, + get_or_add_equiv_class (cst_sid)); + return; + } + } + + /* Otherwise, add the constraint implied by transitivity. */ + enum tree_code new_op + = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE) + ? LE_EXPR : LT_EXPR); + add_constraint (other->m_lhs, new_op, rhs_id); + } + } + } + } +} + +/* Look for SID within the equivalence classes of this constraint_manager; + if found, write the id to *OUT and return true, otherwise return false. */ + +bool +constraint_manager::get_equiv_class_by_sid (svalue_id sid, equiv_class_id *out) const +{ + /* TODO: should we have a map, rather than these searches? */ + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + int j; + svalue_id *iv; + FOR_EACH_VEC_ELT (ec->m_vars, j, iv) + if (*iv == sid) + { + *out = equiv_class_id (i); + return true; + } + } + return false; +} + +/* Ensure that SID has an equivalence class within this constraint_manager; + return the ID of the class. */ + +equiv_class_id +constraint_manager::get_or_add_equiv_class (svalue_id sid) +{ + equiv_class_id result (-1); + + /* Try svalue_id match. */ + if (get_equiv_class_by_sid (sid, &result)) + return result; + + /* Try equality of constants. */ + if (tree cst = maybe_get_constant (sid)) + { + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + if (ec->m_constant) + { + tree eq = fold_build2 (EQ_EXPR, boolean_type_node, + cst, ec->m_constant); + if (eq == boolean_true_node) + { + ec->add (sid, *this); + return equiv_class_id (i); + } + } + } + + + /* Not found. */ + equiv_class *new_ec = new equiv_class (); + new_ec->add (sid, *this); + m_equiv_classes.safe_push (new_ec); + + equiv_class_id new_id (m_equiv_classes.length () - 1); + + if (maybe_get_constant (sid)) + { + /* If we have a new EC for a constant, add constraints comparing this + to other constants we may have (so that we accumulate the transitive + closure of all constraints on constants as the constants are + added). */ + for (equiv_class_id other_id (0); other_id.m_idx < new_id.m_idx; + other_id.m_idx++) + { + const equiv_class &other_ec = other_id.get_obj (*this); + if (other_ec.m_constant) + { + /* If we have two ECs, both with constants, the constants must be + non-equal (or they would be in the same EC). + Determine the direction of the inequality, and record that + fact. */ + tree lt + = fold_build2 (LT_EXPR, boolean_type_node, + new_ec->m_constant, other_ec.m_constant); + //gcc_assert (lt == boolean_true_node || lt == boolean_false_node); + // not true for int vs float comparisons + if (lt == boolean_true_node) + add_constraint_internal (new_id, CONSTRAINT_LT, other_id); + else if (lt == boolean_false_node) + add_constraint_internal (other_id, CONSTRAINT_LT, new_id); + /* Refresh new_id, in case ECs were merged. SID should always + be present by now, so this should never lead to a + recursion. */ + new_id = get_or_add_equiv_class (sid); + } + } + } + + return new_id; +} + +/* Evaluate the condition LHS_EC OP RHS_EC. */ + +tristate +constraint_manager::eval_condition (equiv_class_id lhs_ec, + enum tree_code op, + equiv_class_id rhs_ec) +{ + if (lhs_ec == rhs_ec) + { + switch (op) + { + case EQ_EXPR: + case GE_EXPR: + case LE_EXPR: + return tristate (tristate::TS_TRUE); + + case NE_EXPR: + case GT_EXPR: + case LT_EXPR: + return tristate (tristate::TS_FALSE); + default: + break; + } + } + + tree lhs_const = lhs_ec.get_obj (*this).get_any_constant (); + tree rhs_const = rhs_ec.get_obj (*this).get_any_constant (); + if (lhs_const && rhs_const) + { + tree comparison + = fold_build2 (op, boolean_type_node, lhs_const, rhs_const); + if (comparison == boolean_true_node) + return tristate (tristate::TS_TRUE); + if (comparison == boolean_false_node) + return tristate (tristate::TS_FALSE); + } + + enum tree_code swapped_op = swap_tree_comparison (op); + + int i; + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + if (c->m_lhs == lhs_ec + && c->m_rhs == rhs_ec) + { + tristate result_for_constraint + = eval_constraint_op_for_op (c->m_op, op); + if (result_for_constraint.is_known ()) + return result_for_constraint; + } + /* Swapped operands. */ + if (c->m_lhs == rhs_ec + && c->m_rhs == lhs_ec) + { + tristate result_for_constraint + = eval_constraint_op_for_op (c->m_op, swapped_op); + if (result_for_constraint.is_known ()) + return result_for_constraint; + } + } + + return tristate (tristate::TS_UNKNOWN); +} + +/* Evaluate the condition LHS OP RHS, creating equiv_class instances for + LHS and RHS if they aren't already in equiv_classes. */ + +tristate +constraint_manager::eval_condition (svalue_id lhs, + enum tree_code op, + svalue_id rhs) +{ + return eval_condition (get_or_add_equiv_class (lhs), + op, + get_or_add_equiv_class (rhs)); +} + +/* Delete any information about svalue_id instances identified by P. + Such instances are removed from equivalence classes, and any + redundant ECs and constraints are also removed. + Accumulate stats into STATS. */ + +void +constraint_manager::purge (const purge_criteria &p, purge_stats *stats) +{ + /* Delete any svalue_ids identified by P within the various equivalence + classes. */ + for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); ) + { + equiv_class *ec = m_equiv_classes[ec_idx]; + + int i; + svalue_id *pv; + bool delete_ec = false; + FOR_EACH_VEC_ELT (ec->m_vars, i, pv) + { + if (*pv == ec->m_cst_sid) + continue; + if (p.should_purge_p (*pv)) + { + if (ec->del (*pv)) + if (!ec->m_constant) + delete_ec = true; + } + } + + if (delete_ec) + { + delete ec; + m_equiv_classes.ordered_remove (ec_idx); + if (stats) + stats->m_num_equiv_classes++; + + /* Update the constraints, potentially removing some. */ + for (unsigned con_idx = 0; con_idx < m_constraints.length (); ) + { + constraint *c = &m_constraints[con_idx]; + + /* Remove constraints that refer to the deleted EC. */ + if (c->m_lhs == ec_idx + || c->m_rhs == ec_idx) + { + m_constraints.ordered_remove (con_idx); + if (stats) + stats->m_num_constraints++; + } + else + { + /* Renumber constraints that refer to ECs that have + had their idx changed. */ + c->m_lhs.update_for_removal (ec_idx); + c->m_rhs.update_for_removal (ec_idx); + + con_idx++; + } + } + } + else + ec_idx++; + } + + /* Now delete any constraints that are purely between constants. */ + for (unsigned con_idx = 0; con_idx < m_constraints.length (); ) + { + constraint *c = &m_constraints[con_idx]; + if (m_equiv_classes[c->m_lhs.m_idx]->m_vars.length () == 0 + && m_equiv_classes[c->m_rhs.m_idx]->m_vars.length () == 0) + { + m_constraints.ordered_remove (con_idx); + if (stats) + stats->m_num_constraints++; + } + else + { + con_idx++; + } + } + + /* Finally, delete any ECs that purely contain constants and aren't + referenced by any constraints. */ + for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); ) + { + equiv_class *ec = m_equiv_classes[ec_idx]; + if (ec->m_vars.length () == 0) + { + equiv_class_id ec_id (ec_idx); + bool has_constraint = false; + for (unsigned con_idx = 0; con_idx < m_constraints.length (); + con_idx++) + { + constraint *c = &m_constraints[con_idx]; + if (c->m_lhs == ec_id + || c->m_rhs == ec_id) + { + has_constraint = true; + break; + } + } + if (!has_constraint) + { + delete ec; + m_equiv_classes.ordered_remove (ec_idx); + if (stats) + stats->m_num_equiv_classes++; + + /* Renumber constraints that refer to ECs that have + had their idx changed. */ + for (unsigned con_idx = 0; con_idx < m_constraints.length (); + con_idx++) + { + constraint *c = &m_constraints[con_idx]; + c->m_lhs.update_for_removal (ec_idx); + c->m_rhs.update_for_removal (ec_idx); + } + continue; + } + } + ec_idx++; + } + + validate (); +} + +/* Remap all svalue_ids within this constraint_manager using MAP. */ + +void +constraint_manager::remap_svalue_ids (const svalue_id_map &map) +{ + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + ec->remap_svalue_ids (map); +} + +/* Comparator for use by constraint_manager::canonicalize. + Sort a pair of equiv_class instances, using the representative + svalue_id as a sort key. */ + +static int +equiv_class_cmp (const void *p1, const void *p2) +{ + const equiv_class *ec1 = *(const equiv_class * const *)p1; + const equiv_class *ec2 = *(const equiv_class * const *)p2; + + svalue_id rep1 = ec1->get_representative (); + svalue_id rep2 = ec2->get_representative (); + + return rep1.as_int () - rep2.as_int (); +} + +/* Comparator for use by constraint_manager::canonicalize. + Sort a pair of constraint instances. */ + +static int +constraint_cmp (const void *p1, const void *p2) +{ + const constraint *c1 = (const constraint *)p1; + const constraint *c2 = (const constraint *)p2; + int lhs_cmp = c1->m_lhs.as_int () - c2->m_lhs.as_int (); + if (lhs_cmp) + return lhs_cmp; + int rhs_cmp = c1->m_rhs.as_int () - c2->m_rhs.as_int (); + if (rhs_cmp) + return rhs_cmp; + return c1->m_op - c2->m_op; +} + +/* Reorder the equivalence classes and constraints within this + constraint_manager into a canonical order, to increase the + chances of finding equality with another instance. */ + +void +constraint_manager::canonicalize (unsigned num_svalue_ids) +{ + /* First, sort svalue_ids within the ECs. */ + unsigned i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + ec->canonicalize (); + + /* Next, sort the ECs into a canonical order. */ + + /* We will need to remap the equiv_class_ids in the constraints, + so we need to store the original index of each EC. + Build a lookup table, mapping from representative svalue_id + to the original equiv_class_id of that svalue_id. */ + auto_vec original_ec_id (num_svalue_ids); + for (i = 0; i < num_svalue_ids; i++) + original_ec_id.quick_push (equiv_class_id::null ()); + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + svalue_id rep = ec->get_representative (); + gcc_assert (!rep.null_p ()); + original_ec_id[rep.as_int ()] = i; + } + + /* Sort the equivalence classes. */ + m_equiv_classes.qsort (equiv_class_cmp); + + /* Populate ec_id_map based on the old vs new EC ids. */ + one_way_id_map ec_id_map (m_equiv_classes.length ()); + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + svalue_id rep = ec->get_representative (); + ec_id_map.put (original_ec_id[rep.as_int ()], i); + } + + /* Update the EC ids within the constraints. */ + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + ec_id_map.update (&c->m_lhs); + ec_id_map.update (&c->m_rhs); + } + + /* Finally, sort the constraints. */ + m_constraints.qsort (constraint_cmp); +} + +/* A concrete subclass of constraint_manager for use when + merging two constraint_manager into a third constraint_manager, + each of which has its own region_model. + Calls are delegated to the constraint_manager for the merged model, + and thus affect its region_model. */ + +class cleaned_constraint_manager : public constraint_manager +{ +public: + cleaned_constraint_manager (constraint_manager *merged) : m_merged (merged) {} + + constraint_manager *clone (region_model *) const FINAL OVERRIDE + { + gcc_unreachable (); + } + tree maybe_get_constant (svalue_id sid) const FINAL OVERRIDE + { + return m_merged->maybe_get_constant (sid); + } + svalue_id get_sid_for_constant (tree cst) const FINAL OVERRIDE + { + return m_merged->get_sid_for_constant (cst); + } + virtual int get_num_svalues () const FINAL OVERRIDE + { + return m_merged->get_num_svalues (); + } +private: + constraint_manager *m_merged; +}; + +/* Concrete subclass of fact_visitor for use by constraint_manager::merge. + For every fact in CM_A, see if it is also true in *CM_B. Add such + facts to *OUT. */ + +class merger_fact_visitor : public fact_visitor +{ +public: + merger_fact_visitor (constraint_manager *cm_b, + constraint_manager *out) + : m_cm_b (cm_b), m_out (out) + {} + + void on_fact (svalue_id lhs, enum tree_code code, svalue_id rhs) + FINAL OVERRIDE + { + if (m_cm_b->eval_condition (lhs, code, rhs).is_true ()) + { + bool sat = m_out->add_constraint (lhs, code, rhs); + gcc_assert (sat); + } + } + +private: + constraint_manager *m_cm_b; + constraint_manager *m_out; +}; + +/* Use MERGER to merge CM_A and CM_B into *OUT. + If one thinks of a constraint_manager as a subset of N-dimensional + space, this takes the union of the points of CM_A and CM_B, and + expresses that into *OUT. Alternatively, it can be thought of + as the intersection of the constraints. */ + +void +constraint_manager::merge (const constraint_manager &cm_a, + const constraint_manager &cm_b, + constraint_manager *out, + const model_merger &merger) +{ + gcc_assert (merger.m_sid_mapping); + + /* Map svalue_ids in each equiv class from both sources + to the merged region_model, dropping ids that don't survive merger, + and potentially creating svalues in *OUT for constants. */ + cleaned_constraint_manager cleaned_cm_a (out); + const one_way_svalue_id_map &map_a_to_m + = merger.m_sid_mapping->m_map_from_a_to_m; + clean_merger_input (cm_a, map_a_to_m, &cleaned_cm_a); + + cleaned_constraint_manager cleaned_cm_b (out); + const one_way_svalue_id_map &map_b_to_m + = merger.m_sid_mapping->m_map_from_b_to_m; + clean_merger_input (cm_b, map_b_to_m, &cleaned_cm_b); + + /* At this point, the two cleaned CMs have ECs and constraints referring + to svalues in the merged region model, but both of them have separate + ECs. */ + + /* Merge the equivalence classes and constraints. + The easiest way to do this seems to be to enumerate all of the facts + in cleaned_cm_a, see which are also true in cleaned_cm_b, + and add those to *OUT. */ + merger_fact_visitor v (&cleaned_cm_b, out); + cleaned_cm_a.for_each_fact (&v); +} + +/* A subroutine of constraint_manager::merge. + Use MAP_SID_TO_M to map equivalence classes and constraints from + SM_IN to *OUT. Purge any non-constant svalue_id that don't appear + in the result of MAP_SID_TO_M, purging any ECs and their constraints + that become empty as a result. Potentially create svalues in + the merged region_model for constants that weren't already in use there. */ + +void +constraint_manager:: +clean_merger_input (const constraint_manager &cm_in, + const one_way_svalue_id_map &map_sid_to_m, + constraint_manager *out) +{ + one_way_id_map map_ec_to_m + (cm_in.m_equiv_classes.length ()); + unsigned ec_idx; + equiv_class *ec; + FOR_EACH_VEC_ELT (cm_in.m_equiv_classes, ec_idx, ec) + { + equiv_class cleaned_ec; + if (tree cst = ec->get_any_constant ()) + { + cleaned_ec.m_constant = cst; + /* Lazily create the constant in the out region_model. */ + cleaned_ec.m_cst_sid = out->get_sid_for_constant (cst); + } + unsigned var_idx; + svalue_id *var_in_sid; + FOR_EACH_VEC_ELT (ec->m_vars, var_idx, var_in_sid) + { + svalue_id var_m_sid = map_sid_to_m.get_dst_for_src (*var_in_sid); + if (!var_m_sid.null_p ()) + cleaned_ec.m_vars.safe_push (var_m_sid); + } + if (cleaned_ec.get_any_constant () || !cleaned_ec.m_vars.is_empty ()) + { + map_ec_to_m.put (ec_idx, out->m_equiv_classes.length ()); + out->m_equiv_classes.safe_push (new equiv_class (cleaned_ec)); + } + } + + /* Write out to *OUT any constraints for which both sides survived + cleaning, using the new EC IDs. */ + unsigned con_idx; + constraint *c; + FOR_EACH_VEC_ELT (cm_in.m_constraints, con_idx, c) + { + equiv_class_id new_lhs = map_ec_to_m.get_dst_for_src (c->m_lhs); + if (new_lhs.null_p ()) + continue; + equiv_class_id new_rhs = map_ec_to_m.get_dst_for_src (c->m_rhs); + if (new_rhs.null_p ()) + continue; + out->m_constraints.safe_push (constraint (new_lhs, + c->m_op, + new_rhs)); + } +} + +/* Call VISITOR's on_fact vfunc repeatedly to express the various + equivalence classes and constraints. + This is used by constraint_manager::merge to find the common + facts between two input constraint_managers. */ + +void +constraint_manager::for_each_fact (fact_visitor *visitor) const +{ + /* First, call EQ_EXPR within the various equivalence classes. */ + unsigned ec_idx; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, ec_idx, ec) + { + if (!ec->m_cst_sid.null_p ()) + { + unsigned i; + svalue_id *sid; + FOR_EACH_VEC_ELT (ec->m_vars, i, sid) + visitor->on_fact (ec->m_cst_sid, EQ_EXPR, *sid); + } + for (unsigned i = 0; i < ec->m_vars.length (); i++) + for (unsigned j = i + 1; j < ec->m_vars.length (); j++) + visitor->on_fact (ec->m_vars[i], EQ_EXPR, ec->m_vars[j]); + } + + /* Now, express the various constraints. */ + unsigned con_idx; + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, con_idx, c) + { + const equiv_class &ec_lhs = c->m_lhs.get_obj (*this); + const equiv_class &ec_rhs = c->m_rhs.get_obj (*this); + enum tree_code code = constraint_tree_code (c->m_op); + + if (!ec_lhs.m_cst_sid.null_p ()) + { + for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++) + { + visitor->on_fact (ec_lhs.m_cst_sid, code, ec_rhs.m_vars[j]); + } + } + for (unsigned i = 0; i < ec_lhs.m_vars.length (); i++) + { + if (!ec_rhs.m_cst_sid.null_p ()) + visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_cst_sid); + for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++) + visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_vars[j]); + } + } +} + +/* Assert that this object is valid. */ + +void +constraint_manager::validate () const +{ + /* Skip this in a release build. */ +#if !CHECKING_P + return; +#endif + + int i; + equiv_class *ec; + FOR_EACH_VEC_ELT (m_equiv_classes, i, ec) + { + gcc_assert (ec); + + int j; + svalue_id *sid; + FOR_EACH_VEC_ELT (ec->m_vars, j, sid) + { + gcc_assert (!sid->null_p ()); + gcc_assert (sid->as_int () < get_num_svalues ()); + } + if (ec->m_constant) + gcc_assert (CONSTANT_CLASS_P (ec->m_constant)); +#if 0 + else + gcc_assert (ec->m_vars.length () > 0); +#endif + } + + constraint *c; + FOR_EACH_VEC_ELT (m_constraints, i, c) + { + gcc_assert (!c->m_lhs.null_p ()); + gcc_assert (c->m_lhs.as_int () <= (int)m_equiv_classes.length ()); + gcc_assert (!c->m_rhs.null_p ()); + gcc_assert (c->m_rhs.as_int () <= (int)m_equiv_classes.length ()); + } +} + +#if CHECKING_P + +namespace selftest { + +/* Various constraint_manager selftests. + These have to be written in terms of a region_model, since + the latter is responsible for managing svalue and svalue_id + instances. */ + +/* Verify that setting and getting simple conditions within a region_model + work (thus exercising the underlying constraint_manager). */ + +static void +test_constraint_conditions () +{ + tree int_42 = build_int_cst (integer_type_node, 42); + tree int_0 = build_int_cst (integer_type_node, 0); + + tree x = build_global_decl ("x", integer_type_node); + tree y = build_global_decl ("y", integer_type_node); + tree z = build_global_decl ("z", integer_type_node); + + /* Self-comparisons. */ + { + region_model model; + ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x); + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x); + ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x); + ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x); + } + + /* x == y. */ + { + region_model model; + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y); + + ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x); + + /* Comparison with other var. */ + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z); + } + + /* x == y, then y == z */ + { + region_model model; + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y); + ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z); + + ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z); + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z); + ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z); + ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z); + } + + /* x != y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y); + + ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x); + + /* Comparison with other var. */ + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z); + } + + /* x < y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y); + + ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x); + } + + /* x <= y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y); + + ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x); + } + + /* x > y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y); + + ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x); + ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x); + } + + /* x >= y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y); + + ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y); + + /* Swapped operands. */ + ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x); + ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x); + ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x); + } + + // TODO: implied orderings + + /* Constants. */ + { + region_model model; + ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42); + ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42); + ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42); + ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42); + ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42); + ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42); + } + + /* x == 0, y == 42. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0); + ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42); + + ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y); + ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y); + ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y); + } + + /* Unsatisfiable combinations. */ + + /* x == y && x != y. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y); + ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y); + } + + /* x == 0 then x == 42. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0); + ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42); + } + + /* x == 0 then x != 0. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0); + ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0); + } + + /* x == 0 then x > 0. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0); + ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0); + } + + /* x != y && x == y. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y); + ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y); + } + + /* x <= y && x > y. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y); + ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y); + } + + // etc +} + +/* Test transitivity of conditions. */ + +static void +test_transitivity () +{ + tree a = build_global_decl ("a", integer_type_node); + tree b = build_global_decl ("b", integer_type_node); + tree c = build_global_decl ("c", integer_type_node); + tree d = build_global_decl ("d", integer_type_node); + + /* a == b, then c == d, then c == b. */ + { + region_model model; + ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b); + ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c); + ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d); + ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d); + + ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b); + + ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d); + ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d); + ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d); + + ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b); + ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d); + } + + /* Transitivity: "a < b", "b < c" should imply "a < c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c); + ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a <= b", "b < c" should imply "a < c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c); + ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a <= b", "b <= c" should imply "a <= c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c); + ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a > b", "b > c" should imply "a > c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c); + ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a >= b", "b > c" should imply " a > c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c); + ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a >= b", "b >= c" should imply "a >= c". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c); + ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c); + } + + /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should + imply the easy cases: + (a < c) + (b < d) + but also that: + (a < d). */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b); + ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d); + ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c); + + ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c); + ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d); + ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d); + } + + /* Transitivity: "a >= b", "b >= a" should imply that a == b. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a); + + // TODO: + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b); + } + + /* Transitivity: "a >= b", "b > a" should be impossible. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b); + ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a); + } + + /* Transitivity: "a >= b", "b >= c", "c >= a" should imply + that a == b == c. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c); + ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a); + + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c); + } + + /* Transitivity: "a > b", "b > c", "c > a" + should be impossible. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b); + ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c); + ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a); + } + +} + +/* Test various conditionals involving constants where the results + ought to be implied based on the values of the constants. */ + +static void +test_constant_comparisons () +{ + tree int_3 = build_int_cst (integer_type_node, 3); + tree int_4 = build_int_cst (integer_type_node, 4); + tree int_5 = build_int_cst (integer_type_node, 5); + + tree int_1023 = build_int_cst (integer_type_node, 1023); + tree int_1024 = build_int_cst (integer_type_node, 1024); + + tree a = build_global_decl ("a", integer_type_node); + tree b = build_global_decl ("b", integer_type_node); + + /* Given a >= 1024, then a <= 1023 should be impossible. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024); + ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023); + } + + /* a > 4. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4); + ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4); + ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3); + ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5); + } + + /* a <= 4. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4); + ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4); + ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5); + ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3); + } + + /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b); + ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3); + ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4); + } + + /* Various tests of int ranges where there is only one possible candidate. */ + { + /* If "a <= 4" && "a > 3", then "a == 4", + assuming a is of integral type. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4); + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4); + } + + /* If "a > 3" && "a <= 4", then "a == 4", + assuming a is of integral type. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3); + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4); + } + /* If "a > 3" && "a < 5", then "a == 4", + assuming a is of integral type. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3); + ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4); + } + /* If "a >= 4" && "a < 5", then "a == 4", + assuming a is of integral type. */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4); + ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4); + } + /* If "a >= 4" && "a <= 4", then "a == 4". */ + { + region_model model; + ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4); + ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4); + ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4); + } + } + + /* As above, but for floating-point: + if "f > 3" && "f <= 4" we don't know that f == 4. */ + { + tree f = build_global_decl ("f", double_type_node); + tree float_3 = build_real_from_int_cst (double_type_node, int_3); + tree float_4 = build_real_from_int_cst (double_type_node, int_4); + + region_model model; + ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3); + ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4); + ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, float_4); + ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4); + } +} + +/* Verify various lower-level implementation details about + constraint_manager. */ + +static void +test_constraint_impl () +{ + tree int_42 = build_int_cst (integer_type_node, 42); + tree int_0 = build_int_cst (integer_type_node, 0); + + tree x = build_global_decl ("x", integer_type_node); + tree y = build_global_decl ("y", integer_type_node); + tree z = build_global_decl ("z", integer_type_node); + + /* x == y. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y); + + /* Assert various things about the insides of model. */ + constraint_manager *cm = model.get_constraints (); + ASSERT_EQ (cm->m_constraints.length (), 0); + ASSERT_EQ (cm->m_equiv_classes.length (), 1); + } + + /* y <= z; x == y. */ + { + region_model model; + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + + ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z); + ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y); + + /* Assert various things about the insides of model. */ + constraint_manager *cm = model.get_constraints (); + ASSERT_EQ (cm->m_constraints.length (), 1); + ASSERT_EQ (cm->m_equiv_classes.length (), 2); + + /* Ensure that we merged the constraints. */ + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z); + } + + /* y <= z; y == x. */ + { + region_model model; + ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + + ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z); + ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z); + ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z); + + ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x); + + /* Assert various things about the insides of model. */ + constraint_manager *cm = model.get_constraints (); + ASSERT_EQ (cm->m_constraints.length (), 1); + ASSERT_EQ (cm->m_equiv_classes.length (), 2); + + /* Ensure that we merged the constraints. */ + ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z); + } + + /* x == 0, then x != 42. */ + { + region_model model; + + ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0); + ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42); + + /* Assert various things about the insides of model. */ + constraint_manager *cm = model.get_constraints (); + ASSERT_EQ (cm->m_constraints.length (), 1); + ASSERT_EQ (cm->m_equiv_classes.length (), 2); + ASSERT_EQ (cm->m_constraints[0].m_lhs, + cm->get_or_add_equiv_class (model.get_rvalue (int_0, NULL))); + ASSERT_EQ (cm->m_constraints[0].m_rhs, + cm->get_or_add_equiv_class (model.get_rvalue (int_42, NULL))); + ASSERT_EQ (cm->m_constraints[0].m_op, CONSTRAINT_LT); + } + + // TODO: selftest for merging ecs "in the middle" + // where a non-final one gets overwritten + + // TODO: selftest where there are pre-existing constraints +} + +/* Check that operator== and hashing works as expected for the + various types. */ + +static void +test_equality () +{ + tree x = build_global_decl ("x", integer_type_node); + tree y = build_global_decl ("y", integer_type_node); + + { + region_model model0; + region_model model1; + + constraint_manager *cm0 = model0.get_constraints (); + constraint_manager *cm1 = model1.get_constraints (); + + ASSERT_EQ (cm0->hash (), cm1->hash ()); + ASSERT_EQ (*cm0, *cm1); + + ASSERT_EQ (model0.hash (), model1.hash ()); + ASSERT_EQ (model0, model1); + + ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y); + ASSERT_NE (cm0->hash (), cm1->hash ()); + ASSERT_NE (*cm0, *cm1); + + ASSERT_NE (model0.hash (), model1.hash ()); + ASSERT_NE (model0, model1); + + region_model model2; + constraint_manager *cm2 = model2.get_constraints (); + /* Make the same change to cm2. */ + ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y); + ASSERT_EQ (cm1->hash (), cm2->hash ()); + ASSERT_EQ (*cm1, *cm2); + + ASSERT_EQ (model1.hash (), model2.hash ()); + ASSERT_EQ (model1, model2); + } +} + +/* Verify tracking inequality of a variable against many constants. */ + +static void +test_many_constants () +{ + tree a = build_global_decl ("a", integer_type_node); + + region_model model; + auto_vec constants; + for (int i = 0; i < 20; i++) + { + tree constant = build_int_cst (integer_type_node, i); + constants.safe_push (constant); + ADD_SAT_CONSTRAINT (model, a, NE_EXPR, constant); + + /* Merge, and check the result. */ + region_model other (model); + + region_model merged; + ASSERT_TRUE (model.can_merge_with_p (other, &merged)); + model.canonicalize (NULL); + merged.canonicalize (NULL); + ASSERT_EQ (model, merged); + + for (int j = 0; j <= i; j++) + ASSERT_CONDITION_TRUE (model, a, NE_EXPR, constants[j]); + } +} + +/* Run the selftests in this file, temporarily overriding + flag_analyzer_transitivity with TRANSITIVITY. */ + +static void +run_constraint_manager_tests (bool transitivity) +{ + int saved_flag_analyzer_transitivity = flag_analyzer_transitivity; + flag_analyzer_transitivity = transitivity; + + test_constraint_conditions (); + if (flag_analyzer_transitivity) + { + /* These selftests assume transitivity. */ + test_transitivity (); + test_constant_comparisons (); + } + test_constraint_impl (); + test_equality (); + test_many_constants (); + + flag_analyzer_transitivity = saved_flag_analyzer_transitivity; +} + +/* Run all of the selftests within this file. */ + +void +analyzer_constraint_manager_cc_tests () +{ + /* Run the tests twice: with and without transitivity. */ + run_constraint_manager_tests (true); + run_constraint_manager_tests (false); +} + +} // namespace selftest + +#endif /* CHECKING_P */ + +#endif /* #if ENABLE_ANALYZER */ diff --git a/gcc/analyzer/constraint-manager.h b/gcc/analyzer/constraint-manager.h new file mode 100644 index 000000000000..5b71b3dbd1ce --- /dev/null +++ b/gcc/analyzer/constraint-manager.h @@ -0,0 +1,248 @@ +/* Tracking equivalence classes and constraints at a point on an execution path. + Copyright (C) 2019-2020 Free Software Foundation, Inc. + Contributed by David Malcolm . + +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 +. */ + +#ifndef GCC_ANALYZER_CONSTRAINT_MANAGER_H +#define GCC_ANALYZER_CONSTRAINT_MANAGER_H + +#include "analyzer/region-model.h" // for svalue_id + +class constraint_manager; + +/* Abstract base class for specifying how state should be purged. */ + +class purge_criteria +{ +public: + virtual ~purge_criteria () {} + virtual bool should_purge_p (svalue_id sid) const = 0; +}; + +/* An equivalence class within a constraint manager: a set of + svalue_ids that are known to all be equal to each other, + together with an optional tree constant that they are equal to. */ + +class equiv_class +{ +public: + equiv_class (); + equiv_class (const equiv_class &other); + + hashval_t hash () const; + bool operator== (const equiv_class &other); + + void add (svalue_id sid, const constraint_manager &cm); + bool del (svalue_id sid); + + tree get_any_constant () const { return m_constant; } + + svalue_id get_representative () const; + + void remap_svalue_ids (const svalue_id_map &map); + + void canonicalize (); + + void print (pretty_printer *pp) const; + + /* An equivalence class can contain multiple constants (e.g. multiple + different zeroes, for different types); these are just for the last + constant added. */ + tree m_constant; + svalue_id m_cst_sid; + + // TODO: should this be a set rather than a vec? + auto_vec m_vars; +}; + +/* The various kinds of constraint. */ + +enum constraint_op +{ + CONSTRAINT_NE, + CONSTRAINT_LT, + CONSTRAINT_LE +}; + +const char *constraint_op_code (enum constraint_op c_op); + +/* An ID for an equiv_class within a constraint_manager. Internally, this + is an index into a vector of equiv_class * within the constraint_manager. */ + +class equiv_class_id +{ +public: + static equiv_class_id null () { return equiv_class_id (-1); } + + equiv_class_id (unsigned idx) : m_idx (idx) {} + const equiv_class &get_obj (const constraint_manager &cm) const; + equiv_class &get_obj (constraint_manager &cm) const; + + bool operator== (const equiv_class_id &other) const + { + return m_idx == other.m_idx; + } + bool operator!= (const equiv_class_id &other) const + { + return m_idx != other.m_idx; + } + + bool null_p () const { return m_idx == -1; } + + static equiv_class_id from_int (int idx) { return equiv_class_id (idx); } + int as_int () const { return m_idx; } + + void print (pretty_printer *pp) const; + + void update_for_removal (equiv_class_id other) + { + if (m_idx > other.m_idx) + m_idx--; + } + + int m_idx; +}; + +/* A relationship between two equivalence classes in a constraint_manager. */ + +class constraint +{ + public: + constraint (equiv_class_id lhs, enum constraint_op c_op, equiv_class_id rhs) + : m_lhs (lhs), m_op (c_op), m_rhs (rhs) + { + gcc_assert (!lhs.null_p ()); + gcc_assert (!rhs.null_p ()); + } + + void print (pretty_printer *pp, const constraint_manager &cm) const; + + hashval_t hash () const; + bool operator== (const constraint &other) const; + + /* Is this an ordering, rather than a "!=". */ + bool is_ordering_p () const + { + return m_op != CONSTRAINT_NE; + } + + equiv_class_id m_lhs; + enum constraint_op m_op; + equiv_class_id m_rhs; +}; + +/* An abstract base class for use with constraint_manager::for_each_fact. */ + +class fact_visitor +{ + public: + virtual ~fact_visitor () {} + virtual void on_fact (svalue_id lhs, enum tree_code, svalue_id rhs) = 0; +}; + +/* A collection of equivalence classes and constraints on them. + + Given N svalues, this can be thought of as representing a subset of + N-dimensional space. When we call add_constraint, + we are effectively taking an intersection with that constraint. */ + +class constraint_manager +{ +public: + constraint_manager () {} + constraint_manager (const constraint_manager &other); + virtual ~constraint_manager () {} + + virtual constraint_manager *clone (region_model *) const = 0; + virtual tree maybe_get_constant (svalue_id sid) const = 0; + virtual svalue_id get_sid_for_constant (tree cst) const = 0; + virtual int get_num_svalues () const = 0; + + constraint_manager& operator= (const constraint_manager &other); + + hashval_t hash () const; + bool operator== (const constraint_manager &other) const; + bool operator!= (const constraint_manager &other) const + { + return !(*this == other); + } + + void print (pretty_printer *pp) const; + void dump_to_pp (pretty_printer *pp) const; + void dump (FILE *fp) const; + void dump () const; + + const equiv_class &get_equiv_class_by_index (unsigned idx) const + { + return *m_equiv_classes[idx]; + } + equiv_class &get_equiv_class_by_index (unsigned idx) + { + return *m_equiv_classes[idx]; + } + + equiv_class &get_equiv_class (svalue_id sid) + { + equiv_class_id ec_id = get_or_add_equiv_class (sid); + return ec_id.get_obj (*this); + } + + bool add_constraint (svalue_id lhs, enum tree_code op, svalue_id rhs); + + bool add_constraint (equiv_class_id lhs_ec_id, + enum tree_code op, + equiv_class_id rhs_ec_id); + + bool get_equiv_class_by_sid (svalue_id sid, equiv_class_id *out) const; + equiv_class_id get_or_add_equiv_class (svalue_id sid); + tristate eval_condition (equiv_class_id lhs, + enum tree_code op, + equiv_class_id rhs); + tristate eval_condition (svalue_id lhs, + enum tree_code op, + svalue_id rhs); + + void purge (const purge_criteria &p, purge_stats *stats); + + void remap_svalue_ids (const svalue_id_map &map); + + void canonicalize (unsigned num_svalue_ids); + + static void merge (const constraint_manager &cm_a, + const constraint_manager &cm_b, + constraint_manager *out, + const model_merger &merger); + + void for_each_fact (fact_visitor *) const; + + void validate () const; + + auto_delete_vec m_equiv_classes; + auto_vec m_constraints; + + private: + static void clean_merger_input (const constraint_manager &cm_in, + const one_way_svalue_id_map &map_sid_to_m, + constraint_manager *out); + + void add_constraint_internal (equiv_class_id lhs_id, + enum constraint_op c_op, + equiv_class_id rhs_id); +}; + +#endif /* GCC_ANALYZER_CONSTRAINT_MANAGER_H */