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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
