1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>KLEE - Coreutils Experiments</title>
<link type="text/css" rel="stylesheet" href="menu.css">
<link type="text/css" rel="stylesheet" href="content.css">
</head>
<body>
<!--#include virtual="menu.html.incl"-->
<div id="content">
<!--*********************************************************************-->
<h1>Coreutils Experiments</h1>
<p>
This document is meant to give additional information regarding
the Coreutils experiments discussed in
our <a href="http://llvm.org/pubs/2008-12-OSDI-KLEE.html">KLEE
OSDI'08 paper</a>. However, please note that in the last several
years, KLEE and its dependencies (particularly LLVM and STP), have
undergone major changes, which have resulted in considerable
different behavior on several benchmarks, including Coreutils.</p>
<p>
This document is structured as a series of FAQs:
</p>
<ol>
<li>How did you build Coreutils?<br/>
Please follow the instructions in the <a href="TestingCoreutils.html">Coreutils Tutorial</a>.
</li>
<li>What version of LLVM was used in the OSDI paper?<br/>
We generally kept in sync with the LLVM top-of-tree, which at the time
was somewhere around LLVM 2.2 and 2.3.</li>
</li>
<li>What version of STP was used in the OSDI paper?<br/>
An old version of STP, which is still available as part of KLEE's
repository, in revisions up to r161056.
</li>
<li>What options did you run KLEE with? <br/>
We used the following options (the command below is for paste):
<div class="instr">
$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \ <br/>
--max-memory=1000 --disable-inlining --optimize --use-forked-stp \ <br/>
--use-cex-cache --with-libc --with-file-model=release \ <br/>
--allow-external-sym-calls --only-output-states-covering-new \ <br/>
--exclude-libc-cov --exclude-cov-file=./../lib/functions.txt \ <br/>
--environ=test.env --run-in=/tmp/sandbox --output-dir=paste-data-1h \ <br/>
--max-sym-array-size=4096 --max-instruction-time=10. --max-time=3600. \ <br/>
--watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \ <br/>
--max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \ <br/>
--randomize-fork --use-random-path --use-interleaved-covnew-NURS \ <br/>
--use-batching-search --batch-instructions 10000 --init-env \ <br/>
./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
</div>
Some of these options have been renamed or removed in the current
version of KLEE. Most notably, the options "--exclude-libc-cov"
and "--exclude-cov-file" were implemented in a fragile way and we
decided to remove them from KLEE. The idea was to treat the
functions in libc or specified in a text file as "covered". (For
the Coreutils experiments, we were interested in covering the
code in the tools themselves, as opposed to library code, see the
paper for more details). If you plan to reimplement these
options in a clean way, please consider contributing your code to the mainline.
</li>
<li>What are the options closest to the ones above that
work with the current version KLEE? </br>
Try the following:
<div class="instr">
$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \ <br/>
--max-memory=1000 --disable-inlining --optimize --use-forked-stp \ <br/>
--use-cex-cache --libc=uclibc --posix-runtime \ <br/>
--allow-external-sym-calls --only-output-states-covering-new \ <br/>
--environ=test.env --run-in=/tmp/sandbox \ <br/>
--max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. \ <br/>
--watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \ <br/>
--max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \ <br/>
--randomize-fork --search=random-path --search=nurs:covnew \ <br/>
--use-batching-search --batch-instructions=10000 \ <br/>
./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
</div>
</li>
<li>How do I generate test.env and /tmp/sandbox? <br/>
We used a simple environment and a "sandbox" directory to make
our experiments more deterministic. To recreate them, follow
these steps:
<ol type="a">
<li>Download <tt>testing-env.sh</tt> by clicking <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-cu-testing-env.html">here</a>, and place it in the current directory.</li>
<li>Create <tt>test.env</tt> by running:
<div class="instr">
$ env -i /bin/bash -c '(source testing-env.sh; env >test.env)'
</div>
</li>
<li>Download <tt>sandbox.tgz</tt> by clicking <a href="http://www.doc.ic.ac.uk/~cristic/klee/klee-cu-sandbox.html">here</a>, place it in <tt>/tmp</tt>, and run:
<div class="instr">
$ cd /tmp
$ tar xzfv sandbox.tgz
</div>
</li>
</ol>
</li>
<li>
What symbolic arguments did you use in your experiments? <br/>
We ran most utilities using the arguments below. Our choice was
based on a high-level understanding of the Coreutils
applications: most behavior can be triggered with no more than two
short options, one long option, and two small input streams (stdin and one file).
<div class="instr">
--sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
</div>
For eight tools where the coverage results were unsatisfactory,
we consulted the man page and increased the number and size of
arguments and files as follows:
<div class="instr">
<b>dd:</b> --sym-args 0 3 10 --sym-files 1 8 --sym-stdout <br/>
<b>dircolors:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout <br/>
<b>echo:</b> --sym-args 0 4 300 --sym-files 2 30 --sym-stdout <br/>
<b>expr:</b> --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout <br/>
<b>mknod:</b> --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout <br/>
<b>od:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout <br/>
<b>pathchk:</b> --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout <br/>
<b>printf:</b> --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
</div>
</li>
</ol>
</div>
</body>
</html>
|
