From 087cc9e32b06d48baea03588fb4ee5ca6fa6c907 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 22 Aug 2026 18:21:09 -0400 Subject: [PATCH] fix(klee): name symbolic objects by their type, not by unexpanded macro text klee_make_symbolic(&non_det, sizeof(non_det), "non_det_#type"); `#type` inside a string literal is not the stringify operator -- it is the two characters # and t. Every symbolic object in every .ktest was called the literal "non_det_#type": the same name for an int, a double and a char. Nothing read that name, which is how it survived every baseline this tool has run. The nondet log carries its own type column, so suites and verdicts were correct and there was no symptom to notice. It matters now. KLEE writes one .ktest per explored path, each holding that path's input vector in consumption order -- exactly the material a Cover-Branches suite is made of, produced by the engine for free and without perturbing the search. A .ktest records each object's name, size and bytes but NOT its type, so the name is the only place a type can travel. Without it four bytes could be an int, a float or half of a long and nothing tells them apart. before: object 0: name: 'non_det_#type' size: 4 object 1: name: 'non_det_#type' size: 1 after: object 0: name: 'non_det_int' size: 4 int: 42 object 1: name: 'non_det_char' size: 1 int: 122 The test asserts the pairing of name to size, not just the names: a one-byte object called non_det_int would be worse than no name at all. Writing it also caught a trap worth recording -- klee-last is a symlink, and `find` does not descend into a symlinked start point without -L, so the first version reported "no ktest files" on a run that had produced three. Verified against a full build: new test 5/5, emission suite still 14/14. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 1 + .../backend/library/lib/NonDetGeneratorKlee.c | 13 +- tests/integration/test_ktest_object_names.sh | 120 ++++++++++++++++++ 3 files changed, 133 insertions(+), 1 deletion(-) create mode 100755 tests/integration/test_ktest_object_names.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 05113123e..28cfbf0ce 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -365,6 +365,7 @@ jobs: bash tests/integration/test_add_invariants.sh bash tests/integration/test_test_suite_emission.sh bash tests/integration/test_target_coverage.sh + bash tests/integration/test_ktest_object_names.sh ' # =========================================================== diff --git a/modules/backend/library/lib/NonDetGeneratorKlee.c b/modules/backend/library/lib/NonDetGeneratorKlee.c index 1e92d15e8..74bb6b721 100644 --- a/modules/backend/library/lib/NonDetGeneratorKlee.c +++ b/modules/backend/library/lib/NonDetGeneratorKlee.c @@ -27,10 +27,21 @@ void nondet_assume(int expr) { klee_assume(expr); } extern void klee_make_symbolic(void *addr, size_t nbytes, const char *name); +/* "non_det_" #type, not "non_det_#type". The stringify operator only applies + * to a macro parameter written OUTSIDE a string literal; inside one, # and t + * are just two characters. Every symbolic object was therefore named the + * literal text "non_det_#type" -- the same for an int, a double and a char. + * + * Nothing read that name, which is how it survived: the nondet log carries its + * own type column. It matters now because KLEE writes one .ktest per explored + * path, holding exactly the input vectors a Cover-Branches suite needs, and a + * .ktest records each object's name and size but not its type. With the name + * fixed the type travels with the object; without it, four bytes could be an + * int, a float or half of a long, and nothing tells them apart. */ #define MAP2CHECK_NON_DET_GENERATOR(type) \ type map2check_non_det_##type() { \ type non_det; \ - klee_make_symbolic(&non_det, sizeof(non_det), "non_det_#type"); \ + klee_make_symbolic(&non_det, sizeof(non_det), "non_det_" #type); \ return non_det; \ } diff --git a/tests/integration/test_ktest_object_names.sh b/tests/integration/test_ktest_object_names.sh new file mode 100755 index 000000000..0b99e554c --- /dev/null +++ b/tests/integration/test_ktest_object_names.sh @@ -0,0 +1,120 @@ +#!/bin/bash +# test_ktest_object_names.sh -- symbolic objects must be named by their type. +# +# KLEE writes one .ktest per explored path, and each holds that path's input +# vector: the symbolic objects in the order the program consumed them. That is +# exactly the material a Cover-Branches suite is made of, produced by the +# engine at no cost and without perturbing the search. +# +# What a .ktest records per object is a NAME, a SIZE and the bytes -- not a +# type. So the name is the only place the type can travel, and it got there by +# accident of a macro: +# +# klee_make_symbolic(&non_det, sizeof(non_det), "non_det_#type"); +# +# `#type` inside a string literal is not the stringify operator, it is the two +# characters # and t. Every object in every .ktest was called "non_det_#type", +# identical for an int, a double and a char. Nothing read it, so nothing broke, +# and it survived every baseline this tool has run. +# +# This test exists because the bug was invisible: the suites were correct, the +# verdicts were correct, and only a consumer of the .ktest files would ever +# notice. Now there is one. + +set -u + +MAP2CHECK_DIR="${MAP2CHECK_PATH:-/workspace/install_e2e}" +MAP2CHECK="$MAP2CHECK_DIR/map2check" +KTEST_TOOL="$MAP2CHECK_DIR/bin/ktest-tool" + +PASSED=0 +FAILED=0 +ok() { echo " PASS $1"; PASSED=$((PASSED+1)); } +fail() { echo " FAIL $1: $2"; FAILED=$((FAILED+1)); } + +WORK=$(mktemp -d) +trap 'rm -rf "$WORK"' EXIT + +# Two different types, so a name that ignored the type would collide visibly. +# The sizes differ too (4 and 1), which is what makes the collision harmful: +# without the name there is nothing to say whether one byte is a char or the +# low byte of something wider. +cat > "$WORK/typed.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern char __VERIFIER_nondet_char(void); +extern void reach_error(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + char c = __VERIFIER_nondet_char(); + if (a == 42 && c == 'z') { reach_error(); } + return 0; +} +EOF + +echo "=== KLEE symbolic object names ===" + +if [ ! -x "$KTEST_TOOL" ]; then + fail "ktest-tool available" "not found at $KTEST_TOOL" + echo " Results: $PASSED passed, $FAILED failed" + exit 1 +fi + +# --debug keeps the scratch directory, which is where klee-last lives. +( cd "$WORK" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 250 \ + "$MAP2CHECK" --target-function --target-function-name reach_error \ + --nondet-generator symex --debug --timeout 120 typed.c ) \ + > "$WORK/run.log" 2>&1 + +scratch=$(find "$WORK" -maxdepth 1 -name '*.map2check' -print -quit) +if [ -z "$scratch" ]; then + fail "scratch directory kept" "no *.map2check directory under --debug" + echo " Results: $PASSED passed, $FAILED failed" + exit 1 +fi + +# -L: klee-last is a symlink to klee-out-N, and find does not descend into a +# symlinked start point without it. Without the -L this reported "no ktest +# files" on a run that had produced three. +mapfile -t ktests < <(find -L "$scratch/klee-last" -name '*.ktest' 2>/dev/null | sort) +if [ "${#ktests[@]}" -ge 1 ]; then + ok "KLEE produced per-path test vectors (${#ktests[@]})" +else + fail "ktest files" "none produced" + echo " Results: $PASSED passed, $FAILED failed" + exit 1 +fi + +# The last one is the deepest path, the one that satisfied both conditions. +dump=$("$KTEST_TOOL" "${ktests[-1]}" 2>&1) + +if echo "$dump" | grep -q "non_det_#type"; then + fail "object names carry the type" \ + "still the literal 'non_det_#type' -- the macro does not stringify" +else + ok "no object is named with the unexpanded macro text" +fi + +if echo "$dump" | grep -q "name: 'non_det_int'"; then + ok "the int read is named non_det_int" +else + fail "int object name" "$(echo "$dump" | grep -m1 name)" +fi + +if echo "$dump" | grep -q "name: 'non_det_char'"; then + ok "the char read is named non_det_char" +else + fail "char object name" "$(echo "$dump" | grep -m2 name | tail -1)" +fi + +# Names alone are not enough: the pairing of name to size is what lets a +# consumer decode the bytes. A char named non_det_int would be worse than no +# name at all. +if echo "$dump" | grep -A1 "name: 'non_det_char'" | grep -q "size: 1"; then + ok "non_det_char is one byte, as its name promises" +else + fail "char object size" "not 1" +fi + +echo " ---" +echo " Results: $PASSED passed, $FAILED failed" +[ "$FAILED" -eq 0 ] || exit 1