From f813c88c8cb868fc9c0be78fbf92a94d72ac02b0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 20 Nov 2023 22:41:19 +0000 Subject: Avoid generating array names in solver builders that could accidently collide If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668 --- test/regression/2023-11-20-solver.c | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 test/regression/2023-11-20-solver.c (limited to 'test/regression') diff --git a/test/regression/2023-11-20-solver.c b/test/regression/2023-11-20-solver.c new file mode 100644 index 00000000..ceef8180 --- /dev/null +++ b/test/regression/2023-11-20-solver.c @@ -0,0 +1,36 @@ +// Test case based on #1668, generates array names as part of the solver builder that collide. +// This depends on the order of expression evaluation. +// +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -silent-klee-assume --use-branch-cache=false --use-cex-cache=false --use-independent-solver=false %t1.bc 2>&1 | FileCheck %s +#include "klee/klee.h" +#include + +int main() { + int p1 = klee_int("val"); + int p2 = klee_int("val"); + int p3 = klee_int("val"); + int p4 = klee_int("val"); + int p5 = klee_int("val"); + int p6 = klee_int("val"); + int p7 = klee_int("val"); + int p8 = klee_int("val"); + int p9 = klee_int("val"); + int p10 = klee_int("val"); + int p11 = klee_int("val"); + int p12 = klee_int("val"); + int p13 = klee_int("val"); + int p14 = klee_int("val"); + int p15 = klee_int("val"); + int cond = klee_int("val"); + klee_assume(p12 > p14); + klee_assume(p6 > p3); + // klee_assume(p2 > 0); + klee_assume(p7 != 0); + klee_assume(p11 < p14 & p15 < p13); + klee_assume(cond > p5); + klee_assume(0 > p4); + // CHECK: [[@LINE+1]]: ASSERTION FAIL + assert(p2 > p11); +} \ No newline at end of file -- cgit 1.4.1