[klee-dev] How to get （or capture ） the value of replaying a test case and the usage of KLEE
Andrew Santosa
santosa_1999 at yahoo.com
Sun Nov 27 14:15:38 GMT 2016
On no. 4, I think Lei's approach is probably fine for their purpose, assuming what needs to be accomplished here is simply making a, b, and c represent nondeterministic int input.
But since scanf is a function that reads from the standard input, if one goes through the Coreutils tutorial (thanks to Chengyu for the pointer), one would have the idea that instead of replacing scanf with klee_make_symbolic, one could use:
-sym-stdin <STDIN_SIZE>
Like this:
klee --libc=uclibc --posix-runtime program.bc -sym-stdin 8
In my experiment, program.bc is the bitcode of the following program.
#include <stdio.h>
int main(int argc, char **argv) {
int a, b, c;
int x = 0;
scanf("%d%d%d", &a, &b, &c);
if (a > 0) { x++; } else { x+=2; }
if (b > 0) { x++; } else { x+=2; }
if (c > 0) { x++; } else { x+=2; }
return 0;
}
However, the program still waits for input, and of course after one enters
the right input the program explores only 1 path instead of 8. I am wondering
why myself. Perhaps scanf is a special case that doesn't work with symbolic stdin
(in the similar way its complement printf needs concrete arguments).
Best,
Andrew
On Saturday, 26 November 2016, 20:13, Chengyu Zhang <dale.chengyu.zhang at gmail.com> wrote:
Hi Lei,
Here is my advice:
1. KLEE has support for C and limited support for C++. If you want to test C++ program, you could take a look at KLOVER project.
you can find more information in the paper of KLOVER : http://www.cs.utah.edu/~ligd/publications/KLOVER-CAV11.pdf
2. You could make a little script to solve the problem. I need the full text of your replayingtestcaseesstorageinputoutput.sh script to find what's wrong with the script.
But I think the command like : "KTEST_FILE=klee-last/test000001.ktest ./a.out >> a.txt" in your email is not reasonable, you may need the return code of your tested program, you should redirect the result of "echo $?" to a.txt rather than "KTEST_FILE=klee-last/test000001.ktest ./a.out".
3. You could use klee-reply tool. "To use the klee-replay tool, we just tell it the executable to run and the .ktest file to use"
there is a example of how to use klee-reply on http://klee.github.io/tutorials/testing-coreutils/
4. You should read the tutorial of how to test coreutils, then you could find the way to deal with multiple arguments.
Here is the link: http://klee.github.io/tutorials/testing-coreutils/, the answer is in Step4.
Cheers,
Chengyu
2016-11-24 11:26 GMT+08:00 乔磊 <qiaoleioffice at 163.com>:
Dear all,
>I am a new user of KLEE, I am learning some knoeledge about symbolic execution.
>
>
>I saw the usage of KLEE from the website http://klee.github.io/.
>
>I have some questions as follows:
>
>
>1. Does KLEE just only generate testcases for C program？
>
>
>
>
>2. How to get （or capture ） the value after replaying a test case and how to store the value of replaying a test case into a file.
>
>
>I saw one method from the website：http://klee.github.io/ tutorials/testing-function/
>
>
>$ gcc -L path-to-klee-root/Release+Asse rts/lib/ get_sign.c -lkleeRuntest $ KTEST_FILE=klee-last/test00000 1.ktest ./a.out $ echo $? 1
>After I input and execute the command of KTEST_FILE=klee-last/test00000 1.ktest ./a.out, the result of running the testcase on C program will print a value on the screen. It looks like the function of the Linux command "echo" . I just see it on the screen. I can't get （or capture ）the value after executing the command of KTEST_FILE=klee-last/test00000 1.ktest ./a.out.
>Is there any mistakes on my usage on KLEE.
>
>
>
>
>When I use the command as follows：
>KTEST_FILE=klee-last/test00000 1.ktest ./a.out >> a.txt
>There is no result. How can I store the value of running the testcase on a program.
>
>
>
>
>
>
>When I write the command：KTEST_FILE=klee-last/$ testcase./a.out into a bash file named replayingtestcaseesstorageinpu toutput.sh
>
>
>Then I execute this bash script as follows. Some errors information will print on the screen? I don't know the reason of occuring error. Can you give
>me a help?
>
>
>
>
>
>
>
>
>3.How to run the test cases generated by KLEE on our c program ?
>
>
> just one method as follows?
>$ gcc -L path-to-klee-root/Release+Asse rts/lib/ get_sign.c -lkleeRuntest $ KTEST_FILE=klee-last/test00000 1.ktest ./a.out $ echo $? 1
>Do you have other method or other usage？
>
>
>
>
>4. There are only simple example on the KLEE website http://klee.github.io/ ， the tutorial one and two just give two examples. when my C program has two or three , even more than three input arguments，How to use klee ？
>
>
>When I use klee. I just replace the input variable of the statement “scanf("%d%d%d,&a，&b，&c);”to the function of klee_make_symbolic(&a,sizeof(a),"a")just like the following ; Do I need replace other variable or statement？
>
>
>When the c program has no the statement of “scanf("%d%d%d,&a，&b，&c);” How to make symbolic use klee to generate the testcase？
>
>
>Is the following usage right？
>int main() { int a; klee_make_symbolic(&a, sizeof(a), "a"); return get_sign(a); }
>when there is one input variable ：scanf("%d",&a); I replaceed the Statementscanf("%d",&n)to klee_make_symbolic(&a,sizeof(a),"a");
>when there are two input variables ：scanf("%d%d‘’,&a，&b);I replaceed this statement to two statements klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b");
>when there are three input variables ： scanf("%d%d%d,&a，&b，&c);I replaceed this statement to three statements klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b"); klee_make_symbolic(&c,sizeof(c),"c");
>Is all right？
>
>5.How can I get the learning materials and Instructions of using KLEE, If you have, please send to me by Email. which website or internet forum can I search some usages materials of KLEE？
>
>
>
>
>
>
>Thank you very much.
>
>
>Best wishes.
>
>
>Beijing Institute of Technology
>
>School of Computer Science and Technology
>
>
>Beijing Institute of Technology : 5 South Zhongguancun Street, Haidian District, Beijing Postcode: 100081, CHINA
>
>Lei Qiao
>E-mail: qiaoleioffice at 163.com
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>______________________________ _________________
>klee-dev mailing list
>klee-dev at imperial.ac.uk
>https://mailman.ic.ac.uk/mailm an/listinfo/klee-dev
>
>
--
张枨宇 Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.com
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
More information about the klee-dev
mailing list