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

[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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev