MemHint: Neuro-Symbolic Analysis

Discovers project-specific custom memory management functions by combining LLM semantic understanding with Z3 formal verification.

Usage

# Discover custom allocators
memguard memhint ./src/

# Save to specific file
memguard memhint ./src/ --output hints.json

# Skip Z3 (faster, less precise)
memguard memhint ./src/ --no-z3

# Limit scope
memguard memhint ./src/ --max-functions 200

# Then scan - Infer automatically uses saved summaries
memguard scan /tmp/binary --tools infer
# Log: "MemHint: injecting 6 custom allocators into Infer"

Via GUI: check MemHint checkbox before clicking Run Scan.

How It Works

Phase 1 - Code Extraction: tree-sitter parses every C/C++ file and extracts function metadata. Pointer-type pre-filter reduces candidates by ~50%.

Phase 2 - LLM Classification: Each candidate sent to local Ollama model with function body and callee context. LLM classifies as ALLOCATOR, DEALLOCATOR, or NEITHER.

Phase 3 - Z3 Validation: For each ALLOCATOR, Z3 checks if a feasible CFG path exists where memory is allocated AND returned without being freed. If UNSAT, the summary is rejected as a false positive. Raises LLM’s ~92% precision to ~100%.

Integration: Validated summaries auto-loaded into Infer (--pulse-model-alloc-pattern) and into AI analysis prompts (custom MM context).

Example

Phase 1: 28 extracted → 15 candidates
Phase 2: LLM produced 8 MM summaries
Phase 3: Z3 validated 6, rejected 2
  ✓ parse_request - Allocator (return)
  ✓ format_log    - Allocator (return)
  ✗ free_request  - REJECTED (Z3: no allocation path)
  ✗ handle_and_free - REJECTED (Z3: frees, doesn't allocate)