Hi again I have continued with my test for try to understand klee, and I'm reading some articles about projects with klee that made the coreutils test as in the OSDI 2008 but with more recent versions of klee.
I'm trying to replicate the case of mkdir. I am testing coreutils6-10 and coreutils6-11. I found one error: ptr.error the 6.10 version and with the 6.11 it didn't appear. The problem is that I really don't understand the parameters that I have to use for crash mkdir with the error that I have. Moreover, it doesn't look the same error than the results of the OSDI, so I suppose something is wrong with my test. How should I execute this case for replicate the error with the mkdir that is in obj-gcov? I would like know how to reproduce the errors how obtain the parameters that I really don't understand in the test outputs. When I did klee-replay, it show "./mkdir" "-Z@@@@@@@@" "--" "sym-files" "2" "8" "--sym-dirs" "1" "1" maybe I am doing something bad in the execution line of klee. The execution line is the next one: (I based my line in the article:Symbolic Execution in Difficult Environments<http://www.cs.cmu.edu/%7Edwrensha/15-745/final.pdf> ) klee --simplify-sym-indices --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-stp --use-cex-cache --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --max-sym-array-size=4096 --max-instruction-time=10 --max-time=600 --watchdog --max-memory-inhibit=false --max-static-cpfork-pct=1 --randomize-fork --use-random-path --use-interleaved-covnew-NURS --use-batching-search --batch-instructions 10000 --init-env mkdir.bc --sym-args 0 1 10 --sym-args 0 2 2 sym-files 2 8 --sym-dirs 1 1 Results KLEE: done: explored paths = 26243 KLEE: done: avg. constructs per query = 191 KLEE: done: total queries = 5355 KLEE: done: valid queries = 2723 KLEE: done: invalid queries = 2632 KLEE: done: query cex = 5355 KLEE: done: total instructions = 45464814 KLEE: done: completed paths = 26243 KLEE: done: generated tests = 76 I found an error in one case: ~/llvm/coreutils-6.10/obj-llvm/src/prueba3$ ktest-tool --write-ints test000039.ktest ktest file : 'test000039.ktest' args : ['mkdir.bc', '--sym-args', '0', '1', '10', '--sym-args', '0', '2', '2', 'sym-files', '2', '8', '--sym-dirs', '1', '1'] num objects: 5 object 0: name: 'n_args' object 0: size: 4 object 0: data: 1 object 1: name: 'arg0' object 1: size: 11 object 1: data: '-Z@@@@@@@@\x00' object 2: name: 'n_args' object 2: size: 4 object 2: data: 1 object 3: name: 'arg1' object 3: size: 3 object 3: data: '--\x00' object 4: name: 'model_version' object 4: size: 4 object 4: data: 1 Using klee replay: ~/llvm/coreutils-6.10/obj-gcov/src$ klee-replay ./mkdir ../../obj-llvm/src/prueba3/test000039.ktest klee-replay: TEST CASE: ../../obj-llvm/src/prueba3/test000039.ktest klee-replay: ARGS: "./mkdir" "-Z@@@@@@@@" "--" "sym-files" "2" "8" "--sym-dirs" "1" "1" klee-replay: EXIT STATUS: CRASHED signal 11 (0 seconds) Doing the same execution during 120 seg the error is: :~/llvm/coreutils-6.10/obj-gcov/src$ klee-replay ./mkdir ../../obj-llvm/src/prueba1/klee-out-37/test000024.ktest klee-replay: TEST CASE: ../../obj-llvm/src/prueba1/klee-out-37/test000024.ktest klee-replay: ARGS: "./mkdir" "--c=@@" "--" "sym-files" "2" "8" "--sym-dirs" "1" "1" klee-replay: EXIT STATUS: CRASHED signal 11 (0 seconds) I hope with this example someone can explain me a few more about how klee is working Thanks in advance Marta 2012/3/2 marta vic <[email protected]> > Hello > > I'm starting with klee, I build llvm 2.8 an klee in ubuntu11.10 > and I build COREUTILS 6.10 and 6.11 > I'm trying to reproduce some examples of the paper OSDI-2008 > But I really don't know if it's working. I don't know what results I must > obtain. > I followed all the tutorials of klee (and it seems working). And I tried > to search information in the mailing list > but then when I try to execute the cases of the paper I think I not doing > correctly. > > I hope someone can help me, for know how to start. > my questions in general are: > > 1.- How I know that is correct the output of klee? What is the meaning of > the error write error > : Input/output errorTry? > > 2.- How I can found that for tr.bc the error is "a buffer overflow error > at line 18 of figure 1" of the paper? It must be an test000XX.error in the > cases generates? because I don't have it in my results > > 3.- I must have a error case with (tr [ "" "") > ¿How can I reproduce the error exactly? for see that is crashing > > 4.- Someone know how I can continue learning about klee (more papers, > tutorials, examples). I search a lot but I didn't find too much > information. only sumarys of the OSDI and the klee official work. > > One case that I executed > > Case 1: > > #klee --max-time 2 --libc=uclibc --posix-runtime --init-env ./tr.bc > --sym-args 1 10 10 --sym-files 2 2000 --max-fail 1 > > > KLEE: NOTE: Using model: > /home/marta/llvm2.8_2/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: output directory = "klee-out-18" > KLEE: WARNING: function "vasnprintf" has inline asm > KLEE: WARNING: undefined reference to function: __signbitl > KLEE: WARNING: undefined reference to function: __xstat64 > KLEE: WARNING: undefined reference to function: klee_get_valuel > KLEE: WARNING: executable has module level assembly (ignoring) > KLEE: WARNING: calling external: syscall(54, 0, 21505, 185469936) > KLEE: WARNING: calling __user_main with extra arguments. > KLEE: WARNING: calling external: __xstat64(3, 185393256, 185647888) > missing operand > KLEE: WARNING: calling external: vprintf(184733344, 185645008) > Try `./tr.bc --help' for more information. > KLEE: WARNING: calling close_stdout with extra arguments. > write error > : Input/output errorTry `./tr.bc --help' for more information. > > Try `./tr.bc --help' for more information. > ./tr.bc: option `�m > @5 > 8�' is ambiguous > Try `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > write error > : Input/output errorTry `./tr.bc --help' for more information. > KLEE: HaltTimer invoked > KLEE: halting execution, dumping remaining states > > KLEE: done: total instructions = 322745 > KLEE: done: completed paths = 33 > KLEE: done: generated tests = 33 > > ________________________________________________________ > > when I try to see the results they looks like: > > $ klee-replay ./tr.bc ../../obj-llvm/src/klee-last/*.ktest > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000001.ktest > klee-replay: ARGS: "./tr.bc" "--" > /usr/bin/lli-2.9: missing operand > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (1 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000002.ktest > klee-replay: ARGS: "./tr.bc" "--" > /usr/bin/lli-2.9: missing operand > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000003.ktest > klee-replay: ARGS: "./tr.bc" "--" > /usr/bin/lli-2.9: missing operand > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000004.ktest > klee-replay: ARGS: "./tr.bc" "--" > /usr/bin/lli-2.9: missing operand > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000005.ktest > klee-replay: ARGS: "./tr.bc" "--" > /usr/bin/lli-2.9: missing operand > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000006.ktest > klee-replay: ARGS: "./tr.bc" "--=" > ./tr: la opción «--=» es ambigua > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000007.ktest > klee-replay: ARGS: "./tr.bc" "--=" > ./tr: la opción «--=» es ambigua > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000008.ktest > klee-replay: ARGS: "./tr.bc" "--=" > ./tr: la opción «--=» es ambigua > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000009.ktest > klee-replay: ARGS: "./tr.bc" "--=@" > ./tr: la opción «--=@» es ambigua > Try `./tr --help' for more information. > ..... > > And ther rest of the cases are similar till arrive the last one > > ... > klee-replay: TEST CASE: ../../obj-llvm/src/klee-last/test000029.ktest > klee-replay: ARGS: "./tr.bc" "--=@@@@@@@" > ./tr: la opción «--=@@@@@@@» es ambigua > Try `./tr --help' for more information. > klee-replay: EXIT STATUS: ABNORMAL 1 (0 seconds) > ERROR: ran out of appropriate inputs > > Thanks very much > Regards > Marta >
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
