All of lore.kernel.org
 help / color / mirror / Atom feed
* [PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition
@ 2021-07-13 12:50 Harshvardhan Jha
  2021-07-13 12:50 ` [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of Harshvardhan Jha
  0 siblings, 1 reply; 4+ messages in thread
From: Harshvardhan Jha @ 2021-07-13 12:50 UTC (permalink / raw)
  To: smatch; +Cc: dan.carpenter, Harshvardhan Jha

handle_AND_condition and handle_AND_op gave false outputs. This could be
seen in the test case in validation/sm_bits1.c the expected output was
0x1 for possible and 0x0 for definitely set. However, in the previous
state 0x0 was output for both possibly set and definitely set.

Signed-off-by: Harshvardhan Jha <harshvardhan.jha@oracle.com>
---
 smatch_expressions.c  | 10 ++++++
 smatch_extra.c        | 72 +++++++++----------------------------------
 smatch_extra.h        |  1 +
 validation/sm_bits1.c | 23 ++++++++++++++
 4 files changed, 49 insertions(+), 57 deletions(-)
 create mode 100644 validation/sm_bits1.c

diff --git a/smatch_expressions.c b/smatch_expressions.c
index 4c36a206..b18e82be 100644
--- a/smatch_expressions.c
+++ b/smatch_expressions.c
@@ -61,6 +61,16 @@ struct expression *value_expr(long long val)
 	return expr;
 }
 
+struct expression *value_expr_sval(sval_t sval)
+{
+	struct expression *expr;
+
+	expr = alloc_tmp_expression(get_cur_pos(), EXPR_VALUE);
+	expr->value = sval.value;
+	expr->ctype = sval.type;
+	return expr;
+}
+
 struct expression *member_expression(struct expression *deref, int op, struct ident *member)
 {
 	struct expression *expr;
diff --git a/smatch_extra.c b/smatch_extra.c
index b29235fc..e864646a 100644
--- a/smatch_extra.c
+++ b/smatch_extra.c
@@ -2059,24 +2059,6 @@ static void match_comparison(struct expression *expr)
 	handle_comparison(type, left, expr->op, right);
 }
 
-static sval_t get_high_mask(sval_t known)
-{
-	sval_t ret;
-	int i;
-
-	ret = known;
-	ret.value = 0;
-
-	for (i = type_bits(known.type) - 1; i >= 0; i--) {
-		if (known.uvalue & (1ULL << i))
-			ret.uvalue |= (1ULL << i);
-		else
-			return ret;
-
-	}
-	return ret;
-}
-
 static bool handle_bit_test(struct expression *expr)
 {
 	struct range_list *orig_rl, *rl;
@@ -2122,59 +2104,35 @@ static bool handle_bit_test(struct expression *expr)
 	return true;
 }
 
-static void handle_AND_op(struct expression *var, sval_t known)
+static void handle_AND_op(struct symbol *type, struct expression *var, sval_t known)
 {
-	struct range_list *orig_rl;
-	struct range_list *true_rl = NULL;
-	struct range_list *false_rl = NULL;
-	int bit;
-	sval_t low_mask = known;
-	sval_t high_mask;
-	sval_t max;
-
-	get_absolute_rl(var, &orig_rl);
+	sval_t sval = { .type = type };
+	struct expression *bits_expr;
 
-	if (known.value > 0) {
-		bit = ffsll(known.value) - 1;
-		low_mask.uvalue = (1ULL << bit) - 1;
-		true_rl = remove_range(orig_rl, sval_type_val(known.type, 0), low_mask);
-	}
-	high_mask = get_high_mask(known);
-	if (high_mask.value) {
-		bit = ffsll(high_mask.value) - 1;
-		low_mask.uvalue = (1ULL << bit) - 1;
-
-		false_rl = orig_rl;
-		if (sval_is_negative(rl_min(orig_rl)))
-			false_rl = remove_range(false_rl, sval_type_min(known.type), sval_type_val(known.type, -1));
-		false_rl = remove_range(false_rl, low_mask, sval_type_max(known.type));
-		if (type_signed(high_mask.type) && type_unsigned(rl_type(false_rl))) {
-			false_rl = remove_range(false_rl,
-						sval_type_val(rl_type(false_rl), sval_type_max(known.type).uvalue),
-					sval_type_val(rl_type(false_rl), -1));
-		}
-	} else if (known.value == 1 &&
-		   get_hard_max(var, &max) &&
-		   sval_cmp(max, rl_max(orig_rl)) == 0 &&
-		   max.value & 1) {
-		false_rl = remove_range(orig_rl, max, max);
+	if (known.uvalue == 0) {
+		set_true_false_states_expr(my_id, var, alloc_estate_empty(), NULL);
+		return;
 	}
-	set_extra_expr_true_false(var,
-				  true_rl ? alloc_estate_rl(true_rl) : NULL,
-				  false_rl ? alloc_estate_rl(false_rl) : NULL);
+
+	sval.uvalue = 1ULL << (ffsll(known.uvalue) - 1);
+	bits_expr = value_expr_sval(sval);
+	handle_comparison(type, var, SPECIAL_GTE, bits_expr);
 }
 
 static void handle_AND_condition(struct expression *expr)
 {
 	sval_t known;
+	struct symbol *type;
 
 	if (handle_bit_test(expr))
 		return;
 
+	type = get_type(expr);
+
 	if (get_implied_value(expr->left, &known))
-		handle_AND_op(expr->right, known);
+		handle_AND_op(type, expr->right, known);
 	else if (get_implied_value(expr->right, &known))
-		handle_AND_op(expr->left, known);
+		handle_AND_op(type, expr->left, known);
 }
 
 static void handle_MOD_condition(struct expression *expr)
diff --git a/smatch_extra.h b/smatch_extra.h
index 3d75c7c9..e07b06bb 100644
--- a/smatch_extra.h
+++ b/smatch_extra.h
@@ -215,6 +215,7 @@ void function_comparison(struct expression *left, int comparison, struct express
 /* smatch_expressions.c */
 struct expression *zero_expr();
 struct expression *value_expr(long long val);
+struct expression *value_expr_sval(sval_t sval);
 struct expression *member_expression(struct expression *deref, int op, struct ident *member);
 struct expression *preop_expression(struct expression *expr, int op);
 struct expression *deref_expression(struct expression *expr);
diff --git a/validation/sm_bits1.c b/validation/sm_bits1.c
new file mode 100644
index 00000000..a2b75c00
--- /dev/null
+++ b/validation/sm_bits1.c
@@ -0,0 +1,23 @@
+#include "../check_debug.h"
+
+unsigned int frob();
+
+void test(void)
+{
+        unsigned int x = frob();
+        if (x & ~1)
+                return; 
+        __smatch_bits(x);
+        __smatch_implied(x);
+}
+
+
+/*
+ * check-name: smatch bits 1
+ * check-command: smatch sm_bits1.c
+ *
+ * check-output-start
+sm_bits1.c:10 test() bit info 'x': definitely set 0x0.  possibly set 0x1.
+sm_bits1.c:11 test() implied: x = '0-1'
+ * check-output-end
+ */
-- 
2.32.0

^ permalink raw reply related	[flat|nested] 4+ messages in thread

* [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of
  2021-07-13 12:50 [PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition Harshvardhan Jha
@ 2021-07-13 12:50 ` Harshvardhan Jha
  2021-07-13 15:35   ` Dan Carpenter
  0 siblings, 1 reply; 4+ messages in thread
From: Harshvardhan Jha @ 2021-07-13 12:50 UTC (permalink / raw)
  To: smatch; +Cc: dan.carpenter, Harshvardhan Jha

Imagine we have code like:
	if ((1 << foo) & valid_bits) {

The handle_bit_test() function is supposed to answer the question,
"what does that condition mean about 'foo'"?

This patch fixes several bugs:
1)  The range is off by one.  ffsll() returns 1 for BIT(0) so we need
    to subtract 1 from what ffsll() returns.
2)  This code returns early for impossible conditions but it is better
    to set "foo" to the empty state.
3)  The false state was not set.  We can use rl_filter() for that.

Signed-off-by: Harshvardhan Jha <harshvardhan.jha@oracle.com>
---
 smatch_extra.c        | 17 +++++++++--------
 validation/sm_bits2.c | 28 ++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 8 deletions(-)
 create mode 100644 validation/sm_bits2.c

diff --git a/smatch_extra.c b/smatch_extra.c
index e864646a..27bf5a02 100644
--- a/smatch_extra.c
+++ b/smatch_extra.c
@@ -2061,7 +2061,7 @@ static void match_comparison(struct expression *expr)
 
 static bool handle_bit_test(struct expression *expr)
 {
-	struct range_list *orig_rl, *rl;
+	struct range_list *orig_rl, *rl, *true_rl, *false_rl;
 	struct expression *shift, *mask, *var;
 	struct bit_info *bit_info;
 	sval_t sval;
@@ -2083,23 +2083,24 @@ static bool handle_bit_test(struct expression *expr)
 	bit_info = get_bit_info(mask);
 	if (!bit_info)
 		return false;
-	if (!bit_info->possible)
+	if (!bit_info->possible){
+		set_true_false_states_expr(my_id, var, alloc_estate_empty(), NULL);
 		return false;
+	}
 
 	get_absolute_rl(var, &orig_rl);
 	if (sval_is_negative(rl_min(orig_rl)) ||
 	    rl_max(orig_rl).uvalue > type_bits(get_type(shift->left)))
 		return false;
 
-	low.value = ffsll(bit_info->possible);
-	high.value = sm_fls64(bit_info->possible);
+	low.value = ffsll(bit_info->possible) - 1;
+	high.value = sm_fls64(bit_info->possible) - 1;
 	rl = alloc_rl(low, high);
 	rl = cast_rl(get_type(var), rl);
-	rl = rl_intersection(orig_rl, rl);
-	if (!rl)
-		return false;
+	true_rl = rl_intersection(orig_rl, rl);
+	false_rl = rl_filter(orig_rl, rl);
 
-	set_extra_expr_true_false(shift->right, alloc_estate_rl(rl), NULL);
+	set_extra_expr_true_false(shift->right, alloc_estate_rl(true_rl), alloc_estate_rl(false_rl));
 
 	return true;
 }
diff --git a/validation/sm_bits2.c b/validation/sm_bits2.c
new file mode 100644
index 00000000..1a43538a
--- /dev/null
+++ b/validation/sm_bits2.c
@@ -0,0 +1,28 @@
+#include "../check_debug.h"
+
+unsigned int frob();
+
+void test(void)
+{
+	unsigned int mask = 0xff0;
+        unsigned int x = frob();
+
+	if (x < 4 || x > 11)
+		return;
+
+        if ((1 << x) & mask) {
+		__smatch_implied(x);
+                return;
+	}
+        __smatch_implied(x);
+}
+
+/*
+ * check-name: smatch bits 2
+ * check-command: smatch sm_bits2.c
+ *
+ * check-output-start
+sm_bits2.c:14 test() implied: x = '4-11'
+sm_bits2.c:17 test() implied: x = ''
+ * check-output-end
+ */
-- 
2.32.0

^ permalink raw reply related	[flat|nested] 4+ messages in thread

* Re: [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of
  2021-07-13 12:50 ` [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of Harshvardhan Jha
@ 2021-07-13 15:35   ` Dan Carpenter
  0 siblings, 0 replies; 4+ messages in thread
From: Dan Carpenter @ 2021-07-13 15:35 UTC (permalink / raw)
  To: Harshvardhan Jha; +Cc: smatch

I have applied the first commit but this one still needs work.  Consider
this test case:

#include "check_debug.h"

unsigned int frob();

void test(void)
{
	unsigned int mask = 0xff0;
        unsigned int x = frob();

	if (frob())
		mask |= 0x2;

	if (x < 0 || x > 11)
		return;

        if ((1 << x) & mask) {
		__smatch_implied(x);
                return;
	}
        __smatch_implied(x);
}

The output is:

test.c:17 test() implied: x = '1-11'
test.c:20 test() implied: x = '0'

The first implied is correct but the second is wrong.  BIT(1) or 0x2 is
*possibly* set or *possibly not* set.  So on the false path the range
list should be 0-1.

regards,
dan carpenter

^ permalink raw reply	[flat|nested] 4+ messages in thread

* [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of
@ 2021-07-13 18:05 Harshvardhan Jha
  0 siblings, 0 replies; 4+ messages in thread
From: Harshvardhan Jha @ 2021-07-13 18:05 UTC (permalink / raw)
  To: smatch; +Cc: dan.carpenter, Harshvardhan Jha

Imagine we have code like:
	if ((1 << foo) & valid_bits) {

The handle_bit_test() function is supposed to answer the question,
"what does that condition mean about 'foo'"?

This patch fixes several bugs:
1)  The range is off by one.  ffsll() returns 1 for BIT(0) so we need
    to subtract 1 from what ffsll() returns.
2)  This code returns early for impossible conditions but it is better
    to set "foo" to the empty state.
3)  The false state was not set.  We can use rl_filter() for that.

Signed-off-by: Harshvardhan Jha <harshvardhan.jha@oracle.com>
---
 smatch_extra.c        | 17 +++++++++--------
 validation/sm_bits2.c | 28 ++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 8 deletions(-)
 create mode 100644 validation/sm_bits2.c

diff --git a/smatch_extra.c b/smatch_extra.c
index e864646a..27bf5a02 100644
--- a/smatch_extra.c
+++ b/smatch_extra.c
@@ -2061,7 +2061,7 @@ static void match_comparison(struct expression *expr)
 
 static bool handle_bit_test(struct expression *expr)
 {
-	struct range_list *orig_rl, *rl;
+	struct range_list *orig_rl, *rl, *true_rl, *false_rl;
 	struct expression *shift, *mask, *var;
 	struct bit_info *bit_info;
 	sval_t sval;
@@ -2083,23 +2083,24 @@ static bool handle_bit_test(struct expression *expr)
 	bit_info = get_bit_info(mask);
 	if (!bit_info)
 		return false;
-	if (!bit_info->possible)
+	if (!bit_info->possible){
+		set_true_false_states_expr(my_id, var, alloc_estate_empty(), NULL);
 		return false;
+	}
 
 	get_absolute_rl(var, &orig_rl);
 	if (sval_is_negative(rl_min(orig_rl)) ||
 	    rl_max(orig_rl).uvalue > type_bits(get_type(shift->left)))
 		return false;
 
-	low.value = ffsll(bit_info->possible);
-	high.value = sm_fls64(bit_info->possible);
+	low.value = ffsll(bit_info->possible) - 1;
+	high.value = sm_fls64(bit_info->possible) - 1;
 	rl = alloc_rl(low, high);
 	rl = cast_rl(get_type(var), rl);
-	rl = rl_intersection(orig_rl, rl);
-	if (!rl)
-		return false;
+	true_rl = rl_intersection(orig_rl, rl);
+	false_rl = rl_filter(orig_rl, rl);
 
-	set_extra_expr_true_false(shift->right, alloc_estate_rl(rl), NULL);
+	set_extra_expr_true_false(shift->right, alloc_estate_rl(true_rl), alloc_estate_rl(false_rl));
 
 	return true;
 }
diff --git a/validation/sm_bits2.c b/validation/sm_bits2.c
new file mode 100644
index 00000000..1a43538a
--- /dev/null
+++ b/validation/sm_bits2.c
@@ -0,0 +1,28 @@
+#include "../check_debug.h"
+
+unsigned int frob();
+
+void test(void)
+{
+	unsigned int mask = 0xff0;
+        unsigned int x = frob();
+
+	if (x < 4 || x > 11)
+		return;
+
+        if ((1 << x) & mask) {
+		__smatch_implied(x);
+                return;
+	}
+        __smatch_implied(x);
+}
+
+/*
+ * check-name: smatch bits 2
+ * check-command: smatch sm_bits2.c
+ *
+ * check-output-start
+sm_bits2.c:14 test() implied: x = '4-11'
+sm_bits2.c:17 test() implied: x = ''
+ * check-output-end
+ */
-- 
2.32.0

^ permalink raw reply related	[flat|nested] 4+ messages in thread

end of thread, other threads:[~2021-07-13 18:09 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-07-13 12:50 [PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition Harshvardhan Jha
2021-07-13 12:50 ` [PATCH 2/2] extra: Fix handle_bit_test so that null set condition is taken care of Harshvardhan Jha
2021-07-13 15:35   ` Dan Carpenter
2021-07-13 18:05 Harshvardhan Jha

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.