TODO.txt

TODO
--

Build System / Configure / Release Cleanups
--
 o Rename .pc to .kquery (kleaver query)

 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.