fix(int-overflow): render witnesses in the source type's width and sign

Problem: symbols are 64-bit bitvectors whose low bits carry the source
value, but int-overflow witnesses printed the whole bitvector. For a
32-bit `int a` the report showed a=2147483648 or a=-9223372034707292160,
which are not values of `a` and would make bad fuzz seeds
(tests/fixtures/clones/exact.cpp).

Fix: detect::sourceIntTypesOf() maps the function's integer parameters
and locals to their width and signedness (a name declared with two types
is left out). collectModelBindings() takes that map and prints each bound
symbol truncated to its source width with its signedness
(formatSourceIntValue). int-overflow passes the map for the current
function; other detectors are unchanged.

Test: test_int_overflow "[witness]": every binding for an `int` overflow
lies in int range, and formatSourceIntValue covers sign/width cases.
exact.cpp before: a=2147483648, a=3221225471. After: a=-2147483648,
a=-1073741825, the int values that actually overflow.

include/fold/detect/z3_model_support.hpp

@@ -14,6 +14,22 @@
 
 namespace fold::detect {
 
+// Source type of an integer variable, for rendering its model value. Symbols
+// are 64-bit bitvectors whose low `width` bits carry the source value.
+struct SourceIntType {
+    unsigned width = 0;
+    bool is_signed = false;
+};
+using SourceIntTypes = std::map<std::string, SourceIntType>;
+
+// Integer-typed parameters and locals of `fn`, by name. A name declared with
+// two different integer types is left out rather than guessed.
+[[nodiscard]] SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn,
+                                              const clang::ASTContext& ctx);
+
+// `raw` truncated to the source width and printed with its signedness.
+[[nodiscard]] std::string formatSourceIntValue(uint64_t raw, SourceIntType type);
+
 inline std::string fallbackExprLabel(const clang::Expr* expr, const char* fallback) {
     if (!expr)
         return fallback;
@@ -84,7 +100,8 @@ inline void collectLeafSymbols(const z3::expr& expr, std::map<std::string, z3::e
 }
 
 inline std::vector<std::pair<std::string, std::string>>
-collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned) {
+collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned,
+                     const SourceIntTypes* types = nullptr) {
     std::map<std::string, z3::expr> symbols;
     std::unordered_set<unsigned> seen;
     collectLeafSymbols(expr, symbols, seen);
@@ -92,6 +109,14 @@ collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSi
     std::vector<std::pair<std::string, std::string>> bindings;
     bindings.reserve(symbols.size());
     for (const auto& [name, symbol] : symbols) {
+        uint64_t raw = 0;
+        const auto type = types != nullptr ? types->find(name) : SourceIntTypes::const_iterator{};
+        z3::expr value = model.eval(symbol, true);
+        if (types != nullptr && type != types->end() && value.is_bv() &&
+            value.is_numeral_u64(raw)) {
+            bindings.emplace_back(name, formatSourceIntValue(raw, type->second));
+            continue;
+        }
         bindings.emplace_back(name, formatModelValue(model, symbol, preferSigned));
     }
     return bindings;

src/detect/int_overflow.cpp

@@ -610,13 +610,14 @@ class IntOverflowObserver : public SafetyObserver {
         return fold::mix64(seed, sourceBitWidth);
     }
 
-    static std::pair<std::string, std::vector<std::pair<std::string, std::string>>>
+    std::pair<std::string, std::vector<std::pair<std::string, std::string>>>
     buildCounterexample(const z3::model& model, const z3::expr& lhs, const z3::expr& rhs,
                         const clang::Expr* lhsExpr, const clang::Expr* rhsExpr,
-                        bool isSourceSigned) {
-        auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned);
-        detect::appendUniqueBindings(bindings,
-                                     detect::collectModelBindings(model, rhs, isSourceSigned));
+                        bool isSourceSigned) const {
+        const auto types = detect::sourceIntTypesOf(current_fn_, ctx_); // source width/sign
+        auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned, &types);
+        detect::appendUniqueBindings(
+            bindings, detect::collectModelBindings(model, rhs, isSourceSigned, &types));
         std::string text;
         if (!bindings.empty()) {
             text = " (e.g., when " + detect::joinBindings(bindings) + ")";

src/detect/meson.build

@@ -6,6 +6,7 @@ fold_core_sources += files(
   'hardcoded_credential.cpp',
   'format_string.cpp',
   'summary_store.cpp',
+  'z3_model_support.cpp',
   'incremental_cache.cpp',
   'function_enumeration.cpp',
   'function_flow.cpp',

src/detect/z3_model_support.cpp

@@ -0,0 +1,53 @@
+#include "fold/detect/z3_model_support.hpp"
+
+#include <clang/AST/ASTContext.h>
+#include <clang/AST/Decl.h>
+#include <clang/AST/RecursiveASTVisitor.h>
+
+#include <functional>
+#include <set>
+
+namespace fold::detect {
+
+SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, const clang::ASTContext& ctx) {
+    SourceIntTypes types;
+    if (fn == nullptr)
+        return types;
+    std::set<std::string> ambiguous;
+    auto add = [&](const clang::VarDecl* vd) {
+        const clang::QualType type = vd->getType().getCanonicalType();
+        if (!type->isIntegerType() || type->isDependentType() || vd->getName().empty())
+            return;
+        const SourceIntType info{static_cast<unsigned>(ctx.getTypeSize(type)),
+                                 type->isSignedIntegerType()};
+        const std::string name = vd->getNameAsString();
+        const auto [it, inserted] = types.emplace(name, info);
+        if (!inserted && (it->second.width != info.width || it->second.is_signed != info.is_signed))
+            ambiguous.insert(name);
+    };
+    for (const auto* param : fn->parameters())
+        add(param);
+    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
+        std::function<void(const clang::VarDecl*)> add;
+        bool VisitVarDecl(clang::VarDecl* vd) {
+            add(vd);
+            return true;
+        }
+    } visitor;
+    visitor.add = add;
+    if (fn->hasBody())
+        visitor.TraverseStmt(fn->getBody());
+    for (const auto& name : ambiguous)
+        types.erase(name);
+    return types;
+}
+
+std::string formatSourceIntValue(uint64_t raw, SourceIntType type) {
+    if (type.width == 0 || type.width >= 64)
+        return type.is_signed ? std::to_string(static_cast<int64_t>(raw)) : std::to_string(raw);
+    const uint64_t truncated = raw & ((uint64_t{1} << type.width) - 1);
+    return type.is_signed ? formatSignedBitVector(truncated, type.width)
+                          : std::to_string(truncated);
+}
+
+} // namespace fold::detect

tests/unit/test_int_overflow.cpp

@@ -9,6 +9,7 @@
 
 #include "fold/detect/cross_tu_cache.hpp"
 #include "fold/detect/int_overflow.hpp"
+#include "fold/detect/z3_model_support.hpp"
 #include "fold/report/finding.hpp"
 #include "fold/symbolic/budget.hpp"
 
@@ -669,3 +670,30 @@ TEST_CASE("int-overflow: CFString size output contract proves length-1 safe",
     std::fprintf(stderr, "CFSTRING-POS findings=%zu\n", findings.size());
     REQUIRE(findings.empty());
 }
+
+TEST_CASE("int-overflow: witnesses use the source type's width and signedness",
+          "[int_overflow][witness]") {
+    // Symbols are 64-bit; only the low 32 bits carry an `int`. Witnesses were
+    // printed from the whole bitvector, e.g. a=2147483648 or
+    // a=-9223372034707292160 for `int a`.
+    auto r = run("int sum(int a, int b) { int x = a + b; x += a; return x; }\n");
+    REQUIRE_FALSE(r.findings.empty());
+    for (const auto& f : r.findings) {
+        for (const auto& [name, value] : f.evidence.counterexample) {
+            const long long v = std::stoll(value);
+            CHECK(v >= -2147483648LL);
+            CHECK(v <= 2147483647LL);
+        }
+    }
+}
+
+TEST_CASE("formatSourceIntValue truncates and signs", "[int_overflow][witness]") {
+    using fold::detect::formatSourceIntValue;
+    CHECK(formatSourceIntValue(0x80000000ULL, {32, true}) == "-2147483648");
+    CHECK(formatSourceIntValue(0x8000000080000000ULL, {32, true}) == "-2147483648");
+    CHECK(formatSourceIntValue(0xBFFFFFFFULL, {32, true}) == "-1073741825");
+    CHECK(formatSourceIntValue(0x1FFFFFFFFULL, {32, false}) == "4294967295");
+    CHECK(formatSourceIntValue(7, {32, true}) == "7");
+    CHECK(formatSourceIntValue(0xFFFFFFFFFFFFFFFFULL, {64, true}) == "-1");
+    CHECK(formatSourceIntValue(0xFFULL, {8, true}) == "-1");
+}