From 4ca5a80836de48036e47f611a6ea610a6fb2b54b Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sun, 29 Nov 2020 20:37:11 +0000 Subject: Test reflecting the LLVM 11 behavior for transforming reads of the form f[k], with k symbolic and f a 4-element vector into something along the lines: if k == 0 => f[0] elif k == 1 => f[1] elif k == 2 => f[2] elif k == 3 => f[3] else ==> undef --- test/VectorInstructions/oob-read-llvm-geq11.c | 46 +++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test/VectorInstructions/oob-read-llvm-geq11.c (limited to 'test') diff --git a/test/VectorInstructions/oob-read-llvm-geq11.c b/test/VectorInstructions/oob-read-llvm-geq11.c new file mode 100644 index 00000000..309e05b1 --- /dev/null +++ b/test/VectorInstructions/oob-read-llvm-geq11.c @@ -0,0 +1,46 @@ +// REQUIRES: geq-llvm-11.0 +// XFAIL: geq-llvm-11.0 + +/* The scalarizer pass in LLVM 11 was changed to generate, for a + read f[k], with k symbolic and f a 4-element vector: + if k == 0 => f[0] + elif k == 1 => f[1] + elif k == 2 => f[2] + elif k == 3 => f[3] + else ==> undef + + Therefore, even though an OOB access might exist at the source code + level, no such OOB accesses exist anymore at the LLVM IR level. + + And since undef is currently treated in KLEE as 0, an overflowing + access is always translated as f[0], which may lead to future + problems being missed. + + This test is marked as XFAIL as a reminder that we need to fix this + behaviour, most likely by having undef return a new symbolic variable. +*/ + +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// NOTE: Have to pass `--optimize=false` to avoid vector operations being +// constant folded away. +// RUN: %klee --output-dir=%t.klee-out --optimize=false --exit-on-error %t1.bc 2>%t.log +// RUN: FileCheck -input-file=%t.stderr.log %s + +#include "klee/klee.h" + +#include +#include +#include + +typedef uint32_t v4ui __attribute__((vector_size(16))); +int main() { + v4ui f = {1, 2, 3, 4}; + int k = klee_range(4, 10, "k"); + + uint32_t v = f[k]; // Symbolic out-of-bounds read + v = f[v]; // This should trigger an error, but currently this returns f[0] = 1 + assert(v != 1); + + return 0; +} -- cgit 1.4.1