[klee-dev] Question on dereferencing a symbol pointer

[Liu, Mingyi]

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