klee / klee

KLEE Symbolic Execution Engine
https://klee-se.org/
Other
2.64k stars 683 forks source link

KLEE misses assertion violation with option --use-fast-cex-solver #1666

Open salvadorer opened 1 year ago

salvadorer commented 1 year ago

Dear all, I found that the assertion violation in the following code is missed if you call KLEE with option --use-fast-cex-solver, but finds it if you omit the option:

#include <assert.h>
#include "klee/klee.h"

int N = 13;
int main() {
  int a[N];
  for (int j = 0; j < N - 1; j++) {
    a[j] = klee_int("a[j]");
    klee_assume(a[j] < 2139062144);
  }
  a[N - 1] = 100;
  klee_assume(100 < a[N-2]);
  int i = 2;
  while (i < N) {
    if (a[i] > a[i - 1]) {
      klee_assume(0);
    }
    i = i + 1;
  }
  assert(a[2] <= a[3]);
  return 0;
}

I compiled with clang-14 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I ~/klee/include/ test.c and executed klee --use-fast-cex-solver test.bc. KLEE's output is given by: KLEE: output directory is "/home/klee-out-5" KLEE: Using Z3 solver backend KLEE: Deterministic allocator: Using quarantine queue size 8 KLEE: Deterministic allocator: globals (start-address=0x7fb6ca600000 size=10 GiB) KLEE: Deterministic allocator: constants (start-address=0x7fb44a600000 size=10 GiB) KLEE: Deterministic allocator: heap (start-address=0x7eb44a600000 size=1024 GiB) KLEE: Deterministic allocator: stack (start-address=0x7e944a600000 size=128 GiB) WARNING: this target does not support the llvm.stacksave intrinsic. KLEE: ERROR: test.c:16: invalid klee_assume call (provably false) KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 655 KLEE: done: completed paths = 1 KLEE: done: partially completed paths = 10 KLEE: done: generated tests = 2

KLEE's version is: KLEE 3.1-pre (https://klee.github.io) Build mode: RelWithDebInfo (Asserts: ON) Build revision: 9edf8e8bba51f2d217ead0a9b2469b0b551ad255

Ubuntu LLVM version 14.0.0

Optimized build. Default target: x86_64-pc-linux-gnu Host CPU: alderlake

ccadar commented 1 year ago

Thanks for the report. As documented, --use-fast-cex-solver is an experimental feature, which as far as I know is not being used much. Have you found it useful, or are you testing KLEE?