Powered by Linux
Re: Better handling of always true conditions. — Semantic Matching Tool

Re: Better handling of always true conditions.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



On Sun, Feb 14, 2016 at 03:16:24PM -0500, Oleg Drokin wrote:
> Hello!
> 
>     This is mostly stream of thought at this point, I guess than a question, but might be somebody find that useful too.
> 
>     I am chasing after a somewhat common false positive that could be demonstrated with this simplistic code:
> 
> int test_func(void)
> {
>         bool lock = false;
>         struct mutex a_mutex;
> 
>         mutex_lock(&a_mutex);             // <= line 448 in my code
>         lock = true;
> 
>         if (lock)                         // <= line 451
>                 mutex_unlock(&a_mutex);   // <= line 452
> 
>         return 0;
> }
> 
>     Currently this produces the following warning:
> test_func() warn: 'mutex:&a_mutex' is sometimes locked here and sometimes unlocked.
> 
> 
>     The impossible code already knows that the condition is always true:
> 451 test_func() set_true_false 'impossible'.  Was (null).  Now T:undefined F:impossible
> 
>     Even despite that the else part of the state is produced and then merged back in:
> 452 test_func() merge [check_locking] 'mutex:&a_mutex' locked(L 448) + unlocked(L 452) => merged (locked, unlocked, merged)
> 452 test_func() merge [register_impossible] 'impossible' impossible(L 451) + undefined(L 451) => merged (impossible, undefined, merged)
> 452 test_func() merge [register_smatch_extra] 'lock' (L 451) + 1(L 451) => 1 (1, , 1)
> 
>    The last line is esp. interesting, it basically is poisoning the 'lock' possible values with an "empty" one for the "false" path, I think we could be doing something more smart here for the case where it does matter?

Half the time the empty states just indicate a bug in Smatch.  We muddle
along and hope for the best.  ;)  In this case, it's doing the right
thing.  1 + <empty> is 1.

> 
>    In the end this throws things away and just the mere if statement makes internal state think that the non-unlocking path could somehow happen (which of course it cannot).
>    Also if I add an else statement there, one would think that the "unreachable code" warning is in order too, but nope… (not that I need this particular warning here).

There is so much unreachable code in the kernel.  A lot of it is there
for a good reason too like sanity checks.  That would generate too many
warnings.

> 
>    I tried to somewhat straightforwardly fix this by just checking in the __merge_true/false_states if the corresponding slist is "impossible", and if so, to not merge it back in, turning the function into the discard version:
> @@ -769,7 +769,8 @@ void __merge_false_states(void)
>         struct stree *stree;
>  
>         stree = pop_stree(&false_stack);
> -       merge_stree(&cur_stree, stree);
> +       if (!is_impossible_path_stree(stree))
> +               merge_stree(&cur_stree, stree);
>         free_stree(&stree);
>  }
> 
> 
>     Somehow this does not really have any effect so the state merge must be coming from somewhere else, but I don't readily see where from?

The is_impossible_path_stree() function is something you wrote.  It
looks like it should sort of work to me...  But that stuff is so
knotted that I can't say...  Anyway, I don't think this is the right
approach.

> 
>     Anyway, I noticed that if I change "lock" to "1" on the line 451, then all works ok and it seems this is due to known_condition_true/false checks in __split_stmt STMT_IF case.
>     The condition is evaluated as RL_EXACT.

Yep.

> 
>     So why can't we use implied_condition_true? Seems to be not so bad idea since it already checks for known value too. This certainly fixes the warning I am after…
>     But I guess it cannot be this simple, testing on a bigger codebase, I notice that it produces a lot of "ignoring unreachable code" false positives when failing to anticipate
>     that some intermediate functions change various values between assignment and check even though the previous pass that collects what functions change what is supposedly should be helping here.

Yeah.  That's part of it too...

regards,
dan carpenter
--
To unsubscribe from this list: send the line "unsubscribe smatch" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html



[Index of Archives]     [Linux USB Devel]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]     [Big List of Linux Books]

  Powered by Linux