On Feb 16, 2016, at 3:53 PM, Dan Carpenter wrote:
> I have re-written your test.c file and written a patch:
Thanks!
It seems your standalone test app does not trigger the error either with or without the patch, though?
(before the patch)
$ ./smatch -p=kernel lock_test.c
lock_test.c:18 test_func() [check_locking] 'mutex:&a_mutex' = 'merged' (locked, unlocked, merged)
(after the patch):
$ ./smatch -p=kernel lock_test.c
lock_test.c:17 test_func() [check_locking] 'mutex:&a_mutex' = 'merged' (unlocked, impossible, merged)
> diff --git a/check_locking.c b/check_locking.c
> index d74ba9e..0d9ae01 100644
> --- a/check_locking.c
> +++ b/check_locking.c
> @@ -38,6 +38,7 @@ static int func_has_transition;
> STATE(locked);
> STATE(start_state);
> STATE(unlocked);
> +STATE(impossible);
> +static void pre_merge_hook(struct sm_state *sm)
> +{
> + if (is_impossible_path())
> + set_state(my_id, sm->name, sm->sym, &impossible);
Ah, unchecked for state to override whatever the state was assumed for that path - sneaky ;)
Luckily there's no printing of where we locked as that merge would totally throw it off.
Anyway, while this test case is fixed, I run it across our codebase and noticed that one
true positive has been silenced too.
void up(struct semaphore *);
void down(struct semaphore *);
int some_random_stuff(void);
void test_func2(void)
{
struct semaphore a_sem;
if (some_random_stuff)
goto out;
up(&a_sem);
for (;;) {
if (some_random_stuff)
break;
}
out:
up(&a_sem);
__smatch_states("check_locking");
}
the goto out part is critical, the warning does not disappear.
merging in the discussion from the other email:
>> 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.
Yes, it's basically:
+int is_impossible_path_stree(struct stree *stree)
+{
+ if (get_state_stree(stree, my_id, "impossible", NULL) == &impossible)
+ return 1;
+ return 0;
+}
so pretty much is_impossible_path copy that takes an stree for the argument.
Yes, I figured out already it did not work, though not sure why. But in any case if I wanted this,
the check for implied_condition_true() in IF_STMT was the way to go, if only it worked as good as I hoped ;)
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
