public inbox for smatch@vger.kernel.org
 help / color / mirror / Atom feed
From: Dan Carpenter <dan.carpenter@oracle.com>
To: John Levon <levon@movementarian.org>
Cc: smatch@vger.kernel.org
Subject: Re: Odd smatch issue?
Date: Mon, 14 Jan 2019 13:18:04 +0300	[thread overview]
Message-ID: <20190114101804.GA4482@kadam> (raw)
In-Reply-To: <20190111123241.GA11408@movementarian.org>

On Fri, Jan 11, 2019 at 12:32:41PM +0000, John Levon wrote:
> 
> 
> static long
> lx_cap_update_priv(void)
> {
>         const int lx_cap_mapping[4] = { 0, 0, 0 };
>         int i = 63;
>         /* enabling the below line disables the warning */
>         //int cap_set = i == 0;
>         lx_cap_mapping[i];
> }
> 

Thanks John,

I am testing this patch:

[PATCH] extra: preserve hard_max after comparisons to zero

John Levon reported that if you had code like:

int lx_cap_mapping[4];
int i = 63;

if (i)
	;
lx_cap_mapping[i] = 0;

The code should trigger a warning but it doesn't.

I initially thought the hard_max was getting lost in
merge_estates().  I changed that to say if we were merging an
impossible state with a possible one then we should keep the
hard max from the possible one.  It turns out that wasn't
the issue, but I sort of think it's the correct thing to do
anyway.

The real problem is that we don't preserve the hard_max after
comparisons to zero, whether it's impossible or not.  That is
handled in match_condition().  I changed that function to re-use
handle_comparison().  After that because the original "i" had a
hard_max then handle_comparison() sets the hard_max flag for
both the possible and the impossible sides.

Reported-by: John Levon <levon@movementarian.org>
Signed-off-by: Dan Carpenter <dan.carpenter@oracle.com>
---
 smatch_estate.c |  4 +++-
 smatch_extra.c  | 27 ++-------------------------
 2 files changed, 5 insertions(+), 26 deletions(-)

diff --git a/smatch_estate.c b/smatch_estate.c
index 61a8fd34..69b84d91 100644
--- a/smatch_estate.c
+++ b/smatch_estate.c
@@ -43,7 +43,9 @@ struct smatch_state *merge_estates(struct smatch_state *s1, struct smatch_state
 	tmp = alloc_estate_rl(value_ranges);
 	rlist = get_shared_relations(estate_related(s1), estate_related(s2));
 	set_related(tmp, rlist);
-	if (estate_has_hard_max(s1) && estate_has_hard_max(s2))
+
+	if ((estate_has_hard_max(s1) && (!estate_rl(s2) || estate_has_hard_max(s2))) ||
+	    (estate_has_hard_max(s2) && (!estate_rl(s1) || estate_has_hard_max(s1))))
 		estate_set_hard_max(tmp);
 
 	estate_set_fuzzy_max(tmp, sval_max(estate_get_fuzzy_max(s1), estate_get_fuzzy_max(s2)));
diff --git a/smatch_extra.c b/smatch_extra.c
index c2d97a88..e781c80f 100644
--- a/smatch_extra.c
+++ b/smatch_extra.c
@@ -1989,11 +1989,6 @@ static void handle_MOD_condition(struct expression *expr)
 /* this is actually hooked from smatch_implied.c...  it's hacky, yes */
 void __extra_match_condition(struct expression *expr)
 {
-	struct smatch_state *pre_state;
-	struct smatch_state *true_state;
-	struct smatch_state *false_state;
-	struct range_list *pre_rl;
-
 	expr = strip_expr(expr);
 	switch (expr->type) {
 	case EXPR_CALL:
@@ -2001,27 +1996,9 @@ void __extra_match_condition(struct expression *expr)
 		return;
 	case EXPR_PREOP:
 	case EXPR_SYMBOL:
-	case EXPR_DEREF: {
-		sval_t zero;
-
-		zero = sval_blank(expr);
-		zero.value = 0;
-
-		pre_state = get_extra_state(expr);
-		if (estate_is_empty(pre_state))
-			return;
-		if (pre_state)
-			pre_rl = estate_rl(pre_state);
-		else
-			get_absolute_rl(expr, &pre_rl);
-		if (possibly_true_rl(pre_rl, SPECIAL_EQUAL, rl_zero()))
-			false_state = alloc_estate_sval(zero);
-		else
-			false_state = alloc_estate_empty();
-		true_state = alloc_estate_rl(remove_range(pre_rl, zero, zero));
-		set_extra_expr_true_false(expr, true_state, false_state);
+	case EXPR_DEREF:
+		handle_comparison(get_type(expr), expr, SPECIAL_NOTEQUAL, zero_expr());
 		return;
-	}
 	case EXPR_COMPARE:
 		match_comparison(expr);
 		return;
-- 
2.17.1

  reply	other threads:[~2019-01-14 10:18 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-11 12:32 Odd smatch issue? John Levon
2019-01-14 10:18 ` Dan Carpenter [this message]
2019-01-14 12:42   ` John Levon
2019-01-14 14:38     ` Dan Carpenter
2019-01-14 14:47       ` John Levon
2019-01-14 14:51         ` Dan Carpenter

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=20190114101804.GA4482@kadam \
    --to=dan.carpenter@oracle.com \
    --cc=levon@movementarian.org \
    --cc=smatch@vger.kernel.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