From 705417abf3205a23bae71c607e525b1ba3d82dcc Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 22 Aug 2026 17:47:05 -0400 Subject: [PATCH] fix(nondet-log): unsigned rows carried a duplicated value column nondet_log_to_file wrote the value with two independent `if`s where the first had no `else`: if (type == UNSIGNED) fprintf("%u;", ...); if (type == DOUBLE) fprintf("%lf;", ...); else fprintf("%d;", ...); so an UNSIGNED row fell through into the %d arm as well and printed its value twice. Reproduced against the installed binary before touching anything: 0;3;17;main;0;5;5;5 eight fields, where the format has seven It parsed by accident. The value column is first, so it still landed at index 5 and readNonDetLog kept reading the right number -- which is why the emitted test suites were correct and nothing caught this. What moved is the type column, to index 7, so any consumer of it gets a copy of the value instead. Only __VERIFIER_nondet_unsigned reaches the UNSIGNED enumerator. __VERIFIER_nondet_uint is tagged UINT (13), a different one, and always took the arm that was right. That is why it survived the whole baseline. Two assertions added where the format is actually produced: every row has exactly seven fields, and the type survives as the last one. They run in their own subdirectory because --debug keeps the scratch directory and the cleanup assertion below them looks for exactly that at depth 1. Verified against a full build: emission suite 14/14. Co-Authored-By: Claude Opus 5 (1M context) --- modules/backend/library/lib/NonDetLog.c | 12 +++-- tests/integration/test_test_suite_emission.sh | 53 +++++++++++++++++++ 2 files changed, 61 insertions(+), 4 deletions(-) diff --git a/modules/backend/library/lib/NonDetLog.c b/modules/backend/library/lib/NonDetLog.c index c67dd5f7d..5c458cfae 100644 --- a/modules/backend/library/lib/NonDetLog.c +++ b/modules/backend/library/lib/NonDetLog.c @@ -36,13 +36,17 @@ Bool nondet_log_to_file(MAP2CHECK_CONTAINER klee_container) { // The value generated from nondet function. Read inline: it is stored in // the row, not behind a pointer into a stack frame that no longer exists. + /* else-if, not two independent ifs. The UNSIGNED arm used to be an `if` + * with no `else`, so an unsigned row fell through into the `%d` arm as + * well and printed its value TWICE: `0;3;17;main;0;5;5;5`, eight fields + * where the format has seven. The value column still parsed by accident, + * being first, but the type column moved to index 7 and anything reading + * it got a copy of the value instead. */ if (((int)call->type) == UNSIGNED) { fprintf(output, "%u;", call->value.as_unsigned); - } - if (((int)call->type) == DOUBLE) { + } else if (((int)call->type) == DOUBLE) { fprintf(output, "%lf;", call->value.as_double); - } - else { + } else { fprintf(output, "%d;", call->value.as_int); } diff --git a/tests/integration/test_test_suite_emission.sh b/tests/integration/test_test_suite_emission.sh index dd58904c7..a95030140 100644 --- a/tests/integration/test_test_suite_emission.sh +++ b/tests/integration/test_test_suite_emission.sh @@ -123,6 +123,59 @@ else fail "input vector" "expected [42, 7], got [${inputs[*]}]" fi +# --- the nondet log's own shape ----------------------------------------------- +# The suite is only as good as the CSV it is serialized from, and that CSV is +# written by the C runtime, where nothing else checks it. An UNSIGNED row used +# to come out with EIGHT fields instead of seven: the UNSIGNED arm of the writer +# was an `if` with no `else`, so the value was printed once as %u and again as +# %d. It parsed by accident -- the value column is first, so it still landed at +# index 5 -- while the type column silently moved to index 7. +# +# Checked on __VERIFIER_nondet_unsigned specifically: __VERIFIER_nondet_uint is +# tagged UINT, a different enumerator, and takes the arm that was always right. +# +# Runs in its own subdirectory, because --debug keeps the scratch directory and +# the cleanup assertion below looks for exactly that at depth 1 of $WORK. +UWORK="$WORK/unsigned_run" +mkdir -p "$UWORK" +cat > "$UWORK/unsigned.c" <<'EOF' +extern unsigned __VERIFIER_nondet_unsigned(void); +extern void reach_error(void); +int main(void) { + unsigned u = __VERIFIER_nondet_unsigned(); + if (u == 5u) { reach_error(); } + return 0; +} +EOF + +( + cd "$UWORK" || exit 1 + MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error \ + --nondet-generator symex --debug --timeout 120 unsigned.c +) > "$UWORK/unsigned.log" 2>&1 + +csv=$(find "$UWORK" -name klee_log.csv -print -quit) +if [ -z "$csv" ]; then + fail "unsigned nondet log" "no klee_log.csv produced" +else + malformed=$(awk -F';' 'NF != 7 {print NF" fields: "$0}' "$csv" | head -1) + if [ -z "$malformed" ]; then + ok "every nondet log row has exactly 7 fields" + else + fail "nondet log row shape" "$malformed" + fi + + # The type column is the one the duplicated value displaced. UNSIGNED is 5 in + # enum NONDET_TYPE, and it has to be readable as the LAST field. + last=$(awk -F';' 'NR==1{print $7}' "$csv") + if [ "$last" = "5" ]; then + ok "the type column survives as the last field (UNSIGNED=5)" + else + fail "type column" "last field is '$last', expected 5" + fi +fi + # The suite must survive cleanGarbage(), which removes the scratch directory. if [ -z "$(find "$WORK" -maxdepth 1 -name '*.map2check' -print -quit)" ]; then ok "scratch directory cleaned and the suite survived"