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

[David Ramos]

One observation: the code snippet you provided doesn't create a symbolic value for y. For determinism/reproducibility, KLEE sets uninitialized variables (e.g., y) to "0xabab..." which I think explains those constraints (2880154532 = 0xabababa4).

On May 1, 2013, at 2:07 PM, General Email <general_mail2011 at yahoo.com> wrote:

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

-------------- next part --------------
HTML attachment scrubbed and removed