Re: [klee-dev] KLEE failed to build cleanly with LLVM 3.3
Hello,
Daniel Liew on 2014-09-17:
On 17 September 2014 20:10, Mark R. Tuttle tut...@acm.org wrote:
I just did a git pull to grab the latest commit (2497fdc) and ran into
trouble building against LLVM 3.3 and running the regression tests.
Build failed in file src/tools/klee/main.cpp in function
KleeHandler::openOutputFile
#if LLVM_VERSION_CODE = LLVM_VERSION(3,5)
f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_None);
#elif LLVM_VERSION_CODE = LLVM_VERSION(3,0)
f = new llvm::raw_fd_ostream(path.c_str(), Error,
llvm::sys::fs::F_Binary);
#else
f = new llvm::raw_fd_ostream(path.c_str(), Error,
llvm::raw_fd_ostream::F_Binary);
#endif
because llvm::sys::fs::F_Binary was not defined. LLVM 3.3 source code seems
to define llvm::raw_fd_ostream::F_Binary and not llvm::sys::fs:F_Binary. I
changed the reference to LLVM version 3.0 to 3.4 and the build succeeded.
We are currently targeting LLVM2.9 and LLVM3.4 [1] and are not testing
LLVM3.3 build support. Do you need to use LLVM3.3 for any particular
reason?
We'd happily accept a patch to fix your compilation error provided it
doesn't break the configurations we're testing right now.
I had the same problem a while ago, and it turns out the correct guard
is = LLVM_VERSION(3,4). I've attached a patch.
Thanks,
Sean Bartell
From b7d1273c308a46bbe32c3c156dc70052026035d6 Mon Sep 17 00:00:00 2001
From: Sean Bartell yot...@yotann.org
Date: Mon, 22 Sep 2014 22:06:42 -0500
Subject: [PATCH] Fix compilation with LLVM 3.0-3.3.
F_Binary was actually moved in LLVM 3.4 (r186447), not 3.0.
---
tools/klee/main.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index fce4e31..a92aa55 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -379,7 +379,7 @@ llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string filename) {
std::string path = getOutputFilename(filename);
#if LLVM_VERSION_CODE = LLVM_VERSION(3,5)
f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_None);
-#elif LLVM_VERSION_CODE = LLVM_VERSION(3,0)
+#elif LLVM_VERSION_CODE = LLVM_VERSION(3,4)
f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_Binary);
#else
f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary);
--
2.1.0
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Use Klee with Java?
Zhenyu Zhou on 2015-06-20: I'm looking for a tool for symbolic execution and find that Klee is a fantastic tool. But now I'm wondering whether Klee can analyse JAVA codes (or class files)? I have searched in the mail list and found the same question is posted several years ago. Does anyone know are there any progresses in this direction? KLEE only understands LLVM bitcode--this is part of the fundamental design of KLEE. If you need to use KLEE on Java code, you might be able to use RoboVM[0] or VMKit[1] (unmaintained) to convert Java into LLVM bitcode. However, this will require a lot of work to get usable bitcode, especially when you have to deal with Java libraries and OS interaction. It will be much easier to use a Java-specific tool instead of KLEE, such as JPF-symbc[2]. [0] http://docs.robovm.com/ [1] http://vmkit.llvm.org/ [2] http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Same variable twice in ktest-tool output
Hi,
Alexander Kampmann on 2015-06-25:
For my test input, the ktest-tool outputs the same object name twice and
skips another object.
As you can see, there are two objects named 'var2' and no object named
'var1'. The c code is:
char *var1 = Hallo;
char *var2 = Hallo;
klee_make_symbolic(var1, 6*sizeof(char), var1);
klee_assume(var1[5] == 0);
klee_make_symbolic(var2, 6*sizeof(char), var2);
klee_assume(var2[5] == 0);
Hallo is a string constant, and the compiler puts it in read-only memory.
Because it's read-only, the compiler is allowed to combine both instances of
Hallo to save memory. You aren't supposed to treat the string constants as
writable and if you compile with -Wall you'll get a warning to that effect.
klee_make_symbolic essentially writes to the read-only memory and that is
causing issues.
What you really want is this:
char var1[] = {Hallo};
char var2[] = {Hallo};
Both variables will get separate instances of Hallo in writable memory, so
KLEE should work as expected.
It's interesting that KLEE gets the names confused. I guess it fills the string
constant with symbolic values, then overwrites those symbolic values with *new*
symbolic values, and also overwrites the old name for that memory location with
the new name. You see both sets of symbolic values, but KLEE only remembers the
new name for them.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Path Search Heuristics
Zhiyi Zhang on 2015-05-27: I have found the error report when I only used search==nurs:covnew as the path search heuristic. It is klee: ModuleUtil.cpp:435: llvm::Function* klee::getDirectCallTarget(llvm::CallSite): Assertion `0 FIXME: Unresolved direct target for a constant expression.' failed. There are a few things you can try: 1. Add the `-optimize` option when you run KLEE. That may optimize out the bitcode triggering the assertion. 2. Apply [my patch](https://github.com/yotann/klee/commit/dff4069042e6f7b4bc7211b8e9ba3377ee01c33c) that fixes the assertion in certain cases. 3. Modify KLEE to call `ce-dump()` right before the assertion, which will print out the value that causes the problem. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] About KLEE
eric.ri...@huskers.unl.edu on 2015-05-30: I'm not sure that what you are looking for exists. Klee is designed to test programs and create test suites. It will find assertion violations and other common errors. If you're looking to verify that a particular path through the program is semantically correct, however, you're going to have to find some type of specification for each program. From that point, you could use the inputs/ouputs generated by Klee to make sure they all match the specifications. As I said, however, I don't know where you will be able to find any formal specifications for core-utils. The only option I can think of is to use some competing implementation of the core-utils and verify that they each produce the same outputs given the same inputs. That reminds me, the [original KLEE paper](http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf) crosschecked Coreutils against Busybox (section 5.5). It's not the same as an oracle, though, and it will have lots of false positives due to different feature sets. I'm not sure whether their infrastructure to make crosschecking automatic is open source. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Question about "-load" option
Bin Lin on 2015-09-08: Hello Martin, Thank you! After I set the LD_RUN_PATH, what command should I use in my case? If I use the command './klee main.bc -load=path-to-lib/libfoo.so', I still get the same error. So how to load the dynamic library in my case? Try these, maybe one will work: LD_RUN_PATH=path-to-lib ./klee main.bc ./klee -load=path-to-lib/libfoo.so main.bc In addition, I do not understand why the '-load=path-to-lib/libfoo.so' is part of the arguments for my tested application not for KLEE. As far as I know, KLEE has the '-load' option. It's because of the order. If you use './klee main.bc -load=...', -load is passed through to the application. If you use './klee -load=... main.bc', -load is handled by KLEE. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Question about "-load" option
Bin Lin on 2015-09-09: Both './klee -load=path-to-lib/libfoo.so main.bc' and LD_PRELOAD work for this simple case. But for my situation, the "main()" function of C program is wrapped in the dynamic library not in the program, in which case they do not work. It complains that " 'main' function not found in the module". Does any one have ideas how to fix this? Various parts of KLEE require 'main' to be in the program's bitcode file (main.bc). Your best option is to compile the library as LLVM bitcode, like the program, and link the library and program together somehow so you just have one bitcode file to give to KLEE. On Tue, Sep 8, 2015 at 2:48 PM, Sean Bartell <s...@yotann.org> wrote: Bin Lin on 2015-09-08: Hello Martin, Thank you! After I set the LD_RUN_PATH, what command should I use in my case? If I use the command './klee main.bc -load=path-to-lib/libfoo.so', I still get the same error. So how to load the dynamic library in my case? Try these, maybe one will work: LD_RUN_PATH=path-to-lib ./klee main.bc ./klee -load=path-to-lib/libfoo.so main.bc In addition, I do not understand why the '-load=path-to-lib/libfoo.so' is part of the arguments for my tested application not for KLEE. As far as I know, KLEE has the '-load' option. It's because of the order. If you use './klee main.bc -load=...', -load is passed through to the application. If you use './klee -load=... main.bc', -load is handled by KLEE. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Mixed concrete-symbolic execution
Riyad Parvez on 2015-09-23: I was wondering whether it's possible mixed concrete-symbolic execution in KLEE? Like S2E, where some of the input to the program will be symbolic and other input will be concrete. All inputs are concrete by default. You can make certain inputs symbolic by either calling klee_make_symbolic from within the program, or by using uclibc and the POSIX wrapper and using arguments like -sym-args. Keep in mind KLEE will run the program very slowly, even for parts of the code where there are no symbolic values involved. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Use of --optimize flag
RAJDEEP MUKHERJEE on 2016-06-23: In default mode, klee uses dfs search strategy with incremental solving. What additional optimisations does Klee perform with the --optimize switch ? The --optimize switch causes KLEE to run standard compiler optimizations on the subject program before starting to execute it. It's similar to compiling the subject program with an option like -O2. One difference is that if you tell KLEE to link the subject with uclibc or the POSIX runtime, KLEE will do optimization *after* linking, which gives extra opportunities for inlining. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
