analyzer: eliminate region_model::eval_condition_without_cm [PR101962]

In r12-3094-ge82e0f149b0aba I added the assumption that
POINTER_PLUS_EXPR of non-NULL is non-NULL (for PR analyzer/101962).

Whilst working on another bug, I noticed that this only works
when the LHS is known to be non-NULL via
region_model::eval_condition_without_cm, but not when it's known through
a constraint.

This distinction predates the original commit of the analyzer in GCC 10,
but I believe it became irrelevant in the GCC 11 rewrite of the region
model code (r11-2694-g808f4dfeb3a95f).

Hence this patch eliminates region_model::eval_condition_without_cm in
favor of all users simply calling region_model::eval_condition.  Doing
so enables the "POINTER_PLUS_EXPR of non-NULL is non-NULL" assumption to
also be made when the LHS is known through a constraint (e.g. a
conditional).

gcc/analyzer/ChangeLog:
	PR analyzer/101962
	* region-model-impl-calls.cc: Update comment.
	* region-model.cc (region_model::check_symbolic_bounds): Fix
	layout of "void" return.  Replace usage of
	eval_condition_without_cm with eval_condition.
	(region_model::eval_condition): Take over body of...
	(region_model::eval_condition_without_cm): ...this subroutine,
	dropping the latter.  Eliminating this distinction avoids issues
	where constraints were not considered when recursing.
	(region_model::compare_initial_and_pointer): Update comment.
	(region_model::symbolic_greater_than): Replace usage of
	eval_condition_without_cm with eval_condition.
	* region-model.h
	(region_model::eval_condition_without_cm): Delete decl.

gcc/testsuite/ChangeLog:
	PR analyzer/101962
	* gcc.dg/analyzer/data-model-23.c (test_3): New test.

Signed-off-by: David Malcolm <dmalcolm@redhat.com>

diff --git a/gcc/analyzer/region-model-impl-calls.cc b/gcc/analyzer/region-model-impl-calls.cc
index bc644f8..9ef31f6 100644 (file)
--- a/gcc/analyzer/region-model-impl-calls.cc
+++ b/gcc/analyzer/region-model-impl-calls.cc
@@ -498,7 +498,7 @@ region_model::impl_call_fread (const call_details &cd)
 
    This has to be done here so that the sm-handling can use the fact
    that they point to the same region to establish that they are equal
-   (in region_model::eval_condition_without_cm), and thus transition
+   (in region_model::eval_condition), and thus transition
    all pointers to the region to the "freed" state together, regardless
    of casts.  */
 

diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index 0ca454a..5ffad64 100644 (file)
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -1764,12 +1764,13 @@ public:
 
 /* Check whether an access is past the end of the BASE_REG.  */
 
-void region_model::check_symbolic_bounds (const region *base_reg,
-                                         const svalue *sym_byte_offset,
-                                         const svalue *num_bytes_sval,
-                                         const svalue *capacity,
-                                         enum access_direction dir,
-                                         region_model_context *ctxt) const
+void
+region_model::check_symbolic_bounds (const region *base_reg,
+                                    const svalue *sym_byte_offset,
+                                    const svalue *num_bytes_sval,
+                                    const svalue *capacity,
+                                    enum access_direction dir,
+                                    region_model_context *ctxt) const
 {
   gcc_assert (ctxt);
 
@@ -1777,7 +1778,7 @@ void region_model::check_symbolic_bounds (const region *base_reg,
     = m_mgr->get_or_create_binop (num_bytes_sval->get_type (), PLUS_EXPR,
                                  sym_byte_offset, num_bytes_sval);
 
-  if (eval_condition_without_cm (next_byte, GT_EXPR, capacity).is_true ())
+  if (eval_condition (next_byte, GT_EXPR, capacity).is_true ())
     {
       tree diag_arg = get_representative_tree (base_reg);
       tree offset_tree = get_representative_tree (sym_byte_offset);
@@ -4162,43 +4163,17 @@ region_model::eval_condition (const svalue *lhs,
                               enum tree_code op,
                               const svalue *rhs) const
 {
-  /* For now, make no attempt to capture constraints on floating-point
-     values.  */
-  if ((lhs->get_type () && FLOAT_TYPE_P (lhs->get_type ()))
-      || (rhs->get_type () && FLOAT_TYPE_P (rhs->get_type ())))
-    return tristate::unknown ();
-
-  tristate ts = eval_condition_without_cm (lhs, op, rhs);
-  if (ts.is_known ())
-    return ts;
-
-  /* Otherwise, try constraints.  */
-  return m_constraints->eval_condition (lhs, op, rhs);
-}
-
-/* Determine what is known about the condition "LHS_SVAL OP RHS_SVAL" within
-   this model, without resorting to the constraint_manager.
-
-   This is exposed so that impl_region_model_context::on_state_leak can
-   check for equality part-way through region_model::purge_unused_svalues
-   without risking creating new ECs.  */
-
-tristate
-region_model::eval_condition_without_cm (const svalue *lhs,
-                                         enum tree_code op,
-                                         const svalue *rhs) const
-{
   gcc_assert (lhs);
   gcc_assert (rhs);
 
-  /* See what we know based on the values.  */
-
   /* For now, make no attempt to capture constraints on floating-point
      values.  */
   if ((lhs->get_type () && FLOAT_TYPE_P (lhs->get_type ()))
       || (rhs->get_type () && FLOAT_TYPE_P (rhs->get_type ())))
     return tristate::unknown ();
 
+  /* See what we know based on the values.  */
+
   /* Unwrap any unmergeable values.  */
   lhs = lhs->unwrap_any_unmergeable ();
   rhs = rhs->unwrap_any_unmergeable ();
@@ -4292,9 +4267,7 @@ region_model::eval_condition_without_cm (const svalue *lhs,
               shouldn't warn for.  */
            if (binop->get_op () == POINTER_PLUS_EXPR)
              {
-               tristate lhs_ts
-                 = eval_condition_without_cm (binop->get_arg0 (),
-                                              op, rhs);
+               tristate lhs_ts = eval_condition (binop->get_arg0 (), op, rhs);
                if (lhs_ts.is_known ())
                  return lhs_ts;
              }
@@ -4327,7 +4300,7 @@ region_model::eval_condition_without_cm (const svalue *lhs,
       }
 
   /* Handle comparisons between two svalues with more than one operand.  */
-       if (const binop_svalue *binop = lhs->dyn_cast_binop_svalue ())
+  if (const binop_svalue *binop = lhs->dyn_cast_binop_svalue ())
     {
       switch (op)
        {
@@ -4369,10 +4342,14 @@ region_model::eval_condition_without_cm (const svalue *lhs,
        }
     }
 
-  return tristate::TS_UNKNOWN;
+  /* Otherwise, try constraints.
+     Cast to const to ensure we don't change the constraint_manager as we
+     do this (e.g. by creating equivalence classes).  */
+  const constraint_manager *constraints = m_constraints;
+  return constraints->eval_condition (lhs, op, rhs);
 }
 
-/* Subroutine of region_model::eval_condition_without_cm, for rejecting
+/* Subroutine of region_model::eval_condition, for rejecting
    equality of INIT_VAL(PARM) with &LOCAL.  */
 
 tristate
@@ -4424,18 +4401,18 @@ region_model::symbolic_greater_than (const binop_svalue *bin_a,
       /* Eliminate the right-hand side of both svalues.  */
       if (const binop_svalue *bin_b = dyn_cast <const binop_svalue *> (b))
        if (bin_a->get_op () == bin_b->get_op ()
-           && eval_condition_without_cm (bin_a->get_arg1 (),
-                                         GT_EXPR,
-                                         bin_b->get_arg1 ()).is_true ()
-           && eval_condition_without_cm (bin_a->get_arg0 (),
-                                         GE_EXPR,
-                                         bin_b->get_arg0 ()).is_true ())
+           && eval_condition (bin_a->get_arg1 (),
+                              GT_EXPR,
+                              bin_b->get_arg1 ()).is_true ()
+           && eval_condition (bin_a->get_arg0 (),
+                              GE_EXPR,
+                              bin_b->get_arg0 ()).is_true ())
          return tristate (tristate::TS_TRUE);
 
       /* Otherwise, try to remove a positive offset or factor from BIN_A.  */
       if (is_positive_svalue (bin_a->get_arg1 ())
-         && eval_condition_without_cm (bin_a->get_arg0 (),
-                                       GE_EXPR, b).is_true ())
+         && eval_condition (bin_a->get_arg0 (),
+                            GE_EXPR, b).is_true ())
          return tristate (tristate::TS_TRUE);
     }
   return tristate::unknown ();

diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
index 0caaf82..70c808f 100644 (file)
--- a/gcc/analyzer/region-model.h
+++ b/gcc/analyzer/region-model.h
@@ -450,9 +450,6 @@ class region_model
   tristate eval_condition (const svalue *lhs,
                           enum tree_code op,
                           const svalue *rhs) const;
-  tristate eval_condition_without_cm (const svalue *lhs,
-                                     enum tree_code op,
-                                     const svalue *rhs) const;
   tristate compare_initial_and_pointer (const initial_svalue *init,
                                        const region_svalue *ptr) const;
   tristate symbolic_greater_than (const binop_svalue *a,

diff --git a/gcc/testsuite/gcc.dg/analyzer/data-model-23.c b/gcc/testsuite/gcc.dg/analyzer/data-model-23.c
index c76dd4e..d10dd05 100644 (file)
--- a/gcc/testsuite/gcc.dg/analyzer/data-model-23.c
+++ b/gcc/testsuite/gcc.dg/analyzer/data-model-23.c
@@ -24,3 +24,14 @@ void test_2 (void)
   __analyzer_eval (hide (NULL) - 1 == NULL); /* { dg-warning "FALSE" } */
   __analyzer_eval (hide (NULL) + 1 == NULL); /* { dg-warning "FALSE" } */
 }
+
+void test_3 (void *p)
+{
+  if (!p)
+    return;
+  __analyzer_eval (hide (p) == NULL); /* { dg-warning "FALSE" } */
+  __analyzer_eval (hide (p) + 1 != NULL); /* { dg-warning "TRUE" } */
+  __analyzer_eval (hide (p) + 1 == NULL); /* { dg-warning "FALSE" } */
+  __analyzer_eval (hide (p) - 1 != NULL); /* { dg-warning "TRUE" } */
+  __analyzer_eval (hide (p) - 1 == NULL); /* { dg-warning "FALSE" } */
+}