From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 2209) id 760A3385841E; Fri, 2 Dec 2022 02:31:30 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 760A3385841E DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1669948290; bh=8h8lj4XEGci5WKYx0LySm2R2yK1sNczdqKbBhEbNo3A=; h=From:To:Subject:Date:From; b=dHYpsa0zEjBsirCPss0VQSugBLrqZxNIqNP6vgm/g/HRjAbXiZrMDqZcxFj6NGma6 S4l1TJgzmsgWumSa8DSZj4q5CjcOfYYgt89XgcX40ND2ZcaUAE2TAZB0x44vvcGDN9 CvPxEdhz3bxTaOHETw8psF+tKUXF6Sr578jDQxpA= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: David Malcolm To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-4456] analyzer: handle comparisons against negated symbolic values [PR107948] X-Act-Checkin: gcc X-Git-Author: David Malcolm X-Git-Refname: refs/heads/master X-Git-Oldrev: 5cb7d28dcfb11a2810db55b0bbd71fe562bdc2a3 X-Git-Newrev: 0b737090a69624dea5318c380620283f0321a92e Message-Id: <20221202023130.760A3385841E@sourceware.org> Date: Fri, 2 Dec 2022 02:31:30 +0000 (GMT) List-Id: https://gcc.gnu.org/g:0b737090a69624dea5318c380620283f0321a92e commit r13-4456-g0b737090a69624dea5318c380620283f0321a92e Author: David Malcolm Date: Thu Dec 1 21:28:55 2022 -0500 analyzer: handle comparisons against negated symbolic values [PR107948] gcc/analyzer/ChangeLog: PR analyzer/107948 * region-model-manager.cc (region_model_manager::maybe_fold_binop): Fold (0 - VAL) to -VAL. * region-model.cc (region_model::eval_condition): Handle e.g. "-X <= 0" as equivalent to X >= 0". gcc/testsuite/ChangeLog: PR analyzer/107948 * gcc.dg/analyzer/feasibility-pr107948.c: New test. Signed-off-by: David Malcolm Diff: --- gcc/analyzer/region-model-manager.cc | 3 ++ gcc/analyzer/region-model.cc | 13 ++++++ .../gcc.dg/analyzer/feasibility-pr107948.c | 49 ++++++++++++++++++++++ 3 files changed, 65 insertions(+) diff --git a/gcc/analyzer/region-model-manager.cc b/gcc/analyzer/region-model-manager.cc index ae63c664ae5..471a9272e41 100644 --- a/gcc/analyzer/region-model-manager.cc +++ b/gcc/analyzer/region-model-manager.cc @@ -620,6 +620,9 @@ region_model_manager::maybe_fold_binop (tree type, enum tree_code op, /* (VAL - 0) -> VAL. */ if (cst1 && zerop (cst1)) return get_or_create_cast (type, arg0); + /* (0 - VAL) -> -VAL. */ + if (cst0 && zerop (cst0)) + return get_or_create_unaryop (type, NEGATE_EXPR, arg1); break; case MULT_EXPR: /* (VAL * 0). */ diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc index 91b868f7b16..4f623fd6ca3 100644 --- a/gcc/analyzer/region-model.cc +++ b/gcc/analyzer/region-model.cc @@ -3339,6 +3339,19 @@ region_model::eval_condition (const svalue *lhs, return lhs_ts; } } + else if (const unaryop_svalue *unaryop + = lhs->dyn_cast_unaryop_svalue ()) + { + if (unaryop->get_op () == NEGATE_EXPR) + { + /* e.g. "-X <= 0" is equivalent to X >= 0". */ + tristate lhs_ts = eval_condition (unaryop->get_arg (), + swap_tree_comparison (op), + rhs); + if (lhs_ts.is_known ()) + return lhs_ts; + } + } } /* Handle rejection of equality for comparisons of the initial values of diff --git a/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c b/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c new file mode 100644 index 00000000000..5eb8b0aef22 --- /dev/null +++ b/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c @@ -0,0 +1,49 @@ +#include "analyzer-decls.h" + +void foo(int width) { + int i = 0; + int base; + if (width > 0){ + __analyzer_eval(i == 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(width > 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(width - i > 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(i - width <= 0); /* { dg-warning "TRUE" } */ + if (i - width <= 0) { + base = 512; + } + else { + __analyzer_dump_path (); /* { dg-bogus "path" } */ + } + base+=1; /* { dg-bogus "uninit" } */ + } +} + +void test_ge_zero (int x) +{ + if (x >= 0) + { + __analyzer_eval(x >= 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(x > 0); /* { dg-warning "UNKNOWN" } */ + __analyzer_eval(x <= 0); /* { dg-warning "UNKNOWN" } */ + __analyzer_eval(x < 0); /* { dg-warning "FALSE" } */ + __analyzer_eval(-x <= 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(-x < 0); /* { dg-warning "UNKNOWN" } */ + __analyzer_eval(-x >= 0); /* { dg-warning "UNKNOWN" } */ + __analyzer_eval(-x > 0); /* { dg-warning "FALSE" } */ + } +} + +void test_gt_zero (int x) +{ + if (x > 0) + { + __analyzer_eval(x >= 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(x > 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(x <= 0); /* { dg-warning "FALSE" } */ + __analyzer_eval(x < 0); /* { dg-warning "FALSE" } */ + __analyzer_eval(-x <= 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(-x < 0); /* { dg-warning "TRUE" } */ + __analyzer_eval(-x >= 0); /* { dg-warning "FALSE" } */ + __analyzer_eval(-x > 0); /* { dg-warning "FALSE" } */ + } +}