Re: [klee-dev] Windows support

[Cadar, Cristian]

I don't see any fundamental reason for the core of KLEE not to work 
under Windows -- this being said, we've never tried it so I suspect 
there will be some engineering effort needed to make it work (or even 
compile).  However, uclibc and the POSIX runtime won't work.

If you give it a try, let us know.

Best,
Cristian

On 05/03/2020 14:43, Mikhail Oskin wrote:
> Thanks for the reply!
> I've seen the page, I'm just interested if there any particular reason for 
> that? Is it worth trying to install it on windows (not in WSL / docker) or it 
> won't work anyway due to some internal incompatibility?
> 
> -Original Message-
> From: klee-dev-boun...@imperial.ac.uk 
> [mailto:klee-dev-boun...@imperial.ac.uk] On Behalf Of Cadar, Cristian
> Sent: Thursday, March 5, 2020 5:36 PM
> To: klee-dev 
> Subject: Re: [klee-dev] Windows support
> 
> Hi Mikhail,
> 
> No, KLEE does not have support for Windows.  Only for Linux and
> (partially) for macOS, see https://klee.github.io/build-llvm60/
> 
> Cristian
> 
> On 05/03/2020 07:38, Mikhail Oskin wrote:
>> Dear KLEE developers,
>>
>> I would like to evaluate KLEE for its feasibility in our research. Is
>> there any significant challenges installing it on windows or just
>> windows setup wasn’t targeted and thoroughly tested?
>>
>> Thanks!
>>
>> --
>> --
>>
>> Best regards,
>>
>> Mikhail Oskin
>>
>> Engineer at Russian Research Institute
>>
>> Huawei Technologies Co., Ltd [Russia]
>>
>> cid:image009.jpg@01D4B4C0.6BB34BE0
>>
>>
>> ___
>> 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
> 
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Windows support

[Cadar, Cristian]

Hi Mikhail,

No, KLEE does not have support for Windows.  Only for Linux and 
(partially) for macOS, see https://klee.github.io/build-llvm60/

Cristian

On 05/03/2020 07:38, Mikhail Oskin wrote:
> Dear KLEE developers,
> 
> I would like to evaluate KLEE for its feasibility in our research. Is 
> there any significant challenges installing it on windows or just 
> windows setup wasn’t targeted and thoroughly tested?
> 
> Thanks!
> 
> 
> 
> Best regards,
> 
> Mikhail Oskin
> 
> Engineer at Russian Research Institute
> 
> Huawei Technologies Co., Ltd [Russia]
> 
> cid:image009.jpg@01D4B4C0.6BB34BE0
> 
> 
> ___
> 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

[klee-dev] KLEE 2.1

[Cadar, Cristian]

Hi all,

I'm happy to announce a new release of KLEE, 2.1.  It has a number of 
new features, including better management and visualisation of 
statistics, better implementation of timers and reference handling, 
support for recent LLVM versions, as well as a better KLEE Web 
architecture (http://klee.doc.ic.ac.uk/).

Big thanks to everyone who contributed to this release, and in 
particular to KLEE's co-maintainer @MartinNowack and @251, @andronat, 
@arrowd, @Denis-Gavrielov, @domainexpert, @gdish, @jbuening, 
@KennyMacheka, and @kren1.

More details on this release are at:
https://github.com/klee/klee/releases/tag/v2.1

Best,
Cristian
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] 2nd International KLEE Workshop on Symbolic Execution

[Cadar, Cristian]

Dear all,

I am excited to announce the 2nd International KLEE Workshop on Symbolic
Execution, which will take place on 14-15 September 2020 at Imperial
College London:
https://srg.doc.ic.ac.uk/klee20/

The goal of the workshop is to bring together symbolic execution
researchers, KLEE users and KLEE developers to exchange ideas, find out
about new research in the field, understand each other’s interests and
needs, discuss the evolution of KLEE, and more.

The first edition of the workshop (https://srg.doc.ic.ac.uk/klee18/) was
really great, with a fantastic set of presentations from both academia
and industry and excellent discussions on KLEE, symbolic execution and
related topics.

I hope you'll make the second edition of the workshop equally successful
by responding to the call for presentations, with a deadline of 8 May:
https://srg.doc.ic.ac.uk/klee20/cfpresentations.html

We will also be making regular announcements about the workshop via
@kleesymex on Twitter (the tweets are also available on the workshop
webpage).

Finally, but importantly to keep registration costs low, if your company
would like to sponsor the workshop, please get in touch!

Best,
Cristian and the KLEE 2020 Organising Team
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Error while replaying .path file

[Cadar, Cristian]

Hi Awanish,

Unfortunately that feature has not been maintained -- we need to fix it, 
but there are no immediate plans to do so.

You may be able to achieve something similar via seeding (-seed-file). 
Or if you just want to replay the test case, use klee-replay or link 
with the libkleeRuntest library (see the tutorials).

Best,
Cristian

On 18/02/2020 07:47, Awanish Pandey wrote:
> Dear all,
> I want to replay a path file, but I am getting an assertion 
> violation "hit an invalid branch in replay path mode".
> 
> This is my toy program
> /int main(int argc, char *argv[]){
>    if (argc != 2){
>      printf("error:");
>    }
>    int a;
>    FILE *fp = fopen(argv[1], "r");
>    fscanf(fp,"%d",&a);
>    if (a == 10)
>      assert(0);
>    fclose(fp);
>    return 0;
> }/
> 
> I run klee "/klee --libc=uclibc --posix-runtime --write-paths file.bc 
> --sym-arg 1  --sym-files 1 5/".
> It finds an assertion violation (at test case number 19) and when I 
> replayed it by command
> /klee --libc=uclibc --posix-runtime 
> --replay-path=klee-out-0/test19.path file.bc/
> 
> Klee crashes on assertion violation in Executor.cpp
> 
> What is the issue? It will be very helpful.
> -- 
> Thanking You
> Awanish Pandey
> 
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] What formats does the option "-link-llvm-lib" supports?

[Cadar, Cristian]

Hi, I was checking messages on the list, and noticed that this message 
never received a reply.  Martin has recently improved the documentation 
for -link-llvm-lib (https://github.com/klee/klee/pull/1204) so hopefully 
things are more clear now.

Best,
Cristian

On 14/11/2019 15:42, Ling Jin wrote:
> Hi,
> 
> I got confused about the documentation describing Linking External 
> Libraries. In the documentation, it says
> 
> If some functions in the input file are defined in an external LLVM
> IR file, an archive (.a) of LLVM IR files, or a shared object with
> LLVM IR code, these external files can be linked in using the option
> -link-llvm-lib=LIB_FILENAME.
> 
> What I understand is that I can give a ".so" file, but the example
> 
> $ klee -link-llvm-lib=libhelper.so.bc test.bc
> 
> shows that the option needs a ".so.bc" file. So I want to ask what 
> formats does the option "-link-llvm-lib" supports?
> 
> Does it mean that I can give ".ll", ".a" and/or ".so" files? But the 
> ".a" file should be an archieve of ".bc" files instead of ".obj" files?
> 
> 
> Thanks,
> Ling Jin
> 
> ___
> 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] error while installing klee

[Cadar, Cristian]

LLVM_CONFIG_BINARY should be the full path to llvm-config.

Best,
Cristian

On 04/11/2019 18:29, Cedric Lontsi wrote:
> Hi,
> I'm new in klee and i installed klee with llvm6.0. i followed the 
> different step in this article https://klee.github.io/build-llvm60/  
> until step 9 where i used the command
> 
> |*cmake   *and i had this error: |
> 
> *-- LLVM_CONFIG_BINARY: /usr/lib/llvm-6.0/bin*
> *CMake Error at cmake/find_llvm.cmake:67 (message):
>    Failed running /usr/lib/llvm-6.0/bin;--version
> Call Stack (most recent call first):
>    cmake/find_llvm.cmake:73 (_run_llvm_config)
> *
> *  CMakeLists.txt:208 (include)*
> *
> *
> In attached, you have a snapshot of the execution of the command.
> please, how can i solve this problem?
> best regards.
> 
> ___
> 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] libc function "open" is defined in POSIX runtime

[Cadar, Cristian]

Hi Gleb,

We applied various changes to uclibc to make it work with KLEE, so I 
think taking a look at those patches would help.  I don't recall the 
details, but based on a quick search, I think this patch might be 
relevant: 
https://github.com/klee/klee-uclibc/commit/7231f48dd8e2f9f15f721a77639d7eeea6efd38f

This PR from Martin might also be useful:
https://github.com/klee/klee/pull/483
Look in particular at linkWithMusllibc()

I would welcome changes to KLEE to make it easier to plug in other libc 
implementations.

Best,
Cristian

On 26/10/2019 18:50, Gleb Popov wrote:
> Hello.
> 
> I'm trying to make KLEE support FreeBSD libc instead of uclibc. When I 
> run KLEE with my libc.bca, I get the following error:
> 
> error: Linking globals named 'open': symbol multiply defined!
> 
> It turned out that POSIX runtime contains definition of "open" function, 
> as well as FreeBSD libc do. How to handle this properly?
> 
> ___
> 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] questions about klee-array

[Cadar, Cristian]

Hi Qiao,

In your example, the number of paths depends exponentially on N.

As a side note, please include self-contained C programs, not 
pseudocode.  This avoids misunderstandings and also makes it easy for 
everyone to quickly run the code.

Best,
Cristian

On 04/09/2019 16:57, Qiao Kang wrote:
> Hi Cristian,
> 
> Thanks for the reply, very helpful!! I did use klee_assume to specify 
> the range of the symbolic index.
> 
> I also found that the more read/write operations I perform to the array, 
> the time also grows very fast.
> 
> For instance, in this example I run the loop N times, each iteration has 
> 1 read and 1 write:
> 
> // x[N] and y[N] are symbolic inputs, assumed to be 0~4095
> int a[4096] = {0};
> for (i from 0 to N-1) {
>    a[x[i]] += 1;
>    if (a[y[i]] > 1){
>      // path1
>    } else {
>      // path2
>    }
> }
> 
> Is it fair to say that the constraint complexity grows exponentially with N?
> 
> Thanks,
> Qiao
> 
> 
> On Wed, Sep 4, 2019 at 10:37 AM Cadar, Cristian  <mailto:c.ca...@imperial.ac.uk>> wrote:
> 
> Yes, our array acceleration work is integrated into the mainline (use
> option -optimize-array=all) and on your example it reduces the time on
> my machine from ~80s to only ~4s.  However, there is another issue
> there, which was discussed on the mailing list several times before:
> since the indexes are completely unconstrained, they could refer to any
> other memory object, causing a lot of unnecessary forking.  If you
> constrain the indexes to be in-bounds (klee_assume(x >= 0);
> klee_assume(x < 4096); same for y), KLEE should be much faster, even
> without the array optimization.
> 
> Cristian
> 
> On 04/09/2019 02:01, Qiao Kang wrote:
>  > Hi all,
>  >
>  > When I run klee, I found it is quite slow to resolve array
> constraints
>  > if the array size is large.
>  >
>  > For instance (x, y are both symbolic variables):
>  >
>  > int a[4096] = {0};
>  > a[x] = 1;
>  > if (a[y] > 0){
>  >    // path1
>  > } else {
>  >    // path2
>  > }
>  >
>  > It takes serveral seconds to finish, and the time scales with the
> size
>  > of the array.
>  >
>  > Then I found a paper "Accelerating Array Constraints in Symbolic
>  > Execution" - ISSTA 2017, and seems that this paper aims at
> address this
>  > problem.
>  >
>  > I'm quite interested in reproducing the results of this paper, but I
>  > cannot build klee-array from source, because it relies on LLVM
> 3.4 and
>  > it is not available from ubuntu software repos.
>  >
>  > I'm downloading the vm image (ova file) but it is very slow (200K/s).
>  >
>  > My questions are:
>  > 1) Is the poor performance I have observed expected?
>  > 2) Is klee-array integrated in the klee mainstream?
>  > 3) If not, how can I build klee-array from source which relies on
>  > earlier version of LLVM?
>  > 4) Can I download the ova from other sources like google drive?
>  >
>  > Thank you very much,
>  > Qiao
>  >
>  > ___
>  > klee-dev mailing list
>  > klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
>  > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>  >
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk <mailto: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] questions about klee-array

[Cadar, Cristian]

Yes, our array acceleration work is integrated into the mainline (use 
option -optimize-array=all) and on your example it reduces the time on 
my machine from ~80s to only ~4s.  However, there is another issue 
there, which was discussed on the mailing list several times before: 
since the indexes are completely unconstrained, they could refer to any 
other memory object, causing a lot of unnecessary forking.  If you 
constrain the indexes to be in-bounds (klee_assume(x >= 0); 
klee_assume(x < 4096); same for y), KLEE should be much faster, even 
without the array optimization.

Cristian

On 04/09/2019 02:01, Qiao Kang wrote:
> Hi all,
> 
> When I run klee, I found it is quite slow to resolve array constraints 
> if the array size is large.
> 
> For instance (x, y are both symbolic variables):
> 
> int a[4096] = {0};
> a[x] = 1;
> if (a[y] > 0){
>    // path1
> } else {
>    // path2
> }
> 
> It takes serveral seconds to finish, and the time scales with the size 
> of the array.
> 
> Then I found a paper "Accelerating Array Constraints in Symbolic 
> Execution" - ISSTA 2017, and seems that this paper aims at address this 
> problem.
> 
> I'm quite interested in reproducing the results of this paper, but I 
> cannot build klee-array from source, because it relies on LLVM 3.4 and 
> it is not available from ubuntu software repos.
> 
> I'm downloading the vm image (ova file) but it is very slow (200K/s).
> 
> My questions are:
> 1) Is the poor performance I have observed expected?
> 2) Is klee-array integrated in the klee mainstream?
> 3) If not, how can I build klee-array from source which relies on 
> earlier version of LLVM?
> 4) Can I download the ova from other sources like google drive?
> 
> Thank you very much,
> Qiao
> 
> ___
> 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] build klee-uclibc failed

[Cadar, Cristian]

It looks to me like klee-uclibc was not built correctly.

BTW, if you run into many issues building KLEE, I recommend to use the 
provided Docker containers instead:
https://klee.github.io/docker/

Best,
Cristian

On 19/08/2019 06:40, Zhang, RongX Z wrote:
> Thanks Cristian, I do as you said, and rerun configure successfully, but when 
> I cmake KLEE, another error occurs:
> 
>klee-uclibc library not found at "/home/tiano/env/klee-uclibc/lib/libc.a".
> 
> and I cmake Klee with the latest klee-uclibc on Ubuntu which I ever cmake  
> Klee successfully, it is failed, and error log is the same as on Clear Linux.
> 
> 
> Thanks
> Rong
> 
> -Original Message-
> From: klee-dev-boun...@imperial.ac.uk 
> [mailto:klee-dev-boun...@imperial.ac.uk] On Behalf Of Cadar, Cristian
> Sent: Friday, August 16, 2019 6:22 PM
> To: klee-dev 
> Subject: Re: [klee-dev] build klee-uclibc failed
> 
> What seems to happen there is that you have $CC set to /usr/bin/gcc.
> Unset it and rerun configure and hopefully it should work.  I updated the 
> script to add a more informative error message when this happens (patch to be 
> merged soon).
> 
> Cristian
> 
> On 16/08/2019 02:48, Zhang, RongX Z wrote:
>> Yes, I checked  usr/local/bin/llvm-dis  –version, it is 6.0
>>
>> Thanks
>>
>> Rong
>>
>> *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
>> *Sent:* Thursday, August 15, 2019 5:55 PM
>> *To:* Zhang, RongX Z ; klee-dev
>> 
>> *Subject:* RE: [klee-dev] build klee-uclibc failed
>>
>> For most LLVM tools, it should be '-v'. Just to cross check.
>>
>> On 15 August 2019 11:25:34 CEST, "Zhang, RongX Z"
>> mailto:rongx.z.zh...@intel.com>> wrote:
>>
>>  Sorry, how to check this?  /usr/local/bin/llvm* is installed by
>>  myself, and I thinks it’s llvm 6.0.
>>
>>  *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
>>  *Sent:* Thursday, August 15, 2019 5:15 PM
>>  *To:* Zhang, RongX Z >  <mailto:rongx.z.zh...@intel.com>>; klee-dev >  <mailto:klee-dev@imperial.ac.uk>>
>>  *Subject:* RE: [klee-dev] build klee-uclibc failed
>>
>>  Can you check which LLVM version usr/local/bin/llvm-dis uses?
>>
>>  Cheers,
>>  Martin
>>
>>  On 15 August 2019 11:12:02 CEST, "Zhang, RongX Z"
>>  mailto:rongx.z.zh...@intel.com>> wrote:
>>
>>  Yes, clang is in my PATH and clang version is 6.0.0.
>>
>>  Thanks
>>
>>  Rong
>>
>>  *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
>>  *Sent:* Thursday, August 15, 2019 5:10 PM
>>  *To:* Zhang, RongX Z >  <mailto:rongx.z.zh...@intel.com>>; klee-dev
>>  mailto:klee-dev@imperial.ac.uk>>
>>  *Subject:* Re: [klee-dev] build klee-uclibc failed
>>
>>  Dear Rong,
>>  Can you check if clang is in your PATH?
>>  'clang -v' should print out 6.0 as well.
>>
>>  Clang is not necessarily installed as a dependency of LLVM.
>>
>>  Hope that helps.
>>
>>  Best,
>>  Martin
>>
>>  On 15 August 2019 09:26:23 CEST, "Zhang, RongX Z"
>>  mailto:rongx.z.zh...@intel.com>> wrote:
>>
>>  Hi ,
>>
>>  I am installing KLEE on Clear Linux, when I build the latest
>>  klee-uclibc , and run command : ./configure --make-llvm-lib,
>>  it’s failed and error log is:
>>
>>  INFO:Forcing C compiler to be...gcc
>>
>>  INFO:Absolute path to compiler.../usr/bin/gcc
>>
>>  INFO:Disabling assertions
>>
>>  INFO:Configuring for Debug build
>>
>>  INFO:Configuring for LLVM bitcode archive
>>
>>  INFO:Using llvm-config at.../usr/local/bin/llvm-config
>>
>>  INFO:Using llvm tool dir.../usr/local/bin
>>
>>  INFO:Found "/usr/local/bin/llvm-nm".
>>
>>  INFO:Found "/usr/local/bin/llvm-ar".
>>
>>  INFO:Found "/usr/local/bin/llvm-link".
>>
>>  INFO:Found "/usr/local/bin/llvm-objdump".
>>
>>  INFO:Testing LLVM Bitcode compiler.../usr/bin/gcc
>>
>>  INFO:Conversion of LLVM Bitcode to LLVM Assembly failed with
>>  output:
>>
>>  /usr/local/bin/

Re: [klee-dev] Is it possible to use llvm bitcode lines as target for klee evaluation?

[Cadar, Cristian]

There's no such support in mainline KLEE, but you can look at KATCH for 
such an extension (https://srg.doc.ic.ac.uk/publications/13-katch-fse.html).

Cristian

On 16/08/2019 03:35, Arnab Kumar Biswas wrote:
> I have a couple of llvm bitcode lines that I have already identified as 
> possible targets. Is there any way to use them as target for klee 
> evaluation? Basically, I want klee to reach those lines as fast as 
> possible instead of going in different directions or branches. If there 
> is any existing project or paper, kindly let me know.
> 
> 
> 
> 
> Important: This email is confidential and may be privileged. If you are 
> not the intended recipient, please delete it and notify us immediately; 
> you should not copy or use it for any purpose, nor disclose its contents 
> to any other person. Thank you.
> 
> ___
> 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] build klee-uclibc failed

[Cadar, Cristian]

What seems to happen there is that you have $CC set to /usr/bin/gcc. 
Unset it and rerun configure and hopefully it should work.  I updated 
the script to add a more informative error message when this happens 
(patch to be merged soon).

Cristian

On 16/08/2019 02:48, Zhang, RongX Z wrote:
> Yes, I checked  usr/local/bin/llvm-dis  –version, it is 6.0
> 
> Thanks
> 
> Rong
> 
> *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
> *Sent:* Thursday, August 15, 2019 5:55 PM
> *To:* Zhang, RongX Z ; klee-dev 
> 
> *Subject:* RE: [klee-dev] build klee-uclibc failed
> 
> For most LLVM tools, it should be '-v'. Just to cross check.
> 
> On 15 August 2019 11:25:34 CEST, "Zhang, RongX Z" 
> mailto:rongx.z.zh...@intel.com>> wrote:
> 
> Sorry, how to check this?  /usr/local/bin/llvm* is installed by
> myself, and I thinks it’s llvm 6.0.
> 
> *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
> *Sent:* Thursday, August 15, 2019 5:15 PM
> *To:* Zhang, RongX Z  >; klee-dev  >
> *Subject:* RE: [klee-dev] build klee-uclibc failed
> 
> Can you check which LLVM version usr/local/bin/llvm-dis uses?
> 
> Cheers,
> Martin
> 
> On 15 August 2019 11:12:02 CEST, "Zhang, RongX Z"
> mailto:rongx.z.zh...@intel.com>> wrote:
> 
> Yes, clang is in my PATH and clang version is 6.0.0.
> 
> Thanks
> 
> Rong
> 
> *From:* Nowack, Martin [mailto:m.now...@imperial.ac.uk]
> *Sent:* Thursday, August 15, 2019 5:10 PM
> *To:* Zhang, RongX Z  >; klee-dev
> mailto:klee-dev@imperial.ac.uk>>
> *Subject:* Re: [klee-dev] build klee-uclibc failed
> 
> Dear Rong,
> Can you check if clang is in your PATH?
> 'clang -v' should print out 6.0 as well.
> 
> Clang is not necessarily installed as a dependency of LLVM.
> 
> Hope that helps.
> 
> Best,
> Martin
> 
> On 15 August 2019 09:26:23 CEST, "Zhang, RongX Z"
> mailto:rongx.z.zh...@intel.com>> wrote:
> 
> Hi ,
> 
> I am installing KLEE on Clear Linux, when I build the latest
> klee-uclibc , and run command : ./configure --make-llvm-lib,
> it’s failed and error log is:
> 
> INFO:Forcing C compiler to be...gcc
> 
> INFO:Absolute path to compiler.../usr/bin/gcc
> 
> INFO:Disabling assertions
> 
> INFO:Configuring for Debug build
> 
> INFO:Configuring for LLVM bitcode archive
> 
> INFO:Using llvm-config at.../usr/local/bin/llvm-config
> 
> INFO:Using llvm tool dir.../usr/local/bin
> 
> INFO:Found "/usr/local/bin/llvm-nm".
> 
> INFO:Found "/usr/local/bin/llvm-ar".
> 
> INFO:Found "/usr/local/bin/llvm-link".
> 
> INFO:Found "/usr/local/bin/llvm-objdump".
> 
> INFO:Testing LLVM Bitcode compiler.../usr/bin/gcc
> 
> INFO:Conversion of LLVM Bitcode to LLVM Assembly failed with
> output:
> 
> /usr/local/bin/llvm-dis: error: Invalid bitcode signature
> 
> ERROR:LLVM Bitcode compiler does not work.
> 
> Can you tell me how to resolve this problem?
> 
> Gcc version :9.1.1
> 
> llvm version:6.0.
> 
> Thanks
> 
> Rong
> 
> 
> -- 
> Sent from my Android device with K-9 Mail. Please excuse my brevity.
> 
> 
> ___
> 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

[klee-dev] Questions on mailing list

[Cadar, Cristian]

Hi all,

I just wanted to encourage everyone to answer questions on the mailing 
list.  We have a few hundred people on the mailing list, but quite a 
number of questions go unanswered, which makes it harder for new people 
to get started with KLEE.

Thanks,
Cristian
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] identify multiple executions of the same branch instruction

[Cadar, Cristian]

Hi Qiao,

I hope you've solved this by now.  It should be quite easy to get the 
file & line number for the instruction you're interested in (if you 
compiled with debug info), just look at KInstruction::getSourceLocation().

Best,
Cristian

On 27/07/2019 18:40, Qiao Kang wrote:
> Hi,
> 
> I'm hacking KLEE to run a program that has an N-iteration loop and an 
> if-else branch inside the loop. The if-else branch will be hit for 
> multiple times. I'm trying to capture each branch instruction and 
> identify if it is executing this particular if-else branch, i.e., this 
> particular line of code.
> 
> For instance:
> 
> // N is constant
> loop N times:
>     if (cond):
>           // do something, might change cond
>     else
>          // do something else, might change cond
> 
> Along the execution, this if-else branch will be hit multiple times. How 
> do I capture all executions of this branch and identify them that they 
> are all from this if-else branch, but not other code? A simple use case 
> would be to count how many times this if-else branch was hit along the 
> execution.
> 
> I now can hijack all branch instructions 
> in Executor::executeInstruction, it has a switch case called 
> "Instruction::Br". I can also extract the corresponding path constraint 
> (i.e., cond). However, I don't know how to identify which if-else branch 
> they are executing. Note that this cond is subject to change, so I 
> cannot simply use this cond as the key to classfity them. One the other 
> hand, the line of code would be an appropriate key. Can we extract code 
> line information?
> 
> Any advice will be greatly appreciated!
> 
> Thanks,
> Qiao
> 
> 
> ___
> 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] How to parse (and convert) constraint expressions

[Cadar, Cristian]

As a starting point, I would look in the code for Kleaver, which 
incorporates a parser for KQuery expressions.

Best,
Cristian

On 27/07/2019 23:52, Qiao Kang wrote:
> Hi,
> 
> I'm wondering if we can parse a constraint expression in KLEE and 
> potentially convert it to another format. For instance, given this 
> constraint: (Sle 0 (ZExt w32 (Read w8 0 a))). Is there an esay way to 
> parse it (i.e., using existing APIs) and output a string like "a >= 0"? 
> I'm only considering simple linear constraints like this one.
> 
> Thanks,
> Qiao
> 
> ___
> 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] klee_print_expr in SMTLIB2 format

[Cadar, Cristian]

No, but you should be able to accomplish this easily, by changing the 
code in handlePrintExpr() to use the code for printing expressions in 
the SMT-LIBv2 format (ExprSMTLIBPrinter).

Best,
Cristian

On 25/07/2019 12:43, Ramanuj Chouksey wrote:
> Hi,
> How do I convert the symbolic expression printed by klee_print_expr
> into SMTLIB2 format? Is it possible using kleaver?
> 
> Thanking you,
> Ramanuj,
> Research Scholar,
> CSE, IIT Guwahati,
> India.
> 
> ___
> 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] installing klee error

[Cadar, Cristian]

Hi, did you try the Docker container? (https://klee.github.io/docker/) 
That is the recommended way of starting with KLEE.  If not, follow 
closely the instructions at https://klee.github.io/build-llvm60/.  For 
instance, -DLLVM_CONFIG_BINARY should be set to the full path to 
llvm-config-6.0, not the bin/ directory.

Cristian

On 21/05/2019 12:03, Yağmur Köksal wrote:
> I am using Kde Neon and i am new at linux. I am trying the install Klee 
> with llvm 6.0. When i run cmake .. code, i get llvm-config cannot be 
> find error.
> 
> I have tried passing path to config file from /usr/lib/llvm-6.0/bin.
> 
> ~$ DLLVM_CONFIG_BINARY=/usr/lib/llvm-6.0/bin.
> 
> Command worked fine, but when i tried cmake .. again it didn't work.
> 
> ___
> 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] Read/write symbolic state

[Cadar, Cristian]

Hi,

On 04/05/2019 06:31, Kihong Heo wrote:
> Hi list,
> 
> I am very new to KLEE and have some questions.
> I would appreciate if you could answer the followings:
> 
> - Is there a way to read/write intermediate symbolic states of KLEE to files? 
> If not, would it be simple to implement? I would appreciate if you could 
> point out some files to be changed.
There is currently no such mechanism per se (although we have some 
ongoing work in the area), but you could generate a test case and then 
replay it using the seeding functionality.

> - If a value is not defined externally and not observed by KLEE, how does 
> KLEE handle it? It has the same mechanism as the UC-KLEE paper? (lazy 
> constraint)
Mainline KLEE does not have the lazy initialization mechanisms of UC-KLEE.

Best,
Cristian


> Thanks,
> Kihong
> ___
> 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

[klee-dev] Postdoctoral and PhD positions at Imperial College London related to KLEE

[Cadar, Cristian]

Hi all,

I have both postdoctoral and PhD positions at Imperial College London to 
work on topics involving KLEE (as well as other topics).  The research 
will be part of the ERC Consolidator Grant Project "PASS: Program 
Analysis for Safe and Secure Software Evolution" and will focus on 
helping software systems evolve safely and securely.

The application deadline is 16 June.

For more details about these positions, please see:
https://srg.doc.ic.ac.uk/vacancies/postdoc-erc-2019/
and
https://srg.doc.ic.ac.uk/vacancies/phd-erc-2019/

Informal inquiries are encouraged, simply reply (but don't reply-all) to 
this email.

Best,
Cristian
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] KLEE 2.0 released!

[Cadar, Cristian]

Hi all,

I'm excited to let you know that KLEE 2.0 is now available!
It comes with a lot of new features and fixes, such as better C++ 
support, compatibility with the most recent LLVM versions (including 
LLVM 8), integration of CVC4 and Yices 2, better path merging 
functionality, improved support for vector instructions, a new 
categorized help menu and more!

Big thanks to my co-maintainers for this release -- @MartinNowack, 
@AndreaMattavelli and @delcypher -- and to all the 20+ contributors to 
this release, particularly @251, @AndreaMattavelli, @corrodedHash, 
@delcypher,  @futile, @hoangmle, @jbuening, @jirislaby, @kren1 and 
@MartinNowack.

More details on the release are at:
https://github.com/klee/klee/releases/tag/v2.0

Best,
Cristian
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Intrinsic function llvm.fabs.f32 not supported

[Cadar, Cristian]

Hi, this is another intrinsic for which we need to add support, see my 
previous email to the list.  But note that KLEE cannot handle symbolic 
FP operations yet, but there are a couple of extensions that can (see 
https://srg.doc.ic.ac.uk/projects/klee-float/).

Best,
Cristian

On 28/01/2019 14:46, Samuel Hopstock wrote:
> Hello,
> 
> I've been trying to execute a bitcode file generated by McSema [1] and
> Klee fails with "LLVM ERROR: Code generator does not support intrinsic
> function 'llvm.fabs.f32'!". Are floating point operations like fabs not
> implemented yet/completely or is this a different issue (maybe related
> to McSema)?
> 
> Best,
> Samuel
> 
> 
> [1] https://github.com/trailofbits/mcsema
> 
> 
> ___
> 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] Unsupported Intrinsic Function

[Cadar, Cristian]

Thanks for reporting this issue.  We are aware that there are still some 
unsupported intrinsics, and we'd welcome PRs for such issues.

Best,
Cristian

On 30/01/2019 03:40, Ridwan Shariffdeen wrote:
> Hi,
> 
> I encountered the following error when running klee with LibWebp
> 
> LLVM ERROR: Code generator does not support intrinsic function 
> 'llvm.x86.sse2.packuswb.128'!
> 
> Is there any solution for this?
> Appreciate any help in this regard
> 
> Thanks!
> 
> ___
> 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] Which LLVM version?

[Cadar, Cristian]

Hi, we've recently added support for newer LLVM versions (thanks largely 
to Jiri Slaby) and we plan to release a new KLEE version soon 
incorporating those changes.  We encourage people to give newer LLVM 
versions a try, but in some ways support for recent LLVM versions is 
still experimental, as we haven't used them that much.

We plan to update the website soon.

Best,
Cristian

On 19/12/2018 15:23, program...@nurfuerspam.de wrote:
> hey,
> 
> The klee website (http://klee.github.io/) still says that klee should be 
> compiled with LLVM 3.4, and that compiling with 3.8 is experimental. 
> However, the travis configuration 
> (https://github.com/klee/klee/blob/master/.travis.yml) shows that it is 
> being tested with up to LLVM 7.0.
> 
> Is the website outdated, or is travis testing things that are not 
> expected to work? It would be nice to know that it is no longer 
> necessary to use an old version of LLVM.
> 
> Alex
> 
> 
> ___
> 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] Klee See Mode Concretization

[Cadar, Cristian]

Hi, take a look at https://srg.doc.ic.ac.uk/projects/zesti/.  It's based 
on a very old version of KLEE, but the code might still be helpful.

Cristian

On 12/12/2018 08:55, Ridwan Shariffdeen wrote:
> Hi,
> 
> I am running Klee in seed mode using a generated ktest file, in order to 
> capture the symbolic expression for the path given by the ktest file. 
> However in trying to execute klee, when it comes to external calls it 
> needs to pass concretized values instead of the symbolic value. From my 
> understanding, currently, Klee tries to compute a concrete value for the 
> symbolic variable from the path constraints and pass to the external 
> function.
> 
> Since I am using seed mode with pre-defined values, I need to change the 
> way Klee concretize the symbolic value by using the current value given 
> in the ktest file, instead of resolving through path constraints. But, I 
> have no idea how to achieve this.
> 
> Is there a reference I can look into or is this achievable?
> Any help in this regard would be much appreciated.
> 
> Thanks
> Regards
> 
> ___
> 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] Unexpected instructions in instructions.txt

[Cadar, Cristian]

Hi Alberto, if you suspect a bug, you should try to reproduce it with a 
smaller example and report it on GitHub.

Cristian

On 29/10/2018 18:37, Alberto Barbaro wrote:
> Hi all,
> I'm still working on pngpixel ( libpng 1.6.34 ). I was able to compile 
> everything and execute klee as expected. The only weird thing is that if 
> I make klee to create instructions.txt 
> ( -debug-print-instructions=src:file ) in that file I have references 
> to pngrutil.c:3147 that is an error condition that is never encountered 
> during the klee execution. If you checked you would see that instruction 
> prints and error message that is never shown during the klee execution, 
> so I'm sure that the instruction was never executed.
> 
> Do you know why the reference to pngrutil.c:3147 is anyway present in 
> instructions.txt?
> 
> Thanks
> Alberto
> 
> ___
> 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