On Wed, Jan 07, 2015 at 11:33:58AM +0300, Dan Carpenter wrote:
> Ok. I've pushed the two patches I mentioned earlier.
Thanks!
> On Tue, Jan 06, 2015 at 12:13:12PM -0500, Josef 'Jeff' Sipek wrote:
> > ...
> > > The next question is should I make:
> > > test.c:34 main() implied: arch = '197001,201201'
> > > into:
> > > test.c:34 main() implied: arch = '201201'
> > > I don't think I want to do that. It's a philosophical debate because
> > > how should you handle impossible conditions? In this case we know that
> > > the date is valid so we could ignore that whole if condition but the
> > > problem is that Smatch is often wrong about the stuff which it "knows"
> > > so I normally pretend that nothing is impossible.
> >
> > Hrm? I'm a little confused about how that's possible. I am (naively?)
> > assuming that smatch incrementally builds its view of the world by assuming
> > nothing and using logic to determine what's possible and what's not. I'm
> > not sure where this uncertainty could come from.
>
> One problem is that there is a lot of bugs in impossible to reach code
> so I want to warn about those. There is a lot of impossible to reach
> code, btw.
>
> But a bigger problem for Smatch is that it's super bad about handling
> loops. It just goes through it one time. It handles canonical for
> loops as a special case. So it thinks a lot of code is impossible when
> really it's not.
Aha! Not handling loops fully/correctly would cause all sort of funny
conclusions.
> Also Smatch assumes there is only one thread so some conditions which
> look impossible actually are possible with multi-threading.
Good to know.
> > > But none of that helps in the real life case where we don't start out
> > > with "arch = 201201;".
> >
> > Agreed. Here's what I get with "int arch = atoi(argv[1]);":
> >
> > $ ../oss/smatch/smatch -D__amd64 test.c
> > test.c:26 main() implied: arch / 100 = ''
> > test.c:27 main() implied: arch % 100 = '0-99'
> > test.c:28 main() implied: validate_arch_id(arch) = '0-1'
> > test.c:29 main() implied: (m >= 1) && (m <= 12) && (y >= 1970) && (y < 2100) = '0-1'
> > test.c:34 main() implied: arch = 's32min-s32max'
> > test.c:36 main() error: buffer overflow 'months' 12 <= 98
> >
> > > The problem is Smatch only tracks whole
> > > variables so it understands "var <= 12" but it doesn't understand
> > > "arch % 100 <= 12". I have some ideas about changing this, but it's
> > > going to take months before I can look at it. Also to track this across
> > > function boundaries? Forget about that... :P
> >
> > Heh, I knew this was a bit of a tall order when I was writing my original
> > email :)
> >
> > Huh... now I'm confused. I changed the code so that "validate" would
> > actually return the year & month components:
> >
> > static int parse_arch_id(int arch, int *y, int *m)
> > {
> > *y = arch / 100;
> > *m = arch % 100;
> >
> > return (m >= 1) && (m <= 12) && (y >= 1970) && (y < 2100);
>
> This test needs to be updated by the way. The "m" should be "*m" now.
Doh! That's what I get for not trying to compile it and only running
smatch.
> When you fix that then it will get the months correct as "1-12". But
> gar... It still doesn't get the year right that it's '1970-2099'. Ok.
> I have written a patch for this and I will try test it and push
> tomorrow.
Cool, let me know if you want me to test anything.
Jeff.
--
Bad pun of the week: The formula 1 control computer suffered from a race
condition
--
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
