KLEE is hitting an assertion failure after a few thousand test cases are generated:
Assertion failed: (hasSolution && "state has invalid constraint set"), function computeValue, file /Users/rzg/Projects/llvm/tools/klee/lib/Solver/Solver.cpp, line 540. 0 klee 0x000000010c8431e2 PrintStackTrace(void*) + 34 1 klee 0x000000010c8436c9 SignalHandler(int) + 649 2 libsystem_c.dylib 0x00007fffa725669a _sigtramp + 26 3 libsystem_c.dylib 0x00007fffa72b69b3 __swrite + 0 4 klee 0x000000010c843426 abort + 22 5 klee 0x000000010c8433e5 __assert_rtn + 53 6 klee 0x000000010c0ffb4f STPSolverImpl::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 831 7 klee 0x000000010c0ebb82 CachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 18 8 klee 0x000000010c0f507f IndependentSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 159 9 klee 0x000000010c0fde0a klee::Solver::getValue(klee::Query const&, klee::ref<klee::ConstantExpr>&) + 154 10 klee 0x000000010c0df953 klee::TimingSolver::getValue(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 483 11 klee 0x000000010c0a26aa klee::AddressSpace::resolveOne(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::pair<klee::MemoryObject const*, klee::ObjectState const*>&, bool&) + 234 12 klee 0x000000010c0b380f klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 511 13 klee 0x000000010c0b9347 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 17559 14 klee 0x000000010c0be493 klee::Executor::run(klee::ExecutionState&) + 1251 15 klee 0x000000010c0c11a7 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2199 16 klee 0x000000010c09d02f main + 10015 17 libdyld.dylib 0x00007fffa8d007c1 start + 0 18 libdyld.dylib 0x0000000000000008 start + 18446603337683957831 (This is with the cex cache disabled. I was hitting a different assertion with it on, but I am assuming that it is the same root cause.) I'm not sure where to begin debugging this—is there an option I should be using to dump state more thoroughly before the assertion is hit? It takes a long time to reach the assertion failure, so if there's an easier way to restore state to reproduce the problem it would be very helpful. Thanks, Ryan _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
