[klee-dev] Implied Value Concretization

[Andrew Chi]

I'm working on an extension of KLEE for which implied value concretization
is a necessary prerequisite.  It looks like IVC is currently disabled in
the master branch of KLEE.

>From Executor.h (
https://github.com/klee/klee/blob/master/lib/Core/Executor.h#L193-L195)

/// Whether implied-value concretization is enabled. Currently
/// false, it is buggy (it needs to validate its writes).
bool ivcEnabled;


>From Executor.cpp (
https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L3712-L3715)


void Executor::doImpliedValueConcretization(ExecutionState &state,
                                            ref<Expr> e,
                                            ref<ConstantExpr> value) {
  abort(); // FIXME: Broken until we sort out how to do the write back.


We've started hacking up our own version of IVC for our purposes, but it's
not yet well-tested. Our implementation also walks through the entire
address space looking for expressions to concretize, so it could be pretty
inefficient.

Just to check that I'm not reinventing the wheel, has anyone already
implemented IVC?

Thanks!
Andrew
-------------- next part --------------
HTML attachment scrubbed and removed