[klee-dev] klee crash on expr

[Valiant wang]

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
-------------- next part --------------
HTML attachment scrubbed and removed