I think you can't.In KLEE, each state is represented as a mapping of program
variables to an expression in terms of initial symbolic values.This is probably
better in terms of performance as the number of program variables is likely to
be smaller than the length of the path. Storingthe transitio
Hi Sumit,
Presumably you are looking into Executor::executeInstruction method.If you take
a look at, for example the code that handle LLVM'sInstruction::Add right after
"case Instruction::Add:"
ref left = eval(ki, 0, state).value;
ref right = eval(ki, 1, state).value;
ref result = Ad
Hi Sumit,
It's declared in include/klee/Expr.h using macro COMPARISON_EXPR_CLASS.Note
that below the definition of that macro there is a line that says
COMPARISON_EXPR_CLASS(Eq)
Which actually declares EqExpr.
Best,Andrew
On Thursday, 24 March 2016, 4:18, Sumit Kumar wrote:
Hi,
Can any
Hi Sumit,
I think it's your choice. In our project, we have (or used to have) global
static variables declared in a header file in lib/Core/and defined in a cpp
file in the same directory. We have also added command-line options in
lib/Basic/CmdLineOptions.cppwith globally-accessible declaration
Hi Fabrizio,
1. Your example is missing from your email, but I think validity in KLEE means
that any valuation is a model (as in model theory). Whereas it seems your
understanding of validity (some valuations are models) is more commonly known
as satisfiability.2. I don't recall ever seeing KLEE
Hi Sumit,
I think that comment and declaration are in include/klee/Solver.h and not
Solver.cpp.
My rough understanding is as follows. A Query object is a data structure
containinga list of "constraints" and an "expression" (expr field). I think
Query objects are typicallyused to query the solver
Dear All,
In KLEE, it seems symbolic floating point variables are simply converted to int
and grounded to 0. I am wonderingwhat is the current state of floating point
symbolic execution support in KLEE? I know there has been some workon KLEE-FP
in the past, but does it actually check path feasi
Many thanks to Cristian for his reply to my previous question in this thread:
Re: [klee-dev] Floating-Point Symbolic Execution
| |
| | | | | | | |
| Re: [klee-dev] Floating-Point Symbolic ExecutionHi Andrew,KLEE-FP/KLEE-CL
(https://srg.doc.ic.ac.uk/projects/klee-cl/) is targeted p
Sorry, following is the correct link to the previous email thread that I
mentioned
(which may have disappeared from my email).
http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02334.html
Best,
Andrew
On Friday, 17 June 2016, 11:50, Andrew Santosa wrote:
Many thanks to Cristian for his
Dear Qingkun,
I believe the following is close to your original source:
#include
#include
int get_sign(int x) {
if (x == 0) {
return 0;
}
if (x < 0) {
return -1;
}
return 1;
}
int main() {
int a;
klee_make_symbolic((char *) &a, sizeof(int), "a");
return get_sign(a);
Hi Sergey,
Although this is only a guess, my guess is that this is because KLEE is
worklist-based, where an item in the worklist represents an execution state.
The executor (Executor class) has a field searcher, whose runtime type
determines the kind of exploration strategy used by KLEE. Executo
Dear Iason,
I think a possible solution might be to modify ExprPPrinter class, such that
KQuery format would instead displaythe constraints in the format that you want.
Best,
Andrew
On Tuesday, 1 November 2016, 22:28, "Papapanagiotakis-Bousy, Iason"
wrote:
Hello, I am a new
user
I think this idea has a merit. If we replaced many library code even with
slightly different (or even slightly wrong) implementation in order to get the
KLEE-executable bc, then KLEE execution can remain symbolic for longer before
switching to concrete, potentially gaining better coverage.
Andr
On no. 4, I think Lei's approach is probably fine for their purpose, assuming
what needs to be accomplished here is simply making a, b, and c represent
nondeterministic int input.
But since scanf is a function that reads from the standard input, if one goes
through the Coreutils tutorial (tha
Dear Javier,
I think you can use -write-pcs to make KLEE output test*.pc files which showthe
path condition for each generated test.
-write-pcs will ouput in KLEE's own expression format, but other formats
arealso avaiable: -write-smt2s and -write-cvcs will output in SMT2 and CVC
formatrespectiv
Dear Chelsea,
I think you may want to explore KLEE's -write-paths, -write-pcs, -write-cvcs,
and -weire-smt2s options.-write-paths in particular outputs a sequence of 0s
and 1s in a .path file for each test case indicating whetherrespectively it is
the false or the true branch that is taken at ev
Hi Awanish,
I guess Line 362 of socketcalls.c contains assembly language which is not
supported by KLEE, as KLEE symbolically executes only LLVM.
Best, Andrew
Sent from Yahoo Mail on Android
On Tue, Dec 13, 2016 at 7:29 PM, Awanish wrote:
Hi,
I compiled apache with llvm2.9 and when I
Dear Javier,
I believe the straight answer is no.
I think Z3, which is now supported by KLEE, supports uninterpreted functions,
so itseems possible to implement this feature, but the question is why should C
functionbe mathematical function? What if the C function has side effects?
However, a po
libm functions such as sin() are 1) usually side-effect free and 2) on
floating-point values, which are not typically used for control decision,
so many of them can probably be shown statically to not affect branch decision.
But let us think about the purpose of symbolicizing them:
1. Since t
eria™ smartphone
Andrew Santosa wrote
>
>
> On Friday, 23 December 2016, 14:37, Yude Lin
> wrote:
>
>
> Hi Guys,
>
>For a function in the program source code, i.e., not a library function,
>do you think we have reasons to make it uninterpreted? My idea is
nction call
>and
>focus more on other parts of the program. But the downside is it introduces
>imprecision and false alarms. I wonder how KLEE devs/users view this
>imprecision (as I'm quite new around here). Thanks!
>
>Regards,
>Yude
>
>On Fri, Dec 23, 2016 at 8:11
Dear Qingyang,
Perhaps you may want to first look the comments in SolverImpl.h. For this, you
can generate
the doxygen documentation in the following way:
make doxygen
The documentation for SolverImpl class should be here:
docs/doxygen/html/classklee_1_1SolverImpl.html
Regarding the variety
I think an issue here is that there is no such thing as --sym-file option;
there is only --sym-files.
klee --libc=uclibc --posix-runtime sock_simple.bc A --sym-files 1 1000
worked for me.
Best,
Andrew
On Wednesday, 21 June 2017, 1:05, Shehbaz Jaffer
wrote:
Thank you for your reply, I apo
Hi BNM,
KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM.It
is reported when KLEE determines that the shift amount is greater than the
bitwidth of the data beingshifted. I happen to have a copy of SPEC CPU 2006. At
Line 108 of classic.c there is a loop whose entrycondi
--disable-nls is specific to Coreutils. You may not need to worry about it.
Since you have a Makefile, perhaps you could try the following to build your
benchmark:
LLVM_COMPILER=clang CC=wllvm CXX=wllvm++ make
After the above produced a binary, say prog, please do the following:
extract-bc prog
Hi BNM,
If I understand correctly, here there are two categories of test suites
discussed: one contains the test suite generatedby KLEE, and another contains
test suites that come with the program itself. If you want to measure the
coveragespecifically achieved by KLEE, then you should only run
Hi Charitha,
Perhaps others can provide better answer, but I believe it will involve
significanteffort to implement what you want in KLEE.
Since you also asked for other approaches, I am reminded of work I did years
backon symbolic execution using constraint logic programs, which perhaps is
clos
Hi Charitha,
You can try to run the configure script of Coreutils in the following way:
CFLAGS=-I LDFLAGS=-L LIBS=-lkleeRuntest
./configure
where is where libkleeRuntest.so* live. You may need to set
LD_LIBRARY_PATH to for running the produced executable.
I hope this helps.
Andrew
On S
Hi Charitha,
If I were you, I would try to run cmake in the following way:
CXXFLAGS="-fexceptions" cmake ...
Regards,Andrew
On Wednesday, 7 February 2018, 4:19:31 am GMT+8, Charitha Saumya
wrote:
Hi all,
I want use z3 C++ APIs in a C++ source file I have placed inside
klee/lib/Solver
Hi Norlina,
Yes, generally it is possible for KLEE to generate string inputs, including a
program written in a particular language.For the space program that you are
testing, I guess that you would need to provide a symbolic file as an input
program.KLEE will then replace the content of the file
Hi Qingyang,
I think what you want to know is how to solve array constraints, e.g., x > a[x]
in your example. You can have a look at the following paper on STP, which
is one of the backend solvers KLEE uses:
https://ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-STP-CAV.pdf
Section 3 discuss
Hi Daniel,
Following is several ways that I know how a symbolic variable gets its name, but
none of them depends on debug information.
1. A variable is named by the user via klee_make_symbolic() API,
however in a loop, indexed variants of the same variable may be produced.
You can have a
Hi Alberto,
Perhaps you can simply dump the expression before the call to bindLocal().
That is, if you see bindLocal() call of the form:
bindLocal(kinst, state, expr);
you can do
expr->dump();
immediately after/before the call to see the expression being locally bound.
I hope this helps.
Bes
Hi Charitha,
I think you would need to do the modification in Executor::fork().
You would notice within that function there is the following three lines:
solver->setTimeout(timeout);
bool success = solver->evaluate(current, condition, res);
solver->setTimeout(0);
I would try to replace those wi
Hi Boris,
The select instruction can typically be handled by an SMT solver primitive,
usually called "ite",
hence it seems advantageous in terms of efficiency not to fork a new branch for
it.
It looks benign enough to remove the whole statement
pm3.add(createCFGSimplificationPass());
in KModul
Hi Sang,
I don't think that is possible in KLEE since firstly, given concrete inputsit
will likely simplify the constraints into a constant (true/false). Secondly,it
does not collect the constraints into the path condition whenever it candecide
that a branch can only go one way, which is to alw
Hi Ridwan,
I think you can do this using klee_print_expr() without modifying KLEE.For
example (from [klee-dev] question about klee_print_expr):
|
|
| |
[klee-dev] question about klee_print_expr
|
|
|
#include
int main(int arc, char **argv)
{
int a,b;
klee_make_symbol
Hi Sanghu,
You don't seem to be using klee-replay here. Otherwise, instead of invoking
a.out
you would have invoked klee-replay, with a.out as its argument.
Moreover, you can't just expect klee-replay to work on a single file containing
all the
ktest files by simple appending. I don't think thi
10:30 AM, Andrew Santosa wrote:
> Hi Sanghu,
>
> You don't seem to be using klee-replay here. Otherwise, instead of invoking
> a.out
> you would have invoked klee-replay, with a.out as its argument.
>
> Moreover, you can't just expect klee-replay to work on a sing
Hi Sang,
I urgently need a tool like you mentioned, so I wrote one myself within
KLEEsource tree. You can find the source as tools/gen-bout.cpp in the gen-bout
branchof my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout
I don't exactly know the answer to your question. For normal
un 22, 2018 at 9:32 PM, Andrew Santosa wrote:
> Hi Sang,
>
> I urgently need a tool like you mentioned, so I wrote one myself within KLEE
> source tree. You can find the source as tools/gen-bout.cpp in the gen-bout
> branch
> of my KLEE fork: https://github.com/domainexpert/klee/tr
Hi Norlina,
You first need to download and unpack Coreutils 6.11 in the following way:
wget http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gztar zxvf
coreutils-6.11.tar.gzcd coreutils-6.11
Only after executing the above commands you can proceed with mkdir:
mkdir obj-gcovcd obj-gcov../configu
Hi Alberto,
Thank you for describing your problem. I had submitted this PR some while ago:
https://github.com/klee/klee/pull/956
Basically I would use gen-bout implemented in the PR to create a ktest file
using concrete inputs, then use the ktest file as a seed. In this way, all
inputs will be
th a new searcher in order to 'execute,' queries at
runtime on the code.
Thanks a lot!
Alberto
On Mon, Oct 15, 2018, 01:19 Andrew Santosa wrote:
Hi Alberto,
Thank you for describing your problem. I had submitted this PR some while ago:
https://github.com/klee/klee/pull/956
Basically I wou
Hi Sang,
Yes -only-replay-seed could be the option to use instead of -only-seed, but you
don't need to re-run KLEE for each seed though. There's -seed-out-dir option
where you can specify a directory of seeds.
Best, Andrew
Sent from Yahoo Mail on Android
On Tue, Oct 16, 2018 at 7:50 AM,
Hi Alberto,
Please keep in mind that, although KLEE still tries to follow the seed's path,
the state it maintains is no longerthe concrete state, but the symbolic state.
So, the symbolic file A no longer contains a concrete RGB value at
coordinate(1, 1), but instead a symbolic value. By looking
and only one
path with symbolic data. This path should be generated with a concrete file.
This is I'm working on a searcher but I cannot do it properly for now.
Thanks
On Sat, Oct 20, 2018, 09:58 Andrew Santosa wrote:
Hi Alberto,
Please keep in mind that, although KLEE still tries to follo
47 matches
Mail list logo
