[klee-dev] 回复： symbolic variable appears in the offset of a pointer or an array

[Daniel Schemmel]

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
> 1527733628 at 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.schemmel at imperial.ac.uk>;
> *发送时间:* 2024年7月3日(星期三) 晚上6:54
> *收件人:* "klee-dev"<klee-dev at 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 at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed