I created a solver to solve a state in a new thread, the state is copied from an existing state. The expr can be dumped as follow: ------------before dump------------ : Illegal seek (Slt (ReadLSB w32 12 input) (ReadLSB w32 8 input)) ------------after dump------------
the backtrace : ---------------------------------------------------------------------------------------------------------------- backtrace() returned 13 addresses klee(_ZN4llvm12DenseMapBaseINS_8DenseMapISt4pairIPKN4klee4ExprES6_EcNS_12DenseMapInfoIS7_EEEES7_cS9_E5clearEv+0x17d) [0x56da4d] klee(_ZN19ExprReplaceVisitor213visitExprPostERKN4klee4ExprE+0x89) [0x5d4a49] klee(_ZN4klee11ExprVisitor11visitActualERKNS_3refINS_4ExprEEE+0x82c) [0x5f700c] klee(_ZN4klee11ExprVisitor5visitERKNS_3refINS_4ExprEEE+0x1ba) [0x5f66da] klee(_ZNK4klee17ConstraintManager12simplifyExprENS_3refINS_4ExprEEE+0x3da) [0x5d3b2a] klee(_ZN4klee12TimingSolver10brevaluateERKNS_14ExecutionStateENS_3refINS_4ExprEEERNS_6Solver8ValidityERb+0x1ff) [0x58781f] klee(_ZN4klee8Executor6brforkERNS_14ExecutionStateENS_3refINS_4ExprEEEbRb+0xfe) [0x55f64e] klee(_ZN4klee8Executor18executeInstructionERNS_14ExecutionStateEPNS_12KInstructionE+0x1bf8) [0x562b88] klee(_ZN4klee8Executor3runERNS_14ExecutionStateE+0x6e9) [0x565fd9] klee(*ZN4klee8Executor17runFunctionAsMainEPN4llvm8FunctionEiPPcS5*+0x631) [0x5666c1] klee(main+0x28b3) [0x536fa3] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf5) [0x7f30b7aa3f45] klee() [0x54b60a] klee: /home/wy/workspace/klee/llvm-3.4/include/llvm/ADT/DenseMap.h:124: void llvm::DenseMapBase::clear() [with DerivedT = llvm::DenseMap<std::pair, char, llvm::DenseMapInfo<std::pair > >; KeyT = std::pair; ValueT = char; KeyInfoT = llvm::DenseMapInfo<std::pair >]: Assertion getNumEntries() == 0 && "Node count imbalance!"' failed. backtrace() returned 22 addresses klee(_ZN4llvm12DenseMapBaseINS_8DenseMapISt4pairIPKN4klee4ExprES6_EcNS_12DenseMapInfoIS7_EEEES7_cS9_E5clearEv+0x17d) [0x56da4d] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x139) [0x5cd889] klee(_ZN4klee9Z3Builder15constructActualENS_3refINS_4ExprEEEPi+0x10eb) [0x5cf65b] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x269) [0x5cd9b9] klee(_ZN4klee9Z3Builder15constructActualENS_3refINS_4ExprEEEPi+0xff0) [0x5cf560] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x269) [0x5cd9b9] klee(_ZN4klee9Z3Builder15constructActualENS_3refINS_4ExprEEEPi+0xff0) [0x5cf560] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x269) [0x5cd9b9] klee(_ZN4klee9Z3Builder15constructActualENS_3refINS_4ExprEEEPi+0x203) [0x5ce773] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x269) [0x5cd9b9] klee(_ZN4klee9Z3Builder15constructActualENS_3refINS_4ExprEEEPi+0x5a1) [0x5ceb11] klee(_ZN4klee9Z3Builder9constructENS_3refINS_4ExprEEEPi+0x269) [0x5cd9b9] klee(_ZN4klee12Z3SolverImpl17internalRunSolverERKNS_5QueryEPKSt6vectorIPKNS_5ArrayESaIS7_EEPS4_IS4_IhSaIhEESaISD_EERb+0x17c) [0x5c983c] klee(_ZN16CexCachingSolver13getAssignmentERKN4klee5QueryERPNS0_10AssignmentE+0x104) [0x5b27e4] klee(_ZN16CexCachingSolver15computeValidityERKN4klee5QueryERNS0_6Solver8ValidityE+0x117) [0x5b2fc7] klee(_ZN13CachingSolver15computeValidityERKN4klee5QueryERNS0_6Solver8ValidityE+0x6d) [0x5b04dd] klee(_ZN17IndependentSolver15computeValidityERKN4klee5QueryERNS0_6Solver8ValidityE+0x112) [0x5c12f2] klee(_ZN4klee12TimingSolver8evaluateERKNS_14ExecutionStateENS_3refINS_4ExprEEERNS_6Solver8ValidityE+0xd9) [0x587399] klee(_ZN4klee8Executor6t_forkERNS_14ExecutionStateENS_3refINS_4ExprEEEbPNS_12TimingSolverE+0xd2) [0x553352] klee(_Z6thr_fnPv+0x99) [0x5547d9] /lib/x86_64-linux-gnu/libpthread.so.0(+0x8184) [0x7f30b9a4c184] /lib/x86_64-linux-gnu/libc.so.6(clone+0x6d) [0x7f30b7b7c37d] klee: /home/wy/workspace/klee/llvm-3.4/include/llvm/ADT/DenseMap.h:124: void llvm::DenseMapBase<DerivedT, KeyT, ValueT, KeyInfoT>::clear() [with DerivedT = llvm::DenseMap<std::pair<const klee::Expr*, const klee::Expr*>, char, llvm::DenseMapInfo<std::pair<const klee::Expr*, const klee::Expr*> > >; KeyT = std::pair<const klee::Expr*, const klee::Expr*>; ValueT = char; KeyInfoT = llvm::DenseMapInfo<std::pair<const klee::Expr*, const klee::Expr*> >]: AssertiongetNumEntries() == 0 && “Node count imbalance!”’ failed. -------------------------------------------------------------------------------------------------- It seems that the expr is fine, anyone knows how can it be crashed ? ---thanks ,by wy7980
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev