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

[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
-------------- next part --------------
HTML attachment scrubbed and removed