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
|
TODO
--
Build System / Configure / Release Cleanups
--
o Configure doesn't check for bison / flex, we don't really use these
for anything important (just the command line STP tool), it would
be nice if they weren't required.
o Need a way to hide LLVM options in "klee --help".
KLEE Internal
--
o Make sure that namespaces and .cpp locations match with reorganized
include locations.
o Add replay framework for POSIX model tests.
o We need to reimplement the constant Expr optimization which
previously was embedded in the ref<> class to improve concrete
interpretation performance. See:
http://llvm.org/viewvc/llvm-project?view=rev&revision=72753
The idea is that only the interpreter should have to deal with this
distinction. The new scheme is that we embed small constants inside
the Cell data structure. Clients which want to get an Expr will use
a standard accessor method which will automatically cons up the
appropriate ConstantExpr if needed, and the core interpretation
functions will be modified to operator on Cells directly so that
they can avoid the allocation overhead.
In the end, this should actually improve concrete execution
performance because we have will have tightened the interpreter
loop. The downside is that the Expr language will always allocate
constants, but since performance is usually out-the-window once
dealing with constraints, this seems like the correct tradeoff.
o Support executing programs which are compiled for a different
architecture than that of the host. Steps:
1. Provide a way to find the correct runtime libraries, based on the target architecture.
2. Extend build system to support building the runtime libraries for a separate target.
3. Since calling external functions will be totally invalid in this
environment, we will have to invent replacements for the useful
ones (printf).
Kleaver Internal
--
o We need to fix the constants-in-exprs problem, this makes
separating out a Kleaver expr library much more difficult. There
are two parts:
1. Pull fast (pure constant) path operations out of Expr.cpp,
into Executor.cpp.
2. Lift constants-are-immediate optimization out of ref<Expr>
into Cell. Expressions in memory already have the concrete
cache, so we get that part for free.
We will need a way to distinguish if a cell has an expr or a
constant. Incidentally, this gives us an extra sentinel value
(is-expr == true and Expr* == null) we can use to mark
uninitialized-value of a register.
It may be worth sinking Expr construction into a Builder class
while we are at it.
There is a also a nice cleanup/perf win where we can work with
registers (Cells) directly, now that we build the constant table,
it might be worth doing this at the same time. This exposes a win
for IVC where it can write back a constant value into a register,
which needs to be done with care but would be a big improvement for
IVC.
o The stpArray field of an UpdateNode needs to die. This isn't as
easy as dropping it from the map, because we also need a
notification to free it. I think probably what we should do is
introduce an ExprContext can be used to deal with such things.
o The ExprContext could also have the default builder, for
example, which would make it easy to swap in an optimizing
builder.
Testing
-------
o We should try using klee instead of lli on a nightlytester setup,
to flush out problems with concrete execution.
|
