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.
>> After all this is just a small attempt at distilling down the actual real world code
>> (see live example in drivers/staging/lustre/lustre/llite/lloop.c::loop_thread() )
>
> It's saying that that loop is a forever loop because we set
> "lo->lo_state = LLOOP_BOUND;" at the start of the function and only
> exit when it is set to LLOOP_RUNDOWN which I guess hapens in another
> thread?
>
> Smatch doesn't understand about threads... I don't even have a roadmap
> in my head how to handle this situation.
I understand.
That's why it should always be complaining about the double unlock, right? With your patch
that tracks impossible states it no longer does this.
>>> If you unlock a (&start_state + &unlocked) then it probably should
>>> generate a warning but it doesn't... Check_locking is one of the oldest
>>> remaining checks and it needs to be re-written.
>> I actually noticed it has several modes of operation, sometimes just warning about
>> inconsistent locking and sometimes actually elaborating that here, here and here
>> we return locking, and there, thee and there we return unlocked.
> Yeah. It's not beautiful. The main thing though is that it doesn't do
> cross function analysis…
The other parts of the code do, as in they know what function changes what, don't they?
That's the whole point of the build_kerel_data step that then populates the database I think?
Anyway I am just hoping to provide a bit more output so tha it's easier to cross reference what
the bug refers to without rereading the whole code many times (not a bad thing, mind you, but sometimes extra help is good too).
>>> Thanks for the help on getting lustre to compile. I'm looking at the
>>> warning:
>>> lustre/llite/llite_lib.c:1709 ll_setattr_raw() warn: 'mutex:&inode->i_mutex' is sometimes locked here and sometimes unlocked.
>>> I see a bug in the flow analysis handling:
>>>
>>> if ((((inode->i_mode) & S_IFMT) == S_IFREG))
>>>
>>> The smatch_stored_conditions.c file ignores comparisons because
>>> smatch_extra.c is supposed to handle those. But smatch_extra.c doesn't
>>> handle it either...
>>
>> So you mean the the warning going away with my patch was just an
>> unintended bug and some real world bugs would be hidden by it?--
>
> Smatch wasn't seing that the if (S_ISREG(inode->i_mode)) checks were
> related so it *should* have complained.
>
> Your patch is doing a clone_sm(). The sm has the data about where a
> state is from.
Yes, and I think the merge logic has a bug, that's why my patch.
>
> if (x) {
> foo = 0; <-- foo is from here.
> } else if (y) {
> foo = 1; <-- or here.
> } else {
> foo = 2;
> }
> <-- foo is a merged state 1-3.
>
> if (foo) { <-- we look at all the original places where foo was
> set. If foo is non-zero then we then we take
> the value of x in all those places and merge
> them together to get the implied x for the true
> side. So x is zero.
My patch does not change the logic for this at all.
> The clone_sm() copies over that data but really we just want to copy the
> line number.
>
> + if (one->line == two->line)
> + result->line = one->line;
Well, sort of. I thought about line number copying too, but then it looked like
copying the entire state was better when I looked at it.
Note that you probably want to also check against "ghost" states and assign the line to the other one at the very least?
I see they are not used anywhere, really, so my neatificaton in output might have been due to another change, I guess.
It also looked like I can return directly either one or two depending on the outcome (since really there's no new state),
but that did not work all that well. Also the example most well demonstrating the scope of the change where the flow of
logic is most affected is this:
a = 1;
if (b) <-- split point, here we'll have a=1 for both branches of the execution.
c = 2;
{merge point}. <- Here we would combine back the value of a=1 and where it used to be "a=1, line XXX", it becomes "a=1 {1 L(XXX), 1 L(XXX)}, line XXX+2".
Even if we change XXX+2 back into XXX, I feel like this is not enough because really this particular merge did not really produce a new complex state,
the state really is the same, dating back to XXX, and the condition did not really change it nor did any of the conditional branches.
In fact in the merge function just above my patching place there's even a check for one == two; return one;
> Sorry if these emails are longer and include a lot of unrelated
> information :P It feels great to have these sorts of discussion.
This is good for me too, and hopefully others (now and later when reading the archives).
--
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
