Discussion:
Strange behavior of KLEE when evaluating NULL pointer
Qiuping Yi
2014-05-13 10:09:48 UTC
Permalink
Hi, everyone

I found a strange behavior of KLEE.

When I applied KLEE to the next code snippet, a out-of-bound-pointer error
happened at line 3. However, this code snippet explicitly allocates space
for pointer p at line 2 when it is evaluated to NULL. So what's wrong?

0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));

3 *p = 2;
}

Best Regards!

--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
Paul Thomson
2014-05-13 10:50:16 UTC
Permalink
Please can you provide the code that calls test?

Or, please try using something like:

int main()
{
int *p = NULL;
test(p);
return 0;
}


Thanks,
Paul
Post by Qiuping Yi
Hi, everyone
I found a strange behavior of KLEE.
When I applied KLEE to the next code snippet, a out-of-bound-pointer error
happened at line 3. However, this code snippet explicitly allocates space
for pointer p at line 2 when it is evaluated to NULL. So what's wrong?
0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Qiuping Yi
2014-05-14 14:43:15 UTC
Permalink
Hi, Paul

Next is my whole test code:

1void test2(int *p) {
2 if (p == NULL)
3 p = malloc(sizeof(*p));

4 *p = 1;
}

5 int main() {
6 int *p;
7 test(p);
8 return 0;
}

This code was executed without any error after compiled with gcc. However, when
I applied KLEE to this code, it encountered an 'out of bound pointer'
error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
needs to explicitly initialize each variable, containing the pointers,
right?



--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
Post by Paul Thomson
Please can you provide the code that calls test?
int main()
{
int *p = NULL;
test(p);
return 0;
}
Thanks,
Paul
Post by Qiuping Yi
Hi, everyone
I found a strange behavior of KLEE.
When I applied KLEE to the next code snippet, a out-of-bound-pointer
error happened at line 3. However, this code snippet explicitly allocates
space for pointer p at line 2 when it is evaluated to NULL. So what's wrong?
0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Oscar Soria Dustmann
2014-05-14 14:51:36 UTC
Permalink
Hi Qiuping,

your code exhibits undefined behaviour as you read from uninitialised
memory. The reason it doesn't fail when run natively is implementation
defined and pure luck. It's not that KLEE needs the initialisation; The
C standard demands it (reason behind it: Stack variables are not
default-initialised for performance reasons).

I'd actually consider it desired behaviour for a testtool to throw you
an error.

Cheers,
Oscar
Post by Qiuping Yi
Hi, Paul
1void test2(int *p) {
2 if (p == NULL)
3 p = malloc(sizeof(*p));
4 *p = 1;
}
5 int main() {
6 int *p;
7 test(p);
8 return 0;
}
This code was executed without any error after compiled with gcc. However, when
I applied KLEE to this code, it encountered an 'out of bound pointer'
error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
needs to explicitly initialize each variable, containing the pointers,
right?
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
Post by Paul Thomson
Please can you provide the code that calls test?
int main()
{
int *p = NULL;
test(p);
return 0;
}
Thanks,
Paul
Post by Qiuping Yi
Hi, everyone
I found a strange behavior of KLEE.
When I applied KLEE to the next code snippet, a out-of-bound-pointer
error happened at line 3. However, this code snippet explicitly allocates
space for pointer p at line 2 when it is evaluated to NULL. So what's wrong?
0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Qiuping Yi
2014-05-14 15:20:28 UTC
Permalink
Hi Oscar, Hongxu,

Thank you for you comment.

Yes, you are right. In practice, my test code have an uninitialized error.
But now I am considering some variables from external environment. These
variables may be uninitialized, so I use pointer p in function 'test' to
describe such a simple situation. I want to use the if-statement at line 2
to judge whether the external pointer p is NULL, if it is I want to
explicitly allocate some space to it at line 3. But now I know KLEE cannot
judge on an uninitialized pointer.



--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Wed, May 14, 2014 at 10:51 PM, Oscar Soria Dustmann <
Post by Oscar Soria Dustmann
Hi Qiuping,
your code exhibits undefined behaviour as you read from uninitialised
memory. The reason it doesn't fail when run natively is implementation
defined and pure luck. It's not that KLEE needs the initialisation; The
C standard demands it (reason behind it: Stack variables are not
default-initialised for performance reasons).
I'd actually consider it desired behaviour for a testtool to throw you
an error.
Cheers,
Oscar
Post by Qiuping Yi
Hi, Paul
1void test2(int *p) {
2 if (p == NULL)
3 p = malloc(sizeof(*p));
4 *p = 1;
}
5 int main() {
6 int *p;
7 test(p);
8 return 0;
}
This code was executed without any error after compiled with gcc.
However, when
Post by Qiuping Yi
I applied KLEE to this code, it encountered an 'out of bound pointer'
error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
needs to explicitly initialize each variable, containing the pointers,
right?
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
Post by Paul Thomson
Please can you provide the code that calls test?
int main()
{
int *p = NULL;
test(p);
return 0;
}
Thanks,
Paul
Post by Qiuping Yi
Hi, everyone
I found a strange behavior of KLEE.
When I applied KLEE to the next code snippet, a out-of-bound-pointer
error happened at line 3. However, this code snippet explicitly
allocates
Post by Qiuping Yi
Post by Paul Thomson
Post by Qiuping Yi
space for pointer p at line 2 when it is evaluated to NULL. So what's
wrong?
Post by Qiuping Yi
Post by Paul Thomson
Post by Qiuping Yi
0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Loading...