Re: [klee-dev] KLEE fork failed
On 27 March 2018 at 08:45, Sicco Verwer wrote: > > Dear all, > > I am trying to run KLEE in my class on concolic execution. Some student get > the following message after which KLEE quits, and I cannot seem to find the > cause, or solution. Does anyone know? Just to be explicitly clear. KLEE does not use concolic execution. KLEE implements classical symbolic execution where by it stores every path (and related state) in memory at the same time. This gives KLEE a global view of feasible paths in the programs but this approach can quickly lead to memory exhaustion. The issues you're seeing points at memory exhaustion which is one of the limitations of classical symbolic execution. Concolic execution side steps this by not storing the execution state of every path it discovers. You could try using the Z3 solver instead of STP if you want to avoid forking which might reduce some of the memory overhead. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Missing floor, modf and pow
Hi, On 3 March 2018 at 07:29, Alberto Barbaro wrote: > Hi all, > few months ago I was trying to understand how to test pngpixel via KLEE and > after few suggestion I was able to do it. > > I have just one more question. When I run KLEE I have this output: > > klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee > --libc=uclibc --posix-runtime pngpixel.bc 1 1 file.png > KLEE: NOTE: Using klee-uclibc : > /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca > KLEE: NOTE: Using model: > /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: output directory is > "/home/klee/targets/libpng-1.6.34/contrib/examples/klee-out-3" > KLEE: Using STP solver backend > KLEE: WARNING: undefined reference to function: floor > KLEE: WARNING: undefined reference to function: modf > KLEE: WARNING: undefined reference to function: pow > KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 92453184) at > /home/klee/klee_src/runtime/POSIX/fd.c:1044 > KLEE: WARNING ONCE: calling __user_main with extra arguments. > KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. > Using alignment of 8. > KLEE: WARNING ONCE: _setjmp: ignoring > > KLEE: done: total instructions = 106954 > KLEE: done: completed paths = 1 > KLEE: done: generated tests = 1 > klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ > > Can I "ignore" the fact that floor, modf and pow are missing because I'm > using uclibc? You can ignore the warning as long as the code you run doesn't call these with symbolic arguments. You'll see a warning if this happens because KLEE has to concretize the arguments and call the function via LLVM's JIT. In your case it doesn't look like you're passing any symbolic data to the application so you're running concretely so you should be fine. If any function gets called that's external (i.e. is not in the LLVM bitcode, like floor is in your example) KLEE will emit a message telling you its calling an external. The reason these functions aren't available is because KLEE doesn't link in Uclibc's C library. My fork of KLEE that supports symbolic floating-point arithmetic [1] does link this library. [1] https://github.com/srg-imperial/klee-float ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: error loading program 'pallin.c': Invalid bitcode signature
On 12 October 2017 at 08:49, Chengyu Zhang wrote: > Maybe you should run KLEE on .bc file generated by Clang rather than .c > file. To add to that you can't use "Apple Clang". You need to use a version of Clang that uses the same version of LLVM that KLEE was built with. In your case your version of KLEE uses LLVM 3.4 so you need to use Clang 3.4. At a glance it looks like you're using Docker to run KLEE. So you should probably invoke Clang inside the Docker container to build your code. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Current status of Z3 with FP-support
Hi, On 12 June 2017 at 13:12, Henrik Tjäder wrote: > Hi, > > Reading (1) and quoting Dan Liew, > > "I'm aware of klee-fp. However I should warn you (so that you don't > waste time doing this) that I (and another research institution) have > already extended KLEE with floating point support using Z3. We intend > to open source our implementations in the very near future." > > I am curious about the state of this ongoing work, and if there are any > need for testers or such. Just to note my fork of KLEE that supports floating point arithmetic is now open source [1]. You can build it is as normal but you * Have to build using CMake * You have to build with Z3 support and use that as the constraint solver. The intention is to eventually upstream this implementation along with the implementation of one of my collaborators [2]. It will be several months before this happens though. Have fun, Dan [1] https://github.com/srg-imperial/klee-float [2] https://github.com/danielschemmel/klee-z3float-aachen ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Issue regarding pasting code in klee directory
On 11 September 2017 at 17:11, Mahinder.Shrivas wrote: > Hi, > > I am facing bit problem, I am not able to paste the code for maze example > (i.e. maze.c in Tutorial 3) in klee directory. I am trying to paste it in > example folder and then trying to run it through docker. I have manually > pasted maze.c in “/home/klee/klee_src/examples/maze” in my local system but > when I am trying to see it from the terminal. I am not getting any file > inside it. Can anyone please help. Thanks in advance. There's a note in our docs [1] about this. ``` You may want files on your native filesystem available in the container. By default the host filesystem is not visible inside the container. You can use the --volume= option to docker run to mount directories on the host filesystem into the container. ``` There also other ways of getting files outside the container into it (e.g. `docker cp` command [2]). Using volume mounts is by far the easiest though. See [3]. It sounds to me like you may be very new to using Docker. While we can try our best to help you out, I suggest you read some of the existing Docker documentation (e.g. [4]) to get to grips with some of the fundamentals of Docker before asking the mailing list. [1] http://klee.github.io/docker/ [2] https://docs.docker.com/engine/reference/commandline/cp/ [3] https://docs.docker.com/engine/admin/volumes/bind-mounts/ [4] https://docs.docker.com/engine/userguide/ HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Fwd: Request regarding downloading KLEE code
On 4 September 2017 at 11:20, Mahinder.Shrivas wrote: > Hi All, > > This is regarding KLEE code. I am trying to clone KLEE code through docker > by running this command (docker build -t klee/klee .) While doing that the > connection is getting refused. I tried many times but it is not letting me > clone KLEE source code. Please find the screenshot for your kind reference > and do let me know if you guys know the solution. Any kind of suggestion > would be appreciated. Thanks again. Sounds like networking is not setup correctly in your Docker container. Try passing `--network=host` to docker build. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee and overshift error
On 22 July 2017 at 16:49, Andrew Santosa wrote: > 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 being > shifted. Slight correction. KLEE will report an error if the shift width is greater than **or equal to** the bitwidth being shifted because at the LLVM IR level (and at the level of C) this is undefined behaviour. > > KLEE: ERROR: /klee/libqu/classic.c:108: overshift error > I would like to know what is the cause of this error? Is it related to the > choice of the symbolic variable? Without using KLEE the benchmark works If you really don't care about the undefined behaviour you can remove the check by passing `-check-overshift=0` to klee. You should be careful though. Having undefined behaviour in your program may cause you problems. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Using KLEE in LLVM Pass
Hi,
On 19 July 2017 at 13:55, Khaled Yakdan wrote:
> Hi,
>
> I am working on an LLVM analysis pass where I need to reason about whether
> two values are equal. I am wondering if KLEE can be used for this purpose.
> One idea would be to symbolically execute the given function and then ask
> the solver if two expressions of interest are actually equal. Can KLEE be
> used as previously described? If yes, I would be grateful if you can provide
> some hints how this can be realized.
Unfortunately at this point in time only certain parts of KLEE can
used as a library but it's header layout is a complete mess.
An attempt was made to fix this in [1] but this change was rejected.
It's not impossible to do but you may find the current state of KLEE
makes this a challenge.
You might want to consider whether the reasoning you wish to perform
can be done directly using an SMT solver directly (e.g. Z3) can solve
your problem.
You could also consider doing what the Souper project [2] does. It
uses's KLEE's Expression language which has a close resemblance to
some parts of LLVM IR
and constructs queries and dispatches them to an external solver.
However if you want to go the KLEE route you would need to construct
LLVM IR that effectively does the following
```
// Functions to check
extern int foo0(int arg0);
extern int foo1(int arg0);
int main() {
int branch = klee_range(0, 2); // symbolic variable constrained to be
in range [0,1]
int arg0 = 0;
klee_make_symbolic(&arg0, sizeof(arg0), "arg0");
int result0 = 0;
int result1 = 0;
switch (branch) {
case 0:
// First order
result0 = foo0(arg0);
result1 = foo1(arg1);
break;
case 1:
// Second order
result1 = foo1(arg1);
result0 = foo0(arg0);
break;
}
// Check output equivalence
// Equivalence is proved if and only the abort()
// below is never called and path exploration is
// exhaustive
if (result0 != result1)
abort();
}
```
This is essentially a "driver" that sets up the symbolic arguments to
the functions (in the example `foo0()` and `foo1()`) and calls them
appropriately
and checks whether or not they are equivalent.
You might be wondering why the `branch` variable is created (which
itself is symbolic) and then is used to control the order `foo0()` and
`foo1()` are called in.
The reason for this is a bit a subtle. If we call `foo0()` first it
could be the case that for some inputs the function gets terminated
(e.g. `if (arg0 == 0) abort();`).
That would mean that for all paths leaving `foo0()` some values for
`arg0` would be disallowed when executing `foo1()`, even if `foo1()`
does something special
for those values. This means we wouldn't be fully confirming
equivalence for all inputs so it is necessary to also consider calling
the `foo1()` and `foo2()` in the other order.
[1] https://github.com/klee/klee/pull/478
[2] https://github.com/google/souper
HTH,
Dan
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE on ASAN-enabled binaries
On 19 June 2017 at 15:48, Alexandre Adamski wrote: > Hello there, > > I was wondering: it is possible to use KLEE on a binary compiled with > AddressSanitizer? Obviously using WLLVM to get the LLVM IR. This won't work properly I'm afraid. When compiling with ASan a bunch of extra calls are emitted to the sanitizer runtime libraries that are part of project compiler-rt. KLEE doesn't have an implementation for these so attempting to call these from within KLEE will fail. Even if the runtime issue was fixed there's also the problem of ASan's shadow memory. I'm not sure how well KLEE would cope with having this. I have to ask though. Why would you want to use KLEE on "ASan-ified" LLVM IR? KLEE already detects the kind of memory errors that ASan can find. On they other using like UBSan makes sense because KLEE can't catch all the issues UBSan can catch. Support for a small subset of UBSan runtime calls is already present in KLEE and more can be easily added. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] failed external call: fgets
On 16 June 2017 at 17:05, Nourah mmm wrote: > Hi, > > I try to run KLEE on cutcp benchmark from (Parboil Benchmarks). The > benchmark consists from the following program: main.c parboil.c readatom.c > cutcpu.c excl.c output.c > > First I compile it with the following command: > myclang -I /home/klee/klee_src/include -emit-llvm -c -g main.c parboil.c > readatom.c cutcpu.c excl.c output.c > > Then, I run KLEE with this command: > myklee --posix-runtime --libc=uclibc --link-llvm-lib=parboil.bc > --link-llvm-lib=cutcpu.bc --link-llvm-lib=excl.bc --link-llvm-lib=output.bc > --link-llvm-lib=readatom.bc ./main.bc -i > /home/naloboud/parboil/datasets/cutcp/small/input/watbox.sl40.pqr > > However I get this error: > KLEE: NOTE: Using model: > /home//klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: Linking in library: parboil.bc. > > KLEE: Linking in library: cutcpu.bc. > > KLEE: Linking in library: excl.bc. > > KLEE: Linking in library: output.bc. > > KLEE: Linking in library: readatom.bc. I think the problem is the way you are linking. The `--link-llvm-lib` flag links after klee-uclibc links in. The code that is failing probably comes from `readatom.bc`. This code is calling `fgets()` but because klee-uclibc has already been linked in (note we do "static style" linking so only the parts of klee-uclibc that are needs get linked in) it's too late to get a definition. Arguably this a bug in the `--link-llvm-lib` flag but I'm not particularly interested in fixing it because I voted against adding this feature when it was first introduced. What I'd recommend doing is using wllvm (https://github.com/travitch/whole-program-llvm) to build your program and tell the build system to link everything statically. If you do this everything should be linked together properly. Alternatively if you know which `bc` files you want to link together just use the `llvm-link` tool to link them all together before you give them to KLEE. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Current status of Z3 with FP-support
Hi, On 12 June 2017 at 13:12, Henrik Tjäder wrote: > Hi, > > Reading (1) and quoting Dan Liew, > > "I'm aware of klee-fp. However I should warn you (so that you don't > waste time doing this) that I (and another research institution) have > already extended KLEE with floating point support using Z3. We intend > to open source our implementations in the very near future." > > I am curious about the state of this ongoing work, and if there are any > need for testers or such. The implementation that we have currently will be open sourced once we have some published work using it. However it is our intention to upstream this work to mainline KLEE. I've started trying upstreaming some of the work that came from adding floating point support [1][2][3] but not the actual support it self yet. There's a bunch of stuff I want to get in mainline KLEE before I add the floating point support. At this point I'm impeded by KLEE's overly conservative review process. Given that I have very little time is left to complete my PhD there is a good chance that this work will never upstreamed (at least by me anyway). However the implementation (that is a fork of mainline KLEE) will definitely be open sourced in the next few months and I would certainly like testers :) [1] https://github.com/klee/klee/pull/657 [2] https://github.com/klee/klee/pull/658 [3] https://github.com/klee/klee/pull/629 Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Getting path formula in dimacs format
Hi, On 11 June 2017 at 17:20, Awanish wrote: > Hi, > > I want to get/convert path constraint into dimacs/SAT format. Is there any > way to convert in the desired form? No such feature exists in KLEE itself but I think it should still be possible to get queries in the DIMACS format. I had a quick grep of the STP code and there is some that suggests that it can print DIMACS but this not exposed by its API. So I'm guessing that you need to collect the queries from KLEE in some other format (i.e. CVC or SMT-LIBv2) and then use STP's `--output-CNF` flag on those queries. Alternatively it would be possible to have KLEE get the DIMACS directly if some modifications were made to Z3. I also grepped through Z3's codebase quickly and it does have the capability to print DIMACS but this is not exposed via their C API. If you ask the Z3 developers to expose the ability to get DIMACS as a string in their C API then it would be possible to teach KLEE to call this API. However Z3 doesn't always invoke its SAT solver (it sometimes uses its more general SMT solver) so there will be cases where DIMACS is simply not available. My guess is the right way to do this is have a C function that works on a `Z3_goal` and only gives output if the goal is in CNF form already. If that's something you want to do then open an issue on the Z3 issue tracker on GitHub stating very clearly what you would like. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE behaviour with function call to uclibc
Hi, On 28 May 2017 at 00:55, Shehbaz Jaffer wrote: > Hi Dan, > > > Thank you for your reply. However, I am struggling with how function not > defined in the programs bitcode (like getopt_long function) gets emulated by > KLEE. Please allow me to explain the steps and where I am facing issues in > more detail: getopt_long is part of the C library. In KLEE's case the definition can be found in klee-uclibc. If you don't link in klee-uclibc (i.e. with `-libc=uclibc`) then the `getopt_long()` won't get linked into the final LLVM IR that gets executed. Side note KLEE has the ability to call external functions (i.e. those not defined in LLVM IR) but JIT'ing calls to that function but doing this requires that KLEE concretize all arguments to the function. When running KLEE take a look at the `assembly.ll` file in the klee output directory (e.g. `klee-last`). That file shows the LLVM IR that KLEE actually executes. This IR contains the result of KLEE linking in whatever libraries it decided to link in (e.g. klee-uclibc) and the result of then applying any transformation passes to the IR. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE behaviour with function call to uclibc
On 27 May 2017 at 01:36, Shehbaz Jaffer wrote: > Hello KLEE developers, > > I am trying to understand how KLEE emulates environment variables. In > particular, how do functions like getopt_long get executed with KLEE, when we > give --sym-arg as an argument. getopt_long is found in unistd.h, and is > available in uclibc. For a coreutils file like groups.c where the following > line is encountered: > > while ((optc = getopt_long (argc, argv, "", longopts, NULL)) != -1) > > how would KLEE generate different inputs? for simplicity, consider the case > where we use --sym-arg 1 10 as a command line argument which leads to argv[1] > becoming a symbolic buffer of size 10, if my understanding is correct, when > getopt_long is called, one of the two things can happen: > > 1) argv[1] is declared as a symbolic buffer, we explore all paths of > getopt_long code in uclibc library, so all different if's / elses in > getopt_long code will get forked and execute to give different optc values. > 2) getopt_long is skipped, optc variable is made symbolic, and the main > function in groups.c treats optc as symbolic value. on any successive if/else > condition in groups.c containing optc, a new state is forked with new value > of optc. Take a look at the `klee_init_env()` function [1]. When KLEE is called with --posix-runtime the program's `main()` is rewritten to call `klee_init_env()` at the beginning and change `argc` and `argv`. The `klee_init_env()` function introduces symbolic arguments if requested. From that point onwards execution of the program just proceeds as normal so `getopt_long()` will just be interpreted by KLEE just like any other function. [1] https://github.com/klee/klee/blob/bec4ceafe412a08de303678581e07451a1399e1f/runtime/POSIX/klee_init_env.c#L85 ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] One phenomenon after the execution using klee
Hi, On 10 May 2017 at 03:55, 曾杰 wrote: > Hi, all, > If you write test.c with an error out of bound and test2.c with an > error assertion failed. > You first symbolically execution test.bc(using clang to generate), and > then the test2.c. you will find the contents in klee-last are different from > the latest generated contents in klee-out-n. > klee-last will have an xxx.assert.err and an xxx.ptr.err both. But the > latest generate contents in klee-out-n which is because of the symbolic > execution of test2.bc only have the xxx.assertion.err. > It is just one phenomenon which disobey the rule that klee-last points > to the latest directory klee-out-n and not an error. I just present it. This sounds like a bug but I find your description difficult to read. Could please open an issue on our issue tracker [1] with precise reproduction steps (i.e. the commands and source files to reproduce the issue). [1] https://github.com/klee/klee/issues ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Klee-uclibc.bca Error when Running Coreutils
On 7 May 2017 at 06:27, Zhiyi Zhang wrote: > Hi, > > > I have installed klee on Ubuntu(version, 14.04 64 bit) with LLVM-3.4,and I > successfully run the tutorial 1 & 2. However, I met a problem when I run > Coreutils 6.11. I used the same options which are showed on "OSDI'08 > Coreutils Experiments", and klee showed an error message as following, > > > > KLEE: ERROR: Link with library > /home/jcklee/jc/jcnewklee/klee/Release+Asserts/lib/klee-uclibc.bca failed: > Invalid valueLoading module failed : Invalid value > > > Could you give me some suggestions to solve this problem? Thank you very > much. It is likely that you incorrectly compiled klee-uclibc. You need to ensure that you compile it using a Clang version that matches the LLVM version (in your case that is Clang 3.4 and LLVM 3.4) that you link KLEE against. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] an error occurs when building klee from source against LLVM 3.4
On 2 May 2017 at 04:32, 曾杰 wrote: > Hi, Excuse me, i have a question which i cannot solve.I build KLEE using the > approach below, > > Build from source against LLVM 3.4: this is the current recommended version. > > > and i have complete all steps until i run make command in Klee_build_dir > directory, but the following errors occur. Hope for your help! This is an RTTI issue. See https://github.com/klee/klee/issues/508 I have documentation up for review to clarify how to handle this at https://github.com/klee/klee.github.io/pull/81 ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE "make" errors with LLVM-3.4.2
On 13 April 2017 at 13:11, Zhiyi Zhang wrote: > > Hi, > > I tried building KLEE on Ubuntu 16.04 LTS. I have built LLVM-3.4.2 (put Clang > into /llvm/tools,then cmake llvm )and STP-2.1.2. After I configured KLEE with > "cmake", > > cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON > -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=../klee-uclibc > -DENABLE_SYSTEM_TESTS=ON -DENABLE_UNIT_TESTS=OFF ../klee > > > I built KLEE with "make", but there were some errors about "kleaver". > > "Linking CXX executable ../../bin/kleaver > > ... > > ../../lib/libkleeSupport.a(CompressionStream.cpp.o):(.rodata._ZTIN4klee21compressed_fd_ostreamE[_ZTIN4klee21compressed_fd_ostreamE]+0x10): > undefined reference to `typeinfo for llvm::raw_ostream' > > collect2: error: ld returned 1 exit status > > tools/kleaver/CMakeFiles/kleaver.dir/build.make:105: recipe for target > 'bin/kleaver' failed > > make[2]: *** [bin/kleaver] Error 1 > > CMakeFiles/Makefile2:688: recipe for target > 'tools/kleaver/CMakeFiles/kleaver.dir/all' failed > > make[1]: *** [tools/kleaver/CMakeFiles/kleaver.dir/all] Error 2 > > Makefile:127: recipe for target 'all' failed > > make: *** [all] Error 2" > The linking errors are related to RTTI (run time type information). This is because you built LLVM 3.4 CMake and the built `llvm-config` binary has a bug where it doesn't show the `-fno-rtti` flag. You have two options to fix this 1. Use the LLVM build that you produced using CMake but reconfigure KLEE by forcing the `-fno-rtti` flag. You will need to make a new build directory when you do this. Something like this ``` CFLAGS="-fno-rtti" CXXFLAGS="-fno-rtti" cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=../klee-uclibc -DENABLE_SYSTEM_TESTS=ON -DENABLE_UNIT_TESTS=OFF ../klee ``` 2. Rebuild LLVM using its autoconf/Makefile build system. This issue seem to keep appearing so we should improve our documentation to make it explicit that people should avoid building LLVM 3.4 using CMake. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Add new solver like dreal to backend of klee
Hi, On 9 April 2017 at 04:21, Cx Qingyang wrote: > Thanks very much.Actually i need to add Z3 to the backend of klee-fp which > is an extension of klee.I think the method is similar.But i still confused > about the structure of klee,like the use of metaSMT.Z3 has been directly add > to klee without metaSMT,why not use the metaSMT? IIRC metaSMT doesn't support floating point constraints. I have not confirmed this but I prefer to work with Z3 directly anyway. Z3 has a very powerful API that allows customising many internal options and allows custom tactics to be built. I'm aware of klee-fp. However I should warn you (so that you don't waste time doing this) that I (and another research institution) have already extended KLEE with floating point support using Z3. We intend to open source our implementations in the very near future. > And is there a way to fast > understand klee,besides directly reading the source code?Looking forward to > your reply. "Fast" really depends on what sort of person you are. I find walking through an execution in a debugger like gdb very helpful. Also. Please don't forget to CC the mailing list. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Converting KQuery numbers to signed integers
Hi, On 7 April 2017 at 14:19, Papapanagiotakis-Bousy, Iason wrote: > Hello KLEE community, > > > > I was wondering how would I convert the numbers appearing in KQuery to > signed integers. > > Could you point me to the right direction on how to do that? Could you be more specific. In what context do you want to do this? Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] LLVM directory does not exist/ not found
Hi, On 28 March 2017 at 13:50, Shaikha Al-Khuder wrote: > Hi there, > > I keep getting this type of error when trying to “make” within > klee_build_dir. > At first I tried trouble shooting through “sudo nano” each .h/.cpp file that > contains the non-existing file directory and modifying the line “#include” > to the correct path of the file, but this has Benn the case for the last two > days. That is not the right way to fix the problem you're having. > I felt that I misplaced the llvm-3.4 directory ( it was inside > usr/lib/llvm-3.4/..) so I copied it into the “Klee” folder but still gives > the same error type when trying the command build. > I tried moving the llvm-3.4 directory to where the .h or .cpp file but no > use. > > Any idea how to get a successful “make’ command? > This is part of the steps in this page: Klee.github.io/build-llvm34/ Your description of the problem is not very precise so it's hard to know what the problem is. Did you actually do the configure step (i.e. run the `cmake` command with the appropriate arguments)? If something is wrong with your LLVM installation the configure step should have failed. Given the problems you are having I recommend that you just use KLEE's Docker image because it contain a correctly setup environment a pre-built version of KLEE. It also contains the sources and a build directory so you can modify KLEE inside the container if you need to. Read http://klee.github.io/docker/ for information on how to do this. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] find_llvm.cmake has problems in llvm version like 3.4svn
On 28 March 2017 at 14:51, 王悦 wrote: > Hi, all: > Recently, I was trying to compile KLEE with llvm-3.4. I came into a > problem that klee fail to recognize llvm version. When I looked into > find_llvm.cmake, I think I found the reason. > When try to match llvm version with x.y pattern on line 89 in file > cmake/find_llvm.cmake, the regex "set(_llvm_version_regex > "^([0-9]+)\\.([0-9]+)$")" would fail to match llvm version like 3.4svn. As a > result, I think the regex need to be modified to "set(_llvm_version_regex > "^([0-9]+)\\.([0-9]+)(svn)?$")". > I'll appreciate a lot if anyone could tell me if this modification is > right. > Thank you a lot. Thanks for the information. You can follow this problem on KLEE's issue tracker at https://github.com/klee/klee/issues/633 Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding initial state as a constraint
Hi, On 2 March 2017 at 02:06, Chelsea Metcalf wrote: > > Hi, > > I am trying to add the initial state as a constraint, but it is not taking > effect. The above does not make sense to me. Please clarify your question. Perhaps with a code example to illustrate what you are trying to do. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] One question about external dispatcher
On 27 January 2017 at 04:18, Qiuping Yi wrote:
> Dear all,
>
> I encountered a strange problem when testing the next code snippet:
>
> 1 if (pw = getpwuid(getuid()) == NULL)
> 2 return ;
>
> 3 .. = pw->pw_dir;
Please use the correct mailing list (klee-dev@imperial.ac.uk) instead
of the old klee-...@keeda.stanford.edu mailing list.
It would be better if you provided a small complete example. Like this.
```
#include
#include
#include
#include
#include
int main(int arc, char** argv) {
struct passwd* pw;
uid_t uid = getuid();
printf("uid is %d\n", uid);
if (pw = getpwuid(getuid()) == NULL) {
printf("Failed\n");
return 1;
}
assert(pw && "pw cannot be NULL");
char* pw_dir = pw->pw_dir;
printf("pw_dir: %s\n", pw_dir);
return 0;
}
```
Your code is wrong.
if (pw = getpwuid(getuid()) == NULL)
is doing this
if ( pw = ( getpwuid(getuid()) == NULL )
so a pointer is returned by `getpwuid()` and then we compare with NULL
which is false so then `pw` gets assigned the value zero.
However once I fix your code to
if ((pw = getpwuid(getuid())) == NULL) {
then I can reproduce the problem if I just run `klee program.bc`
I suspect it's to do with the fact `getpwuid()` returns a pointer to
"real memory" which does not point to anything in KLEE's own model of
the memory (i.e. the address space of the program under).
To fix this you need not call `getpwuid()` as an external function but
instead call it from klee-uclibc so that it can be symbolically
executed.
If you run
```
klee -libc=uclibc program.bc
```
no out of bounds access is reported.
HTH,
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Can klee generate a combined path expression to reach a particular statement?
Hi,
On 27 January 2017 at 22:20, Cong Yan wrote:
> Hi,
>
> Is klee able to generate an expression combining different paths? For
> example,
>
> if (a)
> stmt1;
> else
> stmt2;
> stmt3;
The answer is yes and no. It is all dependent on how the C program
above is translated into LLVM IR
For Clang if the code is not optimized these would be broken into
basic blocks with a branch instruction. It that case KLEE
will fork and generate two paths that reach `stmt3`.
To see this
run
clang -S -emit-llvm x.c -o -
on
```
#include
int main() {
int a = 0;
if (a) {
a = 1;
}
else {
a = 2;
}
printf("done %d\n", a);
return 0;
}
```
You'll see something like
```
; Function Attrs: nounwind uwtable
define i32 @main() #0 {
%1 = alloca i32, align 4
%2 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 0, i32* %2, align 4
%3 = load i32, i32* %2, align 4
%4 = icmp ne i32 %3, 0
br i1 %4, label %5, label %6
; :5: ; preds = %0
store i32 1, i32* %2, align 4
br label %7
; :6: ; preds = %0
store i32 2, i32* %2, align 4
br label %7
; :7: ; preds = %6, %5
%8 = load i32, i32* %2, align 4
%9 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x
i8], [9 x i8]* @.str, i32 0, i32 0), i32 %8)
ret i32 0
}
```
Note the branching (`br` instruction). KLEE will fork if more than one
path from the branch is feasible.
However if certain passes are run the branching can be removed.
clang -S -emit-llvm x.c -o - | opt -mem2reg -simplifycfg -S
You'll see output like this.
```
...
define i32 @main() #0 {
%1 = icmp ne i32 0, 0
%. = select i1 %1, i32 1, i32 2
%2 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x
i8], [9 x i8]* @.str, i32 0, i32 0), i32 %.)
ret i32 0
}
...
```
You can see there are no branches here and there is a `select`
instruction instead.
This is a special case though. If you put code that has side effects
in the `if` or `else` blocks then LLVM will not
be able to simplify the control flow graph to remove the branches.
Instead you may want to experiment with the `klee_merge()` instrinsic
with I believe is supposed to do state merging.
Note that this instrinsic is experimental and I have no idea if it
still (did it ever?) works.
HTH,
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] IMPORTANT: Build system changes
Hi All, For those using KLEE right now there are two important build system changes. ## Testing target names Testing target names have changed For the autoconf build system * the `check` target has been renamed `systemtests` * A new `check` target has been added that runs both the `systemtests` and `unittests` targets. ## New Build system KLEE has a new CMake build system. It's been in master for a while now but documentation for building with it has just landed at http://klee.github.io/build-llvm34/ Using CMake gives a few new nice features like: * Building with Ninja (super fast incremental builds :)) * Easier interaction with an IDE by using a CMake IDE generator (e.g. `-G "Eclipse CD4 - Ninja"`) * Build no longer dependent on LLVM source tree. The build should build against an installed LLVM without problems. * When testing if the `FileCheck` and `not` tools are not available the build system will download the sources and build them as part of KLEE's build so testing can be done. * Building the runtime is now decoupled from the main build by invoking a separate build system that builds the runtime. This avoids problems we had in the past where compiler flags for the host compiler ended up being used with the bitcode compiler. The new build system also supports building against LLVM 2.9 although this is not documented because I want to move people away from using that version of LLVM. You are advised to switch to the new build system when possible because the old build system will be deprecated (eventually) and eventually removed. If you hit bugs in the build system please report them on KLEE's issue tracker. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Add new solver like dreal to backend of klee
On 10 January 2017 at 18:04, Cx Qingyang wrote: > Hi,i want to add some solver like dreal to the backend of klee,could you > give some advise? A Z3 solver backend was added fairly recently. You should take a look at that as an example of how to do it. Here's the PR that it was introduced https://github.com/klee/klee/pull/337 Note that the Z3 code has changed a little bit since this was committed so you should look at the master branch to see how things are done currently. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array
Hi Richard,
On 10 January 2017 at 00:19, Richard Rutledge wrote:
> Consider the following program:
>
> //-
> #include
> #include
>
> #define BUFFER_SIZE 16
>
> int main(int argc, char *argv[]) {
>
> char *buffer = malloc(BUFFER_SIZE);
> int index;
>
> klee_make_symbolic(buffer, BUFFER_SIZE, "buffer");
> klee_make_symbolic(&index, sizeof(index), "index");
>
> if (buffer[index] == '\0') {
> return 1;
> }
> return 0;
> }
>
> //-
>
> Given this program, klee generates approx 180 test cases (the actual number
> seems to vary). I understand from prior correspondence here that klee forks
> a path for each object which can be referenced. The forking occurs in
> Executor::executeMemoryOperation().
>
> My objective is to only generate inbounds values of buffer and index that
> induce each of the two paths through the program. My attempts to modify
> AddressSpace::resolve to only return the single desired memory object have
> so far been disappointing (i.e. abject failure).
>
> Any suggestions as to how I should proceed?
For this particular program you could add
```
klee_asume(index >= 0);
klee_assume(index < BUFFER_SIZE);
```
before doing any indexing.
If you want KLEE to always be in bounds you'll have to modify KLEE. It
sounds like you're looking roughly in the right area but this is a
part of the code I've not looked at in detail.
Looking at a glance what you need to change is
`Executor::executeMemoryOperation()`. You can see that it tries to
resolve to check if the pointer can resolve to a single memory object
(`AddressSpace::resolveOne()` then a few additional checks). If it
possible for the pointer to be out of bounds then an unbounded search
using `AddressSpace::resolve()` occurs. You can limit the bound by not
passing `0` as `maxResolutions` (arguably that should be a command
line option that defaults to 0). You could also just delete this code
and fork once and on the forked copy add the constraint that the
pointer doesn't resolve to the previously found object and then
terminate it as an error state for being out of bounds.
To be honest I find the code very hard to follow because the
ImmutableTree that stores the memory object is basically not documents
so I have no idea why the search in `AddressSpace::resolveOne()` is
done the way it is).
HTH,
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Running grep with klee
On 27 December 2016 at 13:11, Awanish wrote: > Hi Everyone, > > I compiled grep source code with both llvm2.9 and llvm-3.4, then try to run > on corresponding klee. In both the cases output is same but not the desired > one. LLVM ERROR: invalid argument to evalConstant(). > > Anyone have Idea what I am doing wrong in this? You're probably not doing anything wrong and this likely a bug in KLEE. I encountered this problem when working on my own fork of KLEE and it turned out the problem was vector constants. I have support for vector instructions in my fork of KLEE but I have not upstreamed the support yet for various reasons. I plan to upstream support once all my existing PRs get accepted. In your case you can see what is wrong by setting a break point on the call to `llvm::report_fatal_error()` in gdb and when hitting it running ``` call c->dump() ``` this will dump the LLVM constant that is not being handled. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Add a C++ file for klee's POSIX library
Hi, On 22 December 2016 at 05:37, Randall wrote: > Hello eyeryone. > > I have met a problem while adding a c++ library which uses > STL. So I get these error as follow: > > ... > > ... > > Unable to find size for global variable: _ZNSs4_Rep20_S_empty_rep_storageE > (use will result in out of bounds access) KLEE does not support C++ properly so it's not surprising that this doesn't work. What is happening is that your program references `std::basic_string, std::allocator >::_Rep::_S_empty_rep_storage` which is part of your compiler's C++ standard library (probably libstdc++ or libcxx). KLEE does not ship with a LLVM bitcode version of that library and so at present it will trigger an out of bounds access if an attempt is made to access it. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Is possible to mark a function as uninterpreted function?
Hi Javier,
On 14 December 2016 at 13:28, Javier Godoy wrote:
> Hi!
>
> Is possible to mark a function as uninterpreted function in Klee?
>
> Example i need:
>
>
> foo(int a)
> {
> if( boo(a) > 0)
> return 0;
> else
> return 1;
> }
>
> boo(int x) //I want to mark this as uninterpreted
> {
> ...
> return x;
> }
You could sort of model an uninterpreted function by having `boo`
return a fresh symbolic variable for every value of x it hasn't seen
before and the same symbolic variable for the corresponding value of x
previously seen.
This isn't really the right way to solve the problem. The STP solver
doesn't support uninterpreted functions however Z3 does and now that
we have first class Z3 support in KLEE this something that could be
implemented.
So the right way of going about this would be to
1. Introduce something like a `UFExprCall` expression and a
`UninterpretedFunction` type to KLEE's Expr language. KLEE's Expr
language is not typed so this might be a bit of challenge.
2. Teach the Z3Builder and other parts of KLEE's code how to handle
these new parts of KLEE's Expr language
3. Figure out a way to annotate functions in C such that KLEE at
runtime can construct the `UninterpretedFunction`s in the program. You
also need to make sure that the function cannot be inlined (there is
an LLVM function attribute that can do this) and that it has no body
(so it can't change any state).
This would be a lot of work but could be a valuable contribution to
KLEE because it would give us a new way model certain functions. E.g.
if we were executing `sin()` we could replace that with a `UF` if we
can statically prove that we never branch on the value that is
returned by `sin()`.
I do not have time to do this myself so if you are interested in this
feature you would have to implement it.
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Building constraints with Expr
Hi, > I am interested to build an Expr constraint given (in the simplest case) > something like “x == 0”, how would I do that? I presume that `x` refers to a symbolic variable here. KLEE's Expr language works on Arrays rather than plain variables so in order construct the expression you want you first need to find the Array corresponding to it and create the appropriate read from that Array. This usually a concatenation (ConcatExpr) of byte reads (ReadExpr). Take a look at `Executor::executeMakeSymbolic()` to see how the Array gets created and how it is stored. Once you have the `Array*` you can easily create the read (assuming you want to read the whole array from offset 0) using `Expr::createTempRead()`. Once you have that then you could do something like ``` ref tempRead = Expr::createTempRead(array, width); ref xEqualsZero = EqExpr::create(tempRead, ConstantExpr::alloc(0, width)); ``` > I have been looking at the code in include/klee/Expr.h but it doesn’t seem > intuitive to me how to proceed. > > > > My goal is to express some constraints with Expr and subsequently query the > solver with the getValue() function to check whether my constraints are > satisfiable on a particular state under evaluation. > > If you can think any other way of achieving that without building an Expr > please feel free to suggest it. Creating the appropriate the `Expr` is the only sane way to do this. Once you have the expression you will need to query the solver. BEWARE for historical reasons KLEE's solver interface generally works in terms of validity rather than satisfiability which is incredibly confusing so you need to carefully construct the query. For satisfiability you can try using solver->mayBeTrue(). Read `Solver.h` for more detail. Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Testing newest Coreutils
On 24 November 2016 at 03:57, Thuan Pham wrote:
> Hi,
> Has anyone tried to use KLEE to test newest version of Coreutils, say 8.25?
> I get stuck at the compilation step. Neither KLEE - LLVM2.9 nor KLEE -
> LLVM3.4 can compile Coreutils successfully.
>
> Here is the error message I got when I tried to compile Coreutils with
> klee-clang wrapper in KLEE - LLVM 3.4
>
> make src/make-prime-list
> make[1]: Entering directory `/home/ubuntu/subjects/coreutils/obj-llvm'
> CCLD src/make-prime-list
> llvm-link: Unknown command line argument '-fno-common'. Try:
> '/usr/lib/llvm-3.4/bin/llvm-link -help'
> llvm-link: Did you mean '-nvj-count'?
> llvm-link: Unknown command line argument '-fdiagnostics-show-option'. Try:
> '/usr/lib/llvm-3.4/bin/llvm-link -help'
> llvm-link: Did you mean '-disable-licm-promotion'?
> llvm-link: Unknown command line argument '-funit-at-a-time'. Try:
> '/usr/lib/llvm-3.4/bin/llvm-link -help'
> llvm-link: Did you mean '-unroll-runtime'?
> make[1]: *** [src/make-prime-list] Error 1
> make[1]: Leaving directory `/home/ubuntu/subjects/coreutils/obj-llvm'
> make: *** [../src/primes.h] Error 2
>
> And here is another error message I got with klee-gcc wrapper. This one I
> may understand the reason since llvm-ld does not exist in LLVM-3.4
>
> make src/make-prime-list
> make[1]: Entering directory `/home/ubuntu/subjects/coreutils/obj-llvm'
> CCLD src/make-prime-list
> Traceback (most recent call last):
> File "/home/ubuntu/KLEE-new/klee/scripts/klee-gcc", line 43, in
> main()
> File "/home/ubuntu/KLEE-new/klee/scripts/klee-gcc", line 39, in main
> os.execvp("llvm-ld", ["llvm-ld", "--disable-opt"] + linkArgs)
> File "/usr/lib/python2.7/os.py", line 344, in execvp
> _execvpe(file, args)
> File "/usr/lib/python2.7/os.py", line 380, in _execvpe
> func(fullname, *argrest)
> OSError: [Errno 2] No such file or directory
> make[1]: *** [src/make-prime-list] Error 1
> make[1]: Leaving directory `/home/ubuntu/subjects/coreutils/obj-llvm'
> make: *** [../src/primes.h] Error 2
>
> Can someone give me some suggestion to fix this compilation issue?
> Many thanks,
> Thuan
Don't use `klee-gcc`. Just use `wllvm`. There are some "work in
progress" instructions on how to use
it to build core utils at
https://github.com/klee/klee.github.io/pull/58 that will be merged
fairly soon.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Cannot compile Coreutils 6.10 inside KLEE Docker image
On 11 November 2016 at 08:41, Thuan Pham wrote: > FYI, the same issue happens while configuring Coreutils-6.11. > > On Fri, Nov 11, 2016 at 4:33 PM, Thuan Pham wrote: >> >> Dear all, >> I am trying to reproduce results of KLEE OSDI'08 paper on the Docker image >> provided on KLEE website. I downloaded Coreutils 6.10 and followed the >> tutorial at https://klee.github.io/tutorials/testing-coreutils/. However, I >> got an error when I run configure. It looks quite strange. >> >> >> config.status: executing po-directories commands >> config.status: creating po/POTFILES >> config.status: creating po/Makefile >> rm: cannot remove >> 'confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/confdir3/..': >> File name too long >> Using the latest docker image built three days ago I cannot reproduce the issue. ``` docker run --rm -ti klee/klee wget http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gz tar -xvf coreutils-6.11.tar.gz cd coreutils-6.11 mkdir obj-llvm ../configure --disable-nls CFLAGS="-g" ``` The configure succeeds for me. This issue has been asked before [1]. The issue appears to be underlying storage driver you are using (aufs) [2]. It has a rather low limit for the path length apparently. I suggest you try one of the following. * Mount a directory on your host into the container (i.e. a volume mount, e.g. `docker run --rm -ti -v /path/on/host:/home/klee/coreutils/`) and then build coreutils in there. This will bypass aufs and should avoid the issue. * Change storage driver (see [3]). I use overlay2. Note if you switch Docker storage driver you will need to nuke your `/var/lib/docker` directory. I advise not nuking it yourself and instead using this script [4] to do it. [1] https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01987.html [2] https://github.com/docker/docker/issues/1413 [3] https://docs.docker.com/engine/userguide/storagedriver/selectadriver/ [4] https://github.com/docker/docker/blob/master/contrib/nuke-graph-directory.sh ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Path constraints as equations of integers
Hi, On 1 November 2016 at 12:17, Papapanagiotakis-Bousy, Iason wrote: > Hello, > > > > I am a new user of KLEE, I was looking into symbolic execution in order to > extract the constraints of the input variables of a program for each path in > the code. > > Following the initial tutorials and searching on the web I’ve managed to get > both the KQuery and SMT2 formatted constraints generated by KLEE. > > > > I was wondering if there is a (new) capability of KLEE or an available > script/tool to generate the constraints as a systems of equations of > integers and not Bit Vectors as the default output in KQuery and SMT2 is. There is no option for this. KLEE analyses programs precisely so it has no use for printing expressions in an approximate form (i.e. using integers). You of course could do this yourself by either modifying KLEE's ExprSMTLIBPrinter class to print KLEE's expressions differently or write your own tool to parse QF_ABV queries and rewrite them as AUFNIRA queries. I don't know if there any existing tools to rewrite QF_ABV constraints to AUFNIRA. > While the output generated works fine with SMT solvers for the main purpose > of KLEE, it would help a lot if constraints could also be presented in a > human-friendly way. KLEE does have a few options to make the printed SMT-LIBv2 queries slightly easier to read (`-smtlib-human-readable`, `-smtlib-abbreviation-mode`, `-smtlib-display-constants`). These might help you. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path
Hi,
On 2 November 2016 at 15:52, wrote:
> Dear Klee developers,
>
>
> I am trying to use Klee for specification generation. To do that I need
> Klee's intermediate symbolic results. Specifically, I need the guards of
> each path in the program to be printed in their symbolic forms. For
> example, in the following program:
>
>
> get_sign(int a,char * sign)
>
> {
>
> if (a==0) *sign = 0;
>
> else if (a<0) *sign = -1;
>
> else *sign = 1;
>
> }
>
>
> I want,
>
>
> Path1 : (a==0)
>
> Path2 : (a<0)
>
> Path3: (a>0)
>
>
> as output and if it is possible to have the value of sign or the range of
> sign value for each path.
>
>
> Path1: (a==0)==> *sign = 0;
>
> Path2: (a<0)==> *sign = -1;
>
> Path3: (a>0)==> *sign = 1;
Whilst KLEE is running you can use the `klee_print_expr()` (see
`include/klee/klee.h`) to print the representation of an expression
for debugging purposes. E.g. in example you would do
```
klee_print_expr("ANYTHING", a)
```
However for more complicated programs you should just look at the
generated constraints for each path. You can use
the `-write-smt2s` to write the constraints for each path in SMT-LIBv2
format. You can also use `-write-pcs` to write the constraints
in KLEE's native constraint language.
HTH,
Dan
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
On 17 October 2016 at 22:52, Marko Dimjašević wrote: > Hi Dan, > > On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote: >> That is likely the cause error. This comes from a rather hacky >> implementation of a linker inside KLEE. >> >> I've mentioned this before that but this is something I'd like to >> remove from KLEE. I think that **all** linking (and optimization) >> should be done outside of KLEE using other tools because this would >> simplify KLEE's implementation and would be far cleaner. > > I don't agree with your root-cause reasoning in this case. I tried to > perform the same linking outside KLEE, i.e. with the llvm-link tool, yet > I got the same outcome. The "I'd like to remove..." is a side comment. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
Hi Marko On 16 October 2016 at 04:34, Marko Dimjašević wrote: > Hi again, > > On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote: > >> Earlier on this list there was a thread on what would be alternatives >> to >> KLEE-uClibc as the library implementation got rather old, which is >> true >> for its upstream as well, though to a lesser extent. Here I would like >> to ask how to add support for another C library implementation to >> KLEE. > > I started implementing support for the Musl C library in KLEE: > > https://github.com/mdimjasevic/klee/commit/367543b6 > > I'd like to use Musl in conjunction with the POSIX runtime. However, > when I run KLEE like this: > > $ klee -libc=musl -posix-runtime hostname.bc > > I get the following: > > KLEE: NOTE: Using musl : /home/marko/research/klee/Release > +Asserts/lib/musl.bca > KLEE: NOTE: Using model: /home/marko/research/klee/Release > +Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: ERROR: Link with library /home/marko/research/klee/Release > +Asserts/lib/libkleeRuntimePOSIX.bca failed: Linking globals named > 'access': symbol multiply defined! That is likely the cause error. This comes from a rather hacky implementation of a linker inside KLEE. I've mentioned this before that but this is something I'd like to remove from KLEE. I think that **all** linking (and optimization) should be done outside of KLEE using other tools because this would simplify KLEE's implementation and would be far cleaner. However we have to live with the horrible hacks that exist right now. To help you debug linking if you build KLEE as a debug build you can pass `-debug-only=klee_linker` to KLEE and that should dump a bunch more output. You can find the relevant code in `lib/Module/ModuleUtil.cpp`. > > How to avoid multiple symbol definitions? > > > If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version > of the library in KLEE (that's what the -libc=musl parameter fetches). I don't think "dynamically linked" makes any sense here. You just have LLVM bitcode. There is no "static" or "dynamic" here. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Linking C++ runtime
On 26 September 2016 at 20:56, Eric Laberge wrote:
> Hello!
>
> I am trying to get KLEE running a simple C++ app through Docker, but am
> obviously not doing it correctly. Anybody got it working?
>
> Here’s what I got:
>
> klee@77c9c1d55f4a:/tmp$ cat hello.cpp
> int main() {
> return 0;
> }
>
> klee@77c9c1d55f4a:/tmp$ clang++ -c hello.cpp -emit-llvm -g -o hello.bc
>
> klee@77c9c1d55f4a:/tmp$ klee
> -link-llvm-lib=/usr/lib/gcc/x86_64-linux-gnu/4.8/libstdc++.so hello.bc
> KLEE: Linking in library: /usr/lib/gcc/x86_64-linux-gnu/4.8/libstdc++.so.
>
> klee: /usr/lib/llvm-3.4/build/include/llvm/Support/Casting.h:97: static bool
> llvm::isa_impl_cl *>::doit(const From *) [To = llvm::object::ObjectFile, From = const
> llvm::object::Binary *]: Assertion `Val && "isa<> used on a null pointer"'
> failed.
> 0 klee0x00dd4432 llvm::sys::PrintStackTrace(_IO_FILE*) +
> 34
> 1 klee0x00dd4224
> 2 libpthread.so.0 0x2ac38e4ee330
> 3 libc.so.6 0x2ac390babc37 gsignal + 55
> 4 libc.so.6 0x2ac390baf028 abort + 328
> 5 libc.so.6 0x2ac390ba4bf6
> 6 libc.so.6 0x2ac390ba4ca2
> 7 klee0x005c8135 klee::linkWithLibrary(llvm::Module*,
> std::string const&) + 3925
> 8 klee0x00576c6c main + 5740
> 9 libc.so.6 0x2ac390b96f45 __libc_start_main + 245
> 10 klee0x005718d9
> Aborted
>
KLEE does not properly support running C++ code. Some things might
work but a lot of things don't.
The option you are using is meant for use on archives of LLVM bit code
files, not native dynamic libraries. I protested about the inclusion
of this option in KLEE because I believe that the majority of the
linking should be done outside of KLEE but I was over-ruled.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] segmentation fault
On 23 September 2016 at 23:43, Reza Ahmadi wrote: > Hi all, > > I tried to run a simple .cpp code using Klee. My code includes some > float-related operations. If I remove the float-related stuff, then, Klee is > successful in generating 3 test cases but fails if I include float things. > > My questions (sorry if too stupid, I am new to Klee): > > 1- Is Klee supposed to support C++ (or just C?). I know that Klee runs llvm > bytecodes, but I am just curious as there is no C++ sample code in Klee > tutorials. If C++ is supported, fully supported? to what extent? C++ code is not properly supported. Multiple features are missing including * Support for exceptions * Support for a symbolic C++ standard library > 2- Does Klee support float data type (or any floating point in general)? It > crashed totally if I include some float-related functions in my code > (function GetDiv in the below code). KLEE doesn't support symbolic floating point operations yet. I'm currently working on a fork of it that does but it isn't ready for public use yet. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Error in make check
On 18 September 2016 at 22:23, Awanish wrote: > Hi, > I configured klee with this command > ../configure --with-llvmsrc=/home/awanish/llvm-2.9/llvm-2.9 > --with-llvmobj=/home/awanish/llvm-2.9/llvm-2.9/build --with-stp=/usr/local > --with-uclibc=/home/awanish/klee-uclibc/ --enable-posix-runtime > > then did > > make DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 ENABLE_SHARED=0 -j2 > which ends without error. > > But when I did make check it says > > Expected Passes: 93 > Expected Failures : 2 > Unsupported Tests : 4 > Unexpected Failures: 84 > > is it correct or I am missing something. Please help me out and thanks in > advance. There shouldn't be any unexpected failures however: * I would advise that you do not use LLVM 2.9 and just use LLVM 3.4 * You can save yourself a bunch of effort by using the KLEE docker image [1]. * You have not said which tests actually failed. You need to provide this information otherwise nobody will be able to help you debug it. [1] http://klee.github.io/docker/ HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee and c++14
Hi, On 15 August 2016 at 14:48, Leandro Rabindranath Leon wrote: > Hi > > Apologies if this is not the appropriate space for pose this question. > > As I have understood, I can not use klee on programs in C++14, as > llvm-3.4 does not support it. > > However, I would like to know if there is any way, trick, experimental > version, etc, which would allow me. What you mean is that "Clang 3.4" doesn't support C++14 (I've not actually checked this). We have had ports of KLEE to newer LLVM versions however to make this work you would need to find a way to compile libcxx to bitcode and have KLEE use that. There are likely to be other complications in KLEE's current design which creates problems symbolically executing C++ programs (e.g. no support for exceptions). Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee-uclibc installation fails
On 17 August 2016 at 17:03, Reza Ahmadi wrote: > Hi, > > I had installed klee (with llvm 2.9) without klee-uclibc. Now I want to > re-install klee including klee-uclibc. When I try to configure it complains > that I need to install ncurses. > > I installed ncurses using this, but still recieve that error message. > > sudo apt-get install libncurses-dev > > Here is what I receive. I am wondering if you could help. Thanks. > > > ahmadi@jding001:~/klee-uclibc$ ./configure --make-llvm-lib > INFO:Disabling assertions > INFO:Configuring for Debug build > INFO:Configuring for LLVM bitcode archive > INFO:Using llvm-config > at.../home/ahmadi/llvm-2.9/Release+Asserts/bin/llvm-config > INFO:Using llvm tool dir.../home/ahmadi/llvm-2.9/Release+Asserts/bin > INFO:Found "/home/ahmadi/llvm-2.9/Release+Asserts/bin/llvm-objdump". > INFO:Found "/home/ahmadi/llvm-2.9/Release+Asserts/bin/llvm-link". > INFO:Found "/home/ahmadi/llvm-2.9/Release+Asserts/bin/llvm-ar". > INFO:Found "/home/ahmadi/llvm-2.9/Release+Asserts/bin/llvm-nm". > INFO:Searching for LLVM Bitcode compiler... > INFO:Found clang in LLVM Build > dir.../home/ahmadi/llvm-2.9/Release+Asserts/bin/clang > INFO:Testing LLVM Bitcode > compiler.../home/ahmadi/llvm-2.9/Release+Asserts/bin/clang > INFO:Compiler /home/ahmadi/llvm-2.9/Release+Asserts/bin/clang works > INFO:Using LLVM Bitcode > Compiler.../home/ahmadi/llvm-2.9/Release+Asserts/bin/clang > INFO:Checking for ncurses... > ERROR:Failed to find ncurses. Compiler said: > /usr/bin/ld: cannot find crtbegin.o: No such file or directory > /usr/bin/ld: cannot find -lgcc > /usr/bin/ld: cannot find -lgcc_s > clang: error: linker command failed with exit code 1 (use -v to see > invocation) > > ERROR:You should install the ncurses library and development headers. Using clang 2.9 as your host compiler is not a configuration we test. You can see in your error message that it is failing to link. Have you actually tested that your copy of clang 2.9 can actually build native code? Note take a look at the `determineHostCompiler()` function in the `configure` script. You may need to hack this to force the right compiler to build the native code that uclibc's build system needs. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] make check fails 10 tests
Hi, > Command 0 Stderr: > /home/ahmadi/klee/test/Feature/LongDouble.cpp:11:10: fatal error: 'cstdio' > file not found > #include > ^ > 1 error generated. Looks like llvm-gcc couldn't find the header file. You might be able to fix that my telling llvm-gcc where the tests are by doing the following. ``` export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu ``` I would advise staying away from llvm-gcc though. That compiler has been dead for years. Just build KLEE with LLVM 3.4 with Clang 3.4 HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Option for generating MC/DC testcases
Hi Damir,
On 9 May 2016 at 01:55, Damir wrote:
>
> Hello everyone!
>
> I've recently started using KLEE, and I'm wondering how hard it would be to
> implement full MC/DC testcases generation in KLEE.
>
> You can read about MC/DC on Wiki
>
> https://en.wikipedia.org/wiki/Modified_condition/decision_coverage
>
> I've done some analysis, and figured out how it can be done in klee,
> theoretically,
Your analysis here isn't really correct here. If KLEE worked directly
on C code your analysis might be in some cases but that is not how
KLEE is implemented. KLEE works on LLVM IR so that needs to be
considered when thinking about implementing new features. I also don't
think you are trying to do will work in general as it assumes
"conditions" are simple expressions that don't contain forking.
> As I see it, implementing such feature would require tampering with forking
> mechanism in KLEE, in following ways:
>
> 1) Allow breaking a complex decision into conditions, for example
>
> if (A && B && C)
> the decision is (A && B && C) here, and conditions are A, B and C.
>
> All conditions are functions of symbolic variables, returning boolean, and
> combined into decision using only boolean logic.
This is wrong in several ways.
First in the LLVM IR that KLEE interprets the conditions will likely
appear as separate branch instructions as they are short-circuiting
operators (they might not depending on if LLVM's optimizer modifies
the branches)
Second your conditions in general might not be plain expressions. They
could be function calls for example which may contain forking. E.g.
```
void foo(const char* a) {
if ( strlen(a) == 5 && a[0]='h' && (a[1] == 'i] || a[1] == 'x')) {
// do something
}
}
```
one or more of the conditionals may change the state of the program too.
> 2) Instead of forking on whether decision is true or false, forks are based
> on conditions.
>
> Before (current KLEE):
>
> fork 1: Decision(A, B, C) == false
> fork 2: Decision(A, B, C) == true
As stated above KLEE does not work this way.
> MC/DC way:
>
> Before forking, set of conditions (in addition to previous ones) must be
> solved:
>
> For example, for condition A:
>
> A(x1, y1, ... z1) == false
> A(x2, y2, ... z2) == true
>
> B(x1, y1, ... z1) == Bfixed
> B(x2, y2, z2) == Bfixed
>
> C(x1, y1, ... z1) == Cfixed
> C(x2, y2, z2) == Cfixed
>
> Decision(x1, y1, ... z1) != Decision(x2, y2, ... z2)
>
> If there is a solution (Bfixed, Cfixed) to those constraints, two forks are
> created with following conditions on them:
>
> fork 1: A == true, B == Bfixed, C == Cfixed
> fork 2: A == false, B == Bfixed, C == Cfixed
As stated above this will not work in general because your conditions
may not be simple expressions.
However if your conditions are simple expressions it would be
technically possible to change the forking behaviour to target MC/DC
coverage. You would need to perform some sort of LLVM pass before
running that
- labels the different conditions (probably using LLVM's metadata) so
that later we can work out which expressions correspond to what
conditions
- Merge the basic blocks and branching used in the short circuit
operators so there is only a single branch instruction corresponding
to the ``if()``
For these merged branches we would handle them specially by trying for
each condition to fork on that condition while holding the other
conditions as the having the same value on either side of the fork. If
for a particular condition we can't fork then we know that the
condition can't affect the branch and that for the particular path we
are on that condition is irrelevant. Note I said "particular path"
here! There could be another path where the condition could affect the
branch. I'm not sure if MC/DC says anything about this (i.e. whether a
condition must independently effect a branch for all paths leading to
the condition or if just a single path must do this).
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to add label to assert statements
>> 3. We need to control Z3's memory management for Z3_ast and Z3_sort >> nodes manually. IIRC the C++ API doesn't let you do this. > > > I could not understand the 3rd point. Can you please explain it a little > more. It would help me understand the working of KLEE better. The Z3Builder caches declared Arrays and Updates to be across multiple solver queries. Therefore we can't use Z3's automatic memory management because that clears expressions when they are popped from the solver assertion stack. See Z3Builder::getInitialArray(..) and Z3Builder::getArrayForUpdate(..) So instead we do our own memory management by using ``Z3_mk_context_rc(..)`` and using the Z3ASTHandle and Z3SortHandle helper classes to automate most of the increment/decrement of references. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to add label to assert statements
Hi, On 29 April 2016 at 06:55, Sumit Kumar wrote: > Hi Dan, > > Thanks for introducing the z3 support. It has been great help. It has saved > me tons of work :). > Please find below my answers to some of your queries: > >>Yes your previous e-mails were misleading because you said > "getConstraintLog method in Executor.cpp is called with > logFormat=STP". > > Well, not exactly, because I am explicitly calling the getConstraintLog(...) > method with logFormat=STP option even when the backend is z3. Now since my > backend solver is z3, it in turn calls getConstraintLog() method on the > z3 core solver object using the TimingSolver Object: > > char *log = solver->getConstraintLog(query); //in Executor.cpp inside > function getConstraintLog when logFormat=STP Okay so our naming is really bad here. I've opened an issue so we don't forget to fix this https://github.com/klee/klee/issues/382 >>If your aim is to get to constraints in the SMT-LIBv2 format then why are >> you using ``getConstraintLog()`` which will use the core solver's natural >> constraint language (for Z3 this happens to be SMT-LIBv2 but you don't have >> fine the grained control you need)? Instead you should do what Thuan is >> suggesting and modify the ExprSMTLIBPrinter to add labels if that is your >> goal. > > I chose to use the getConstraintLog method instead of modifying > ExprSMTLIBPrinter for these reasons: > 1. getConstraintLog(..) exposes Z3 C api to me. It allows me to modify/use > Z3 C api to get desired output. ``Executor::getConstraintLog()`` doesn't really expose the Z3 C API to you. The method just gets the solver to emit the constraint log which if you're using Z3 eventually calls Z3. > 2. getConstraintLog(..) method returns me a string instead of printing the > result. The ExprSMTLIBPrinter doesn't have to "print the result". It just writes to an ``llvm::raw_ostream``. That can be a file but you can also use ``llvm::raw_string_ostream`` instead to write to a std::string. You use the following method to set the output. ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output). Any if you have used ``logFormat=SMTLIB2`` with ``Executor::getConstraintLog()`` you would have got a string in SMT-LIBv2 format. > Also, although I started with printing labels to assert statements, I later > realized that I didn't need to do that as I had access to z3 c/c++ api and > could pass the labels to z3 directly. I'm curious what Z3 C API function did you use to label the Z3_asts? Was it ``Z3_solver_assert_and_track(..)``? >>If you are already using Z3 as the solver backend why don't you use > its C API to get the unsat core? > > I also realized the same sometime back :) . I have already done exactly what > you have suggested. I am able to get the unsat core using the z3 c++ api. > P.S: While working on this I realized that it would be a lot better if > instead of using Z3 C api, C++ api was used as Z3 C++ api is much easier to > use than Z3 C api. I wonder if it would be good to rewrite the Z3 Core > Solver methods using Z3 C++ api. I don't want to use Z3's C++ API for several reasons 1. The C++ API is built on top of the C API so everything the C++ API can do the C API can also do. 2. The C++ API doesn't expose everything the C API does. This is improving but the C API is where all newly exposed features will be added first. 3. We need to control Z3's memory management for Z3_ast and Z3_sort nodes manually. IIRC the C++ API doesn't let you do this. Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to add label to assert statements
Hi, On 28 April 2016 at 20:57, Sumit Kumar wrote: > Hi, > I forgot to add this earlier and I think that this is important in this > context: I am running klee with following setting: -solver-backend=z3. I > apologize for missing this information. Yes your previous e-mails were misleading because you said "getConstraintLog method in Executor.cpp is called with logFormat=STP". It's cool that you're using the Z3 support I recently introduced but I am very bemused by how you are using it. * If your aim is to get to constraints in the SMT-LIBv2 format then why are you using ``getConstraintLog()`` which will use the core solver's natural constraint language (for Z3 this happens to be SMT-LIBv2 but you don't have fine the grained control you need)? Instead you should do what Thuan is suggesting and modify the ExprSMTLIBPrinter to add labels if that is your goal. * If you are already using Z3 as the solver backend why don't you use its C API to get the unsat core? Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Some questions about SMT solvers
On 18 April 2016 at 12:20, Fabrizio Biondi wrote: >> > 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. >> Indeed, that' correct. > > Thanks, it's clearer now. Sorry for the missing example, but it seems you > guys got the question right anyway :). > >> > 2. I don't recall ever seeing KLEE extracts more information from the >> > solver other than satisfiability decision. Perhaps others would know more. >> KLEE does several constraint simplification and optimisation passes, but >> does not extract any information from the solver other than >> satisfiability/validity results and solutions/counterexamples. > > I see. Does this not mean that possibly the solver is asked to simplify the > same constraints over and over? I am assuming the simplifications don't over- > or underapproximate the constraints, of course. This might be the case. However we don't have a good way right now of communicating the solver's expression simplifications to KLEE right now. We have only recently added Z3 support which can simplify expressions for us on demand but use of this hasn't been investigated yet. In the case of Z3 simplification would be simpler if we used the solver's expression language for constraints but currently we use KLEE's own language for several reasons: * Independence from a particular solver implementation. This allows to support STP, Z3 and MetaSMT * The semantics of KLEE's Expression language and the solver's expression language aren't exactly the same. The reason for this is that KLEE's expression language closely models LLVM's instructions. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Some questions about SMT solvers
Hi Fabrizio, On 15 April 2016 at 13:10, Fabrizio Biondi wrote: > Hi all, > > I have been tinkering with KLEE's SMT solver chain, and I have a few > doubts some of you may find the time to address. > > 1) I have noticed that computeValidity returns 0 (Unknown) a lot. This is an > example: Your example is missing from the e-mail. > Since in the example above there is no constraint on word number 6 and the > query is on word number 6, I would expect the solver to return 1 (True), > meaning that there exists a model satisfying the query under the > constraints. Is my understanding of what 'validity' and 'invalid' mean > wrong? Yes your understanding is incorrect here. See the comments on the ``computeValidity(...)`` method [1]. You are confusing validity and satisfiability which are two different but related concepts. Validity is in general concerned with some formula being true for all possible variable substitutions whereas satisfiability is in general concerned with some formula being true for at least one variable substitution. In KLEE a ``Query`` object is made up of a "query expression" and a set of constraints. The ``computeValidity()`` method computes the value of ∀ X : C(X) → Q(X) which is either true (valid) or false (invalid). Here X is a set of free variables, C is the set of constraints conjuncted that may use the free variables and Q is the "query expression" which may use the free variables. This is equivalent to ¬ ∃ X : C(X) ∧ ¬ Q(X) > 2) I have noticed that KLEE does not simplify SMT statements much, I guess > this is because it expects the underlying SMT solver (STP or Z3) to take > care of the simplification. However, is the simplified version of the > constraints obtained from the solver and used in the rest of the symbolic > execution? Ideally KLEE should simplify expressions as much as possible to try to avoid expressions from growing large as execution continues. We assume that the underlying SMT solver can do some simplification but currently for Z3 we are missing an opportunity to do further simplificiation because Z3 exposes an API (Z3_simplify()) which we aren't currently using. See [2]. I think it would be useful to investigate doing this. > Allow me to elaborate. I have some large set of constraints C, and I query > the solver for e.g. its validity. The solver internally simplifies C to a > smaller set C', computes its validity, and answers. Does KLEE henceforth use > C' as its set of constraints for that trace, or does it use C? KLEE continues to use C. Even so are you assuming that C' and C are equivalent or equisatisifiable? The SMT solver and KLEE are currently decoupled from each other so this is unlikely to change any time soon. [1] https://github.com/klee/klee/blob/master/include/klee/SolverImpl.h#L60 [2] https://github.com/klee/klee/blob/master/lib/Solver/Z3Builder.cpp#L416 Hope that helps, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how KLEE handles variable scoping
On 8 April 2016 at 18:01, Sumit Kumar wrote: > Hi, > > Can anyone please tell how KLEE handles variable scoping ? KLEE executes LLVM IR. Clang is handling the variable scoping here so that KLEE never sees any scoping issues. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to introduce a new symbolic variable
On 4 April 2016 at 15:34, Sumit Kumar wrote: > Hi, > > Can anyone please tell me how to introduce a new (not declared in test > program) symbolic variable from within KLEE. Your question is not specific enough. "symbolic variable" here could mean several different things. E.g. you could just make a new ``Array`` and create ReadExpr of it or you could actually create something in KLEE's model of memory and read from that. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to Interpret Klee Path Predicate
On 4 April 2016 at 17:55, Azizul Hakim wrote: > Thanks Dan. I can also print the constraints in the format below. Do you > happen to have any idea where I can get a documentation of this format? > > > > (query [(Eq false > (Eq (w32 0x0) > (And w32 (Add w32 (w32 0xfffe) > (ZExt w32 (Read w8 0x0 v0_str_0))) > (w32 0xff] >false) > > > > Thanks for your time. > That is the [kQuery format](https://klee.github.io/docs/kquery/) which is specific to KLEE. One thing you could try doing is porting the ExprSMTLIBPrinter to your fork of KLEE, it shouldn't be too difficult. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Steps required for adding expr
Hi, On 4 April 2016 at 16:22, Sumit Kumar wrote: > Hi, > > I was reading Expr.h file when I came across this comment: > > Steps required for adding an expr: > -# Add case to printKind > -# Add to ExprVisitor > -# Add to IVC (implied value concretization) if possible > > Can anyone please explain the above in anyway possible (brief / detail) ? I have been adding a lot of new expressions to my fork of KLEE recently so I can tell you what I've found to be the bare minimum. 1. Add class declaration and a corresponding ``Expr::Kind`` to ``Expr.h`` and implementation to ``Expr.cpp``. You might need to provide an implementation of ``computeHash()``, ``create()`` and ``compareContents()`` depending on which existing class your derive form. You will need to add your new Expr class to ``Expr::printKind()``. 2. Add support for your new Expr class to ExprVisitor. 3. Add support for your new Expr class to STPBuilder.cpp and/or Z3Builder.cpp depending on which solver you care about it. If you want to be able to print your constraints as SMT-LIBv2 you'll need to add support for your new Expr class in ``ExprSMTLIBPrinter``. Similarly you will need to put some extra work in to add support for your new Expr class to the KQuery printer/parser. Hope that helps, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE generated only one path whereas program has two
> But the output from KLEE indicated that it completed only one path whereas > the program clearly has two paths. Can anyone please explain why this > happened ? Remember that KLEE executes LLVM IR, not C! You should look at the LLVM IR. If you look (see ``klee-last/assembly.ll``) you'll see that the branch has been lowered to a select instruction (i.e. an if then else instruction). This happens due to the running the pass created by ``createCFGSimplificationPass()`` in ``KModule::prepare(...)`` ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to clone an expression
On 24 March 2016 at 11:52, Sumit Kumar wrote: > Hi, > > Can anyone please tell me how to clone an expression. I want to get a copy > of given expression but they must not share any object. You are using the wrong mailing list. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to Interpret Klee Path Predicate
On 21 Mar 2016 11:19 a.m., "Dan Liew" wrote: > > > On 21 Mar 2016 10:33 a.m., "Azizul Hakim" wrote: > > > > How do we interpret the path predicates generated by KLEE. I've the following path predicates generated by S2E tool which uses KLEE. This predicate is generated from one branch of an IF-ELSE statement. > > > > IIRC you're looking at STP's internal format which I think is based on CVC's internal format > > http://cvc4.cs.nyu.edu/wiki/CVC4%27s_native_language > > Mainline KLEE supports emitting constraints in the SMT-LIBv2 format which is more widely used and documented. However I don't know when S2E forked from KLEE so I find know if S2E has this capability Sorry phone autocorrected incorrectly. It should say However I don't know when S2E forked from KLEE so I don't know if S2E has this capability. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to Interpret Klee Path Predicate
On 21 Mar 2016 10:33 a.m., "Azizul Hakim" wrote: > > How do we interpret the path predicates generated by KLEE. I've the following path predicates generated by S2E tool which uses KLEE. This predicate is generated from one branch of an IF-ELSE statement. > IIRC you're looking at STP's internal format which I think is based on CVC's internal format http://cvc4.cs.nyu.edu/wiki/CVC4%27s_native_language Mainline KLEE supports emitting constraints in the SMT-LIBv2 format which is more widely used and documented. However I don't know when S2E forked from KLEE so I find know if S2E has this capability HTH, Dan ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] how to know if variable is symbolic
On 17 March 2016 at 17:18, Sumit Kumar wrote: > Hi, > I want to know if there is a way to know if a variable is symbolic or not in > KLEE when KLEE is executing an instruction involving the variable. Within the application it self you can call ``klee_is_symbolic()``. Inside KLEE you just have to test whether the expression representing the register is constant. See ``SpecialFunctionHandler::handleIsSymbolic()``. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How can I get KLEE to generate constraints from within function calls
On 18 March 2016 at 15:00, Sumit Kumar wrote: > Hi, > > My test program is this: I declare 'x' as symbolic and then pass the address > / value of x as argument to function foo like foo(x) or foo(&x). Inside the > function foo no variables have been explicitly made symbolic. Based on your description it sounds like the address of ``x`` is not symbolic. The contents of memory that ``x`` points to is. > Now when I run > KLEE I do not see any constraints generated from foo. How can I get KLEE to > generate constraints from within function calls. I am using KLEE with > llvm2.9. Your question is far too vague. If you write a precise question you are more likely to get a useful answer. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] what the third argument in SpecialFunctionHandler::handleMakeSymbolic
On 19 March 2016 at 10:23, Sumit Kumar wrote: > Hi, > > Can anyone please explain what the third argument is in the following > function/method: > > SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, > KInstruction *target, std::vector > &arguments) > > Please explain what expressions are supposed to be contained in "arguments" > vector. Its not clear from the code. In this case they are the arguments to the function ``klee_make_symbolic()`` with argument 0 being the left most argument. Each argument will be the expression that represents that argument. If the arguments are a constant they will be of type ``ConstantExpr``. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] question: how to create read expression
On 1 March 2016 at 07:19, Sumit Kumar wrote: > Hi, > Let "x" be an integer identifier and it is made symbolic. I want to create > or get this expression: > > ReadLSB w32 0 x > To make a ReadExpr you should use ``ReadExpr::alloc()``. But that represents a 1 byte read. To get a read of width 32 you will need to Create several ``ConcatExpr`` to concatenate that reads. You can use the ``ConcatExpr::create4()`` to help you with this. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] a question about kleaver
Hi,
On 8 January 2016 at 10:18, xiaoqixue_1 wrote:
>
>
> Hi,
>
> When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be
> used at the same time.
> the logic is simple:
> if( sn > 5) {
>if( sn < 8 ) {
> if (sn==0) printf("hello");
> }
> }
>
> the query is as follows:
>
>array sn[4] : w32 -> w8 = symbolic
> (query [(Ult 5
> N0:(ReadLSB w8 0 sn))
> (Ugt N0 8) ]
> (Eq N0 0) [] [ sn ] )
>
>
> it crashes the kleaver, but when I change the file to :
The crash is due to Ult not being supported by the STPBuilder. In KLEE
a Ult expression shouldn't ever occur due to expression
canonicalisation rules used internally inside KLEE. The assertion
failure you hit is
Query 0:kleaver:
/home/dan/dev/klee/src/lib/Solver/STPBuilder.cpp:903: klee::ExprHandle
klee::STPBuilder::constructActual(klee::ref, int*):
Assertion `0 && "unhandled Expr type"' failed.
Take a look at ``include/klee/Expr.h`` to get an explanation of why
these rules exists. If you pass `` --builder=simplify`` to kleaver the
expression builder should try to canonicalise the expressions for you
and avoid the crash.
Hope that helps.
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Klee path statistics and merging options
> Is the number of completed paths same as number of feasible paths in the > program ? > > 2> Does Klee invoke a SAT query at every branch point in the program by > default to determine > the eager infeasibility of a path ? Or is there other heuristics to > selectively chose branch points ? AFAIK KLEE issues a query at every branch point. This does not necessarily trigger a call to the underlying solver though as KLEE has some caching mechanisms that may fire. > 3> Does Klee support SAT solvers in the backend like MiniSAT etc ? You are looking at the wrong level. KLEE works at the level of SMT solvers, not SAT solvers as it needs a logic over bitvectors, not booleans. Typically an SMT solver will be implemented in terms of a SAT solver but KLEE does not know this. STP itself supports two backends MiniSat and CryptoMinisat4. KLEE doesn't currently set the backend to use in STP but support could be added. I would happily review a pull request that added this. KLEE supports a few other SMT solvers via the MetaSMT interface (untested) and I am currently working on native Z3 support. > believe that the default SMT solver > used is STP. The follow-up to this question is that are there options to > dump the path-constraints > in DIMACS format to use with a SAT solver. KLEE supports emission of the constraints in its own custom language (KQuery) and as SMT-LIBv2. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Testing coreutils: Invalid record
On 28 December 2015 at 05:35, felicia wrote: > I followed the instruction on > https://klee.github.io/tutorials/testing-coreutils/ > I would like to run coreutils by using KLEE latest version and LLVM 3.4 > Since, I use clang instead of llvm-gcc. In the step 2, I use clang to build > coreutils with these commands below: > > ../configure --disable-nls CFLAGS="-g" > export LLVM_COMPILER=clang > make CC=/home/felicia/whole-program-llvm-master/wllvm > make -C src arch hostname CC=/home/felicia/whole-program-llvm-master/wllvm > > However when I proceed to step 3: Using KLEE as Interpreter by execute: > > ~/full-path-to KLEE/Release+Asserts/bin/klee --libc=uclibc --posix-runtime > ./cat.bc --version, > > the output is KLEE: ERROR: error loading program './cat.bc': Invalid record > > Am I missing something? Thank you very much. That error likely means something is wrong with the LLVM bitcode you are feeding to KLEE. One possible cause is that the version of LLVM that your clang was compiled against does not match the version that you built KLEE with. The LLVM bitcode format changes over time so to have things work correctly you should use the version of Clang the the KLEE build system uses to compile its own runtime library. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Klee path statistics and merging options
Hi, On 17 December 2015 at 02:08, RAJDEEP MUKHERJEE wrote: > > Hi, > > I have the following queries regarding Klee. I would really appreciate any > help. > > 1> How to obtain the following statistics from Klee: > A> Total number of feasible paths, > B> Total number of infeasible paths, > C> Total number of paths in the program. > D> Total number of solver queries and > E> Total time spent in solver Use the ``klee-stats`` tool tool on an output directory (e.g. ``klee-last``) produced by KLEE after it has finished executing. > 2> Does Klee perform any state merging or path-merging ? What option to use > for this ? Not by default. There is experimental support for merging paths with the ``klee_merge()`` special function but I've never used it. > 3> Does Klee perform property driven slicing before it begins symbolic > execution ? Technically I think running an optimisation that the LLVM optimiser considers remove dead code could be considered a form of program slicing but that's probably not what you mean by "property driven slicing" in which case the answer is probably no. Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Warning: Switching to C++11 soon
Hi, Just a heads up for anyone not following KLEE's issue tracker [1]. We will soon be requiring a C++11 capable compiler to build KLEE. This is kind of already a requirement because STP requires C++11 so this shouldn't really be much of a shock. I'm just waiting for the tests for [2] to pass and then this change will be merged. [1] https://github.com/klee/klee/issues [2] https://github.com/klee/klee/pull/317 Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] make: error: Unable to link with functions of libllvm
> I've checked that libLLVM-3.4.2.so exports above functions correctly by nm > command. > KLEE is currently intended to be linked against the LLVM static libraries, not the dynamic one. I think passing ``ENABLE_SHARED=0`` to make to have KLEE link against the LLVM static libraries ought to work. Feel free to dig deeper to find the root cause of the issue though. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding assignments to state constraints
Hi,
On 4 November 2015 at 09:11, felicia wrote:
> Hi Tomek,
>
> The purpose I am doing this, is because I would like to ask the solver even
> at the point before x is used in the branch condition.
I don't understand what you mean. If you ask the solver if (x <= 0) is
satisfiable before executing the (x <=0) branch and the input x was
not constrained then of course (x <= 0) will be satisfiable.
> For example, in this code:
> int add(int p1, int p2, int p3, int x) {
> if(x <= 0){
> if(p1 > 8) x = x;
> else x = x + 1;
> if(p2 > 8) x = x;
> else x = x + 2;
>
> assert(x <= 3);
> }
> return x;
> }
>
> In this case, the code has 3 branches condition (p1 > 8), (p2 >8) and the
> assertion (x <= 3).
> Since KLEE normally do the FALSE condition first, it will execute (p1 <= 8)
> and it will do the addition (x + 1). At the second branch (p2 > 8), for
> example, I need to ask the solver whether x <= 0 by using
> solver->evaluate(current constraint, x <= 0, result) . Since the current
> constraints are only x <= 0 and p1<=8, the solver would say it is
> satisfiable (although it's actually not). Therefore, I would like to add
> constraint x + 1 at this point, so the solver aware about this.
I think talking about the constraints at the C level might be
confusing things. At the LLVM IR level the code is SSA form so once a
register is assigned to is never changed. There will be different
registers corresponding to different versions of "x" in the IR. So I
don't think you need to add "assignment constraints" at all. You just
need to ask if latest version of "x" if <= 0.
Besides a constraint "x == x +1" is always false. The constraint you
give " (Add w32 1 (ReadLSB w32 0 x))" is also wrong. A constraint must
be expression of boolean type, "x + 1" does not give a boolean type.
Dan.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Error unable found llvm-config when build uclibc
On 3 September 2015 at 20:22, felicia wrote: >> Hi, >> >> I would like to install Build uclibc and the POSIX environment model. >> But, when I ran ./configure --make-llvm-lib, it produces errors like this: >> >> INFO:Disabling assertions >> INFO:Configuring for Debug build >> INFO:Configuring for LLVM bitcode archive >> INFO:Using llvm-config at...None >> ERROR:llvm-config cannot be found The configure script is trying to find a compiler capable of creating LLVM bitcode (see the comment at the top of the file of an explanation of what its doing). The easiest thing to do is to set an environment variable to point to the version of clang you want to use .e.g CC=/path/to/clang ./configure --make-llvmlib ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Error in configuring KLEE with Ubuntu 12.04 LTS 64-bit
On 2 September 2015 at 09:25, Giuseppe Petracca wrote: > Hi, > I am currently encountering the following error while configuring KLEE > > http://stackoverflow.com/questions/32337845/klee-configuration-error?noredirect=1#comment52581865_32337845 I posted an answer of stack overflow ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE+Z3 (an instance of KLEE-MultiSolver) still concretizes floating point expression to 0.
> Is there a way to tell KLEE not to concretieze floating point expression to > 0 so KLEE + Z3 can be useful when handling floating point program? > Not right now no. KLEE's expression language does not support floating point constraints right now which is why floating point numbers get concretised. There is a fork of KLEE (KLEE-CL/KLEE-FP) that does support floating point numbers in its expression language (but not for constraint solving via an SMT solver) but it is not actively maintained. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] EasyKLEE
Hi, On 16 August 2015 at 11:02, Owl owl wrote: > Hey, > > Wanted to give people a heads up that I've started a project to simplify the > install process for KLEE. > > https://github.com/Owlz/EasyKLEE > > At the moment, I've only gotten support for Ubuntu 15.04 x64, but am > planning on adding other versions too. It builds out KLEE 3.4 with LLVM 3.4 > and associated dependencies. On my VM at home, this takes about 10-15 > minutes to complete the install. Thanks for having a go at this however others have done this in the past (e.g. [1]) so that isn't really where effort needs to be spent (also scripts for building KLEE are already in the git repository which are used for TravisCI and for building the Docker image). What really needs doing is * Documenting using our Docker image [2][3]. Using the docker image is much more convenient and reliable than using shell scripts. * Building a KLEE Ubuntu package. This is on my TODO list but it is quite involved because we need to make STP and Cryptominisat4 packages too. [1] http://mailman.ic.ac.uk/pipermail/klee-dev/2014-October/000852.html [2] https://hub.docker.com/r/klee/klee/ [3] http://mailman.ic.ac.uk/pipermail/klee-dev/2015-April/001036.html ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE make pointer symbolically
On 3 June 2015 at 05:28, 张若虚 wrote:
>
> Hi all,
>
> In the following program, I make a pointer symbolically. The name of
> program file is array.c
>
> int main(int argc, char **argv) {
> int a = 0;
> int *p = &a;
> klee_make_symbolic(&p, sizeof(p), "a");
> *p = 1;
> return EXIT_SUCCESS;
> }
>
> I use the following command to invoke KLEE.
>
> klee --search=random-path array.o
>
> And KLEE finds 89 paths and generate 84 test cases.
>
> Firstly, did I make some mistake, like the parameter of function
> klee_make_symbolic() ? Or did I miss some KLEE command line options which
> can solve this problem?
>
> If I am correct, I don't think this is reasonable. Why does KLEE handle
> symbolic pointer in this way?
It's not exactly clear what your intention is but what KLEE is doing
perfectly reasonable. You made the pointer ``p`` symbolic so it can
point to anything (including ``a``) so KLEE's current approach is to
create a path for every possible memory object that could be pointed
to by the symbolic (I suspect KLEE also generates a path for the case
where the pointer does not point inside any memory object).
I noticed you set the third argument to ``klee_make_symbolic()`` to
"a" despite the fact the pointer ``p`` might not point to ``a``.
If you actually wanted to make the variable ``a`` symbolic you should do
```
klee_make_symbolic(&a, sizeof(a), "a");
```
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] structure definition in KLEE source code
Look at Expr.h and Expr.cpp. https://github.com/klee/klee/blob/master/include/klee/Expr.h https://github.com/klee/klee/blob/master/lib/Expr/Expr.cpp If you're looking at adding floating point support consider looking at Peter Collingbourne's fork of KLEE (klee-fp/klee-cl) which extends KLEE's expression language with support for floating point (amongst other things). ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Klee Make Check
Hi, On 22 May 2015 at 01:04, Ben Mehne wrote: > Hello, > > I am trying to compile and use Klee with the POSIX/uClibc environment, but > "make check" exits with error and "Unexpected Failures: 36". Does this mean > that klee will not function as intended? Any guidance would appreciated. > > -- My Setup > I am building Klee using stp r940 with the patches from this mailing list > (and its git), LLVM 2.9 with the unistd.h patch, and trunk Klee. "make > unittests" does not exit with error. I am using the attached build_klee.sh > script (if it is not scrubbed - it is just the directions from the wiki + > patches in a bash script). As far as I can tell, the llvm-gcc is being used > wherever a compiler is needed in klee and llvm-2.9. I am on 64 bit, Arch > Linux; I have GCC 4.9.2 installed, and llvm 3.6, but I think if those were > the problem, the issue would be during compilation, not running tests. LLVM 3.6 is not supported yet but LLVM 3.4 is if you wish to use that. > -- Bug/Issue Details > All of the unexpected failures (unless I missed one) exit on the assert: > klee: main.cpp:1109: llvm::Module* linkWithUclibc(llvm::Module*, > llvm::StringRef): Assertion `ft->getNumParams() == 7' failed. All test > cases that call this function fail. > > This is failing because the FunctionType has no params and is variable args > as per the getOrInsertFunction on line 1025. This leads me to believe that > either the bca file that is being linked in is corrupt/wrong or there is > some deep bug in the LLVM 2.9 code that links it in. Attached is the bca > file (if it has not been scrubbed). The archive file does seem to have > "__uClibc_main" defined in __uClibc_main.os . Sounds like your klee-uclibc build didn't work properly. Looking at your script I see a bug ``` ./configure --make-llvm-lib --with--lvm-config "$SCRIPT_DIR""/tmp/llvm-2.9/Release+Asserts/bin/llvm-config" make -j2 || exitmsg "Failed to build posix/uclibc env" #why 2? ``` First it's ``--with-llvm-config`` not ``--with-lvm-config``. Second you are not checking the exit code of running the configure script which will very likely fail (either that or it'll pick up your LLVM 3.6 install, I can't remember what will happen). You should make your shebang ``#!/bin/bash -e`` rather than ``#!/bin/bash`` so that if any command exits with a non-zero exit code your script will stop running rather than continuing. With regards to the "why 2", that's an arbitrary choice, choose whatever number works for you. Just to note we have an experiment Docker image you can use which seems to work okay [2], this will save you from having to build KLEE and it's dependencies. > I notice that the travis build system does not run "make check" - could it > be a subtle compilation issue with llvm-2.9? Travis does effectively run ``make check``. The invocation of ``lit -v .`` [1] is equivalent. Not running ``make check`` directly is an implementation detail due to the fact ``llvm-lit`` is not available in the build environment but ``lit`` (which is actually the same program) is. [1] https://github.com/klee/klee/blob/master/.travis/klee.sh#L94 [2] https://registry.hub.docker.com/u/klee/klee/ Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] More about all/solver-queries.smt2 files
Hi, On 12 May 2015 at 14:50, Andrea Aquino wrote: > Dear all, > > I analyzed the coreutils of the linux kernel using KLEE (llvm version 2.9 on > host 1386-pc-linux-gnu (Ubuntu 32 bits)). > > I configured KLEE to use both caches, to timeout after 1 minute, to produce > no output and to log all queries in smt2 format to a file and the queries > that reach the solver to another file. The complete command I used is the > following one (used in a bash script where $1 represents the name of a given > coreutils program). > > klee --use-cache --use-cex-cache --no-output --use-query-log=all:smt2 > --use-query-log=solver:smt2 --simplify-sym-indices --write-cvcs --write-cov > --output-module --max-memory=1000 --disable-inlining --optimize > --use-forked-solver --libc=uclibc --posix-runtime --allow-external-sym-calls > --only-output-states-covering-new --environ=test.env --run-in=/tmp/sandbox > --max-sym-array-size=4096 --max-instruction-time=30. --max-time=$MAX_TIME. > --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 > --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal > --randomize-fork --search=random-path --search=nurs:covnew > --use-batching-search --batch-instructions=1 ./$1.bc --sym-args 0 1 10 > --sym-args 0 2 2 --sym-files 1 8 --sym-stdout &> /dev/null > > What I found is that the formulas in the all-queries.smt2 file seem to be > still sliceable (that is, they can be separated in many more independent > subformulas (i.e., formulas that do not share variables)). Is this normal? I think so. I remember this being reported on this list a while ago. > On a second thought, this might be due to the fact that the slicing procedure > I implemented takes in input a formula and returns all of its subformulas > that do not share variables, while KLEE slices a formula with respect to the > last path condition on the branch the current formula belongs to. Is my > intuition correct? AFAICT > Given this I would like to understand clearly how the all-queries.smt2 and > solver-queries.smt2 are populated (that is, the conditions that must hold for > a formula to be logged in one file or the other and what is the relation > between the formulas in these two files). I had a look at the code but it did > not help. The relevant code is in ConstructSolverChain.cpp [1]. This constructs a chain of ``SolverImpl`` objects that essentially form a pipeline for solving queries. The "all queries" is at the beginning of the pipeline and thus logs every single query sent to it by the Executor. The "solver queries" are at the other end of the pipeline once the queries have passed through the other ``SolverImpl`` objects. So this records the actual queries sent to the underlying SMT solver (i.e. STP by default). Note that the other ``SolverImpl`` objects in the chain may change the query (e.g. IndependenceSolver) or prevent it from even reaching the underlying SMT solver (e.g. CexCache). [1] https://github.com/klee/klee/blob/master/lib/Basic/ConstructSolverChain.cpp Hope that helps. Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Beginnier to KLEE
Hi, > I want to explore symbolic execution and KLEE seems like a good choice for > beginning. But I would like you guidance in getting to know the best way to > understand the code of KLEE. One thing you certainly do is read the OSDI'08 paper on KLEE to get a high level understanding of what it tries to do. One approach you could take to trying to understand the code is by trying to run a simple closed world (i.e. makes no external calls) program that contains no symbolic variables and does not link in any libraries (i.e. do not use --posix-runtime or --libc=...). Once you understand what KLEE has done by looking at the output files (e.g. assembly.ll) you could try following what KLEE is doing by running through gdb and break at points of interest and then following through what KLEE does. If you succeed in doing that try introducing a symbolic variable in your simple closed world program and running through gdb and see how KLEE behaves. This requires that you learn how to use gdb or use it indirectly via an IDE like Eclipse (with the CDT plug-in). It will certainly take time to learn this but IMHO it's worth the effort. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] error : klee + coreutils + experimental [+docker]
On 16 April 2015 at 13:59, Joshep J. Cortez Sanchez wrote: > Dan, > > Thanks for answer! > > In the 1) case, using whole-program-llvm all works fine. Great. > I don't know why in the tutorial(step 6) gives: > > Lines executed:97.03% of 101 > > and I obtained: > Lines executed:97.09% of 103 > > for : File '../../src/echo.c' << I'm using coreutils 6.11 too. I don't know. You are using a different compiler (clang) than the tutorial was written for (llvm-gcc) so that might potentially be the source of the discrepancy. Clang is supposed to be a drop-in replacement for gcc though so I would be surprised if that's the problem. > In the 2) case (Docker case with klee/klee container) > I downloaded some containers with same results. My docker is 1.5.0 too. > Executing ../configure for coreutils 6.11 (in mi computer) is done some kind > of recursion with a long path and fails creating the Makefile. [attached > image] > Surfing the web I arrive to: > https://github.com/docker/docker/issues/1413 > And I believe thats my problem, ( but I dont know why occur the "recursion") I suspected that was the issue which is why I suggested you mounted a directory from your host machine as a volume inside the docker container. This will bypass the storage driver (i.e. in your case aufs) so you'll have the path limit of your real filesystem rather than aufs. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] My forked KLEE using LLVM 3.6 passes regression and unit tests
> 4. Enable TravisCI tests for LLVM 3.6. Look at the /.travis.yml file. > Hopefully it would just be a case of adding a few more configurations > the ``env`` key > > - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 > DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 > - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 > DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 > - LLVM_VERSION=3.6 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 > ENABLE_OPTIMIZED=1 > - LLVM_VERSION=3.6 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 > ENABLE_OPTIMIZED=1 Oh I forgot to say you'll need to add the following to the before_install section in the ``travis.yml`` as well. - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.6 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.6 main" >> /etc/apt/sources.list.d/llvm.list' ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] My forked KLEE using LLVM 3.6 passes regression and unit tests
Hi Chase, Thanks for taking this work on. On 15 April 2015 at 20:43, Chace Clark wrote: > I have been working on updating KLEE to work using the newest stable version > of LLVM (3.6). > > It now passes the same regression tests that the llvm 3.4.2 version does, as > well as all the unit tests. > > I would love for these changes to be pushed to the main branch of KLEE. So would I. > What should i do to prepare before I submit a pull request to you guys? 1. Rebase your changes on the current KLEE master. I will not accept a pull request that's full of merge commits. 2. Try to make your commits are as "single purpose" as possible (i.e. don't try to do completely unrelated things in the same commit) 3. If possible run your patches through clang-format-diff (we use the LLVM style) so there aren't any formatting issues. You can use git-clang-format [1] to make this easier for you. 4. Enable TravisCI tests for LLVM 3.6. Look at the /.travis.yml file. Hopefully it would just be a case of adding a few more configurations the ``env`` key - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.6 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.6 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 The TravisCI build might not work straight away but doing this will help us iron out these issues before your changes go into master. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] error : klee + coreutils + experimental [+docker]
>> sudo docker run -ti klee/klee >> klee@2f1c0eaa949c:~$ wget >> http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gz >> klee@2f1c0eaa949c:~$ tar xf coreutils-6.11.tar.gz >> klee@2f1c0eaa949c:~$ cd coreutils-6.11 >> klee@2f1c0eaa949c:~/coreutils-6.11$ mkdir obj-gcov && cd obj-gcov >> klee@2f1c0eaa949c:~/coreutils-6.11/obj-gcov$ ../configure --disable-nls >> CFLAGS="-g -fprofile-arcs -ftest-coverage" >> >> config.status: executing po-directories commands >> config.status: creating po/POTFILES >> config.status: creating po/Makefile >> rm: cannot remove 'confdir3/confdir3/confdir3/.. >> .(many many repetitions ).../confdir3/confdir3': File name too long Oh I forgot to mention that (just in case it wasn't implied). I can't reproduce the above behaviour. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] error : klee + coreutils + experimental [+docker]
Hi, > Clearly i have not llvm-ld because it was removed. > So, what shuold I change in klee-gcc to make it work with the new > settings/version of things klee-gcc is only meant to be used with llvm-gcc. I would use whole-program-llvm [1] to build core utils if you are using clang. $ export LLVM_COMPILER=clang $ mkdir obj-llvm $ CC=/path/to/whole-program-llvm/wllvm ../configure --disable-nls CFLAGS="-g" $ make Now extract the bit code for the application you want to run $ /path/to/whole-program-llvm/extract-bc src/du # Now you will have a src/du.bc file which is a LLVM module $ klee --posix-runtime --libc=uclibc src/du.bc --version > 2) WITH DOCKER klee/klee case: > It fails in step 1 (2 too) > I run: > sudo docker run -ti klee/klee > klee@2f1c0eaa949c:~$ wget > http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gz > klee@2f1c0eaa949c:~$ tar xf coreutils-6.11.tar.gz > klee@2f1c0eaa949c:~$ cd coreutils-6.11 > klee@2f1c0eaa949c:~/coreutils-6.11$ mkdir obj-gcov && cd obj-gcov > klee@2f1c0eaa949c:~/coreutils-6.11/obj-gcov$ ../configure --disable-nls > CFLAGS="-g -fprofile-arcs -ftest-coverage" > > config.status: executing po-directories commands > config.status: creating po/POTFILES > config.status: creating po/Makefile > rm: cannot remove 'confdir3/confdir3/confdir3/.. > .(many many repetitions ).../confdir3/confdir3': File name too long Perhaps you're running an old buggy version of docker? I'm using Docker 1.5.0 Or perhaps there's something wrong with the underlying storage driver being used by your version of Docker. You could try doing the build of coretuils in a Docker volume to bypass the storage driver to see if that fixes your issue: $ docker run -ti -v /path/on/host/system:/mnt klee/klee the above will make the /path/on/host/system available in the /mnt inside the container. Then you could try extracting the coreutils files into /mnt and trying the build there. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Experimental official Docker image
Hi, > My wish is that such would keep updated with Klee and LLVM moving > forward, as my so far experience with such projects is that they get > outdated every time when creation of new images is not automated. As I stated in my original e-mail. The build of the docker image **is automated.** A new image is regenerated every time new commits are pushed to KLEE's GitHub repository. The newly built image will only replace the old image if the tests pass. > So > ideally, I imagine a script downloading Klee, LLVM, Docker base , and > creating image as output. That is exactly what the Dockerfile allows you to do. $ git clone https://github.com/klee/klee.git $ cd klee $ docker build -t name_of_klee_image . After running the above you will have a image on your system called "name_of_klee_image". You can then create a container from that image and gain shell access to it. $ docker run -ti name_of_klee_image /bin/bash Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] problems configuring klee on debian 7.8
On 8 April 2015 at 00:45, Donald Raikes wrote: > Hello, > I am trying to get klee compiled and installed on a debian 7.8 32-bit > virtual machine for some testing I need to do for my thesis. > > I successfully installed llvm, clang, and stp from their respective > repositories. > > I cloned https://github.com/klee/klee.git this afternoon, > and when I try to configure it using: > $ ./configure --with-llvm=$HOME/llvm-top/llvm > --with-stp=/usr/local/bin --enable-posix-runtime > I get an error saying that: > > gcc: error: unrecognized command-line option '-V' > > I can't figure out where this option is being set nor can I figure out > how to correct it. My only advise would be take a look at the generated ``config.log`` file this may give you an idea of what happened. Although I have to ask if you're using a VM why are you using Debian Wheezy, it's really old. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] [KLEE-dev] printing queries in SMT2 format
Hi, KLEE already has SMTLIBv2 printing support (I presume that's what you mean by SMT2). It is implemented in the ExprSMTLIBPrinter class [1]. You can tell klee to log in this format using ``--use-query-log=all:smt2``. You can also convert .pc files to SMT-LIBv2 format using the ``kleaver`` tool using the the ``-print-smtlib`` command line option. Hope that helps. [1] https://github.com/klee/klee/blob/master/include/klee/util/ExprSMTLIBPrinter.h Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Named Annotations in SMT-LIB2 expressions
Hi Srijan, > While '--smtlib-abbreviation-mode=named' had the desired effect, I also > wanted the mapping of expressions to emitted annotations which I believe can > be obtained from BindingMap in lib/Expr/ExprSMTLIBPrinter.cpp. That is correct. > Could someone shed more light on the same/ correct me if I'm wrong and give > me a few pointers about how the bindings work. I'll be obliged by any help > in this regard. To understand how the printer is used you should take a look at ExprSMTLIBPrinter.h [1] which is very well documented. The named bindings work by first traversing the Expr tree looking for expressions that can be abbreviated before doing any printing. You should look at ExprSMTLIBPrinter::scanAll(...) [2] and ExprSMTLIBPrinter::printExpression(...) [3] [1] https://github.com/klee/klee/blob/master/include/klee/util/ExprSMTLIBPrinter.h [2] https://github.com/klee/klee/blob/master/lib/Expr/ExprSMTLIBPrinter.cpp#L435-L447 [3] https://github.com/klee/klee/blob/master/lib/Expr/ExprSMTLIBPrinter.cpp#L167-L206 Hope that helps. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Invalid recordLoading
On 24 March 2015 at 21:16, Alberto Barbaro wrote: > Hi all, > I'm trying to set up klee with llvm 3.4 following the step by step guide. > Everything looks good apart the last step. When I execute lit -v . I have > this error: > Klee-uclibc.bca failed: invalid record loading module failed: Invalid record That error message suggests that you didn't build klee-uclibc correctly. Try openining the ``klee-uclibc.bca`` file with ``llvm-ar`` to check its a proper archive ``` $ llvm-ar p /path/to/klee-uclibc.bca ``` ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee with llvm-3.6?
On 22 March 2015 at 21:03, Cristian Cadar wrote: > I think there is some rationale for having that code there, as we have > found it useful to have finer-grained control over optimisations in KLEE > in order to improve performance. You can run all LLVM optimisations outside of KLEE using the opt tool. ``opt`` is very flexible and provides all the control you could probably want. I would much rather see an external script or external tool that processes the LLVM bitcode separately. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee with llvm-3.6?
Hi, > There was some discussion about linking in Klee earlier on github > (https://github.com/klee/klee/pull/141). My preference is to remove all > linking from Klee. A provided wrapper script can do the necessary linking > using llvm-link and possibly some opt calls for internalization of functions > and global dead code elimination. What are the current plans for linking > within Klee? I don't know what the current plans are but I would very much like to see optimisation and linking done outside KLEE. I'm one of the authors of the linking code borrowed from LLVM 3.3. I was never happy with it and I would like it removed. It's far too fragile as attempts at porting to LLVM 3.5 and 3.6 have proved. That would simplify KLEE's internals and leave it up to the author of the LLVM bitcode to do linking and optimisation. Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] whole-program-llvm
Hi, > Exception: Could not find ".llvm_bc" ELF section in > "/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64" You probably didn't use whole-program-llvm for your compilation process if you see this message. You should check if ``make`` was actually using wllvm, my guess it wasn't (try ``make --just-print``) It's just a guess but you should probably be passing CC and CXX to the configure commands rather than just make ``` export WLLVM_OUTPUT=DEBUG export CC=wllvm export CXX=wllvm++ ../configure --disable-nls CFLAGS="-g" make ``` The ``export WLLVM_OUTPUT=DEBUG`` will cause wllvm to emit lots of debuggin information when it runs. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] whole-program-llvm
Hi, > it reports the error that > > ERROR:File > "/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64.o" > of type ELF_OBJECT cannot be used. You're supposed to run ``extract-bc`` on the final executable i.e. ``base64``. You tried running ``extract-bc`` on one of the constituent object files of ``base64`` which will not work. Please read the whole-program-llvm README [1] more carefully. [1] https://github.com/travitch/whole-program-llvm/blob/master/README.md ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] coreutils on KLEE3.4
Hi Zhiyi, Please do reply-all when using the mailing list so that klee-dev gets CC'ed. On 18 March 2015 at 08:32, Zhiyi Zhang wrote: > Hi Dan, > > Thank you for your reply very much. > > I am still confused that do you mean coreutills cannot be run on KLEE > compiled with > LLVM 3.4, expect I use the whole-program-llvm? No. I am saying - ``klee-gcc`` is just a wrapper script (read the code) for ``llvm-gcc``. - ``llvm-gcc`` will emit LLVM bitcode in the format used by LLVM 2.9. - KLEE supports being built with different versions of LLVM. - You have built KLEE with LLVM 3.4 therefore you cannot use ``llvm-gcc`` (the LLVM bitcode will be incompatible) therefore you cannot use the ``klee-gcc`` wrapper script. You have three options * Use whole-program-llvm. This is what I would advise. * Use ``klee-clang`` [1] which is wrapper script around clang. * Use KLEE with llvm 2.9, llvm-gcc and the klee-gcc wrapper script. [1] https://github.com/klee/klee/pull/213 ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] coreutils on KLEE3.4
On 18 March 2015 at 08:17, Zhiyi Zhang wrote: > Hi all, > > I have built the KLEE3.4 on Ubuntu14.10 and the Tutorial get_sign and Regexp > can also be run by KLEE3.4. I used clang to compile programs and run .bc > file on KLEE. However, when I built the coreutils on KLEE3.4 and make > obj-llvm with makeCC=/full/path/to/klee/scripts/klee-gcc,it reports some > errors. The errors are in enclosed in the attachment. klee-gcc is only meant for llvm-gcc and not for clang, the fact it worked probably suggests you have llvm-gcc on your PATH. llvm-gcc will not produce LLVM bitcode that is compatible with KLEE compiled with LLVM 3.4. If you intend to use clang with KLEE then I would advise you use the whole-program-llvm [1] to build your application. [1] https://github.com/travitch/whole-program-llvm Thanks, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] about klee inputs
On 11 March 2015 at 17:13, douglas schroeder wrote: > Hello, thanks for the reply. > another question. > in my tests, almost all generated inputs are zeros. > > 0: name: 'string' > object0: size: 8 > object0: data: '\x00\x00\x00\x00\x00\x00\x00\x00' > object1: name: 'data' > object1: size: 1 > object1: data: '\x00' > > is there a way to improve the generation of inputs? > I don't know, but what is your definition of improve? Also please make sure you keep klee-dev CC'ed so that the discussion remains public. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] about klee inputs
Hi, On 10 March 2015 at 22:27, douglas schroeder wrote: > hello. > I have the following question. > why when I hava a constraint like "if(x < 0)", klee always set the value of > x to -2147483648?? > why not something like "-1"? It is up to KLEE's constraint solver to pick a value and if the constraint is x < 0 then -2147483648 is perfectly fine. If you used a different solver in KLEE then you could quite easily get a different value. If you desire a particular value you can use klee_prefer_cex() to suggest to KLEE a particular value for x. See [1] as an example. [1] https://github.com/klee/klee/blob/master/test/Feature/PreferCex.c ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE pthread support
On 3 March 2015 at 06:45, Insu Yun wrote: > Dear all, > > I want to run KLEE on program with pthread. I know that > cloud9(http://cloud9.epfl.ch/) supports pthread. However, it is built on > old-version KLEE and the project is not active. Therefore I want to add > pthread feature to KLEE. > > I analyzed cloud9 code and I made KLEE with single thread and single > process. (As you know, KLEE has no concept of thread and process). Now I am > trying to add pthread_create function support. For that, I copied a > test(Runtime/Synchronization/Mutex.c) from cloud9. It gives me a following > error. > > KLEE: WARNING: undefined reference to function: __xstat64 That's a warning and not an error. KLEE will emit this warning if your LLVM IR references a function without a body. Your problem is somewhere else. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)
> Dan, the message starts with "We tried two versions of STP (r940 and the > latest)" :) Yes but - I was asking if you had STP built with assertions when trying to reproduce the issue. It is obvious the the OP had assertions enabled when they ran their build of KLEE. - The stacktrace shown by the old OP is for the old STP - The OP could have cloned the latest code from the old stp SVN repo which is very out of date ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)
On 27 February 2015 at 10:52, Cristian Cadar wrote: > I cannot reproduce this on my machine. Can you open an issue at > https://github.com/klee/klee/issues, giving more details on your > configuration and how you ran KLEE? Do you have STP built with assertions? They've been enabled by default in the latest upstream STP but I'm not sure if this the case for r940. I think we should stop recommending people using r940, it's really old, doesn't even build on new linux distros and has bugs that have been fixed in the upstream version. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Dockerizing Klee
Hi, > I think it would be useful to have an official repository for the dockerized > KLEE, which we would recommend to new users on the KLEE website, and which > would be maintained as part of the KLEE project on GitHub > (https://github.com/klee). Also, it would be useful to automatically update > an associated KLEE Docker image and upload it to the Docker registry either > after each KLEE commit, or at regular time intervals. The docker registry provides a service where you can link it with your github repository and it will automatically rebuild the docker image on every commit. I use this for several docker images I have (e.g. [1] [2] and [3]) [1] https://github.com/delcypher/gpuverify-docker [2] https://github.com/delcypher/boogaloo-docker [3] https://github.com/delcypher/klee-cl-docker ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
