[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: Re: [klee-dev] klee memory access model and test cases
From: Richard Rutledge <rrutledge3 () gatech ! edu>
Date: 2018-12-05 16:40:37
Message-ID: 1544028035.29749.0 () smtp ! office365 ! com
[Download RAW message or body]
[Attachment #2 (text/plain)]
You get multiple test cases even though there are no program branches due to the \
unconstrained buf indexed access.
To remain sound, klee forks a case for each value of index that could resolve to a \
memory object. The value corresponding to zero is the buf array. The other values \
resolve the access to other memory objects found in the virtual state.
│⚙ Cheers! │Richard Rutledge \
└────────────────────
On Tue, Dec 4, 2018 at 9:52 PM, Hank Zhang <westrainzxh@gmail.com> wrote:
Hi all,
I am new to klee, and I wrote a test case, but I do not understand the generated \
testcases, and the memory model of klee. I tried to search the email archive and \
other websites but no result. Here is my question.
My simple program, test_main.c, looks like below:
```
#include <stdio.h>
#include <klee/klee.h>
int main(){
int i;
klee_make_symbolic(&i, sizeof i, "sym_i");
char buf[20];
buf[i]=9;
return 0;
}
```
And then
```
clang -I /PATH/klee/include -emit-llvm -c test_main.c -o test_main.bc
klee test_main.bc
```
After that, the result is:
```
KLEE: done: total instructions = 14
KLEE: done: completed paths = 5
KLEE: done: generated tests = 5
```
Which means klee finds 5 paths and generate 5 tests. With this scripts I can see \
that the test cases are: $ for testfile in `ls klee-last/*.ktest`; do ktest-tool \
--write-ints $testfile |grep data; done
```
object 0: data: 536870912
object 0: data: -1216296
object 0: data: -1216208
object 0: data: 0
object 0: data: -1216288
```
My question is, why klee finds 5 paths? and what are the meaning of generated 5 \
tests, especially the 3 negative ones?
Thank you very much
[Attachment #3 (text/html)]
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div id="geary-body">
<div>You get multiple test cases even though there are no program branches due to the \
unconstrained buf indexed access. </div> <div><br>
</div>
<div>To remain sound, klee forks a case for each value of index that could resolve to \
a memory object. The value corresponding to zero is the buf array. The \
other values resolve the access to other memory objects found in the virtual \
state.</div> <div><br>
</div>
</div>
<div id="geary-signature">
<div style="white-space: pre;">│⚙ Cheers! │Richard Rutledge \
└────────────────────</div> </div>
<div id="geary-quote"><br>
On Tue, Dec 4, 2018 at 9:52 PM, Hank Zhang <westrainzxh@gmail.com> wrote:<br>
<blockquote type="cite">
<div dir="ltr">Hi all,
<div>I am new to klee, and I wrote a test case, but I do not understand the generated \
testcases, and the memory model of klee. I tried to search the email archive and \
other websites but no result. Here is my question.</div> <div><br>
</div>
<div>My simple program, test_main.c, looks like below:</div>
<div>
<div><br>
</div>
<div>```</div>
<div>#include <stdio.h></div>
<div>#include <klee/klee.h></div>
<div>int main(){<br>
</div>
<div> int i;</div>
<div> klee_make_symbolic(&i, sizeof i, \
"sym_i");</div> <div> char buf[20];</div>
<div> buf[i]=9;</div>
<div> return 0; </div>
<div>}</div>
</div>
<div>```</div>
<div><br>
</div>
<div>And then </div>
<div>```</div>
<div>clang -I /PATH/klee/include -emit-llvm -c test_main.c -o test_main.bc<br>
</div>
<div>klee test_main.bc</div>
<div>```</div>
<div>After that, the result is:</div>
<div><br>
</div>
<div>```</div>
<div>
<div>KLEE: done: total instructions = 14</div>
<div>KLEE: done: completed paths = 5</div>
<div>KLEE: done: generated tests = 5</div>
</div>
<div>```</div>
<div>Which means klee finds 5 paths and generate 5 tests. With this scripts I \
can see that the test cases are:</div> <div>$ for testfile in `ls \
klee-last/*.ktest`; do ktest-tool --write-ints $testfile |grep data; done </div> \
<div> <br> </div>
<div>```</div>
<div>
<div>object 0: data: 536870912</div>
<div>object 0: data: -1216296</div>
<div>object 0: data: -1216208</div>
<div>object 0: data: 0</div>
<div>object 0: data: -1216288</div>
</div>
<div><br>
</div>
<div>```</div>
<div><br>
</div>
<div>My question is, why klee finds 5 paths? and what are the meaning of generated 5 \
tests, especially the 3 negative ones? </div> <div><br>
</div>
<div><br>
</div>
<div><br>
</div>
<div>Thank you very much </div>
</div>
</blockquote>
</div>
</body>
</html>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--===============4389185618185556521==--
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic