Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom

[Kirill Bogdanov]

Hello Everyone,

I wonder if I can ask a question about KLEE FP here, I am getting an
assertion in Solver.cpp after 1 hour of klee-fp run and I am trying to
understand why.

What is the meaning of this assertion? Am I doing something wrong? How can
I find which line in my code has triggered it?

Any directions would be appreciated!
Thank you very much!

$ clang -emit-llvm -c -g main.cpp
$ time klee -libc=uclibc main.o
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev
KLEE: WARNING: undefined reference to function: _ZSt17__throw_bad_allocv
KLEE: WARNING: undefined reference to function:
_ZSt18_Rb_tree_decrementPKSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function:
_ZSt18_Rb_tree_decrementPSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function:
_ZSt18_Rb_tree_incrementPKSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function:
_ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function:
_ZSt20__throw_out_of_rangePKc
KLEE: WARNING: undefined reference to function:
_ZSt28_Rb_tree_rebalance_for_erasePSt18_Rb_tree_node_baseRS_
KLEE: WARNING: undefined reference to function:
_ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_
KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __cxa_end_catch
KLEE: WARNING: undefined reference to function: __cxa_rethrow
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __restore_rt
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: klee_cos
KLEE: WARNING: undefined reference to function: klee_cosf
KLEE: WARNING: undefined reference to function: klee_sin
KLEE: WARNING: undefined reference to function: klee_sinf
KLEE: WARNING: undefined reference to function: klee_sqrt
KLEE: WARNING: undefined reference to function: klee_sqrtf
KLEE: WARNING: undefined reference to function: lseek64
KLEE: WARNING: undefined reference to function: syscall
KLEE: WARNING: undefined reference to function: time
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: _ZNSt8ios_base4InitC1Ev(139919863132416)
KLEE: WARNING: calling external: syscall(16, 0, 21505, 139919863148000)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: time(0)
KLEE: WARNING: calling external:
_ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_(true,
139919863156288, 139919863151184, 139919863151184)
KLEE: WARNING: calling external: exp(0)
KLEE: WARNING: calling external:
_ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base(139919863234656)
klee: Solver.cpp:1103: MINISAT::PropagatedFrom
MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.
0 klee 0x0000000000e6bdcf
1 klee 0x0000000000e6c2d9
2 libpthread.so.0 0x00007f41b29b7cb0
3 libc.so.6 0x00007f41b1c08425 gsignal + 53
4 libc.so.6 0x00007f41b1c0bb8b abort + 379
5 libc.so.6 0x00007f41b1c010ee
6 libc.so.6 0x00007f41b1c01192
7 klee 0x0000000000ec6c85 MINISAT::Solver::propagate(bool) +
1461
8 klee 0x0000000000ece364 MINISAT::Solver::search(int, int,
bool) + 196
9 klee 0x0000000000ecf009
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 1465
10 klee 0x0000000000ebfbe9
BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool,
BEEV::CNFMgr*&, bool, bool) + 3609
11 klee 0x0000000000ec021d
BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int,
BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const,
BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 125
12 klee 0x0000000000ec0dcc
BEEV::ToSAT::CallSAT(MINISAT::Solver&, BEEV::ASTNode const&) + 2956
13 klee 0x0000000000ebce2f
BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 31
14 klee 0x0000000000eabab2
BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 8050
15 klee 0x0000000000eacd8e BEEV::STP::TopLevelSTP(BEEV::ASTNode
const&, BEEV::ASTNode const&) + 238
16 klee 0x0000000000e85a4d vc_query + 157
17 klee 0x0000000000617fa5
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&) + 1477
18 klee 0x00000000006024ee
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
254
19 klee 0x0000000000603829
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1065
20 klee 0x0000000000600ff0
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 144
21 klee 0x00000000006114cc
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 348
22 klee 0x00000000005d59f2
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 546
23 klee 0x000000000059ab3f
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool,
int) + 303
24 klee 0x00000000005a3f02
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 12706
25 klee 0x00000000005a71a2
klee::Executor::run(klee::ExecutionState&) + 1906
26 klee 0x00000000005a7c1f
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1823
27 klee 0x000000000057ddf8 main + 5320
28 libc.so.6 0x00007f41b1bf376d __libc_start_main + 237
29 klee 0x000000000058df81
Aborted (core dumped)

real 100m21.991s
user 99m41.830s
sys 0m20.345s

[Kuchta, Tomasz]

Hi Kirill,

I would check if you are not running out of memory and
try to do ulimit –s unlimited.

Tomek

From: Kirill Bogdanov <kirill.sc-***@public.gmane.org<mailto:kirill.sc-***@public.gmane.org>>
Date: Friday, 25 April 2014 14:02
To: klee-dev <klee-dev-AQ/***@public.gmane.org<mailto:klee-dev-AQ/***@public.gmane.org>>
Subject: [klee-dev] Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.

Hello Everyone,

I wonder if I can ask a question about KLEE FP here, I am getting an assertion in Solver.cpp after 1 hour of klee-fp run and I am trying to understand why.

What is the meaning of this assertion? Am I doing something wrong? How can I find which line in my code has triggered it?

Any directions would be appreciated!
Thank you very much!

$ clang -emit-llvm -c -g main.cpp
$ time klee -libc=uclibc main.o
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev
KLEE: WARNING: undefined reference to function: _ZSt17__throw_bad_allocv
KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_decrementPKSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_decrementPSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_incrementPKSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base
KLEE: WARNING: undefined reference to function: _ZSt20__throw_out_of_rangePKc
KLEE: WARNING: undefined reference to function: _ZSt28_Rb_tree_rebalance_for_erasePSt18_Rb_tree_node_baseRS_
KLEE: WARNING: undefined reference to function: _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_
KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __cxa_end_catch
KLEE: WARNING: undefined reference to function: __cxa_rethrow
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __restore_rt
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: klee_cos
KLEE: WARNING: undefined reference to function: klee_cosf
KLEE: WARNING: undefined reference to function: klee_sin
KLEE: WARNING: undefined reference to function: klee_sinf
KLEE: WARNING: undefined reference to function: klee_sqrt
KLEE: WARNING: undefined reference to function: klee_sqrtf
KLEE: WARNING: undefined reference to function: lseek64
KLEE: WARNING: undefined reference to function: syscall
KLEE: WARNING: undefined reference to function: time
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: _ZNSt8ios_base4InitC1Ev(139919863132416)
KLEE: WARNING: calling external: syscall(16, 0, 21505, 139919863148000)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: time(0)
KLEE: WARNING: calling external: _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_(true, 139919863156288, 139919863151184, 139919863151184)
KLEE: WARNING: calling external: exp(0)
KLEE: WARNING: calling external: _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base(139919863234656)
klee: Solver.cpp:1103: MINISAT::PropagatedFrom MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.
0 klee 0x0000000000e6bdcf
1 klee 0x0000000000e6c2d9
2 libpthread.so.0 0x00007f41b29b7cb0
3 libc.so.6 0x00007f41b1c08425 gsignal + 53
4 libc.so.6 0x00007f41b1c0bb8b abort + 379
5 libc.so.6 0x00007f41b1c010ee
6 libc.so.6 0x00007f41b1c01192
7 klee 0x0000000000ec6c85 MINISAT::Solver::propagate(bool) + 1461
8 klee 0x0000000000ece364 MINISAT::Solver::search(int, int, bool) + 196
9 klee 0x0000000000ecf009 MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 1465
10 klee 0x0000000000ebfbe9 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 3609
11 klee 0x0000000000ec021d BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int, BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const, BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 125
12 klee 0x0000000000ec0dcc BEEV::ToSAT::CallSAT(MINISAT::Solver&, BEEV::ASTNode const&) + 2956
13 klee 0x0000000000ebce2f BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 31
14 klee 0x0000000000eabab2 BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&) + 8050
15 klee 0x0000000000eacd8e BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 238
16 klee 0x0000000000e85a4d vc_query + 157
17 klee 0x0000000000617fa5 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&) + 1477
18 klee 0x00000000006024ee CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 254
19 klee 0x0000000000603829 CexCachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 1065
20 klee 0x0000000000600ff0 CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 144
21 klee 0x00000000006114cc IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 348
22 klee 0x00000000005d59f2 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 546
23 klee 0x000000000059ab3f klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool, int) + 303
24 klee 0x00000000005a3f02 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 12706
25 klee 0x00000000005a71a2 klee::Executor::run(klee::ExecutionState&) + 1906
26 klee 0x00000000005a7c1f klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1823
27 klee 0x000000000057ddf8 main + 5320
28 libc.so.6 0x00007f41b1bf376d __libc_start_main + 237
29 klee 0x000000000058df81
Aborted (core dumped)

real 100m21.991s
user 99m41.830s
sys 0m20.345s

[Daniel Liew]

The assertion is failing inside STP.

I would probably try attaching to GDB, let it run so GDB can catch the
assertion failure. Make sure you've built STP with debug symbols so
you can get a useful backtrace.

Post by Kuchta, Tomasz
Hi Kirill,
I would check if you are not running out of memory and
try to do ulimit –s unlimited.
Tomek
Date: Friday, 25 April 2014 14:02
Subject: [klee-dev] Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom
MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.
Hello Everyone,
I wonder if I can ask a question about KLEE FP here, I am getting an
assertion in Solver.cpp after 1 hour of klee-fp run and I am trying to
understand why.
What is the meaning of this assertion? Am I doing something wrong? How can I
find which line in my code has triggered it?
Any directions would be appreciated!
Thank you very much!
$ clang -emit-llvm -c -g main.cpp
$ time klee -libc=uclibc main.o
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev
KLEE: WARNING: undefined reference to function: _ZSt17__throw_bad_allocv
_ZSt18_Rb_tree_decrementPKSt18_Rb_tree_node_base
_ZSt18_Rb_tree_decrementPSt18_Rb_tree_node_base
_ZSt18_Rb_tree_incrementPKSt18_Rb_tree_node_base
_ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base
_ZSt20__throw_out_of_rangePKc
_ZSt28_Rb_tree_rebalance_for_erasePSt18_Rb_tree_node_baseRS_
_ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_
KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __cxa_end_catch
KLEE: WARNING: undefined reference to function: __cxa_rethrow
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __restore_rt
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: klee_cos
KLEE: WARNING: undefined reference to function: klee_cosf
KLEE: WARNING: undefined reference to function: klee_sin
KLEE: WARNING: undefined reference to function: klee_sinf
KLEE: WARNING: undefined reference to function: klee_sqrt
KLEE: WARNING: undefined reference to function: klee_sqrtf
KLEE: WARNING: undefined reference to function: lseek64
KLEE: WARNING: undefined reference to function: syscall
KLEE: WARNING: undefined reference to function: time
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: _ZNSt8ios_base4InitC1Ev(139919863132416)
KLEE: WARNING: calling external: syscall(16, 0, 21505, 139919863148000)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: time(0)
_ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_(true,
139919863156288, 139919863151184, 139919863151184)
KLEE: WARNING: calling external: exp(0)
_ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base(139919863234656)
klee: Solver.cpp:1103: MINISAT::PropagatedFrom
MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.
0 klee 0x0000000000e6bdcf
1 klee 0x0000000000e6c2d9
2 libpthread.so.0 0x00007f41b29b7cb0
3 libc.so.6 0x00007f41b1c08425 gsignal + 53
4 libc.so.6 0x00007f41b1c0bb8b abort + 379
5 libc.so.6 0x00007f41b1c010ee
6 libc.so.6 0x00007f41b1c01192
7 klee 0x0000000000ec6c85 MINISAT::Solver::propagate(bool) +
1461
8 klee 0x0000000000ece364 MINISAT::Solver::search(int, int,
bool) + 196
9 klee 0x0000000000ecf009
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 1465
10 klee 0x0000000000ebfbe9
BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool,
BEEV::CNFMgr*&, bool, bool) + 3609
11 klee 0x0000000000ec021d
BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int,
BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const,
BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 125
12 klee 0x0000000000ec0dcc BEEV::ToSAT::CallSAT(MINISAT::Solver&,
BEEV::ASTNode const&) + 2956
13 klee 0x0000000000ebce2f
BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 31
14 klee 0x0000000000eabab2
BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 8050
15 klee 0x0000000000eacd8e BEEV::STP::TopLevelSTP(BEEV::ASTNode
const&, BEEV::ASTNode const&) + 238
16 klee 0x0000000000e85a4d vc_query + 157
17 klee 0x0000000000617fa5
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> > >

Post by Kirill Bogdanov
&, bool&) + 1477

18 klee 0x00000000006024ee
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
254
19 klee 0x0000000000603829
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1065
20 klee 0x0000000000600ff0
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 144
21 klee 0x00000000006114cc
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 348
22 klee 0x00000000005d59f2
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 546
23 klee 0x000000000059ab3f
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool,
int) + 303
24 klee 0x00000000005a3f02
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 12706
25 klee 0x00000000005a71a2
klee::Executor::run(klee::ExecutionState&) + 1906
26 klee 0x00000000005a7c1f
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1823
27 klee 0x000000000057ddf8 main + 5320
28 libc.so.6 0x00007f41b1bf376d __libc_start_main + 237
29 klee 0x000000000058df81
Aborted (core dumped)
real 100m21.991s
user 99m41.830s
sys 0m20.345s