[klee-dev] Disallow errors on external calls

[Mario García Pérez]

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 disallowedKLEE:
NOTE: now ignoring this error at this locationKLEE: 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?

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?

Thank you in advance.

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