[klee-dev] KLEE 3.1 released

Hi all, It is my pleasure to announce the release of KLEE 3.1! Big thanks to all the contributors to this version. The full list of changes can be found at https://github.com/klee/klee/releases/tag/v3.1 Best wishes, Cristian ___ klee-dev mailing

[klee-dev] KLEE 2024 -- Keynote speakers announced & early registration deadline coming up

Dear all, It is my pleasure to announce a fantastic list of keynotes -- Tevfik Bultan, Tomasz Kuchta, and Corina Pasareanu -- for the upcoming KLEE'24 workshop: https://srg.doc.ic.ac.uk/klee24/keynotes.html The workshop will be co-located with ICSE'24, and will take place 15-16 April in

Re: [klee-dev] Mapping Path Constraint to the Actual Path in Source Code

Hi, KLEE does not provide this information, although you could add such metadata when adding a new constraint. However, because constraint solving optimisations could combine constraints, obtaining the origin of a constraint might not be possible in the general case. Best, Cristian On

Re: [klee-dev] Different behavior when invoking the "error" function with the argument buffer from heap or stack

Hi Haoxin, It looks to me that you are not passing a null-terminated string to error() in the heap case, and the error reported by KLEE is genuine. Best, Cristian On 24/01/2024 15:53, TU Haoxin wrote: Dear KLEE developers, Hope you are all doing well, and hope this is the right place to

[klee-dev] KLEE'24 workshop late submission deadline this Friday

Dear all, The late (and last) submission deadline for the KLEE'24 workshop is this Friday! We have already accepted a number of interesting presentations and posters in the early submission round, and we are looking forward to more interesting contributions in the second round!

[klee-dev] KLEE 2024: First (visa-safe) submission deadline is TODAY

/cfposters.html Best, Cristian On 27/10/2023 13:23, Cristian Cadar wrote: Hi all, Just a short reminder that there is one week left until the early submission deadline for KLEE 2024!  As I mentioned before, the submission process is very lightweight: an abstract and a link to already published

[klee-dev] KLEE 2024: One week until first (visa-safe) deadline

pages for work in progress. https://srg.doc.ic.ac.uk/klee24/ https://srg.doc.ic.ac.uk/klee24/ Best wishes, Cristian On 13/09/2023 12:57, Cristian Cadar wrote: Dear all, It is my great pleasure to announce the 4th edition of the International KLEE Workshop on Symbolic Execution, KLEE 2024

[klee-dev] Announcing KLEE 2024: 4th International KLEE Workshop on Symbolic Execution, April 2024 in Lisbon

Dear all, It is my great pleasure to announce the 4th edition of the International KLEE Workshop on Symbolic Execution, KLEE 2024! KLEE 2024 will take place in April in Lisbon, Portugal, co-located with ICSE 2024, the flagship software engineering conference:

Re: [klee-dev] Why is ConstraintSet not a set?

Hi, KLEE does not add duplicate constraints, in fact it does not add a constraint if it is implied by the current PC. Best, Cristian On 07/07/2023 06:57, Nguyễn Gia Phong wrote: Hi, I notice that ConstraintSet is implemented via std::vector. This make me wonder about the likelihood of

[klee-dev] KLEE 3.0 is released!

Hi all, KLEE 3.0 is released! KLEE now has a purposely-designed deterministic memory allocator (KDAlloc), improved detection of use-after-free errors, ability to handle UBSan checks, support for concrete inline assembly, better statistics, compatibility with newer LLVM versions & more! Big

Re: [klee-dev] Getting symbolic expressions from the symbolic store with `klee_print_expr`

Hi Ferhat, Essentially, you want something like this: printer.printExpression(arguments[1], ExprSMTLIBPrinter::SORT_BITVECTOR); To do this right requires a bit more work, but as a quick proof of concept, just change the visibility of this method. Best, Cristian On 03/04/2023 01:39, Ferhat

Re: [klee-dev] General question

Hi both, Let me answer this as part of the more detailed email Ferhat sent today. But more generally, you can use Kleaver to load queries in KQuery format and print them to SMT-LIB2 format: kleaver --print-smtlib file.kquery Best, Cristian On 30/03/2023 21:57, Ferhat Erata wrote: Hi Teja,

Re: [klee-dev] About external shared libraries

Hi Ziqi, There is no such feature in KLEE currently. If this is something you'd like to contribute, we'd be happy to discuss your proposal in more detail. Best, Cristian On 25/02/2023 03:29, Ziqi Shuai wrote: Hi all, I'm trying to use KLEE to analyze some real-world programs such as image

Re: [klee-dev] Debugging options

On 22/12/2022 16:09, Muralee, Siddharth wrote: Hello, I am currently working on a project to verify states that end due to errors such as "memory error: out of bound pointer". Currently, I am trying to extract some information about these states, and the most information I am able to extract

Re: [klee-dev] On how the standard library is linked.

Hi Alex, We typically link against a custom version of uclibc, where printf is treated specially by default as an external function. Does this answer your question? It is possible to load binary-only libraries with KLEE via the --load option. Best, Cristian On 03/11/2022 14:28, Alex

Re: [klee-dev] Use KLEE with JAVA and C#

Hi Piyush, The short answer is no. More precisely, KLEE runs on LLVM bitcode, so you need an LLVM frontend for the language. Each language also needs some additional support to work with KLEE. Best, Cristian On 26/08/2022 02:09, Piyush Jha wrote: Hi everyone, I'm looking for a tool for

Re: [klee-dev] Running KLEE on Linux

Hi Faysal, You should contact the authors of those papers for more details, they might not be subscribed to this list. Best, Cristian On 12/09/2022 08:46, Faysal Hossain Shezan wrote: I saw your post: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03057.html

[klee-dev] KLEE 2022 Workshop: Free online registration now available & in-person registration still open

Hi all, We have opened today the online registration for the KLEE'22 workshop, which is free for everyone! (but we might need to restrict the number of places) In-person registration is still available until 1st September; if you can make it to London, in-person participation is the best

Re: [klee-dev] Deadline moved to THURSDAY for presentation and poster proposals to the next KLEE Workshop

, Cristian Cadar wrote: Hi all, Just a reminder that the deadline for presentation and poster proposals to the next KLEE Workshop is today, 12th July. Best, Cristian On 11/06/2022 22:55, Cristian Cadar wrote: Hi all, The submission site for the 3rd KLEE Workshop is now OPEN!  The deadline

[klee-dev] Deadline TODAY for presentation and poster proposals to the next KLEE Workshop

Hi all, Just a reminder that the deadline for presentation and poster proposals to the next KLEE Workshop is today, 12th July. Best, Cristian On 11/06/2022 22:55, Cristian Cadar wrote: Hi all, The submission site for the 3rd KLEE Workshop is now OPEN!  The deadline is in about one month

Re: [klee-dev] Working with fixed memory locations.

Hi Marco, you seem to be reaching an issue with the solver, which is having trouble reasoning about the huge symbolic array (requiring excessive time and memory). You should try to shrink that array if possible. You can also try --optimize-array=all, but it might not help in your case.

Re: [klee-dev] Need help in understanding a kquery generated by KLEE

Hi Sandip, Those constants are most likely derived from concrete addresses, but you should try to simplify the program as much as possible and send a full program that can be compiled and run. Best, Cristian On 02/05/2022 19:22, Sandip Ghosal wrote: Hello, I need help in understanding a

Re: [klee-dev] Errors when files unconform to the format!

Hi Yukai, You can use klee_assume (https://klee.github.io/docs/intrinsics/#klee_assumecondition) on the desired symbolic file created by the POSIX runtime, see https://github.com/klee/klee/blob/master/runtime/POSIX/fd_init.c#L61 Best, Cristian On 06/06/2022 15:06, 房合钧 wrote: Hello! I

Re: [klee-dev] Idea: Klee experiment on Coreutils reimplementation in Rust

You should look at the work of Alastair Reid / Google on this topic: https://project-oak.github.io/rust-verification-tools/2021/07/14/coreutils.html Best, Cristian On 04/06/2022 22:26, gwpub...@wp.pl wrote: Klee got famous with coreutils experiments. As they reimplement coreutils in Rust,

Re: [klee-dev] KLEE for stateful C API

Hi Niklaus, There is no obvious improvement to recommend for the general case. Of course, search heuristics have an important influence on which API sequences are explored first. There is also a lot of research into this problem: I would recommend Randoop

Re: [klee-dev] How to determine the concretized size when dealing with malloc()

Hi Austin, Sorry to see that nobody has answered your email. I'm not sure what you are trying to do though. Are you trying to make KLEE choose a specific size? (That code is a bit broken, btw. We fixed it in some extensions but haven't managed to merge the changes into the mainline yet.)

[klee-dev] 3rd International KLEE Workshop on Symbolic Execution -- submission site NOW OPEN

, London and online Date: Mon, 16 May 2022 23:00:20 +0100 From: Cristian Cadar To: klee-dev@imperial.ac.uk Hi all, I'm very excited to announce the 3rd International KLEE Workshop on Symbolic Execution (KLEE 2022), taking place in London and online on 15-16 September 2022: https

[klee-dev] 3rd International KLEE Workshop on Symbolic Execution -- 15-16 September, London and online

Hi all, I'm very excited to announce the 3rd International KLEE Workshop on Symbolic Execution (KLEE 2022), taking place in London and online on 15-16 September 2022: https://srg.doc.ic.ac.uk/klee22/ https://twitter.com/kleesymex/status/1526310428485341187 The first two workshops were really

Re: [klee-dev] Collect path constraints with seed mode

Hi, On 21/09/2021 09:00, zy j wrote: Hi, I want to collect the path constraints of a specific PoC generated by fuzzing, I have found similar question in https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html ,

Re: [klee-dev] Need help in making a structure pointer symbolic

Hi, You can make pointers symbolic in KLEE, but this might not accomplish what you hope. Making a pointer symbolic means it can refer to any address in memory, including invalid ones. Best, Cristian On 04/03/2022 08:37, Sandip Ghosal wrote: Hello Everyone, Can somebody help me to make a

Re: [klee-dev] fork() : creating child processes in KLEE's execution

Hi, KLEE does not use the system call fork() to fork states. See Executor::fork() in the code. Best, Cristian On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote: Hi, I would like to check the possible scenarios where KLEE creates a child process. 1.My current understanding is that a

Re: [klee-dev] How should the function parameter be symbolised if the function parameter is a file type?

Hi, To use symbolic files, you should use KLEE's symbolic environment support. See https://klee.github.io/docs/options/#symbolic-environment and the tutorials for information on how KLEE supports symbolic files. Best wishes, Cristian On 18/01/2022 03:46, rongze xv wrote: Hi, I am

Re: [klee-dev] Packaging klee on Nix - gtest broken?

Hi all, Indeed, it would be great to update https://klee.github.io/getting-started/ (via a PR at https://github.com/klee/klee.github.io) to mention the Fedora and Nix packages. And thanks to everyone who is maintaining KLEE packages! Best, Cristian On 05/01/2022 10:01, Julian Büning

Re: [klee-dev] Default counterexample value generated by solver

Hi Weiqi, There is an open PR trying to implement this behaviour, but unfortunately it has not been finalized yet (perhaps you'd like to work on it?): https://github.com/klee/klee/pull/1117 Best, Cristian P.S. Kleaver does not pick the smallest valid value, the value generally comes from

Re: [klee-dev] How to distinguish klee's print of different execution paths

Hi, you would need to modify the code associated with those klee_ intrinsics to also output state information (see https://github.com/klee/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp). Best, Cristian On 01/09/2021 16:38, 樊雨鑫 wrote: Hi, I am new to Klee, use it to do program

Re: [klee-dev] Write to symbolic position

Hi Weiqi, Note that such an assignment does not impose any constraints on the input, which is why you don't see them in the path constraints (otherwise a simple code snippet such as buf[1] = '9'; buf[2] = '0' would be considered infeasible). You might want to check the initial KLEE paper

Re: [klee-dev] Improving KLEE coverage

Hi Vlad, It's difficult to say without seeing the full program, but it could be that KLEE is spending all its time in some other parts on the code. You can use klee-stats to understand how many states are in memory, how much time is spent in constraint solving etc., and kcachegrind to

Re: [klee-dev] Inquiry on path record and reply component of KLEE

Hi Harper, As I mentioned on GitHub, the .path feature is currently unmaintained, but it would be great to revive it. Best, Cristian On 10/07/2021 15:24, Wei Chen wrote: Dear developers, Hi, I found there is a case that KLEE would generate the same .path files for different paths in

Re: [klee-dev] About the two methods of test replay.

Hi Alex, I noticed this email went unanswered, hopefully the response is still useful. In short, we plan to maintain both replay methods. As you point out, the klee-replay tool only works when there are no klee_ intrinsics in the code. In this case, it is the preferred method, as it's

Re: [klee-dev] Filename length for kleaver

Hi Weiqi, I haven't looked at the code yet, but if this happens only for filenames longer than 32 characters, this might be a bug. Can you file an issue on GitHub, with an example? Best, Cristian On 06/08/2021 21:23, Weiqi Wang wrote: Hi, I noticed that kleaver generates different

[klee-dev] Postdoctoral position at Imperial College London

Hi all, We have another open postdoctoral position in my group, which involves projects that build up on KLEE (as well as others): https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-22/ I am happy to answer any informal queries (but please don't reply to the whole list). Best, Cristian

Re: [klee-dev] Phi nodes and LLVM11

Hi Alastair, I think your suspicions are reasonable, but perhaps the first thing would be to report a small code example that triggers this issue. Have you tried C-Reduce? Best, Cristian On 28/06/2021 15:02, Alastair Reid wrote: Hi, I am seeing KLEE crash on a large example generated by

[klee-dev] Workshop starting in 15'!

For those of you who registered, just a reminder that the workshop starts in 15' (making sure there is no timezone confusion!) Best, Cristian On 09/06/2021 12:55, Cristian Cadar wrote: Hi all, Just a reminder that the registration for the KLEE workshop is closing today.  We have around 200

[klee-dev] [REMINDER] Registration now open for the 2nd International KLEE Workshop on Symbolic Execution

2021 17:56, Cristian Cadar wrote: Hi all, I am happy to let you know that registration is now open for the 2nd KLEE workshop, taking place online on 10-11 June: https://srg.doc.ic.ac.uk/klee21/registration.html We have a very interesting program with a keynote from Chao Wang on adversaria

[klee-dev] Registration now open for the 2nd International KLEE Workshop on Symbolic Execution

Hi all, I am happy to let you know that registration is now open for the 2nd KLEE workshop, taking place online on 10-11 June: https://srg.doc.ic.ac.uk/klee21/registration.html We have a very interesting program with a keynote from Chao Wang on adversarial symbolic execution for detecting

[klee-dev] 2nd KLEE Workshop: Presentation proposals due on 10th May

Hi all, Just a quick reminder that the presentation proposal deadline for the 2nd International KLEE Workshop on Symbolic Execution is coming up, on Monday, 10th May. We have already received many interesting proposals, but there is still time for more!

Re: [klee-dev] KLEE as bitcode interpreter

Yes, without any symbolic input, KLEE essentially functions like an interpreter for LLVM bitcode. Best, Cristian On 19/03/2021 11:49, prashant chaturvedi wrote: Hi all.  I have compiled a source file to bitcode without debug information, i'm not using "any" of the KLEE's intrinsic, i.e i'm

Re: [klee-dev] Running KLEE for 32-bit

Hi, We don't support 32-bit anymore. See e.g.: https://github.com/klee/klee/issues/1327 https://github.com/klee/klee/issues/286 Cristian On 23/03/2021 06:08, kmohit wrote: Hi, KLEE version: 2.2 LLVM version: 9.0.0 Uclibc version: 1.2 Solver: Z3 I am trying to run a 32-bit bitcode on KLEE

Re: [klee-dev] Homebrew Package

Hi Carlo, We had a Homebrew tap set up a while ago see, https://github.com/klee/homebrew-klee, but it is currently unmaintained. So what we need is to have maintainers for these different packages. This is why it was great to hear about the Homebrew package you created (which I hope you'd

Re: [klee-dev] Using KLEE to analyze (complex) data structures

Hi, You say that you "got no useful results from KLEE so far" but it's difficult to help without more info and a self-contained program which reproduces the problem. Most likely though, you are hitting the challenge described in this paper, which offers a solution (and an extension of KLEE)

Re: [klee-dev] Homebrew Package

the website with installation instructions. Thanks! Best, Cristian Best, Carlo On 12 Mar 2021, at 17:13, Cristian Cadar wrote: Hi Carlo, This is great to hear! Thanks for this contribution! We should update the website with this info soon. It would be of course great to have one for Linux

[klee-dev] 2nd edition of the KLEE workshop moving online

Dear all, Thanks, Alastair for the reminder, we have literally just reached a decision about the new editions of the KLEE workshop. As you know, we were hoping to have the second edition in London, similar to the first. The atmosphere at the first workshop was fantastic, and we were

Re: [klee-dev] Homebrew Package

Hi Carlo, This is great to hear! Thanks for this contribution! We should update the website with this info soon. It would be of course great to have one for Linux too; from what I can tell, many of our users use Ubuntu, although I don't have any stats. Best, Cristian On 12/03/2021 16:45,

Re: [klee-dev] Question on dereferencing a symbol pointer

Hi, The short answer is that KLEE does not support mmap. However, it shouldn't crash and I cannot reproduce that behaviour: when I run it, KLEE reports a memory error at "*(int*)addr = 0;", as I also expected. Best, Cristian On 09/03/2021 14:46, Liu, Mingyi wrote: Hi klee-dev members, I

Re: [klee-dev] Use of -sym-stdin/stdout

=uclibc. Best, Cristian Thanks, best regards, Eduarrod On 9 Feb 2021, at 11:33, Cristian Cadar wrote: Hi Eduardo, Indeed, we need better documentation here. But in a nutshell: 1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF when compiling KLEE's uclibc to change

Re: [klee-dev] Use of -sym-stdin/stdout

Hi Eduardo, Indeed, we need better documentation here. But in a nutshell: 1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF when compiling KLEE's uclibc to change this) 2) you should only use —sym-sdout if you need to symbolically analyze the contents of stdout,

Re: [klee-dev] math.h functions interpreted as external

Hi Juan, The warnings say that no implementation for these functions is available. You should compile uclibc with support for these functions. However, note that mainline KLEE does not have support for symbolic floating point operations, but there are a couple of (open-source but

Re: [klee-dev] Question on use-after-free detection.

You are right, KLEE doesn't catch this use-after-free bug currently, as it doesn't implement a quarantine. It wouldn't it be too hard to add this though (you might want to refer to the ASan paper for details). Best, Cristian On 02/01/2021 18:16, Yoonseok Ko wrote: Hello,  I have an

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

Hi all, I have a couple of postdoctoral positions in my group at Imperial College London, at least one of which will involve KLEE: https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-21/ The application deadline is 7th January 2021. We also have fully-funded PhD positions, for which I am of

Re: [klee-dev] Bool vs i1 in STPBuilder

Hi Alastair, Our assumption is that code should not be able to construct such expressions in the first place and they are thus invalid at the KQuery level. That expression is also invalid at the SMT level, as Concat should take bitvectors and not booleans as arguments. If for some reason

Re: [klee-dev] How to handle 32bit bc file with 64bit klee

In particular, I would suggest to continue at https://github.com/klee/klee/issues/286 Cristian On 15/12/2020 14:35, Nowack, Martin wrote: Hi, There are a couple of missing features. Can you open an issue https://github.com/klee/klee/issues ? we can continue the discussion there. Best,

Re: [klee-dev] Strange compilation failure on 32-bit FreeBSD

Hi Gleb, Please see the discussion at https://github.com/klee/klee/issues/1327. In short, we're not supporting 32-bit platforms anymore, but if someone wants to revive support for this, we're happy to accept such a contribution. Best, Cristian On 13/12/2020 19:55, Gleb Popov wrote: Hello

[klee-dev] KLEE 2.2 released

Dear all, KLEE 2.2 is now released, many thanks for all the great contributions! And extra thanks to my co-maintainer @MartinNowack and to the authors of key improvements this release: @corrodedHash, @futile, @jbuening, @251, @kren1, @MartinNowack. The full list of changes can be found at

Re: [klee-dev] [KLEE] write to a symbolic address & constraints for write

Hi Mingyi, it's unclear to me what you are running exactly. In general, it's good to include a complete program and the exact commands you ran. Best wishes, Cristian On 20/11/2020 02:58, Liu, Mingyi wrote: Hi klee-dev members, I made args symbolic and provided a seed ktest file for the

Re: [klee-dev] How to make assumption on symbolic stdin in klee

Hi Pushi, to do this, you will need to modify the code in runtime/POSIX. Best, Cristian On 16/11/2020 12:34, Pushi Zhang wrote: Hi all,       As in the documentation of klee, we can use command "-sym-stdin" to make inputs symbolic.       Here my question is: how can we make assumptions

Re: [klee-dev] KLEE floating-point support

Hi Aleksei, From what I understand, you managed to rebase the KLEE-Float extension on top of KLEE's mainline. That's great! As I mentioned on GitHub, my main concern is that KLEE-Float changes the expression representation, which has a significant impact on the core of KLEE. The question

Re: [klee-dev] Retrieve concrete values of variables from an execution path

Hi Seemanta, Since you didn't include a full program, it's not clear what you want to do exactly. But at a higher level, note that KLEE is not a concolic execution engine, although it has some concolic execution features. However, it uses a counterexample cache, so you could adapt the code

[klee-dev] KLEE Open Projects list

Hi all, I have updated the list of KLEE Open Projects at https://klee.github.io/projects/ In particular -- and as also advertised on Twitter -- we are looking for package maintainers for Ubuntu and other popular distributions (thanks to Gleb Popov for maintaining KLEE's package on FreeBSD)

[klee-dev] KLEE: external tutorials, blog posts & more

Hi all, I've just added to the KLEE website a list of external tutorials, blog posts and other external resources on KLEE. In particular, I added a link David Korczynski's video tutorials on KLEE; Dennis Yurichev's "SAT/SMT by Example" book; Alastair Reid's project on checking Rust code

Re: [klee-dev] Crosschecking core solvers and printing the query causing the mismatch

Hi, I think what you want is --debug-crosscheck-core-solver. Best, Cristian On 16/09/2020 18:54, Shuo Ding wrote: Hi All, My goal is to compare the outputs of two core solvers (e.g. Z3 and STP) and get the query issued to those core solvers causing the mismatch. However, it seems that the

Re: [klee-dev] About klee's detection problems in real software

Hi, Yes, you need to compile the system under test to LLVM bitcode. However, nowadays things are much easier with the use of wllvm, as illustrated in that tutorial. Regarding the error you mentioned, just look in the .external.err file, it should contain an explanation about the issue.

Re: [klee-dev] Dealing with missing intrinsics (Rust support)

+1 to this, we should only terminate those paths that hit unhandled intrinsics. This is what we do with unavailable external functions and inline assembly for instance, so we should adopt the same behaviour here. Best, Cristian On 14/08/2020 18:06, Nowack, Martin wrote: Hi Alastair, I

Re: [klee-dev] Klee & pointers

Hi Igor, For this example, I don't think it makes sense to make the pointer itself symbolic. You could instead replace the klee_make_symbolic call with klee_make_symbolic(a, sizeof(*a), "a"); to make the malloc'ed memory symbolic. If you're interested in symbolic pointers more generally, I

Re: [klee-dev] Dummy pthread library?

Hi again Alastair, I'm not aware of anything like this, but it would be a nice extension of KLEE's POSIX environment. Best, Cristian On 30/07/2020 17:37, Alastair Reid wrote: Is there a dummy pthread library that I can use with single-threaded programs that only use a single thread but are

Re: [klee-dev] Distinguishing klee from runtest

Hi Alastair, Unless I'm misremembering things, we've never added anything like this, but this is the right approach, and I'd be happy to accept such a PR. I think the right way to do this would be to have this as an intrinsic defined in both runtime/Intrinsic and runtime/Runtest. Best,

Re: [klee-dev] Checking Tool Equivalence

Hi Linda, I cannot find that infrastructure anymore, but as explained in the paper, the idea was to rename global symbols and link the two tools together, accompanied by a new main function that looks similar in spirit to the one in Figure 11. The only tricky part is to capture and compare

Re: [klee-dev] Dbg Location

KLEE performs various transformations & optimizations on the input bitcode file, which is why you see those differences. Best, Cristian On 23/07/2020 09:55, Yugesh Kothari wrote: Hi, I had a question about the dbg location as seem in the assembly.ll file generated by Klee. I assume that

Re: [klee-dev] code style for easy, efficient symbolic execution

Hi Laszlo, There is no optimal code style for symbolic execution, although sometimes the style can significantly influence performance. There is some research on these topics (e.g., estimating constraint solving performance, understanding the impact of program transformations in symbolic

Re: [klee-dev] Executing Concretely inside a certain function

Hi, There is no direct way to do this, in the sense that KLEE doesn't have such an option. One possibility would be to concretize the arguments to the function using calls to klee_get_value_*. This is particularly easy if the arguments have primitive types. Best, Cristian On 17/06/2020

Re: [klee-dev] Error while using C++ STL, libcxx

On 26/05/2020 13:32, Namrata Jain wrote: I also want to know about klee version-2.1-pre, is it the same as version 2.0? This is because I have made some changes in my klee source (2.1-pre) for a project and now I will be using version-2.1. 2.1-pre is the version string reported by the mainline

Re: [klee-dev] ERROR 21: Can not open input file: .adl**

The POSIX runtime model creates file names 'A', 'B', 'C', etc. You can easily extend the model to support other file names, but this is not part of the mainline. You can read more about --sym-files in this tutorial: https://klee.github.io/tutorials/using-symbolic/ Cristian On 28/05/2020

Re: [klee-dev] Why KLEE still symbolic executing program after reaching max-fork?

Hi, This was the simplest way to implement --max-forks. I agree you could improve this, depending also on what you want to achieve. Best, Cristian On 25/05/2020 10:31, XIE Xuan wrote: Hi all, I am reading KLEE’s source code and find that if I set “-max-fork=n” when KLEE reach its fork

[klee-dev] KLEE workshop deadline extended to Tuesday

Dear all, Based on some requests, we are extending the deadline for sending presentation proposals to the KLEE workshop to Tuesday, 12 May: https://srg.doc.ic.ac.uk/klee20/cfpresentations.html Best, Cristian ___ klee-dev mailing list

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

Dear all, I am writing to remind you of the deadline for submitting a presentation proposal to the upcoming KLEE workshop: Friday, 8 May. I realize now that things are quite uncertain due to the COVID-19 situation. Therefore, we have also reserved 22-23 April 2021 as alternative dates if

Re: [klee-dev] Type of bugs that KLEE can find

Hi, The kind of bugs KLEE can find are memory errors (buffer overflows, null pointer dereference, etc.), division/modulo by zero, overshifts, and assertion violations. If I forgot anything, others should feel free to add to this list. KLEE does not report memory leaks, but it could be

Re: [klee-dev] KLEE Slow execution while executing natively

Improving the interpretation speed of KLEE is on our todo list. But KLEE's speed should be comparable to that of lli in interpreter mode (lli --force-interpreter=true). If you have examples where it's slower, I'd be curious to take a look, please open an issue on GitHub. Best, Cristian On

Re: [klee-dev] KLEE aborts with tcmalloc error

As you can see from the log ("LLVM ERROR: out of memory") the run exhausted all available memory. This is not that surprising for a 36h run. When you enable query logging, memory consumption increases further, as the textual representation of the queries can become massive after a long run.

Re: [klee-dev] Timed-out solver queries

Hi Hooman, How do you know it is not working? Are you sure there are queries that time out? Best, Cristian On 14/04/2020 08:39, Hooman wrote: Dear all, I have two questions and I will appreciate any help. 1- I am wondering how is it possible to find out the percentage of timed-out

Re: [klee-dev] KLEE finishes fast

Hi, Without including the program, it's not clear whether KLEE should have run for longer. One relevant thing one can tell from the log is that KLEE concretized a symbolic object size. Best, Cristian On 24/03/2020 09:45, XIE Xuan wrote: Dear KLEE, I am running KLEE on a fuzzing dirver.

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

Hi all, I have again both postdoctoral and PhD positions in my group at Imperial College London to work on topics involving KLEE (as well as other topics). You can find more details at: https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-20/ https://srg.doc.ic.ac.uk/vacancies/phd-pass-20/ The

Re: [klee-dev] Status of KATCH

I see your point :) But as a research project, it is still available if you want to give it a try. Cristian On 27/09/18 05:53, Xiao Liang Yu wrote: Hello Cristian, Does not integrated into mainline mean that it's discontinued? Thanks Xiao Liang On Wed, 26 Sep 2018, 8:07 PM Cristian Cadar

Re: [klee-dev] Status of KATCH

Hi Sang, KATCH was unfortunately not integrated into the mainline, but you should still be able to build it using LLVM 2.9 if you'd like to give it a try. Best, Cristian On 21/09/18 18:47, Sang Phan wrote: Hi everyone, May I ask what is the status of KATCH?

Re: [klee-dev] Solver goals

Hi Andy, the answer to the first two questions is a qualified yes -- you can make these guarantees assuming no interaction with external code, no constraint solving timeouts, no bugs in KLEE, etc. As to your final question, there are several research projects that aim to do this (e.g.,

Re: [klee-dev] Test cases generated for symbolic file

Hi, you can ignore the model_version, it just keeps track of the version for the POSIX model. The stat buffer keeps the stat info associated with the file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you have time, it would be useful to document this on the website (e.g.,

Re: [klee-dev] Options for symbolic environments no longer exist?

This should still work under Docker. Are you sure you are passing the options correctly? Those are not options to the KLEE tool itself, take a look at the tutorials for examples. If you still have problems, please fill out a bug report detailing the exact steps you followed. Cristian On

Re: [klee-dev] LLVM Error in Klee: does not support intrinsic function

Thanks for reporting this. Can you create a small test case and fill out a bug report on GitHub? Cristian On 11/06/18 05:20, Ridwan Shariffdeen wrote: Hi, I am trying to run klee with OpenJPEG (https://github.com/uclouvain/openjpeg), and encountered the following error: LLVM ERROR: Code

Re: [klee-dev] Klee Process Tree

Hi Sang, The option for dumping and visualizing the process tree is not well tested, so it would be useful to report bugs on GitHub, or even better, contribute a fix, if you have one. Best, Cristian On 24/05/2018 22:58, Sang Phan wrote: Hi everyone, I'm trying to dump the process tree of

Re: [klee-dev] About -sym-stdout

Hi, many programs write their output to stdout, and if this output is symbolic, you might want to check that it respects various properties. For instance, we used this option for the crosschecking study between Coreutils and Busybox utilities in the original KLEE paper. I agree more

Re: [klee-dev] Unable to build Klee with LLVM 3.8

Hi Sang, We plan to merge #729 into the mainline soon. However, the other PR, #605, still needs some work. But I hope to be able to bring support for 3.8 into the mainline in the next few weeks. Best, Cristian On 04/05/2018 22:44, Sang Phan wrote: Hello, I'm using a newer Ubuntu where

Re: [klee-dev] Replay ktestfile directory

Hi Awanish, this might be a bug, but we'd need more info. Can you open a bug report/issue on GitHub with steps to reproduce this? Best, Cristian On 01/04/18 17:01, Awanish Pandey wrote: Hi, I run klee over the coreutils using the command mentioned in coreutils experiments. When I replay

  1   2   3   >