search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

Speculation v1.0 #356

Closed rasoolmaghareh closed 4 years ago

rasoolmaghareh commented 4 years ago

@xuanlinhha: I have ran make check. There are 4 new failures on the programs. Can you please check and fix it. The errors are in Executor::branchFork function:

FAIL: KLEE :: Feature/DanglingConcreteReadExpr.c (61 of 185)
******************** TEST 'KLEE :: Feature/DanglingConcreteReadExpr.c' FAILED ********************
Script:
--
/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang -I/home/sajjad/Tracer-X/klee/include /home/sajjad/Tracer-X/klee/test/Feature/DanglingConcreteReadExpr.c -emit-llvm -O0 -c -o /home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp1.bc
rm -rf /home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 --optimize=false --output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out -no-interpolation /home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp1.bc
grep "total queries = 2" /home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out/info
--
Exit Code: -11

Command Output (stdout):
--
Command 0: "/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang" "-I/home/sajjad/Tracer-X/klee/include" "/home/sajjad/Tracer-X/klee/test/Feature/DanglingConcreteReadExpr.c" "-emit-llvm" "-O0" "-c" "-o" "/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp1.bc"
Command 0 Result: 0
Command 0 Output:

Command 0 Stderr:
/home/sajjad/Tracer-X/klee/test/Feature/DanglingConcreteReadExpr.c:11:3: warning: implicit declaration of function 'klee_make_symbolic' is invalid in C99 [-Wimplicit-function-declaration]
  klee_make_symbolic(&x, sizeof x);
  ^
/home/sajjad/Tracer-X/klee/test/Feature/DanglingConcreteReadExpr.c:21:3: warning: implicit declaration of function 'klee_silent_exit' is invalid in C99 [-Wimplicit-function-declaration]
  klee_silent_exit(0);
  ^
2 warnings generated.

Command 1: "rm" "-rf" "/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out"
Command 1 Result: 0
Command 1 Output:

Command 1 Stderr:

Command 2: "/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee" "-solver-backend=z3" "--optimize=false" "--output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out" "-no-interpolation" "/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp1.bc"
Command 2 Result: -11
Command 2 Output:

Command 2 Stderr:
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Feature/Output/DanglingConcreteReadExpr.c.tmp.klee-out"
Using Z3 solver backend
0  libLLVM-3.4.so  0x00007ff091b7f052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007ff091b7e7c4
2  libpthread.so.0 0x00007ff09127c390
3  klee            0x000000000047d710 klee::Executor::branchFork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 480
4  klee            0x00000000004878d1 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 8161
5  klee            0x000000000048d080 klee::Executor::run(klee::ExecutionState&) + 3440
6  klee            0x000000000048e087 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1703
7  klee            0x000000000045f68d main + 12765
8  libc.so.6       0x00007ff08ed22830 __libc_start_main + 240
9  klee            0x0000000000467e59 _start + 41

--

********************
FAIL: KLEE :: Feature/KleeReportError.c (75 of 185)
******************** TEST 'KLEE :: Feature/KleeReportError.c' FAILED ********************
Script:
--
/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang -I/home/sajjad/Tracer-X/klee/include /home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c -g -emit-llvm -O0 -c -o /home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp2.bc
rm -rf /home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 -no-interpolation --output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out --emit-all-errors /home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp2.bc 2>&1 | FileCheck /home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c
ls /home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out/ | grep .my.err | wc -l | grep 2
--
Exit Code: 1

Command Output (stdout):
--
Command 0: "/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang" "-I/home/sajjad/Tracer-X/klee/include" "/home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c" "-g" "-emit-llvm" "-O0" "-c" "-o" "/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp2.bc"
Command 0 Result: 0
Command 0 Output:

Command 0 Stderr:
/home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c:11:3: warning: implicit declaration of function 'klee_make_symbolic' is invalid in C99 [-Wimplicit-function-declaration]
  klee_make_symbolic(&x, sizeof x);
  ^
/home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c:23:5: warning: implicit declaration of function 'klee_report_error' is invalid in C99 [-Wimplicit-function-declaration]
    klee_report_error(__FILE__, __LINE__, "My error", "my.err");
    ^
2 warnings generated.

Command 1: "rm" "-rf" "/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out"
Command 1 Result: 0
Command 1 Output:

Command 1 Stderr:

Command 2: "/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee" "-solver-backend=z3" "-no-interpolation" "--output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out" "--emit-all-errors" "/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp2.bc"
Command 2 Result: -11
Command 2 Output:

Command 2 Stderr:

Command 3: "FileCheck" "/home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c"
Command 3 Result: 1
Command 3 Output:

Command 3 Stderr:
/home/sajjad/Tracer-X/klee/test/Feature/KleeReportError.c:20:12: error: expected string not found in input
 // CHECK: KleeReportError.c:23: My error
           ^
<stdin>:1:1: note: scanning from here
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out"
^
<stdin>:1:74: note: possible intended match here
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Feature/Output/KleeReportError.c.tmp.klee-out"
                                                                         ^

--

********************
FAIL: KLEE :: Feature/LowerSwitch.c (83 of 185)
******************** TEST 'KLEE :: Feature/LowerSwitch.c' FAILED ********************
Script:
--
/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang -I/home/sajjad/Tracer-X/klee/include /home/sajjad/Tracer-X/klee/test/Feature/LowerSwitch.c -emit-llvm -g -c -o /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.bc
rm -rf /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 --no-interpolation --output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out --exit-on-error --allow-external-sym-calls --switch-type=internal /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.bc
not test -f /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out/test000010.ktest
rm -rf /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 --no-interpolation --output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out --exit-on-error --allow-external-sym-calls --switch-type=simple /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.bc
test -f /home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out/test000010.ktest
--
Exit Code: -11

Command Output (stdout):
--
Command 0: "/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang" "-I/home/sajjad/Tracer-X/klee/include" "/home/sajjad/Tracer-X/klee/test/Feature/LowerSwitch.c" "-emit-llvm" "-g" "-c" "-o" "/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.bc"
Command 0 Result: 0
Command 0 Output:

Command 0 Stderr:
/home/sajjad/Tracer-X/klee/test/Feature/LowerSwitch.c:13:11: warning: implicit declaration of function 'klee_range' is invalid in C99 [-Wimplicit-function-declaration]
  int c = klee_range(0, 256, "range");
          ^
1 warning generated.

Command 1: "rm" "-rf" "/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out"
Command 1 Result: 0
Command 1 Output:

Command 1 Stderr:

Command 2: "/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee" "-solver-backend=z3" "--no-interpolation" "--output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out" "--exit-on-error" "--allow-external-sym-calls" "--switch-type=internal" "/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.bc"
Command 2 Result: -11
Command 2 Output:

Command 2 Stderr:
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Feature/Output/LowerSwitch.c.tmp.klee-out"
Using Z3 solver backend
KLEE: WARNING: undefined reference to function: printf
0  libLLVM-3.4.so  0x00007f02655d8052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007f02655d77c4
2  libpthread.so.0 0x00007f0264cd5390
3  klee            0x000000000047d710 klee::Executor::branchFork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 480
4  klee            0x00000000004878d1 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 8161
5  klee            0x000000000048d080 klee::Executor::run(klee::ExecutionState&) + 3440
6  klee            0x000000000048e087 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1703
7  klee            0x000000000045f68d main + 12765
8  libc.so.6       0x00007f026277b830 __libc_start_main + 240
9  klee            0x0000000000467e59 _start + 41

********************
FAIL: KLEE :: Runtime/POSIX/FD_Fail2.c (124 of 185)
******************** TEST 'KLEE :: Runtime/POSIX/FD_Fail2.c' FAILED ********************
Script:
--
/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang -I/home/sajjad/Tracer-X/klee/include /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/FD_Fail2.c -emit-llvm -O0 -c -o /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp1.bc
rm -rf /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 --no-interpolation --output-dir=/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out --libc=uclibc --posix-runtime --search=dfs /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp1.bc --sym-files 1 10 --max-fail 2
FileCheck -input-file=/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/assembly.ll /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/FD_Fail2.c
test -f /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/test000001.ktest
test -f /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/test000002.ktest
test -f /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/test000003.ktest
test -f /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/test000004.ktest
not test -f /home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out/test000005.ktest
--
Exit Code: -11

Command Output (stdout):
--
Command 0: "/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang" "-I/home/sajjad/Tracer-X/klee/include" "/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/FD_Fail2.c" "-emit-llvm" "-O0" "-c" "-o" "/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp1.bc"
Command 0 Result: 0
Command 0 Output:

Command 0 Stderr:

Command 1: "rm" "-rf" "/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out"
Command 1 Result: 0
Command 1 Output:

Command 1 Stderr:

Command 2: "/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee" "-solver-backend=z3" "--no-interpolation" "--output-dir=/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out" "--libc=uclibc" "--posix-runtime" "--search=dfs" "/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp1.bc" "--sym-files" "1" "10" "--max-fail" "2"
Command 2 Result: -11
Command 2 Output:

Command 2 Stderr:
KLEE: NOTE: Using klee-uclibc : /home/sajjad/Tracer-X/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/sajjad/Tracer-X/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Runtime/POSIX/Output/FD_Fail2.c.tmp.klee-out"
Using Z3 solver backend
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
0  libLLVM-3.4.so  0x00007f2edbdad052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007f2edbdac7c4
2  libpthread.so.0 0x00007f2edb4aa390
3  klee            0x000000000047d710 klee::Executor::branchFork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 480
4  klee            0x00000000004878d1 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 8161
5  klee            0x000000000048d080 klee::Executor::run(klee::ExecutionState&) + 3440
6  klee            0x000000000048e087 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1703
7  klee            0x000000000045f68d main + 12765
8  libc.so.6       0x00007f2ed8f50830 __libc_start_main + 240
9  klee            0x0000000000467e59 _start + 41

--
xuanlinhha commented 4 years ago

If you remove "-no-interpolation", it will work fine

rasoolmaghareh commented 4 years ago

Merging the code for Tracer-X Speculation.

Speculation types: 1- Coverage 2- Bug finding

Speculation strategies: 1- Timid 2- Aggressive 3- Custom