From: Dan Carpenter Date: Mon, 15 Jul 2013 06:38:38 +0000 (+0300) Subject: math: improve how bitwise ANDs are handled X-Git-Tag: 1.59~1 X-Git-Url: https://repo.or.cz/w/smatch.git/commitdiff_plain/e4251a39fb409ff9c0e03b04e51acd60f38a92fc math: improve how bitwise ANDs are handled Before it just calculated the the 0-max from both sides and took the intersection. In the new way, we take zero, and the min with one bit set up to the max for both sides and find the intersection. So before if we had 0xff00 then we took "0-0xff00" but now we do "0,0x0100-0xff00" It's still not very accurate really but it's an improvement. Signed-off-by: Dan Carpenter --- diff --git a/smatch_math.c b/smatch_math.c index 12389306..c1643dc3 100644 --- a/smatch_math.c +++ b/smatch_math.c @@ -239,34 +239,68 @@ static struct range_list *handle_mod_rl(struct expression *expr, int implied) return alloc_rl(zero, right); } +static sval_t sval_lowest_set_bit(sval_t sval) +{ + int i; + int found = 0; + + for (i = 0; i < 64; i++) { + if (sval.uvalue & 1ULL << i) { + if (!found++) + continue; + sval.uvalue &= ~(1ULL << i); + } + } + return sval; +} + static struct range_list *handle_bitwise_AND(struct expression *expr, int implied) { struct symbol *type; struct range_list *left_rl, *right_rl; + sval_t known; if (implied != RL_IMPLIED && implied != RL_ABSOLUTE) return NULL; type = get_type(expr); - left_rl = _get_rl(expr->left, implied); - if (left_rl) { + if (get_implied_value(expr->left, &known)) { + sval_t min; + + min = sval_lowest_set_bit(known); + left_rl = alloc_rl(min, known); left_rl = cast_rl(type, left_rl); - left_rl = alloc_rl(sval_type_val(type, 0), rl_max(left_rl)); + add_range(&left_rl, sval_type_val(type, 0), sval_type_val(type, 0)); } else { - if (implied == RL_HARD) - return NULL; - left_rl = alloc_whole_rl(type); + left_rl = _get_rl(expr->left, implied); + if (left_rl) { + left_rl = cast_rl(type, left_rl); + left_rl = alloc_rl(sval_type_val(type, 0), rl_max(left_rl)); + } else { + if (implied == RL_HARD) + return NULL; + left_rl = alloc_whole_rl(type); + } } - right_rl = _get_rl(expr->right, implied); - if (right_rl) { + if (get_implied_value(expr->right, &known)) { + sval_t min; + + min = sval_lowest_set_bit(known); + right_rl = alloc_rl(min, known); right_rl = cast_rl(type, right_rl); - right_rl = alloc_rl(sval_type_val(type, 0), rl_max(right_rl)); + add_range(&right_rl, sval_type_val(type, 0), sval_type_val(type, 0)); } else { - if (implied == RL_HARD) - return NULL; - right_rl = alloc_whole_rl(type); + right_rl = _get_rl(expr->right, implied); + if (right_rl) { + right_rl = cast_rl(type, right_rl); + right_rl = alloc_rl(sval_type_val(type, 0), rl_max(right_rl)); + } else { + if (implied == RL_HARD) + return NULL; + right_rl = alloc_whole_rl(type); + } } return rl_intersection(left_rl, right_rl); diff --git a/validation/sm_bitwise1.c b/validation/sm_bitwise1.c new file mode 100644 index 00000000..9b8ba834 --- /dev/null +++ b/validation/sm_bitwise1.c @@ -0,0 +1,22 @@ +#include "check_debug.h" + +unsigned int x; +void test(void) +{ + __smatch_implied(x & 0x1); + __smatch_implied(x & 0x2); + __smatch_implied(x & ~(0xffU)); + __smatch_implied(x & ~(0xff)); +} + +/* + * check-name: smatch bitwise #1 + * check-command: smatch -I.. sm_bitwise1.c + * + * check-output-start +sm_bitwise1.c:6 test() implied: x & 1 = '0-1' +sm_bitwise1.c:7 test() implied: x & 2 = '0,2' +sm_bitwise1.c:8 test() implied: x & ~(255) = '0,256-4294967040' +sm_bitwise1.c:9 test() implied: x & ~(255) = '0-u32max' + * check-output-end + */