public inbox for smatch@vger.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 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
  -- strict thread matches above, loose matches on Subject: below --
2021-07-13 18:05 Harshvardhan Jha

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox