a598e9dd96
- Concurrency: 7 Infer checkers, 0 in fold — biggest gap - C++ lifetime: 4 Infer, 0 fold (dangling refs, ownership) - Resource mgmt: file/socket leak missing from fold's memory-leak - Performance: vector reallocation, loop invariants
77 lines
3.1 KiB
Markdown
77 lines
3.1 KiB
Markdown
# Facebook Infer Checkers vs fold Detectors — Gap Matrix
|
|
|
|
> Generated 2026-05-29. Maps every Infer C/C++ checker to fold's existing detectors.
|
|
|
|
## Coverage Summary
|
|
|
|
Infer has ~30 C/C++ checkers across 6 categories. fold covers 9 of these domains.
|
|
|
|
| Category | Infer Checkers | fold Has | fold Missing |
|
|
|----------|---------------|----------|-------------|
|
|
| Memory safety | 5 | 5 | 0 |
|
|
| Resource management | 4 | 3 | 1 |
|
|
| Concurrency | 7 | 0 | 7 |
|
|
| Performance | 5 | 1 | 4 |
|
|
| C++ lifetime | 4 | 0 | 4 |
|
|
| Taint / security | 3 | 1 | 2 |
|
|
| **Total** | **~30** | **10** | **18** |
|
|
|
|
## Key Gaps
|
|
|
|
### Concurrency (7 Infer checkers, 0 in fold)
|
|
|
|
| Infer Checker | What it finds |
|
|
|---------------|--------------|
|
|
| RacerD | Data races on Java/ObjC fields (some C++ support) |
|
|
| Starvation | Deadlocks from lock ordering |
|
|
| Thread-safety | Unsafe publication, missing synchronization |
|
|
| Lock consistency | Lock/unlock imbalance |
|
|
| GuardedBy | Missing lock acquisition before accessing guarded field |
|
|
|
|
**fold opportunity**: Syntactic lock/unlock imbalance detection (low effort). Full RacerD equivalent requires thread interleaving model (high effort, beyond current scope).
|
|
|
|
### Resource Management (1 gap)
|
|
|
|
| Infer Checker | fold Equivalent |
|
|
|---------------|----------------|
|
|
| Resource leak (files) | `memory-leak` (heap only) — missing file/socket leak |
|
|
| Memory leak | `memory-leak` ✅ |
|
|
|
|
### C++ Lifetime (4 Infer checkers, 0 in fold)
|
|
|
|
| Infer Checker | What it finds | fold Feasibility |
|
|
|---------------|--------------|-----------------|
|
|
| Dangling pointer | Use-after-free | `use-after-free` ✅ (observer-based) |
|
|
| Dangling reference | Reference to temporary | NEW — syntactic check |
|
|
| Ownership | shared_ptr cycles | Beyond scope |
|
|
| Smart pointer | unique_ptr/shared_ptr misuse | NEW — syntactic check |
|
|
|
|
### Performance (5 Infer checkers, 1 in fold)
|
|
|
|
| Infer Checker | fold Equivalent |
|
|
|---------------|----------------|
|
|
| Unnecessary copy | `redundant-store` (partial) |
|
|
| Expensive loop invariant | NEW — Z3 could prove expression is loop-invariant |
|
|
| Vector reallocation | NEW — detect reserve() opportunities |
|
|
| Boxed primitive | N/A (Java-specific) |
|
|
|
|
## What fold Does Better Than Infer
|
|
|
|
| Capability | fold | Infer |
|
|
|-----------|------|-------|
|
|
| Z3-proved findings | Yes (UNSAT proofs) | No (biabduction, heuristic) |
|
|
| Semantic equivalence | Yes (Type-4 clones) | No |
|
|
| Binary scanning | Yes | No |
|
|
| Dead branch detection | Yes | Partial (pulse dead store) |
|
|
| Cross-language (Rust/Swift) | Yes | No |
|
|
| Observer architecture | Yes (pluggable detectors) | No (checker registration) |
|
|
|
|
## Recommended Additions
|
|
|
|
| Priority | Detector | Approach | Effort |
|
|
|----------|----------|----------|--------|
|
|
| 1 | File/socket leak | Extend memory-leak to track non-heap resources | M |
|
|
| 2 | Dangling reference | Syntactic: detect references to temporaries | S |
|
|
| 3 | Lock imbalance | Syntactic: count lock/unlock per function | S |
|
|
| 4 | Vector reallocation | Syntactic: detect push_back in loop without reserve | S |
|
|
| 5 | Expensive loop invariant | Z3: prove expression is loop-invariant | L |
|