Re: [klee-dev] Need help in understanding a kquery generated by KLEE

2022-06-16 Thread Cristian Cadar 

Hi Sandip,

Those constants are most likely derived from concrete addresses, but you 
should try to simplify the program as much as possible and send a full 
program that can be compiled and run.


Best,
Cristian

On 02/05/2022 19:22, Sandip Ghosal wrote:

Hello,

I need help in understanding a kquery file generated by KLEE.

Consider the following C program:

void* foo(struct node *item1. struct node *item2){
          if(item1 == item2){
              item1->next = NULL;
          }
          return item1;
}

void main(){
       struct list *array[3];
       // next allocate memory for each array[I], i=0,1,2
      int item1 = klee_range(0, 3, "item1");
      int item2 = klee_range(0, 3, "item2");
      foo(array[item1], array[item2]);
}

Since my main objective is to understand the query, the above program is 
simplified and loosely written for reference. Now KLEE generates one 
kquery as follows:


array const_arr1[24] : w32 -> w8 = [32 77 0 133 168 85 0 0 240 68 0 133 
168 85 0 0 0 77 0 133 168 85 0 0]

array item1[4] : w32 -> w8 = symbolic
array item2[4] : w32 -> w8 = symbolic

(query [(Ult N0:(ReadLSB w32 0 item1)
               3)

          (Ult N1:(ReadLSB w32 0 item2)
               3)

          (Eq N2:(ReadLSB w64 N3:(Extract w32 0 (Mul w64 8 (SExt w64 
N0))) const_arr1)
              (ReadLSB w64 N4:(Extract w32 0 (Mul w64 8 (SExt w64 N1))) 
const_arr1))


          (Eq false
              (Ult (Add w64 18446649891435295456 N2) 9))

          (Ult (Add w64 18446649891435295488 N2) 9)]
         false)

I am struggling to understand the second and third last line of the 
query which seems to be performing a boundary check on a flat byte 
memory address. I understand KLEE is implicitly branching over the 
statement  item1->next = NULL, 18446649891435295456 perhaps is the base 
address for item1, and N2 computes the offset. However, I am failing to 
understand how the base address is computed and why it is always 
compared with a constant value of 9?


Thanks in advance.

--
Thanks & Regards
Sandip Ghosal




___
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] Need help in understanding a kquery generated by KLEE

2022-05-02 Thread Sandip Ghosal 
Hello,

I need help in understanding a kquery file generated by KLEE.

Consider the following C program:

void* foo(struct node *item1. struct node *item2){
 if(item1 == item2){
 item1->next = NULL;
 }
 return item1;
}

void main(){
  struct list *array[3];
  // next allocate memory for each array[I], i=0,1,2
 int item1 = klee_range(0, 3, "item1");
 int item2 = klee_range(0, 3, "item2");
 foo(array[item1], array[item2]);
}

Since my main objective is to understand the query, the above program is
simplified and loosely written for reference. Now KLEE generates one
kquery as follows:

array const_arr1[24] : w32 -> w8 = [32 77 0 133 168 85 0 0 240 68 0 133 168
85 0 0 0 77 0 133 168 85 0 0]
array item1[4] : w32 -> w8 = symbolic
array item2[4] : w32 -> w8 = symbolic

(query [(Ult N0:(ReadLSB w32 0 item1)
  3)

 (Ult N1:(ReadLSB w32 0 item2)
  3)

 (Eq N2:(ReadLSB w64 N3:(Extract w32 0 (Mul w64 8 (SExt w64 N0)))
const_arr1)
 (ReadLSB w64 N4:(Extract w32 0 (Mul w64 8 (SExt w64 N1)))
const_arr1))

 (Eq false
 (Ult (Add w64 18446649891435295456 N2) 9))

 (Ult (Add w64 18446649891435295488 N2) 9)]
false)

I am struggling to understand the second and third last line of the query
which seems to be performing a boundary check on a flat byte memory
address. I understand KLEE is implicitly branching over the statement
item1->next = NULL, 18446649891435295456 perhaps is the base address for
item1, and N2 computes the offset. However, I am failing to understand how
the base address is computed and why it is always compared with a constant
value of 9?

Thanks in advance.

-- 
Thanks & Regards
Sandip Ghosal
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev