Re: [klee-dev] Question on Tracking Number of Instructions Per Path in Klee

Hello, the idea of stats in KLEE is to provide aggregate statistics, which means it is rather unsuited for getting information for each individual path. The per-instruction step count is available as `klee::ExecutionState::steppedInstructions`

[klee-dev] Question on Tracking Number of Instructions Per Path in Klee

Hi everyone, I want to find the number of LLVM instructions executed on each path in Klee. I can get the number of total instructions across all paths using standart Klee outputs so far. There must be a way to find out the number of instruction on each path, but I don't know how. Here’s what

[klee-dev] [Question about process of seed in KLEE] For mechanism of detailed process when putting seed in KLEE

To Whom it may concern, Hello, this is jaehyoek Lee, a master degree's student in computer science in South Korea. I have some questions about the detailed process of KLEE, especially the seeding process, so I'd like to send this mail. I'm using klee-2.1 under LLVM 6.0.0 version. >From my

Re: [klee-dev] C++ Support Status

Hello Volodomyr, C++ support in KLEE is available, with the major caveat that (as for C code) you need to compile everything to LLVM bitcode. Just like for C code, we have a prepared standard library available, although there are some limitations in that regard (again, just as for C). The

[klee-dev] C++ Support Status

Hello, Is Klee a good tool for analyzing C++ code?  I saw an email from 2018 regarding C++,  what's progress on it? Do you have examples of using Klee in C++ projects with CMake, Qt, Boost, STL, Google Test, etc? I just started to go through examples. I set compiler and linker flags as

Re: [klee-dev] How to solve path explosion caused by loop?

The number of paths explored by KLEE is exponential in the number of iterations: a path discovered in the first iteration is extended by every path discovered in the second iteration, and so on. It seems that you introduce the loop only to explore all possible values of event.  If so, just

[klee-dev] A question on using gcov for coverage testing

Dear klee developers, I am recently using klee for test case generation and it has been proved to be an efficient tool in the field of symbolic execution. But when it comes to coverage, a question occurs. Currently the coverage type i want is modified condition/decision coverage, but klee

[klee-dev] How to solve path explosion caused by loop?

Hi all I met a problem which loop cause path explosion. For example, there are 3 variables, control_block, p_data and event. Control_block and p_data are structures and have some fields as symbolic. Event is an integer between 0 to 42. Now I want to run smp_sm_event(control_block, p_data,

Re: [klee-dev] Why can't we use ExecutionState object in vector or map templates in cpp

Hi, On Thu, 4 Apr 2024 00:32:02 +0530 Adarsh Sudheer wrote: > Recently i tried to map the current the executionstate to it's left and > right nodes using execution tree and all seemed fine until I encountered > various segmentation errors. Firsty, in the ExecutionState class > definition, i

Re: [klee-dev] Why can't we use ExecutionState object in vector or map templates in cpp

Please forgive me for some grammatical errors. I just was in a hurry. On Thu, Apr 4, 2024 at 12:32 AM Adarsh Sudheer wrote: > Hi all, > > Recently i tried to map the current the executionstate to it's left and > right nodes using execution tree and all seemed fine until I encountered > various

[klee-dev] Why can't we use ExecutionState object in vector or map templates in cpp

Hi all, Recently i tried to map the current the executionstate to it's left and right nodes using execution tree and all seemed fine until I encountered various segmentation errors. Firsty, in the ExecutionState class definition, i defined my new attribute as like this

Re: [klee-dev] Connection between CFG and execution state

Dear Adarsh, On Wed, 21 Feb 2024 07:33:09 +0530 Adarsh Sudheer wrote: > Is there any parameter in the Execution state that links the CFG to the > ExecutionSt ate. To be particular, I want to access all ExecutionState > nodes generated from a CFG? You can't really map a state to the CFG

Re: [klee-dev] [Question] What is the correct/efficient way to implement a separate execution without affecting the normal execution in KLEE?

Dear Haoxin, On Tue, 26 Mar 2024 07:51:13 + TU Haoxin wrote: > In the first normal execution, I don't know which state is good to > explore so I randomly select one (say "C" is selected). Then, I want > to use a "simulation" run (a separate execution from a normal > execution ) to evaluate

[klee-dev] [Question] What is the correct/efficient way to implement a separate execution without affecting the normal execution in KLEE?

Dear KLEE developers, May I ask a question about implementing a separate execution in KLEE? My initial idea is to separate ("simulate") running a state and evaluate whether this state is worthy of exploring in the future further. I will use the attached figure to explain what I want to do

[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] Connection between CFG and execution state

Hi all, Is there any parameter in the Execution state that links the CFG to the ExecutionSt ate. To be particular, I want to access all ExecutionState nodes generated from a CFG? With Regards Adarsh Sudheer ___ klee-dev mailing list

Re: [klee-dev] Logging the Symbolic Values of Variables

Hi Luke, As KLEE builds on LLVM, the value is either part of an SSA register or a heap/global allocation. In the first case, the register’s value can be accessed via `eval()`, i.e. for a Load instruction

[klee-dev] Logging the Symbolic Values of Variables

Hello, My research group is looking to output the value of each variable's symbolic representation after the execution of each line in the source program. Alternatively, the symbolic values of only the variables whose values are modified on that line would be sufficient as well. For example,

[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] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

Hi Daniel, Thanks for your further investigation. Your explanation makes sense to me. I started my project a few years ago so I used a relatively older version of KLEE I believe I will build on my next project on the newest versions of them to avoid similar issues and catch up with KLEE's new

Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

Hi Haoxin, The described behavior is indeed very odd. Luckily, the `assembly.ll` that is generated by KLEE shows that this is an actual optimization error - the code that is intended to print your messages does not exist anymore. This means that the issue lies either with the LLVM

Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

Hi Nguyen, Just installed and run this case using KLEE-3.0 with LLVM-10, and it seems the issue is still reproducible for KLEE 3. Please check more here: https://gist.github.com/haoxintu/183dda2923965d1e33f64ad59c7f5338#other-trials Thanks, Haoxin From:

Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

On 2024-01-31 at 05:07+00:00, TU Haoxin wrote: > The behavior is that KLEE fails to fork at a branch > that should be forked with the option --optimize option enabled > (i.e., --optimize=true). While the --optimize option is disabled > i.e., --optimize=false), the branch can be successfully

[klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

Dear KLEE developers, I found an interesting behavior of KLEE while using a variant tool of KLEE (https://github.com/haoxintu/SymLoc) to test the dircolors​ package in GNU Coreutils. The behavior is that KLEE fails to fork at a branch that should be forked with the option --optimize option

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

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

收件人:klee-dev@imperial.ac.uk 周三 2024/1/24 19:18 Hi, I am new to Klee. I have a question about how to determine which path constraints generated in the KQuery file correspond to specific paths or lines of code in the original source code or in the IR? For example; I have a dummy c code that have

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] Different behavior when invoking the "error" function with the argument buffer from heap or stack

Dear KLEE developers, Hope you are all doing well, and hope this is the right place to raise questions about KLEE. I have a question regarding the modeling of the function `error` function in `klee-uclibc` when I used KLEE. Since I couldn't find similar cases either in the GitHub issue or the

[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!

Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

Hi Oleg, Ah - yeah there is. The name is `klee::findSymbolicObjects` but it’s a bit hidden: https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/include/klee/Expr/ExprUtil.h#L38 and

Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

Hi Martin, Thanks for the quick response.  Our question was slightly different, let me clarify.  Given an instance of the Expr object, we want to obtain the set of symbolic names used in that instance.  ExprPPrinter does it, for example, but in a very specific way and, frankly, we struggled

Re: [klee-dev] Using Klee with Dynamic Libraries

Hi Yukai Zhao, Can you provide the output of your KLEE run? My guess is that `max`, `min` are treated as external functions that forces a and b to be concretised, i.e. which leads to only one path being generated. But let’s have a look at your output to confirm this. Best, Martin > On 12. Dec

Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

Hi Haozhi Fan, The symbolic names are generated using the call `klee_make_symbolic` indirectly or directly in your software under test. KLEE tracks the memory object that have been associated with these calls

[klee-dev] Using Klee with Dynamic Libraries

hi， I am curious about the boundary situation of Klee. Will it constrain the generation of functions in the file specified by the parameter "-- link llvm lib"? Of course, this file is also a. bc file, in fact it is a dynamic library generated by the project. My executable file is dynamically

[klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

Dear klee-dev members, I was wondering if you could share some insight into how KLEE collects the set of symbolic names from an expression? Namely, how does KLEE generate the kquery for a specific path condition and from which files should I be looking for the details of such implementation?

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

Hi all, A final reminder about the first (visa-safe) submission deadline for KLEE 2024. We are looking forward to your submissions! And thanks to everyone who has already submitted their interesting work! https://srg.doc.ic.ac.uk/klee24/cfpresentations.html

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

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 work that you'd like to present, or an extended abstract of up to two

Re: [klee-dev] can't get the get_sign.c to work under Tumbleweed Suse with clang-17

Am 02.10.2023 um 16:31 schrieb Nowack, Martin: Unfortunately you have to stick with LLVM 14 in this case. fine - thank you for all the work on Klee im currently starting to use it to check if i translated 16bit dos disassembly correctly to equal C code - Klee helps creating the test-cases i

Re: [klee-dev] can't get the get_sign.c to work under Tumbleweed Suse with clang-17

Hi Dennis, KLEE currently doesn’t support newer LLVM versions than 14. We are working on this but it’s not in a stage for upstreaming it yet. Unfortunately you have to stick with LLVM 14 in this case. Best, Martin > On 1. Oct 2023, at 11:23, Dennis Luehring wrote: > > Standard Clang 17.0.1

[klee-dev] can't get the get_sign.c to work under Tumbleweed Suse with clang-17

Standard Clang 17.0.1 and Klee 3.0 from Tumbleweed package manager per default the klee packages comes with LLVM 14.0.6 linux@localhost:~/tests/klee_dev> clang --version clang version 17.0.1 Target: x86_64-suse-linux Thread model: posix InstalledDir: /usr/bin linux@localhost:~/tests/klee_dev>

[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:

[klee-dev] ExprVisitor::visitExpr[Post] and ExprReplaceVisitor[2]

Hi, In lib/Expr/Constraints.cpp I notice class ExprReplaceVisitor : public ExprVisitor { public: Action visitExpr(const Expr ) override { if (e == *src) { return Action::changeTo(dst); } return Action::doChildren(); } Action visitExprPost(const Expr ) override { if

Re: [klee-dev] All possible paths from source to destination function.

On 2023-07-25 at 18:50+05:30, Sailesh Sai Teja wrote: > So lets say I want to trace the execution path from function > "functionA" to function "divide", the following is the output > I am expecting > > 1. "functionA && ((x < y) && divide)" > 2. "functionA && ((y > 0) && divide)" Since no one gave

[klee-dev] All possible paths from source to destination function.

Hello all, I am performing static analysis on a codebase and for that I am trying to find all the possible paths from function 'A' to function 'B' along with the conditions that are responsible while traversing that path. My input is a large llvm IR file which contains all the functions

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

On 2023-07-12 at 22:03+01:00, Cristian Cadar wrote: > On 07/07/2023 06:57, Nguyễn Gia Phong wrote: > > I notice that ConstraintSet is implemented via std::vector. > > This make me wonder about the likelihood of duplucated constraints > > during executions. > > KLEE does not add duplicate

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] Tracking changes of specific variables

Hello All, I am trying to add a new search algorithm, so that the states where a certain variable change happens are selected for exploration over the others, and only fall back to the BFS/DFS when this given criteria does not exist in any of the possible states. For example, in this code I

Re: [klee-dev] About Using KLEE to Check CoreBench

On 2023-07-09 at 20:25+08:00, 尹麓鸣 wrote: > How should I compile CoreBench using wllvm > and use KLEE to check CoreBench? CoreBench essentially provides the error-introducing and -fixing commits for each bug. Included programs use the GNU Build System, which warrants neither backward nor forward

[klee-dev] About Using KLEE to Check CoreBench

Hello, I would like to use KLEE to check CoreBench (an open source work on Coreutils). How should I compile CoreBench using wllvm and use KLEE to check CoreBench?Thank you for taking the time out of your busy schedule to read my letter. Looking forward to your

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

Hi, I notice that ConstraintSet is implemented via std::vector. This make me wonder about the likelihood of duplucated constraints during executions. Does anyone have any emprical data or experience regarding this aspect? Regards, McSinyx ___

Re: [klee-dev] About TestComp-specific KLEE command-line options.

Hi Alex, The remaining patches are not submitted yet and need some cleaning. But in a nutshell, `-tc-type` is set based on type of goal the test has: bug finding vs. coverage. They are slightly different in both cases, please refer to the TestComp documentation (categories).

[klee-dev] About TestComp-specific KLEE command-line options.

Hello, In the KLEE Wrapper used for TestComp there are some command-line options that are not present in the KLEE repository. The following options are missing: -write-xml-tests -tc-orig -tc-hash --tc-type -dump-test-case-type -coverage-on-the-fly The first three are present in the following

Re: [klee-dev] adding setjmp/longjmp support?

Hi Dan, We are always looking for contributors and contributions ;) A good starting point for KLEE development is: https://klee.github.io/docs/developers-guide/ >From a technical perspective, it is not trivial but not too hard either. The main function you are interested in is

[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

[klee-dev] adding setjmp/longjmp support?

I'm looking to apply KLEE to a program that heavily uses co-routines. These syscalls aren't implemented, so I'm investigating whether a patch can be written/upstreamed. This is my first patch for KLEE (but I have written patches for other large open-source projects). A few questions: 1. Are

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

On 2023-05-23 at 18:05+01:00, Frank Busse wrote: > On Tue, 23 May 2023 16:38:25 +0900 > Nguyễn Gia Phong wrote: > > what are the potential drawbacks of enabling > > symbolic printf in KLEE's µClibc? > > printf has to transform its parameters into strings. This is heavily > branching code (even

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

Hi, On Tue, 23 May 2023 16:38:25 +0900 Nguyễn Gia Phong wrote: > Do you recall the reason for that default, > i.e. what are the potential drawbacks of enabling > symbolic printf in KLEE's µClibc? printf has to transform its parameters into strings. This is heavily branching code (even worse

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

On Tue Feb 9 11:33:00 GMT 2021, Cristian Cadar wrote: > printf is run concretely by default (you can add -DKLEE_SYM_PRINTF > when compiling KLEE's uclibc to change this) Do you recall the reason for that default, i.e. what are the potential drawbacks of enabling symbolic printf in KLEE's µClibc?

Re: [klee-dev] get the absolute path of file in InstructionInfo

Hi Jiayi, On Thu, 11 May 2023 22:48:28 +0800 王加益 wrote: > I have a question about the `const std::string ` in `struct > InstructionInfo`. From my observation, this `file` is always a > relative path, regardless of whether the file is in klee-uclibc, klee > runtime, or my own testing subjects.

[klee-dev] get the absolute path of file in InstructionInfo

Hi, I have a question about the `const std::string ` in `struct InstructionInfo`. From my observation, this `file` is always a relative path, regardless of whether the file is in klee-uclibc, klee runtime, or my own testing subjects. For example, we have: - runtime/POSIX/fd.c -

Re: [klee-dev] Symbolic calls to mqueue.h functions ?

Hi Delphine, > On 25. Apr 2023, at 16:07, LONGUET Delphine > wrote: > > Hi Martin, > > Thanks a lot for your answer. That works, in the sense that now mq_open is > found, but unfortunately, the implementation contains assembly code not > supported by Klee : > > KLEE: WARNING: function

Re: [klee-dev] Symbolic calls to mqueue.h functions ?

Hi Martin, Thanks a lot for your answer. That works, in the sense that now mq_open is found, but unfortunately, the implementation contains assembly code not supported by Klee : KLEE: WARNING: function "__syscall_mq_open" has inline asm [...] KLEE: ERROR: librt/mq_open.c:15: inline assembly is

Re: [klee-dev] Symbolic calls to mqueue.h functions ?

Hi, > On 24. Apr 2023, at 10:53, LONGUET Delphine > wrote: > > > I am trying to execute Klee on a code using mqueue.h and despite the > -posix-runtime and -libc=uclibc options, functions mq_open, mq_close, etc, > remain "undefined references". I can see that there actually are >

[klee-dev] Symbolic calls to mqueue.h functions ?

Hello, I am trying to execute Klee on a code using mqueue.h and despite the -posix-runtime and -libc=uclibc options, functions mq_open, mq_close, etc, remain "undefined references". I can see that there actually are implementations of these functions in /klee-uclibc/librt/, but they don't seem

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] General question

Hi Teja, I was also looking for this feature. Have you come up with a workaround? Do you know if there is a way to transform expressions in kquery format to smt2 format? Best, ~ Ferhat On Mon, Jan 9, 2023 at 7:21 AM Teja Sai Srikar Bodavula wrote: > Hello, I was wondering if there is way in

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

Hi, I wanted to ask about converting symbolic expressions in KQuery format to SMTLIB format. Currently, I am able to obtain the symbolic expressions using `klee_print_expr` in KQuery format, but I need to manipulate them in bit-vector logic, which requires converting them to SMTLIB format to

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

[klee-dev] About external shared libraries

Hi all, I'm trying to use KLEE to analyze some real-world programs such as image processing programs. Unfortunately, I found KLEE usually terminated early because of 'failed external call' errors, where the call was from shared libraries located in directories on the system search path. I know I

[klee-dev] General question

Hello, I was wondering if there is way in which we can get symbolic formula for a variable in a code in smt2 format unlike kquery format which we get using klee_print_expr. ___ klee-dev mailing list klee-dev@imperial.ac.uk

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

[klee-dev] Debugging options

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 is the instruction log from replaying only the

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

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

Hello. KLEE can call functions that do not have IR available as externals. Some C standard library functions are also called as externals (e.g. printf). How is the standard library linked to the JIT engine that calls externals? Also, why isn't loading of binary-only libraries supported in KLEE?

Re: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Great! will look into the code. Thanks very much for help. Nazir, Tareq Mohammed 于2022年10月24日周一 15:17写道： > Hi, > > > Found below link > > > https://github.com/tum-i4/macke > > GitHub - tum-i4/macke: Modular And Compositional analysis with KLEE Engine >

Re: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Hi, Found below link https://github.com/tum-i4/macke [https://opengraph.githubassets.com/8e0dac6e7d018e975a14a12be73f158f99de4c22b0fa610dc0502b0245c3b249/tum-i4/macke] GitHub - tum-i4/macke: Modular And Compositional analysis with KLEE

Re: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Thank you. I have read the paper you recommended. I know now that compositional analysis can be achieved in KLEE but the details are not discussed in that paper. Is there any open source code for this? Nazir, Tareq Mohammed 于2022年10月23日周日 20:44写道： > Hi, > > > Please find the below paper is this

Re: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Hi, Please find the below paper is this related to the topic : https://dl.acm.org/doi/abs/10.1145/2970276.2970281 [https://dl.acm.org/cms/asset/53e7485c-29f4-4b88-b12f-3ac86ec74c11/2970276.cover.jpg] MACKE: compositional analysis of

[klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Hi, I'm currently planning to verify an idea about compositional symbolic execution (CSE). But CSE is not officially supported by KLEE now as far as I know. So I am eager to know whether it is possible to implement CSE in KLEE. If so, please give some suggestions about how to implement that. Thank

Re: [klee-dev] Video games and embedded systems???

 Martin,    Ok thank you very much for your response.     I greatly appreciate it.     I was wondering is there any verified and validated methodology to divide a large application such as a modern video game into more testable sub systems??? Then once you combine those separate components back

Re: [klee-dev] Regarding getting variable names from KLEE

Hi Tareq, I can highly recommend you the following documents to get an understanding of the internal details of debug information and LLVM that KLEE uses in the first place: * https://llvm.org/docs/SourceLevelDebugging.html * https://llvm.org/docs/HowToUpdateDebugInfo.html For the examples

Re: [klee-dev] Video games and embedded systems???

Hi David, Have a look at https://klee.github.io/publications for a multitude of use cases that KLEE has been used successfully: That said, the larger your application is the more challenging it becomes to test it with any method. In those cases it becomes useful to test parts of the

[klee-dev] Video games and embedded systems???

KLEE dev question.  I was wondering if the KLEE environment has ever been used for a large application like a modern video game or for development or testing of an embedded system such as a microcontroller or FPGA?  Is this feasible Thanks David

Re: [klee-dev] Regarding getting variable names from KLEE

Hi Frank, Thanks for the reply, Yes I have used the second option and -fno-discard-value-names and I am able to see the variable name in the llvm bitcode .ll file. But what I need is the access to this variables in KLEE engine. Also I am trying to use DILocalVariable. I would like to know

Re: [klee-dev] Regarding getting variable names from KLEE

On Wed, 5 Oct 2022 at 14:10, Nazir, Tareq Mohammed wrote: > Yes I would be needing the source-level variable names and source-level info. > We are currently trying to understand the vulnerabilities such as heap > overflow that can be present in the source code. We are able to understand > the

Re: [klee-dev] Regarding getting variable names from KLEE

Hi Ryan, Thanks for the reply, Yes I would be needing the source-level variable names and source-level info. We are currently trying to understand the vulnerabilities such as heap overflow that can be present in the source code. We are able to understand the how KLEE engine is able to

Re: [klee-dev] Regarding getting variable names from KLEE

On Wed, 5 Oct 2022 at 10:28, Nazir, Tareq Mohammed wrote: > I would like to know if I can get variable names of the source code in KLEE > engine. Would also like to know if KLEE engine is storing the variable name > information while executing the llvm bitcode symbolically. KLEE currently

Re: [klee-dev] Regarding getting variable names from KLEE

Hi, On Wed, 5 Oct 2022 09:26:35 + "Nazir, Tareq Mohammed" wrote: > I would like to know if I can get variable names of the source code > in KLEE engine. Would also like to know if KLEE engine is storing the > variable name information while executing the llvm bitcode > symbolically. > >

[klee-dev] Regarding getting variable names from KLEE

Hi, I would like to know if I can get variable names of the source code in KLEE engine. Would also like to know if KLEE engine is storing the variable name information while executing the llvm bitcode symbolically. For example : From the below C code I want to get the buffer variable name is

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] Use KLEE with JAVA and C#

Hi everyone, I'm looking for a tool for symbolic execution in C# or JAVA. Does Klee support C# or JAVA? I searched the mailing list archive and found the same question for JAVA posted several years back. Does anyone know if there are any updates regarding these? I would really appreciate any

[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

[klee-dev] Understanding of KQuery

Hi, I was going through the documentation of KQuery, and I got a little confused about Query Commands. The documentation says that query-expression​ is the expression to determine the validity of the query. Does it mean that Klee evaluates query-expression​ under the constraints defined in

Re: [klee-dev] 3rd International KLEE Workshop on Symbolic Execution: Registration Open

Hi all, A quick reminder: the early registration deadline is approaching fast - tomorrow, 10th August. Looking forward to welcome you in person. The KLEE 2022 Organisers > On 29. Jul 2022, at 16:00, Nowack, Martin wrote: > > Hi all, > > We are delighted to host this September the 3rd

Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

Hi, On Mon, 8 Aug 2022 18:24:27 -0700 Biqian Cheng wrote: > Did you rebuild it (make) in case it was wrong beforehand? > > Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON > -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then > "make -j2" to rebuild it. I meant uclibc.

Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

Hi Frank, Did you rebuild it (make) in case it was wrong beforehand? Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then "make -j2" to rebuild it. Then check the LLVM version klee is linked against (e.g. ldd > /bin/klee)

Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

Hi, On Mon, 8 Aug 2022 13:18:54 -0700 Biqian Cheng wrote: > Thanks for your reply. I typed this command as you suggested > previously: ./configure --make-llvm-lib --with-cc clang-11 > --with-llvm-config llvm-config-11 > > Here are what I got after typing that command: Looks good. Did you

Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

Hi Frank, Thanks for your reply. I typed this command as you suggested previously: ./configure --make-llvm-lib --with-cc clang-11 --with-llvm-config llvm-config-11 Here are what I got after typing that command: INFO:Forcing C compiler to be...clang-11 INFO:Absolute path to

  1   2   3   4   5   6   7   8   9   10   >