Hi,
The short answer is that KLEE does not support mmap.
However, it shouldn't crash and I cannot reproduce that behaviour: when
I run it, KLEE reports a memory error at "*(int*)addr = 0;", as I also
expected.
Best,
Cristian
On 09/03/2021 14:46, Liu, Mingyi wrote:
Hi klee-dev members,
I made a pointer symbolic in a program, but I didn't understand why the
results were different with the following two scenarios.
Case 1:
#include "klee/klee.h"
#include <stdio.h>
#include <stdlib.h>
#include <sys/mman.h>
#include <unistd.h>
int main(int argc, char* argv[]) {
int* ptr;
klee_make_symbolic(&ptr, sizeof(ptr), "ptr");
void* addr = mmap((void*)(rand() & (~0xfff)), getpagesize(),
PROT_READ | PROT_WRITE, MAP_ANONYMOUS | MAP_FIXED | MAP_PRIVATE, -1, 0);
if (addr == MAP_FAILED) {
printf("mmap error\n");
exit(-1);
}
*(int*)addr = 0;
printf("ptr=%p\n", ptr);
if (ptr == (int*)addr) {
printf("enter\n");
*ptr = 65;
*printf("after: *ptr=%s\n", ptr);*
}
return 0;
}
After running klee with the command $ klee -write-kqueries
-external-calls=all program.bc , I got 2 paths as expected:
KLEE: done: total instructions = 45
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
The output when executing against the second ktest file is shown below:
ptr=0x6b8b4000
enter
after: *ptr=A
However, in Case 2, the only difference is that I replaced
*printf("after: *ptr=**%s**\n", **ptr**);* with *printf("after:
*ptr=%d\n", *ptr); *. When running with the same command, the program
was aborted with the following messages:
klee: /usr/lib/llvm-6.0/include/llvm/Support/Casting.h:92: static
bool llvm::isa_impl_cl<To, From*>::doit(const From*) [with To =
klee::ConstantExpr; From = klee::Expr]: Assertion `Val && "isa<>
used on a null pointer"' failed.
#0 0x00007fe5c64b60ea llvm::sys::PrintStackTrace(llvm::raw_ostream&)
(/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81e0ea)
#1 0x00007fe5c64b4366 llvm::sys::RunSignalHandlers()
(/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81c366)
#2 0x00007fe5c64b449b (/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81c49b)
#3 0x00007fe5c5173fd0 (/lib/x86_64-linux-gnu/libc.so.6+0x3efd0)
#4 0x00007fe5c5173f47 gsignal
/build/glibc-2ORdQG/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
#5 0x00007fe5c51758b1 abort
/build/glibc-2ORdQG/glibc-2.27/stdlib/abort.c:81:0
#6 0x00007fe5c516542a __assert_fail_base
/build/glibc-2ORdQG/glibc-2.27/assert/assert.c:89:0
#7 0x00007fe5c51654a2 (/lib/x86_64-linux-gnu/libc.so.6+0x304a2)
#8 0x000055d863a75ba0
klee::ExprOptimizer::optimizeExpr(klee::ref<klee::Expr> const&,
bool) /vagrant/vagrant/xxx/klee/lib/Expr/ArrayExprOptimizer.cpp:193:0
#9 0x000055d8639dd657
klee::ref<klee::Expr>::operator=(klee::ref<klee::Expr>&&)
/vagrant/vagrant/xxx/klee/include/klee/util/Ref.h:184:0
#10 0x000055d8639dd657
klee::Executor::callExternalFunction(klee::ExecutionState&,
klee::KInstruction*, llvm::Function*,
std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:3366:0
#11 0x000055d8639e9668
klee::Executor::executeCall(klee::ExecutionState&,
klee::KInstruction*, llvm::Function*,
std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:1441:0
#12 0x000055d8639f11e7
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:2015:0
#13 0x000055d8639f27ad klee::Executor::run(klee::ExecutionState&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:3110:0
#14 0x000055d8639f30bc
std::enable_if<std::__and_<std::__not_<std::__is_tuple_like<klee::PTree*>
>, std::is_move_constructible<klee::PTree*>,
std::is_move_assignable<klee::PTree*> >::value, void>::type
std::swap<klee::PTree*>(klee::PTree*&, klee::PTree*&)
/usr/include/c++/7/bits/move.h:198:0
#15 0x000055d8639f30bc std::unique_ptr<klee::PTree,
std::default_delete<klee::PTree> >::reset(klee::PTree*)
/usr/include/c++/7/bits/unique_ptr.h:369:0
#16 0x000055d8639f30bc std::unique_ptr<klee::PTree,
std::default_delete<klee::PTree> >::operator=(decltype(nullptr))
/usr/include/c++/7/bits/unique_ptr.h:307:0
#17 0x000055d8639f30bc
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**,
char**) /vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:4261:0
#18 0x000055d8639c23f3 main
/vagrant/vagrant/xxx/klee/tools/klee/main.cpp:1555:0
#19 0x00007fe5c5156b97 __libc_start_main
/build/glibc-2ORdQG/glibc-2.27/csu/../csu/libc-start.c:344:0
#20 0x000055d8639ce7ea _start (./xxxx/klee+0x6c7ea)
Aborted (core dumped)
Could anyone please explain to me why that assertion failed? Or is it a
bug?
Thanks in advance!
Best,
Mingyi
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
