[PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition

[PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition

[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_extra.c        | 72 +++++++++----------------------------------
 smatch_extra.h        |  1 +
 validation/sm_bits1.c | 23 ++++++++++++++
 3 files changed, 39 insertions(+), 57 deletions(-)
 create mode 100644 validation/sm_bits1.c

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

[PATCH 2/2] [PATCH 2/2] Fix handle_bit_test so that null set condition is taken care of

[Harshvardhan Jha]

The handle_bit_test condition wasn't setting a false range_list for the
false state and hence the implied rl was coming out to be false. The
false and true rls have been calculating using rl_intersection and
rl_filter commands.

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

Re: [PATCH 2/2] [PATCH 2/2] Fix handle_bit_test so that null set condition is taken care of

[Dan Carpenter]

On Mon, Jul 12, 2021 at 06:24:28PM +0530, Harshvardhan Jha wrote:
> ---
>  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);

The false_rl isn't correct.  For the false_side we should use
bit_info->set instead of bit_info->possible.  It doesn't matter in the
test code because the value of mask is known so the possibly set and
the definitely set are the same.

In other words there can be some overlap between the potential values
on the true path and the false path.

regards,
dan carpenter

Re: [PATCH 1/2] extra: Fix false output of handle_AND_op and handle_AND_condition

[Dan Carpenter]

On Mon, Jul 12, 2021 at 06:24:27PM +0530, Harshvardhan Jha wrote:
> 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_extra.c        | 72 +++++++++----------------------------------
>  smatch_extra.h        |  1 +
>  validation/sm_bits1.c | 23 ++++++++++++++

We've got the .h now but not the smatch_expressions.c file.  ;)

regards,
dan carpenter