On Mon, Jan 05, 2015 at 01:54:46PM -0500, Josef 'Jeff' Sipek wrote:
> While I'm writing this email, I might as well point out a false positive
> smatch told me about. I have a program that takes an year and month as a 6
> digit number (e.g., 201501) and I want double check that it's valid. (The
> first 4 digits look like a year and the last two digits look like a month
> number.) Later on, I use the month part to index into an array of month
> names. Here's a simplified test case:
I've changed your test case a little to add some smatch debugging stuff:
#include <stdio.h>
#include <unistd.h>
#include "check_debug.h"
static int validate_arch_id(int arch)
{
int y = arch / 100;
int m = arch % 100;
return (m >= 1) && (m <= 12) && (y >= 1970) && (y < 2100);
}
int main(int argc, char **argv)
{
static const char *months[12] = {
"January", "February", "March", "April", "May", "June",
"July", "August", "September", "October", "November",
"December",
};
int arch = 201201; /* test */
int y = arch / 100;
int m = arch % 100;
__smatch_implied(arch / 100);
__smatch_implied(arch % 100);
__smatch_implied(validate_arch_id(arch));
__smatch_implied((m >= 1) && (m <= 12) && (y >= 1970) && (y < 2100));
if (!validate_arch_id(arch))
arch = 197001;
__smatch_implied(arch);
printf("%s\n", months[(arch % 100) - 1]);
return 0;
}
If I run ./smatch test.c then this is the output:
test.c:26 main() implied: arch / 100 = '2012'
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 = '197001,201201'
test.c:36 main() error: buffer overflow 'months' 12 <= 98
And, oh crap, it thinks 201201 % 100 is 0-99 instead of 1. I have
written a fix for that and I'll test it and push later. Now the output
is:
test.c:26 main() implied: arch / 100 = '2012'
test.c:27 main() implied: arch % 100 = '1'
test.c:28 main() implied: validate_arch_id(arch) = '0-1'
test.c:29 main() implied: (m >= 1) && (m <= 12) && (y >= 1970) && (y < 2100) = '1'
test.c:34 main() implied: arch = '197001,201201'
test.c:36 main() error: buffer overflow 'months' 12 <= 98
Really given that 201201 is a valid date, I can make:
test.c:28 main() implied: validate_arch_id(arch) = '0-1'
into:
test.c:28 main() implied: validate_arch_id(arch) = '1'
I have written this patch and I'll test it.
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.
Another idea that occurs to me is that '197001,201201' % 100 can be
calculated as '197001 % 100, 201201 % 100' and we know that is '1'
instead of 0-99 which makes the error message go away.
But none of that helps in the real life case where we don't start out
with "arch = 201201;". 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
I maybe should remove the "foo % 100" as something which generates an
array out of bounds warning... I've gone back and forth on this one.
Let me think about that.
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
