[klee-dev] Klee terminating oddly

[Shaheen Cullen-Baratloo]

Hi,

I'm running Klee on a program that performs binary multiplication:
-------

#include <stdio.h>

#include <klee/klee.h>


int binmult(long binary1, long binary2)

{


    long multiply = 0;

    int digit, factor = 1;

    while (binary2 != 0)

    {

        digit =  binary2 % 10;

        if (digit == 1)

        {

            binary1 = binary1 * factor;


            int i = 0, remainder = 0, sum[20];

            int binaryprod = 0;


            while (binary1 != 0 || binary2 != 0)

            {

                sum[i++] =(binary1 % 10 + binary2 % 10 + remainder) % 2;

                remainder =(binary1 % 10 + binary2 % 10 + remainder) / 2;

                binary1 = binary1 / 10;

                binary2 = binary2 / 10;

            }

            if (remainder != 0)

                sum[i++] = remainder;

            --i;

            while (i >= 0)

                binaryprod = binaryprod * 10 + sum[i--];

            multiply = binaryprod;

        }

        else

            binary1 = binary1 * factor;

        binary2 = binary2 / 10;

        factor = 10;

    }

    return 0;

}


int main() {


  long binary1;

  klee_make_symbolic(&binary1, sizeof(binary1),
"2b6700e0c99f4934b960a895efa60e22");


  long binary2;

  klee_make_symbolic(&binary2, sizeof(binary2),
"f55f4c1e835743c3b415e6f1290b372f");

  return binmult(binary1, binary2);

}

-------

I'm compiling it with

clang-6.0 -I /app/klee/include -emit-llvm -c -g -O0 -Xclang
-disable-O0-optnone binmult.c

and running klee with

klee --max-time=1min --watchdog binmult.bc


On a computer running Ubuntu 22.04, running this occasionally works
properly but mostly gives me a message about solver failure, and then
trying to check the output gives incomplete results (there's no number for
paths covered, for example):

-------

KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT


KLEE: WARNING: Unexpected solver failure. Reason is "interrupted from
keyboard,"


/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1a)[0x7ff50e16471a]

/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x3e)[0x7ff50e1627ee]

/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1(+0x92097d)[0x7ff50e16297d]

/lib/x86_64-linux-gnu/libc.so.6(+0x37840)[0x7ff50d395840]

/lib/x86_64-linux-gnu/libc.so.6(gsignal+0x10b)[0x7ff50d3957bb]

/lib/x86_64-linux-gnu/libc.so.6(abort+0x121)[0x7ff50d380535]

klee(+0xbf782)[0x56326e66a782]

klee(+0xc06cf)[0x56326e66b6cf]

klee(+0xc3fb0)[0x56326e66efb0]

klee(+0xc4864)[0x56326e66f864]

klee(+0xc29f5)[0x56326e66d9f5]

klee(+0xb8387)[0x56326e663387]

klee(+0x838ed)[0x56326e62e8ed]

klee(+0x4d08e)[0x56326e5f808e]

klee(+0x564b6)[0x56326e6014b6]

klee(+0x5be21)[0x56326e606e21]

klee(+0x5c6a5)[0x56326e6076a5]

klee(+0x2d919)[0x56326e5d8919]

/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xeb)[0x7ff50d38209b]

klee(+0x3928a)[0x56326e5e428a]

KLEE: WARNING: KLEE: watchdog exiting (no child)

-------


On my 2019 MacBook Pro running macOS Monterey, the error happens very
occasionally but it usually runs and terminates fine. I am running Klee in
a Docker image, so it's extra strange that the two machines run
differently. Does anyone have any idea why this could be happening, and how
to get the path count/test count to display properly when the program halts?


Thanks,

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