| """ |
| AMC command-line interface. |
| |
| Usage: |
| uv run amc generate --source examples/simple_driver.c --driver mydriver --output artifacts/ |
| uv run amc check --driver mydriver --function rb_write |
| uv run amc verify --source examples/simple_driver.c --driver mydriver |
| """ |
|
|
| from __future__ import annotations |
|
|
| import argparse |
| import json |
| import re |
| import sys |
| from pathlib import Path |
|
|
|
|
| def _resolve_domain_knowledge(raw: str) -> str: |
| """Return domain knowledge text: read from file if raw is a valid existing path, else use as-is.""" |
| try: |
| p = Path(raw) |
| if p.exists(): |
| return p.read_text(encoding="utf-8") |
| except OSError: |
| pass |
| return raw |
|
|
|
|
| def _apply_model_arg(config: "object", args: argparse.Namespace) -> None: |
| """Override config.llm_model if --model was supplied on the command line.""" |
| model = getattr(args, "model", None) |
| if model: |
| config.llm_model = model |
|
|
|
|
| def _resolve_threat_model_context(value: "str | None") -> str: |
| """Resolve a ``--threat-model-context`` argument to its text. Accepts either |
| a path to a file (read it) or an inline string (used verbatim). Returns "" for |
| a missing/empty value. Keeps the CLI ergonomic: usually a path, occasionally |
| a short inline note. |
| """ |
| if not value: |
| return "" |
| try: |
| from pathlib import Path as _P |
| p = _P(value) |
| if p.is_file(): |
| return p.read_text(encoding="utf-8", errors="replace").strip() |
| except Exception: |
| pass |
| return value.strip() |
|
|
|
|
| def _apply_threat_model_context(config: "object", args: argparse.Namespace) -> None: |
| """Apply ``--threat-model-context`` (path or inline text) onto the config.""" |
| note = _resolve_threat_model_context(getattr(args, "threat_model_context", None)) |
| if note: |
| config.threat_model_context = note |
|
|
|
|
| def _apply_provider_args(config: "object", args: argparse.Namespace) -> None: |
| """Apply the agentic / provider-routing flags. |
| |
| These are CLI conveniences over the existing env-var routing |
| (``BMC_AGENT_LLM_PROVIDER`` and ``BMC_AGENT_LLM_<ROLE>_PROVIDER``): |
| |
| --agentic GENERAL agentic stack: every agent role becomes |
| an investigating agent, but each is instantiated |
| by WHATEVER backend its routing says — a per-role |
| BMC_AGENT_LLM_<ROLE>_PROVIDER override, else the |
| global default provider (--provider / env), else |
| the auto-resolved provider. So roles can be a mix |
| of API / claude-code / codex / etc. Turns on the |
| soundness gate, agentic harness repair, split |
| spec-gen and component gating — WITHOUT forcing |
| any particular backend. |
| --agentic-claude-code Like --agentic, but FORCES every agent role onto |
| the local Claude Code CLI provider (the previous |
| --agentic behaviour). A per-role env override |
| still wins, so individual agents can be repointed. |
| --provider X sets the global default provider for every role. |
| --specs-via-claude-code routes ONLY the spec_gen + refinement roles to |
| the Claude Code CLI provider (your local |
| ``claude`` login; no API key), leaving every |
| other role on the global default. |
| --claude-code-agentic lets the claude-code provider use read-only |
| tools (Read/Grep/Glob) to explore the source |
| tree while drafting/refining, instead of a |
| one-shot text completion. |
| |
| Merges (rather than replaces) any role override already present from env so |
| explicit ``BMC_AGENT_LLM_*`` settings still compose. |
| """ |
| agentic = getattr(args, "agentic", False) |
| agentic_cc = getattr(args, "agentic_claude_code", False) |
| agentic_refine = getattr(args, "agentic_refine", False) |
|
|
| provider = getattr(args, "provider", "") or "" |
| if provider: |
| config.llm_provider = provider |
|
|
| |
| |
| |
| |
| ALL_AGENT_ROLES = ( |
| "spec_gen", "refinement", "realism", "triage", |
| "disagreement_diagnose", "feedback_distill", "classifier", |
| "dynamic_repro", "dynval_triage", "cbmc_driver", |
| ) |
| |
| |
| |
| |
| |
| |
| |
| cc_roles: set[str] = set() |
| if agentic_cc: |
| cc_roles |= set(ALL_AGENT_ROLES) |
| if getattr(args, "specs_via_claude_code", False): |
| cc_roles |= {"spec_gen", "refinement"} |
| if agentic_refine: |
| cc_roles |= {"refinement"} |
|
|
| want_cc_tools = (agentic or agentic_cc or agentic_refine |
| or getattr(args, "claude_code_agentic", False)) |
|
|
| if cc_roles: |
| overrides = getattr(config, "llm_role_overrides", None) |
| if overrides is None: |
| overrides = {} |
| config.llm_role_overrides = overrides |
| for role in sorted(cc_roles): |
| merged = dict(overrides.get(role, {})) |
| |
| |
| |
| if not merged.get("provider"): |
| merged["provider"] = "claude-code" |
| overrides[role] = merged |
|
|
| if want_cc_tools: |
| config.claude_code_agentic = True |
| |
| |
| dirs: list[str] = list(getattr(config, "claude_code_add_dirs", None) or []) |
| src = getattr(args, "source", "") or "" |
| if src: |
| dirs.append(str(Path(src).resolve().parent)) |
| for inc in getattr(args, "include_dir", None) or []: |
| dirs.append(str(Path(inc).resolve())) |
| |
| seen: set[str] = set() |
| config.claude_code_add_dirs = [d for d in dirs if not (d in seen or seen.add(d))] |
|
|
| if agentic or agentic_cc or agentic_refine: |
| |
| |
| config.enable_soundness_gate = True |
| config.enable_agentic_harness_repair = True |
| |
| |
| |
| config.enable_split_spec_gen = True |
|
|
| if agentic or agentic_cc: |
| |
| |
| |
| |
| |
| |
| |
| if not getattr(args, "no_dynamic_validation", False): |
| config.enable_dynamic_validation = True |
| if not getattr(args, "enable_realism_check", False): |
| config.enable_realism_check = False |
| if not getattr(args, "enable_triage", False): |
| config.enable_phase_3e_triage = False |
| |
| |
| |
| |
| |
| |
| if not getattr(args, "no_flag_selection", False): |
| config.enable_flag_selection = True |
| if not getattr(args, "no_inlining_advisor", False): |
| config.enable_inlining_advisor = True |
|
|
|
|
| def _print_ai_layers(config) -> None: |
| """Print the active AI layers so the operator can see what's running. |
| |
| The default-on AI layers are listed here; --no-* / --minimal flags |
| individually disable. Visible at startup so users can audit what |
| a given run actually exercises. |
| """ |
| layers = [ |
| ("realism check", getattr(config, "enable_realism_check", False)), |
| ("dynamic validation", getattr(config, "enable_dynamic_validation", False)), |
| ("flag selection", getattr(config, "enable_flag_selection", False)), |
| ("feedback loop", getattr(config, "enable_feedback_loop", False)), |
| ("spec refiner", getattr(config, "enable_spec_refiner", False)), |
| ("inlining advisor", getattr(config, "enable_inlining_advisor", False)), |
| ("spec-gen tools (v2.2)",getattr(config, "enable_spec_gen_tools", False)), |
| ("realism tools", getattr(config, "enable_realism_tools", False)), |
| ] |
| on = [n for n, v in layers if v] |
| off = [n for n, v in layers if not v] |
| if on: |
| thinking_tag = ( |
| " (extended thinking)" |
| if getattr(config, "enable_realism_thinking", False) |
| and getattr(config, "enable_realism_check", False) |
| else "" |
| ) |
| print(f"AI layers ON: {', '.join(on)}{thinking_tag}") |
| if off: |
| print(f"AI layers OFF: {', '.join(off)}") |
|
|
|
|
| def _cmd_generate(args: argparse.Namespace) -> int: |
| """Phase 1: Generate specs for all functions in a C source file.""" |
| from bmc_agent.artifacts import ArtifactStore |
| from bmc_agent.config import Config |
| from bmc_agent.llm import LLMClient |
| from bmc_agent.spec_generator import SpecGenerator |
|
|
| config = Config.from_env() |
| if args.output: |
| config.artifact_dir = args.output |
| if getattr(args, "include_dir", None): |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
| _apply_model_arg(config, args) |
| _apply_provider_args(config, args) |
|
|
| store = ArtifactStore(config.artifact_dir) |
| llm = LLMClient(config) |
| generator = SpecGenerator(config, llm, store) |
|
|
| domain_knowledge = _resolve_domain_knowledge(args.domain_knowledge) if args.domain_knowledge else "" |
|
|
| print(f"Generating specs for: {args.source}") |
| print(f"Driver name: {args.driver}") |
| print(f"Output directory: {config.artifact_dir}") |
|
|
| specs = generator.generate_specs( |
| source_file=args.source, |
| driver_name=args.driver, |
| domain_knowledge=domain_knowledge, |
| ) |
|
|
| print(f"\nGenerated {len(specs)} specs:") |
| for fn_name, spec in sorted(specs.items()): |
| fallback = spec.__dict__.get("fallback", False) |
| tag = " [FALLBACK]" if fallback else "" |
| print(f" {fn_name}{tag}") |
| print(f" pre: {spec.precondition[:80]}") |
| print(f" post: {spec.postcondition[:80]}") |
|
|
| return 0 |
|
|
|
|
| def _cmd_check(args: argparse.Namespace) -> int: |
| """Phase 2: Run BMC on previously generated specs.""" |
| from bmc_agent.artifacts import ArtifactStore |
| from bmc_agent.bmc_engine import BMCEngine |
| from bmc_agent.config import Config |
| from bmc_agent.backends import backend_for |
| from bmc_agent.source_parser import detect_language, parse_source_file |
|
|
| config = Config.from_env() |
| if hasattr(args, "output") and args.output: |
| config.artifact_dir = args.output |
| |
| |
| |
| if getattr(args, "include_dir", None): |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
|
|
| store = ArtifactStore(config.artifact_dir) |
| |
| |
| engine = BMCEngine( |
| config, |
| store, |
| backend=backend_for(detect_language(args.source), config), |
| ) |
|
|
| |
| source_file = args.source |
| print(f"Checking driver: {args.driver}") |
| print(f"Source file: {source_file}") |
| print(f"Artifact dir: {config.artifact_dir}") |
|
|
| parsed = parse_source_file(source_file) |
|
|
| |
| driver_name = args.driver |
| specs: dict = {} |
| target_func = getattr(args, "function", "") or "" |
| functions_to_check = list(parsed.functions.keys()) |
| if target_func: |
| if target_func not in parsed.functions: |
| print(f"Error: function '{target_func}' not found in {source_file}", file=sys.stderr) |
| return 1 |
| functions_to_check = [target_func] |
|
|
| for fn_name in functions_to_check: |
| spec = store.load_spec(driver_name, fn_name) |
| if spec is not None: |
| specs[fn_name] = spec |
| else: |
| print(f" Warning: no spec found for '{fn_name}' — skipping") |
|
|
| if not specs: |
| print("No specs to check. Run 'amc generate' first.") |
| return 1 |
|
|
| funcs = { |
| name: parsed.get_function_info(name) |
| for name in specs |
| if parsed.get_function_info(name) is not None |
| } |
|
|
| print(f"\nRunning BMC on {len(funcs)} function(s)...") |
| verdicts = engine.check_all(funcs, specs, parsed, driver_name) |
|
|
| |
| print(f"\nResults:") |
| verified_count = 0 |
| failed_count = 0 |
| error_count = 0 |
| for fn_name, verdict in sorted(verdicts.items()): |
| err_lower = (verdict.error or "").lower() |
| if verdict.error and "not found" in err_lower: |
| status = "SKIPPED (verifier not installed)" |
| error_count += 1 |
| elif verdict.error and ("unwind" in err_lower or "timed out" in err_lower): |
| |
| |
| status = f"INCONCLUSIVE ({verdict.error})" |
| error_count += 1 |
| elif verdict.error: |
| status = f"ERROR: {verdict.error}" |
| error_count += 1 |
| elif verdict.verified: |
| status = "VERIFIED" |
| verified_count += 1 |
| else: |
| status = f"FAILED ({len(verdict.counterexamples)} counterexample(s))" |
| failed_count += 1 |
| print(f" {fn_name:30s} {status}") |
|
|
| print(f"\nSummary: {verified_count} verified, {failed_count} failed, {error_count} errors/skipped") |
| return 0 |
|
|
|
|
| def _cmd_eval(args: argparse.Namespace) -> int: |
| """Phase 4: Run AMC and baselines on a corpus of C programs.""" |
| from bmc_agent.config import Config |
| from bmc_agent.evaluation.corpus import Corpus |
| from bmc_agent.evaluation.runner import EvaluationRunner |
|
|
| config = Config.from_env() |
| corpus = Corpus(args.corpus) |
| runner = EvaluationRunner(config) |
|
|
| print(f"Running evaluation on corpus: {args.corpus}") |
| print(f"Output directory: {args.output}") |
| print(f"Run baselines: {args.baselines}") |
|
|
| summary = runner.run_corpus( |
| corpus=corpus, |
| output_dir=args.output, |
| run_baselines=args.baselines, |
| ) |
|
|
| print(f"\n=== Evaluation Summary ===") |
| print(f" Total drivers: {summary.total_drivers}") |
| print(f" Total functions: {summary.total_functions}") |
| print(f" Total bugs found: {summary.total_bugs_found}") |
| print(f" Avg spec coverage: {summary.avg_spec_coverage * 100:.1f}%") |
| print(f" Avg FP rate: {summary.avg_false_positive_rate * 100:.1f}%") |
| print(f"\nReports saved to: {args.output}") |
| return 0 |
|
|
|
|
| def _cmd_report(args: argparse.Namespace) -> int: |
| """Phase 4: Generate a summary report from evaluation artifacts.""" |
| import json |
| from bmc_agent.artifacts import ArtifactStore |
| from bmc_agent.evaluation.metrics import DriverMetrics, EvaluationSummary |
| from bmc_agent.evaluation.report import ReportGenerator |
|
|
| eval_dir = Path(args.eval_dir) |
| summary_json = eval_dir / "eval_summary.json" |
|
|
| if not summary_json.exists(): |
| print( |
| f"Error: no eval_summary.json found in {args.eval_dir}. " |
| "Run 'amc eval' first.", |
| file=sys.stderr, |
| ) |
| return 1 |
|
|
| with summary_json.open("r", encoding="utf-8") as fh: |
| data = json.load(fh) |
|
|
| |
| per_driver = [ |
| DriverMetrics( |
| driver_name=d["driver_name"], |
| total_functions=d["total_functions"], |
| functions_specified=d["functions_specified"], |
| functions_checked=d["functions_checked"], |
| functions_verified=d["functions_verified"], |
| counterexamples_found=d["counterexamples_found"], |
| real_bugs_confirmed=d["real_bugs_confirmed"], |
| spurious_cex_count=d["spurious_cex_count"], |
| false_positive_rate=d["false_positive_rate"], |
| refinement_iterations=[], |
| avg_refinement_iters=d["avg_refinement_iters"], |
| spec_coverage=d["spec_coverage"], |
| runtime_seconds=d["runtime_seconds"], |
| token_cost=d["token_cost"], |
| bugs_by_type=d["bugs_by_type"], |
| ) |
| for d in data.get("per_driver", []) |
| ] |
| summary = EvaluationSummary( |
| total_drivers=data["total_drivers"], |
| total_functions=data["total_functions"], |
| total_bugs_found=data["total_bugs_found"], |
| avg_false_positive_rate=data["avg_false_positive_rate"], |
| avg_spec_coverage=data["avg_spec_coverage"], |
| avg_refinement_iters=data["avg_refinement_iters"], |
| total_token_cost=data["total_token_cost"], |
| bugs_by_type=data.get("bugs_by_type", {}), |
| per_driver=per_driver, |
| amc_unique_bugs=data.get("amc_unique_bugs", 0), |
| baseline_unique_bugs=data.get("baseline_unique_bugs", {}), |
| ) |
|
|
| from bmc_agent.artifacts import ArtifactStore |
|
|
| store = ArtifactStore(str(eval_dir)) |
| gen = ReportGenerator(store) |
| md = gen.generate_summary_report(summary) |
|
|
| output = args.output |
| if output: |
| Path(output).write_text(md, encoding="utf-8") |
| print(f"Report written to: {output}") |
| else: |
| print(md) |
|
|
| return 0 |
|
|
|
|
| def _cmd_corpus_generate(args: argparse.Namespace) -> int: |
| """Phase 4: Use LLM to generate synthetic C programs for the corpus.""" |
| from bmc_agent.config import Config |
| from bmc_agent.evaluation.corpus import Corpus |
| from bmc_agent.llm import LLMClient |
|
|
| config = Config.from_env() |
| llm = LLMClient(config) |
| corpus = Corpus(args.output) |
|
|
| print(f"Generating {args.count} synthetic corpus entries into: {args.output}") |
| entries = corpus.generate_synthetic_corpus( |
| output_dir=args.output, |
| llm=llm, |
| count=args.count, |
| ) |
| print(f"Generated {len(entries)} entries:") |
| for e in entries: |
| print(f" {e.name} ({e.driver_type}): {len(e.ground_truth_bugs)} known bug(s)") |
| return 0 |
|
|
|
|
| def _run_standalone(args: argparse.Namespace, config: "object") -> int: |
| """Standalone whole-program verification (see bmc_agent.standalone).""" |
| from bmc_agent.standalone import verify_standalone |
|
|
| entry = getattr(args, "entry", None) or "main" |
| unwind = int(getattr(args, "standalone_unwind", None) or 64) |
| if getattr(args, "include_dir", None): |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
|
|
| print(f"Standalone whole-program verification: {args.source}") |
| print(f"Entry: {entry} unwind: {unwind}") |
| print("Checks: bounds, pointer, signed-overflow, pointer-overflow, " |
| "div-by-zero, unwinding-assertions") |
|
|
| result, n_acsl = verify_standalone( |
| args.source, config, entry=entry, unwind=unwind, |
| timeout=int(getattr(config, "cbmc_timeout", 0) or 300), |
| ) |
|
|
| print("\n=== Standalone result ===") |
| if result.error and not result.counterexamples: |
| print(f"INVALID / CBMC ERROR: {result.error}") |
| return 2 |
| if result.verified: |
| extra = f" (incl. {n_acsl} //@ assert)" if n_acsl else "" |
| print(f"VERIFICATION SUCCESSFUL — the program as written is safe{extra}.") |
| return 0 |
| print(f"VERIFICATION FAILED — {len(result.counterexamples)} property violation(s):") |
| for ce in result.counterexamples[:25]: |
| loc = ce.failure_location or {} |
| where = f"{loc.get('file','?')}:{loc.get('line','?')}" if loc else "" |
| print(f" - {ce.failing_property or '?'} {where} {ce.description}".rstrip()) |
| return 1 |
|
|
|
|
| def _run_assert_synth(args: argparse.Namespace, config: "object") -> int: |
| """Assertion-driven spec synthesis (see bmc_agent.assert_driven_specs).""" |
| from bmc_agent.assert_driven_specs import synthesize |
| from bmc_agent.llm import LLMClient |
|
|
| entry = getattr(args, "entry", None) or "main" |
| if getattr(args, "include_dir", None): |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
|
|
| print(f"Assertion-driven spec synthesis: {args.source}") |
| print(f"Entry: {entry} (refine postconditions until //@ asserts hold; " |
| "with no goal, mine + soundly verify a contract)") |
| r = synthesize(args.source, config, LLMClient(config), entry=entry) |
| if getattr(r, "entry", "") and r.entry != entry: |
| print(f" (entry auto-resolved to '{r.entry}' — the function containing the asserts)") |
| entry = r.entry |
|
|
| |
| |
| |
| |
| |
| |
| |
| _ovf_used = False |
| _ovf_wp = None |
| if (r.ok and getattr(config, "oracle", "cbmc") == "frama-c" |
| and getattr(args, "overflow_rigor", True)): |
| try: |
| from bmc_agent.frama_c import (insert_contract_acsl, run_wp, |
| function_assigns_clause, |
| function_frame_precondition) |
| from bmc_agent.assert_driven_specs import ( |
| _conjoin_precondition, overflow_preconditions, |
| overflow_preconditions_from_body) |
| _src0 = open(str(args.source)).read() |
| _fc = getattr(config, "frama_c_path", "frama-c") |
| ovf = overflow_preconditions(_src0, r.postconditions or {}) |
| |
| |
| |
| |
| |
| if getattr(config, "math_ints", False): |
| body_ovf = overflow_preconditions_from_body( |
| _src0, list((r.postconditions or {}).keys()), frama_c_path=_fc) |
| for fn, term in body_ovf.items(): |
| if fn not in ovf: |
| ovf[fn] = term |
| elif term not in ovf[fn]: |
| ovf[fn] = f"({ovf[fn]}) && ({term})" |
| if ovf: |
| _assigns0 = {fn: function_assigns_clause(_src0, fn) |
| for fn in (r.postconditions or {})} |
| aug_pre = dict(r.preconditions or {}) |
| for fn, term in ovf.items(): |
| aug_pre[fn] = _conjoin_precondition(aug_pre.get(fn, "true"), term) |
| for fn, assigns in _assigns0.items(): |
| frame_pre = function_frame_precondition(_src0, fn, assigns) |
| if frame_pre: |
| aug_pre[fn] = _conjoin_precondition(aug_pre.get(fn, "true"), frame_pre) |
| annotated = "#include <limits.h>\n" + _src0 |
| for fn, p in (r.postconditions or {}).items(): |
| annotated = insert_contract_acsl( |
| annotated, fn, requires=aug_pre.get(fn, "true"), ensures=p, |
| assigns=_assigns0.get(fn, "")) |
| wp = run_wp(annotated, frama_c_path=getattr(config, "frama_c_path", "frama-c"), |
| rte=True, exclude_terminates=True) |
| if wp.available and wp.n_total and wp.n_proved == wp.n_total: |
| r.preconditions = aug_pre |
| _ovf_used, _ovf_wp = True, wp |
| print("overflow-rigor: added no-overflow precondition(s) " |
| f"for {', '.join(ovf)} — re-verified with RTE on") |
| except Exception as exc: |
| print(f"overflow-rigor: skipped ({exc}); math-int contract stands.") |
|
|
| |
| |
| from bmc_agent.acsl import contract_to_acsl |
| from bmc_agent.assert_driven_specs import _conjoin_precondition |
| from bmc_agent.frama_c import function_assigns_clause, function_frame_precondition |
| _src_text = open(str(args.source)).read() |
| fn_assigns = {fn: function_assigns_clause(_src_text, fn) |
| for fn in (r.postconditions or {})} |
| fn_requires = {} |
| for fn in (r.postconditions or {}): |
| req = (r.preconditions or {}).get(fn, "true") |
| frame_pre = function_frame_precondition(_src_text, fn, fn_assigns.get(fn, "")) |
| if frame_pre: |
| req = _conjoin_precondition(req, frame_pre) |
| fn_requires[fn] = req |
|
|
| if getattr(config, "oracle", "cbmc") == "frama-c" and (r.postconditions or {}) and not _ovf_used: |
| from bmc_agent.assert_driven_specs import _split_conjuncts |
| from bmc_agent.frama_c import insert_contract_block, run_wp |
|
|
| def _annotated_for(posts): |
| annotated_src = _src_text |
| for _fn, _p in (posts or {}).items(): |
| _block = contract_to_acsl(fn_requires.get(_fn, "true"), _p, |
| assigns=fn_assigns.get(_fn, "")) |
| annotated_src = insert_contract_block( |
| annotated_src, _fn, _block.rstrip() + "\n") |
| return annotated_src |
|
|
| math_ints = bool(getattr(config, "math_ints", False)) |
| posts = dict(r.postconditions or {}) |
| wp0 = run_wp(_annotated_for(posts), |
| frama_c_path=getattr(config, "frama_c_path", "frama-c"), |
| rte=not math_ints, exclude_terminates=True) |
| if wp0.available and wp0.n_total and wp0.n_proved == wp0.n_total: |
| if not r.ok: |
| r.ok = True |
| r.failing_asserts = [] |
| r.note = ("Frama-C/WP confirmed the rendered ACSL contract " |
| "(engine did not prove it)") |
| if wp0.available and wp0.n_total and wp0.n_proved < wp0.n_total: |
| best_gap = wp0.n_total - wp0.n_proved |
| best_posts = dict(posts) |
| pruned = [] |
| changed = True |
| trials = 0 |
| max_trials = 24 |
|
|
| def _prune_priority(item): |
| _idx, _clause = item |
| clause = _clause.strip() |
| if re.fullmatch(r"\\old\s*\([^)]+\)\s*==\s*-?\d+\b", clause): |
| return 0 |
| if re.fullmatch(r"[A-Za-z_]\w*\s*==\s*-?\d+\b", clause): |
| return 1 |
| if "\\old" in clause: |
| return 2 |
| return 3 |
|
|
| while changed and best_gap > 0: |
| changed = False |
| for fn in list(posts): |
| clauses = _split_conjuncts(posts.get(fn, "")) |
| if len(clauses) <= 1: |
| continue |
| ordered = sorted(enumerate(list(clauses)), key=_prune_priority) |
| for idx, clause in ordered: |
| if trials >= max_trials: |
| break |
| trials += 1 |
| trial_clauses = clauses[:idx] + clauses[idx + 1:] |
| trial_posts = dict(posts) |
| trial_posts[fn] = " && ".join(trial_clauses) or "true" |
| wp = run_wp( |
| _annotated_for(trial_posts), |
| frama_c_path=getattr(config, "frama_c_path", "frama-c"), |
| rte=not math_ints, |
| exclude_terminates=True, |
| ) |
| if not (wp.available and wp.n_total): |
| continue |
| gap = wp.n_total - wp.n_proved |
| if gap < best_gap: |
| posts, best_gap = trial_posts, gap |
| best_posts = dict(trial_posts) |
| pruned.append(f"{fn}: {clause}") |
| changed = True |
| break |
| if trials >= max_trials: |
| break |
| if changed: |
| break |
| if pruned and best_gap == 0: |
| r.postconditions = best_posts |
| was_ok = r.ok |
| r.ok = True |
| r.failing_asserts = [] |
| msg = "WP-pruned unproved postcondition conjunct(s): " + "; ".join(pruned) |
| if was_ok: |
| r.note += "; " + msg |
| else: |
| r.note = "Frama-C/WP confirmed the pruned ACSL contract; " + msg |
|
|
| acsl_blocks = {} |
| for fn, p in (r.postconditions or {}).items(): |
| block = contract_to_acsl(fn_requires.get(fn, "true"), p, |
| assigns=fn_assigns.get(fn, "")) |
| if block: |
| acsl_blocks[fn] = block |
|
|
| |
| import json as _json, os as _os |
| out_dir = getattr(config, "artifact_dir", None) or "." |
| _os.makedirs(out_dir, exist_ok=True) |
| _base = _os.path.splitext(_os.path.basename(str(args.source)))[0] or "out" |
| out_path = _os.path.join(out_dir, f"synthesized_specs_{_base}.json") |
| payload = { |
| "source": str(args.source), |
| "entry": entry, |
| "satisfied": bool(r.ok), |
| "na": bool(getattr(r, "no_goals", False)), |
| "iterations": r.iterations, |
| "asserts": list(r.asserts or []), |
| "failing_asserts": list(r.failing_asserts or []), |
| "synthesized_specs": { |
| fn: {"requires": fn_requires.get(fn, "true"), "ensures": p} |
| for fn, p in (r.postconditions or {}).items() |
| }, |
| "note": r.note, |
| } |
| try: |
| with open(out_path, "w") as fh: |
| _json.dump(payload, fh, indent=2) |
| except OSError as exc: |
| print(f"(warning: could not write {out_path}: {exc})") |
|
|
| payload["acsl"] = acsl_blocks |
| for fn, a in fn_assigns.items(): |
| if a: |
| payload["synthesized_specs"].get(fn, {})["assigns"] = a |
| try: |
| with open(out_path, "w") as fh: |
| _json.dump(payload, fh, indent=2) |
| except OSError: |
| pass |
|
|
| from bmc_agent.dsl_to_cbmc import fully_parenthesize |
| print("\n=== Synthesized specs (DSL) ===") |
| for fn, p in (r.postconditions or {}).items(): |
| |
| |
| req = fn_requires.get(fn, "true") |
| print(f" {fn}: requires {fully_parenthesize(req)}") |
| if fn_assigns.get(fn): |
| print(f" {' ' * len(fn)} assigns {fn_assigns[fn]}") |
| print(f" {' ' * len(fn)} ensures {fully_parenthesize(p)}") |
| print("\n=== Synthesized specs (ACSL) ===") |
| if _ovf_used: |
| print("#include <limits.h>") |
| for fn, block in acsl_blocks.items(): |
| print(f"// contract for {fn}") |
| print(block) |
| print(f"\nasserts: {len(r.asserts)} iterations: {r.iterations}") |
| print(f"written: {out_path}") |
|
|
| |
| |
| |
| |
| if r.ok and _ovf_used and _ovf_wp is not None: |
| |
| print(f"Frama-C/WP: CONFIRMED — proved {_ovf_wp.n_proved}/{_ovf_wp.n_total} " |
| "goals (RTE on; signed overflow checked).") |
| elif r.ok and getattr(config, "oracle", "cbmc") == "frama-c": |
| from bmc_agent.frama_c import insert_contract_acsl, run_wp |
| try: |
| annotated = _src_text |
| for fn, p in (r.postconditions or {}).items(): |
| |
| |
| |
| |
| |
| |
| annotated = insert_contract_acsl( |
| annotated, fn, |
| requires=fn_requires.get(fn, "true"), ensures=p, |
| assigns=fn_assigns.get(fn, "")) |
| |
| |
| math_ints = bool(getattr(config, "math_ints", False)) |
| wp = run_wp(annotated, frama_c_path=getattr(config, "frama_c_path", "frama-c"), |
| rte=not math_ints, exclude_terminates=True) |
| if not wp.available: |
| print(f"Frama-C/WP: requested but unavailable ({wp.error}); contract " |
| "validated by CBMC only — install frama-c + alt-ergo for WP confirmation.") |
| elif wp.n_total and wp.n_proved == wp.n_total: |
| print(f"Frama-C/WP: CONFIRMED — proved {wp.n_proved}/{wp.n_total} goals.") |
| else: |
| print(f"Frama-C/WP: proved {wp.n_proved}/{wp.n_total} goals; " |
| f"unproved: {', '.join(wp.unproved) or '?'}") |
| except Exception as exc: |
| print(f"Frama-C/WP: confirmation step errored ({exc}); CBMC verdict stands.") |
|
|
| if getattr(r, "no_goals", False): |
| print(f"RESULT: N/A — {r.note}.") |
| print(" (No assertion target, and no non-trivial contract could be mined " |
| "from a function body. This is NOT a pass — add a //@ assert / assert / " |
| "__VERIFIER_assert stating the expected result to make it a real target.)") |
| return 2 |
| if r.ok: |
| if r.asserts: |
| print("RESULT: SATISFIED — all //@ asserts are provable from the synthesized specs.") |
| else: |
| |
| |
| print("RESULT: SATISFIED — synthesized function contract(s) from the body " |
| "and proved the implementation satisfies them (no explicit goal needed).") |
| return 0 |
| print(f"RESULT: NOT SATISFIED — {r.note}") |
| for a in (r.failing_asserts or []): |
| print(f" unprovable: {a}") |
| return 1 |
|
|
|
|
| def _run_specs_bench(args: argparse.Namespace, config: "object") -> int: |
| """One-flag Specification-Synthesis benchmark runner. Turns on the |
| mathematical-integer semantics these benchmarks assume, then dispatches by |
| program content: loops → loop-invariant synthesis; otherwise → function- |
| contract synthesis. Both emit ACSL.""" |
| config.math_ints = True |
| |
| |
| |
| |
| if getattr(args, "oracle", None): |
| config.oracle = args.oracle |
| else: |
| from bmc_agent.frama_c import frama_c_available |
| fc_path = getattr(config, "frama_c_path", "frama-c") |
| config.oracle = "frama-c" if frama_c_available(fc_path) else "cbmc" |
| print(f"specs-bench: oracle auto-selected → {config.oracle}" |
| + ("" if config.oracle == "frama-c" |
| else " (frama-c not on PATH; install frama-c + alt-ergo to use WP)")) |
| from bmc_agent.loop_invariants import find_loops, brace_braceless_loops |
| src = "" |
| try: |
| with open(args.source) as fh: |
| src = fh.read() |
| except OSError as exc: |
| print(f"error: cannot read {args.source}: {exc}") |
| return 2 |
| |
| |
| if find_loops(brace_braceless_loops(src)): |
| print("specs-bench: loops present → loop-invariant synthesis (+ --math-ints)") |
| return _run_loop_invariant_synth(args, config) |
| print("specs-bench: no loops → function-contract synthesis") |
| return _run_assert_synth(args, config) |
|
|
|
|
| def _run_loop_invariant_synth(args: argparse.Namespace, config: "object") -> int: |
| """Specification-synthesis mode: synthesize loop invariants (ACSL) that are |
| inductive and sufficient to prove the program's goals (see |
| bmc_agent.loop_invariants).""" |
| from bmc_agent.loop_invariants import synthesize_loop_invariants |
| from bmc_agent.llm import LLMClient |
|
|
| entry = getattr(args, "entry", None) or "main" |
| if getattr(args, "include_dir", None): |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
| unwind = int(getattr(args, "standalone_unwind", 0) or 0) |
| |
| |
| |
| |
| |
| |
| if (getattr(args, "math_ints", False) |
| or getattr(args, "specs_bench", False) |
| or getattr(config, "math_ints", False)): |
| config.math_ints = True |
| if getattr(args, "oracle", None): |
| config.oracle = args.oracle |
|
|
| print(f"Loop-invariant synthesis: {args.source}") |
| print(f"Entry: {entry} (propose → CBMC validity+adequacy → refine)") |
| r = synthesize_loop_invariants(args.source, config, LLMClient(config), |
| entry=entry, unwind=unwind) |
|
|
| import json as _json, os as _os |
| out_dir = getattr(config, "artifact_dir", None) or "." |
| _os.makedirs(out_dir, exist_ok=True) |
| base = _os.path.splitext(_os.path.basename(str(args.source)))[0] or "out" |
| out_path = _os.path.join(out_dir, f"synthesized_loop_invariants_{base}.json") |
| inst_path = _os.path.join(out_dir, f"{base}_instrumented.c") |
| log_path = _os.path.join(out_dir, f"{base}_cbmc.log") |
| payload = { |
| "source": str(args.source), "entry": entry, |
| "satisfied": bool(r.ok), |
| "na": bool(getattr(r, "no_goals", False)), |
| "iterations": r.iterations, |
| "goals": list(r.goals or []), |
| "loop_invariants": {str(o): invs for o, invs in (r.annotations or {}).items()}, |
| "acsl": r.acsl, "note": r.note, |
| "instrumented_source": _os.path.relpath(inst_path) if r.instrumented else "", |
| "cbmc_log": _os.path.relpath(log_path) if r.cbmc_log else "", |
| } |
| try: |
| with open(out_path, "w") as fh: |
| _json.dump(payload, fh, indent=2) |
| if r.instrumented: |
| with open(inst_path, "w") as fh: |
| fh.write(r.instrumented) |
| if r.cbmc_log: |
| with open(log_path, "w") as fh: |
| fh.write(r.cbmc_log) |
| except OSError as exc: |
| print(f"(warning: could not write artifacts: {exc})") |
|
|
| print("\n=== Synthesized loop invariants (ACSL) ===") |
| print(r.acsl or " (none)") |
| print(f"\ngoals: {len(r.goals)} iterations: {r.iterations}") |
| print(f"written: {out_path}") |
| if r.instrumented: |
| print(f"harness: {inst_path}") |
| if r.cbmc_log: |
| print(f"cbmc log: {log_path}") |
| if getattr(r, "no_goals", False): |
| print(f"RESULT: N/A — {r.note}.") |
| print(" (No assertion target, so nothing was proved. This is NOT a pass — add a " |
| "//@ assert / assert / __VERIFIER_assert stating the expected result.)") |
| return 2 |
| if r.ok: |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| if (getattr(config, "oracle", "cbmc") == "frama-c" |
| and getattr(config, "math_ints", False) |
| and getattr(args, "overflow_rigor", True) |
| and r.annotations): |
| try: |
| from bmc_agent.loop_invariants import check_loop_invariants_wp |
| _src = open(str(args.source)).read() |
| _chk = check_loop_invariants_wp(_src, r.annotations, config, entry, |
| force_rte=True) |
| _wp = getattr(_chk, "result", None) |
| if _wp is not None and _wp.available: |
| _ovf = [g for g in _wp.unproved if "overflow" in g.lower()] |
| if _wp.proved: |
| print("overflow-rigor: machine-int sound — re-verified with RTE on " |
| "(signed overflow provably absent at the loop bound).") |
| elif _ovf: |
| print(f"overflow-rigor: math-int only — {len(_ovf)} signed-overflow " |
| "site(s) in the loop body are NOT machine-int safe at this bound; " |
| "the result holds under mathematical-integer semantics (--math-ints).") |
| else: |
| print("overflow-rigor: math-int only — the invariants are not preserved " |
| "under machine-int (wrapping) semantics; the result holds under " |
| "mathematical-integer semantics (--math-ints).") |
| except Exception as exc: |
| print(f"overflow-rigor: recheck skipped ({exc}); math-int result stands.") |
| print("RESULT: SATISFIED — invariants are inductive and prove all goals.") |
| return 0 |
| print(f"RESULT: NOT SATISFIED — {r.note}") |
| return 1 |
|
|
|
|
| def _cmd_verify(args: argparse.Namespace) -> int: |
| """Full pipeline: generate specs + run BMC + validate counterexamples (Phase 3).""" |
| from bmc_agent.config import Config |
| from bmc_agent.pipeline import AMCPipeline |
|
|
| config = Config.from_env() |
| if hasattr(args, "output") and args.output: |
| config.artifact_dir = args.output |
| if hasattr(args, "include_dir") and args.include_dir: |
| config.include_dirs = args.include_dir |
| config.preprocess = True |
| if getattr(args, "real_libc", False): |
| |
| |
| |
| config.cbmc_real_libc = True |
| config.preprocess = False |
| if getattr(args, "strict_dsl", False): |
| config.strict_dsl = True |
| if getattr(args, "raw_bytes", False): |
| config.raw_bytes = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
| if getattr(args, "skip_refinement", False): |
| config.skip_refinement = True |
| if getattr(args, "enable_realism_check", False): |
| config.enable_realism_check = True |
| if getattr(args, "enable_realism_thinking", False): |
| config.enable_realism_thinking = True |
| if getattr(args, "enable_flag_selection", False): |
| config.enable_flag_selection = True |
| if getattr(args, "enable_feedback_loop", False): |
| config.enable_feedback_loop = True |
| if getattr(args, "feedback_max_iters", None) is not None: |
| config.feedback_max_iters = int(args.feedback_max_iters) |
| if getattr(args, "enable_dynamic_validation", False): |
| config.enable_dynamic_validation = True |
| if getattr(args, "threat_model", None): |
| config.threat_model = args.threat_model |
| _apply_threat_model_context(config, args) |
| if getattr(args, "lite_mode", False): |
| config.lite_mode = True |
| if getattr(args, "legacy_spec_gen", False): |
| config.use_legacy_spec_gen = True |
| if getattr(args, "enable_spec_refiner", False): |
| config.enable_spec_refiner = True |
| if getattr(args, "enable_soundness_gate", False): |
| config.enable_soundness_gate = True |
| if getattr(args, "enable_agentic_harness_repair", False): |
| config.enable_agentic_harness_repair = True |
| if getattr(args, "enable_classifier", False): |
| config.enable_classifier = True |
| if getattr(args, "enable_triage", False): |
| config.enable_phase_3e_triage = True |
| if getattr(args, "enable_inlining_advisor", False): |
| config.enable_inlining_advisor = True |
| |
| if getattr(args, "no_realism_check", False): |
| config.enable_realism_check = False |
| if getattr(args, "no_dynamic_validation", False): |
| config.enable_dynamic_validation = False |
| if getattr(args, "no_flag_selection", False): |
| config.enable_flag_selection = False |
| if getattr(args, "no_feedback_loop", False): |
| config.enable_feedback_loop = False |
| if getattr(args, "no_spec_refiner", False): |
| config.enable_spec_refiner = False |
| if getattr(args, "no_inlining_advisor", False): |
| config.enable_inlining_advisor = False |
| if getattr(args, "no_spec_gen_tools", False): |
| config.enable_spec_gen_tools = False |
| if getattr(args, "no_realism_tools", False): |
| config.enable_realism_tools = False |
| if getattr(args, "minimal", False): |
| config.enable_realism_check = False |
| config.enable_dynamic_validation = False |
| config.enable_flag_selection = False |
| config.enable_feedback_loop = False |
| config.enable_spec_refiner = False |
| config.enable_inlining_advisor = False |
| config.enable_spec_gen_tools = False |
| config.enable_realism_tools = False |
| _apply_model_arg(config, args) |
| _apply_provider_args(config, args) |
|
|
| |
| |
| |
| |
| if getattr(args, "standalone", False): |
| return _run_standalone(args, config) |
|
|
| |
| |
| if getattr(args, "specs_from_asserts", False): |
| return _run_assert_synth(args, config) |
|
|
| if getattr(args, "synth_loop_invariants", False): |
| return _run_loop_invariant_synth(args, config) |
|
|
| if getattr(args, "specs_bench", False): |
| return _run_specs_bench(args, config) |
|
|
| domain_knowledge = _resolve_domain_knowledge(args.domain_knowledge) if (hasattr(args, "domain_knowledge") and args.domain_knowledge) else "" |
|
|
| print(f"Full verification pipeline for: {args.source}") |
| print(f"Driver: {args.driver}") |
| print(f"Artifact dir: {config.artifact_dir}") |
| if config.skip_refinement: |
| print("Mode: FilteringOnly (skip_refinement=True) — RQ3 ablation baseline") |
| if config.preprocess: |
| print(f"Include dirs: {config.include_dirs}") |
| _print_ai_layers(config) |
|
|
| pipeline = AMCPipeline(config) |
| bug_reports = pipeline.run( |
| source_file=args.source, |
| driver_name=args.driver, |
| domain_knowledge=domain_knowledge, |
| ) |
|
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| def _final_classification_is_spurious(driver_name: str, fn_name: str, violated_property: str) -> bool: |
| import json, os |
| path = os.path.join(config.artifact_dir, driver_name, fn_name, "classification.json") |
| try: |
| with open(path) as f: |
| data = json.load(f) |
| cls = data.get("classification") or {} |
| saved_prop = (cls.get("counterexample") or {}).get("failing_property") |
| if saved_prop and violated_property and saved_prop != violated_property: |
| return False |
| return cls.get("outcome") == "spurious" |
| except Exception: |
| return False |
|
|
| def _realism_was_unrealistic(report) -> bool: |
| rc = getattr(report, "realism_check", None) or {} |
| if isinstance(rc, dict): |
| return (rc.get("verdict") or "").lower() == "unrealistic" |
| return getattr(rc, "verdict", "").lower() == "unrealistic" if rc else False |
|
|
| survivors = [ |
| r for r in bug_reports |
| if not _realism_was_unrealistic(r) |
| and not _final_classification_is_spurious(args.driver, r.function_name, getattr(r, "violated_property", "") or "") |
| ] |
| dropped = len(bug_reports) - len(survivors) |
|
|
| print(f"\n=== Results ===") |
| if dropped > 0: |
| print( |
| f"(suppressed {dropped} stale finding(s): rejected by realism check " |
| f"or re-classified as spurious after refinement)" |
| ) |
| if not survivors: |
| print("No bugs confirmed.") |
| else: |
| print(f"Confirmed bugs: {len(survivors)}") |
| for report in survivors: |
| print(f"\n [{report.bug_type.upper()}] {report.function_name}") |
| print(f" Property: {report.violated_property}") |
| print(f" Confidence: {report.confidence}") |
| if report.call_chain: |
| print(f" Call chain: {' → '.join(report.call_chain)}") |
|
|
| |
| |
| |
| latent_reports = getattr(pipeline, "latent_reports", None) or [] |
| if latent_reports: |
| print(f"\nLatent panics on pub API: {len(latent_reports)}") |
| print( |
| " (panic reachable via cargo-fuzz / future-caller, " |
| "but no in-tree call site produces the state)" |
| ) |
| for report in latent_reports: |
| print(f"\n [{(report.bug_type or 'panic').upper()}] {report.function_name}") |
| print(f" Property: {report.violated_property}") |
|
|
| |
| summary = pipeline.reporter.generate_summary(args.driver) |
| print(f"\n{summary}") |
|
|
| return 0 |
|
|
|
|
| def _cmd_baseline(args: argparse.Namespace) -> int: |
| """Run CBMC-alone baseline on a C source file (no LLM, no spec generation).""" |
| from bmc_agent.artifacts import ArtifactStore |
| from bmc_agent.config import Config |
| from bmc_agent.evaluation.baselines import CBMCAloneBaseline |
|
|
| config = Config.from_env() |
| if args.output: |
| config.artifact_dir = args.output |
|
|
| store = ArtifactStore(config.artifact_dir) |
| baseline = CBMCAloneBaseline() |
|
|
| print(f"CBMC-alone baseline for: {args.source}") |
| print(f"Driver: {args.driver}") |
| print(f"Artifact dir: {config.artifact_dir}") |
|
|
| result = baseline.run( |
| source_file=args.source, |
| driver_name=args.driver, |
| config=config, |
| store=store, |
| ) |
|
|
| if result.error: |
| print(f"\nWarning: {result.error}", file=sys.stderr) |
|
|
| print(f"\n=== CBMC-Alone Baseline Results ===") |
| if not result.bugs_found: |
| print("No bugs found by CBMC alone.") |
| else: |
| print(f"Findings ({len(result.bugs_found)} total):") |
| for bug in result.bugs_found: |
| print(f" {bug}") |
|
|
| print(f"\nRuntime: {result.runtime_seconds:.1f}s") |
| return 0 |
|
|
|
|
| def _cmd_ablation_baseline(args: argparse.Namespace) -> int: |
| """Run AMC-ablation baseline: bottom-up spec generation (no caller context).""" |
| from bmc_agent.config import Config |
| from bmc_agent.evaluation.baselines import AMCAblationBaseline |
|
|
| config = Config.from_env() |
| if args.output: |
| config.artifact_dir = args.output |
| _apply_model_arg(config, args) |
| _apply_provider_args(config, args) |
|
|
| baseline = AMCAblationBaseline() |
|
|
| print(f"AMC-ablation baseline for: {args.source}") |
| print(f"Driver: {args.driver}") |
| print(f"Artifact dir: {config.artifact_dir}") |
| print(f"Model: {config.llm_model}") |
| print("Mode: bottom-up spec generation (no caller context)") |
|
|
| result = baseline.run( |
| source_file=args.source, |
| driver_name=args.driver, |
| config=config, |
| ) |
|
|
| if result.error: |
| print(f"\nWarning: {result.error}", file=sys.stderr) |
|
|
| print(f"\n=== AMC-Ablation Baseline Results ===") |
| if not result.bugs_found: |
| print("No bugs found.") |
| else: |
| print(f"Findings ({len(result.bugs_found)} total):") |
| for bug in result.bugs_found: |
| print(f" {bug}") |
|
|
| print(f"\nRuntime: {result.runtime_seconds:.1f}s") |
| return 0 |
|
|
|
|
| def _cmd_judge_dir(args: argparse.Namespace) -> int: |
| """Simple LLM-as-judge mode. No multi-stage pipeline.""" |
| from pathlib import Path |
| from bmc_agent.config import Config |
| from bmc_agent.judge_pipeline import run_judge_pipeline |
|
|
| config = Config.from_env() |
| if getattr(args, "model", None): |
| config.llm_model = args.model |
| if getattr(args, "enable_flag_selection", False): |
| config.enable_flag_selection = True |
| if getattr(args, "enable_feedback_loop", False): |
| config.enable_feedback_loop = True |
| if getattr(args, "agentic_harness", False): |
| config.enable_agentic_harness = True |
| if getattr(args, "refine_rounds", None) is not None: |
| config.agentic_refine_rounds = int(args.refine_rounds) |
|
|
| summary = run_judge_pipeline( |
| config=config, |
| source_dir=Path(args.source_dir), |
| driver=args.driver, |
| output=Path(args.output), |
| exclude_patterns=list(getattr(args, "exclude", None) or []), |
| include_dirs=list(getattr(args, "include_dir", None) or []), |
| defines=list(getattr(args, "defines", None) or []), |
| cbmc_unwind=int(getattr(args, "cbmc_unwind", 4)), |
| cbmc_timeout=int(getattr(args, "cbmc_timeout", 60)), |
| max_functions=getattr(args, "max_functions", None), |
| only_files=getattr(args, "only_file", None), |
| ) |
|
|
| |
| total_real = 0 |
| total_unreal = 0 |
| total_uncertain = 0 |
| total_adj = 0 |
| for stem, pf in summary.get("per_file", {}).items(): |
| v = pf.get("verdicts", {}) |
| total_real += v.get("realistic", 0) |
| total_unreal += v.get("unrealistic", 0) |
| total_uncertain += v.get("uncertain", 0) |
| for fn_name, rec in (pf.get("functions") or {}).items(): |
| for cex_rec in (rec.get("cexs") or []): |
| total_adj += len((cex_rec.get("judge") or {}).get("adjacent_bugs") or []) |
| print(f"\n=== judge-dir summary ===") |
| print(f" files parsed: {summary.get('n_files_parsed', 0)}") |
| print(f" files skipped: {summary.get('n_files_skipped', 0)}") |
| print(f" verdict counts: realistic={total_real} unrealistic={total_unreal} uncertain={total_uncertain}") |
| print(f" adjacent-bug hypotheses: {total_adj}") |
| print(f" summary.json: {Path(args.output) / args.driver / 'summary.json'}") |
| return 0 |
|
|
|
|
| def _cmd_verify_dir(args: argparse.Namespace) -> int: |
| """Run the full pipeline on every .c file in a directory.""" |
| from bmc_agent.config import Config |
| from bmc_agent.pipeline import AMCPipeline |
|
|
| config = Config.from_env() |
| if args.output: |
| config.artifact_dir = args.output |
| if getattr(args, "skip_refinement", False): |
| config.skip_refinement = True |
| if getattr(args, "enable_dynamic_validation", False): |
| config.enable_dynamic_validation = True |
| if getattr(args, "enable_realism_check", False): |
| config.enable_realism_check = True |
| if getattr(args, "enable_realism_thinking", False): |
| config.enable_realism_thinking = True |
| if getattr(args, "enable_flag_selection", False): |
| config.enable_flag_selection = True |
| if getattr(args, "enable_feedback_loop", False): |
| config.enable_feedback_loop = True |
| if getattr(args, "feedback_max_iters", None) is not None: |
| config.feedback_max_iters = int(args.feedback_max_iters) |
| if getattr(args, "real_libc", False): |
| config.cbmc_real_libc = True |
| config.preprocess = False |
| if getattr(args, "strict_dsl", False): |
| config.strict_dsl = True |
| if getattr(args, "raw_bytes", False): |
| config.raw_bytes = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
| if getattr(args, "threat_model", None): |
| config.threat_model = args.threat_model |
| _apply_threat_model_context(config, args) |
| if getattr(args, "lite_mode", False): |
| config.lite_mode = True |
| if getattr(args, "legacy_spec_gen", False): |
| config.use_legacy_spec_gen = True |
| if getattr(args, "enable_spec_refiner", False): |
| config.enable_spec_refiner = True |
| if getattr(args, "enable_soundness_gate", False): |
| config.enable_soundness_gate = True |
| if getattr(args, "enable_agentic_harness_repair", False): |
| config.enable_agentic_harness_repair = True |
| if getattr(args, "enable_classifier", False): |
| config.enable_classifier = True |
| if getattr(args, "enable_triage", False): |
| config.enable_phase_3e_triage = True |
| if getattr(args, "enable_inlining_advisor", False): |
| config.enable_inlining_advisor = True |
| if getattr(args, "enable_phase_3e_triage", False): |
| config.enable_phase_3e_triage = True |
| |
| if getattr(args, "no_realism_check", False): |
| config.enable_realism_check = False |
| if getattr(args, "no_dynamic_validation", False): |
| config.enable_dynamic_validation = False |
| if getattr(args, "no_flag_selection", False): |
| config.enable_flag_selection = False |
| if getattr(args, "no_feedback_loop", False): |
| config.enable_feedback_loop = False |
| if getattr(args, "no_spec_refiner", False): |
| config.enable_spec_refiner = False |
| if getattr(args, "no_inlining_advisor", False): |
| config.enable_inlining_advisor = False |
| if getattr(args, "no_spec_gen_tools", False): |
| config.enable_spec_gen_tools = False |
| if getattr(args, "no_realism_tools", False): |
| config.enable_realism_tools = False |
| if getattr(args, "no_phase_3e_triage", False): |
| config.enable_phase_3e_triage = False |
| if getattr(args, "minimal", False): |
| config.enable_realism_check = False |
| config.enable_dynamic_validation = False |
| config.enable_flag_selection = False |
| config.enable_feedback_loop = False |
| config.enable_spec_refiner = False |
| config.enable_inlining_advisor = False |
| config.enable_spec_gen_tools = False |
| config.enable_realism_tools = False |
| config.enable_phase_3e_triage = False |
| _apply_model_arg(config, args) |
| _apply_provider_args(config, args) |
|
|
| include_dirs = args.include_dir or [] |
| if include_dirs: |
| config.include_dirs = include_dirs |
| |
| |
| |
| if not config.cbmc_real_libc: |
| config.preprocess = True |
|
|
| domain_knowledge = _resolve_domain_knowledge(args.domain_knowledge) if args.domain_knowledge else "" |
|
|
| exclude = args.exclude or [] |
|
|
| print(f"Verifying directory: {args.source_dir}") |
| print(f"Driver prefix: {args.driver}") |
| print(f"Include dirs: {include_dirs or '(none)'}") |
| print(f"Artifact dir: {config.artifact_dir}") |
| if exclude: |
| print(f"Excluded patterns: {exclude}") |
|
|
| pipeline = AMCPipeline(config) |
| only_functions = None |
| _fns = getattr(args, "functions", "") or "" |
| if _fns.strip(): |
| only_functions = {f.strip() for f in _fns.split(",") if f.strip()} |
| print(f"Only functions: {sorted(only_functions)} (cross-file gen+refinement)") |
| results = pipeline.run_directory( |
| source_dir=args.source_dir, |
| driver_name=args.driver, |
| include_dirs=include_dirs, |
| domain_knowledge=domain_knowledge, |
| exclude_patterns=exclude, |
| only_functions=only_functions, |
| ) |
|
|
| |
| |
| |
| |
| |
| |
| |
| |
| def _is_unlikely(report) -> bool: |
| return (getattr(report, "confidence", "") or "").lower() == "unlikely" |
|
|
| filtered_results: dict = {} |
| suppressed_total = 0 |
| for fname, bugs in results.items(): |
| kept = [b for b in bugs if not _is_unlikely(b)] |
| filtered_results[fname] = kept |
| suppressed_total += len(bugs) - len(kept) |
|
|
| print(f"\n=== Summary ===") |
| total = sum(len(v) for v in filtered_results.values()) |
| print(f"Files processed: {len(results)}") |
| print(f"Total bugs confirmed: {total}") |
| if suppressed_total > 0: |
| print( |
| f"(suppressed {suppressed_total} finding(s) downgraded by realism " |
| f"check to 'unlikely' — see per-file bug_report.json for the audit trail)" |
| ) |
| for fname, bugs in sorted(filtered_results.items()): |
| if not bugs: |
| continue |
| print(f" {fname}: {len(bugs)} bug(s)") |
| for report in bugs: |
| print(f" [{report.bug_type.upper()}] {report.function_name} — {report.violated_property}") |
|
|
| |
| |
| |
| follow_n = int(getattr(args, "follow_adjacent_rounds", 0) or 0) |
| if follow_n > 0: |
| from pathlib import Path as _Path |
| from bmc_agent.adjacent_follower import follow_rounds |
| sweep_output = _Path(config.artifact_dir) / args.driver |
| source_dir = _Path(args.source_dir) |
| print(f"\n=== Adjacent-bug follow-up: up to {follow_n} round(s) ===") |
| rounds_out = follow_rounds( |
| source_dir=source_dir, |
| sweep_output=sweep_output, |
| config=config, |
| rounds=follow_n, |
| ) |
| for round_num, drivers in sorted(rounds_out.items()): |
| total = sum(len(bs) for bs in drivers.values()) |
| print(f" Round {round_num}: {len(drivers)} driver(s), {total} new bug(s)") |
| for drv, bs in sorted(drivers.items()): |
| if not bs: |
| continue |
| for r in bs: |
| print(f" [{r.bug_type.upper()}] {drv}/{r.function_name} — {r.violated_property}") |
|
|
| |
| |
| |
| |
| |
| |
| |
| try: |
| from bmc_agent.report_generator import generate_reports |
| rerun_cmd = ( |
| f"python -m bmc_agent.cli verify-dir --source-dir {args.source_dir} " |
| f"--driver {args.driver} --output <new_output> " |
| f"--exclude 'test_*' # (re-supply the include/defines/flags you used)" |
| ) |
| written = generate_reports( |
| sweep_output=config.artifact_dir, |
| driver=args.driver, |
| rerun_cmd=rerun_cmd, |
| ) |
| if written: |
| print(f"\n=== Per-bug reports: {len(written) - 1} finding(s) + index ===") |
| for p in written: |
| print(f" {p}") |
| else: |
| print("\n=== Per-bug reports: 0 realism-confirmed findings ===") |
| except Exception as exc: |
| print(f"\nReport generation failed: {exc}") |
|
|
| return 0 |
|
|
|
|
| def _cmd_self_patch_review(args: argparse.Namespace) -> int: |
| """Walk a sweep's proposed_patches/ dir and digest every staged proposal.""" |
| import json as _json |
| from pathlib import Path as _Path |
|
|
| root = _Path(args.proposals_dir) |
| if not root.exists(): |
| print(f"path not found: {root}", file=__import__("sys").stderr) |
| return 2 |
|
|
| meta_files = sorted(root.rglob("*.meta.json")) |
| if not meta_files: |
| print(f"No staged proposals found under {root}") |
| return 0 |
|
|
| print(f"=== Staged self-patch proposals: {root} ===\n") |
| print(f"Found {len(meta_files)} proposal(s)\n") |
|
|
| for mf in meta_files: |
| try: |
| with mf.open() as f: |
| meta = _json.load(f) |
| except Exception as exc: |
| print(f" ! failed to read {mf}: {exc}") |
| continue |
|
|
| diff_path = mf.with_suffix("").with_suffix(".diff") |
| test_path = mf.with_suffix("").with_suffix(".test.py") |
| |
| |
|
|
| round_dir = mf.parent.name |
| print(f"--- [{round_dir}] {mf.stem.replace('.meta', '')} ---") |
| print(f" Status: {meta.get('status')}") |
| print(f" Error class: {meta.get('error_class')}") |
| print(f" Error target: {meta.get('error_target') or '(none)'}") |
| print(f" Files touched: {meta.get('files_touched')}") |
| print(f" Lines changed: {meta.get('lines_changed')}") |
| rt_name = meta.get("regression_test_name", "(unknown)") |
| rt_path = meta.get("regression_test_path", "(unknown)") |
| print(f" Regression test: {rt_path}::{rt_name}") |
| rationale = (meta.get("rationale") or "").strip() |
| if rationale: |
| print(f" Rationale: {rationale}") |
| review = (meta.get("review_instructions") or "").strip() |
| if review: |
| print(" Manual apply:") |
| for line in review.splitlines(): |
| print(f" {line}") |
| if args.show_diff and diff_path.exists(): |
| print(f"\n Diff ({diff_path}):\n") |
| for line in diff_path.read_text().splitlines(): |
| print(f" {line}") |
| print() |
|
|
| return 0 |
|
|
|
|
| def _cmd_autonomous(args: argparse.Namespace) -> int: |
| """Phase 2 of autonomous mode: round-based verify-dir with convergence. |
| |
| Each round runs the full verify-dir pipeline with the autonomous-mode |
| defaults (lite_mode + realism + dynamic + Phase 2b auto-retry + |
| feedback loop). After each round, the loop computes a fingerprint |
| (coverage, total_bugs, total_errors, total_uncertain) and stops on: |
| |
| * coverage ≥ ``--target-coverage`` (default 0.80) |
| * fingerprint matches a previous round (fixed point) |
| * ``--max-rounds`` reached (default 3) |
| |
| Between rounds, knobs are adjusted based on the previous round's |
| output: |
| |
| * Many UNCERTAIN realism verdicts → enable |
| ``enable_realism_thinking`` for the next round. |
| * Many post-retry CBMC errors that all share the same identifier |
| → promote into ``session_strip_typedefs`` for the next round |
| (already done in-round by Phase 2b, but persisted across rounds |
| here so round-2 starts with round-1's wins). |
| |
| Per-round artifact: ``<output>/autonomous/round_<N>.json`` with the |
| summary, the strip-set deltas applied, and the convergence verdict. |
| """ |
| from bmc_agent.config import Config |
| from bmc_agent.pipeline import AMCPipeline |
| import json as _json |
| import time as _time |
| from pathlib import Path as _Path |
|
|
| config = Config.from_env() |
| if args.output: |
| config.artifact_dir = args.output |
|
|
| |
| |
| |
| config.lite_mode = True |
| config.enable_realism_check = True |
| config.enable_feedback_loop = True |
| if config.feedback_max_iters in (None, 3): |
| config.feedback_max_iters = 3 |
| if getattr(args, "enable_dynamic_validation", False): |
| config.enable_dynamic_validation = True |
| if getattr(args, "real_libc", False): |
| config.cbmc_real_libc = True |
| config.preprocess = False |
| if getattr(args, "raw_bytes", False): |
| config.raw_bytes = True |
| if getattr(args, "defines", None): |
| config.cbmc_defines = list(args.defines) |
| if getattr(args, "threat_model", None): |
| config.threat_model = args.threat_model |
| _apply_threat_model_context(config, args) |
| if getattr(args, "allow_self_patch", None): |
| config.allow_self_patch = args.allow_self_patch |
| _apply_model_arg(config, args) |
| _apply_provider_args(config, args) |
|
|
| include_dirs = args.include_dir or [] |
| if include_dirs: |
| config.include_dirs = include_dirs |
| if not config.cbmc_real_libc: |
| config.preprocess = True |
|
|
| domain_knowledge = _resolve_domain_knowledge(args.domain_knowledge) if args.domain_knowledge else "" |
| exclude = args.exclude or [] |
|
|
| max_rounds = int(args.max_rounds) |
| target_coverage = float(args.target_coverage) |
|
|
| print(f"=== AUTONOMOUS MODE ===") |
| print(f"Source dir: {args.source_dir}") |
| print(f"Driver prefix: {args.driver}") |
| print(f"Include dirs: {include_dirs or '(none)'}") |
| print(f"Artifact dir: {config.artifact_dir}") |
| print(f"Max rounds: {max_rounds}") |
| print(f"Target coverage: {target_coverage:.0%}") |
| print(f"Defaults: lite_mode=True, realism=True, feedback_loop=True,") |
| print(f" auto_retry_max_rounds={config.auto_retry_max_rounds}") |
| print() |
|
|
| autonomous_dir = _Path(config.artifact_dir) / "autonomous" |
| autonomous_dir.mkdir(parents=True, exist_ok=True) |
|
|
| round_summaries: list[dict] = [] |
| seen_fingerprints: set[tuple] = set() |
|
|
| for round_idx in range(max_rounds): |
| print(f"\n===== AUTONOMOUS ROUND {round_idx + 1} / {max_rounds} =====") |
| t0 = _time.time() |
|
|
| |
| |
| strip_typedefs_before = list(config.session_strip_typedefs) |
| strip_structs_before = list(config.session_strip_structs) |
| opaque_before = list(config.session_opaque_param_structs) |
|
|
| pipeline = AMCPipeline(config) |
| results = pipeline.run_directory( |
| source_dir=args.source_dir, |
| driver_name=args.driver, |
| include_dirs=include_dirs, |
| domain_knowledge=domain_knowledge, |
| exclude_patterns=exclude, |
| ) |
| elapsed = _time.time() - t0 |
|
|
| summary = _summarize_autonomous_round( |
| config=config, |
| args_driver=args.driver, |
| results=results, |
| elapsed_s=elapsed, |
| strip_typedefs_before=strip_typedefs_before, |
| strip_structs_before=strip_structs_before, |
| opaque_before=opaque_before, |
| ) |
| summary["round"] = round_idx + 1 |
| round_summaries.append(summary) |
|
|
| |
| (autonomous_dir / f"round_{round_idx + 1}.json").write_text( |
| _json.dumps(summary, indent=2) |
| ) |
|
|
| print(_format_round_summary(summary)) |
|
|
| fingerprint = ( |
| summary["total_files"], |
| summary["total_functions"], |
| summary["cbmc_verdicts"], |
| summary["cbmc_errors"], |
| summary["confirmed_bugs"], |
| ) |
| if summary["coverage"] >= target_coverage: |
| print( |
| f"\n✓ Converged: coverage {summary['coverage']:.1%} ≥ target " |
| f"{target_coverage:.0%}" |
| ) |
| break |
| if fingerprint in seen_fingerprints: |
| print( |
| f"\n✓ Converged: fixed-point fingerprint reached " |
| f"(no progress this round)" |
| ) |
| break |
| seen_fingerprints.add(fingerprint) |
|
|
| |
| next_knobs: list[str] = [] |
| if summary["uncertain_count"] > max(1, summary["confirmed_bugs"]) * 0.5: |
| if not config.enable_realism_thinking: |
| config.enable_realism_thinking = True |
| next_knobs.append("enable_realism_thinking=True") |
|
|
| |
| |
| |
| |
| from bmc_agent.realism_hint_injector import collect_hints, persist_hints |
| driver_root = _Path(config.artifact_dir) / args.driver |
| if driver_root.exists(): |
| hint_bundle = collect_hints(driver_root) |
| persist_hints(hint_bundle, autonomous_dir, round_idx) |
| if hint_bundle.text: |
| config.realism_extra_skepticism = hint_bundle.text |
| patterns = ", ".join( |
| f"{k}={v}" for k, v in hint_bundle.patterns_observed.items() |
| if v |
| ) |
| next_knobs.append(f"realism_extra_skepticism (patterns: {patterns})") |
|
|
| if next_knobs: |
| print(f" Adjusting for round {round_idx + 2}: {', '.join(next_knobs)}") |
| else: |
| print(f"\n× Stopped: max rounds ({max_rounds}) reached without convergence") |
|
|
| |
| summary_md = _format_autonomous_summary(round_summaries) |
| (autonomous_dir / "summary.md").write_text(summary_md) |
| print(f"\nAutonomous artifacts: {autonomous_dir}") |
|
|
| return 0 |
|
|
|
|
| def _summarize_autonomous_round( |
| config, |
| args_driver: str, |
| results: dict, |
| elapsed_s: float, |
| strip_typedefs_before: list, |
| strip_structs_before: list, |
| opaque_before: list, |
| ) -> dict: |
| """Build a one-round summary dict from the run_directory output. |
| |
| Reads per-file coverage_diagnostics.json (written by Phase 2b) and |
| classification.json files (written by Phase 3) to compute aggregate |
| counts. Pure file-scan; never re-runs CBMC. |
| """ |
| import json as _json |
| from pathlib import Path as _Path |
|
|
| artifact_dir = _Path(config.artifact_dir) |
| driver_root = artifact_dir / args_driver |
|
|
| total_runs = 0 |
| total_verdicts = 0 |
| total_errors = 0 |
| files_with_verdicts = 0 |
| files_all_errored = 0 |
| for cov in driver_root.rglob("coverage_diagnostics.json"): |
| try: |
| with cov.open() as f: |
| d = _json.load(f) |
| runs = int(d.get("total_cbmc_runs", 0)) |
| verd = int(d.get("produced_verdict", 0)) |
| fail = int(d.get("failed_before_verdict", 0)) |
| total_runs += runs |
| total_verdicts += verd |
| total_errors += fail |
| if runs and fail == runs: |
| files_all_errored += 1 |
| elif runs: |
| files_with_verdicts += 1 |
| except Exception: |
| pass |
|
|
| |
| outcome_counts: dict[str, int] = {} |
| realism_counts: dict[str, int] = {} |
| for cls in driver_root.rglob("classification.json"): |
| try: |
| with cls.open() as f: |
| cd = _json.load(f) |
| c = cd.get("classification") or {} |
| outcome_counts[c.get("outcome", "unknown")] = outcome_counts.get(c.get("outcome", "unknown"), 0) + 1 |
| except Exception: |
| pass |
| for br in driver_root.rglob("bug_report.json"): |
| try: |
| with br.open() as f: |
| bd = _json.load(f) |
| rc = bd.get("realism_check") or {} |
| v = (rc.get("verdict") if isinstance(rc, dict) else None) or "n/a" |
| realism_counts[v] = realism_counts.get(v, 0) + 1 |
| except Exception: |
| pass |
|
|
| confirmed_bugs = sum(len(b) for b in results.values()) |
| coverage = (total_verdicts / total_runs) if total_runs else 0.0 |
|
|
| return { |
| "elapsed_s": round(elapsed_s, 1), |
| "total_files": len(results), |
| "total_functions": total_runs, |
| "cbmc_verdicts": total_verdicts, |
| "cbmc_errors": total_errors, |
| "coverage": coverage, |
| "files_with_verdicts": files_with_verdicts, |
| "files_all_errored": files_all_errored, |
| "outcome_counts": outcome_counts, |
| "realism_counts": realism_counts, |
| "uncertain_count": int(realism_counts.get("UNCERTAIN", 0)), |
| "unrealistic_count": int(realism_counts.get("UNREALISTIC", 0)), |
| "realistic_count": int(realism_counts.get("REALISTIC", 0)), |
| "confirmed_bugs": confirmed_bugs, |
| "session_strip_typedefs_added": [ |
| t for t in config.session_strip_typedefs |
| if t not in strip_typedefs_before |
| ], |
| "session_strip_structs_added": [ |
| s for s in config.session_strip_structs |
| if s not in strip_structs_before |
| ], |
| "session_opaque_param_structs_added": [ |
| o for o in config.session_opaque_param_structs |
| if o not in opaque_before |
| ], |
| } |
|
|
|
|
| def _format_round_summary(s: dict) -> str: |
| """One-screen round summary for stdout.""" |
| lines = [] |
| lines.append(f" Elapsed: {s['elapsed_s']:.1f}s") |
| lines.append(f" Files: {s['total_files']} ({s['files_with_verdicts']} with verdicts, {s['files_all_errored']} all-errored)") |
| lines.append(f" Functions: {s['total_functions']}") |
| lines.append(f" CBMC verdicts: {s['cbmc_verdicts']}, errors: {s['cbmc_errors']}, coverage: {s['coverage']:.1%}") |
| lines.append(f" Phase 3 outcomes: {s['outcome_counts']}") |
| lines.append(f" Realism: REALISTIC={s['realistic_count']}, UNCERTAIN={s['uncertain_count']}, UNREALISTIC={s['unrealistic_count']}") |
| lines.append(f" Confirmed bugs (post-realism): {s['confirmed_bugs']}") |
| if s.get("session_strip_typedefs_added"): |
| lines.append(f" Auto-retry added typedefs: {s['session_strip_typedefs_added']}") |
| if s.get("session_strip_structs_added"): |
| lines.append(f" Auto-retry added structs: {s['session_strip_structs_added']}") |
| if s.get("session_opaque_param_structs_added"): |
| lines.append(f" Auto-retry forced opaque: {s['session_opaque_param_structs_added']}") |
| return "\n".join(lines) |
|
|
|
|
| def _format_autonomous_summary(rounds: list[dict]) -> str: |
| """Markdown summary across all rounds, written to summary.md.""" |
| lines = ["# Autonomous-mode sweep summary", ""] |
| lines.append(f"Rounds run: {len(rounds)}") |
| if not rounds: |
| return "\n".join(lines) |
| last = rounds[-1] |
| lines.append(f"Final coverage: {last['coverage']:.1%}") |
| lines.append(f"Final confirmed bugs: {last['confirmed_bugs']}") |
| lines.append("") |
| lines.append("| Round | Elapsed | Files | Functions | Verdicts | Errors | Coverage | Confirmed | UNCERTAIN |") |
| lines.append("|---:|---:|---:|---:|---:|---:|---:|---:|---:|") |
| for r in rounds: |
| lines.append( |
| f"| {r['round']} | {r['elapsed_s']:.1f}s | {r['total_files']} | " |
| f"{r['total_functions']} | {r['cbmc_verdicts']} | {r['cbmc_errors']} | " |
| f"{r['coverage']:.1%} | {r['confirmed_bugs']} | {r['uncertain_count']} |" |
| ) |
| lines.append("") |
| |
| promoted_typedefs: list[str] = [] |
| promoted_structs: list[str] = [] |
| promoted_opaque: list[str] = [] |
| for r in rounds: |
| promoted_typedefs.extend(r.get("session_strip_typedefs_added", [])) |
| promoted_structs.extend(r.get("session_strip_structs_added", [])) |
| promoted_opaque.extend(r.get("session_opaque_param_structs_added", [])) |
| if promoted_typedefs or promoted_structs or promoted_opaque: |
| lines.append("## Auto-retry promotion candidates") |
| lines.append("") |
| lines.append("Review and consider adding to the static sets in `harness_generator.py`:") |
| lines.append("") |
| if promoted_typedefs: |
| lines.append("- Typedefs added to session strip set: " + ", ".join(sorted(set(promoted_typedefs)))) |
| if promoted_structs: |
| lines.append("- Structs added to session strip set: " + ", ".join(sorted(set(promoted_structs)))) |
| if promoted_opaque: |
| lines.append("- Structs forced opaque: " + ", ".join(sorted(set(promoted_opaque)))) |
| return "\n".join(lines) |
|
|
|
|
| def build_parser() -> argparse.ArgumentParser: |
| parser = argparse.ArgumentParser( |
| prog="bmc-agent", |
| description="BMC-Agent: Agentic Model Checking for C programs (part of AProver)", |
| ) |
| subparsers = parser.add_subparsers(dest="command", metavar="COMMAND") |
| subparsers.required = True |
|
|
| |
| def _add_model_arg(p: argparse.ArgumentParser) -> None: |
| p.add_argument( |
| "--model", |
| default="", |
| metavar="MODEL_ID", |
| help=( |
| "Override the LLM model (e.g. claude-opus-4-7, claude-sonnet-4-6). " |
| "Defaults to BMC_AGENT_LLM_MODEL env var or claude-sonnet-4-6." |
| ), |
| ) |
|
|
| |
| def _add_provider_args(p: argparse.ArgumentParser) -> None: |
| p.add_argument( |
| "--agentic", |
| action="store_true", |
| default=False, |
| dest="agentic", |
| help=( |
| "GENERAL agentic stack: make EVERY LLM agent role (spec-gen, " |
| "refinement, realism, triage, disagreement, …) an investigating " |
| "agent and enable the soundness gate + agentic harness-repair + " |
| "split spec-gen + component gating — but DO NOT force any backend. " |
| "Each role is instantiated by whatever its routing says: a per-role " |
| "BMC_AGENT_LLM_<ROLE>_PROVIDER/_MODEL override, else the global " |
| "default (--provider / BMC_AGENT_LLM_DEFAULT_*), else the " |
| "auto-resolved provider — so roles may be a mix of API / " |
| "claude-code / codex / etc. The conventional core (CBMC, harness " |
| "translation, compile+run) is unaffected. Use --agentic-claude-code " |
| "to force every role onto the local Claude Code CLI." |
| ), |
| ) |
| p.add_argument( |
| "--agentic-claude-code", |
| action="store_true", |
| default=False, |
| dest="agentic_claude_code", |
| help=( |
| "Like --agentic, but FORCE every agent role onto the local Claude " |
| "Code CLI provider (read-only code-exploration tools, your `claude` " |
| "login, no API key). This was the original --agentic behaviour. A " |
| "per-role BMC_AGENT_LLM_<ROLE>_PROVIDER override still wins, so an " |
| "individual agent can be repointed to an API/codex backend. NOTE: " |
| "claude-code is a serial subprocess — slow for high-volume roles." |
| ), |
| ) |
| p.add_argument( |
| "--agentic-refine", |
| action="store_true", |
| default=False, |
| dest="agentic_refine", |
| help=( |
| "LEAN agentic: route ONLY refinement (+ its soundness guard) to " |
| "the Claude Code CLI with tools, and enable the guard / " |
| "harness-repair / split-spec-gen — but keep SPEC GENERATION on " |
| "the fast default provider. Recommended for batch runs (avoids " |
| "slow per-function agentic spec-gen)." |
| ), |
| ) |
| p.add_argument( |
| "--provider", |
| default="", |
| choices=["", "anthropic", "openai", "claude-code"], |
| metavar="PROVIDER", |
| help=( |
| "LLM provider for all roles (default: auto-detect / env). " |
| "'claude-code' shells out to the local Claude Code CLI, reusing " |
| "your existing login — no API key required." |
| ), |
| ) |
| p.add_argument( |
| "--specs-via-claude-code", |
| action="store_true", |
| default=False, |
| dest="specs_via_claude_code", |
| help=( |
| "Route ONLY spec generation + refinement to the Claude Code CLI " |
| "(reuses your Claude Code login; no API key). Every other role " |
| "keeps the global/default provider." |
| ), |
| ) |
| p.add_argument( |
| "--claude-code-agentic", |
| action="store_true", |
| default=False, |
| dest="claude_code_agentic", |
| help=( |
| "When the claude-code provider is active, grant it read-only " |
| "tools (Read/Grep/Glob) so it can explore the source tree while " |
| "drafting/refining specs, instead of a one-shot text completion." |
| ), |
| ) |
|
|
| |
| gen = subparsers.add_parser( |
| "generate", |
| help="Generate specs for all functions in a C source file (Phase 1)", |
| ) |
| gen.add_argument("--source", required=True, help="Path to a C (.c/.h) or Rust (.rs) source file") |
| gen.add_argument("--driver", required=True, help="Driver name (used for artifact storage)") |
| gen.add_argument("--output", default="artifacts", help="Artifact output directory") |
| gen.add_argument( |
| "--domain-knowledge", |
| default="", |
| metavar="TEXT_OR_FILE", |
| help="Domain knowledge string or path to a file containing domain knowledge", |
| ) |
| gen.add_argument( |
| "--include-dir", |
| action="append", |
| default=[], |
| metavar="DIR", |
| help="Add an include directory for C preprocessing (repeatable).", |
| ) |
| gen.add_argument( |
| "-D", "--define", |
| action="append", |
| default=[], |
| dest="defines", |
| help="Pass a preprocessor define (repeatable), e.g. -D HAVE_CONFIG_H.", |
| ) |
| _add_model_arg(gen) |
| _add_provider_args(gen) |
| gen.set_defaults(func=_cmd_generate) |
|
|
| |
| chk = subparsers.add_parser( |
| "check", |
| help="Run BMC on previously generated specs (Phase 2)", |
| ) |
| chk.add_argument("--source", required=True, help="Path to a C (.c/.h) or Rust (.rs) source file") |
| chk.add_argument("--driver", required=True, help="Driver name") |
| chk.add_argument("--output", default="artifacts", help="Artifact directory") |
| chk.add_argument("--function", default="", help="Specific function to check (optional)") |
| chk.add_argument( |
| "--include-dir", |
| action="append", |
| default=[], |
| metavar="DIR", |
| help="Add an include directory for C preprocessing (repeatable). Required when " |
| "the harness pulls in build-config headers (e.g. config.h).", |
| ) |
| chk.add_argument( |
| "-D", "--define", |
| action="append", |
| default=[], |
| dest="defines", |
| help="Pass a preprocessor define to CBMC (repeatable), e.g. -D HAVE_CONFIG_H.", |
| ) |
| chk.set_defaults(func=_cmd_check) |
|
|
| |
| ver = subparsers.add_parser( |
| "verify", |
| help="Run full pipeline: generate + check + validate (Phase 3)", |
| ) |
| ver.add_argument("--source", required=True, help="Path to a C (.c/.h) or Rust (.rs) source file") |
| ver.add_argument("--driver", required=True, help="Driver name") |
| ver.add_argument("--output", default="artifacts", help="Artifact directory") |
| ver.add_argument( |
| "--domain-knowledge", |
| default="", |
| metavar="TEXT_OR_FILE", |
| help="Domain knowledge string or path to a file containing domain knowledge", |
| ) |
| ver.add_argument( |
| "--include-dir", |
| action="append", |
| default=[], |
| metavar="DIR", |
| help="Add an include directory for C preprocessing (repeatable)", |
| ) |
| ver.add_argument( |
| "--skip-refinement", |
| action="store_true", |
| default=False, |
| help="FilteringOnly mode: classify counterexamples but skip spec update and caller re-queue (RQ3 ablation)", |
| ) |
| ver.add_argument( |
| "--enable-dynamic-validation", |
| action="store_true", |
| default=False, |
| help="Stage 3: compile and run a GCC harness to confirm bugs at runtime (confirmed_dynamic tier)", |
| ) |
| ver.add_argument( |
| "--enable-realism-check", |
| action="store_true", |
| default=False, |
| help="Run LLM realism audit on every REAL_BUG finding to reduce false positives", |
| ) |
| ver.add_argument( |
| "--enable-realism-thinking", |
| action="store_true", |
| default=False, |
| help="Use extended thinking in the realism checker (higher quality, slower, implies --enable-realism-check)", |
| ) |
| ver.add_argument( |
| "--enable-flag-selection", |
| action="store_true", |
| default=False, |
| help="Phase 1.5: LLM selects per-function CBMC flags (unsigned/signed overflow, conversion, pointer overflow)", |
| ) |
| ver.add_argument( |
| "--enable-feedback-loop", |
| action="store_true", |
| default=False, |
| help="Distill UNREALISTIC realism rejections into learned constraints (function-spec or project invariant) " |
| "or code-change TODOs. Persists to <output>/learned_constraints.json so subsequent sweeps stop " |
| "re-producing the same artifact pattern.", |
| ) |
| ver.add_argument( |
| "--feedback-max-iters", |
| type=int, |
| default=None, |
| help="In-sweep convergence: after distilling a clause, re-run CBMC on the same function up to N times " |
| "until the function verifies clean, a REALISTIC verdict emerges, or the same CE class repeats. " |
| "Default 3 (set via Config.feedback_max_iters).", |
| ) |
| ver.add_argument( |
| "--real-libc", |
| action="store_true", |
| default=False, |
| help="Real-libc mode: harness #includes the source .c file and lets CBMC do all preprocessing via -I. Required for real-world glibc-using OSS (jq, curl, OpenSSL, …); leave off for bare-metal targets like VibeOS.", |
| ) |
| ver.add_argument( |
| "--strict-dsl", |
| action="store_true", |
| default=False, |
| help="Strict-formal Phase 1 prompts: pre/post must be a single C boolean expression (no natural language). Required for bounty/CVE work — prose-mixed specs translate to comments and produce vacuous verifications.", |
| ) |
| ver.add_argument( |
| "--raw-bytes", |
| action="store_true", |
| default=False, |
| help="Treat single char* / const char* params as raw byte buffers (no NUL termination) in the harness. Required for wire-format parsers (protobuf upb, length-prefixed blobs) that read N raw bytes regardless of NULs.", |
| ) |
| ver.add_argument( |
| "-D", "--define", |
| action="append", |
| default=[], |
| dest="defines", |
| help="Pass a preprocessor define to CBMC (repeatable). Use NAME or NAME=VALUE form, e.g. -D HAVE_CONFIG_H -D BUILDING_LIBCURL. Required for build-config-driven C codebases (curl, OpenSSL) where headers gate on autoconf-style flags.", |
| ) |
| ver.add_argument( |
| "--standalone", |
| action="store_true", |
| default=False, |
| help="Whole-program mode: verify the program AS WRITTEN from its real entry point (no per-function harness synthesis, no nondet injection). Answers 'is THIS program safe?' Loops with concrete bounds unwind fully; //@ assert annotations are checked. Runs CBMC directly with the full memory-safety + overflow check set.", |
| ) |
| ver.add_argument( |
| "--entry", |
| default="main", |
| help="Entry function for --standalone / --specs-from-asserts mode (default: main).", |
| ) |
| ver.add_argument( |
| "--specs-from-asserts", |
| action="store_true", |
| default=False, |
| help="Assertion-driven spec synthesis: treat the program's //@ assert clauses as the goal and refine function postconditions until every assert is provable AND sound (implied by the body). Reports the synthesized contracts; flags any assert no sound spec can satisfy (i.e. genuinely false).", |
| ) |
| ver.add_argument( |
| "--synth-loop-invariants", |
| action="store_true", |
| default=False, |
| help="Specification-synthesis mode: synthesize LOOP INVARIANTS (and render them in ACSL) that are inductive AND sufficient to prove the program's verification goals (assert / static_assert / __VERIFIER_assert / //@ assert). Reuses the gen+refine engine; CBMC validates each invariant per-iteration (Local Validity) and proves the goals (Global Adequacy) for unwindable loops.", |
| ) |
| ver.add_argument( |
| "--specs-bench", |
| action="store_true", |
| default=False, |
| help="Specification-synthesis BENCHMARK preset (one flag). Reads the goals (assert/static_assert/__VERIFIER_assert///@ assert), dispatches by program content — loops → loop-invariant synthesis, otherwise → function-contract synthesis — turns on --math-ints (mathematical-integer semantics these benchmarks assume), and emits ACSL. Equivalent to picking the right synthesis mode + --math-ints automatically.", |
| ) |
| ver.add_argument( |
| "--math-ints", |
| action="store_true", |
| default=False, |
| help="Loop-invariant synthesis (unbounded loops): assume the loop body's signed arithmetic does not overflow (mathematical-integer semantics, as IC3-style benchmarks and Frama-C/WP assume), so invariants like x>=1 under x=x+y are inductive. Off => machine-int (wrapping) semantics.", |
| ) |
| ver.add_argument( |
| "--no-overflow-rigor", |
| dest="overflow_rigor", |
| action="store_false", |
| default=True, |
| help="Disable the verification-gated overflow-rigor pass (Frama-C oracle, contract synthesis). On by default: even under --math-ints the synthesized contract is upgraded to machine-int soundness by enumerating every signed-overflow site in the body, bounding it INT_MIN<=e<=INT_MAX, and re-verifying with RTE on — adopted ONLY if WP still discharges every goal (additive; never turns a pass into a failure). Pass this to keep the PURE mathematical-integer contract (no synthesized no-overflow precondition), e.g. for exact-match against an IC3-style benchmark's golden math-int spec.", |
| ) |
| ver.add_argument( |
| "--oracle", |
| choices=["cbmc", "frama-c"], |
| default=None, |
| help="Verification oracle for spec synthesis. Unset: 'cbmc' everywhere EXCEPT --specs-bench, which auto-prefers 'frama-c' when frama-c is on PATH (the correct oracle for specification benchmarks: native ACSL + mathematical integers + unbounded/aggregate goals) and falls back to 'cbmc' otherwise. 'cbmc': bounded model checking — unwinds bounded loops, machine integers. 'frama-c': Frama-C/WP deductive verification — consumes the synthesized ACSL loop invariants/contracts natively, mathematical integers, discharges base+preservation+goal for UNBOUNDED loops and aggregate (\\sum) invariants CBMC can't. Requires frama-c + an SMT prover (e.g. alt-ergo) on PATH. An explicit value always wins.", |
| ) |
| ver.add_argument( |
| "--standalone-unwind", |
| type=int, |
| default=0, |
| help="Loop-unwinding bound for --standalone / --synth-loop-invariants modes. 0 (default) means: --standalone uses 64; --synth-loop-invariants auto-derives bound+2 from a literal loop bound. With --unwinding-assertions on, an undersized bound is reported, not silently assumed.", |
| ) |
| ver.add_argument( |
| "--threat-model", |
| choices=["security", "safety", "functional"], |
| default="security", |
| help="Threat model: shapes CBMC baseline flags, spec prompts, and realism context (default: security)", |
| ) |
| ver.add_argument( |
| "--threat-model-context", |
| default=None, |
| metavar="PATH_OR_TEXT", |
| help="Trust-boundary note for THIS target (path to a file, or inline text): which inputs are attacker-controlled vs. caller/hardware-guaranteed. Injected into spec-gen, refinement, classifier, dynamic-validation and realism so the precondition is shaped correctly at generation time. Conservative default (treat inputs as attacker-controlled) applies when omitted.", |
| ) |
| ver.add_argument( |
| "--lite-mode", |
| action="store_true", |
| default=False, |
| help=( |
| "bmc-agent-lite: skip the LLM spec_gen call for every function " |
| "(every function gets a permissive pre=post=true spec) and also " |
| "skip Pass 1.5 domain-knowledge extraction. CBMC's built-in checks " |
| "(--bounds-check / --pointer-check / --signed-overflow-check) " |
| "surface memory-safety bugs directly from nondet harness inputs. " |
| "LLM budget shifts to realism + classifier in Phase 3, where the " |
| "LLM adds real signal rather than parroting the function body. " |
| "Pairs well with --raw-bytes." |
| ), |
| ) |
| ver.add_argument( |
| "--legacy-spec-gen", |
| action="store_true", |
| default=False, |
| help=( |
| "Use the legacy v1 SpecGenerator instead of the default v2 " |
| "(caller-grounded, evidence-tagged). v1 drafts from the function " |
| "body alone; v2 reconciles body + observed call sites + doc " |
| "annotations + signature patterns. Use this flag only for parity " |
| "comparison against historical runs — v2 should otherwise be " |
| "strictly better on internal functions." |
| ), |
| ) |
| ver.add_argument( |
| "--enable-spec-refiner", |
| action="store_true", |
| default=False, |
| help=( |
| "Enable realism-feedback-driven in-sweep spec refinement. When " |
| "realism rejects a CEx with verdict=UNREALISTIC + concrete " |
| "key_concern, spec_refiner asks the LLM for the precise clause " |
| "that would exclude the rejected CEx, re-runs BMC, and applies " |
| "the soundness acceptance check (targeted CEx gone AND no " |
| "previously-realistic CEx silently dropped). Opt-in." |
| ), |
| ) |
| ver.add_argument( |
| "--enable-inlining-advisor", |
| action="store_true", |
| default=False, |
| help=( |
| "Enable LLM-driven inline-vs-stub decisions for callees the " |
| "mechanical rule (file-local static, ≤30 LoC, no loops/alloc/" |
| "recursion) marked STUB. The advisor reconsiders them per-caller " |
| "in a batched LLM call; may PROMOTE small predicates / getters / " |
| "accessors to inline when stubbing would produce stub-disconnect " |
| "FPs. Bounded — never demotes; default STUB on uncertainty. " |
| "Default ON; pass --no-inlining-advisor to disable." |
| ), |
| ) |
| |
| |
| |
| |
| |
| ver.add_argument("--no-realism-check", action="store_true", default=False, |
| help="Disable the LLM realism filter on CExs.") |
| ver.add_argument("--no-dynamic-validation", action="store_true", default=False, |
| help="Disable building + running the GCC reproducer.") |
| ver.add_argument("--no-flag-selection", action="store_true", default=False, |
| help="Disable per-function CBMC flag selection.") |
| ver.add_argument("--no-feedback-loop", action="store_true", default=False, |
| help="Disable in-sweep realism-driven feedback loop.") |
| ver.add_argument("--no-spec-refiner", action="store_true", default=False, |
| help="Disable in-sweep realism-feedback-driven spec refiner.") |
| ver.add_argument("--enable-soundness-gate", action="store_true", default=False, |
| dest="enable_soundness_gate", |
| help="Caller-grounded soundness gate on refinement: block a " |
| "refiner clause that isn't caller-guaranteed (keeps the CEx " |
| "as a real-bug lead instead of assuming it away). Best with " |
| "--specs-via-claude-code --claude-code-agentic.") |
| ver.add_argument("--enable-agentic-harness-repair", action="store_true", default=False, |
| dest="enable_agentic_harness_repair", |
| help="On a CBMC harness BUILD error (conversion / incomplete-type / " |
| "parse), rebuild the harness with the agentic code-reading " |
| "generator and re-run. Fires only on build errors.") |
| ver.add_argument("--enable-classifier", action="store_true", default=False, |
| dest="enable_classifier", |
| help="Force the CEx classifier ON (REAL/SPURIOUS/UNRESOLVED + the " |
| "spurious->refinement->soundness-gate loop). On by default, " |
| "including under --agentic; this overrides " |
| "BMC_AGENT_ENABLE_CLASSIFIER=false.") |
| ver.add_argument("--enable-triage", action="store_true", default=False, |
| dest="enable_triage", |
| help="Re-enable Phase-3e triage of UNRESOLVED counterexamples " |
| "(independent of classifier/realism).") |
| ver.add_argument("--no-inlining-advisor", action="store_true", default=False, |
| help="Disable LLM inline-vs-stub advisor.") |
| ver.add_argument("--no-spec-gen-tools", action="store_true", default=False, |
| help="Disable v2.2 spec_gen bounded tool-use branch.") |
| ver.add_argument("--no-realism-tools", action="store_true", default=False, |
| help="Disable realism check's bounded tool-use augmentation.") |
| ver.add_argument("--minimal", action="store_true", default=False, |
| help=("Turn ALL default-on AI layers off (realism, " |
| "dyn-val, flag-selection, feedback-loop, spec-refiner, " |
| "inlining-advisor, spec-gen-tools). Equivalent to " |
| "passing every --no-* individually. For " |
| "zero-LLM-cost smoke runs.")) |
| _add_model_arg(ver) |
| _add_provider_args(ver) |
| ver.set_defaults(func=_cmd_verify) |
|
|
| |
| bl = subparsers.add_parser( |
| "baseline", |
| help="Run CBMC-alone baseline on a C source file (no LLM, no spec generation)", |
| ) |
| bl.add_argument("--source", required=True, help="Path to a C (.c/.h) or Rust (.rs) source file") |
| bl.add_argument("--driver", required=True, help="Driver name (used for artifact storage)") |
| bl.add_argument("--output", default="artifacts", help="Artifact output directory") |
| bl.set_defaults(func=_cmd_baseline) |
|
|
| |
| ab = subparsers.add_parser( |
| "ablation-baseline", |
| help="Run AMC-ablation baseline: bottom-up spec generation without caller context", |
| ) |
| ab.add_argument("--source", required=True, help="Path to a C (.c/.h) or Rust (.rs) source file") |
| ab.add_argument("--driver", required=True, help="Driver name (used for artifact storage)") |
| ab.add_argument("--output", default="artifacts", help="Artifact output directory") |
| _add_model_arg(ab) |
| _add_provider_args(ab) |
| ab.set_defaults(func=_cmd_ablation_baseline) |
|
|
| |
| vd = subparsers.add_parser( |
| "verify-dir", |
| help="Run full pipeline on every .c file in a directory", |
| ) |
| vd.add_argument("--source-dir", required=True, help="Directory containing .c files") |
| vd.add_argument("--driver", required=True, help="Driver name prefix") |
| vd.add_argument("--output", default="artifacts", help="Artifact directory") |
| vd.add_argument( |
| "--functions", default="", |
| help="Comma-separated function names: build the cross-file call graph over the " |
| "whole dir but VERIFY only these functions (coaudit audit-flagged path with " |
| "full cross-file spec gen + refinement). Empty = verify all.", |
| ) |
| vd.add_argument( |
| "--include-dir", |
| action="append", |
| default=[], |
| metavar="DIR", |
| help="Add an include directory for C preprocessing (repeatable)", |
| ) |
| vd.add_argument( |
| "--domain-knowledge", |
| default="", |
| metavar="TEXT_OR_FILE", |
| help="Domain knowledge string or path to a file", |
| ) |
| vd.add_argument( |
| "--exclude", |
| action="append", |
| default=[], |
| metavar="PATTERN", |
| help="Glob pattern of filenames to skip (repeatable)", |
| ) |
| vd.add_argument( |
| "--skip-refinement", |
| action="store_true", |
| default=False, |
| help="FilteringOnly mode: classify counterexamples but skip spec update and caller re-queue (RQ3 ablation)", |
| ) |
| vd.add_argument( |
| "--enable-dynamic-validation", |
| action="store_true", |
| default=False, |
| help="Stage 3: compile and run a GCC harness to confirm bugs at runtime (confirmed_dynamic tier)", |
| ) |
| vd.add_argument( |
| "--enable-realism-check", |
| action="store_true", |
| default=False, |
| help="Run LLM realism audit on every REAL_BUG finding to reduce false positives", |
| ) |
| vd.add_argument( |
| "--enable-realism-thinking", |
| action="store_true", |
| default=False, |
| help="Use extended thinking in the realism checker (higher quality, slower)", |
| ) |
| vd.add_argument( |
| "--enable-flag-selection", |
| action="store_true", |
| default=False, |
| help="Phase 1.5: LLM selects per-function CBMC flags (unsigned/signed overflow, conversion, pointer overflow)", |
| ) |
| vd.add_argument( |
| "--enable-feedback-loop", |
| action="store_true", |
| default=False, |
| help="Distill UNREALISTIC realism rejections into learned constraints or code-change TODOs. " |
| "Persists to <output>/learned_constraints.json so subsequent sweeps stop re-producing " |
| "the same artifact pattern.", |
| ) |
| vd.add_argument( |
| "--feedback-max-iters", |
| type=int, |
| default=None, |
| help="In-sweep convergence: after distilling a clause, re-run CBMC on the same function up to N times " |
| "until the function verifies clean, a REALISTIC verdict emerges, or the same CE class repeats. " |
| "Default 3.", |
| ) |
| vd.add_argument( |
| "--real-libc", |
| action="store_true", |
| default=False, |
| help="Real-libc mode: harness #includes the source .c file and lets CBMC do all preprocessing via -I. Required for real-world glibc-using OSS.", |
| ) |
| vd.add_argument( |
| "--strict-dsl", |
| action="store_true", |
| default=False, |
| help="Strict-formal Phase 1 prompts: pre/post must be a single C boolean expression. Required for bounty/CVE work.", |
| ) |
| vd.add_argument( |
| "--raw-bytes", |
| action="store_true", |
| default=False, |
| help="Treat single char* / const char* params as raw byte buffers (no NUL termination). Required for wire-format parsers.", |
| ) |
| vd.add_argument( |
| "-D", "--define", |
| action="append", |
| default=[], |
| dest="defines", |
| help="Pass a preprocessor define to CBMC (repeatable). Use NAME or NAME=VALUE. Required for build-config-driven C codebases.", |
| ) |
| vd.add_argument( |
| "--threat-model", |
| choices=["security", "safety", "functional"], |
| default="security", |
| help="Threat model: shapes CBMC baseline flags, spec prompts, and realism context (default: security)", |
| ) |
| vd.add_argument( |
| "--threat-model-context", |
| default=None, |
| metavar="PATH_OR_TEXT", |
| help="Trust-boundary note for THIS target (path to a file, or inline text): which inputs are attacker-controlled vs. caller/hardware-guaranteed. Injected into spec-gen, refinement, classifier, dynamic-validation and realism so the precondition is shaped correctly at generation time. Conservative default (treat inputs as attacker-controlled) applies when omitted.", |
| ) |
| vd.add_argument( |
| "--lite-mode", |
| action="store_true", |
| default=False, |
| help=( |
| "bmc-agent-lite: skip the LLM spec_gen call for every function " |
| "(permissive pre=post=true spec) and skip Pass 1.5 domain extraction. " |
| "CBMC built-in checks surface memory-safety bugs from nondet harness " |
| "inputs; LLM budget shifts to realism + classifier in Phase 3. " |
| "Pairs well with --raw-bytes." |
| ), |
| ) |
| vd.add_argument( |
| "--legacy-spec-gen", |
| action="store_true", |
| default=False, |
| help=( |
| "Use the legacy v1 SpecGenerator instead of the default v2 " |
| "(caller-grounded, evidence-tagged). See `verify --help` for the " |
| "full explanation. Use only for parity comparison." |
| ), |
| ) |
| vd.add_argument( |
| "--enable-spec-refiner", |
| action="store_true", |
| default=False, |
| help="See `verify --help` for the full explanation. Opt-in.", |
| ) |
| vd.add_argument( |
| "--enable-inlining-advisor", |
| action="store_true", |
| default=False, |
| help="Default ON; pass --no-inlining-advisor to disable.", |
| ) |
| vd.add_argument( |
| "--enable-phase-3e-triage", |
| action="store_true", |
| default=False, |
| help=( |
| "Phase 3e: in-pipeline TriageToolsAgent oracle on UNRESOLVED " |
| "counterexamples. Promotes REAL_BUG/high verdicts to bug " |
| "reports and writes per-CEx triage.json sidecars matching " |
| "scripts/triage_unresolved.py. Default OFF (expensive)." |
| ), |
| ) |
| |
| vd.add_argument("--no-realism-check", action="store_true", default=False, |
| help="Disable the LLM realism filter on CExs.") |
| vd.add_argument("--no-dynamic-validation", action="store_true", default=False, |
| help="Disable building + running the GCC reproducer.") |
| vd.add_argument("--no-flag-selection", action="store_true", default=False, |
| help="Disable per-function CBMC flag selection.") |
| vd.add_argument("--no-feedback-loop", action="store_true", default=False, |
| help="Disable in-sweep realism-driven feedback loop.") |
| vd.add_argument("--no-spec-refiner", action="store_true", default=False, |
| help="Disable in-sweep realism-feedback-driven spec refiner.") |
| vd.add_argument("--enable-soundness-gate", action="store_true", default=False, |
| dest="enable_soundness_gate", |
| help="Caller-grounded soundness gate on refinement: block a " |
| "refiner clause that isn't caller-guaranteed (keeps the CEx " |
| "as a real-bug lead instead of assuming it away). Best with " |
| "--specs-via-claude-code --claude-code-agentic.") |
| vd.add_argument("--enable-agentic-harness-repair", action="store_true", default=False, |
| dest="enable_agentic_harness_repair", |
| help="On a CBMC harness BUILD error (conversion / incomplete-type / " |
| "parse), rebuild the harness with the agentic code-reading " |
| "generator and re-run. Fires only on build errors.") |
| vd.add_argument("--enable-classifier", action="store_true", default=False, |
| dest="enable_classifier", |
| help="Force the CEx classifier ON (REAL/SPURIOUS/UNRESOLVED + the " |
| "spurious->refinement->soundness-gate loop). On by default, " |
| "including under --agentic; this overrides " |
| "BMC_AGENT_ENABLE_CLASSIFIER=false.") |
| vd.add_argument("--enable-triage", action="store_true", default=False, |
| dest="enable_triage", |
| help="Re-enable Phase-3e triage of UNRESOLVED counterexamples " |
| "(independent of classifier/realism).") |
| vd.add_argument("--no-inlining-advisor", action="store_true", default=False, |
| help="Disable LLM inline-vs-stub advisor.") |
| vd.add_argument("--no-spec-gen-tools", action="store_true", default=False, |
| help="Disable v2.2 spec_gen bounded tool-use branch.") |
| vd.add_argument("--no-realism-tools", action="store_true", default=False, |
| help="Disable realism check's bounded tool-use augmentation.") |
| vd.add_argument("--no-phase-3e-triage", action="store_true", default=False, |
| help="Disable Phase 3e triage even if env BMC_AGENT_ENABLE_PHASE_3E_TRIAGE=true.") |
| vd.add_argument("--minimal", action="store_true", default=False, |
| help=("Turn ALL default-on AI layers off. For " |
| "zero-LLM-cost smoke runs / ablations.")) |
| vd.add_argument( |
| "--follow-adjacent-rounds", |
| type=int, |
| default=0, |
| metavar="N", |
| help=( |
| "After the main sweep, harvest realism_check.adjacent_bugs[] from " |
| "every bug_report.json and re-run the pipeline on each referenced " |
| "function. Round-N outputs go to <output>/adjacent_round_N/. " |
| "Default 0 (disabled). Recommended: 1 for MVP." |
| ), |
| ) |
| _add_model_arg(vd) |
| _add_provider_args(vd) |
| vd.set_defaults(func=_cmd_verify_dir) |
|
|
| |
| au = subparsers.add_parser( |
| "autonomous", |
| help=( |
| "Run verify-dir in a round-based loop with auto-retry, " |
| "convergence detection, and per-round summaries. " |
| "Implements Phase 2 of PLAN_autonomous_mode.md." |
| ), |
| ) |
| au.add_argument("--source-dir", required=True, help="Directory containing .c files") |
| au.add_argument("--driver", required=True, help="Driver name prefix") |
| au.add_argument("--output", default="artifacts", help="Artifact directory") |
| au.add_argument( |
| "--include-dir", |
| action="append", |
| default=[], |
| metavar="DIR", |
| help="Add an include directory for C preprocessing (repeatable)", |
| ) |
| au.add_argument( |
| "--domain-knowledge", |
| default="", |
| metavar="TEXT_OR_FILE", |
| help="Domain knowledge string or path to a file", |
| ) |
| au.add_argument( |
| "--exclude", |
| action="append", |
| default=[], |
| metavar="PATTERN", |
| help="Glob pattern of filenames to skip (repeatable)", |
| ) |
| au.add_argument( |
| "--max-rounds", |
| type=int, |
| default=3, |
| help="Maximum number of autonomous rounds before stopping (default: 3)", |
| ) |
| au.add_argument( |
| "--target-coverage", |
| type=float, |
| default=0.80, |
| help="Stop early when per-file CBMC coverage reaches this fraction (default: 0.80)", |
| ) |
| au.add_argument( |
| "--enable-dynamic-validation", |
| action="store_true", |
| default=False, |
| help="Phase 3: compile + run a GCC harness to confirm bugs at runtime", |
| ) |
| au.add_argument( |
| "--real-libc", |
| action="store_true", |
| default=False, |
| help="Real-libc mode: harness #includes the source .c file and lets CBMC do all preprocessing via -I", |
| ) |
| au.add_argument( |
| "--raw-bytes", |
| action="store_true", |
| default=False, |
| help="Treat single char* / const char* params as raw byte buffers (no NUL termination)", |
| ) |
| au.add_argument( |
| "-D", "--define", |
| action="append", |
| default=[], |
| dest="defines", |
| help="Pass a preprocessor define to CBMC (repeatable). NAME or NAME=VALUE.", |
| ) |
| au.add_argument( |
| "--threat-model", |
| choices=["security", "safety", "functional"], |
| default="security", |
| help="Threat model: shapes CBMC baseline flags and realism context (default: security)", |
| ) |
| au.add_argument( |
| "--threat-model-context", |
| default=None, |
| metavar="PATH_OR_TEXT", |
| help="Trust-boundary note for THIS target (path to a file, or inline text): which inputs are attacker-controlled vs. caller/hardware-guaranteed. Injected into spec-gen, refinement, classifier, dynamic-validation and realism so the precondition is shaped correctly at generation time. Conservative default (treat inputs as attacker-controlled) applies when omitted.", |
| ) |
| au.add_argument( |
| "--allow-self-patch", |
| choices=["deny", "stage", "auto"], |
| default="deny", |
| help=( |
| "Phase 3 (self-patch agent) mode. 'deny' (default): the " |
| "agent is off and CBMC errors with no registered retry " |
| "action stay errored. 'stage': when Phase 2b exhausts its " |
| "actionable plans, the agent asks an LLM to propose a " |
| "patch to bmc_agent/harness_generator.py (or preprocessor.py) " |
| "plus a regression test; on passing all safety gates the " |
| "diff is written to <output>/<driver>/proposed_patches/ " |
| "for operator review (working tree stays clean). 'auto': " |
| "same as stage plus git-apply + commit (only after every " |
| "gate passes). See bmc_agent/self_patch_agent.py for the " |
| "gate logic." |
| ), |
| ) |
| _add_model_arg(au) |
| _add_provider_args(au) |
| au.set_defaults(func=_cmd_autonomous) |
|
|
| |
| spr = subparsers.add_parser( |
| "self-patch-review", |
| help=( |
| "Walk a sweep's ``proposed_patches/`` directory and print " |
| "a digest of every staged self-patch proposal — error " |
| "class, rationale, files touched, manual-apply commands. " |
| "Use this after an autonomous run with --allow-self-patch=stage." |
| ), |
| ) |
| spr.add_argument( |
| "--proposals-dir", |
| required=True, |
| metavar="DIR", |
| help=( |
| "Path to the proposed_patches directory (e.g. " |
| "<output>/<driver>/proposed_patches/)." |
| ), |
| ) |
| spr.add_argument( |
| "--show-diff", |
| action="store_true", |
| default=False, |
| help="Print the full unified diff for each proposal (default: just the digest)", |
| ) |
| spr.set_defaults(func=_cmd_self_patch_review) |
|
|
| |
| ev = subparsers.add_parser( |
| "eval", |
| help="Run AMC + baselines on a corpus of C programs (Phase 4)", |
| ) |
| ev.add_argument("--corpus", required=True, help="Path to corpus directory") |
| ev.add_argument("--output", default="artifacts/eval", help="Output directory for results") |
| ev.add_argument( |
| "--baselines", |
| action="store_true", |
| default=False, |
| help="Also run CBMC-alone and AMC-ablation baselines", |
| ) |
| ev.set_defaults(func=_cmd_eval) |
|
|
| |
| rpt = subparsers.add_parser( |
| "report", |
| help="Generate a summary report from evaluation artifacts (Phase 4)", |
| ) |
| rpt.add_argument("--eval-dir", required=True, help="Directory produced by 'amc eval'") |
| rpt.add_argument("--output", default="", help="Output file path (default: stdout)") |
| rpt.set_defaults(func=_cmd_report) |
|
|
| |
| corpus_p = subparsers.add_parser( |
| "corpus", |
| help="Corpus management commands (Phase 4)", |
| ) |
| corpus_sub = corpus_p.add_subparsers(dest="corpus_command", metavar="SUBCOMMAND") |
| corpus_sub.required = True |
|
|
| cg = corpus_sub.add_parser( |
| "generate", |
| help="Use LLM to generate synthetic C programs", |
| ) |
| cg.add_argument("--output", required=True, help="Output directory for generated corpus") |
| cg.add_argument("--count", type=int, default=5, help="Number of programs to generate") |
| cg.set_defaults(func=_cmd_corpus_generate) |
|
|
| |
| |
| |
| |
| jd = subparsers.add_parser( |
| "judge-dir", |
| help=( |
| "Simple LLM-as-judge mode: for each CBMC counterexample, hand " |
| "everything to one tool-using LLM call. No multi-stage pipeline." |
| ), |
| ) |
| jd.add_argument("--source-dir", required=True, help="Directory containing .c files") |
| jd.add_argument("--driver", required=True, help="Driver name prefix") |
| jd.add_argument("--output", default="judge_out", help="Artifact directory") |
| jd.add_argument("--include-dir", action="append", default=[], |
| help="Add include directory for preprocessing (repeatable)") |
| jd.add_argument("-D", "--define", dest="defines", action="append", default=[], |
| help="Preprocessor define (repeatable)") |
| jd.add_argument("--exclude", action="append", default=[], |
| help="Glob pattern of filenames to skip (repeatable)") |
| jd.add_argument("--cbmc-unwind", type=int, default=4) |
| jd.add_argument("--cbmc-timeout", type=int, default=60) |
| jd.add_argument("--max-functions", type=int, default=None, |
| help="Cap total functions judged (for smoke testing)") |
| jd.add_argument("--only-file", action="append", default=None, |
| help="Only run on these files (basename or stem; repeatable)") |
| jd.add_argument( |
| "--enable-flag-selection", |
| action="store_true", |
| default=False, |
| help="Phase 1.5: per-function LLM-picked CBMC flags (unsigned-overflow / " |
| "conversion / pointer-overflow). Default off.", |
| ) |
| jd.add_argument( |
| "--enable-feedback-loop", |
| action="store_true", |
| default=False, |
| help="Distill UNREALISTIC/UNCERTAIN verdicts into learned constraints " |
| "(persisted to <output>/<driver>/learned_constraints.json) " |
| "and apply them to subsequent harness gens. WARNING: can quietly " |
| "kill real bugs (see feedback_llm_as_judge memory).", |
| ) |
| jd.add_argument( |
| "--agentic-harness", |
| action="store_true", |
| default=False, |
| help="Use the LLM-driven harness builder (bmc_agent/agentic_harness_gen.py) " |
| "instead of the deterministic HarnessGenerator. The LLM reads " |
| "callees/callers, decides per-callee stub-vs-inline, sizes buffers " |
| "to match real callers, and emits a complete harness. Falls back " |
| "to deterministic gen on failure.", |
| ) |
| jd.add_argument( |
| "--refine-rounds", |
| type=int, |
| default=0, |
| metavar="N", |
| help="When the judge rules a CEx UNREALISTIC/UNCERTAIN and " |
| "--agentic-harness is on, hand verdict reasoning + harness + " |
| "witness back to the agentic generator and re-run CBMC up to N " |
| "rounds. Stops on REALISTIC, clean, or budget exhaustion. The " |
| "LLM (not a regex) decides whether/how to incorporate the " |
| "judge's reasoning, so this avoids the legacy feedback-loop " |
| "failure mode of regex-distilled __CPROVER_assume killing real " |
| "bugs. Default 0 (disabled). Recommended starting value: 1.", |
| ) |
| _add_model_arg(jd) |
| _add_provider_args(jd) |
| jd.set_defaults(func=_cmd_judge_dir) |
|
|
| return parser |
|
|
|
|
| def main(argv: list[str] | None = None) -> int: |
| parser = build_parser() |
| args = parser.parse_args(argv) |
| return args.func(args) |
|
|
|
|
| if __name__ == "__main__": |
| sys.exit(main()) |
|
|
