From 279be1d2748f9694c27423cc650deb46638736ad Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 7 Jun 2021 16:19:57 +0100 Subject: Test case for externally concretized variables and constraint fully symbolic variables The test case is based on the example provided by Mingyi Liu from the KLEE mailing list. --- test/Feature/ConcretizeSymbolicExternals.c | 35 ++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test/Feature/ConcretizeSymbolicExternals.c diff --git a/test/Feature/ConcretizeSymbolicExternals.c b/test/Feature/ConcretizeSymbolicExternals.c new file mode 100644 index 00000000..89f1ad8d --- /dev/null +++ b/test/Feature/ConcretizeSymbolicExternals.c @@ -0,0 +1,35 @@ +// Check for calling external functions using symbolic parameters. +// Externals calls might modify memory objects that have been previously fully symbolic. +// The constant modifications should be propagated back. +// RUN: %clang %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -external-calls=all %t.bc > %t.log +// RUN: FileCheck -input-file=%t.log %s +// REQUIRES: not-darwin +#include "klee/klee.h" +#include + +int main() { + + int a; + int b; + int c; + + // Symbolize argument that gets concretized by the external call + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + klee_make_symbolic(&c, sizeof(c), "c"); + if (a == 2 && b == 3) { + // Constrain fully symbolic `a` and `b` to concrete values + + // Although a and b are not character vectors, explicitly constraining them to `2` and `3` + // leads to the most significant bits of the int (e.g. bit 8 to 31 of 32bit) set to `\0`. + // This leads to an actual null-termination of the character vector, which makes it safe + // to use by an external function. + printf("%s%s%n\n", (char *)&a, (char *)&b, &c); + printf("after: a = %d b = %d c = %d\n", a, b, c); + //CHECK: after: a = 2 b = 3 c = 2 + } + + return 0; +} -- cgit 1.4.1