Re: [klee-dev] How to show (get) the negative values returned in klee's .pc files?
Hi,
When sending replies please CC the mailing list.
klee_assume() is a special function that adds constraints to the
current path being explored (if the resulting path is possible). See
SpecialFunctionHandler::handleAssume() in SpecialFunctionHandler.cpp
SpecialFunctionHandler::handleAssume() receives std::vectorrefExpr
arguments as one of its arguments which will be an expression tree
describing the constraint that was passed into klee_assume().
klee_assert() is a macro defined in klee.h that will call the special
function __assert_fail() if the assertion is false. This special
function is handled by SpecialFunctionHandler::handleAssertFail() this
will terminate the path currently being explored.
On 1 May 2013 20:29, General Email general_mail2...@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(y0);
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.l...@imperial.ac.uk
To: General Email general_mail2...@yahoo.com
Cc: klee-dev klee-dev@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_mail2...@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(y0);
}
--
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] How to show (get) the negative values returned in klee's .pc files?
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(y0);
}
--
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to show (get) the negative values returned in klee's .pc files?
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(y0);
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.l...@imperial.ac.uk
To: General Email general_mail2...@yahoo.com
Cc: klee-dev klee-dev@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_mail2...@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(y0);
}
--
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
