From ce9b84b6062fe1c97b4650e601014df65d6fb7c9 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Tue, 21 Jan 2020 10:31:22 -0500
Subject: [PATCH 03/68] analyzer: fix ICE in __builtin_isnan (PR 93356)

PR analyzer/93356 reports an ICE handling __builtin_isnan due to a
failing assertion:
  674     gcc_assert (lhs_ec_id != rhs_ec_id);
with op=UNORDERED_EXPR.
when attempting to add an UNORDERED_EXPR constraint.

This is an overzealous assertion, but underlying it are various forms of
sloppiness regarding NaN within the analyzer:

  (a) the assumption in the constraint_manager that equivalence classes
  are reflexive (X == X), which isn't the case for NaN.

  (b) Hardcoding the "honor_nans" param to false when calling
  invert_tree_comparison throughout the analyzer.

  (c) Ignoring ORDERED_EXPR, UNORDERED_EXPR, and the UN-prefixed
  comparison codes.

This patch tackles these issues by:

  (i) adding an "is nan" tristate to equivalence classes: if it's known
  to be false (which is the case if any non-floating values are in the
  class, or if it has more than one value), then it is self-equal; if
  it's known to be true then X != X is known

  (ii) adding a region_model::maybe_honor_nans method for use when
  calling invert_tree_comparison, which uses HONOR_NANS, but also
  returns false for the case where we know that neither argument is NaN

  (iii) handling the ORDERED_EXPR, UNORDERED_EXPR, and the UN-prefixed
  comparison codes

  (iv) reworking the constraint-handling to eliminate the failing
  assertion, fixing the ICE

Note that (i) effectively extends the data model to track the NaN-ness
of floating-point values, so there are some additional code and tests to
ensure that state-merging can cope with the new information, and that
the richer state doesn't bloat the exploded graphs for any of the
existing tests.

gcc/analyzer/ChangeLog:
	PR analyzer/93356
	* analyzer-selftests.cc (selftest::build_real_cst_from_string):
	Move here from region-model.cc and make non-static.
	* analyzer-selftests.h (selftest::build_real_cst_from_string):
	New decl.
	* checker-path.cc
	(start_cfg_edge_event::maybe_describe_condition): When inverting
	the comparison for false edges, use HONOR_NANS.  Handle
	ERROR_MARK.
	* constraint-manager.cc (equiv_class::equiv_class): Handle new
	field m_is_nan in default ctor and copy ctor.
	(equiv_class::hash): Handle new field m_is_nan.
	(equiv_class::operator==): Likewise.
	(cst_is_nan): New function.
	(equiv_class::add): When adding a constant, call cst_is_nan and
	use the result to set m_is_nan on the equiv_class.  When adding
	more than one value to an ec, or a non-float value, set m_is_nan
	to false.
	(constraint_manager::print): Print m_is_nan of each ec.
	(constraint_manager::dump_to_pp): Likewise.
	(constraint_manager::add_constraint): Assert that op is a
	tcc_comparison in both overloads.  For the equiv_class_id
	overload: remove assertion that we have two different IDs.
	For EQ_EXPR, set m_is_nan to false, and bail early if we
	have self-equality.  For GE_EXPR and GT_EXPR, note that neither
	can be NaN and so it's legitimate to flip the constraint.
	For NE_EXPR, handle self-comparison by setting m_is_nan to true
	and not calling add_constraint_internal.  Handle the UN-prefixed
	codes by checking to see if both are known to be non-NaN and
	failing gracefully otherwise.  Handle ORDERED_EXPR and
	UNORDERED_EXPR.  Mark the default case as unreachable as we should
	now be handling all tcc_comparison codes.
	(constraint_manager::add_constraint_internal): Add assertion that
	we have two different EC IDS.  Set m_is_nan to false is we have
	a non-!= constraint.
	(constraint_manager::get_or_add_equiv_class): Only accumulate
	inter-constant constraints when both constraints are known to
	be non-NaN.
	(constraint_manager::eval_condition): For the EC overload,
	determine if either input could be NaN.  Use this to handle
	ORDERED_EXPR and UNORDERED_EXPR, and other comparisons.  Guard the
	self-comparison shortcut by a check that neither is NaN.
	For the svalue_id overload, assert that op is a tcc_comparison.
	(constraint_manager::eval_condition): Likewise.
	(constraint_manager::maybe_nan): New.
	(cleaned_constraint_manager::get_type): New.
	(clean_merger_input): Propagate m_is_nan to the cleaned_ec for
	those ECs that have a FLOAT_TYPE_P value.
	(constraint_manager::for_each_fact): If m_is_nan in known for an
	EC, call on_fact on the EC compared with itself with NE_EXPR or
	EQ_EXPR as appropriate.
	(constraint_manager::validate): Assert that if EC has a constant,
	then the NaN-ness of the EC is known and reflects that of the
	constant.
	(selftest::real_str_is_nan): New helper function.
	(selftest::test_cst_is_nan): New test.
	(selftest::test_constant_comparisons): Assert that e.g. "f > 3"
	implies that f can't be NaN.
	(selftest::test_nan_comparisons): New test.
	(selftest::run_constraint_manager_tests): Call
	selftest::test_nan_comparisons.
	(selftest::analyzer_constraint_manager_cc_tests): Call
	selftest::test_cst_is_nan.
	* constraint-manager.h (class equiv_class): Update leading comment
	to describe NaN-handling.
	(equiv_class::get_is_nan): New.
	(equiv_class::set_is_nan): New.
	(equiv_class::m_is_nan): New.
	(constraint_manager::get_type): New vfunc.
	(constraint_manager::maybe_nan): New member function.
	* region-model.cc (impl_constraint_manager::get_type): New.
	(region_model::maybe_honor_nans): New.
	(tree_and_sid): New typedef.
	(dump_vec_of_tree): Rename to...
	(dump_vec_of_tree_and_sid): ...this, converting vec param's type
	from tree to tree_and_sid, and adding constraint_manager and
	show_isnan params.  Use the new params to optionally show the
	NaN-ness of each floating-point value.
	(region_model::dump_summary_of_map): Update for above change.
	(region_model::on_assignment): Handle ORDERED_EXPR and
	UNORDERED_EXPR.
	(region_model::eval_condition): Assert that op is a
	tcc_comparison.
	(region_model::eval_condition_without_cm): Likewise.  Update
	the handling of self-comparison of an svalue to check for
	non-floating types before assuming self-equality.
	(region_model::add_constraint): Assert that op is a
	tcc_comparison.
	(region_model::add_any_constraints_from_ssa_def_stmt):
	Likewise.  When calling invert_tree_comparison, call
	maybe_honor_nans, and handle ERROR_MARK.
	(region_model::eval_condition): Assert that op is a
	tcc_comparison.
	(region_model::apply_constraints_for_gcond): When calling
	invert_tree_comparison, call maybe_honor_nans, and handle
	ERROR_MARK.
	(selftest::build_real_cst_from_string): Move to
	analyzer-selftests.cc.
	(selftest::test_dump_2): New test.
	(selftest::test_constraint_merging_2): New test.
	(selftest::analyzer_region_model_cc_tests): Call the new tests.
	* region-model.h (region_model::maybe_honor_nans): New decl.

gcc/testsuite/ChangeLog:
	PR analyzer/93356
	* gcc.dg/analyzer/complex.c: New test.
	* gcc.dg/analyzer/float-fast.c: New test.
	* gcc.dg/analyzer/float.c: New test.
	* gcc.dg/analyzer/torture/nan-notrap.c: New test.
	* gcc.dg/analyzer/torture/nan.c: New test.

gcc/ChangeLog:
	PR analyzer/93356
	* doc/analyzer.texi (Limitations): Remove item about the
	constraint manager assuming reflexivity.
	* tristate.cc (selftest::test_ctors): Test is_unknown.
	* tristate.h (tristate::is_unknown): New.
	(tristate::get_value): New.
---
 gcc/analyzer/analyzer-selftests.cc            |  10 +
 gcc/analyzer/analyzer-selftests.h             |   1 +
 gcc/analyzer/checker-path.cc                  |   6 +-
 gcc/analyzer/constraint-manager.cc            | 304 ++++++++++++++++--
 gcc/analyzer/constraint-manager.h             |  30 +-
 gcc/analyzer/region-model.cc                  | 236 ++++++++++++--
 gcc/analyzer/region-model.h                   |   2 +
 gcc/doc/analyzer.texi                         |   3 -
 gcc/testsuite/gcc.dg/analyzer/complex.c       |  18 ++
 gcc/testsuite/gcc.dg/analyzer/float-fast.c    |  13 +
 gcc/testsuite/gcc.dg/analyzer/float.c         |  56 ++++
 .../gcc.dg/analyzer/torture/nan-notrap.c      | 176 ++++++++++
 gcc/testsuite/gcc.dg/analyzer/torture/nan.c   | 175 ++++++++++
 gcc/tristate.cc                               |   3 +
 gcc/tristate.h                                |   3 +
 15 files changed, 986 insertions(+), 50 deletions(-)
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/complex.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/float-fast.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/float.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/torture/nan-notrap.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/torture/nan.c

diff --git a/gcc/analyzer/analyzer-selftests.cc b/gcc/analyzer/analyzer-selftests.cc
index 8e200a3844b..43ab04886d4 100644
--- a/gcc/analyzer/analyzer-selftests.cc
+++ b/gcc/analyzer/analyzer-selftests.cc
@@ -45,6 +45,16 @@ build_global_decl (const char *name, tree type)
   return decl;
 }
 
+/* Build a constant tree of the given type from STR.  */
+
+tree
+build_real_cst_from_string (tree type, const char *str)
+{
+  REAL_VALUE_TYPE real;
+  real_from_string (&real, str);
+  return build_real (type, real);
+}
+
 /* Run all analyzer-specific selftests.  */
 
 void
diff --git a/gcc/analyzer/analyzer-selftests.h b/gcc/analyzer/analyzer-selftests.h
index 7924b8c8f01..9b26ac88524 100644
--- a/gcc/analyzer/analyzer-selftests.h
+++ b/gcc/analyzer/analyzer-selftests.h
@@ -28,6 +28,7 @@ namespace ana {
 namespace selftest {
 
 extern tree build_global_decl (const char *name, tree type);
+extern tree build_real_cst_from_string (tree type, const char *str);
 
 extern void run_analyzer_selftests ();
 
diff --git a/gcc/analyzer/checker-path.cc b/gcc/analyzer/checker-path.cc
index 7f6cdf599cf..0c234a698e7 100644
--- a/gcc/analyzer/checker-path.cc
+++ b/gcc/analyzer/checker-path.cc
@@ -504,7 +504,11 @@ start_cfg_edge_event::maybe_describe_condition (bool can_colorize) const
 	  tree lhs = gimple_cond_lhs (cond_stmt);
 	  tree rhs = gimple_cond_rhs (cond_stmt);
 	  if (cfg_sedge.false_value_p ())
-	    op = invert_tree_comparison (op, false /* honor_nans */);
+	    {
+	      op = invert_tree_comparison (op, HONOR_NANS (lhs));
+	      if (op == ERROR_MARK)
+		return label_text::borrow (NULL);
+	    }
 	  return maybe_describe_condition (can_colorize,
 					   lhs, op, rhs);
 	}
diff --git a/gcc/analyzer/constraint-manager.cc b/gcc/analyzer/constraint-manager.cc
index 777bd1b13c9..8594643e416 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -164,7 +164,7 @@ range::constrained_to_single_element (tree *out)
 
 equiv_class::equiv_class ()
 : m_constant (NULL_TREE), m_cst_sid (svalue_id::null ()),
-  m_vars ()
+  m_vars (), m_is_nan (tristate::TS_UNKNOWN)
 {
 }
 
@@ -172,7 +172,7 @@ equiv_class::equiv_class ()
 
 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 ())
+  m_vars (other.m_vars.length ()), m_is_nan (other.m_is_nan)
 {
   int i;
   svalue_id *sid;
@@ -216,6 +216,7 @@ equiv_class::hash () const
   inchash::add_expr (m_constant, hstate);
   FOR_EACH_VEC_ELT (m_vars, i, sid)
     inchash::add (*sid, hstate);
+  hstate.add_int ((unsigned)m_is_nan.get_value ());
   return hstate.end ();
 }
 
@@ -238,9 +239,27 @@ equiv_class::operator== (const equiv_class &other)
     if (! (*sid == other.m_vars[i]))
       return false;
 
+  if (m_is_nan != other.m_is_nan)
+    return false;
+
   return true;
 }
 
+/* Return true if CST is NaN.  */
+
+static bool
+cst_is_nan (tree cst)
+{
+  if (!FLOAT_TYPE_P (TREE_TYPE (cst)))
+    return false;
+  tree tem = fold_binary (UNORDERED_EXPR, integer_type_node, cst, cst);
+  gcc_assert (tem);
+  if (integer_onep (tem))
+    return true;
+  else
+    return false;
+}
+
 /* Add SID to this equiv_class, using CM to check if it's a constant.  */
 
 void
@@ -254,6 +273,26 @@ equiv_class::add (svalue_id sid, const constraint_manager &cm)
 	 when there are multiple equal constants?  */
       m_constant = cst;
       m_cst_sid = sid;
+      if (cst_is_nan (cst))
+	{
+	  gcc_assert (m_vars.length () == 0);
+	  set_is_nan (true);
+	}
+      else
+	set_is_nan (false);
+    }
+  else
+    {
+      /* If we have equality between two or more values, then they're
+	 not NaN.  */
+      if (m_vars.length () > 0)
+	set_is_nan (false);
+      else if (get_is_nan ().is_unknown ())
+	{
+	  tree type = cm.get_type (sid);
+	  if (type && !FLOAT_TYPE_P (type))
+	    set_is_nan (false);
+	}
     }
   m_vars.safe_push (sid);
 }
@@ -563,6 +602,7 @@ constraint_manager::print (pretty_printer *pp) const
       equiv_class_id (i).print (pp);
       pp_string (pp, ": ");
       ec->print (pp);
+      pp_printf (pp, " (isnan: %s)", ec->get_is_nan ().as_string ());
     }
   pp_string (pp, "  |  ");
   constraint *c;
@@ -592,6 +632,7 @@ constraint_manager::dump_to_pp (pretty_printer *pp) const
       equiv_class_id (i).print (pp);
       pp_string (pp, ": ");
       ec->print (pp);
+      pp_printf (pp, " (isnan: %s)", ec->get_is_nan ().as_string ());
       pp_newline (pp);
     }
   pp_string (pp, "  constraints:");
@@ -643,6 +684,8 @@ constraint_manager::add_constraint (svalue_id lhs,
 				    enum tree_code op,
 				    svalue_id rhs)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   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);
@@ -658,6 +701,8 @@ constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
 				    enum tree_code op,
 				    equiv_class_id rhs_ec_id)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
 
   /* Discard constraints that are already known.  */
@@ -668,16 +713,24 @@ constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
   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);
+
+	/* If we have equality, then it's not NaN.  */
+	lhs_ec_obj.set_is_nan (false);
+
+	if (lhs_ec_id == rhs_ec_id)
+	  {
+	    validate ();
+	    return true;
+	  }
+
+	/* Merge rhs_ec into lhs_ec.  */
 	const equiv_class &rhs_ec_obj = rhs_ec_id.get_obj (*this);
 
 	int i;
@@ -721,22 +774,60 @@ constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
       }
       break;
     case GE_EXPR:
+      /* Neither can be NaN.  Flip the constraint.  */
       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);
+      if (lhs_ec_id == rhs_ec_id)
+	  {
+	    /* It's NaN.  */
+	    lhs_ec_id.get_obj (*this).set_is_nan (true);
+	  }
+      else
+	add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
       break;
     case GT_EXPR:
+      /* Neither can be NaN.  Flip the constraint.  */
       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;
+
+    case UNEQ_EXPR:
+    case UNGT_EXPR:
+    case UNGE_EXPR:
+    case UNLT_EXPR:
+    case UNLE_EXPR:
+      /* If both are known to be not NaN, then we can invert the condition
+	 without honoring NaNs.  */
+      if ((lhs_ec_id.get_obj (*this).get_is_nan ()
+	   || lhs_ec_id.get_obj (*this).get_is_nan ()).is_false ())
+	{
+	  enum tree_code inv_op = invert_tree_comparison (op, false);
+	  gcc_assert (TREE_CODE_CLASS (inv_op) == tcc_comparison);
+	  add_constraint (rhs_ec_id, inv_op, lhs_ec_id);
+	}
+      /* Otherwise, do nothing; we don't have a way of representing this.  */
+      break;
+
+    case ORDERED_EXPR:
+      /* Both are not NaN.  */
+      lhs_ec_id.get_obj (*this).set_is_nan (false);
+      rhs_ec_id.get_obj (*this).set_is_nan (false);
+      break;
+    case UNORDERED_EXPR:
+      /* At least one is NaN; if self-comparison then it's NaN.  */
+      if (lhs_ec_id == rhs_ec_id)
+	lhs_ec_id.get_obj (*this).set_is_nan (true);
+      break;
+
     default:
-      /* do nothing.  */
+      /* All tcc_comparison should have been handled in cases above.  */
+      gcc_unreachable ();
       break;
     }
   validate ();
@@ -751,9 +842,18 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 					     enum constraint_op c_op,
 					     equiv_class_id rhs_id)
 {
+  gcc_assert (lhs_id != rhs_id);
+
   /* Add the constraint.  */
   m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id));
 
+  /* If we have a < or <= constraint, then neither can be NaN.  */
+  if (c_op != CONSTRAINT_NE)
+    {
+      lhs_id.get_obj (*this).set_is_nan (false);
+      rhs_id.get_obj (*this).set_is_nan (false);
+    }
+
   if (!flag_analyzer_transitivity)
     return;
 
@@ -958,10 +1058,12 @@ constraint_manager::get_or_add_equiv_class (svalue_id sid)
 	   other_id.m_idx++)
 	{
 	  const equiv_class &other_ec = other_id.get_obj (*this);
-	  if (other_ec.m_constant)
+	  if (other_ec.m_constant
+	      && new_ec->get_is_nan ().is_false ()
+	      && other_ec.get_is_nan ().is_false ())
 	    {
 	      /* If we have two ECs, both with constants, the constants must be
-		 non-equal (or they would be in the same EC).
+		 non-equal (or they would be in the same EC), or they are NaN.
 		 Determine the direction of the inequality, and record that
 		 fact.  */
 	      tree lt
@@ -991,26 +1093,65 @@ constraint_manager::eval_condition (equiv_class_id lhs_ec,
 				    enum tree_code op,
 				    equiv_class_id rhs_ec)
 {
-  if (lhs_ec == rhs_ec)
+  const equiv_class &lhs_ec_obj = lhs_ec.get_obj (*this);
+  const equiv_class &rhs_ec_obj = rhs_ec.get_obj (*this);
+
+  tristate either_is_nan = (lhs_ec_obj.get_is_nan ()
+			    || rhs_ec_obj.get_is_nan ());
+
+  switch (op)
+    {
+    case ORDERED_EXPR:
+      return !either_is_nan;
+    case UNORDERED_EXPR:
+      return either_is_nan;
+    default:
+      break;
+    }
+
+  if (either_is_nan.is_true ())
     {
+      /* One or both values is NaN: most comparisons are false.  */
       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);
+	case NE_EXPR:
+	  return tristate (tristate::TS_TRUE);
 	default:
 	  break;
 	}
     }
+  else if (either_is_nan.is_false ())
+    {
+      /* Both values are known to be not NaN.  */
+      if (lhs_ec == rhs_ec)
+	{
+	  /* Self-comparison when we know it's not NaN.  */
+	  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 ();
+  tree lhs_const = lhs_ec_obj.get_any_constant ();
+  tree rhs_const = rhs_ec_obj.get_any_constant ();
   if (lhs_const && rhs_const)
     {
       tree comparison
@@ -1057,11 +1198,21 @@ constraint_manager::eval_condition (svalue_id lhs,
 				    enum tree_code op,
 				    svalue_id rhs)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
   return eval_condition (get_or_add_equiv_class (lhs),
 			 op,
 			 get_or_add_equiv_class (rhs));
 }
 
+/* Return true if SID could be NaN.  */
+
+bool
+constraint_manager::maybe_nan (svalue_id sid)
+{
+  equiv_class_id ec_id = get_or_add_equiv_class (sid);
+  return !ec_id.get_obj (*this).get_is_nan ().is_false ();
+}
+
 /* 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.
@@ -1303,6 +1454,10 @@ public:
   {
     return m_merged->maybe_get_constant (sid);
   }
+  tree get_type (svalue_id sid) const FINAL OVERRIDE
+  {
+    return m_merged->get_type (sid);
+  }
   svalue_id get_sid_for_constant (tree cst) const FINAL OVERRIDE
   {
     return m_merged->get_sid_for_constant (cst);
@@ -1401,11 +1556,14 @@ clean_merger_input (const constraint_manager &cm_in,
   FOR_EACH_VEC_ELT (cm_in.m_equiv_classes, ec_idx, ec)
     {
       equiv_class cleaned_ec;
+      bool has_float = false;
       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);
+	  if (FLOAT_TYPE_P (TREE_TYPE (cst)))
+	    has_float = true;
 	}
       unsigned var_idx;
       svalue_id *var_in_sid;
@@ -1413,10 +1571,17 @@ clean_merger_input (const constraint_manager &cm_in,
 	{
 	  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);
+	    {
+	      cleaned_ec.m_vars.safe_push (var_m_sid);
+	      tree type = cm_in.get_type (*var_in_sid);
+	      if (type && FLOAT_TYPE_P (type))
+		has_float = true;
+	    }
 	}
       if (cleaned_ec.get_any_constant () || !cleaned_ec.m_vars.is_empty ())
 	{
+	  if (ec->get_is_nan ().is_known () && has_float)
+	    cleaned_ec.set_is_nan (ec->get_is_nan ().is_true ());
 	  map_ec_to_m.put (ec_idx, out->m_equiv_classes.length ());
 	  out->m_equiv_classes.safe_push (new equiv_class (cleaned_ec));
 	}
@@ -1461,8 +1626,17 @@ constraint_manager::for_each_fact (fact_visitor *visitor) const
 	    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]);
+	{
+	  /* If we know the NaN-ness of the EC, express that.  */
+	  if (ec->get_is_nan ().is_true ())
+	    visitor->on_fact (ec->m_vars[i], NE_EXPR, ec->m_vars[i]);
+	  else if (ec->get_is_nan ().is_false ())
+	    visitor->on_fact (ec->m_vars[i], EQ_EXPR, ec->m_vars[i]);
+
+	  /* Express the various equalities.  */
+	  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.  */
@@ -1515,7 +1689,13 @@ constraint_manager::validate () const
 	  gcc_assert (sid->as_int () < get_num_svalues ());
 	}
       if (ec->m_constant)
-	gcc_assert (CONSTANT_CLASS_P (ec->m_constant));
+	{
+	  gcc_assert (CONSTANT_CLASS_P (ec->m_constant));
+	  if (cst_is_nan (ec->m_constant))
+	    gcc_assert (ec->get_is_nan ().is_true ());
+	  else
+	    gcc_assert (ec->get_is_nan ().is_false ());
+	}
 #if 0
       else
 	gcc_assert (ec->m_vars.length () > 0);
@@ -1536,6 +1716,33 @@ constraint_manager::validate () const
 
 namespace selftest {
 
+/* Subroutine for test_cst_is_nan.  */
+
+static bool
+real_str_is_nan (tree type, const char *str)
+{
+  return cst_is_nan (build_real_cst_from_string (type, str));
+}
+
+/* Verify that cst_is_nan works.  */
+
+static void
+test_cst_is_nan ()
+{
+  ASSERT_FALSE (cst_is_nan (build_int_cst (integer_type_node, 0)));
+  ASSERT_FALSE (cst_is_nan (build_int_cst (integer_type_node, 42)));
+  ASSERT_FALSE (cst_is_nan (build_int_cst (unsigned_type_node, 0)));
+  ASSERT_FALSE (cst_is_nan (build_int_cst (unsigned_type_node, 42)));
+  ASSERT_TRUE (real_str_is_nan (float_type_node, "QNaN"));
+  ASSERT_TRUE (real_str_is_nan (float_type_node, "-QNaN"));
+  ASSERT_TRUE (real_str_is_nan (float_type_node, "SNaN"));
+  ASSERT_TRUE (real_str_is_nan (float_type_node, "-SNaN"));
+  ASSERT_FALSE (real_str_is_nan (float_type_node, "0.0"));
+  ASSERT_FALSE (real_str_is_nan (float_type_node, "-0.0"));
+  ASSERT_FALSE (real_str_is_nan (float_type_node, "Inf"));
+  ASSERT_FALSE (real_str_is_nan (float_type_node, "-Inf"));
+}
+
 /* 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
@@ -2055,6 +2262,62 @@ test_constant_comparisons ()
     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);
+    /* The fact than e.g. "f > 3" implies that f can't be NaN.  */
+    ASSERT_CONDITION_TRUE (model, f, EQ_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, ORDERED_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, f, UNORDERED_EXPR, f);
+  }
+}
+
+/* Test various comparisons involving NaN or properties of NaN.  */
+
+static void
+test_nan_comparisons ()
+{
+  /* Test comparisons of NaN.  */
+  {
+    tree f = build_global_decl ("f", float_type_node);
+    tree n = build_real_cst_from_string (float_type_node, "QNaN");
+
+    region_model model;
+    ASSERT_CONDITION_TRUE (model, n, NE_EXPR, n);
+    ASSERT_CONDITION_FALSE (model, n, EQ_EXPR, n);
+    ASSERT_CONDITION_TRUE (model, n, UNORDERED_EXPR, n);
+    ASSERT_CONDITION_FALSE (model, n, ORDERED_EXPR, n);
+
+    ASSERT_CONDITION_TRUE (model, n, NE_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, EQ_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, GT_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, GE_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, LT_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, LE_EXPR, f);
+
+    ASSERT_CONDITION_TRUE (model, n, UNORDERED_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, n, ORDERED_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, UNORDERED_EXPR, n);
+    ASSERT_CONDITION_FALSE (model, f, ORDERED_EXPR, n);
+  }
+
+  /* f == f should imply f is not NaN.  */
+  {
+    tree f = build_global_decl ("f", double_type_node);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, f, EQ_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, EQ_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, f, NE_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, ORDERED_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, f, UNORDERED_EXPR, f);
+  }
+
+  /* f != f should imply f is NaN.  */
+  {
+    tree f = build_global_decl ("f", double_type_node);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, f, NE_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, NE_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, f, EQ_EXPR, f);
+    ASSERT_CONDITION_TRUE (model, f, UNORDERED_EXPR, f);
+    ASSERT_CONDITION_FALSE (model, f, ORDERED_EXPR, f);
   }
 }
 
@@ -2235,6 +2498,7 @@ run_constraint_manager_tests (bool transitivity)
       test_transitivity ();
       test_constant_comparisons ();
     }
+  test_nan_comparisons ();
   test_constraint_impl ();
   test_equality ();
   test_many_constants ();
@@ -2247,6 +2511,8 @@ run_constraint_manager_tests (bool transitivity)
 void
 analyzer_constraint_manager_cc_tests ()
 {
+  test_cst_is_nan ();
+
   /* Run the tests twice: with and without transitivity.  */
   run_constraint_manager_tests (true);
   run_constraint_manager_tests (false);
diff --git a/gcc/analyzer/constraint-manager.h b/gcc/analyzer/constraint-manager.h
index 0f4506cc40d..9c8ef267c27 100644
--- a/gcc/analyzer/constraint-manager.h
+++ b/gcc/analyzer/constraint-manager.h
@@ -36,7 +36,10 @@ public:
 
 /* 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.  */
+   together with an optional tree constant that they are equal to.
+
+   If m_is_nan is true (or unknown), then this equiv_class is (or
+   might be) NaN, in which case it isn't equal to itself.  */
 
 class equiv_class
 {
@@ -60,6 +63,24 @@ public:
 
   void print (pretty_printer *pp) const;
 
+  tristate get_is_nan () const { return m_is_nan; }
+
+  /* Set m_is_nan, asserting that we haven't contradicted existing
+     knowledge.  */
+  void set_is_nan (bool val)
+  {
+    if (val)
+      {
+	gcc_assert (!m_is_nan.is_false ());
+	m_is_nan = true;
+      }
+    else
+      {
+	gcc_assert (!m_is_nan.is_true ());
+	m_is_nan = false;
+      }
+  }
+
   /* An equivalence class can contain multiple constants (e.g. multiple
      different zeroes, for different types); these are just for the last
      constant added.  */
@@ -68,6 +89,10 @@ public:
 
   // TODO: should this be a set rather than a vec?
   auto_vec<svalue_id> m_vars;
+
+private:
+  /* Is this NaN?  */
+  tristate m_is_nan;
 };
 
 /* The various kinds of constraint.  */
@@ -170,6 +195,7 @@ public:
 
   virtual constraint_manager *clone (region_model *) const = 0;
   virtual tree maybe_get_constant (svalue_id sid) const = 0;
+  virtual tree get_type (svalue_id sid) const = 0;
   virtual svalue_id get_sid_for_constant (tree cst) const = 0;
   virtual int get_num_svalues () const = 0;
 
@@ -217,6 +243,8 @@ public:
 			   enum tree_code op,
 			   svalue_id rhs);
 
+  bool maybe_nan (svalue_id sid);
+
   void purge (const purge_criteria &p, purge_stats *stats);
 
   void remap_svalue_ids (const svalue_id_map &map);
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index c838454a1eb..d29759fb402 100644
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -137,6 +137,12 @@ class impl_constraint_manager : public constraint_manager
     return svalue->maybe_get_constant ();
   }
 
+  tree get_type (svalue_id sid) const FINAL OVERRIDE
+  {
+    svalue *svalue = m_model->get_svalue (sid);
+    return svalue->get_type ();
+  }
+
   svalue_id get_sid_for_constant (tree cst) const FINAL OVERRIDE
   {
     gcc_assert (CONSTANT_CLASS_P (cst));
@@ -554,6 +560,26 @@ region_svalue::walk_for_canonicalization (canonicalization *c) const
   c->walk_rid (m_rid);
 }
 
+/* Return true if LHS or RHS have HONOR_NANS on their type, but not if
+   they're both known by the constraint_manager to not be NaN.  */
+
+bool
+region_model::maybe_honor_nans (tree lhs, tree rhs,
+				region_model_context *ctxt)
+{
+  if (!HONOR_NANS (lhs))
+    return false;
+  if (!HONOR_NANS (rhs))
+    return false;
+  svalue_id lhs_sid = get_rvalue (lhs, ctxt);
+  if (m_constraints->maybe_nan (lhs_sid))
+    return true;
+  svalue_id rhs_sid = get_rvalue (rhs, ctxt);
+  if (m_constraints->maybe_nan (rhs_sid))
+    return true;
+  return false;
+}
+
 /* Evaluate the condition LHS OP RHS.
    Subroutine of region_model::eval_condition for when we have a pair of
    pointers.  */
@@ -3530,13 +3556,17 @@ region_model::debug () const
   dump (false);
 }
 
+typedef std::pair<tree, svalue_id> tree_and_sid;
+
 /* Dump VEC to PP, in the form "{VEC elements}: LABEL".  */
 
 static void
-dump_vec_of_tree (pretty_printer *pp,
-		  bool *is_first,
-		  const auto_vec<tree> &vec,
-		  const char *label)
+dump_vec_of_tree_and_sid (pretty_printer *pp,
+			  bool *is_first,
+			  const auto_vec<tree_and_sid> &vec,
+			  const char *label,
+			  const constraint_manager *cm,
+			  bool show_isnan)
 {
   if (vec.length () == 0)
     return;
@@ -3544,12 +3574,35 @@ dump_vec_of_tree (pretty_printer *pp,
   dump_separator (pp, is_first);
   pp_printf (pp, "{");
   unsigned i;
-  tree key;
-  FOR_EACH_VEC_ELT (vec, i, key)
+  tree_and_sid *p;
+  FOR_EACH_VEC_ELT (vec, i, p)
     {
+      tree key = p->first;
+      svalue_id sid = p->second;
       if (i > 0)
 	pp_string (pp, ", ");
       dump_tree (pp, key);
+      if (cm && show_isnan && FLOAT_TYPE_P (TREE_TYPE (key)))
+	{
+	  equiv_class_id ec_id (-1);
+	  if (cm->get_equiv_class_by_sid (sid, &ec_id))
+	    {
+	      switch (ec_id.get_obj (*cm).get_is_nan ().get_value ())
+		{
+		default:
+		  gcc_unreachable ();
+		case tristate::TS_UNKNOWN:
+		  pp_string (pp, " (maybe-NaN)");
+		  break;
+		case tristate::TS_TRUE:
+		  pp_string (pp, " (NaN)");
+		  break;
+		case tristate::TS_FALSE:
+		  pp_string (pp, " (not-NaN)");
+		  break;
+		}
+	    }
+	}
     }
   pp_printf (pp, "}: %s", label);
 }
@@ -3579,8 +3632,8 @@ region_model::dump_summary_of_map (pretty_printer *pp,
      gather keys for unknown and uninit values.  */
   unsigned i;
   tree key;
-  auto_vec<tree> unknown_keys;
-  auto_vec<tree> uninit_keys;
+  auto_vec<tree_and_sid> unknown_keys;
+  auto_vec<tree_and_sid> uninit_keys;
   FOR_EACH_VEC_ELT (keys, i, key)
     {
       region_id child_rid = *map_region->get (key);
@@ -3620,14 +3673,14 @@ region_model::dump_summary_of_map (pretty_printer *pp,
 	  dump_tree (pp, sval->dyn_cast_constant_svalue ()->get_constant ());
 	  break;
 	case SK_UNKNOWN:
-	  unknown_keys.safe_push (key);
+	  unknown_keys.safe_push (tree_and_sid (key, sid));
 	  break;
 	case SK_POISONED:
 	  {
 	    poisoned_svalue *poisoned_sval = as_a <poisoned_svalue *> (sval);
 	    enum poison_kind pkind = poisoned_sval->get_poison_kind ();
 	    if (pkind == POISON_KIND_UNINIT)
-	      uninit_keys.safe_push (key);
+	      uninit_keys.safe_push (tree_and_sid (key, sid));
 	    else
 	      {
 		dump_separator (pp, is_first);
@@ -3645,8 +3698,10 @@ region_model::dump_summary_of_map (pretty_printer *pp,
     }
 
   /* Print unknown and uninitialized values in consolidated form.  */
-  dump_vec_of_tree (pp, is_first, unknown_keys, "unknown");
-  dump_vec_of_tree (pp, is_first, uninit_keys, "uninit");
+  dump_vec_of_tree_and_sid (pp, is_first, unknown_keys, "unknown",
+			    m_constraints, true);
+  dump_vec_of_tree_and_sid (pp, is_first, uninit_keys, "uninit",
+			    NULL, false);
 }
 
 /* Assert that this object is valid.  */
@@ -4017,6 +4072,8 @@ region_model::on_assignment (const gassign *assign, region_model_context *ctxt)
     case NE_EXPR:
     case GT_EXPR:
     case LT_EXPR:
+    case ORDERED_EXPR:
+    case UNORDERED_EXPR:
       {
 	tree rhs2 = gimple_assign_rhs2 (assign);
 
@@ -5144,6 +5201,8 @@ region_model::eval_condition (svalue_id lhs_sid,
 			      enum tree_code op,
 			      svalue_id rhs_sid) const
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   tristate ts = eval_condition_without_cm (lhs_sid, op, rhs_sid);
 
   if (ts.is_known ())
@@ -5165,6 +5224,8 @@ region_model::eval_condition_without_cm (svalue_id lhs_sid,
 					 enum tree_code op,
 					 svalue_id rhs_sid) const
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   svalue *lhs = get_svalue (lhs_sid);
   svalue *rhs = get_svalue (rhs_sid);
   gcc_assert (lhs);
@@ -5173,7 +5234,9 @@ region_model::eval_condition_without_cm (svalue_id lhs_sid,
   /* See what we know based on the values.  */
   if (lhs && rhs)
     {
-      if (lhs == rhs)
+      if (lhs == rhs
+	  && (lhs->get_type () && !FLOAT_TYPE_P (lhs->get_type ()))
+	  && (rhs->get_type () && !FLOAT_TYPE_P (rhs->get_type ())))
 	{
 	  /* If we have the same svalue, then we have equality
 	     (apart from NaN-handling).
@@ -5252,6 +5315,8 @@ bool
 region_model::add_constraint (tree lhs, enum tree_code op, tree rhs,
 			      region_model_context *ctxt)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   svalue_id lhs_sid = get_rvalue (lhs, ctxt);
   svalue_id rhs_sid = get_rvalue (rhs, ctxt);
 
@@ -5305,6 +5370,8 @@ region_model::add_any_constraints_from_ssa_def_stmt (tree lhs,
 						     tree rhs,
 						     region_model_context *ctxt)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
+
   if (TREE_CODE (lhs) != SSA_NAME)
     return;
 
@@ -5367,8 +5434,13 @@ region_model::add_any_constraints_from_ssa_def_stmt (tree lhs,
 	tree rhs1 = gimple_assign_rhs1 (assign);
 	tree rhs2 = gimple_assign_rhs2 (assign);
 	if (!is_true)
-	  rhs_code
-	    = invert_tree_comparison (rhs_code, false /* honor_nans */);
+	  {
+	    rhs_code = invert_tree_comparison (rhs_code,
+					       maybe_honor_nans (rhs1, rhs,
+								 ctxt));
+	    if (op == ERROR_MARK)
+	      return;
+	  }
 	add_constraint (rhs1, rhs_code, rhs2, ctxt);
       }
       break;
@@ -5385,6 +5457,7 @@ region_model::eval_condition (tree lhs,
 			      tree rhs,
 			      region_model_context *ctxt)
 {
+  gcc_assert (TREE_CODE_CLASS (op) == tcc_comparison);
   return eval_condition (get_rvalue (lhs, ctxt), op, get_rvalue (rhs, ctxt));
 }
 
@@ -5706,7 +5779,11 @@ region_model::apply_constraints_for_gcond (const cfg_superedge &sedge,
   tree lhs = gimple_cond_lhs (cond_stmt);
   tree rhs = gimple_cond_rhs (cond_stmt);
   if (cfg_edge->flags & EDGE_FALSE_VALUE)
-    op = invert_tree_comparison (op, false /* honor_nans */);
+    {
+      op = invert_tree_comparison (op, maybe_honor_nans (lhs, rhs, ctxt));
+      if (op == ERROR_MARK)
+	return true;
+    }
   return add_constraint (lhs, op, rhs, ctxt);
 }
 
@@ -6919,16 +6996,6 @@ namespace ana {
 
 namespace selftest {
 
-/* Build a constant tree of the given type from STR.  */
-
-static tree
-build_real_cst_from_string (tree type, const char *str)
-{
-  REAL_VALUE_TYPE real;
-  real_from_string (&real, str);
-  return build_real (type, real);
-}
-
 /* Append various "interesting" constants to OUT (e.g. NaN).  */
 
 static void
@@ -7031,6 +7098,33 @@ test_dump ()
   ASSERT_DUMP_EQ (model, true, "");
 }
 
+/* Verify that summarization works when dumping.  */
+
+static void
+test_dump_2 ()
+{
+  /* NaN-ness should not be printed for int.  */
+  {
+    region_model model;
+    tree x = build_global_decl ("x", integer_type_node);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, x);
+    ASSERT_DUMP_EQ (model, true, "{x}: unknown");
+  }
+
+  /* NaN-ness should be printed for float.  */
+  {
+    tree f = build_global_decl ("f", float_type_node);
+
+    region_model model0;
+    ADD_SAT_CONSTRAINT (model0, f, EQ_EXPR, f);
+    ASSERT_DUMP_EQ (model0, true, "{f (not-NaN)}: unknown");
+
+    region_model model1;
+    ADD_SAT_CONSTRAINT (model1, f, NE_EXPR, f);
+    ASSERT_DUMP_EQ (model1, true, "{f (NaN)}: unknown");
+  }
+}
+
 /* Verify that calling region_model::get_rvalue repeatedly on the same
    tree constant retrieves the same svalue_id.  */
 
@@ -8015,6 +8109,94 @@ test_constraint_merging ()
 	     tristate (tristate::TS_UNKNOWN));
 }
 
+/* Verify that NaN-ness is correctly merged when merging region_model
+   instances.  */
+
+static void
+test_constraint_merging_2 ()
+{
+  tree f = build_global_decl ("f", double_type_node);
+
+  region_model base_model;
+  base_model.set_to_new_unknown_value (base_model.get_lvalue (f, NULL),
+				       double_type_node, NULL);
+
+  /* A model in which f is an unknown not-NaN value.  */
+  region_model not_nan_model (base_model);
+  not_nan_model.add_constraint (f, EQ_EXPR, f, NULL);
+  ASSERT_NE (not_nan_model, base_model);
+
+  /* A model in which f is an unknown NaN value.  */
+  region_model nan_model (base_model);
+  nan_model.add_constraint (f, NE_EXPR, f, NULL);
+  ASSERT_NE (nan_model, base_model);
+  ASSERT_NE (nan_model, not_nan_model);
+
+  /* Verify the various mergers (3x3 == 9 cases, for the various
+     combinations of unknown-if-NaN, known-NaN and known-not-NaN).  */
+
+  /* not-NaN merged with not-NaN should be not-NaN.  */
+  {
+    region_model merged;
+    ASSERT_TRUE (not_nan_model.can_merge_with_p (not_nan_model, &merged));
+    ASSERT_EQ (merged, not_nan_model);
+    ASSERT_NE (merged, base_model);
+  }
+
+  /* NaN merged with NaN should be NaN.  */
+  {
+    region_model merged;
+    ASSERT_TRUE (nan_model.can_merge_with_p (nan_model, &merged));
+    ASSERT_EQ (merged, nan_model);
+    ASSERT_NE (merged, base_model);
+  }
+
+  /* NaN merged with not-NaN should be unknown-NaN-ness.  */
+  {
+    region_model merged;
+    ASSERT_TRUE (nan_model.can_merge_with_p (not_nan_model, &merged));
+    ASSERT_EQ (merged, base_model);
+  }
+
+  /* ...and vice-versa.  */
+  {
+    region_model merged;
+    ASSERT_TRUE (not_nan_model.can_merge_with_p (nan_model, &merged));
+    ASSERT_EQ (merged, base_model);
+  }
+
+  /* unknown-NaN-ness merged with known-NaN-ness should be unknown-NaN-ness.  */
+  {
+    {
+      region_model merged;
+      ASSERT_TRUE (not_nan_model.can_merge_with_p (base_model, &merged));
+      ASSERT_EQ (merged, base_model);
+    }
+    {
+      region_model merged;
+      ASSERT_TRUE (nan_model.can_merge_with_p (base_model, &merged));
+      ASSERT_EQ (merged, base_model);
+    }
+    {
+      region_model merged;
+      ASSERT_TRUE (base_model.can_merge_with_p (not_nan_model, &merged));
+      ASSERT_EQ (merged, base_model);
+    }
+    {
+      region_model merged;
+      ASSERT_TRUE (base_model.can_merge_with_p (nan_model, &merged));
+      ASSERT_EQ (merged, base_model);
+    }
+  }
+
+  /* Self-merger of unknown-NaN-ness should be unknown-NaN-ness.  */
+  {
+      region_model merged;
+      ASSERT_TRUE (base_model.can_merge_with_p (base_model, &merged));
+      ASSERT_EQ (merged, base_model);
+  }
+}
+
 /* Run all of the selftests within this file.  */
 
 void
@@ -8022,6 +8204,7 @@ analyzer_region_model_cc_tests ()
 {
   test_tree_cmp_on_constants ();
   test_dump ();
+  test_dump_2 ();
   test_unique_constants ();
   test_svalue_equality ();
   test_region_equality ();
@@ -8036,6 +8219,7 @@ analyzer_region_model_cc_tests ()
   test_canonicalization_4 ();
   test_state_merging ();
   test_constraint_merging ();
+  test_constraint_merging_2 ();
 }
 
 } // namespace selftest
diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
index 70e3eb4c716..62ff442c88e 100644
--- a/gcc/analyzer/region-model.h
+++ b/gcc/analyzer/region-model.h
@@ -1758,6 +1758,8 @@ class region_model
   svalue_id set_to_new_unknown_value (region_id dst_rid, tree type,
 				      region_model_context *ctxt);
 
+  bool maybe_honor_nans (tree lhs, tree rhs, region_model_context *ctxt);
+
   tristate eval_condition (svalue_id lhs,
 			   enum tree_code op,
 			   svalue_id rhs) const;
diff --git a/gcc/doc/analyzer.texi b/gcc/doc/analyzer.texi
index 81acdd8998b..b4e9b01da2e 100644
--- a/gcc/doc/analyzer.texi
+++ b/gcc/doc/analyzer.texi
@@ -388,9 +388,6 @@ The implementation of call summaries is currently very simplistic.
 @item
 Lack of function pointer analysis
 @item
-The constraint-handling code assumes reflexivity in some places
-(that values are equal to themselves), which is not the case for NaN.
-@item
 The region model code creates lots of little mutable objects at each
 @code{region_model} (and thus per @code{exploded_node}) rather than
 sharing immutable objects and having the mutable state in the
diff --git a/gcc/testsuite/gcc.dg/analyzer/complex.c b/gcc/testsuite/gcc.dg/analyzer/complex.c
new file mode 100644
index 00000000000..b9cf0d84085
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/complex.c
@@ -0,0 +1,18 @@
+#include "analyzer-decls.h"
+
+__complex__ float
+test_1 (__complex__ float c,
+	__complex__ float d)
+{
+  return c + d;
+}
+
+__complex__ float
+test_2 (__complex__ float c,
+	__complex__ float d)
+{
+  if (c == d)
+    __analyzer_eval (c == d); /* { dg-warning "TRUE" } */
+  else
+    __analyzer_eval (c == d); /* { dg-warning "FALSE" } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/float-fast.c b/gcc/testsuite/gcc.dg/analyzer/float-fast.c
new file mode 100644
index 00000000000..9aff5036253
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/float-fast.c
@@ -0,0 +1,13 @@
+/* { dg-additional-options "-ffast-math" } */
+
+#include "analyzer-decls.h"
+
+void test_1 (float x)
+{
+  __analyzer_eval (x == x); /* { dg-warning "TRUE" } */
+  __analyzer_eval (x != x); /* { dg-warning "FALSE" } */
+  __analyzer_eval (x > x);  /* { dg-warning "FALSE" } */
+  __analyzer_eval (x >= x); /* { dg-warning "TRUE" } */
+  __analyzer_eval (x < x);  /* { dg-warning "FALSE" } */
+  __analyzer_eval (x <= x); /* { dg-warning "TRUE" } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/float.c b/gcc/testsuite/gcc.dg/analyzer/float.c
new file mode 100644
index 00000000000..269703539af
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/float.c
@@ -0,0 +1,56 @@
+#include "analyzer-decls.h"
+
+static void __attribute__((noinline)) avoid_measuring_at_join (void) {}
+
+void test_1 (float x)
+{
+  __analyzer_eval (x == x); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (x != x); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (x > x);  /* { dg-warning "FALSE" } */
+  __analyzer_eval (x >= x); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (x < x);  /* { dg-warning "FALSE" } */
+  __analyzer_eval (x <= x); /* { dg-warning "UNKNOWN" } */
+}
+
+/* Verify that we merge isnan states, and that we preserve isnan state in
+   the face of unrelated merges.  */
+
+/* Verify that we preserve isnan state in the face of unrelated merges.  */
+
+void test_2 (float x, int flag)
+{
+  __analyzer_eval (x == x); /* { dg-warning "UNKNOWN" } */
+  if (__builtin_isnan (x))
+    {
+      __analyzer_eval (x == x); /* { dg-warning "FALSE" } */
+      __analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+
+      if (flag)
+	__analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+      else
+	__analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+      avoid_measuring_at_join ();
+      __analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+
+      __analyzer_eval (x == x); /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (x == x); /* { dg-warning "TRUE" } */
+      __analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+
+      if (flag)
+	__analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+      else
+	__analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+      avoid_measuring_at_join ();
+      __analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+
+      __analyzer_eval (x == x); /* { dg-warning "TRUE" } */
+
+    }
+  avoid_measuring_at_join ();
+  __analyzer_dump_exploded_nodes (0); /* { dg-warning "1 exploded node" } */
+
+  __analyzer_eval (x == x); /* { dg-warning "UNKNOWN" } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/torture/nan-notrap.c b/gcc/testsuite/gcc.dg/analyzer/torture/nan-notrap.c
new file mode 100644
index 00000000000..b15835b641a
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/torture/nan-notrap.c
@@ -0,0 +1,176 @@
+/* { dg-skip-if "" { *-*-* } { "-fno-fat-lto-objects" } { "" } } */
+/* { dg-additional-options "-fno-trapping-math" } */
+
+#include "../analyzer-decls.h"
+
+void
+test_1 (double d1)
+{
+  if (__builtin_isnan (d1))
+    {
+      __analyzer_eval (__builtin_isnan (d1)); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 == d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 <= d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 >= d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 < d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 > d1); /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d1));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 == d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 >= d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 <= d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 > d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 < d1); /* { dg-warning "FALSE" } */
+    }
+}
+
+void
+test_2_self_eq (double d2)
+{
+  if (d2 == d2)
+    {
+      __analyzer_eval (__builtin_isnan (d2));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d2));  /* { dg-warning "TRUE" } */
+    }
+}
+
+void
+test_3_self_ne (double d3)
+{
+  if (d3 != d3)
+    {
+      __analyzer_eval (__builtin_isnan (d3));  /* { dg-warning "TRUE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d3));  /* { dg-warning "FALSE" } */
+    }
+}
+
+void
+test_4_eq (double d4, double e4)
+{
+  if (d4 == e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_lt (double d4, double e4)
+{
+  if (d4 < e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_le (double d4, double e4)
+{
+  if (d4 <= e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_ge (double d4, double e4)
+{
+  if (d4 >= e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_gt (double d4, double e4)
+{
+  if (d4 > e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_5 (double d5, double e5)
+{
+  if (d5 != e5)
+    {
+      __analyzer_eval (__builtin_isnan (d5));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e5));  /* { dg-warning "UNKNOWN" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d5));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e5));  /* { dg-warning "FALSE" } */
+    }
+}
+
+static double __attribute__((noinline))
+get_nan ()
+{
+  return __builtin_nan ("");
+}
+
+void
+test_6 ()
+{
+  __analyzer_eval (__builtin_isnan (get_nan ())); /* { dg-warning "TRUE" } */
+}
+
+void
+test_7 (double d7)
+{
+  __analyzer_eval (get_nan () == d7); /* { dg-warning "FALSE" } */
+  __analyzer_eval (get_nan () != d7); /* { dg-warning "TRUE" } */
+  __analyzer_eval (get_nan () == get_nan ()); /* { dg-warning "FALSE" } */
+  __analyzer_eval (get_nan () != get_nan ()); /* { dg-warning "TRUE" } */
+}
+
+void
+test_8 (float f8, float g8)
+{
+  if (!__builtin_isnan (f8) && !__builtin_isnan (g8))
+    {
+      if (f8 > g8)
+	__analyzer_eval (f8 > g8);  /* { dg-warning "TRUE" } */
+      else
+	__analyzer_eval (f8 <= g8);  /* { dg-warning "TRUE" } */
+    }
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/torture/nan.c b/gcc/testsuite/gcc.dg/analyzer/torture/nan.c
new file mode 100644
index 00000000000..052b0b4d5bf
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/torture/nan.c
@@ -0,0 +1,175 @@
+/* { dg-skip-if "" { *-*-* } { "-fno-fat-lto-objects" } { "" } } */
+
+#include "../analyzer-decls.h"
+
+void
+test_1 (double d1)
+{
+  if (__builtin_isnan (d1))
+    {
+      __analyzer_eval (__builtin_isnan (d1)); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 == d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 <= d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 >= d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 < d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 > d1); /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d1));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 == d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 >= d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 <= d1); /* { dg-warning "TRUE" } */
+      __analyzer_eval (d1 > d1); /* { dg-warning "FALSE" } */
+      __analyzer_eval (d1 < d1); /* { dg-warning "FALSE" } */
+    }
+}
+
+void
+test_2_self_eq (double d2)
+{
+  if (d2 == d2)
+    {
+      __analyzer_eval (__builtin_isnan (d2));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d2));  /* { dg-warning "TRUE" } */
+    }
+}
+
+void
+test_3_self_ne (double d3)
+{
+  if (d3 != d3)
+    {
+      __analyzer_eval (__builtin_isnan (d3));  /* { dg-warning "TRUE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d3));  /* { dg-warning "FALSE" } */
+    }
+}
+
+void
+test_4_eq (double d4, double e4)
+{
+  if (d4 == e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_lt (double d4, double e4)
+{
+  if (d4 < e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_le (double d4, double e4)
+{
+  if (d4 <= e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_ge (double d4, double e4)
+{
+  if (d4 >= e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_4_gt (double d4, double e4)
+{
+  if (d4 > e4)
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "FALSE" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d4));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e4));  /* { dg-warning "UNKNOWN" } */
+    }
+}
+
+void
+test_5 (double d5, double e5)
+{
+  if (d5 != e5)
+    {
+      __analyzer_eval (__builtin_isnan (d5));  /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (__builtin_isnan (e5));  /* { dg-warning "UNKNOWN" } */
+    }
+  else
+    {
+      __analyzer_eval (__builtin_isnan (d5));  /* { dg-warning "FALSE" } */
+      __analyzer_eval (__builtin_isnan (e5));  /* { dg-warning "FALSE" } */
+    }
+}
+
+static double __attribute__((noinline))
+get_nan ()
+{
+  return __builtin_nan ("");
+}
+
+void
+test_6 ()
+{
+  __analyzer_eval (__builtin_isnan (get_nan ())); /* { dg-warning "TRUE" } */
+}
+
+void
+test_7 (double d7)
+{
+  __analyzer_eval (get_nan () == d7); /* { dg-warning "FALSE" } */
+  __analyzer_eval (get_nan () != d7); /* { dg-warning "TRUE" } */
+  __analyzer_eval (get_nan () == get_nan ()); /* { dg-warning "FALSE" } */
+  __analyzer_eval (get_nan () != get_nan ()); /* { dg-warning "TRUE" } */
+}
+
+void
+test_8 (float f8, float g8)
+{
+  if (!__builtin_isnan (f8) && !__builtin_isnan (g8))
+    {
+      if (f8 > g8)
+	__analyzer_eval (f8 > g8);  /* { dg-warning "TRUE" } */
+      else
+	__analyzer_eval (f8 <= g8);  /* { dg-warning "TRUE" } */
+    }
+}
diff --git a/gcc/tristate.cc b/gcc/tristate.cc
index 127d7407163..bcc810cf0cf 100644
--- a/gcc/tristate.cc
+++ b/gcc/tristate.cc
@@ -121,18 +121,21 @@ test_ctors ()
 {
   tristate u (tristate::TS_UNKNOWN);
   ASSERT_FALSE (u.is_known ());
+  ASSERT_TRUE (u.is_unknown ());
   ASSERT_FALSE (u.is_true ());
   ASSERT_FALSE (u.is_false ());
   ASSERT_STREQ (u.as_string (), "UNKNOWN");
 
   tristate t (tristate::TS_TRUE);
   ASSERT_TRUE (t.is_known ());
+  ASSERT_FALSE (t.is_unknown ());
   ASSERT_TRUE (t.is_true ());
   ASSERT_FALSE (t.is_false ());
   ASSERT_STREQ (t.as_string (), "TRUE");
 
   tristate f (tristate::TS_FALSE);
   ASSERT_TRUE (f.is_known ());
+  ASSERT_FALSE (f.is_unknown ());
   ASSERT_FALSE (f.is_true ());
   ASSERT_TRUE (f.is_false ());
   ASSERT_STREQ (f.as_string (), "FALSE");
diff --git a/gcc/tristate.h b/gcc/tristate.h
index e65cb6a09ac..833908fd347 100644
--- a/gcc/tristate.h
+++ b/gcc/tristate.h
@@ -38,9 +38,12 @@ class tristate {
   const char *as_string () const;
 
   bool is_known () const { return m_value != TS_UNKNOWN; }
+  bool is_unknown () const { return m_value == TS_UNKNOWN; }
   bool is_true () const { return m_value == TS_TRUE; }
   bool is_false () const { return m_value == TS_FALSE; }
 
+  enum value get_value () const { return m_value; }
+
   tristate not_ () const;
   tristate or_ (tristate other) const;
   tristate and_ (tristate other) const;
-- 
2.21.0

