klee-float hangs when calling external function.

[guaguagou]

Hello, I am trying to use klee-float to generate test cases for bessel_J0.c in gsl. But when calling the external function cos (), klee hangs.

Compiled as follows: clang -I ../include -I gsl-2.6 -emit-llvm -fsanitize=signed-integer-overflow -fsanitize=unsigned-integer-overflow -c -g -O0 bessel_J0.c

Run as follows:

~/klee/DataVolumeContainer $ klee -libc=uclibc -libm -link-llvm-lib=/usr/local/lib/libgsl.bca -link-llvm-lib=/usr/local/lib/libgslcblas.bca -link-llvm-lib=gsl-2.6/specfunc/libgamma.bca -link-llvm-lib=gsl-2.6/specfunc/libhy.bca -link-llvm-lib=gsl-2.6/specfunc/libhyperg.bca -link-llvm-lib=gsl-2.6/sys/libminmax.bca  -allow-external-sym-calls -pc-float-constants-as-hex-float bessel_J0.bc
KLEE: Linking with libm
KLEE: NOTE: Using klee-uclibc : /usr/local/lib64/klee/runtime/klee-uclibc.bca
KLEE: Linking in library: /usr/local/lib/libgsl.bca.

KLEE: Linking in library: /usr/local/lib/libgslcblas.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libgamma.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libhy.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libhyperg.bca.

KLEE: Linking in library: gsl-2.6/sys/libminmax.bca.

KLEE: output directory is "/home/user/klee/DataVolumeContainer/klee-out-44"
KLEE: Using Z3 solver backend
KLEE: Replacing function "__isnan" with "klee_internal_isnan"
KLEE: Replacing function "__isinf" with "klee_internal_isinf"
KLEE: Replacing function "__finite" with "klee_internal_finite"
KLEE: Replacing function "sqrt" with "klee_internal_sqrt"
KLEE: Replacing function "fabs" with "klee_internal_fabs"
KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: acosh
KLEE: WARNING: undefined reference to function: asin
KLEE: WARNING: undefined reference to function: atan
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: atanh
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: cosh
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: exp2
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: fmod
KLEE: WARNING: undefined reference to function: fprintf
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: hypot
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: log
KLEE: WARNING: undefined reference to function: log1p
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: pow
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sinh
KLEE: WARNING: undefined reference to function: tan
KLEE: WARNING: undefined reference to function: tanh
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 73912336)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(48144816, (ReadLSB w64 0 x), 4607182418800017408)
J0(0)=1.000000000000000000e+00
J0(2.98023e-08)=9.999999999999995559e-01
KLEE: WARNING ONCE: calling external: sin((FAbs w64 (ReadLSB w64 0 x)))
KLEE: WARNING ONCE: calling external: cos((FAbs w64 (ReadLSB w64 0 x)))

The file:

#include <gsl/gsl_math.h>
#include <gsl/gsl_errno.h>
#include <gsl/gsl_mode.h>
#include <specfunc/bessel.h>
#include <specfunc/bessel_amp_phase.h>
#include <gsl/gsl_sf_trig.h>
#include <specfunc/gsl_sf_bessel.h>
#include <klee/klee.h>

#include <specfunc/cheb_eval.c>

static double bj0_data[13] = {
   0.100254161968939137, 
  -0.665223007764405132, 
   0.248983703498281314, 
  -0.0332527231700357697,
   0.0023114179304694015,
  -0.0000991127741995080,
   0.0000028916708643998,
  -0.0000000612108586630,
   0.0000000009838650793,
  -0.0000000000124235515,
   0.0000000000001265433,
  -0.0000000000000010619,
   0.0000000000000000074,
};
static cheb_series bj0_cs = {
  bj0_data,
  12,
  -1, 1,
  9
};

/*-*-*-*-*-*-*-*-*-*-*-* Functions with Error Codes *-*-*-*-*-*-*-*-*-*-*-*/

int gsl_sf_bessel_J0_ee(const double x, gsl_sf_result * result)
{
  double y = fabs(x);

  /* CHECK_POINTER(result) */

  if(y < 2.0*GSL_SQRT_DBL_EPSILON) {
    result->val = 1.0;
    result->err = y*y;
    return GSL_SUCCESS;
  }
  else if(y <= 4.0) {
    return cheb_eval_e(&bj0_cs, 0.125*y*y - 1.0, result);
  }
  else {
    const double z = 32.0/(y*y) - 1.0;
    gsl_sf_result ca;
    gsl_sf_result ct;
    gsl_sf_result cp;
    const int stat_ca = cheb_eval_e(&_gsl_sf_bessel_amp_phase_bm0_cs,  z, &ca);
    const int stat_ct = cheb_eval_e(&_gsl_sf_bessel_amp_phase_bth0_cs, z, &ct);
    const int stat_cp = gsl_sf_bessel_cos_pi4_e(y, ct.val/y, &cp);
    const double sqrty = sqrt(y);
    const double ampl  = (0.75 + ca.val) / sqrty;
    result->val  = ampl * cp.val;
    result->err  = fabs(cp.val) * ca.err/sqrty + fabs(ampl) * cp.err;
    result->err += GSL_DBL_EPSILON * fabs(result->val);
    return GSL_ERROR_SELECT_3(stat_ca, stat_ct, stat_cp);
  }
}

/*-*-*-*-*-*-*-*-*-* Functions w/ Natural Prototypes *-*-*-*-*-*-*-*-*-*-*/

#include <specfunc/eval.h>

double gsl_sf_bessel_J00(const double x)
{
  EVAL_RESULT(gsl_sf_bessel_J0_ee(x, &result));
}

int main(void)
{
  double x;
  klee_make_symbolic(&x, sizeof(x), "x" );
  double y = gsl_sf_bessel_J00(x);
  printf("J0(%g)=%.18e\n", x, y);
  return 0;
}

Then I used the same method to test Hypergeometric Functions hyperg_1F1.c in gsl. An overflow error has occurred and hangs again after running for a long time.

d9c3ffba2519:~/klee/DataVolumeContainer $ klee -link-llvm-lib=/usr/local/lib/libgsl.bca -link-llvm-lib=/usr/local/lib/libgslcblas.bca -link-llvm-lib=gsl-2.6/specfunc/libgamma.bca -link-llvm-lib=gsl-2.6/specfunc/libhy.bca -link-llvm-lib=gsl-2.6/specfunc/libhyperg.bca -link-llvm-lib=gsl-2.6/sys/libminmax.bca  -allow-external-sym-calls hyperg_1F1.bc 
KLEE: Linking in library: /usr/local/lib/libgsl.bca.

KLEE: Linking in library: /usr/local/lib/libgslcblas.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libgamma.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libhy.bca.

KLEE: Linking in library: gsl-2.6/specfunc/libhyperg.bca.

KLEE: Linking in library: gsl-2.6/sys/libminmax.bca.

KLEE: output directory is "/home/user/klee/DataVolumeContainer/klee-out-47"
KLEE: Using Z3 solver backend
KLEE: Replacing function "__isnan" with "klee_internal_isnan"
KLEE: Replacing function "__isinf" with "klee_internal_isinf"
KLEE: Replacing function "__finite" with "klee_internal_finite"
KLEE: Replacing function "sqrt" with "klee_internal_sqrt"
KLEE: Replacing function "fabs" with "klee_internal_fabs"
KLEE: WARNING: undefined reference to function: __ubsan_handle_negate_overflow
KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: acosh
KLEE: WARNING: undefined reference to function: asin
KLEE: WARNING: undefined reference to function: atan
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: atanh
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: cosh
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: exp2
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: fmod
KLEE: WARNING: undefined reference to function: fprintf
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: hypot
KLEE: WARNING: undefined reference to function: log
KLEE: WARNING: undefined reference to function: log1p
KLEE: WARNING: undefined reference to function: pow
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sinh
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to variable: stdout
KLEE: WARNING: undefined reference to function: tan
KLEE: WARNING: undefined reference to function: tanh
KLEE: WARNING ONCE: calling external: exp((ReadLSB w64 0 x))
KLEE: WARNING ONCE: calling external: printf(52212784, (ReadLSB w32 0 m), (ReadLSB w32 0 n), (ReadLSB w64 0 x), 4607182418800017408)
hyperg_1F1(0,0,0)=1.000000000000000000e+00
KLEE: WARNING ONCE: calling external: fprintf(139770400621824, 171217136, 178008688, 1805, 97399824, 96841008)
gsl: hyperg_1F1.c:1805: ERROR: domain error
gsl: exp.c:113: ERROR: underflow
KLEE: WARNING ONCE: calling external: fflush(139770400622048)
KLEE: WARNING ONCE: calling external: fwrite(97400656, 35, 1, 139770400621824)
Default GSL error handler invoked.
KLEE: ERROR: /home/user/klee/DataVolumeContainer/gsl-2.6/err/error.c:47: abort failure
KLEE: NOTE: now ignoring this error at this location
gsl: exp.c:110: ERROR: overflow
Default GSL error handler invoked.
Default GSL error handler invoked.
hyperg_1F1(0,-1,4.45015e-308)=1.000000000000000000e+00
hyperg_1F1(0,0,4.45015e-308)=1.000000000000000000e+00
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:1816: overflow on unsigned subtraction
KLEE: NOTE: now ignoring this error at this location
gsl: hyperg_1F1.c:1814: ERROR: domain error
Default GSL error handler invoked.
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:1820: overflow on unsigned addition
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:1832: overflow on unsigned subtraction
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:1816: overflow on unsigned subtraction
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:1820: overflow on unsigned subtraction
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: calling external: sin((FMul w64 (SIToFP w64 (ReadLSB w32 0 n))
           3.1415926535897931E+0))
KLEE: WARNING ONCE: calling external: log((FDiv w64 (FAdd w64 (FAdd w64 (SIToFP w64 (ReadLSB w32 0 n))
                               -1.0E+0)
                     7.5E+0)
           2.7182818284590451E+0))
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:950: overflow on unsigned addition
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:958: overflow on unsigned addition
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:977: overflow on unsigned multiplication
KLEE: NOTE: now ignoring this error at this location
hyperg_1F1(-1,-2147483648,1.67772e+07)=1.007812500000000000e+00
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:967: overflow on unsigned addition
KLEE: NOTE: now ignoring this error at this location

main:

int main(void)
{
  int m,n;
  double x;
  klee_make_symbolic(&m, sizeof(m), "m" );
  klee_make_symbolic(&n, sizeof(n), "n" );
  klee_make_symbolic(&x, sizeof(x), "x" );
  double y = gsl_sf_hyperg_1F1_int(m,n,x);
  printf("hyperg_1F1(%d,%d,%g)=%.18e\n", m,n,x,y);
  return 0;
}

[guaguagou]

KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:977: overflow on unsigned multiplication
KLEE: NOTE: now ignoring this error at this location
hyperg_1F1(-1,-2147483648,1.67772e+07)=1.007812500000000000e+00
KLEE: ERROR: /home/user/klee/DataVolumeContainer/hyperg_1F1.c:967: overflow on unsigned addition
KLEE: NOTE: now ignoring this error at this location
gsl: exp.c:113: ERROR: underflow
gsl: gamma.c:1227: ERROR: error
KLEE: WARNING ONCE: flushing 4104 bytes on read, may be slow and/or crash: MO255[4104] allocated at global:fact_table
gsl: gamma.c:769: ERROR: error
Default GSL error handler invoked.
Default GSL error handler invoked.
Default GSL error handler invoked.
gsl: exp.c:113: ERROR: underflow
hyperg_1F1(-2,-204472320,124)=1.000001212878472767e+00

[ccadar]

Looking at your logs, I can see that your code invokes sin and cos with a symbolic argument:

KLEE: WARNING ONCE: calling external: sin((FAbs w64 (ReadLSB w64 0 x)))
KLEE: WARNING ONCE: calling external: cos((FAbs w64 (ReadLSB w64 0 x)))

If you want to reason symbolically about these functions, you have two options: 1) Link with an implementation of these functions or 2) Represent them as operands in the expression language, as we do for instance for FAbs (which you can see in the expressions above)

[guaguagou]

Option 1 means I should use wllvm to recompile the uclibc to the llvm bitcode(.bca), right? Because when I use -libc=uclibc and -libm options, klee can't find sin() and cos() functions.

[ccadar]

@guaguagou yes. You would need to reconfigure it first to make sure the implementations for these functions are included. You should also make sure uclibc provides these functions, but I assume it does.