Divide by zero occurring when division is performed with a result of a multiplication

[Himeshi]

The following code produces a divide by zero error even with --scaling argument.

int main() { int a = 3, b = 2, answer;

klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");

klee_track_error(&a, "error_a");
klee_track_error(&b, "error_b");

answer = a + (b * b);

klee_bound_error(answer, "answer", 1.3);
return 0; }

The expression for answer however contains the scaling expression.

[domainexpert]

@Himeshi I failed to observe this. I tried the following more complete version:

/*
 * This example triggers division by zero when run with scaling.
 *
 * Copyright 2018 National University of Singapore
 *
 * by Himeshi De Silva <himeshidslv@gmail.com>
 */
#include <klee/klee.h>

int main() {
  int a = 3, b = 2, answer;

  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");

  klee_track_error(&a, "error_a");
  klee_track_error(&b, "error_b");

  answer = a + (b * b);

  klee_bound_error(answer, "answer", 1.3);
  return 0;
}

What were the exact options you ran KLEE with?

[Himeshi]

klee --write-kqueries --precision --scaling add_test.bc

[domainexpert]

@Himeshi I am still not able to observe the issue.

[Himeshi]

It should be a divide, not an add which computes the answer. Corrected code below.

/*
 * This example triggers division by zero when run with scaling.
 *
 * Copyright 2018 National University of Singapore
 *
 * by Himeshi De Silva <himeshidslv@gmail.com>
 */
#include <klee/klee.h>

int main() {
  int a = 3, b = 2, answer;

  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");

  klee_track_error(&a, "error_a");
  klee_track_error(&b, "error_b");

  answer = a  /  (b * b);

  klee_bound_error(answer, "answer", 1.3);
  return 0;
}

[domainexpert]

@Himeshi Ok confirmed. I'll work on this. This is my output:

KLEE: output directory is "/home/andrew/software/fp-examples/basic/klee-out-0"
KLEE: Using STP solver backend
KLEE: ERROR: /home/andrew/software/fp-examples/basic/division.c:19: divide by zero
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 26
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

[domainexpert]

@Himeshi This seems to not actually be a problem. This is because indeed division by zero should occur because b is symbolic (thus there is a possibility that b times b = 0). Now, the purpose of scaling is to multiply the numerator by a constant so that the result of division does not get rounded to 0. The scaling cannot prevent division by zero when, as in this case, the divisor is a symbolic value that can be assigned 0.

I will let you close this issue if you agree.