Incorrrect use of Z3 with floats #114
Description
On a source:
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail("0", "float3.c", 3, "reach_error"); }
int __VERIFIER_nondet_int();
double d = 0.0;
void f1()
{
d = 1.0;
}
int main()
{
int x = 2;
if(__VERIFIER_nondet_int())
x = 4;
(void) f1();
d += (x == 2);
d += (x > 3);
if(!(d == 2.0)) {reach_error();abort();}
}
Compilation commands:
clang -Wno-everything -emit-llvm -Xclang -disable-O0-optnone -g -O0 -fno-default-inline -c test.c -o test.bc
clang -emit-llvm -Xclang -disable-O0-optnone -g -c -fno-default-inline klee-test-comp.c -o klee-test-comp.bc
llvm-link klee-test-comp.bc test.bc -o test.bcRun commands:
klee --optimize test.bcLog:
Error: Incorrect use of Z3. [3] fp sort expected
#0 0x00007f02fee3fd01 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe3fd01)
#1 0x00007f02fee3da0c llvm::sys::RunSignalHandlers() (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe3da0c)
#2 0x00007f02fee40236 (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe40236)
#3 0x00007f02fd842520 (/lib/x86_64-linux-gnu/libc.so.6+0x42520)
#4 0x00007f02fd896a7c __pthread_kill_implementation ./nptl/./nptl/pthread_kill.c:44:76
#5 0x00007f02fd896a7c __pthread_kill_internal ./nptl/./nptl/pthread_kill.c:78:10
#6 0x00007f02fd896a7c pthread_kill ./nptl/./nptl/pthread_kill.c:89:10
#7 0x00007f02fd842476 gsignal ./signal/../sysdeps/posix/raise.c:27:6
#8 0x00007f02fd8287f3 abort ./stdlib/./stdlib/abort.c:81:7
#9 0x000055b42d8bee30 klee::Z3NodeHandle<_Z3_sort*>::dump() /home/user/Documents/klee/lib/Solver/Z3Builder.cpp:33:48
#10 0x00007f0304c2116d Z3_fpa_get_ebits (/home/user/klee_build/z3-4.8.15-install/lib/libz3.so+0x22116d)
#11 0x000055b42d8c660f klee::Z3BitvectorBuilder::castToBitVector(klee::Z3NodeHandle<_Z3_ast*> const&) /home/user/Documents/klee/lib/Solver/Z3BitvectorBuilder.cpp:1070:25
#12 0x000055b42d8cdad3 klee::Z3NodeHandle<_Z3_ast*>::~Z3NodeHandle() /home/user/Documents/klee/lib/Solver/Z3Builder.h:45:9
#13 0x000055b42d8cdad3 klee::Z3BitvectorBuilder::constructActual(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/lib/Solver/Z3Builder.h:44:3
#14 0x000055b42d8c0fc3 klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#15 0x000055b42d8c0fc3 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#16 0x000055b42d8c0fc3 klee::Z3Builder::construct(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/include/klee/ADT/Ref.h:85:3
#17 0x000055b42d8cc286 klee::Z3BitvectorBuilder::constructActual(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/lib/Solver/Z3BitvectorBuilder.cpp:794:70
#18 0x000055b42d8c0fc3 klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#19 0x000055b42d8c0fc3 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#20 0x000055b42d8c0fc3 klee::Z3Builder::construct(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/include/klee/ADT/Ref.h:85:3
#21 0x000055b42d8cc211 klee::Z3BitvectorBuilder::constructActual(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/lib/Solver/Z3BitvectorBuilder.cpp:793:68
#22 0x000055b42d8c0fc3 klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#23 0x000055b42d8c0fc3 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#24 0x000055b42d8c0fc3 klee::Z3Builder::construct(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/include/klee/ADT/Ref.h:85:3
#25 0x000055b42d8ca5e1 klee::Z3BitvectorBuilder::constructActual(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/lib/Solver/Z3BitvectorBuilder.cpp:725:68
#26 0x000055b42d8c0fc3 klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#27 0x000055b42d8c0fc3 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#28 0x000055b42d8c0fc3 klee::Z3Builder::construct(klee::ref<klee::Expr>, int*) /home/user/Documents/klee/include/klee/ADT/Ref.h:85:3
#29 0x000055b42d8a946c klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#30 0x000055b42d8a946c klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#31 0x000055b42d8a946c klee::Z3Builder::construct(klee::ref<klee::Expr>) /home/user/Documents/klee/include/klee/ADT/Ref.h:85:3
#32 0x000055b42d8a946c klee::Z3SolverImpl::internalRunSolver(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const*, std::vector<klee::SparseStorage<unsigned char>, std::allocator<klee::SparseStorage<unsigned char> > >*, klee::ValidityCore*, bool&) /home/user/Documents/klee/lib/Solver/Z3Solver.cpp:406:37
#33 0x000055b42d8ab127 klee::Z3SolverImpl::check(klee::Query const&, klee::ref<klee::SolverResponse>&) /home/user/Documents/klee/lib/Solver/Z3Solver.cpp:326:24
#34 0x000055b42d8b5e39 CexCachingSolver::getResponse(klee::Query const&, klee::ref<klee::SolverResponse>&) /home/user/Documents/klee/lib/Solver/CexCachingSolver.cpp:246:27
#35 0x000055b42d8b754d CexCachingSolver::computeValidity(klee::Query const&, klee::PartialValidity&) /home/user/Documents/klee/lib/Solver/CexCachingSolver.cpp:302:21
#36 0x000055b42d8b0ff5 CachingSolver::computeValidity(klee::Query const&, klee::PartialValidity&) /home/user/Documents/klee/lib/Solver/CachingSolver.cpp:223:37
#37 0x000055b42d88cb76 klee::ref<klee::Expr>::dec() const /home/user/Documents/klee/include/klee/ADT/Ref.h:94:9
#38 0x000055b42d88cb76 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#39 0x000055b42d88cb76 klee::Query::~Query() /home/user/Documents/klee/include/klee/Solver/SolverUtil.h:46:8
#40 0x000055b42d88cb76 IndependentSolver::computeValidity(klee::Query const&, klee::PartialValidity&) /home/user/Documents/klee/lib/Solver/IndependentSolver.cpp:73:61
#41 0x000055b42d859a6a klee::TimingSolver::evaluate(klee::ConstraintSet const&, klee::ref<klee::Expr>, klee::PartialValidity&, klee::SolverQueryMetaData&, bool) /home/user/Documents/klee/lib/Core/TimingSolver.cpp:51:40
#42 0x000055b42d7f0f22 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#43 0x000055b42d7f0f22 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, klee::KBlock*, klee::KBlock*, BranchType) /home/user/Documents/klee/lib/Core/Executor.cpp:1200:31
#44 0x000055b42d80c791 klee::ref<klee::Expr>::~ref() /home/user/Documents/klee/include/klee/ADT/Ref.h:85:15
#45 0x000055b42d80c791 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) /home/user/Documents/klee/lib/Core/Executor.cpp:2566:15
#46 0x000055b42d80f1fe klee::Executor::executeStep(klee::ExecutionState&) /home/user/Documents/klee/lib/Core/Executor.cpp:4372:16
#47 0x000055b42d80f633 klee::Executor::run(std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> >) /home/user/Documents/klee/lib/Core/Executor.cpp:4290:13
#48 0x000055b42d810899 std::_Vector_base<klee::ExecutionState*, std::allocator<klee::ExecutionState*> >::~_Vector_base() /usr/include/c++/11/bits/stl_vector.h:336:45
#49 0x000055b42d810899 std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> >::~vector() /usr/include/c++/11/bits/stl_vector.h:683:7
#50 0x000055b42d810899 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) /home/user/Documents/klee/lib/Core/Executor.cpp:6717:6
#51 0x000055b42d7c4cfe __gnu_cxx::__normal_iterator<KTest* const*, std::vector<KTest*, std::allocator<KTest*> > >::__normal_iterator(KTest* const* const&) /usr/include/c++/11/bits/stl_iterator.h:1028:9
#52 0x000055b42d7c4cfe std::vector<KTest*, std::allocator<KTest*> >::end() const /usr/include/c++/11/bits/stl_vector.h:839:16
#53 0x000055b42d7c4cfe std::vector<KTest*, std::allocator<KTest*> >::empty() const /usr/include/c++/11/bits/stl_vector.h:1008:30
#54 0x000055b42d7c4cfe run_klee_on_function(int, char**, char**, std::unique_ptr<KleeHandler, std::default_delete<KleeHandler> >&, std::unique_ptr<klee::Interpreter, std::default_delete<klee::Interpreter> >&, llvm::Module*, std::vector<bool, std::allocator<bool> >&) (.isra.0) /home/user/Documents/klee/tools/klee/main.cpp:1507:24
#55 0x000055b42d7a48af main /home/user/Documents/klee/tools/klee/main.cpp:2029:25
#56 0x00007f02fd829d90 __libc_start_call_main ./csu/../sysdeps/nptl/libc_start_call_main.h:58:16
#57 0x00007f02fd829e40 call_init ./csu/../csu/libc-start.c:128:20
#58 0x00007f02fd829e40 __libc_start_main ./csu/../csu/libc-start.c:379:5
#59 0x000055b42d7be145 _start (/home/user/klee_build/klee_build140stp_z3/bin/klee+0x56145)