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
