Andrea Mattavelli

DecisionProcedureTest fails due to hard-coded z3 path

2

Hard-coding paths is a bad solution, since the build will likely fail on different environments. A possible solution would be to rely on an environment variable, and then `assumeTrue` that...

CVE 2014 now crashes

5

```bash /data/klee-slicing/klee-build/bin/klee --libc=uclibc --search=dfs --skip-functions=_asn1_get_octet_string:1092,asn1_delete_structure:1374 --no-output test.bc 32 [..] klee: /data/klee-slicing/klee/lib/Core/Executor.cpp:4526: void klee::Executor::onRecoveryStateWrite(klee::ExecutionState&, klee::ref, const klee::MemoryObject*, klee::ref, klee::ref): Assertion `isa(address)' failed. 0 klee 0x0000000001030c72 llvm::sys::PrintStackTrace(_IO_FILE*) + 50 1 klee 0x00000000010304cc...

Currently we dump many interesting things. Unfortunately, on large applications this leads to huge files: ```bash andrea@ruchill$ ll -h coreutils-6.10/obj-llvm/src/klee-last/sa.log -rw-rw-r-- 1 andrea andrea 3.4M Aug 14 09:23 coreutils-6.10/obj-llvm/src/klee-last/sa.log ```

KLEE crashes on dwarfdump

3

```bash /home/andrea/work/klee-slicing/klee-build/bin/klee --link-llvm-lib=/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc -skip-functions=dwarf_record_cmdline_options dwarfdump.bc -ka ../../regressiontests/marinescu/hello.original KLEE: Linking in library: /home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc. KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/dwarf-20110612/dwarfdump/klee-out-48" Using STP solver backend KLEE: Runnining reachability analysis... KLEE: Runnining pointer analysis... KLEE:...

KLEE crashes on Coreutils 6.10 ptx

3

Invocation `/home/andrea/work/klee-slicing/klee-build/bin/klee --posix-runtime -libc=uclibc --search=random-state --max-time=360. --skip-functions=usage,quotearg ptx.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout` Output: ```bash ... %2 = load i8* %1,...

The issue is mainly due to how LLVM handles the returned struct: ```llvm define i32 @main(i32 %argc, i8** %argv, i8** %envp) #0 { entry: %retval = alloca i32, align 4...

1. Configured CMake with ASAN: ```bash $ CXXFLAGS="-fno-rtti -fsanitize=address -fno-omit-frame-pointer" CFLAGS="-fsanitize=address -fno-omit-frame-pointer" cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/andrea/work/klee-slicing/klee-uclibc -DLLVM_CONFIG_BINARY=/usr/local/bin/llvm-config -DENABLE_UNIT_TESTS=OFF -DKLEE_RUNTIME_BUILD_TYPE=Release+Asserts -DENABLE_SYSTEM_TESTS=ON -DSVF_ROOT_DIR=/home/andrea/work/klee-slicing/SVF -DDG_ROOT_DIR=/home/andrea/work/klee-slicing/dg -DSLICING_ROOT_DIR=/home/andrea/work/klee-slicing/se-slicing ../klee ``` 2. Compiled with: ```bash...