[CSA] CSA Weekly Report - 130 findings (2026-02-25)

[github-actions[bot]]

Clang Static Analyzer Report

Date: 2026-02-25
Commit: 48de0f8a5e03 (updated compiled workflows)
Build Type: Debug (CMake + Ninja)
Analyzer: scan-build (LLVM 18.1.3)
Report Location: /tmp/csa-report/2026-02-25-001615-405-1/

---

Summary

Metric	Count
Total findings	130
High severity (core.* logic errors)	94
Medium severity (suspicious operations)	9
Low severity (dead code)	27
Files analyzed	885
Build time	~90 minutes

---

Changes Since Last Run (2026-02-24)

Status: ✅ No changes detected

• Total findings: 130 (unchanged)
• Bug distribution: Consistent with previous run
• Top affected files: Unchanged

Interpretation: The recent workflow compilation updates (48de0f8a5e03) did not introduce new static analysis issues.

---

Findings by Category

🔴 High Severity - Core Logic Errors (94 findings)

Bug Type	Count	Severity
Called C++ object pointer is null	55	Critical
Dereference of null pointer	19	Critical
Returning null reference	5	Critical
Division by zero	5	Critical
Uninitialized argument value	3	High
Branch condition evaluates to garbage	3	High
Result of operation is garbage	3	High
Stack address stored into global variable	1	High

🟡 Medium Severity - Suspicious Operations (9 findings)

Bug Type	Count	Notes
Bitwise shift overflow	9	Shift by 32+ bits or negative shift amounts

🟢 Low Severity - Dead Code (27 findings)

Bug Type	Count	Notes
Dead assignment	18	Value written but never read
Dead initialization	6	Variable initialized but never used
Dead increment	3	Increment has no effect

---

Top Affected Files

File	Warnings	Primary Issue Types
src/ast/ast.h	18	Called C++ object null, returning null reference
src/smt/smt_context.h	7	Called C++ object null
src/ast/sls/sls_seq_plugin.cpp	6	Called C++ object null
src/util/util.h	5	Returning null reference
src/math/simplex/bit_matrix.cpp	5	Bitwise shift overflow (genuine issue)
src/math/realclosure/realclosure.cpp	5	Called C++ object null, dead stores
src/ast/euf/euf_mam.cpp	5	Called C++ object null
src/smt/mam.cpp	4	Called C++ object null
src/math/lp/nla_core.cpp	4	Called C++ object null, division by zero
src/util/bit_util.cpp	4	Bitwise shift overflow (genuine issue)

---

High-Priority Findings (Detailed)

1. 🔴 Null Pointer Dereference in Debug Code

File: src/util/debug.cpp:163

warning: Dereference of null pointer (loaded from variable 'x') [core.NullDereference]
    *x = 0;

Impact: Intentional crash trigger in debug assertion handler. Likely a false positive - this is deliberate behavior.

---

2. 🔴 Called C++ Object Null (Multiple locations)

File: src/math/realclosure/realclosure.cpp:3461,3477,3494

warning: Called C++ object pointer is null [core.CallAndMessage]
    return ext->sdt()->qs()[sc->qidx()].size();

Impact: Potential segmentation fault in real closure arithmetic. Likely protected by preconditions not visible to static analyzer.

---

3. 🟡 Bitwise Shift Overflow (GENUINE ISSUE)

File: src/math/simplex/bit_matrix.cpp:128

warning: Left shift by '32' overflows the capacity of 'int' [core.BitwiseShift]
    for (auto & u : v) u |= (1 << (n-1));

Impact: Undefined behavior when n > 32. This appears to be a genuine bug requiring a fix.

Recommendation: Add bounds check or use 1U << (n-1) with validation.

---

4. 🟡 Negative Right Shift (GENUINE ISSUE)

File: src/util/mpff.cpp:164,178

warning: Right operand is negative in right shift [core.BitwiseShift]
    return *s >> exp;
````

**Impact**: **Undefined behavior** with negative exponents. Likely a **genuine bug** requiring validation.

---

### 5. 🔴 Division by Zero (5 locations)

Found in arithmetic modules. Requires **manual code review** to verify runtime guards exist.

---

## Sample Warnings (First 30)

<details>
<summary>Click to expand raw warning excerpts</summary>

````
src/util/debug.cpp:163:16: warning: Dereference of null pointer (loaded from variable 'x') [core.NullDereference]
src/util/bit_util.cpp:222:41: warning: Right shift by '32' overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/bit_util.cpp:286:37: warning: Left shift overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/bit_util.cpp:338:33: warning: Left shift overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/bit_util.cpp:343:33: warning: Left shift overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/mpff.cpp:164:15: warning: Right operand is negative in right shift [core.BitwiseShift]
src/util/mpff.cpp:178:24: warning: Right operand is negative in right shift [core.BitwiseShift]
src/math/simplex/bit_matrix.cpp:128:36: warning: Left shift by '32' overflows the capacity of 'int' [core.BitwiseShift]
src/math/realclosure/realclosure.cpp:3461:37: warning: Called C++ object pointer is null [core.CallAndMessage]
src/math/polynomial/polynomial.cpp:2581:28: warning: Access to field 'm_next' results in a dereference of a null pointer (loaded from field 'm_del_eh') [core.NullDereference]
src/ast/act_cache.cpp:178:22: warning: The left operand of '&' is a garbage value [core.UndefinedBinaryOperatorResult]

---

Analysis Notes

False Positive Likelihood: Moderate to High

Many findings are likely false positives due to:

1. Assertion-protected code: Many warnings occur in SASSERT() macros active only in debug builds
2. Precondition guarantees: Static analyzer cannot infer invariants from surrounding context
3. Tagged pointers: Warnings in act_cache.cpp involve intentional low-bit tagging schemes

Genuine Issues Identified

The following categories likely contain real bugs:

1. ✅ Bitwise shift overflows (9 findings) - Most appear to lack bounds validation
2. ✅ Some null checks - Cases without obvious guards warrant review
3. ⚠️ Division by zero (5 findings) - Requires case-by-case verification

---

Recommendations

🔴 Immediate Actions (Critical)

1. Audit all 5 division-by-zero warnings - Verify runtime guards or add checks
2. Fix bitwise shift overflows in:
   • src/util/bit_util.cpp (4 locations)
   • src/math/simplex/bit_matrix.cpp (5 locations)
3. Review negative shift operations in src/util/mpff.cpp

🟡 Short-term Actions

1. Add shift amount validation in bit manipulation utilities
2. Review null pointer dereferences outside assertion contexts
3. Clean up dead stores (may indicate incomplete refactoring)

🟢 Long-term Actions

1. Integrate scan-build into CI with baseline filtering to catch regressions
2. Add __attribute__((nonnull)) or similar annotations to help analyzer
3. Enable additional checkers: alpha.*, security.*, nullability.*
4. Create suppression list for known false positives

---

How to Reproduce Locally

# Install clang-tools
sudo apt-get install clang clang-tools cmake ninja-build

# Configure with scan-build
mkdir build && cd build
/usr/lib/llvm-18/bin/scan-build cmake -DCMAKE_BUILD_TYPE=Debug -G Ninja ../

# Build with static analysis (takes ~90 minutes)
/usr/lib/llvm-18/bin/scan-build -o /tmp/csa-report --html-title "Z3 CSA Report" ninja

# View results
scan-view /tmp/csa-report/(timestamp)/

---

Notes

• This report was automatically generated by the Z3 CSA Analysis workflow
• False positives are expected - human review required before acting on findings
• HTML reports with detailed traces available at: /tmp/csa-report/2026-02-25-001615-405-1/
• Older CSA discussions are automatically closed per workflow configuration
• No regressions detected compared to previous run (2026-02-24)

Next scheduled run: Automatic weekly trigger or manual workflow dispatch

AI generated by Clang Static Analyzer (CSA) Report

• expires on Mar 4, 2026, 1:42 AM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-04T01:42:46.828Z.

Closed by Workflow