Repository navigation
SMT2 backend with FPA but without datatypes emits ill-typed SMT-LIB for arrays of structs with a float member #9372
Description
Found by comparing the semantics described in the SMT-LIB FloatingPoint theory with how CBMC implements them. An AI agent found this bug, reproduced it with CBMC 5783f86 and drafted this report. A second agent tried to refute it and searched upstream for duplicates. The methodology is described here.
Related: #9146 / PR #9147 (ill-typed SMT2 for floats in aggregates); the cases below still reproduce on develop 5783f86.
Tested commit: 32441ee (develop).
Reproducer
struct-array.c:
struct S { float f; int i; };
int main(){ struct S a[3]; int k; float x; __CPROVER_assume(k>=0 && k<3);
struct S s = {x, 5};
a[k] = s;
__CPROVER_assert(!(a[k].f == 1.5f), "x");
}cbmc struct-array.c --cprover-smt2
Expected behavior
VERIFICATION FAILED with a counterexample where x == 1.5f. The SAT backend
and --z3 --fpa, which encodes structs as datatypes, both report this:
$ cbmc struct-array.c --z3 --fpa
[main.assertion.1] line 5 x: FAILURE
VERIFICATION FAILED
Actual behavior
$ cbmc struct-array.c --cprover-smt2
SMT2 solver returned error message:
'line 137: FloatingPoint equality takes FloatingPoint operands'
[main.assertion.1] line 5 x: ERROR
VERIFICATION ERROR
The same configuration, FP theory without datatypes, is the default for
--bitwuzla. I did not run Bitwuzla.
Cause
When datatypes are not available, structs are flattened to bit-vectors. The
flattening uses concat directly over FP-sorted members, and member reads use
(_ extract ...) on the flattened value, which is then passed to fp.eq. FP
members need to be converted to and from their IEEE bit pattern during
flattening and unflattening. smt2_convt::flatten2bv and unflatten
(src/solvers/smt2/smt2_conv.cpp, around 5276-5320) have no FPA handling for
non-constant floats.
Probably related to #9102 (open PR adding a bvfromfloat round-trip to
flatten2bv for non-constant floats; it targets unions and may not cover the
struct/array path shown here).
Reproducer files
run.sh
#!/usr/bin/env bash
cd "$(dirname "$0")" || exit 2
# cbmc-smt2-fpa-struct-float-array-ill-typed: usage CBMC=<cbmc> [SMT2SOLVER=<smt2_solver>] [HARNESS=<prebuilt harness>] ./run.sh
CBMC=${CBMC:-cbmc}
SMT2SOLVER=${SMT2SOLVER:-}
command -v "$CBMC" >/dev/null 2>&1 || [ -x "$CBMC" ] || { echo "harness error: cbmc not found: $CBMC"; exit 2; }
BUG=0; OK=0; SKIP=0; ERR=0
# cbmc_case NAME EXPECTED_RC FILE ARGS... (spec-correct: exit EXPECTED_RC, no crash/solver error)
cbmc_case() {
local name=$1 want=$2 file=$3; shift 3
local out rc msg
out=$(timeout 120 "$CBMC" "$file" "$@" 2>&1); rc=$?
msg=$(printf "%s\n" "$out" | grep -m1 -A1 -E "INVARIANT|Exception|Reason:|SMT2 solver returned error|VERIFICATION ERROR|invalid|incompatible|error|Condition:" | tr -s "[:space:]" " ")
local res; res=$(printf "%s\n" "$out" | grep -m1 -E "^VERIFICATION (SUCCESSFUL|FAILED|ERROR)")
if [ $rc -eq 124 ]; then echo "case $name: rc=124 TIMEOUT -> harness error"; ERR=$((ERR+1))
elif [ $rc -eq "$want" ] && ! printf "%s\n" "$out" | grep -qE "INVARIANT|Exception|VERIFICATION ERROR|SMT2 solver returned error"; then
echo "case $name: rc=$rc $res -> OK"; OK=$((OK+1))
else
echo "case $name: rc=$rc ${res:-no verdict} [${msg}] (want rc=$want) -> BUG"; BUG=$((BUG+1))
fi
}
skip_case() { echo "case $1: SKIP ($2)"; SKIP=$((SKIP+1)); }
finish() {
echo "summary: ok=$OK bug=$BUG skip=$SKIP harness_error=$ERR"
[ $ERR -gt 0 ] && exit 2
[ $BUG -gt 0 ] && exit 1
exit 0
}
# expected: VERIFICATION FAILED (rc 10), as SAT backend and --z3 --fpa
cbmc_case sat-reference 10 struct-array.c
cbmc_case z3-fpa-reference 10 struct-array.c --z3 --fpa
cbmc_case cprover-smt2 10 struct-array.c --cprover-smt2
if command -v bitwuzla >/dev/null 2>&1; then cbmc_case bitwuzla 10 struct-array.c --bitwuzla
else skip_case bitwuzla "bitwuzla not installed (draft did not run it either)"; fi
finishstruct-array.c
struct S { float f; int i; };
int main(){ struct S a[3]; int k; float x; __CPROVER_assume(k>=0 && k<3);
struct S s = {x, 5};
a[k] = s;
__CPROVER_assert(!(a[k].f == 1.5f), "x");
}If this is intended behaviour or a duplicate, feel free to close it, and I'll use that as feedback to improve future reports. For questions, or to have this re-checked on a newer version of CBMC, mention @JeroenRobben or email jeroen@robben.io.
Activity