Hello tao.zhang,
what is the actual criterion by which you want to add a constraint? A
pointer need not point at (exactly) one object. In your example it seems
as if the driver makes certain guarantees about how the function is
called (it passes a pointer to an array and what should presumably be a
valid index for it), which means just crafting the driver in a way that
encodes the constraints (personally, I prefer using branches, but
`klee_assume` will also work) is the canonical and sensible way of
dealing with the issue.
Take the following examples, in which `p` points to some integer array
and `n` is constrained to be a valid index to that array:
```
int example_a(int* p, int n) {
int* my_null = NULL;
return my_null[n]; // error
}
int example_b(int* p, int n) {
int arr[] = { 1 };
int* q = (n % 2 == 0 ? p : q);
return q[n]; // points at different objects, depending on n
}
int example_c(int* p, int n) {
return p[n + 1]; // while `n` is a valid index, `n + 1` is not
}
int example_d(int* p, int n) {
int arr[] = { 1 };
return arr[n]; // while `n` is valid index for `p`, it is not
necessarily a valid index for `arr`
```
Best,
Daniel
On 03/07/2024 16:05, im wrote:
Thanks for your reply！
I may not have described it clearly，I use klee to generate test cases
for a source code.
On the basis of not changing the source code,I want to generate cases
to cover all the path.
If the code test.c is written like this:
int my_test(int *p,int index){
if (p[index] > 5){
/*....*/
}
for (int i = 0;i < index;i++){
if (p[index] > 3){/*....*/}
}
}
then I want to generate test cases for the function my_test.
Although this code has bug that it does not limit the value of
index,on the basis of not changing the source code, I want to
automatically generate a driver template (main.c) like that:
#include "test.c"
int main(){
int b[2];
int index,b1,b0;
klee_make_symbolic(&index,sizeof(index),"index");
klee_make_symbolic(&b1,sizeof(b1),"b1");
klee_make_symbolic(&b0,sizeof(b0),"b0");
b[0] = b0;
b[1] = b1;
int *p = b;
my_test(p,index);
}
then I will compile main.c and test.c into xxx.bc, and use klee to do
symbolic execution.
If I can change the origin source code,I may do that as you suggested:
if (index >= 0 && index < 2){
if (p[index] > 5){
/*....*/
}
for (int i = 0;i < index;i++){
if (p[index] > 3){/*....*/}
}
}
or I can also change the driver template (main.c) that:
add code : klee_assume(index >= 0 && index < 2);
insert this code after klee_make_symbolic also limit the index.
But in reality, I cannot do that because the source code test.c cannot
be changed and the conditions in klee_assume that "index < 2" cannot
be known before symbolic execution. The number "2" can be anything if
the source code changed.
So I want to change some code in klee where it handles the
getelementptr instruction and memory allocation,which can help me
automatically avoid the "out of bound pointer" error when processing
getelementptr instruction. Let the symbolic variable "index" be
smaller than a constant if it appears in the offset of a pointer or array.
I have solved the issue with array because I can get the size of array
when handling the gep instruction(in Executor.cpp):
for (gep_type_iterator ii = ib;ii != ie;++ii){
if (isa<ArrayType>(*ii)){
const auto *sq = cast<ArrayType>(*ii);
unsigned int array_len = sq->getNumElements();
}
}
After getting the array_len, I add constraint that : ref<Expr> res =
SleExpr::create(index_expr, ConstantExpr::alloc(array_len,
Context::get().getPointerWidth()));
then the symbolic variable index will not be larger than the
array_len. Is this right?
but when I handle the pointerType,I cannot get the length of the
pointer (not the size of the int*) if it has been allocated by an
array. The pointerType class does not store the information
Take the above as an example, pointer *p is assigned b,the length of
the pointer is "2",then automatically add constraint : create a
SleExpr (index, 2).
If I do not get the pointer size ,use a constant "2" that when
symbolic variable appears in the offset of pointer,add constraint to
let it smaller than "2".Does this work?
I hope you can understand what I mean. thanks for your help!!
Best
tao.zhang
------------------------------------------------------------------------
im
1527733...@qq.com
<https://wx.mail.qq.com/home/index?t=readmail_businesscard_midpage&nocheck=true&name=im&icon=http%3A%2F%2Fthirdqq.qlogo.cn%2Fek_qqapp%2FAQUbwicK99G5LXTRpfGianK2yzIx8bodz3ebltdfw84mw00iawCSicRShcPsFAYugwvJMDxnDZ4b%2F0&mail=1527733628%40qq.com&code=aJif2h2RDikCujQYWJmJFsvEdzcRTprdzuy7L_djga3AF3Bn1gVBgnR1VBF6yIcj4V7vK4dvNx1UOzze3I8iiw>
------------------ 原始邮件 ------------------
*发件人:* "Daniel Schemmel" <d.schem...@imperial.ac.uk>;
*发送时间:* 2024年7月3日(星期三) 晚上6:54
*收件人:* "klee-dev"<klee-dev@imperial.ac.uk>;
*主题:* Re: [klee-dev] symbolic variable appears in the offset of a
pointer or an array
Hello,
if you wish to only execute a piece of code (such as `if (p[x] > 3) { /*
... */ }`) when a condition (such as `x >= 0 && x < sizeof(b) /
sizeof(*b)`) holds, you can use an if statement like this:
```
if (x >= 0 && x < sizeof(b) / sizeof(*b)) {
if (p[x] > 3){ /*...*/ }
if (b[x] > 3){ /*...*/ }
for (int i = 0;i < x;i++){ /* p[i] ... */ }
}
```
Best,
Daniel
On 2024-07-02 03:35, im wrote:
> I hope to use Klee to help me in generating test cases, and I have met
> some problems.
> When the symbolic variable appears in the offset of a pointer or an
> array, such as:
> int *p;
> int b[3];
> int x;
> klee_make_symbolic(&x,sizeof(x),"x");
> if (p[x] > 3){...}
> if (b[x] > 3){...}
> for (int i = 0;i < x;i++){ p[i] ... }
> during the symbolic execution,it always occurs error like "out of
> bound pointer",
> And the value of x that solved by klee also is greater than the size
> of the pointer or array.
> If the pointer is allocated memory by a sized array, such as:
> p = b;
> How can I make sure that the symbolic variable x is restricted from
0-2 ?
>
> I have an idea that when I fix with the gep instruction in
> executeInstruction(), if the offset is not a constantexpr and the
> geptype has <ArrayType>, I append two constraints that x >=0 and x <
> sizeof(b).So that the symbolic value x will not be out of bound.This
> can solve the problem of array,but I do not know how to fix pointer.
> If the pointer is allocates memory by a sized array(int *p = b),I hope
> that the offset should be restricted from 0 to the size of the array,
> but when I fix with the gep instruction(p[x]),I cannot get the size of
> the array.I only know the pointer type and the size of the type from
> the gep instruction.How can I do it?
> My English is not so good, sorry
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
