Thanks for your reply!
I want to add the constraints before klee deals with the getelementptr 
instructions in Executor.cpp.
Take arrays as an example:
int b[4];
int x;
klee_make_symbolic(&x,sizeof(x), "x");
if (b[x] > 3){/*... */}


In assembly.ll file, the code "b[x]" is translated into instructions:
%x = ....
%arrayidx = getelementptr [4 x i32], [4 x i32]* %b, i64 0,i64 x
the arrayidx expression may be invalid because x can be out of boundary (if the 
solved value is larger than 3)
when klee deals with the getelementptr instructions in Executor.cpp, the actual 
criterion is that I get the elementnum of the array operand in the gep 
instruction.
I will add constraints to let x &gt;=0 and x < sizeof(b) in the function 
"Executor::executeInstruction(),case Instruction::GetElementPtr" in 
Executor.cpp. 
Then klee can execute correctly,all cases generated are valid (x is in boundary 
0-3).
Handle with pointers by the same method, if pointers have point at an array, I 
will add constraints to let the offset be in boundary of 0-sizeof(array).
If not, I will let the offset smaller than a constant such as "20".
I want to handle all of the above in Klee code , not to change my test code or 
my driver code(I generate the drive code by jinja2 template automatically).
My question is that my above idea for array is feasible ? When I deal with 
pointer and make it like array,it seems has problem in structure pointer,is 
there any better method?
What I expected is that klee can generate correct test cases: the symbolic 
variable which appears in array index or offset of pointer is in boundary. For 
example:
test.c:
int my_test(int b[4],int index){
        if (b[index] &gt; 5){
                /*....*/
        }
        for (int i = 0;i < index;i++){
                if (b[index] &gt; 3){/*....*/}
        }
}
main.c:
#include "test.c"
int main(){
        int b[4];
        int index,b0,b1,b2,b3;
        klee_make_symbolic(&amp;index,sizeof(index),"index");
        klee_make_symbolic(&amp;b0,sizeof(b0),"b0");
        klee_make_symbolic(&amp;b1,sizeof(b1),"b1");
        klee_make_symbolic(&amp;b2,sizeof(b2),"b2");
        klee_make_symbolic(&amp;b3,sizeof(b3),"b3");
        b[0] = b0;
        b[1] = b1;
        b[2] = b2;
        b[3] = b3;
        my_test(b,index);
}
To generate test cases for test.c, I will automatically generate drive code 
"main.c" and then use klee to execute symbolic.

I found that some characters may cause garbled characters to appear as "??", 
I'm sorry for that.


Yours sincerely
tao.zhang


??????:                                                                         
                                               "Daniel Schemmel"                
                                                                    
<d.schem...@imperial.ac.uk&gt;;
????????:&nbsp;2024??7??5??(??????) ????7:24
??????:&nbsp;"klee-dev"<klee-dev@imperial.ac.uk&gt;;

????:&nbsp;Re: [klee-dev]?????? symbolic variable appears in the offset of a 
pointer or an array



           
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) {
       &nbsp; int* my_null = NULL;
       &nbsp; return my_null[n]; // error
       }
       
       int example_b(int* p, int n) {
       &nbsp; int arr[] = { 1 };
       &nbsp; int* q = (n % 2 == 0 ? p : q);
       &nbsp; return q[n]; // points at different objects, depending on n
       }
       
       int example_c(int* p, int n) {
       &nbsp; return p[n + 1]; // while `n` is a valid index, `n + 1` is not
       }
       
       int example_d(int* p, int n) {
       &nbsp; int arr[] = { 1 };
       &nbsp; 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] &gt; 5){
                        /*....*/
                }
                for (int i = 0;i <             index;i++){
                        if (p[index] &gt;             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(&amp;index,sizeof(index),"index");
                klee_make_symbolic(&amp;b1,sizeof(b1),"b1");
                klee_make_symbolic(&amp;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 &gt;= 0 &amp;&amp; index < 2){
                if (p[index] &gt; 5){
                        /*....*/
                }
                for (int i = 0;i <             index;i++){
                        if (p[index] &gt;             3){/*....*/}
                }
         }
         or I can also change the driver template (main.c) that:
         add code : klee_assume(index &gt;= 0 &amp;&amp; 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&gt;(*ii)){
                        const auto *sq =             cast<ArrayType&gt;(*ii);
                        unsigned int array_len =             
sq-&gt;getNumElements();
                }
         }
         After getting the array_len, I add constraint that :           
ref<Expr&gt; 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
                                    
                                       
       
       &nbsp;
                
         
         
         
         ------------------           ???????? ------------------
                    ??????: "Daniel Schemmel"             
<d.schem...@imperial.ac.uk&gt;;
           ????????:&nbsp;2024??7??3??(??????) ????6:54
           ??????:&nbsp;"klee-dev"<klee-dev@imperial.ac.uk&gt;;
           ????:&nbsp;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]         
&gt; 3) { /* 
         ... */ }`) when a condition (such as `x &gt;= 0 &amp;&amp; x         < 
sizeof(b) / 
         sizeof(*b)`) holds, you can use an if statement like this:
         ```
         if (x &gt;= 0 &amp;&amp; x < sizeof(b) / sizeof(*b)) {
         &nbsp;&nbsp; if (p[x] &gt; 3){ /*...*/ }
         &nbsp;&nbsp; if (b[x] &gt; 3){ /*...*/ }
         &nbsp;&nbsp; for (int i = 0;i < x;i++){ /* p[i] ... */ }
         }
         ```
         
         Best,
         Daniel
         
         On 2024-07-02 03:35, im wrote:
         &gt; I hope to use Klee to help me in generating test cases, and       
  I have met 
         &gt; some problems.
         &gt; When the symbolic variable appears in the offset of a         
pointer or an 
         &gt; array, such as:
         &gt; int *p;
         &gt; int b[3];
         &gt; int x;
         &gt; klee_make_symbolic(&amp;x,sizeof(x),"x");
         &gt; if (p[x] &gt; 3){...}
         &gt; if (b[x] &gt; 3){...}
         &gt; for (int i = 0;i < x;i++){ p[i] ... }
         &gt; during the symbolic execution,it always occurs error like         
"out of 
         &gt; bound pointer",
         &gt; And the value of x that solved by klee also is greater than       
  the size 
         &gt; of the pointer or array.
         &gt; If the pointer is allocated memory by a sized array, such         
as:
         &gt; p = b;
         &gt; How can I make sure that the symbolic variable x is         
restricted from 0-2 ?
         &gt;
         &gt; I have an idea that when I fix with the gep instruction in        
 
         &gt; executeInstruction(), if the offset is not a constantexpr         
and the 
         &gt; geptype has <ArrayType&gt;, I append two constraints         that 
x &gt;=0 and x < 
         &gt; sizeof(b).So that the symbolic value x will not be out of         
bound.This 
         &gt; can solve the problem of array,but I do not know how to fix       
  pointer.
         &gt; If the pointer is allocates memory by a sized array(int *p        
 = b),I hope 
         &gt; that the offset should be restricted from 0 to the size of        
 the array, 
         &gt; but when I fix with the gep instruction(p[x]),I cannot get        
 the size of 
         &gt; the array.I only know the pointer type and the size of the        
 type from 
         &gt; the gep instruction.How can I do it?
         &gt; My English is not so good, sorry
         &gt;
         &gt; _______________________________________________
         &gt; klee-dev mailing list
         &gt; klee-dev@imperial.ac.uk
         &gt; 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

Reply via email to