We did some measurements using the coreutils test suite and the slowdown was in
the 10x - 100x area.
Paul
On 2 Jun 2011, at 04:39, Philip Guo wrote:
When running a typical program (e.g., coreutils) with Klee with NO symbolics,
how much slower is it than native execution? i.e., just using
Most likely the compiler optimizes away the if/then/else (it could for example
transform it into a bitwise operation here). Look at the assembly.ll file
generated in the klee output folder to see what's going on.
Paul
On 14 Jul 2011, at 08:52, Zhang Yufeng wrote:
Hi, everybody. I am new to
to
the list.
Thanks.
Lu
On 07/13/2011 02:59 PM, Paul Marinescu wrote:
t (i.e., no seeds), KLEE starts with a tree that has only one node, the
program entry point, and explores from there. A seed is essentially a tree
that you can provide as the starting point for the explorat
When compiling KLEE (svn head) against LLVM 2.9 on 64bit Ubuntu, the
POSIX tests never terminate. Upon looking at klee-last/assembly.ll (for
FDNumbers) it seems that memset recursively calls itself:
define i8* @memset(i8* %dst, i32 %s, i64 %count) nounwind {
entry:
%0 = icmp eq i64 %count,
that return pointers to
static data (unless it's defined in the LLVM module) or that allocate and
return pointers to new data.
-David
(I forgot to CC the list first, sorry!)
On Oct 27, 2011, at 7:19 AM, Paul Marinescu wrote:
Hi,
Most likely this is an invalid memory access which doesn't
I didn't have time to check this, but it should work by adding a call to
klee_define_fixed_object(my ptr, my ptr size) in the program, somewhere
before my ptr is dereferenced. See lib/Core/SpecialFunctionHandler.cpp for
the intrinsic implementation.
Paul
On 5 Dec 2011, at 16:06, arrowdodger
, Paul Marinescu
paul.marine...@imperial.ac.uk mailto:paul.marine...@imperial.ac.uk
wrote:
Hi James,
It doesn't seem like what you're trying to do is sound. Take this
slightly modified example:
#include klee/klee.h
void f(int c) {
if(c==1) {printf(Do A\n);}
if(c==2
The error can be caused by an inline asm instruction in your program
(e.g. call i32 asm ...). KLEE does not support them.
Paul
On 21/02/12 09:46, Jiaqi Tan wrote:
Hi,
I did some poking around the KLEE source, and found that this error is
being generated due to the assertion here (code
'!
Is this also caused by unsupported inline asm? Apart from the __asm__
calls, are there any other C constructs that might generate inlined
asm?
Thanks,
Jiaqi
On Wed, Feb 22, 2012 at 1:02 AM, Paul Marinescu
paul.marine...@imperial.ac.uk wrote:
The error can be caused by an inline asm instruction
the
recommended version of LLVM to use with klee from trunk?
Thanks,
Jiaqi
On Wed, Feb 22, 2012 at 1:55 PM, Paul Marinescu
paul.marine...@imperial.ac.uk wrote:
These intrinsics were added to LLVM after KLEE was released. Furthermore,
you can avoid them by disabling the instruction combine pass
Hello Lionel,
You are unlikely to be able to run httpd out-of-the-box with only ad-hoc
changes. The assertion that you're seeing is probably due to inline assembly.
Even if you get rid of that, you're going to stumble across other problems
related to the 'undefined' functions that you're
Hi Kapil,
You might be able to get around the issue by also setting
--max-sym-array-size to a reasonable value. For example
/klee.cde --optimize --libc=uclibc --posix-runtime --init-env
--max-sym-array-size=512 ./mknod.bc -sym-args 0 2 2
Paul
On 18/06/12 18:02, Kapil Anand wrote:
Hi all,
I
Try adding --max-sym-array-size=1024 (or smaller) to the invocation. I believe
this has been discussed before so you may find more info in the list archives
Paul
On 1 Sep 2012, at 14:20, Delcypher delcyp...@gmail.com wrote:
Hi,
I've been testing KLEE on core-utils (6.11) recently and I've
Depends on what changes you want to make. Assuming that you want to make
changes to the address space, copy the ExecutionState via the copy
constructor (or ExecutionState::branch) and then use the
AddressSpace::getWritable function for each object that you want to
modify to activate the
Hi John,
This issue seems to be similar to the one mentioned here
http://keeda.stanford.edu/pipermail/klee-dev/2012-June/000873.html. A
workaround is to give up some symbolic state by using --max-sym-array-size.
Some more information on the underlying problem is at
Hello Sunha,
llvm-gcc -c -emit-llvm test.c main.c
llvm-link test.o main.o -o program.o
klee program.o
Paul
On 20 Feb 2013, at 22:34, Sunha Ahn s...@princeton.edu wrote:
Hello,
May I ask about how to run multiple c source files?
For example,
--- test.h ---
int foo();
---
The problem is that if you run a program concretely, you will get no seeds with
KLEE (for command line arguments or input files). This is a sensible thing to
do, since you can use the same concrete values as input and you will get the
same results. Perhaps your usage scenario is a bit more
1. How do you define 'design structure'?
2. You might be criticising an apple for not being a good orange. KLEE is
designed to tests the program it's being executed on, and if one also wants to
test 41 variants, he/she will run KLEE again on the variants. I'm not sure what
you would expect,
You're probably looking for klee_print_expr, e.g. klee_print_expr(k = , k)
You can include includes/klee/klee.h for the prototype.
Paul
On 08/04/13 22:47, General Email wrote:
Hi,
How to get the content of a symbolic variable?
When I tried to run the code listed below, I got the following
Hello Loi,
DFS is not the default searcher for a few months now. What results do
you get with no --search argument?
Paul
On 23/04/13 12:03, Loi Luu wrote:
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly,
Hi,
Vanilla KLEE does not support multi-threading/multi-processes. If you're using
an extension, implementing shared memory/mmap depends on how multi-processes
are implemented, but it essentially amounts to creating an mmap model, similar
in principle to the existing models (see the
Hello Anton,
From your emails, it doesn't seem that ZESTI is what you're looking for. The
paper that you mention is related to KATCH
(http://srg.doc.ic.ac.uk/projects/katch/), which is a different project. We
don't currently offer KATCH for download but we might do so in the near future;
we'll
this
information from the version control system. We never got to port this
functionality back to ZESTI though.
Paul
On 25 Jun 2013, at 18:00, Jonathan Neuschäfer j.neuschae...@gmx.net wrote:
On Tue, Jun 25, 2013 at 05:35:34PM +0100, Paul Marinescu wrote:
Hello Anton,
From your emails
Hi Shiyu,
For --max-forks=10 the number of completed paths is 42 due to a bug: klee still
forks when encountering switch statements. A patch is available at
https://github.com/paulmar/klee/commit/90601a60fb6a0f22337c46680f150ec04ad3c6cb
. The output should now look similar to
KLEE: done: total
.
What if I'm interested only in getting the feasible paths that satisfy the
condition ((c==2)||(d==1)), i.e., in the paths that are evaluated to true.
How can I achieve this (if possible)?
Thanks,
AKhalil
On Monday, November 11, 2013 7:51 AM, Paul Marinescu
paul.marine
You may have missed a message sent to the list just a few days ago, related to
your non-determinism question
You might want to take a look at our CAV'13 paper
(http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html), which
discusses in more detail the constraint solving
There's no easy way to do it as far as I know. We did this, among others, in
ZESTI (http://srg.doc.ic.ac.uk/projects/zesti/) but it required changes to code.
If you only want to use KLEE, the 'easiest' way to do it would be to somehow
create a ktest file corresponding to your concrete input and
You're probably looking for TimingSolver::getInitialValues
Paul
On 19/11/13 04:40, jingde liu wrote:
Hi,
I want to seed a solution to evaluate the constraints of an
ExecutionState ignore the expr. In klee, evaluate(ExecutionState, expr,
Validity) evaluates the result of the expr (constraints--
You can break this down into two steps:
1. Figure out what the Expr for your constraint looks like
2. Figure out how to build that constraint
For 1, the easiest thing is to create a simple program that uses
klee_print_expr on your expression then run the program through klee.
For example
int
Unfortunately, this does not affect the way paths are explored. In
general, it doesn't make sense to use klee_assume(false) and
klee_assume(true). The first one terminates the state (klee_assert or
klee_report_error are more appropriate for that) and the second one does
nothing.
Paul
On
Not sure what you mean by ‘cannot handle'. If klee does not find the function,
you may be able to force loading the library using a command line argument like
--load=/path/to/lib**.so This won’t work if you need/have to symbolically
execute the library code, in which case either statically link
As Daniel pointed out, this is most likely one of those (rare?) cases when
installing Linux makes your problems go away.
Paul
On 9 Sep 2014, at 16:55, Dinh Ngoc Thi dinhngoc...@gmail.com wrote:
Dear Daniel Liew
Now I consider about Symbolic Execution tool, so I want to compile KLEE.
But
KLEE should handle this more gracefully. I’ve opened an issue on your behalf at
https://github.com/klee/klee/issues/248
Paul
On 25 Jun 2015, at 14:49, Sean Bartell s...@yotann.org wrote:
Hi,
Alexander Kampmann on 2015-06-25:
For my test input, the ktest-tool outputs the same object name
Hi Mario,
This is a really interesting project. I’m wondering about two things:
1. How do you introduce symbolic data? Does the Haskell program need to be
manually instrumented with klee_make_symbolic calls? grep-ing through your
repo, I didn’t find any --sym-arg(s) or klee_make_symbolic
2. How
34 matches
Mail list logo
