public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
From: David Malcolm <dmalcolm@redhat.com>
To: gcc-patches@gcc.gnu.org
Subject: [committed] analyzer: fix ICE when merging constraints w/o transitivity [PR96650]
Date: Tue, 15 Sep 2020 17:48:37 -0400	[thread overview]
Message-ID: <20200915214837.9934-1-dmalcolm@redhat.com> (raw)

PR analyzer/96650 reports an assertion failure when merging the
intersection of two sets of constraints, due to the resulting
constraints being infeasible.

It turns out that the two input sets were each infeasible if
transitivity were considered, but -fanalyzer-transitivity was off.
However for this case, the merging code was "discovering" the
transitive infeasibility of the intersection of the constraints even
when -fanalyzer-transitivity is off, triggering an assertion failure.

I attempted various fixes for this, but each of them would have
introduced O(N^2) logic into the constraint-handling code into the
-fno-analyzer-transitivity case (with N == the number of constraints).

This patch fixes the ICE by tweaking the assertion, so that we
silently drop such constraints if -fanalyzer-transitivity is off.

Successfully bootstrapped & regrtested on x86_64-pc-linux-gnu.
Pushed to master as r11-3212-g50ddbd0282e06614b29f0d3f3be5fbe70085a8bd.

gcc/analyzer/ChangeLog:
	PR analyzer/96650
	* constraint-manager.cc (merger_fact_visitor::on_fact): Replace
	assertion that add_constraint succeeded with an assertion that
	if it fails, -fanalyzer-transitivity is off.

gcc/testsuite/ChangeLog:
	PR analyzer/96650
	* gcc.dg/analyzer/pr96650-1-notrans.c: New test.
	* gcc.dg/analyzer/pr96650-1-trans.c: New test.
	* gcc.dg/analyzer/pr96650-2-notrans.c: New test.
	* gcc.dg/analyzer/pr96650-2-trans.c: New test.
---
 gcc/analyzer/constraint-manager.cc            | 10 ++++++-
 .../gcc.dg/analyzer/pr96650-1-notrans.c       | 30 +++++++++++++++++++
 .../gcc.dg/analyzer/pr96650-1-trans.c         | 30 +++++++++++++++++++
 .../gcc.dg/analyzer/pr96650-2-notrans.c       | 30 +++++++++++++++++++
 .../gcc.dg/analyzer/pr96650-2-trans.c         | 30 +++++++++++++++++++
 5 files changed, 129 insertions(+), 1 deletion(-)
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/pr96650-1-notrans.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/pr96650-1-trans.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/pr96650-2-notrans.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/pr96650-2-trans.c

diff --git a/gcc/analyzer/constraint-manager.cc b/gcc/analyzer/constraint-manager.cc
index e578e0502f2..521501fd4f4 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -1752,7 +1752,15 @@ public:
     if (m_cm_b->eval_condition (lhs, code, rhs).is_true ())
       {
 	bool sat = m_out->add_constraint (lhs, code, rhs);
-	gcc_assert (sat);
+	if (!sat)
+	  {
+	    /* If -fanalyzer-transitivity is off, we can encounter cases
+	       where at least one of the two constraint_managers being merged
+	       is infeasible, but we only discover that infeasibility
+	       during merging (PR analyzer/96650).
+	       Silently drop such constraints.  */
+	    gcc_assert (!flag_analyzer_transitivity);
+	  }
       }
   }
 
diff --git a/gcc/testsuite/gcc.dg/analyzer/pr96650-1-notrans.c b/gcc/testsuite/gcc.dg/analyzer/pr96650-1-notrans.c
new file mode 100644
index 00000000000..94c755540b0
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/pr96650-1-notrans.c
@@ -0,0 +1,30 @@
+/* { dg-additional-options "-O2 -fno-analyzer-transitivity" } */
+
+int *wf;
+
+void
+yd (void);
+
+int
+cy (void);
+
+int *
+ee (int hp)
+{
+  if (hp != 0)
+    yd ();
+
+  return 0;
+}
+
+void
+z0 (int co)
+{
+  int l4 = sizeof (int);
+
+ aq:
+  wf = ee (l4);
+  if (l4 < co)
+    l4 = cy () + sizeof (int);
+  goto aq;
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/pr96650-1-trans.c b/gcc/testsuite/gcc.dg/analyzer/pr96650-1-trans.c
new file mode 100644
index 00000000000..b20630bb806
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/pr96650-1-trans.c
@@ -0,0 +1,30 @@
+/* { dg-additional-options "-O2 -fanalyzer-transitivity" } */
+
+int *wf;
+
+void
+yd (void);
+
+int
+cy (void);
+
+int *
+ee (int hp)
+{
+  if (hp != 0)
+    yd ();
+
+  return 0;
+}
+
+void
+z0 (int co)
+{
+  int l4 = sizeof (int);
+
+ aq:
+  wf = ee (l4);
+  if (l4 < co)
+    l4 = cy () + sizeof (int);
+  goto aq;
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/pr96650-2-notrans.c b/gcc/testsuite/gcc.dg/analyzer/pr96650-2-notrans.c
new file mode 100644
index 00000000000..fc7c045a32f
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/pr96650-2-notrans.c
@@ -0,0 +1,30 @@
+/* { dg-additional-options "-fno-analyzer-transitivity" } */
+
+#include "analyzer-decls.h"
+
+int foo (void);
+
+/* Infeasible path, requiring transitivity to find.  */
+
+void test_1 (int co, int y)
+{
+  if (4 < co)
+    if (co < y)
+      if (y == 0)
+	__analyzer_dump_path (); /* { dg-message "path" } */
+}
+
+/* Infeasible path, requiring transitivity to find, with a merger.  */
+
+void test_2 (int co, int y, int z)
+{
+  if (4 < co)
+    if (co < y)
+      if (y == 0)
+	{
+	  while (foo ())
+	    {
+	    }
+	  __analyzer_dump_path (); /* { dg-message "path" } */
+	}
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/pr96650-2-trans.c b/gcc/testsuite/gcc.dg/analyzer/pr96650-2-trans.c
new file mode 100644
index 00000000000..8d0c2950876
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/pr96650-2-trans.c
@@ -0,0 +1,30 @@
+/* { dg-additional-options "-fanalyzer-transitivity" } */
+
+#include "analyzer-decls.h"
+
+int foo (void);
+
+/* Infeasible path, requiring transitivity to find.  */
+
+void test_1 (int co, int y)
+{
+  if (4 < co)
+    if (co < y)
+      if (y == 0)
+	__analyzer_dump_path (); /* { dg-bogus "path" } */
+}
+
+/* Infeasible path, requiring transitivity to find, with a merger.  */
+
+void test_2 (int co, int y, int z)
+{
+  if (4 < co)
+    if (co < y)
+      if (y == 0)
+	{
+	  while (foo ())
+	    {
+	    }
+	  __analyzer_dump_path (); /* { dg-bogus "path" } */
+	}
+}
-- 
2.26.2


                 reply	other threads:[~2020-09-15 21:48 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20200915214837.9934-1-dmalcolm@redhat.com \
    --to=dmalcolm@redhat.com \
    --cc=gcc-patches@gcc.gnu.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).