[klee-dev] Question on dereferencing a symbol pointer

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>