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 Feb 19, 2016, at 4:22 PM, Dan Carpenter wrote:

> On Fri, Feb 19, 2016 at 12:15:01PM -0500, Oleg Drokin wrote:
>> 
>> On Feb 19, 2016, at 2:49 AM, Dan Carpenter wrote:
>> 
>>> On Thu, Feb 18, 2016 at 05:35:47PM -0500, Oleg Drokin wrote:
>>>> 
>>>> On Feb 18, 2016, at 5:04 PM, Dan Carpenter wrote:
>>>> 
>>>>> On Wed, Feb 17, 2016 at 10:47:45AM -0500, Oleg Drokin wrote:
>>>>>> Does not matter, I noticed the lack of the function call and changed it to be one and did not
>>>>>> see any difference in smatch output.
>>>>>> 
>>>>> 
>>>>> For me it works...  I get a double unlock bug.
>>>> 
>>>> I think we are talking about different things.
>>>> I get double unlock bug too every time. Unless your patch is applied and then I don't.
>>> I'm totally lost.  What do you want it to do?
>> 
>> I think the code with double up should report as a bug (double unlock).
>> Your patch (the one about checking impossible state) silences it which makes me think
>> some other true positives would be silenced too?
>> The testcase I came up with does not work, but the original code still shows this, that's how I noticed it.
> 
> It does print the double unlock warning, though.  Maybe send me your
> exact test file.

So it turned out to be a lot more fringe than I thought.

void up(struct semaphore *);
void down(struct semaphore *);

int some_random_stuff(void);
int a=1;

void test_func2(void)
{
        struct semaphore a_sem;

        if (some_random_stuff)     // <== 1
                goto out;

        up(&a_sem);

        for (;;) {
                if (some_random_stuff)    // <== 2
                        break;
        }

out:
        __smatch_states("check_locking");
        up(&a_sem);
}

Speaking of the new code (old one always prints the warning) the one above does not print the warning and it's correct.

Now if we change some_random_stuff at location 1 to some_random_stuff() - the warning reappears and that's good.
If we only change some_random_stuff to some_random_stuff() at location 2 - the warning also reappears and it's a false positive.
Even if we replace some_random_stuff with a at 2, warning reappears, and even if we only replace some_random_stuff at 1 with a - it reappears again.
But those all are false positives, not false negatives, so I guess we are fine.

> Wow.  Sorry.  We're really talking at cross purposes.  I'm describing
> the flow analysis for drivers/staging/lustre/lustre/llite/lloop.c::loop_thread()
> not the test file.
> 
> In loop_thread() we have a double unlock if "lo->lo_state ==
> LLOOP_RUNDOWN", but that can only happen in another thread so Smatch
> (incorrectly) says it is impossible and ignores it.

Ah, I see. now it all makes sense esp. since we assigned lo->lo_state earlier on in the function.

I imagine it's possible to invalidate a whole struct state (except locks?) if
a lock within that structure was used as that implies there are other threads
at least potentially in place that mess with the structure content (though we don't
really know what parts of it).
I guess this will have it's good and bad sides, since we cannot really know which
parts of the structs really could be accessed by parallel threads so it might as well
lead to worse results than this false negative, so probably just needs to be tried or perhaps even
be retained as an option.

> For the test file, whe the test is "if (some_random_stuff()) " then that
> works, before and after the change.  When it is "if (some_random_stuff) "
> then that is evaulated as always true as you would expect so what
> check_locking sees is:
> 
> void test1(void)
> {
> 	struct semaphore a_sem;
> 
> 	if (always_true)
> 		goto out;
> 	// impossible stuff snipped
> out:
> 	up(&a_sem);
> }
> 
> So originally it would complain about the double unlock but now that
> we're ignoring impossible stuff it doesn't.

Yes, it's clear now.

Except apparently if there's another condition or a loop within that impossible stuff, then it suddenly
forgets that stuff is impossible, but that might be for the better.

Thanks!

Bye,
    Oleg--
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