[klee-dev] Klee terminating oddly

[Sangharatna Godboley]

Hi Shaheen,

My suggestion:

Try running with below command

klee --max-time=60 --watchdog binmult.bc

Usually max time count is in seconds.

Please check and let us know if it works.

Thanks
Sanghu

On Wed, 1 Jun 2022 at 1:50 PM, Shaheen Cullen-Baratloo <shaheen at gmail.com>
wrote:

> 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
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-- 
---------------------
Thanks & Regards,

Dr. Sangharatna Godboley,
Ph.D.(NITR), Post-Doc(NUS),
Assistant Professor,
IEEE and ACM Member,
ER-22 (Web Chair),
Department of Computer Science and Engineering,
National Institute of Technology (NIT) Warangal,
Telangana, Pin- 506004, India.
Mobile: +91-7013306805
Vidwan Website <https://nitw.irins.org/profile/154056>
-------------- next part --------------
HTML attachment scrubbed and removed