diff options
| -rw-r--r-- | TODO.txt | 92 |
1 files changed, 0 insertions, 92 deletions
diff --git a/TODO.txt b/TODO.txt deleted file mode 100644 index 794c3352..00000000 --- a/TODO.txt +++ /dev/null @@ -1,92 +0,0 @@ -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. |