[klee-dev] Disallow errors on external calls

[Nowack, Martin]

Hi Mario,

On 20. Jun 2022, at 18:44, Mario García Pérez <mgarcp13 at gmail.com<mailto:mgarcp13 at gmail.com>> wrote:

Hi,

I'm using klee with gnat-llvm generated bytecodes (to execute symbolically Ada programs) and I have some problems.

When executing the program there are done some runtime checks, that are done by calling to GNAT external functions, such as __gnat_rcheck_CE_Overflow_Check. By running klee with option --external-calls=none the call to external functions are disallowed but an error is raised which caused that the path is not completed:

KLEE: output directory is "/home/mario/automatic_ada_symbolic_execution/klee-out-15"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: __gnat_rcheck_CE_Overflow_Check
KLEE: WARNING ONCE: String not terminated by \0 passed to one of the klee_ functions
KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check

KLEE: ERROR: (location information missing) external calls disallowed
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check

KLEE: ERROR: (location information missing) external calls disallowed
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check

KLEE: ERROR: (location information missing) external calls disallowed
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check


KLEE: done: total instructions = 129
KLEE: done: completed paths = 4
KLEE: done: partially completed paths = 4
KLEE: done: generated tests = 7

There are any option to skip this error and complete the path?

One way would be to remove the calls to those functions. Use an external LLVM opt pass or add this feature to KLEE, i.e. have a look here: https://github.com/klee/klee/tree/master/lib/Module to give you an idea.



In addition, I have a bytecode with all the gnat libraries, but linking with it gives some errors while executing some instructions (the module is broken, so I have to switch the option --disable-verify=true):

klee: /home/mario/klee/include/klee/ADT/Bits.h:79: uint64_t klee::bits64::truncateToNBits(uint64_t, unsigned int): Assertion `N > 0 && N <= 64' failed.
 #0 0x00000000028dd261 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:565:22
 #1 0x00000000028dd324 PrintStackTraceSignalHandler(void*) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:632:1
 #2 0x00000000028db1ba llvm::sys::RunSignalHandlers() /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Signals.cpp:97:20
 #3 0x00000000028dcc99 SignalHandler(int) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:407:1
 #4 0x00007f24b69b2140 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x14140)
 #5 0x00007f24b647bce1 raise (/lib/x86_64-linux-gnu/libc.so.6+0x3bce1)
 #6 0x00007f24b6465537 abort (/lib/x86_64-linux-gnu/libc.so.6+0x25537)
 #7 0x00007f24b646540f (/lib/x86_64-linux-gnu/libc.so.6+0x2540f)
 #8 0x00007f24b6474662 (/lib/x86_64-linux-gnu/libc.so.6+0x34662)
 #9 0x0000000000429f8d /home/mario/klee/include/klee/ADT/Bits.h:79:7
#10 0x000000000044d389 klee::ConstantExpr::create(unsigned long, unsigned int) /home/mario/klee/include/klee/ADT/Ref.h:93:7
#11 0x00000000004554f7 klee::Executor::evalConstant(llvm::Constant const*, klee::KInstruction const*) /home/mario/klee/lib/Core/ExecutorUtil.cpp:63:73
#12 0x0000000000455752 llvm::StructLayout::getElementOffset(unsigned int) const /usr/local/include/llvm/IR/DataLayout.h:635:5
#13 0x0000000000455752 llvm::StructLayout::getElementOffsetInBits(unsigned int) const /usr/local/include/llvm/IR/DataLayout.h:640:28
#14 0x0000000000455752 klee::Executor::evalConstant(llvm::Constant const*, klee::KInstruction const*) /home/mario/klee/lib/Core/ExecutorUtil.cpp:84:59
#15 0x000000000043985e klee::ref<klee::Expr>& klee::ref<klee::Expr>::operator=<klee::ConstantExpr>(klee::ref<klee::ConstantExpr>&&) /home/mario/klee/include/klee/ADT/Ref.h:188:5
#16 0x000000000043985e klee::Executor::bindModuleConstants() /home/mario/klee/lib/Core/Executor.cpp:3384:49
#17 0x0000000000449efc klee::Executor::run(klee::ExecutionState&) /home/mario/klee/lib/Core/Executor.cpp:3446:15
#18 0x000000000044b048 std::__uniq_ptr_impl<klee::PTree, std::default_delete<klee::PTree> >::reset(klee::PTree*) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:179:16
#19 0x000000000044b048 std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::reset(klee::PTree*) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:460:12
#20 0x000000000044b048 std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::operator=(std::nullptr_t) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:401:7
#21 0x000000000044b048 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) /home/mario/klee/lib/Core/Executor.cpp:4437:17
#22 0x0000000000414be7 main /home/mario/klee/tools/klee/main.cpp:1532:5
#23 0x00007f24b6466d0a __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x26d0a)
#24 0x0000000000421d6a _start (/usr/local/bin/klee+0x421d6a)
Aborted (core dumped)

Why is this error due to? Is a problem with the bytecode or it can be solved any way?

According to the stack trace, there is a constant generated that is larger than 64bit for an structure access.
Unfortunately, I cannot tell you anything more without bitcode.


Best,
Martin


-------------- next part --------------
HTML attachment scrubbed and removed