Spaces:

AProver
/

aprover

Running

aprover / bmc_agent /fp_pattern_detector.py

Humaid Alqasimi

AProver Space — built from main@d852c29

4f0bd4e 4 months ago

13.2 kB

"""
False-positive pattern detection (Phase 4 of autonomous mode).
Inspect a confirmed bug finding (CEx state + classification + realism
verdict) and check whether it matches a known FP pattern. Returns a
typed :class:`FpPattern` plus evidence the autonomous outer loop can use
to inject a session-local skepticism hint into the next round's realism
prompt.
The patterns are derived from the methodology insight in
``findings/methodology_insight_2026-05-22.md`` and the 12-bug
libarchive_rb.c result from the 2026-05-23 sweep (all confirmed but
all caller-contract slips):
* :data:`FpPattern.UNINIT_VTABLE` — the CEx assigns NULL to a function
  pointer that's a member of a ``*->ops->*`` / ``*->vtable->*``
  structure. In practice the container is initialized by a separate
  ``foo_init(handle, ops)`` call that the lite-mode harness skipped.
* :data:`FpPattern.UNINIT_CONTAINER` — every field of the param's
  struct backing is nondet/default and the witness depends on those
  fields being a particular value (NULL/zero). Strong signal of a
  container that's supposed to be initialized by the caller before
  use.
* :data:`FpPattern.UNREACHABLE_BRANCH` — the witness state requires
  a sentinel value (e.g. ``-1`` / ``MAX_INT``) that the caller-site
  guard explicitly rejects.
This module is *pure detection*. It returns the pattern + evidence;
the autonomous loop in cli.py decides what hint to inject.
"""

from __future__ import annotations

import json
import re
from dataclasses import dataclass, field
from enum import Enum
from pathlib import Path
from typing import Optional


class FpPattern(str, Enum):
    UNINIT_VTABLE = "uninit_vtable"
    """CEx requires a NULL function pointer to be invoked. Almost
    always the caller-contract slip where the container's ops/vtable
    field is unset because the harness didn't simulate the init call."""

    UNINIT_CONTAINER = "uninit_container"
    """CEx witness shows every container field at its default nondet
    value (NULL / 0). Likely a forgotten initialization on the harness
    side. Weaker signal than UNINIT_VTABLE — many real bugs also have
    nondet fields, but the *combination* of all-nondet + system-entry
    confidence flags this for follow-up."""

    UNREACHABLE_BRANCH = "unreachable_branch"
    """CEx requires a sentinel input value (often ``-1``, ``UINT_MAX``,
    very large size) that callers explicitly guard against. Pattern
    detection: combination of integer-overflow CEx + system-entry
    caller chain through a known length-validating wrapper."""

    UNRELATED_PAIRED_POINTERS = "unrelated_paired_pointers"
    """CEx has two parameters whose names suggest a pointer pair
    (``start``/``end``, ``begin``/``end``, ``first``/``last``,
    ``src``/``dst``, ``head``/``tail``) but their backing arrays in
    the witness are independent allocations. Every real caller passes
    pointers into the SAME buffer (caller-contract), so the unrelated-
    backing CEx is unreachable from any public API. Observed on
    libarchive's ``ismode(const char *start, const char *end, …)``
    family in the 2026-05-23 archive_acl calibration."""

    NO_PATTERN = "no_pattern"
    """No known FP pattern matched — finding looks like a candidate
    real bug or an unclassified FP class."""


@dataclass
class FpEvidence:
    """The detector's verdict for one bug finding."""

    pattern: FpPattern
    confidence: float
    """0.0 - 1.0 — heuristic certainty that this is the named FP
    pattern. Used by the realism-hint injector to weigh hints by
    frequency × confidence."""

    cited_fields: list[str] = field(default_factory=list)
    """The witness-state field names that triggered the match.
    Example: ``['compare_key', 'compare_nodes']`` for an UNINIT_VTABLE
    on archive_rb."""

    cited_functions: list[str] = field(default_factory=list)
    """The call-chain functions implicated in the FP. The hint
    injector uses these to phrase the skepticism rule concretely
    ("for callers of ``__archive_rb_tree_*``, the tree object is
    initialized via ``__archive_rb_tree_init`` first.")."""


# ---------------------------------------------------------------------------
# Witness-state walker
# ---------------------------------------------------------------------------


_FN_POINTER_PAT = re.compile(
    # CBMC formats function-pointer variables as ``signed int (*)(...) name = NULL``
    # in the variable_assignments dict. The KEY is the variable name; the
    # VALUE is the function-pointer type string.
    r'^(?:const\s+)?(?:un)?signed\s+\w+\s*\(\s*\*\s*\)\s*\(.*\)$'
)


def _is_null_function_pointer(field_name: str, value: str) -> bool:
    """True if ``value`` represents a NULL function pointer.
    CBMC writes function-pointer NULLs in several forms — match any of:
      * ``((signed int (*)(struct X *, const void *))NULL)``
      * ``NULL``  (in the context of a known fn-pointer field name)
      * ``((<sig>)NULL)`` for any sig
    """
    v = value.strip()
    if v == "NULL":
        # Only treat bare NULL as a fn-pointer if the field name strongly
        # suggests it (compare_*, *_fn, *_cb, *_callback, *->ops->*).
        return _field_name_suggests_function_pointer(field_name)
    # Strip outer parens.
    if v.startswith("((") and v.endswith(")NULL)"):
        inside = v[2:-len(")NULL)")]
        # Detect a function-pointer type signature.
        if "(" in inside and "*" in inside:
            return True
    return False


def _field_name_suggests_function_pointer(name: str) -> bool:
    """Heuristic: a field name strongly suggesting a function-pointer
    callback. Matches camelCase and snake_case forms.
    """
    name_l = name.lower()
    return (
        name_l.startswith("compare_") or name_l.endswith("_fn") or
        name_l.endswith("_cb") or name_l.endswith("_callback") or
        name_l in {"ctor", "dtor", "init_fn", "hook", "free_fn",
                   "compare", "compare_nodes", "compare_key",
                   "alloc_fn", "release_fn"} or
        "->ops->" in name_l or "->vtable->" in name_l
    )


# ---------------------------------------------------------------------------
# Public API
# ---------------------------------------------------------------------------


def detect_pattern(
    bug_report: dict,
    classification: Optional[dict] = None,
) -> FpEvidence:
    """Inspect a bug-report dict (the on-disk ``bug_report.json``) and
    classify the likely FP pattern.
    Pure function. Optionally accepts a ``classification`` dict (the
    ``classification.json`` companion) for the witness state when the
    bug report doesn't carry it inline.
    """
    # The bug_report.json may be stored at two nesting levels:
    #   (a) outer ``{saved_at, report: {function_name, counterexample, …}}``
    #   (b) inner ``{function_name, counterexample, …}`` directly.
    # Accept either.
    if "report" in bug_report and isinstance(bug_report["report"], dict):
        report = bug_report["report"]
    else:
        report = bug_report

    # Extract the variable_assignments dict from wherever it lives.
    cex: dict = {}
    state = report.get("state") or {}
    if isinstance(state, dict) and state:
        cex = state
    if not cex:
        ce = report.get("counterexample") or {}
        if isinstance(ce, dict):
            cex = ce.get("variable_assignments") or {}
    if not cex and classification:
        ce_outer = classification.get("classification") or {}
        ce_cls = ce_outer.get("counterexample") or {}
        cex = ce_cls.get("variable_assignments") or {}

    call_chain: list[str] = report.get("call_chain") or []
    if not call_chain and classification:
        cls_inner = classification.get("classification") or {}
        call_chain = cls_inner.get("caller_path") or []

    # Pattern 1: uninit vtable — any field name + value that looks
    # like a NULL function pointer.
    null_fn_fields = [
        k for k, v in cex.items()
        if isinstance(v, str) and _is_null_function_pointer(k, v)
    ]
    if null_fn_fields:
        return FpEvidence(
            pattern=FpPattern.UNINIT_VTABLE,
            confidence=0.9 if len(null_fn_fields) >= 2 else 0.7,
            cited_fields=null_fn_fields,
            cited_functions=call_chain,
        )

    # Pattern 2: uninit container — all non-CPROVER fields nondet/NULL.
    user_fields = {
        k: v for k, v in cex.items()
        if isinstance(v, str)
        and not k.startswith("__CPROVER")
        and not k.startswith("return_value_")
        and not k.startswith("_") and not k.endswith("_buf")
    }
    if user_fields and len(user_fields) >= 3:
        nondet_count = sum(
            1 for v in user_fields.values()
            if v.strip() in ("NULL", "0", "0u", "0ul", "0l")
            or "{'name': 'unknown'}" in v
        )
        if nondet_count >= len(user_fields) * 0.8:
            return FpEvidence(
                pattern=FpPattern.UNINIT_CONTAINER,
                confidence=0.6,
                cited_fields=list(user_fields.keys())[:6],
                cited_functions=call_chain,
            )

    # Pattern 3: unrelated paired pointers.
    paired = _detect_paired_pointers(cex)
    if paired:
        return FpEvidence(
            pattern=FpPattern.UNRELATED_PAIRED_POINTERS,
            confidence=0.7,
            cited_fields=paired,
            cited_functions=call_chain,
        )

    return FpEvidence(
        pattern=FpPattern.NO_PATTERN,
        confidence=0.0,
        cited_fields=[],
        cited_functions=call_chain,
    )


# Pairs of parameter names that the harness almost certainly mis-models
# when given independent nondet backings. Each entry: (a, b) such that
# real callers always pass pointers into the SAME buffer.
_PAIRED_POINTER_NAMES: frozenset[tuple[str, str]] = frozenset({
    ("start", "end"),
    ("begin", "end"),
    ("first", "last"),
    ("src", "dst"),
    ("source", "destination"),
    ("head", "tail"),
    ("low", "high"),
    ("from", "to"),
})


def _detect_paired_pointers(cex: dict) -> list[str]:
    """Look for canonical paired-pointer parameter names where the
    witness state shows independent backings (``_<a>_buf`` and
    ``_<b>_buf`` distinct arrays). Returns the field-name list if a
    pair is detected, empty list otherwise.
    Pattern fingerprint in CBMC's variable_assignments:
      ``start = _start_buf!0@1``
      ``end   = _end_buf!0@1``  (different backing → unrelated)
    Real callers would have:
      ``start = _shared_buf!0@1``
      ``end   = _shared_buf!N@1`` (offset into same backing).
    """
    if not cex:
        return []
    for a, b in _PAIRED_POINTER_NAMES:
        if a in cex and b in cex:
            va = str(cex[a])
            vb = str(cex[b])
            if "!" not in va or "!" not in vb:
                continue
            # Pointer base = everything before the ``!``.
            base_a = va.split("!", 1)[0].strip()
            base_b = vb.split("!", 1)[0].strip()
            if base_a and base_b and base_a != base_b:
                return [a, b]
    return []


def detect_pattern_from_paths(
    bug_report_path: str | Path,
    classification_path: Optional[str | Path] = None,
) -> FpEvidence:
    """Convenience: load both JSON files and detect."""
    with open(bug_report_path) as f:
        bug = json.load(f)
    classification = None
    if classification_path:
        try:
            with open(classification_path) as f:
                classification = json.load(f)
        except FileNotFoundError:
            pass
    return detect_pattern(bug, classification)


def scan_artifact_tree(artifact_root: str | Path) -> dict[FpPattern, int]:
    """Walk every ``bug_report.json`` under *artifact_root* and tally
    detected FP patterns. Used by the autonomous outer loop to decide
    which hints are worth injecting next round.
    """
    root = Path(artifact_root)
    counts: dict[FpPattern, int] = {p: 0 for p in FpPattern}
    examples: dict[FpPattern, list[tuple[str, list[str]]]] = {p: [] for p in FpPattern}
    for br in root.rglob("bug_report.json"):
        try:
            with br.open() as f:
                bug = json.load(f)
            if not bug:
                continue
            # Outer-or-inner shape.
            top = bug.get("report") if isinstance(bug.get("report"), dict) else bug
            if not (top.get("function_name") or top.get("violated_property")):
                continue
            cls_path = br.parent / "classification.json"
            classification = None
            if cls_path.exists():
                try:
                    with cls_path.open() as f:
                        classification = json.load(f)
                except Exception:
                    classification = None
            ev = detect_pattern(bug, classification)
            counts[ev.pattern] += 1
            fn = (top.get("function_name") or br.parent.name)
            if len(examples[ev.pattern]) < 5:
                examples[ev.pattern].append((fn, ev.cited_fields))
        except Exception:
            continue
    return {"counts": counts, "examples": examples}

	"""
	False-positive pattern detection (Phase 4 of autonomous mode).

	Inspect a confirmed bug finding (CEx state + classification + realism
	verdict) and check whether it matches a known FP pattern. Returns a
	typed :class:`FpPattern` plus evidence the autonomous outer loop can use
	to inject a session-local skepticism hint into the next round's realism
	prompt.

	The patterns are derived from the methodology insight in
	``findings/methodology_insight_2026-05-22.md`` and the 12-bug
	libarchive_rb.c result from the 2026-05-23 sweep (all confirmed but
	all caller-contract slips):

	* :data:`FpPattern.UNINIT_VTABLE` — the CEx assigns NULL to a function
	pointer that's a member of a ``->ops->`` / ``->vtable->``
	structure. In practice the container is initialized by a separate
	``foo_init(handle, ops)`` call that the lite-mode harness skipped.
	* :data:`FpPattern.UNINIT_CONTAINER` — every field of the param's
	struct backing is nondet/default and the witness depends on those
	fields being a particular value (NULL/zero). Strong signal of a
	container that's supposed to be initialized by the caller before
	use.
	* :data:`FpPattern.UNREACHABLE_BRANCH` — the witness state requires
	a sentinel value (e.g. ``-1`` / ``MAX_INT``) that the caller-site
	guard explicitly rejects.

	This module is pure detection. It returns the pattern + evidence;
	the autonomous loop in cli.py decides what hint to inject.
	"""

	from __future__ import annotations

	import json
	import re
	from dataclasses import dataclass, field
	from enum import Enum
	from pathlib import Path
	from typing import Optional


	class FpPattern(str, Enum):
	UNINIT_VTABLE = "uninit_vtable"
	"""CEx requires a NULL function pointer to be invoked. Almost
	always the caller-contract slip where the container's ops/vtable
	field is unset because the harness didn't simulate the init call."""

	UNINIT_CONTAINER = "uninit_container"
	"""CEx witness shows every container field at its default nondet
	value (NULL / 0). Likely a forgotten initialization on the harness
	side. Weaker signal than UNINIT_VTABLE — many real bugs also have
	nondet fields, but the combination of all-nondet + system-entry
	confidence flags this for follow-up."""

	UNREACHABLE_BRANCH = "unreachable_branch"
	"""CEx requires a sentinel input value (often ``-1``, ``UINT_MAX``,
	very large size) that callers explicitly guard against. Pattern
	detection: combination of integer-overflow CEx + system-entry
	caller chain through a known length-validating wrapper."""

	UNRELATED_PAIRED_POINTERS = "unrelated_paired_pointers"
	"""CEx has two parameters whose names suggest a pointer pair
	(``start``/``end``, ``begin``/``end``, ``first``/``last``,
	``src``/``dst``, ``head``/``tail``) but their backing arrays in
	the witness are independent allocations. Every real caller passes
	pointers into the SAME buffer (caller-contract), so the unrelated-
	backing CEx is unreachable from any public API. Observed on
	libarchive's ``ismode(const char start, const char end, …)``
	family in the 2026-05-23 archive_acl calibration."""

	NO_PATTERN = "no_pattern"
	"""No known FP pattern matched — finding looks like a candidate
	real bug or an unclassified FP class."""


	@dataclass
	class FpEvidence:
	"""The detector's verdict for one bug finding."""

	pattern: FpPattern
	confidence: float
	"""0.0 - 1.0 — heuristic certainty that this is the named FP
	pattern. Used by the realism-hint injector to weigh hints by
	frequency × confidence."""

	cited_fields: list[str] = field(default_factory=list)
	"""The witness-state field names that triggered the match.
	Example: ``['compare_key', 'compare_nodes']`` for an UNINIT_VTABLE
	on archive_rb."""

	cited_functions: list[str] = field(default_factory=list)
	"""The call-chain functions implicated in the FP. The hint
	injector uses these to phrase the skepticism rule concretely
	("for callers of ``__archive_rb_tree_*``, the tree object is
	initialized via ``__archive_rb_tree_init`` first.")."""


	# ---------------------------------------------------------------------------
	# Witness-state walker
	# ---------------------------------------------------------------------------


	_FN_POINTER_PAT = re.compile(
	# CBMC formats function-pointer variables as ``signed int (*)(...) name = NULL``
	# in the variable_assignments dict. The KEY is the variable name; the
	# VALUE is the function-pointer type string.
	r'^(?:const\s+)?(?:un)?signed\s+\w+\s\(\s\\s\)\s\(.\)$'
	)


	def _is_null_function_pointer(field_name: str, value: str) -> bool:
	"""True if ``value`` represents a NULL function pointer.

	CBMC writes function-pointer NULLs in several forms — match any of:
	* ``((signed int ()(struct X , const void *))NULL)``
	* ``NULL`` (in the context of a known fn-pointer field name)
	* ``((<sig>)NULL)`` for any sig
	"""
	v = value.strip()
	if v == "NULL":
	# Only treat bare NULL as a fn-pointer if the field name strongly
	# suggests it (compare_, _fn, _cb, _callback, ->ops->).
	return _field_name_suggests_function_pointer(field_name)
	# Strip outer parens.
	if v.startswith("((") and v.endswith(")NULL)"):
	inside = v[2:-len(")NULL)")]
	# Detect a function-pointer type signature.
	if "(" in inside and "*" in inside:
	return True
	return False


	def _field_name_suggests_function_pointer(name: str) -> bool:
	"""Heuristic: a field name strongly suggesting a function-pointer
	callback. Matches camelCase and snake_case forms.
	"""
	name_l = name.lower()
	return (
	name_l.startswith("compare_") or name_l.endswith("_fn") or
	name_l.endswith("_cb") or name_l.endswith("_callback") or
	name_l in {"ctor", "dtor", "init_fn", "hook", "free_fn",
	"compare", "compare_nodes", "compare_key",
	"alloc_fn", "release_fn"} or
	"->ops->" in name_l or "->vtable->" in name_l
	)


	# ---------------------------------------------------------------------------
	# Public API
	# ---------------------------------------------------------------------------


	def detect_pattern(
	bug_report: dict,
	classification: Optional[dict] = None,
	) -> FpEvidence:
	"""Inspect a bug-report dict (the on-disk ``bug_report.json``) and
	classify the likely FP pattern.

	Pure function. Optionally accepts a ``classification`` dict (the
	``classification.json`` companion) for the witness state when the
	bug report doesn't carry it inline.
	"""
	# The bug_report.json may be stored at two nesting levels:
	# (a) outer ``{saved_at, report: {function_name, counterexample, …}}``
	# (b) inner ``{function_name, counterexample, …}`` directly.
	# Accept either.
	if "report" in bug_report and isinstance(bug_report["report"], dict):
	report = bug_report["report"]
	else:
	report = bug_report

	# Extract the variable_assignments dict from wherever it lives.
	cex: dict = {}
	state = report.get("state") or {}
	if isinstance(state, dict) and state:
	cex = state
	if not cex:
	ce = report.get("counterexample") or {}
	if isinstance(ce, dict):
	cex = ce.get("variable_assignments") or {}
	if not cex and classification:
	ce_outer = classification.get("classification") or {}
	ce_cls = ce_outer.get("counterexample") or {}
	cex = ce_cls.get("variable_assignments") or {}

	call_chain: list[str] = report.get("call_chain") or []
	if not call_chain and classification:
	cls_inner = classification.get("classification") or {}
	call_chain = cls_inner.get("caller_path") or []

	# Pattern 1: uninit vtable — any field name + value that looks
	# like a NULL function pointer.
	null_fn_fields = [
	k for k, v in cex.items()
	if isinstance(v, str) and _is_null_function_pointer(k, v)
	]
	if null_fn_fields:
	return FpEvidence(
	pattern=FpPattern.UNINIT_VTABLE,
	confidence=0.9 if len(null_fn_fields) >= 2 else 0.7,
	cited_fields=null_fn_fields,
	cited_functions=call_chain,
	)

	# Pattern 2: uninit container — all non-CPROVER fields nondet/NULL.
	user_fields = {
	k: v for k, v in cex.items()
	if isinstance(v, str)
	and not k.startswith("__CPROVER")
	and not k.startswith("return_value_")
	and not k.startswith("_") and not k.endswith("_buf")
	}
	if user_fields and len(user_fields) >= 3:
	nondet_count = sum(
	1 for v in user_fields.values()
	if v.strip() in ("NULL", "0", "0u", "0ul", "0l")
	or "{'name': 'unknown'}" in v
	)
	if nondet_count >= len(user_fields) * 0.8:
	return FpEvidence(
	pattern=FpPattern.UNINIT_CONTAINER,
	confidence=0.6,
	cited_fields=list(user_fields.keys())[:6],
	cited_functions=call_chain,
	)

	# Pattern 3: unrelated paired pointers.
	paired = _detect_paired_pointers(cex)
	if paired:
	return FpEvidence(
	pattern=FpPattern.UNRELATED_PAIRED_POINTERS,
	confidence=0.7,
	cited_fields=paired,
	cited_functions=call_chain,
	)

	return FpEvidence(
	pattern=FpPattern.NO_PATTERN,
	confidence=0.0,
	cited_fields=[],
	cited_functions=call_chain,
	)


	# Pairs of parameter names that the harness almost certainly mis-models
	# when given independent nondet backings. Each entry: (a, b) such that
	# real callers always pass pointers into the SAME buffer.
	_PAIRED_POINTER_NAMES: frozenset[tuple[str, str]] = frozenset({
	("start", "end"),
	("begin", "end"),
	("first", "last"),
	("src", "dst"),
	("source", "destination"),
	("head", "tail"),
	("low", "high"),
	("from", "to"),
	})


	def _detect_paired_pointers(cex: dict) -> list[str]:
	"""Look for canonical paired-pointer parameter names where the
	witness state shows independent backings (``_<a>_buf`` and
	``_<b>_buf`` distinct arrays). Returns the field-name list if a
	pair is detected, empty list otherwise.

	Pattern fingerprint in CBMC's variable_assignments:
	``start = _start_buf!0@1``
	``end = _end_buf!0@1`` (different backing → unrelated)

	Real callers would have:
	``start = _shared_buf!0@1``
	``end = _shared_buf!N@1`` (offset into same backing).
	"""
	if not cex:
	return []
	for a, b in _PAIRED_POINTER_NAMES:
	if a in cex and b in cex:
	va = str(cex[a])
	vb = str(cex[b])
	if "!" not in va or "!" not in vb:
	continue
	# Pointer base = everything before the ``!``.
	base_a = va.split("!", 1)[0].strip()
	base_b = vb.split("!", 1)[0].strip()
	if base_a and base_b and base_a != base_b:
	return [a, b]
	return []


	def detect_pattern_from_paths(
	bug_report_path: str \| Path,
	classification_path: Optional[str \| Path] = None,
	) -> FpEvidence:
	"""Convenience: load both JSON files and detect."""
	with open(bug_report_path) as f:
	bug = json.load(f)
	classification = None
	if classification_path:
	try:
	with open(classification_path) as f:
	classification = json.load(f)
	except FileNotFoundError:
	pass
	return detect_pattern(bug, classification)


	def scan_artifact_tree(artifact_root: str \| Path) -> dict[FpPattern, int]:
	"""Walk every ``bug_report.json`` under artifact_root and tally
	detected FP patterns. Used by the autonomous outer loop to decide
	which hints are worth injecting next round.
	"""
	root = Path(artifact_root)
	counts: dict[FpPattern, int] = {p: 0 for p in FpPattern}
	examples: dict[FpPattern, list[tuple[str, list[str]]]] = {p: [] for p in FpPattern}
	for br in root.rglob("bug_report.json"):
	try:
	with br.open() as f:
	bug = json.load(f)
	if not bug:
	continue
	# Outer-or-inner shape.
	top = bug.get("report") if isinstance(bug.get("report"), dict) else bug
	if not (top.get("function_name") or top.get("violated_property")):
	continue
	cls_path = br.parent / "classification.json"
	classification = None
	if cls_path.exists():
	try:
	with cls_path.open() as f:
	classification = json.load(f)
	except Exception:
	classification = None
	ev = detect_pattern(bug, classification)
	counts[ev.pattern] += 1
	fn = (top.get("function_name") or br.parent.name)
	if len(examples[ev.pattern]) < 5:
	examples[ev.pattern].append((fn, ev.cited_fields))
	except Exception:
	continue
	return {"counts": counts, "examples": examples}