klee/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.

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.