[klee-dev] klee: buffer overflow detected
Daniel Liew
daniel.liew at imperial.ac.uk
Thu Jan 23 09:10:41 GMT 2014
Glad to hear you solved your problem. Although klee-fp is not actively
maintained KLEE is. Would you mind seeing if this an issue in the
upstream KLEE[1] and...
* Provide a patch to fix the issue along with a test case (the better
option :) )
OR
* Report the issue along with a test case on our issue tracker [2]
?
[1] https://github.com/ccadar/klee
[2] https://github.com/ccadar/klee/issues?state=open
Thanks,
Dan Liew.
On 22 January 2014 20:41, Double Dave <dave.t273 at yahoo.com> wrote:
> ok, i got a solution. Problem was that the name of a symbolic variable was
> just to long.
> Although i wouldn't consider 24 letters as too long, shortening these
> variable names got my klee finally running.
>
> Regards,
> David
>
>
> On Tuesday, January 7, 2014 4:56 PM, Double Dave <dave.t273 at yahoo.com>
> wrote:
> Hello all,
>
> I am testing a program with klee-fp. I use around 12 symbolic variables
> without problems, but when i make a specific variable symbolic i get this
> overflow.
>
>
> Any ideas?
>
>
> *** buffer overflow detected ***: klee terminated
> ======= Backtrace: =========
> /lib/x86_64-linux-gnu/libc.so.6(__fortify_fail+0x37)[0x7f8c47620f47]
> /lib/x86_64-linux-gnu/libc.so.6(+0x109e40)[0x7f8c4761fe40]
> /lib/x86_64-linux-gnu/libc.so.6(+0x1092a9)[0x7f8c4761f2a9]
> /lib/x86_64-linux-gnu/libc.so.6(_IO_default_xsputn+0xdd)[0x7f8c4759213d]
> /lib/x86_64-linux-gnu/libc.so.6(_IO_vfprintf+0x1d42)[0x7f8c47560702]
> /lib/x86_64-linux-gnu/libc.so.6(__vsprintf_chk+0x94)[0x7f8c4761f344]
> /lib/x86_64-linux-gnu/libc.so.6(__sprintf_chk+0x7d)[0x7f8c4761f28d]
> klee(_ZN4klee10STPBuilder15getInitialArrayEPKNS_5ArrayE+0x81)[0x603741]
> klee(_ZN4klee10STPBuilder17getArrayForUpdateEPKNS_5ArrayEPKNS_10UpdateNodeE+0x155)[0x603c15]
> klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1932)[0x605552]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3]klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3]
> klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3]
> klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3]
> klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STP
> ExprTypeE+0x427)[0x604047]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287]
> klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3]
> klee(_ZN13STPSolverImpl20computeInitialValuesERKN4klee5QueryERKSt6vectorIPKNS0_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EERb+0xbc)[0x5ff64c]
> klee(_ZN16CexCachingSolver13getAssignmentERKN4klee5QueryERPNS0_10AssignmentE+0xfe)[0x5ea0ce]
> klee(_ZN16CexCachingSolver20computeInitialValuesERKN4klee5QueryERKSt6vectorIPKNS0_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EERb+0x41)[0x5ea781]
> klee(_ZN4klee6Solver16getInitialValuesERKNS_5QueryERKSt6vectorIPKNS_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EE+0x13)[0x5fdef3]
> klee(_ZN4klee12TimingSolver16getInitialValuesERKNS_14ExecutionStateERKSt6vectorIPKNS_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EE+0x15c)[0x5bcebc]
> klee(_ZN4klee8Executor19getSymbolicSolutionERKNS_14ExecutionStateERSt6vectorISt4pairISsS4_IhSa
> IhEEESaIS8_EE+0x28c)[0x57a89c]
> klee[0x5a0e03]
> klee(_ZN4klee8Executor20terminateStateOnExitERNS_14ExecutionStateE+0x2e)[0x57d1fe]
> klee(_ZN4klee8Executor18executeInstructionERNS_14ExecutionStateEPNS_12KInstructionE+0x5832)[0x58cfa2]
> klee(_ZN4klee8Executor3runERNS_14ExecutionStateE+0x772)[0x58dd52]
> klee(_ZN4klee8Executor17runFunctionAsMainEPN4llvm8FunctionEiPPcS5_+0x71f)[0x58e7af]
> klee(main+0x14c8)[0x568458]
> /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xed)[0x7f8c4753776d]
> klee[0x574a31]
> ======= Memory map: ========
> 00400000-01248000 r-xp 00000000 08:05 725940
> /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee
> 01447000-0149e000 r--p 00e47000 08:05 725940
> /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee
> 0149e000-0152b000 rw-p 00e9e000 08:05 725940
> /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee
> 0152b000-01538000 rw-p 00000000 00:00 0
> 02dc3000-063cf000 rw-p 00000000 00:00 0
> [heap]
> 7f8c37516000-7f8c47516000 rw-p 00000000 00:00 0
> 7f8c47516000-7f8c476cb000 r-xp 00000000 08:05 130848
> /lib/x86_64-linux-gnu/libc-2.15.so
> 7f8c476cb000-7f8c478cb000 ---p 001b5000 08:05 130848
> /lib/x86_64-linux-gnu/libc-2.15.so
> 7f8c478cb000-7f8c478cf000 r--p 001b5000 08:05 130848
> /lib/x86_64-linux-gnu/libc-2.15.so
> 7f8c478cf000-7f8c478d1000 rw-p 001b9000 08:05 130848
> /lib/x86_64-linux-gnu/libc-2.15.so
> 7f8c478d1000-7f8c478d6000 rw-p 00000000 00:00 0
> 7f8c478d6000-7f8c478eb000 r-xp 00000000 08:05 135220
> /lib/x86_64-linux-gnu/libgcc_s.so.1
> 7f8c478eb000-7f8c47aea000 ---p 00015000 08:05 135220
> /lib/x86_64-linux-gnu/libgcc_s.so.1
> 7f8c47aea000-7f8c47aeb000 r--p 00014000 08:05 135220
> /lib/x86_64-linux-gnu/libgcc_s.so.1
> 7f8c47aeb000-7f8c47aec000 rw-p 00015000 08:05 135220
> /lib/x86_64-linux-gnu/libgcc_s.so.1
> 7f8c47aec000-7f8c47be7000 r-xp 00000000 08:05 130957
> /lib/x86_64-linux-gnu/libm-2.15.so
> 7f8c47be7000-7f8c47de6000 ---p 000fb000 08:05 130957
> /lib/x86_64-linux-gnu/libm-2.15.so
> 7f8c47de6000-7f8c47de7000 r--p 000fa000 08:05 130957
> /lib/x86_64-linux-gnu/libm-2.15.so
> 7f8c47de7000-7f8c47de8000 rw-p 000fb000 08:05 130957
> /lib/x86_64-linux-gnu/libm-2.15.so
> 7f8c47de8000-7f8c47eca000 r-xp 00000000 08:05 401337
> /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16
> 7f8c47eca000-7f8c480c9000 ---p 000e2000 08:05 401337
> /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16
> 7f8c480c9000-7f8c480d1000 r--p 000e1000 08:05 401337
> /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16
> 7f8c480d1000-7f8c480d3000 rw-p 000e9000 08:05 401337
> /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16
> 7f8c480d3000-7f8c480e8000 rw-p 00000000 00:00 0
> 7f8c480e8000-7f8c480ea000 r-xp 00000000 08:05 130961
> /lib/x86_64-linux-gnu/libdl-2.15.so
> 7f8c480ea000-7f8c482ea000 ---p 00002000 08:05 130961
> /lib/x86_64-linux-gnu/libdl-2.15.so
> 7f8c482ea000-7f8c482eb000 r--p 00002000 08:05 130961
> /lib/x86_64-linux-gnu/libdl-2.15.so
> 7f8c482eb000-7f8c482ec000 rw-p 00003000 08:05 130961
> /lib/x86_64-linux-gnu/libdl-2.15.so
> 7f8c482ec000-7f8c48304000 r-xp 00000000 08:05 130955
> /lib/x86_64-linux-gnu/libpthread-2.15.so
> 7f8c48304000-7f8c48503000 ---p 00018000 08:05 130955
> /lib/x86_64-linux-gnu/libpthread-2.15.so
> 7f8c48503000-7f8c48504000 r--p 00017000 08:05 130955
> /lib/x86_64-linux-gnu/libpthread-2.15.so
> 7f8c48504000-7f8c48505000 rw-p 00018000 08:05 130955
> /lib/x86_64-linux-gnu/libpthread-2.15.so
> 7f8c48505000-7f8c48509000 rw-p 00000000 00:00 0
> 7f8c48509000-7f8c4852b000 r-xp 00000000 08:05 130958
> /lib/x86_64-linux-gnu/ld-2.15.so
> 7f8c48658000-7f8c486d8000 rwxp 00000000 00:00 0
> 7f8c486d8000-7f8c486f9000 rw-p 00000000 00:00 0
> 7f8c48713000-7f8c48719000 rw-p 00000000 00:00 0
> 7f8c48727000-7f8c4872b000 rw-p 00000000 00:00 0
> 7f8c4872b000-7f8c4872c000 r--p 00022000 08:05 130958
> /lib/x86_64-linux-gnu/ld-2.15.so
> 7f8c4872c000-7f8c4872e000 rw-p 00023000 08:05 130958
> /lib/x86_64-linux-gnu/ld-2.15.so
> 7fffea404000-7fffea494000 rw-p 00000000 00:00 0
> [stack]
> 7fffea5f8000-7fffea5f9000 r-xp 00000000 00:00 0
> [vdso]
> ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0
> [vsyscall]
> 0 klee 0x0000000000d99fcf
> 1 klee 0x0000000000d9a4d9
> 2 libpthread.so.0 0x00007f8c482fbcb0
> 3 libc.so.6 0x00007f8c4754c425 gsignal + 53
> 4 libc.so.6 0x00007f8c4754fb8b abort + 379
> 5 libc.so.6 0x00007f8c4758a39e
> 6 libc.so.6 0x00007f8c47620f47 __fortify_fail + 55
> 7 libc.so.6 0x00007f8c4761fe40
> 8 libc.so.6 0x00007f8c4761f2a9
> 9 libc.so.6 0x00007f8c4759213d _IO_default_xsputn + 221
> 10 libc.so.6 0x00007f8c47560702 _IO_vfprintf + 7490
> 11 libc.so.6 0x00007f8c4761f344 __vsprintf_chk + 148
> 12 libc.so.6 0x00007f8c4761f28d __sprintf_chk + 125
> 13 klee 0x0000000000603741
> klee::STPBuilder::getInitialArray(klee::Array const*) + 129
> 14 klee 0x0000000000603c15
> klee::STPBuilder::getArrayForUpdate(klee::Array const*, klee::UpdateNode
> const*) + 341
> 15 klee 0x0000000000605552
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 6450
> 16 klee 0x0000000000603287
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 503
> 17 klee 0x00000000006034b3
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType) + 67
> 18 klee 0x00000000006051d2
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 5554
> 19 klee 0x0000000000603287
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 503
> 20 klee 0x00000000006034b3
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType) + 67
> 21 klee 0x00000000006051d2
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 5554
> 22 klee 0x0000000000603287
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 503
> 23 klee 0x00000000006034b3
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType) + 67
> 24 klee 0x00000000006051d2
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 5554
> 25 klee 0x0000000000603287
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 503
> 26 klee 0x00000000006034b3
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType) + 67
> 27 klee 0x0000000000604047
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 1063
> 28 klee 0x0000000000603287
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType*) + 503
> 29 klee 0x00000000006034b3
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*,
> klee::STPBuilder::STPExprType) + 67
> 30 klee 0x00000000005ff64c
> STPSolverImpl::computeInitialValues(klee::Query const&,
> std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
> std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
> std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>>&, bool&) + 188
> 31 klee 0x00000000005ea0ce
> CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
> 254
> 32 klee 0x00000000005ea781
> CexCachingSolver::computeInitialValues(klee::Query const&,
> std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
> std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
> std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>>&, bool&) + 65
> 33 klee 0x00000000005fdef3
> klee::Solver::getInitialValues(klee::Query const&, std::vector<klee::Array
> const*, std::allocator<klee::Array const*> > const&,
> std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
> std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>>&) + 19
> 34 klee 0x00000000005bcebc
> klee::TimingSolver::getInitialValues(klee::ExecutionState const&,
> std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
> std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
> std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>>&) + 348
> 35 klee 0x000000000057a89c
> klee::Executor::getSymbolicSolution(klee::ExecutionState const&,
> std::vector<std::pair<std::string, std::vector<unsigned char,
> std::allocator<unsigned char> > >, std::allocator<std::pair<std::string,
> std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 652
> 36 klee 0x00000000005a0e03
> 37 klee 0x000000000057d1fe
> klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 46
> 38 klee 0x000000000058cfa2
> klee::Executor::executeInstruction(klee::ExecutionState&,
> klee::KInstruction*) + 22578
> 39 klee 0x000000000058dd52
> klee::Executor::run(klee::ExecutionState&) + 1906
> 40 klee 0x000000000058e7af
> klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
> 1823
> 41 klee 0x0000000000568458 main + 5320
> 42 libc.so.6 0x00007f8c4753776d __libc_start_main + 237
> 43 klee 0x0000000000574a31
> Aborted (core dumped)
>
> Regards,
> David
>
>
More information about the klee-dev
mailing list