[klee-dev] How to show (get) the negative values returned in klee's .pc files?

[General Email]

Thanks Daniel,

This is very helpful.
So, my next question is how does klee generate such a condition based on the following set of commands?!

klee_assume(!(0<(x+5)));
klee_assume(y==x+7);
klee_assert(y<0);

I would appreciate if you provide me with some guidance of how klee_assume and klee_assert work.

Again thank you so much for your help.

________________________________
 From: Daniel Liew <daniel.liew at imperial.ac.uk>
To: General Email <general_mail2011 at yahoo.com> 
Cc: klee-dev <klee-dev at imperial.ac.uk> 
Sent: Wednesday, May 1, 2013 1:01 PM
Subject: Re: [klee-dev] How to show (get) the negative values returned in klee's .pc files?
 

The path constraint is in the KQuery language ( see
http://klee.llvm.org/KQuery.html#ReadLSB_expr ). The stuff in the
square brackets are the constraints which can be understood to mean

2880154532 == (array X concatenated together). X was simply an integer
in your case so this concatenation is just concatenating 4bytes
together the integer.

Decimal constants (such as 2880154532 ) used in this way as far as I
know represent the unsigned interpretation of a bitvector.

Assuming that a two-complement representation for signed integers you
can use gdb to quickly calculate what the decimal representation of
the signed integer x is.

$ gdb
(gdb) print /t 2880154532
$1 = 10101011101010111010101110100100
# The most significant bit is 1 so we know the number is negative. We
can invert the bits and add 1 to find the absolute value (
 see
http://en.wikipedia.org/wiki/Two%27s_complement#The_most_negative_number
)
(gdb) print ~(2880154532) + 1
$2 = 1414812764
(gdb) exit

So this tells you that the decimal value of integer x is -1414812764
in the constraints you showed.

Hope that helps.

On 1 May 2013 17:16, General Email <general_mail2011 at yahoo.com> wrote:
> Hi,
>
> I need to understand how to use klee_assume and klee_assert.
> I tried to implement the following assumptions (in the function listed
> below) which assumed that if a symbolic variable x satisfies the condition
> !(0<(x+5)) and that if another variable y is set to x+7, I want to check
> whether y is < 0 or not.
> ------------------------------------------------------------------
> void main()
> {
>   int
 x,y;
>   klee_make_symbolic(&x, sizeof(x), "x");
>
>   klee_assume(!(0<(x+5)));
>   klee_assume(y==x+7);
>   klee_assert(y<0);
> }
> ------------------------------------------------------------------
> The result from klee showed that the assersion is satisfiable based on the
> following path constraint which I couldn't understand.
>
> array x[4] : w32 -> w8 = symbolic
> (query [(Eq 2880154532
>             (ReadLSB w32 0 x))]
>        false)
>
> Also how to get the equivelant negative value of the number 2880154532?
>
> Would you please advise?
> Thanks
-------------- next part --------------
HTML attachment scrubbed and removed