[klee-dev] failed external call
Hello everyone,
I am trying to use the taint analysis from the following project:
http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto/ . They have a KLEE program
that is doing taint analysis, it is in the examples folder.
I receive the following KLEE error : *failed external call:
klee_set_pc_taint*. In my entire KLEE root folder, klee_set_pc_taint
appears only in their .c program:
*#define TEST(x) { printf(testing #x \n); klee_set_pc_taint(0);
test_##x(); }*
by using the linux command grep -r klee_set_pc_taint *
So it is defined only there (not appearing in any header file).
My question is : klee_set_pc_taint is
*1.* their own definition, only in the .c file and it is a problem with the
project program
*2.* It should be defined in the *klee/Release+Asserts/lib* folder, where I
had another problem. I was able to install KLEE, but when I was trying to
run the taint analysis example, it failed requiring for *
klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca* , which was not in
the folder. So I renamed the libkleeRuntimeIntrinsic.a file to
libkleeRuntimeIntrinsic.bca and the problem was apparently removed. Maybe
this has any link with their own defined klee_set_pc_taint ? I suppose I
set up good the PATH with llvm-gcc, since I had no problems with building.
Thank for your any advice !
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] failed external call
Hi,
If you search the PATCH OF KLEE
http://keeda.stanford.edu/pipermail/klee-dev/attachments/20121007/6b3c595b/attachment-0001.obj
for:
add(klee_set_taint
...you will see that it is handled in
klee/lib/Core/SpecialFunctionHandler.cpp.
Thanks,
Paul
On 1 May 2013 12:51, Alexandru Ionut Diaconescu
alexandruionutdiacone...@gmail.com wrote:
Hello everyone,
I am trying to use the taint analysis from the following project:
http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto/ . They have a KLEE program
that is doing taint analysis, it is in the examples folder.
I receive the following KLEE error : failed external call:
klee_set_pc_taint. In my entire KLEE root folder, klee_set_pc_taint
appears only in their .c program:
#define TEST(x) { printf(testing #x \n); klee_set_pc_taint(0);
test_##x(); }
by using the linux command grep -r klee_set_pc_taint *
So it is defined only there (not appearing in any header file).
My question is : klee_set_pc_taint is
1. their own definition, only in the .c file and it is a problem with the
project program
2. It should be defined in the klee/Release+Asserts/lib folder, where I had
another problem. I was able to install KLEE, but when I was trying to run
the taint analysis example, it failed requiring for
klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca , which was not in the
folder. So I renamed the libkleeRuntimeIntrinsic.a file to
libkleeRuntimeIntrinsic.bca and the problem was apparently removed. Maybe
this has any link with their own defined klee_set_pc_taint ? I suppose I set
up good the PATH with llvm-gcc, since I had no problems with building.
Thank for your any advice !
___
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
Re: [klee-dev] failed external call
I was trying again to use wget and patch but it seems it doesn't work. I will look for the warnings received during installation. Sorry for the beginner questions, I will try to solve it. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] failed external call
I'm not sure your patch is applying cleanly there but the bigger problem is that the configure step can't find the STP header file hence nothing can be built. Take a look at config.log (generated when running configure in the KLEE directory) for hints about what went wrong but it looks like configure had trouble with your STP installation (STP is the constraint solver KLEE uses and it is separate from KLEE). Given that you've got this far it is probably better to try to do the rest by hand instead of rerunning the installation script. 1. Check STP built and installed correctly (if you run make again, make sure you use the arguments used in the script - with the variables expanded of course) 2. Reperform the configure command for KLEE 3. If the above succeeds you should be able to build KLEE. I glanced at the patch for KLEE and it doesn't look like it changes any part of the build system so you could actually build KLEE first apply the patch and then build again to be sure that the patch did not break the build. On 1 May 2013 14:46, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: I started to apply the installation script from the beginning. And KLEE is not installing anymore, having : patching file lib/Module/KModule.cpp patching file tools/klee/main.cpp patch unexpectedly ends in middle of line Hunk #3 succeeded at 1314 with fuzz 1. checking build system type... i686-pc-linux-gnu checking host system type... i686-pc-linux-gnu ... configure: error: Unable to use stp/c_interface.h header Makefile:15: Makefile.config: No such file or directory Makefile.common:3: Makefile.config: No such file or directory Makefile.common:6: /Makefile.config: No such file or directory Makefile.common:21: /Makefile.rules: No such file or directory make: *** No rule to make target `/Makefile.rules'. Stop. /home/pc/Desktop/llvm/NEWKLEE run . ./setenv.sh for setting up the environment Done. Try: cd klee/examples/taint make In the script from http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto/ , all the steps from installing KLEE seem to be respected... On Wed, May 1, 2013 at 2:49 PM, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: -- Forwarded message -- From: Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com Date: Wed, May 1, 2013 at 2:48 PM Subject: Re: [klee-dev] failed external call To: Daniel Liew daniel.l...@imperial.ac.uk Yes, I saw in the script the patch usage and I didn't received any error during running their script. And still, I have the original KLEE files, their patch being not applied.. On Wed, May 1, 2013 at 2:46 PM, Daniel Liew daniel.l...@imperial.ac.uk wrote: You can apply the patch as follows $ cd klee_root # this is where the include/, lib/ and other folders are $ patch -p1 the_patch_to_apply.patch If you're using git you can also use $ git apply the_patch_to_apply.patch I've not tried actually applying the patch so I can't tell you if it will apply cleanly. On 1 May 2013 13:42, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: I was trying again to use wget and patch but it seems it doesn't work. I will look for the warnings received during installation. Sorry for the beginner questions, I will try to solve it. -- Best regards, Alexandru Ionut Diaconescu -- Best regards, Alexandru Ionut Diaconescu -- Best regards, Alexandru Ionut Diaconescu ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] failed external call
Yes, that's why I was afraid for, the patch breaking the build. thank you a lot for the detailed information ! I will try and hope it works On Wed, May 1, 2013 at 4:05 PM, Daniel Liew daniel.l...@imperial.ac.ukwrote: I'm not sure your patch is applying cleanly there but the bigger problem is that the configure step can't find the STP header file hence nothing can be built. Take a look at config.log (generated when running configure in the KLEE directory) for hints about what went wrong but it looks like configure had trouble with your STP installation (STP is the constraint solver KLEE uses and it is separate from KLEE). Given that you've got this far it is probably better to try to do the rest by hand instead of rerunning the installation script. 1. Check STP built and installed correctly (if you run make again, make sure you use the arguments used in the script - with the variables expanded of course) 2. Reperform the configure command for KLEE 3. If the above succeeds you should be able to build KLEE. I glanced at the patch for KLEE and it doesn't look like it changes any part of the build system so you could actually build KLEE first apply the patch and then build again to be sure that the patch did not break the build. On 1 May 2013 14:46, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: I started to apply the installation script from the beginning. And KLEE is not installing anymore, having : patching file lib/Module/KModule.cpp patching file tools/klee/main.cpp patch unexpectedly ends in middle of line Hunk #3 succeeded at 1314 with fuzz 1. checking build system type... i686-pc-linux-gnu checking host system type... i686-pc-linux-gnu ... configure: error: Unable to use stp/c_interface.h header Makefile:15: Makefile.config: No such file or directory Makefile.common:3: Makefile.config: No such file or directory Makefile.common:6: /Makefile.config: No such file or directory Makefile.common:21: /Makefile.rules: No such file or directory make: *** No rule to make target `/Makefile.rules'. Stop. /home/pc/Desktop/llvm/NEWKLEE run . ./setenv.sh for setting up the environment Done. Try: cd klee/examples/taint make In the script from http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto/ , all the steps from installing KLEE seem to be respected... On Wed, May 1, 2013 at 2:49 PM, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: -- Forwarded message -- From: Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com Date: Wed, May 1, 2013 at 2:48 PM Subject: Re: [klee-dev] failed external call To: Daniel Liew daniel.l...@imperial.ac.uk Yes, I saw in the script the patch usage and I didn't received any error during running their script. And still, I have the original KLEE files, their patch being not applied.. On Wed, May 1, 2013 at 2:46 PM, Daniel Liew daniel.l...@imperial.ac.uk wrote: You can apply the patch as follows $ cd klee_root # this is where the include/, lib/ and other folders are $ patch -p1 the_patch_to_apply.patch If you're using git you can also use $ git apply the_patch_to_apply.patch I've not tried actually applying the patch so I can't tell you if it will apply cleanly. On 1 May 2013 13:42, Alexandru Ionut Diaconescu alexandruionutdiacone...@gmail.com wrote: I was trying again to use wget and patch but it seems it doesn't work. I will look for the warnings received during installation. Sorry for the beginner questions, I will try to solve it. -- Best regards, Alexandru Ionut Diaconescu -- Best regards, Alexandru Ionut Diaconescu -- Best regards, Alexandru Ionut Diaconescu -- Best regards, Alexandru Ionut Diaconescu ___ 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
