==============================
MemHint: Neuro-Symbolic Analysis
==============================

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

Usage
-----

.. code-block:: bash

   # 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
-------

.. code-block:: text

   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)